59da8a1f1f04971f709cfe0dd7b79d187ed4593b
[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         MEMALLOC
30 private:
31         void explore(thread_id_t tid);
32
33         ModelAction *action;
34         int num_threads;
35         std::vector< bool, MyAlloc<bool> > explored_children;
36         std::vector< bool, MyAlloc<bool> > backtrack;
37 };
38
39 typedef std::list<class Node *, MyAlloc< class Node * > > node_list_t;
40
41 class NodeStack {
42 public:
43         NodeStack();
44         ~NodeStack();
45         ModelAction * explore_action(ModelAction *act);
46         Node * get_head();
47         Node * get_next();
48         void reset_execution();
49
50         int get_total_nodes() { return total_nodes; }
51
52         void print();
53
54         MEMALLOC
55 private:
56         node_list_t node_list;
57         node_list_t::iterator iter;
58
59         int total_nodes;
60 };
61
62 #endif /* __NODESTACK_H__ */