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