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