Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker
[model-checker.git] / nodestack.h
1 #ifndef __NODESTACK_H__
2 #define __NODESTACK_H__
3
4 #include <list>
5 #include <vector>
6 #include <cstddef>
7 #include "threads.h"
8 #include "mymemory.h"
9
10 class ModelAction;
11
12 class Node {
13 public:
14         Node(ModelAction *act = NULL, int nthreads = 1);
15         ~Node();
16         /* return true = thread choice has already been explored */
17         bool has_been_explored(thread_id_t tid);
18         /* return true = backtrack set is empty */
19         bool backtrack_empty();
20         void explore_child(ModelAction *act);
21         /* return false = thread was already in backtrack */
22         bool set_backtrack(thread_id_t id);
23         thread_id_t get_next_backtrack();
24         bool is_enabled(Thread *t);
25         ModelAction * get_action() { return action; }
26
27         void print();
28
29         static int get_total_nodes() { return total_nodes; }
30
31         MEMALLOC
32 private:
33         void explore(thread_id_t tid);
34
35         static int total_nodes;
36         ModelAction *action;
37         int num_threads;
38         std::vector< bool, MyAlloc<bool> > explored_children;
39         std::vector< bool, MyAlloc<bool> > backtrack;
40 };
41
42 typedef std::list<class Node *, MyAlloc< class Node * > > node_list_t;
43
44 class NodeStack {
45 public:
46         NodeStack();
47         ~NodeStack();
48         ModelAction * explore_action(ModelAction *act);
49         Node * get_head();
50         Node * get_next();
51         void reset_execution();
52
53         void print();
54
55         MEMALLOC
56 private:
57         node_list_t node_list;
58         node_list_t::iterator iter;
59 };
60
61 #endif /* __NODESTACK_H__ */