1 | % (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
2 | % Heinrich Heine Universitaet Duesseldorf | |
3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
4 | ||
5 | :- module(state_space_open_nodes_c,[not_all_transitions_added/1, | |
6 | reset_open_ids/0, | |
7 | add_id_at_front/1, | |
8 | add_id_at_end/1, | |
9 | add_id_random/1, | |
10 | add_id_to_process/3, | |
11 | add_id_with_weight/2, | |
12 | pop_id_from_front_direct/1, | |
13 | pop_id_from_end_direct/1, | |
14 | pop_id_oldest_direct/1, | |
15 | retract_open_node_direct/1, | |
16 | ||
17 | open_ids_empty/0, | |
18 | ||
19 | retract_open_ids_with_statistics/0, | |
20 | print_state_space_open_nodes/0, | |
21 | assert_not_all_transitions_added/1, assert_not_all_z/1]). | |
22 | ||
23 | :- use_module(tools). | |
24 | :- use_module(debug). | |
25 | :- use_module(error_manager). | |
26 | :- use_module(module_information). | |
27 | :- module_info(group,animator). | |
28 | :- module_info(description,'This module keeps track of the unprocessed states queue of the model checker/animator.'). | |
29 | ||
30 | % Open Node Queue Interface | |
31 | % The interface for adding new ids and popping them from the list of open nodes: | |
32 | ||
33 | :- dynamic not_all_transitions_added/1. | |
34 | %not_all_transitions_added(v_0). | |
35 | ||
36 | ||
37 | :- use_module(myheap,'../extensions/myheap/myheap.pl',[myheap_init/0, | |
38 | myheap_reset/0, myheap_add_node/2, myheap_add_node_at_front/1, myheap_add_node_at_end/1, | |
39 | myheap_add_node_random/1, | |
40 | myheap_size/1, myheap_empty/1, myheap_isempty/0, | |
41 | myheap_top_id/1, myheap_top_weight/1, | |
42 | myheap_pop/1, | |
43 | ||
44 | myheap_max_weight/1, | |
45 | myheap_pop_max/1]). | |
46 | ||
47 | ||
48 | open_ids_empty :- myheap_empty(X),X==1. | |
49 | ||
50 | reset_open_ids :- myheap_init, retractall(ids_still_to_process(_,_,_)), | |
51 | retractall(not_all_transitions_added(_)). | |
52 | retract_open_ids_with_statistics :- | |
53 | retract_with_statistics(state_space_open_nodes, | |
54 | [not_all_transitions_added(_), ids_still_to_process(_,_,_)]), | |
55 | myheap_init. % To do: expand and compute statistics | |
56 | ||
57 | :- dynamic ids_still_to_process/3. %ids for which we still have to compute the heuristic function | |
58 | % purpose: delay the computation until all transitions have been added of PredecessorID | |
59 | ||
60 | add_id_to_process(ID,Hash,PredecessorID) :- | |
61 | assert(ids_still_to_process(ID,Hash,PredecessorID)), assert(not_all_transitions_added(ID)). | |
62 | ||
63 | process_ids :- retract(ids_still_to_process(ID,Hash,PredID)), % we assume ID cannot be root | |
64 | state_space:out_degree(PredID,Degree), % print(add_out_degree_id(ID,PredID,Degree)),nl, | |
65 | Weight is Degree*1000 + Hash mod 1000, | |
66 | % Weight = Degree, | |
67 | myheap_add_node(ID,Weight),fail. | |
68 | process_ids. | |
69 | ||
70 | ||
71 | add_id_at_front(root) :- !, | |
72 | myheap_add_node_at_front(-99), | |
73 | assertz(not_all_transitions_added(root)). | |
74 | add_id_at_front(NodeID) :- | |
75 | myheap_add_node_at_front(NodeID), | |
76 | % print_node(add_front,NodeID), | |
77 | assertz(not_all_transitions_added(NodeID)). | |
78 | ||
79 | ||
80 | add_id_at_end(root) :- !, myheap_add_node_at_end(-99), assert(not_all_transitions_added(root)). | |
81 | add_id_at_end(NodeID) :- myheap_add_node_at_end(NodeID), | |
82 | % print_node(add_end,NodeID), | |
83 | assertz(not_all_transitions_added(NodeID)). | |
84 | ||
85 | ||
86 | add_id_with_weight(root,W) :- !, myheap_add_node(-99,W), assert(not_all_transitions_added(root)). | |
87 | add_id_with_weight(ID,W) :- myheap_add_node(ID,W), assert(not_all_transitions_added(ID)). | |
88 | ||
89 | add_id_random(root) :- !, myheap_add_node_random(-99), assert(not_all_transitions_added(root)). | |
90 | add_id_random(ID) :- myheap_add_node_random(ID), assert(not_all_transitions_added(ID)). | |
91 | ||
92 | ||
93 | % pop id with the smallest weight: | |
94 | pop_id_from_front_direct(NodeID) :- nonvar(NodeID),!, | |
95 | add_internal_error('Illegal call: ', pop_id_from_front_direct(NodeID)),fail. | |
96 | pop_id_from_front_direct(RNodeID) :- process_ids, | |
97 | myheap_pop(ID), ID \= -1, | |
98 | translate_id(ID,NodeID), | |
99 | % print_node(pop_front,NodeID), | |
100 | (retract(not_all_transitions_added(NodeID)) -> RNodeID=NodeID | |
101 | ; % the node has been retracted directly and already been processed | |
102 | %print_message(no_node(NodeID)), | |
103 | pop_id_from_front_direct(RNodeID) % simply get the next node | |
104 | ). | |
105 | ||
106 | ||
107 | % pop id with the highest weight: | |
108 | pop_id_from_end_direct(NodeID) :- nonvar(NodeID),!, | |
109 | add_internal_error('Illegal call: ', pop_id_from_end_direct(NodeID)),fail. | |
110 | pop_id_from_end_direct(RNodeID) :- process_ids, | |
111 | myheap_pop_max(ID), ID \= -1, | |
112 | (ID= -99 -> NodeID=root ; NodeID=ID), | |
113 | %print_node(pop_end,NodeID), | |
114 | (retract(not_all_transitions_added(NodeID)) -> RNodeID=NodeID | |
115 | ; % the node has been retracted directly and already been processed | |
116 | print_message(node_already_processed(NodeID,ID)), | |
117 | pop_id_from_end_direct2(RNodeID) % simply get the next node | |
118 | ). | |
119 | pop_id_from_end_direct2(RNodeID) :- | |
120 | myheap_pop_max(ID), ID \= -1, | |
121 | (ID= -99 -> NodeID=root ; NodeID=ID), | |
122 | (retract(not_all_transitions_added(NodeID)) -> RNodeID=NodeID | |
123 | ; print_message(node_already_processed(NodeID,ID)), | |
124 | pop_id_from_end_direct(RNodeID) % simply get the next node | |
125 | ). | |
126 | ||
127 | % pop the oldest node | |
128 | pop_id_oldest_direct(NodeID) :- nonvar(NodeID),!, | |
129 | add_internal_error('Illegal call: ', pop_id_oldest_direct(NodeID)),fail. | |
130 | pop_id_oldest_direct(NodeID) :- | |
131 | retract(not_all_transitions_added(NodeID)). | |
132 | % in principle we should try and delete the node; but currently this cannot be done efficiently in the multi-map | |
133 | ||
134 | %print_node(Info,ID) :- state_space:visited_expression(ID,State), print(Info), print(' '),print(ID), print(' : '), print(State),nl. | |
135 | ||
136 | translate_id(-99,X) :- !, X=root. | |
137 | translate_id(X,X). | |
138 | ||
139 | ||
140 | retract_open_node_direct(NodeID) :- retract(not_all_transitions_added(NodeID)), | |
141 | (myheap_top_id(TID),translate_id(TID,NodeID) | |
142 | -> myheap_pop(_) | |
143 | ; debug_println(9,'Cannot delete node from C++ multimap yet; node will be ignored when popped'), | |
144 | debug_println(9,NodeID) | |
145 | % we would need to use another C++ datastructure (mymultimap.cpp ?) | |
146 | %Note: here we simply use the fact that not_all_transitions_added(NodeID) has been removed to indicate that a node has been removed | |
147 | ). | |
148 | ||
149 | ||
150 | not_all_transitions_added_saved(X) :- not_all_transitions_added(X). % to avoid name clashes; as consulting occurs in state_space module | |
151 | not_all_z_saved(_) :- fail. % just here for compatibility with Prolog version of Queue | |
152 | ||
153 | :- use_module(tools_printing, [print_dynamic_pred/3]). | |
154 | print_state_space_open_nodes :- print_message(saving), | |
155 | print_dynamic_pred(state_space_open_nodes_c,not_all_z_saved,1), | |
156 | print_dynamic_pred(state_space_open_nodes_c,not_all_transitions_added_saved,1), | |
157 | print_message('Cannot save open nodes C++ multimap yet; Node IDs will be reloaded in random order'). | |
158 | %print_dynamic_pred(state_space_open_nodes,not_all_z,1), | |
159 | ||
160 | % called to transfer nodes back here when loading saved stated in state_space.pl: | |
161 | assert_not_all_transitions_added(NodeID) :- add_id_random(NodeID). | |
162 | assert_not_all_z(_). % nothing to do: this information is not used with C version of queue |