1		% (c) 2009-2026 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,
6		[get_state_space_stats/3, get_state_space_stats/4,
7		gen_new_state_id/1,
8		history/1, forward_history/1,
9		get_action_trace/1, % old trace/1
10		get_action_trace_with_limit/2,
11		get_action_term_trace/1,
12		op_trace_ids/1, add_to_op_trace_ids/1, remove_from_op_trace_ids/1, reset_op_trace_ids/0,
13		get_state_id_trace/1,
14		current_state_id/1, current_expression/2,
15		set_current_state_id/1,
16		current_options/1, set_current_options/1,
17		get_current_predecessor_state_id/1,
18
19		add_id_at_front/1, add_id_at_end/1,
20		add_id_random/1, /* from state_space_open_nodes_c */
21		add_id_with_weight/2, add_id_to_process/3,
22		pop_id_from_front/1, pop_id_from_end/1, pop_id_oldest/1,
23		retract_open_node/1, open_ids_empty/0,
24		top_front_id/1, top_front_weight/1,
25
26		visited_expression/3, visited_expression/2, visited_expression_id/1,
27		find_hashed_packed_visited_expression/3,
28		retract_visited_expression/2,
29		not_all_transitions_added/1,
30		not_invariant_checked/1, set_invariant_checked/1,
31		invariant_not_yet_checked/1, invariant_still_to_be_checked/1,
32		not_interesting/1, % nodes ignored because they do not satisfy a user-provided scope predicate
33		mark_as_not_interesting/1,
34		max_reached_for_node/1,
35		max_reached_or_timeout_for_node/1,
36		use_no_timeout/1, time_out_for_node/1, time_out_for_node/3, virtual_time_out_for_node/1,
37		hash_to_id/2,id_to_marker/2, hash_to_nauty_id/2,
38		register_back_edge/2, try_compute_depth_of_state_id/2,
39		invariant_violated/1, time_out_for_invariant/1, time_out_for_assertions/1,
40		set_invariant_violated/1,
41
42		state_error_exists/0, state_error/3, store_state_error/3,
43		set_context_state/1, set_context_state/2,
44		update_context_state/1, clear_context_state/0, get_current_context_state/1,
45		store_error_for_context_state/2,
46		copy_current_errors_to_state/2,
47		store_abort_error_for_context_state_if_possible/4,
48		abort_error_exists_in_context_state/1,
49
50		transition/3,transition/4, any_transition/3,
51		store_transition/4,
52		deadlocked_state/1, % no outgoing edge
53		is_initial_state_id/1, is_concrete_constants_state_id/1,
54		multiple_concrete_constants_exist/0,
55		root_sufficiently_explored/0,
56		get_constants_state_for_id/2, get_constants_state_for_id/3,
57		get_constants_state_id_for_id/2,
58		try_get_unique_constants_state/1,
59		get_constants_id_for_state_id/2,
60		get_variables_state_for_id/2,
61		out_degree/2,
62		operation_not_yet_covered/1, operation_name_not_yet_covered/1,
63		get_operation_name_coverage_infos/4,
64		mark_operation_as_covered/1,
65		initialise_operation_not_yet_covered/0,
66
67		transition_info/2, store_transition_infos/2,
68		keep_transition_info/1, check_relevant_transition_info_stored/2,
69		compute_transitions_if_necessary/1,
70
71		state_space_initialise/0, state_space_initialise_with_stats/0,
72		state_space_reset/0,
73		state_space_add/2, state_space_packed_add/2,
74		delete_node/1,
75
76		current_state_corresponds_to_initialised_b_machine/0,
77		current_state_corresponds_to_fully_setup_b_machine/0,
78		current_state_corresponds_to_setup_constants_b_machine/0,
79		visited_state_corresponds_to_initialised_b_machine/1,
80		visited_state_corresponds_to_setup_constants_b_machine/1,
81
82		specialized_inv/2, %reuse_operation/4,
83		assert_max_reached_for_node/1, assert_time_out_for_node/3,
84		assert_time_out_for_invariant/1, assert_time_out_for_assertions/1,
85
86		set_max_nr_of_new_impl_trans_nodes/1,
87		get_max_nr_of_new_impl_trans_nodes/1,
88		impl_trans_term/3, impl_trans_term/4,
89		impl_trans_term_all/2,
90		impl_trans_id/4, impl_trans_not_complete/1,
91		compute_transitions_if_necessary_saved/1,
92		max_nr_of_new_nodes_limit_not_reached/0,
93
94		find_trace_to_initial_state/2, find_initialised_states/1,
95
96		tcltk_save_state_space/1, tcltk_load_state/1,
97		compute_full_state_space_hash/1,
98
99		execute_id_trace_from_current/1, execute_id_trace_from_current/3,
100		set_trace_by_transition_ids/1, try_set_trace_by_transition_ids/1,
101		extend_trace_by_transition_ids/1,
102		extract_term_trace_from_transition_ids/2,
103
104		add_counterexample_node/1, add_counterexample_op/1,
105		reset_counterexample/0, set_counterexample_by_transition_ids/1,
106		counterexample_node/1, counterexample_op/1, % specific predicates to register counter examples
107
108		portray_history/0
109		]).
110
111		:- use_module(library(lists)).
112
113		:- use_module(self_check).
114		:- use_module(error_manager).
115		:- use_module(gensym).
116		:- use_module(preferences).
117		:- use_module(tools).
118		:- use_module(debug,[debug_println/1, debug_println/2]).
119		%:- use_module(state_space_exploration_modes,[compute_hash/3]).
120
121		:- use_module(extension('counter/counter'),
122		[counter_init/0, new_counter/1, get_counter/2, inc_counter/1, inc_counter/2, inc_counter_by/2, reset_counter/1, set_counter/2]).
123
124		:- use_module(module_information).
125		:- module_info(group,state_space).
126		:- module_info(description,'This module keeps track of the visited states by the animator/model checker.').
127
128		% ----------------------------------
129
130		:- load_files(library(system), [when(compile_time), imports([environ/2])]).
131		:- if((environ(prob_myheap,false) ; \+ predicate_property(load_foreign_resource(_), _))).
132		:- use_module(state_space_open_nodes). %% comment in to use only Prolog datastructures
133		:- else.
134		:- use_module(state_space_open_nodes_c). %% comment in to use C++ multimap queue; can make use of HEURISTIC_FUNCTION
135		:- endif.
136
137		% ----------------------------------
138
139		get_state_space_stats(NrNodes,NrTransitions,ProcessedNodes) :-
140		get_counter(states,N), NrNodes is N+1,
141		get_counter(transitions,NrTransitions),
142		get_counter(processed_nodes,ProcessedNodes).
143
144		get_state_space_stats(NrNodes,NrTransitions,ProcessedNodes,IgnoredNodes) :-
145		get_state_space_stats(NrNodes,NrTransitions,ProcessedNodes),
146		get_counter(not_interesting_nodes,IgnoredNodes).
147
148		gen_new_state_id(Nr) :-
149		inc_counter(states,N1), Nr is N1-1. % only one C call
150		%get_counter(states,Nr), inc_counter(states).
151		reset_state_counter :- reset_counter(states).
152		reset_state_counter(Nr) :- set_counter(states,Nr).
153
154		get_state_id_trace(StateIds) :-
155		history(History),
156		current_state_id(CurID),
157		reverse([CurID|History],StateIds).
158
159		get_current_predecessor_state_id(PriorID) :-
160		history([PriorID|_]).
161
162		:- dynamic history/1.
163		history([]).
164
165
166		:- dynamic forward_history/1.
167
168		:- dynamic current_state_id/1.
169		current_state_id(root).
170		/* INITIAL STATE, third arg: clp(fd) constraints as generated
171		by fd_copy_term */
172
173		current_expression(ID,State) :- current_state_id(ID),
174		visited_expression(ID,State).
175		current_packed_expression(ID,State) :- current_state_id(ID),
176		packed_visited_expression(ID,State).
177
178		:- use_module(specfile,[state_corresponds_to_initialised_b_machine/1,
179		state_corresponds_to_fully_setup_b_machine/1,
180		state_corresponds_to_set_up_constants/1]).
181		current_state_corresponds_to_initialised_b_machine :-
182		current_packed_expression(_,PS), unpack_state_top_level(PS,TLState),
183		state_corresponds_to_initialised_b_machine(TLState).
184		visited_state_corresponds_to_initialised_b_machine(ID) :-
185		packed_visited_expression(ID,PS), unpack_state_top_level(PS,TLState),
186		state_corresponds_to_initialised_b_machine(TLState).
187
188		current_state_corresponds_to_fully_setup_b_machine :-
189		current_packed_expression(_,PS), unpack_state_top_level(PS,TLState),
190		state_corresponds_to_fully_setup_b_machine(TLState).
191
192		current_state_corresponds_to_setup_constants_b_machine :-
193		current_packed_expression(_,PS), unpack_state_top_level(PS,TLState),
194		state_corresponds_to_set_up_constants(TLState).
195
196		visited_state_corresponds_to_setup_constants_b_machine(ID) :-
197		packed_visited_expression(ID,PS), unpack_state_top_level(PS,TLState),
198		state_corresponds_to_set_up_constants(TLState).
199
200		:- dynamic current_options/1.
201		current_options([]).
202
203		set_current_options(Options) :-
204		retractall( current_options(_) ),
205		assertz( current_options(Options) ).
206
207		:- dynamic packed_visited_expression/2.
208		%packed_visited_expression(v_0,true).
209
210		:- use_module(state_packing).
211
212		retract_visited_expression(ID,State) :- retract(packed_visited_expression(ID,PState)),
213		unpack_state(PState,State).
214
215		retractall_visited_expression(ID) :- retractall(packed_visited_expression(ID,_)).
216
217		state_space_packed_add(Id,PackedTerm) :- assertz(packed_visited_expression(Id,PackedTerm)).
218
219		state_space_add(Id,Term) :-
220		(pack_state(Term,PackedTerm) -> assertz(packed_visited_expression(Id,PackedTerm))
221		; add_internal_error('State packing failed: ',pack_state(Term,_)),
222		assertz(packed_visited_expression(Id,Term))).
223
224		% deprecated:
225		visited_expression(ID,State,true) :- visited_expression(ID,State).
226		% not call(CurBody); for the moment we always have true as last argument
227
228	?	visited_expression(A,B) :- packed_visited_expression(A,PB),
229		(unpack_state(PB,R) -> B=R ; add_internal_error('Unpacking state failed: ',unpack_state(PB,R)),R=A).
230
231		%visited_expression_id(A) :- packed_visited_expression(A,_). % avoid unpacking state
232		% even better: not to look up fact at all to avoid constructing state term, this is done below:
233		:- use_module(library(between),[between/3]).
234		visited_expression_id(ID) :- number(ID),!, ID>=0, get_counter(states,N), ID<N.
235		visited_expression_id(ID) :- ID==root,!.
236		visited_expression_id(root).
237	?	visited_expression_id(Nr) :- Nr \== root, get_counter(states,N), N1 is N-1, between(0,N1,Nr).
238
239		% given a hash and a packed state: find ID (fail if does not exist)
240		find_hashed_packed_visited_expression(Hash,PackedState,ID) :-
241		hash_to_id(Hash,ID),
242		(packed_visited_expression(ID,PackedState)
243		-> true /* warning: may instantiate State if not ground */
244		; functor(PackedState,concrete_constants,1),
245		preference(maxNrOfInitialisations,Max), Max =< 4
246		-> debug_println(19,hash_collision_for_constants(Hash,ID)),fail
247		% this is not too bad if maxNrOfInitialisations small;
248		% can happen due to depth limit in term_depth_hash in compute_hash
249		; formatsilent('* hash collision for id=~w hash=~w~n',[ID,Hash]),fail
250		).
251
252
253		:- dynamic not_invariant_checked/1.
254		set_invariant_checked(ID) :- %print(inv_checked(ID)),nl,
255		retract(not_invariant_checked(ID)).
256
257		invariant_not_yet_checked(ID) :-
258		not_all_transitions_added(ID) ; /* assumption: if not all transitions added then we haven't checked invariant yet */
259		not_invariant_checked(ID) ;
260		not_interesting(ID). % assumption: if a node is marked as not interesting it will not be examined
261
262		% difference with invariant_not_yet_checked: not interesting nodes not reported and cannot be backtracked
263		invariant_still_to_be_checked(ID) :-
264		(not_all_transitions_added(ID) -> true ; not_invariant_checked(ID) -> true).
265
266		:- dynamic not_interesting/1.
267		%not_interesting(v_0).
268
269		:- dynamic max_reached_for_node/1.
270		/* true if not all outgoing transistions were computed due to the limit
271		on the number of operations/initialisations computed */
272		:- dynamic time_out_for_node/3, use_no_timeout/1, time_out_for_invariant/1, time_out_for_assertions/1.
273
274		time_out_for_node(ID) :- (var(ID) -> visited_expression_id(ID) ; true),
275		(time_out_for_node(ID,_,_) -> true ; fail).
276
277		% only succeeds for virtual time_outs
278		virtual_time_out_for_node(ID) :- (var(ID) -> visited_expression_id(ID) ; true),
279		(time_out_for_node(ID,_,virtual_time_out) -> true ; fail).
280
281		:- dynamic transition/4.
282		%transition(v_0,a,1,v_1).
283
284		store_transition(Org,Action,Dest,Id) :-
285		%get_counter(transitions,Id), inc_counter(transitions),
286		inc_counter(transitions,Id1), Id is Id1-1, % only one C call
287		assertz(transition(Org,Action,Id,Dest)).
288
289	?	deadlocked_state(Origin) :- \+ any_transition(Origin,_,_).
290
291		is_concrete_constants_state_id(ID) :-
292	?	logical_transition_from_root(ID),
293		packed_visited_expression(ID,PState), % Note: in CSP||B mode there is no csp_and_b wrapper
294		unpack_state_top_level(PState,concrete_constants(_)).
295
296		% get the transition to the first logical successor to root, jumping over start_cspm_MAIN in CSP||B mode
297		logical_transition_from_root(ID) :-
298	?	transition(root,T,_TransId,ID1),
299		(T=start_cspm_MAIN, csp_with_bz_mode
300		-> transition(ID1,_,_,ID) % the first logical successor of root is a successor of ID1
301		; ID1=ID
302		).
303
304		% check if we have explored a successor of root node to find constants (or initial state if no constants exist)
305		% i.e., did we compute successors of root, and in case of CSP||B did we from there set up constants or initialise machine
306		root_sufficiently_explored :-
307		transition(root,T,_TransId,ID1),!,
308		(T=start_cspm_MAIN, csp_with_bz_mode
309		-> \+ not_all_transitions_added(ID1)
310		; true
311		).
312
313		% check if we have multiple constant setups
314		multiple_concrete_constants_exist :-
315	?	is_concrete_constants_state_id(ID),
316	?	is_concrete_constants_state_id(ID2), ID2 \= ID,!.
317
318
319		is_initial_state_id(InitialStateID) :-
320		logical_transition_from_root(State),
321		packed_visited_expression(State,P),
322		(P = concrete_constants(_) % also covers '$partial_setup_constants'
323		-> state_space:transition(State,_,InitialStateID)
324		; InitialStateID=State).
325
326		% get the constants for a state (if there are constants), avoid unpacking variables
327		get_constants_state_for_id(ID,CS) :- get_constants_state_for_id(ID,[],CS).
328		get_constants_state_for_id(ID,Opts,ConstantsState) :-
329		packed_visited_expression(ID,PState),
330		unpack_state_top_level(PState,TLState),
331		(get_const_and_vars_id(TLState,CID) -> get_constants_state_for_id(CID,[],ConstantsState)
332		; unpack_state(PState,UPState),
333		(UPState = concrete_constants(CS) -> ConstantsState=CS
334		; UPState = [_|_], member(allow_variable_list,Opts),
335		ConstantsState=UPState,
336		% could be that we have a state where constants and variables are mixed in a single list
337		% e.g., ProB2's FindStateCommand does currently not create new intermediate constant states
338		add_message(get_constants_state_for_id,'State is a list of bindings and has no reference to a constant valuation: ',ID)
339		)
340		).
341
342		get_const_and_vars_id(const_and_vars(CID,_),CID).
343		get_const_and_vars_id(csp_and_b(_,BState),CID) :- get_const_and_vars_id(BState,CID).
344
345		% get the state id for associated constants state for a state (if there are constants)
346		get_constants_state_id_for_id(ID,CstID) :-
347		packed_visited_expression(ID,PState),
348		unpack_state_top_level(PState,TLState),
349		get_constants_id_for_id_aux(TLState,ID,CstID).
350		get_constants_id_for_id_aux(concrete_constants(_),ID,ID).
351		get_constants_id_for_id_aux(const_and_vars(ID,_),_,ID).
352		get_constants_id_for_id_aux(csp_and_b(_,BState),ID,CstID) :- get_constants_id_for_id_aux(BState,ID,CstID).
353
354		get_variables_state_for_id(ID,VarState) :-
355		visited_expression(ID,State),
356		get_vars_aux(State,VarState).
357		%get_vars_aux(concrete_constants(ConstantsState),[]).
358		get_vars_aux(const_and_vars(_,Vars),State) :- !, State=Vars.
359		get_vars_aux([],[]).
360		get_vars_aux([H|T],[H|T]).
361
362		% check if there is a unique constants state:
363		try_get_unique_constants_state(ConstantsState) :-
364		logical_transition_from_root(DestID),
365		\+ (logical_transition_from_root(DestID2), DestID2 \= DestID), % no other transition exists
366		\+ max_reached_or_timeout_for_node(root),
367		DestID \= root, % DestID=root should never happen
368		get_constants_state_for_id(DestID,ConstantsState).
369
370		% returns id of constants state for a state (if it exists)
371		get_constants_id_for_state_id(ID,ConstID) :-
372		packed_visited_expression(ID,PState),
373		get_cstid_from_vars(PState,ConstID).
374
375		get_cstid_from_vars('$cst_vars'(ConstID,_),ConstID). % const_and_vars are always converted to this
376		get_cstid_from_vars(csp_and_b(_,B),ConstID) :- get_cstid_from_vars(B,ConstID).
377
378	?	any_transition(Origin,TransID,Destination) :- transition(Origin,_,TransID,Destination).
379
380	?	transition(Origin,Action,Destination) :- transition(Origin,Action,_TransID,Destination).
381
382		:- dynamic transition_info/2.
383		store_transition_infos([],_TransId).
384		store_transition_infos([Info|Irest],TransId) :-
385		store_transition_info(Info,TransId),
386		store_transition_infos(Irest,TransId).
387		store_transition_info(Info,TransId) :- %print(info(Info,TransId)),nl,
388		(keep_transition_info(Info)
389		-> assertz(transition_info(TransId,Info))
390		; true).
391
392		% Do not store path info by default
393		keep_transition_info(path(_)) :- !,
394		preference(eventtrace,true). % STORE_DETAILED_TRANSITION_INFOS
395		keep_transition_info(eventtrace(_)) :- !,preference(eventtrace,true).
396		keep_transition_info(event(_)) :- !,
397		preference(store_event_transinfo,true). % store info about parameters and abstract Rodin events
398		keep_transition_info(_). % store everything else
399
400		% check if all relevant transition infos have been stored for a transition
401		check_relevant_transition_info_stored([],_).
402		check_relevant_transition_info_stored([Info|Irest],TransId) :-
403		(keep_transition_info(Info) -> transition_info(TransId,Info) ; true),
404		check_relevant_transition_info_stored(Irest,TransId).
405
406
407		reset_transition_store :-
408		retractall(transition(_,_,_,_)),
409		retractall(transition_info(_,_)),
410		reset_counter(transitions),
411		reset_counterexample.
412
413		/*
414		Version with packing of transitions:
415		store_transition(Org,Action,Dest,Id) :-
416		retract(transition_counter(Id)),
417		NewId is Id+1,
418		assertz(transition_counter(NewId)),
419		Action =.. [ActionName|Parameters],
420		pack_values(Parameters,PackedParameters),
421		assertz(packed_transition(Org,ActionName,PackedParameters,Id,Dest)).
422
423		transition(Origin,Action,TransID,Destination) :- nonvar(Action),!,
424		Action =.. [ActionName|Parameters],
425		packed_transition(Origin,ActionName,PackedParameters,TransID,Destination),
426		unpack_values(PackedParameters,Parameters).
427		transition(Origin,Action,TransID,Destination) :-
428		packed_transition(Origin,ActionName,PackedParameters,TransID,Destination),
429		unpack_values(PackedParameters,Parameters),
430		Action =.. [ActionName|Parameters].
431		any_transition(Origin,TransID,Destination) :- packed_transition(Origin,_,_,TransID,Destination).
432		*/
433
434		% compute out-degree of a node
435		out_degree(ID,OutDegree) :- findall(0, transition(ID,_,_,_), L), length(L,OutDegree).
436
437		operation_name_not_yet_covered(OpName) :- operation_not_yet_covered(OpName).
438
439
440		get_operation_name_coverage_infos(PossibleNr,FeasibleNr,UncovNr,UncoveredList) :-
441		findall(ON, specfile:get_possible_event(ON), Possible), length(Possible,PossibleNr),
442		findall(OF, specfile:get_feasible_event(OF), Feasible), length(Feasible,FeasibleNr),
443		findall(OpName, state_space: operation_name_not_yet_covered(OpName), UncoveredList),
444		length(UncoveredList,UncovNr).
445
446
447		:- dynamic operation_not_yet_covered/1.
448		%operation_not_yet_covered(b).
449
450		:- use_module(probsrc(debug),[formatsilent/2]).
451		mark_operation_as_covered(OpName) :-
452		(operation_not_yet_covered(OpName), % small improvement in B/PerformanceTests/ModelChecking/EnumSetLookups.mch
453		retract(operation_not_yet_covered(OpName))
454		-> (preferences:get_preference(provide_trace_information,true)
455		-> formatsilent('Covered ~w~n',[OpName])
456		; true),
457	?	(operation_not_yet_covered(_) -> true ; formatsilent('~nALL OPERATIONS COVERED~n',[]))
458		; true
459		).
460
461		:- use_module(bmachine,[b_top_level_operation/1]).
462		:- use_module(probcspsrc(haskell_csp),[channel/2]).
463		initialise_operation_not_yet_covered :- retractall(operation_not_yet_covered(_)),
464		b_or_z_mode,
465	?	b_top_level_operation(Name),
466		% b_get_machine_operation(Name,_,Par,_), length(Par,Arity), functor(Op,Name,Arity),
467		% Note: no '-->' added
468		assertz(operation_not_yet_covered(Name)),
469		fail.
470		/* Missing: treat operations with return values */
471		initialise_operation_not_yet_covered :- csp_mode, \+ csp_with_bz_mode,
472		channel(Name,_),
473		assertz(operation_not_yet_covered(Name)),
474		fail.
475		initialise_operation_not_yet_covered.
476
477		state_error_exists :- state_error(_,_,_),!.
478		:- dynamic state_error/3.
479
480		%state_error([],invariant_violated).
481
482		reset_next_state_error_id_counter :- reset_counter(next_state_error_id).
483		:- use_module(tools_printing, [print_error/1, format_error_with_nl/2]).
484		:- use_module(error_manager,[print_error_span/1]).
485		store_state_error(State,Error,Id) :- state_error(State,Id,Error),!. % do not store identical error twice
486		store_state_error(State,Error,Id) :-
487		%retract( next_state_error_id(Id) ),
488		inc_counter(next_state_error_id,Id),
489		% tools_printing:print_term_summary(Error),nl, tools_printing:nested_print_term(Error),nl,
490		assertz( state_error(State,Id,Error) ).
491		store_error_for_context_state(Error,Id) :-
492		( context_state(State,Errs) ->
493		(Errs<25
494		-> store_state_error(State,Error,Id), E1 is Errs+1,
495		%assertz(context_state(State,E1))
496		set_context_number_of_errors(E1)
497		; store_state_error(State,max_state_errors_reached(25),Id)
498		)
499		;
500		add_internal_error('No known context when calling store_error_for_context_state: ',store_error_for_context_state(Error,Id)),
501		fail).
502
503		% check if we already have a certain type of error in the current context state
504		abort_error_exists_in_context_state(ErrType) :- get_current_context_state(State),
505		Error = abort_error(ErrType,_Msg,_Term,_Pos),
506		state_error(State,_Id,Error).
507
508		% copy current errors from error_manager to state errors
509		copy_current_errors_to_state(StateID,Context) :-
510		% error_manager:logged_error(Source,ErrMsg,_Context,Span), % will not retract
511		error_manager:get_error_with_span(Source,ErrMsg,Span), % will retract
512		store_state_error(StateID,abort_error(Source,ErrMsg,'',span_context(Span,Context)),SID),
513		% TO DO: use other error class
514		debug_println(4,stored_state_error(Source,SID,_Context,ErrMsg)),
515		fail.
516		copy_current_errors_to_state(_,_).
517
518		store_abort_error_for_context_state_if_possible(ErrType,Msg,Term,Span) :-
519		%print(store(Msg,Term,Span)),nl,
520		( get_current_context_state(State) ->
521		error_manager:get_error_context(Context),
522		(abort_error_for_same_location_exists(State,Id1,ErrType,Msg,Span),
523		abort_error_for_same_location_exists(State,Id2,ErrType,Msg,Span),
524		Id2>Id1
525		-> /* two errors of same type, for same state and same source location exists */
526		/* TO DO: maybe merge state errors */
527		simplify_span(Span,Span1),
528		compress_span(Span1,Span2),
529		store_state_error(State,abort_error(ErrType,'Further identical errors occurred (not stored !)',Term,span_context(Span2,Context)),_)
530		;
531		format_error_with_nl('! An error occurred in state ~w: ~w !',[State,ErrType]),
532		% usual errors: precondition_error, while_invariant_violation, while_variant_error,
533		% assert_error, well_definedness_error, card_overflow_error
534		print_error(Msg),
535		print_error_term(Term,Span),
536		% print_error(context_state_id(State)), % printed by print_error_context
537		print_error_context,
538		(debug_mode(on),visited_expression(State,S) -> translate:translate_bstate(S,O),print_error(O) ; true),
539		compress_span(Span,Span2),
540		print_error_span(Span2),
541		store_state_error(State,abort_error(ErrType,Msg,Term,span_context(Span2,Context)),_)
542		),
543		(add_new_event_in_error_scope(abort_error(ErrType)) -> true ; true), % should we use well_definedness_error?
544		assert_real_error_occurred(abort_error) % Note that in this case the error manager list of errors maybe empty even though real_error_occured is true. (see ProB2 kernel test de.prob.cli.integration.rules.RulesMachineTest > testReuseStateSpace)
545		; % no current context_state exists:
546		compress_span(Span,Span2),
547		add_error(ErrType,Msg,Term,Span2)
548		).
549
550
551		:- use_module(bsyntaxtree, [find_identifier_uses/3]).
552		compress_span(span_context(Span,C),span_context(CS,C)) :- !,
553		compress_span(Span,CS).
554		compress_span(pos_context(Span1,C,Span2),pos_context(CS1,C,CS2)) :- !,
555		compress_span(Span1,CS1),
556		compress_span(Span2,CS2).
557		compress_span(span_predicate(Pred,LS,S),Res) :- find_identifier_uses(Pred,[],Ids),
558		sort(Ids,SIds),
559		filter_state(LS,SIds,FLS),
560		filter_state(S,SIds,FS), % TODO: do we need to store the global state? we can reconstruct it ?
561		% format('Compressed span_predicate (~w)~n',[Ids]),
562		!,
563		Res = span_predicate(Pred,FLS,FS).
564		compress_span(S,S).
565		% avoid storing large useless values
566		% TO DO: probably we should stop storing spans when a certain threshold of number of errors is reached
567
568
569		:- use_module(library(ordsets),[ord_member/2]).
570		filter_state([],_,[]).
571		filter_state([bind(ID,L)|T],Vars,Res) :-
572		(ord_member(ID,Vars) -> Res = [bind(ID,L)|RT] ; Res=RT),
573		filter_state(T,Vars,RT).
574
575
576		:- use_module(translate, [translate_error_term/3]).
577		print_error_term(T,S) :- (var(T);var(S)),!,
578		print_error('### VARIABLE error term or span:'), print_error(print_error_term(T,S)).
579		print_error_term(Term,Span) :- translate_error_term(Term,Span,S),
580		(S='' -> true ; print_error(S)).
581
582		abort_error_for_same_location_exists(State,Id,ErrType,Msg,Span) :-
583		state_error(State,Id,abort_error(ErrType,Msg,_Term2,span_context(Span2,_Ctxt2))),
584		same_span_location(Span2,Span).
585		% should be moved to error_manager ?
586		same_span_location(span_context(Span1,C),span_context(Span2,C)) :- !, same_span_location(Span1,Span2).
587		same_span_location(pos_context(Span1,C,_),pos_context(Span2,C,_)) :- !,
588		same_span_location(Span1,Span2). % should we check second span?
589		same_span_location(span_predicate(Pred1,_,_),span_predicate(Pred2,_,_)) :- !,Pred1=Pred2.
590		same_span_location(X,X).
591
592		:- dynamic saved_nested_context_state/2.
593		save_nested_context_state(_S) :-
594		bb_get(state_space_context_state,ID),
595		bb_get(state_space_context_errors,Errs),!,
596		%print(saving_context_state(_S,ID,Errs)),nl,
597		asserta(saved_nested_context_state(ID,Errs)).
598		save_nested_context_state(_).
599
600		% actually pops context state
601		clear_context_state :-
602		retract(saved_nested_context_state(ID,Errs)),!, %print(restoring_nested(ID,Errs)),nl,
603		bb_put(state_space_context_state,ID),
604		bb_put(state_space_context_errors,Errs).
605		clear_context_state :-
606		(bb_delete(state_space_context_state,_) -> true ; true).
607		%(retract(context_state(_,_)) -> true ; true). % retractall seems to be slowing down with use
608
609		% Note: Each Prolog module maintains its own blackboard for bb_get/bb_put
610		context_state(ID,Errs) :-
611		bb_get(state_space_context_state,ID), bb_get(state_space_context_errors,Errs).
612
613		% sets a new context state; pushing the previous one if necessary
614		set_context_state(State) :- %print(set_id(State)),nl,
615		save_nested_context_state(State),
616		bb_put(state_space_context_state,State),
617		bb_put(state_space_context_errors,0).
618
619		set_context_state(State,_Context) :- % Context can be used for debugging later
620		set_context_state(State).
621
622		% update current context state, without storing nested states
623		update_context_state(State) :-
624		bb_put(state_space_context_state,State),
625		bb_put(state_space_context_errors,0).
626
627		get_current_context_state(ID) :- bb_get(state_space_context_state,ID).
628		%get_current_context_state(ID) :- context_state(ID,_).
629
630		set_context_number_of_errors(Errs) :- bb_put(state_space_context_errors,Errs).
631
632		retractall_invariant_violated(State) :-
633		retractall(state_error(State,_,invariant_violated)).
634		invariant_violated(State) :-
635		state_error(State,_,invariant_violated).
636		set_invariant_violated(State) :-
637		( invariant_violated(State) -> true
638		; time_out_for_invariant(ID) -> print('Timeout for node: '), print(ID),nl,
639		print('Not setting invariant violation status'),nl
640		; store_state_error(State,invariant_violated,_)
641		).
642
643		%:- set_invariant_violated([]). % why is this ??
644
645
646		:- dynamic hash_to_id/2.
647		:- dynamic id_to_marker/2.
648		:- dynamic id_back_edge/3. % optional facts to keep track where a state was constructed from
649
650		:- dynamic hash_to_nauty_id/2. % used in nauty mode to map nauty id's to hash values
651
652		:- dynamic specialized_inv/2. /* stores whether for a node a specialized invariant
653		version could be computed */
654
655		% :- dynamic reuse_operation/4. /* when for a state and given operation name we can reuse the operation computed for another state */
656		% used to be used for OPERATION_REUSE TRUE
657
658		:- use_module(hashing).
659		state_space_startup :- % call once at startup to ensure all counters exist
660		counter_init,
661		new_counter(states), new_counter(processed_nodes), new_counter(transitions),
662		new_counter(next_state_error_id),
663		new_counter(not_interesting_nodes),
664		reset_open_ids. % also calls myheap init
665		state_space_initialise :- counter_init, reset_gennum, reset_gensym,
666		new_counter(states), new_counter(processed_nodes), new_counter(transitions),
667		new_counter(next_state_error_id), new_counter(not_interesting_nodes),
668		reset_state_counter, reset_processed_nodes_counter, reset_next_state_error_id_counter,
669		retractall_visited_expression(_),
670		reset_open_ids,
671		reset_stored_values, % state_packing
672		retractall(not_invariant_checked(_)),
673		reset_not_interesting,
674		retractall(max_reached_for_node(_)),
675		retractall(time_out_for_node(_,_,_)),
676		retractall(time_out_for_invariant(_)),
677		retractall(time_out_for_assertions(_)),
678		retractall(use_no_timeout(_)),
679		retractall(state_error(_,_,_)),
680		clear_context_state,
681		reset_transition_store,
682		retractall(operation_not_yet_covered(_)),
683		retractall(hash_to_id(_,_)),
684		retractall(id_back_edge(_,_,_)),
685		retractall(hash_to_nauty_id(_,_)),
686		retractall(id_to_marker(_,_)),
687		retractall(specialized_inv(_,_)),
688		%retractall(reuse_operation(_,_,_,_)),
689		state_space_add(root,root),
690		add_id_at_front(root),
691		my_term_hash(root,RootHash),
692		assertz(hash_to_id(RootHash,root)),
693		%assertz(not_invariant_checked(root)),
694		state_space_reset.
695
696		:- use_module(eventhandling,[register_event_listener/3]).
697		:- register_event_listener(startup_prob,state_space_startup,
698		'Initialise Statespace Counters.').
699		:- register_event_listener(reset_specification,state_space_initialise,
700		'Reset Statespace.').
701		:- register_event_listener(change_of_animation_mode,state_space_initialise,
702		'Reset Statespace.').
703		:- register_event_listener(specification_initialised,initialise_operation_not_yet_covered,
704		'Init coverage info.').
705		:- register_event_listener(reset_prob,state_space_initialise,
706		'Reset Statespace.').
707
708		/* A version of reset which checks how much memory is used by each fact */
709		/* state_space:init_with_stats */
710		state_space_initialise_with_stats :-
711		reset_gennum, reset_gensym, reset_state_counter, reset_processed_nodes_counter,
712		reset_next_state_error_id_counter,
713		retract_open_ids_with_statistics,
714		retract_with_statistics(state_space,[packed_visited_expression(_,_),
715		not_invariant_checked(_),
716		not_interesting(_),
717		max_reached_for_node(_),
718		time_out_for_node(_,_,_),
719		time_out_for_invariant(_),
720		time_out_for_assertions(_),
721		use_no_timeout(_),
722		state_error(_,_,_),
723		transition(_,_,_,_),
724		transition_info(_,_),
725		operation_not_yet_covered(_),
726		hash_to_id(_,_),
727		hash_to_nauty_id(_,_),
728		id_to_marker(_,_),
729		specialized_inv(_,_),
730		%reuse_operation(_,_,_,_),
731		history(_), forward_history(_), op_trace_ids(_)]),
732		reset_not_interesting,
733		retract_stored_values_with_statistics,
734		clear_context_state,
735		reset_transition_store,
736		state_space_add(root,root),
737		add_id_at_front(root),
738		%assertz(not_invariant_checked(root)),
739		state_space_reset,
740		initialise_operation_not_yet_covered.
741
742
743
744		:- dynamic op_trace_ids/1.
745		reset_trace :- retractall(op_trace_ids(_)), assertz(op_trace_ids([])).
746		get_action_trace(T) :- trace(T).
747		get_action_term_trace(PT) :- get_action_trace_with_limit(0,T), project_on_action_term(T,PT).
748		trace(Trace) :- get_action_trace_with_limit(500,Trace).
749		get_action_trace_with_limit(Limit,Trace) :-
750		op_trace_ids(IDT), reverse(IDT,RIDT),
751		extract_trace_from_transition_ids(RIDT,root,Limit,[],Trace).
752
753		reset_op_trace_ids :- retractall(op_trace_ids(_)), assertz(op_trace_ids([])).
754		add_to_op_trace_ids(OpID) :- retract(op_trace_ids(OpIDS)), assertz(op_trace_ids([OpID|OpIDS])).
755		remove_from_op_trace_ids(OpID) :- retract(op_trace_ids(OpIDS)),
756		(OpIDS = [R|Rest]
757		-> assertz(op_trace_ids(Rest)), OpID = R
758		; assertz(op_trace_ids(OpIDS)), fail).
759
760		% translate a list of transition ids (from root) into a list of operation terms
761		extract_term_trace_from_transition_ids(TransIDListFromRoot,Trace) :-
762		extract_trace_from_transition_ids(TransIDListFromRoot,root,0,[],ActionTrace),
763		reverse_and_project_on_action_term(ActionTrace,[],Trace).
764
765		reverse_and_project_on_action_term([],A,A).
766		reverse_and_project_on_action_term([action(_,Term)|T],Acc,Res) :- !,
767		reverse_and_project_on_action_term(T,[Term|Acc],Res).
768		reverse_and_project_on_action_term([H|T],Acc,Res) :-
769		add_error(reverse_and_project_on_action_term,'Illegal action: ',H),
770		reverse_and_project_on_action_term(T,[H|Acc],Res).
771
772		project_on_action_term([],[]).
773		project_on_action_term([action(_,Term)|T],Res) :- !, Res=[Term|TR],
774		project_on_action_term(T,TR).
775		project_on_action_term([H|T],Res) :-
776		add_error(project_on_action_term,'Illegal action: ',H),
777		project_on_action_term(T,Res).
778
779		extract_trace_from_transition_ids([],_CurrentState,_,Trace,Trace).
780		extract_trace_from_transition_ids([TransId|Rest],CurrentState,Limit,AccTrace,Trace) :-
781		compute_op_string(TransId,CurrentState,Limit,OpTerm,OpString,DestState),!,
782		extract_trace_from_transition_ids(Rest,DestState,Limit,
783		[action(OpString,OpTerm)|AccTrace],Trace).
784		extract_trace_from_transition_ids([TransId|_],CurrentState,_,_,_Trace) :-
785		add_error(state_space,'Could not execute transition id: ', TransId:from(CurrentState)),fail.
786
787		:- use_module(translate,[translate_event_with_src_and_target_id/5]).
788		compute_op_string(jump(TO),_CurID,_,Term,String,DestID) :- !, Term=jump,String=jump,DestID=TO.
789		compute_op_string(TransId,CurID,Limit,Term,String,DestID) :- transition(CurID,Term,TransId,DestID),
790		translate_event_with_src_and_target_id(Term,CurID,DestID,Limit,String).
791
792		% reset history and forward history, but not state-space itself
793		state_space_reset :-
794		reset_trace,
795		retractall(history(_)),
796		retractall(forward_history(_)),
797		retractall(current_state_id(_)),
798		retractall(current_options(_)),
799		assertz(history([])),
800		assertz(current_state_id(root)).
801
802		reset_not_interesting :- retractall(not_interesting(_)), reset_counter(not_interesting_nodes).
803
804		mark_as_not_interesting(ID) :- assertz(not_interesting(ID)), inc_counter(not_interesting_nodes).
805
806		set_current_state_id(ID) :- (retract(current_state_id(_)) -> true ; true),
807		assertz(current_state_id(ID)).
808
809		state_space_clean_all :-
810		retractall(state_space_version_in_file(_)),
811		retractall_visited_expression(_),
812		reset_open_ids,
813		retractall(not_invariant_checked(_)),
814		reset_not_interesting,
815		retractall(max_reached_for_node(_)),
816		retractall(time_out_for_node(_,_,_)),
817		retractall(time_out_for_invariant(_)),
818		retractall(time_out_for_assertions(_)),
819		retractall(use_no_timeout(_)),
820		retractall(state_error(_,_,_)),
821		clear_context_state,
822		reset_transition_store,
823		retractall(operation_not_yet_covered(_)),
824		retractall(hash_to_id(_,_)),
825		retractall(id_back_edge(_,_,_)),
826		retractall(hash_to_nauty_id(_,_)),
827		retractall(id_to_marker(_,_)),
828		retractall(specialized_inv(_,_)),
829		%retractall(reuse_operation(_,_,_,_)),
830		retractall(history(_)),
831		retractall(forward_history(_)),
832		retractall(op_trace_ids(_)),
833		retractall(current_state_id(_)),
834		retractall(current_options(_)).
835
836		% this is only used from within the Tcl/Tk animator at the moment:
837		delete_node(ID) :- print(deleting(ID)),nl,
838		retractall_visited_expression(ID),
839		retractall_invariant_violated(ID),
840		retract_open_node_and_update_processed_nodes(ID),
841		retractall(not_invariant_checked(ID)),
842		(retract(not_interesting(ID)) -> inc_counter_by(not_interesting_nodes,-1) ; true),
843		retractall(max_reached_for_node(ID)),
844		retractall(time_out_for_node(ID,_,_)),
845		retractall(time_out_for_invariant(ID)),
846		retractall(time_out_for_assertions(ID)),
847		retractall(use_no_timeout(ID)),
848		retractall(state_error(ID,_,_)),
849		retractall(transition(ID,_,_,_)),
850		% to do: check if operation_not_yet_covered(_) changes
851		retract_hash(ID),
852		retractall(id_to_marker(ID,_)).
853
854		retract_hash(ID) :- retract(hash_to_id(Hash,ID)), retractall(hash_to_nauty_id(_TermHash,Hash)),fail.
855		retract_hash(_).
856
857		% assert max_operations reachoed
858		assert_max_reached_for_node(Id) :- %print_message(max_reached_for_node(Id)),
859		(max_reached_for_node(Id) -> true ; assertz(max_reached_for_node(Id))).
860
861		:- use_module(probsrc(debug),[debug_mode/1]).
862		assert_time_out_for_node(Id,OpName,TypeOfTimeOut) :-
863		(debug_mode(off),functor(TypeOfTimeOut,virtual_time_out,_) -> true % can easily happen when parameters are unbounded
864		; print_message(time_out_for_node(Id,OpName,TypeOfTimeOut))),
865		(time_out_for_node(Id,OpName,_) -> true ; assertz(time_out_for_node(Id,OpName,TypeOfTimeOut))).
866		assert_time_out_for_invariant(Id) :- print_message(time_out_for_invariant(Id)),
867		(time_out_for_invariant(Id) -> true ; assertz(time_out_for_invariant(Id))).
868		assert_time_out_for_assertions(Id) :- print_message(time_out_for_assertions(Id)),
869		(time_out_for_assertions(Id) -> true ; assertz(time_out_for_assertions(Id))).
870
871		max_reached_or_timeout_for_node(Id) :-
872		(max_reached_for_node(Id) ; time_out_for_node(Id,_,_)).
873		/* ---------------------- */
874		/* state space saving */
875		/* ---------------------- */
876
877		:- dynamic state_space_version_in_file/1. %
878		state_space_version(1).
879
880		check_state_space_version :- state_space_version(V),
881		(state_space_version_in_file(F) -> true ; F=0),
882		(V>F -> add_message(state_space,'Warning: saved state_space may be incompatible with current version: ',F:V) ; true).
883
884		% save all infos of state space (transitions, evaluated invariants, ...)
885		tcltk_save_state_space(File) :-
886		print('% saving full state space to: '), print(File),nl,
887		open(File,write,Stream,[encoding(utf8)]),
888		print_state_space(Stream),
889		close(Stream),
890		print_message(done).
891
892
893		:- use_module(tools_printing, [print_dynamic_fact/2,print_dynamic_pred/4]).
894		print_state_space(Stream) :-
895		state_space_version(V),
896		print_dynamic_fact(Stream,state_space_version_in_file(V)),
897		% TO DO: maybe also save some important preferences, and warn user and/or propose to adapt preferences ?
898		print_dynamic_pred(Stream,state_space,history,1),
899		print_dynamic_pred(Stream,state_space,forward_history,1),
900		print_dynamic_pred(Stream,state_space,op_trace_ids,1),
901		print_dynamic_pred(Stream,state_space,current_state_id,1),
902		print_dynamic_pred(Stream,state_space,current_options,1),
903		print_dynamic_pred(Stream,state_space,packed_visited_expression,2),
904		print_dynamic_pred(Stream,state_space,not_invariant_checked,1),
905		print_dynamic_pred(Stream,state_space,not_interesting,1),
906		print_dynamic_pred(Stream,state_space,max_reached_for_node,1),
907		print_dynamic_pred(Stream,state_space,time_out_for_node,3),
908		print_dynamic_pred(Stream,state_space,use_no_timeout,1),
909		print_dynamic_pred(Stream,state_space,transition,4),
910		print_dynamic_pred(Stream,state_space,transition_info,2),
911		print_dynamic_pred(Stream,state_space,operation_not_yet_covered,1),
912		print_dynamic_pred(Stream,state_space,state_error,3),
913		print_state_space_open_nodes(Stream),
914		print_stored_values(Stream),
915		get_counter(states,X),
916		write_term(Stream,saved_gennum_count(X),[quoted(true)]),write(Stream,'.'),nl(Stream).
917
918		saved_gennum_count(99999).
919
920		/* ---------------------- */
921		/* state space loading */
922		/* ---------------------- */
923
924		tcltk_load_state(File) :- state_space_clean_all,
925		print('Loading: '), print(File),nl,
926		user_consult_without_redefine_warning(File), % this will read in bind_skeleton/2, ..., next_value_id/1
927		check_state_space_version,
928		print('Generating open node info'),nl,
929		transfer_open_node_info,
930		print('Transfer state packing info'),nl,
931		transfer_state_packing_info,
932		print('Recomputing hash index'),nl,
933		recompute_all_hash,
934		(saved_gennum_count(X) -> reset_state_counter(X) ; true),
935		reset_processed_nodes_counter, % TO DO: restore or save it
936		reset_next_state_error_id_counter, % DITTO
937		print('Done'),nl,!.
938		tcltk_load_state(File) :-
939		add_error(tcltk_load_state,'Could not load state from file: ',File),
940		state_space_initialise.
941
942		:- dynamic not_all_z_saved/1, not_all_transitions_added_saved/1.
943		:- dynamic bind_skeleton/2, stored_value/2, stored_value_hash_to_id/2, next_value_id/1.
944
945		% transfer facts read into state_space into other modules:
946		transfer_open_node_info :- retract(not_all_z_saved(X)), %print(not_all_z(X)),nl,
947		assert_not_all_z(X),fail.
948		transfer_open_node_info :- retract(not_all_transitions_added_saved(X)),
949		assert_not_all_transitions_added(X),fail.
950		transfer_open_node_info.
951		% now for transferring to state_packing module info generated by print_stored_values
952		transfer_state_packing_info :- retract(bind_skeleton(X,Y)), %print(skel(X)),nl,
953		assertz(state_packing:bind_skeleton(X,Y)),fail.
954		transfer_state_packing_info :- retract(stored_value(X,Y)),
955		assertz(state_packing:stored_value(X,Y)),fail.
956		transfer_state_packing_info :- retract(stored_value_hash_to_id(X,Y)),
957		assertz(state_packing:stored_value_hash_to_id(X,Y)),fail.
958		transfer_state_packing_info :- retract(next_value_id(X)),
959		state_packing:set_next_value_id(X),fail.
960		transfer_state_packing_info.
961
962		recompute_all_hash :-
963		retractall(hash_to_id(_,_)),retractall(id_to_marker(_,_)),
964		retractall(hash_to_nauty_id(_,_)),
965		visited_expression(ID,StateTemplate),
966		state_space_exploration_modes:compute_hash(StateTemplate,Hash,Marker),
967		assertz(hash_to_id(Hash,ID)),
968		assertz(id_to_marker(ID,Marker)),
969		fail.
970		recompute_all_hash.
971
972		:- use_module(hashing,[my_term_hash/2]).
973		% generates a hash for the entire state space not depending on the order in which states where added
974		compute_full_state_space_hash(Hash) :-
975		%listing(hash_to_id/2), listing(packed_visited_expression/2),
976		findall(Hash,hash_to_id(Hash,_),ListOfHashCodes),
977		sort(ListOfHashCodes,SortedList),
978		my_term_hash(SortedList,Hash).
979		% TO DO: also provide transition hashes
980
981		:- use_module(tools_meta,[safe_on_exception/3]).
982		user_consult_without_redefine_warning(File) :-
983		get_set_optional_prolog_flag(redefine_warnings, Old, off),
984		get_set_optional_prolog_flag(single_var_warnings, Old2, off),
985		(safe_on_exception(Exc,
986		%consult(File), %
987		load_files([File], [load_type(source),compilation_mode(consult),encoding(utf8)]),
988		(nl,print('Exception occurred:'),print(Exc),nl,fail))
989		-> OK=true ; OK=false),
990		get_set_optional_prolog_flag(redefine_warnings, _, Old),
991		get_set_optional_prolog_flag(single_var_warnings, _, Old2),
992		OK=true.
993
994		% execute a transition id list from current ID and update animator history,...
995		execute_id_trace_from_current(OperationIDList) :-
996		current_state_id(CurID),
997		get_state_list_from_opids(OperationIDList,CurID,StateIDList,NewCurID),
998		execute_id_trace_from_current(NewCurID,OperationIDList,StateIDList).
999
1000		get_state_list_from_opids([],CurID,[],CurID).
1001		get_state_list_from_opids([TransId|TO],CurID,[NextCurID|TS],FinalCurID) :-
1002		transition(CurID,_,TransId,NextCurID),
1003		get_state_list_from_opids(TO,NextCurID,TS,FinalCurID).
1004
1005
1006		% execute_id_trace_from_current(NewCurID,OperationIDList,StateIDList)
1007		execute_id_trace_from_current(ID,OpIDL,StateIDList) :-
1008		current_state_id(CurID),
1009		reverse([CurID|StateIDList],Rev),
1010		Rev = [Dest|TRev],
1011		(Dest==ID -> true ; print(not_eq(Dest,ID)),nl),
1012		retract(history(H)),
1013		update_forward_history(OpIDL), % check if OpIDL conforms to forward history and keep it
1014		append(TRev,H,NewH),
1015		assertz(history(NewH)),
1016		retract(op_trace_ids(OldTrace)),
1017		reverse(OpIDL,NewTrace),
1018		append(NewTrace,OldTrace,Trace),
1019		assertz(op_trace_ids(Trace)),
1020		retractall(current_state_id(_)),
1021		assertz(current_state_id(ID)).
1022		%execute_trace_to_node(OpL,StateIDList). /* <----- BOTTLENECK FOR LONG SEQUENCES */
1023		%generate_trace([],Acc,Acc).
1024		%generate_trace([OpTerm|T],Acc,Res) :-
1025		% translate:translate_event(OpTerm,OpString),
1026		% generate_trace(T,[action(OpString,OpTerm)|Acc],Res).
1027
1028		update_forward_history(TransitionIds) :-
1029		(retract(forward_history(Forward)),
1030		prune_forward_history(TransitionIds,Forward,NewForward)
1031		-> assert(forward_history(NewForward))
1032		; true).
1033		% try and prune forward history if it matches operation trace
1034		prune_forward_history([],ForwardHistory,ForwardHistory).
1035		prune_forward_history([TransID|T],[forward(_,TransID)|TF],Res) :-
1036		prune_forward_history(T,TF,Res).
1037
1038		try_set_trace_by_transition_ids(TransIds) :-
1039		(set_trace_by_transition_ids(TransIds) -> true
1040		; add_internal_error('Call failed:',set_trace_by_transition_ids(TransIds))).
1041
1042		set_trace_by_transition_ids(TransitionIds) :-
1043		extract_history_from_transition_ids(TransitionIds,root,[],[],Last,History,OpTrace),
1044		%visited_expression(Last,LastState,LastCond),
1045		retractall(history(_)),
1046		retractall(forward_history(_)), % TODO: we could try and recover a new forward history if transition ids match current history^forward history
1047		update_forward_history(TransitionIds),
1048		retractall(current_state_id(_)),
1049		retractall(op_trace_ids(_)),
1050		assertz(history(History)),
1051		assertz(op_trace_ids(OpTrace)),
1052		assertz(current_state_id(Last)).
1053
1054
1055		extract_history_from_transition_ids([],CurrentState,History,Trace,CurrentState,History,Trace).
1056		extract_history_from_transition_ids([TransId|Rest],CurrentState,AccHist,AccTrace,Last,History,Trace) :-
1057		transition(CurrentState,_,TransId,DestState),!,
1058		extract_history_from_transition_ids(Rest,DestState,[CurrentState|AccHist],
1059		[TransId|AccTrace],Last,History,Trace).
1060		extract_history_from_transition_ids([skip|Rest],CurrentState,AccHist,AccTrace,Last,History,Trace) :- !,
1061		extract_history_from_transition_ids(Rest,CurrentState,AccHist,AccTrace,Last,History,Trace).
1062		extract_history_from_transition_ids([TransId|_],CurrentState,_,_,_,_,_Trace) :-
1063		add_error(state_space,'Could not execute transition id: ', TransId:from(CurrentState)),fail.
1064
1065		% extend trace from current state
1066		extend_trace_by_transition_ids(TransitionIds) :-
1067		current_state_id(CurID),
1068		history(OldH), op_trace_ids(OldOT),
1069		extract_history_from_transition_ids(TransitionIds,CurID,OldH,OldOT,Last,History,OpTrace),
1070		retractall(history(_)), retractall(forward_history(_)),
1071		retractall(current_state_id(_)),
1072		retractall(op_trace_ids(_)),
1073		assertz(history(History)),
1074		assertz(op_trace_ids(OpTrace)),
1075		assertz(current_state_id(Last)).
1076
1077		/* --------------------------------- */
1078		:- dynamic max_nr_of_new_nodes/1.
1079
1080		% negative number or non-number signifies no limit
1081		set_max_nr_of_new_impl_trans_nodes(MaxNrOfNewNodes) :-
1082		retractall(max_nr_of_new_nodes(_)),
1083		(number(MaxNrOfNewNodes), MaxNrOfNewNodes>=0
1084		-> assertz(max_nr_of_new_nodes(MaxNrOfNewNodes))
1085		; true). % no need to store limit; we will explore as much as needed
1086
1087		get_max_nr_of_new_impl_trans_nodes(MaxNrOfNewNodes) :-
1088		(max_nr_of_new_nodes(Max) -> MaxNrOfNewNodes=Max; MaxNrOfNewNodes = 0).
1089
1090		% used e.g., in refinement or ltl checker
1091		impl_trans_term(From,ActionAsTerm,TransID,To) :-
1092		compute_transitions_if_necessary_saved(From),
1093		transition(From,ActionAsTerm,TransID,To).
1094		impl_trans_term(From,ActionAsTerm,To) :-
1095		compute_transitions_if_necessary_saved(From),
1096		transition(From,ActionAsTerm,_TID,To).
1097
1098		% a variation also giving the transition id:
1099		impl_trans_id(From,ActionAsTerm,TransitionID,To) :-
1100		compute_transitions_if_necessary_saved(From),
1101		transition(From,ActionAsTerm,TransitionID,To).
1102
1103		impl_trans_term_all(From,Ops) :-
1104		compute_transitions_if_necessary_saved(From),
1105		findall(op(Id,ActionAsTerm,To),
1106		transition(From,ActionAsTerm,Id,To),
1107		Ops).
1108
1109		% true if e.g., a time-out occurred during computation of all transitions
1110		impl_trans_not_complete(From) :- max_reached_or_timeout_for_node(From).
1111
1112		compute_transitions_if_necessary_saved(From) :-
1113		catch(
1114		compute_transitions_if_necessary(From),
1115		error(forced_interrupt_error('User has interrupted the current execution'),_),
1116		user_interrupts:process_interrupted_error_message).
1117
1118		:- use_module(tcltk_interface,[compute_all_transitions_if_necessary/2]).
1119		compute_transitions_if_necessary(From) :-
1120		not_all_transitions_added(From),!,
1121		decrease_max_nr_of_new_nodes(From),
1122		compute_all_transitions_if_necessary(From,false).
1123		compute_transitions_if_necessary(_From).
1124
1125		decrease_max_nr_of_new_nodes(ID) :-
1126		retract(max_nr_of_new_nodes(Max)),!,
1127		( Max>0 ->
1128		NewMax is Max-1,
1129		assertz(max_nr_of_new_nodes(NewMax))
1130		; Max=0 -> NM is -1,
1131		assertz(max_nr_of_new_nodes(NM)),
1132		add_warning(state_space,'Maximum number of new nodes reached for CTL/LTL/refinement check, node id = ',ID),
1133		fail
1134		; % negative number: re-assert and fail
1135		assertz(max_nr_of_new_nodes(Max)),
1136		fail).
1137		decrease_max_nr_of_new_nodes(_). % no limit stored; just proceed
1138
1139		% will be called from TCL/TK side
1140		max_nr_of_new_nodes_limit_not_reached :-
1141		max_nr_of_new_nodes(N),N>0.
1142
1143		:- use_module(specfile,[b_or_z_mode/0, csp_mode/0, csp_with_bz_mode/0]).
1144		retract_open_node(NodeID) :- retract_open_node_and_update_processed_nodes(NodeID),
1145		(b_or_z_mode -> assertz(not_invariant_checked(NodeID)) ; true).
1146
1147		reset_processed_nodes_counter :- reset_counter(processed_nodes).
1148		%reset_processed_nodes_counter(Nr) :- set_counter(processed_nodes,Nr).
1149
1150		retract_open_node_and_update_processed_nodes(NodeID) :-
1151		retract_open_node_direct(NodeID),
1152		inc_processed.
1153
1154		inc_processed :-
1155		inc_counter(processed_nodes).
1156
1157		pop_id_from_front(ID) :- pop_id_from_front_direct(ID), inc_processed.
1158		pop_id_from_end(ID) :- pop_id_from_end_direct(ID), inc_processed.
1159	?	pop_id_oldest(ID) :- pop_id_oldest_direct(ID), inc_processed.
1160
1161
1162
1163		/* --------------------------------- */
1164
1165		% find initialised states; very similar to is_initial_state_id/1
1166		% but is used by ltl/ctl/sap
1167		% TO DO: merge these two variations of the same concept
1168
1169		:- use_module(specfile,[animation_mode/1]).
1170
1171		find_initialised_states(Init) :-
1172		animation_mode(Mode),
1173		( init_states_mode_cst_init(Mode) ->
1174		findall(I,find_init1(root,I,_),Init)
1175		; init_states_mode_one_step(Mode) ->
1176		next_states_from_root(Init)
1177		;
1178		fail).
1179
1180		% find trace to some initialised state
1181		find_trace_to_initial_state(Target,Trace) :- animation_mode(Mode),
1182		find_aux(Mode,Target,Trace).
1183		find_aux(Mode,Target,[root,Target]) :-
1184		init_states_mode_one_step(Mode).
1185		find_aux(Mode,Target,[root|Trace]) :-
1186		init_states_mode_cst_init(Mode),
1187		find_init1(root,Target,Trace).
1188
1189
1190		init_states_mode_cst_init(b).
1191		init_states_mode_cst_init(z).
1192		init_states_mode_cst_init(csp_and_b).
1193
1194		init_states_mode_one_step(csp).
1195		init_states_mode_one_step(cspm).
1196		init_states_mode_one_step(xtl).
1197		%init_states_mode_one_step(promela).
1198
1199		next_states_from_root(States) :-
1200		impl_trans_term_all(root,Ops),
1201		findall(S, member(op(_Id,_,S),Ops), States).
1202
1203		find_init1(Start,Init,Trace) :- Start==Init,!,Trace=[]. % usually called with Start=Init=root
1204		find_init1(Start,Init,[State|Rest]) :-
1205		impl_trans_term(Start,O,State),
1206		find_init2(O,State,Init,Rest).
1207		find_init2(O,Init,Init,[]) :-
1208		has_functor_and_maybe_tau(O,'$initialise_machine').
1209		find_init2(O,State,Init,Path) :-
1210		has_functor_and_maybe_tau(O,F),
1211		(F='$setup_constants' ; F='$partial_setup_constants'),
1212		find_init1(State,Init,Path).
1213		find_init2(start_cspm_MAIN,State,Init,Path) :-
1214		find_init1(State,Init,Path).
1215		find_init2(start_cspm(_Proc),State,Init,Path) :-
1216		find_init1(State,Init,Path).
1217
1218		% has_functor_and_maybe_tau(Term,Functor)
1219		% checks if Term has the form "Functor(...)" or "tau(Functor(...))"
1220		% this is used for CSP||B specification where the initialisation is wrapped with
1221		% in a tau operator
1222		has_functor_and_maybe_tau(tau(Term),Functor) :-
1223		has_functor_and_maybe_tau(Term,Functor),!.
1224		has_functor_and_maybe_tau(Term,Functor) :-
1225		functor(Term,Functor,_).
1226
1227		% compute how far the state is from the root node using back_edge markers (if available)
1228		try_compute_depth_of_state_id(root,R) :- !, R=0.
1229		try_compute_depth_of_state_id(Node,Depth) :- id_back_edge(Node,Depth,_Back).
1230
1231		% optional registering of back_edges: to quickly find trace from root and to computed depth/diameter
1232		register_back_edge(ID,FromID) :-
1233		try_compute_depth_of_state_id(FromID,D),!,
1234		D1 is D+1,
1235		assertz(id_back_edge(ID,D1,FromID)).
1236		register_back_edge(ID,FromID) :- write(cannot_store_back_edge(ID,FromID)),nl.
1237
1238		/* --------------------------------- */
1239
1240		%
1241		% Code to compute equivalence classes
1242		% using the standard DFA minimization algorithm
1243
1244		:- dynamic equivalent/2.
1245		% state_space:compute_equivalence_classes
1246		:- public compute_equivalence_classes/0.
1247
1248		compute_equivalence_classes :- init_equi,
1249		split_equivalence_classes,nl,
1250		print_equi.
1251
1252		print_equi :- state_space:equivalent(A,B), visited_expression(A,State),
1253		visited_expression(B,StateB),
1254		nl,
1255		print(A), print(' : '), print(State),nl,
1256		print(B), print(' : '), print(StateB),nl,fail.
1257		print_equi.
1258
1259		init_equi :- retractall(equivalent(_,_)),
1260		packed_visited_expression(ID,_State),
1261		\+ not_all_transitions_added(ID),
1262		findall(Action,transition(ID,Action,_,_),List),
1263		packed_visited_expression(ID2,_S2), ID2 @> ID,
1264		\+ not_all_transitions_added(ID2),
1265		findall(Action,transition(ID2,Action,_,_),List),
1266		assertz(equivalent(ID,ID2)), % they have the same signature
1267		%print(equivalent(ID,ID2)),nl,
1268		fail.
1269		init_equi :- print(finished_initialising),nl.
1270
1271		split_equivalence_classes :- retractall(echange),
1272		equivalent(ID1,ID2),
1273		transition(ID1,A,_,Dest1),
1274		transition(ID2,A,_,Dest2),
1275		\+ check_equi(Dest1,Dest2),
1276		retract(equivalent(ID1,ID2)), % splitting class
1277		% print(diff(ID1,ID2, A, Dest1, Dest2)),nl,
1278		assert_echange,
1279		fail.
1280		split_equivalence_classes :- echange -> split_equivalence_classes ; true.
1281
1282		:- dynamic echange/0.
1283		assert_echange :- echange -> true ; assertz(echange),print('.'),flush_output.
1284
1285		check_equi(A,B) :- A=B -> true ; A @<B -> equivalent(A,B) ; equivalent(B,A).
1286
1287		/*
1288		% benchmark how much time it takes to copy the state space state_space:bench_state_space.
1289		bench_state_space :-
1290		statistics(walltime,_),
1291		(state_space:packed_visited_expression(ID,S), assertz(pve(ID,S)),fail ; true),
1292		statistics(walltime,[_,Delta]), format('Time to copy packed_visited_expression: ~w ms~n',[Delta]),
1293		(state_space:transition(A,B,C,D), assertz(tr(A,B,C,D)),fail ; true),
1294		statistics(walltime,[_,Delta2]), format('Time to copy transition: ~w ms~n',[Delta2]),
1295		(state_packing:stored_value(A,B), assertz(sv(A,B)),fail ; true),
1296		(state_packing:stored_value_hash_to_id(A,B), assertz(svhi(A,B)),fail ; true),
1297		statistics(walltime,[_,Delta3]), format('Time to copy stored_value: ~w ms~n',[Delta3]).
1298		*/
1299
1300		:- public portray_state_space/0.
1301		portray_state_space :- packed_visited_expression(ID,S), functor(S,F,N),
1302		format('State ~w : ~w/~w~n',[ID,F,N]), fail.
1303		portray_state_space :- transition(ID,Action,TransID,DestID),
1304		format(' ~w: ~w -- ~w --> ~w~n',[TransID,ID,Action,DestID]),fail.
1305		portray_state_space.
1306
1307
1308		portray_history :- op_trace_ids(List), length(List,Len),
1309		format('History of length ~w:~n',[Len]), reverse(List,His),
1310		portray_op_trace_ids(His,1,root).
1311		portray_op_trace_ids([],_,_CurrentState) :- !.
1312		portray_op_trace_ids([TransId|Rest],Step,CurrentState) :-
1313		compute_op_string(TransId,CurrentState,200,_OpTerm,OpString,DestState),!,
1314		format('~w: ~w -- ~w --> ~w : ~w~n',[Step,CurrentState,TransId,DestState,OpString]),
1315		S1 is Step+1,
1316		portray_op_trace_ids(Rest,S1,DestState).
1317		portray_op_trace_ids(L,Step,CurrentState) :-
1318		format('### Cannot print history from step ~w at state ~w:~n~w~n',[Step,CurrentState,L]).
1319
1320		bench_state_space :- statistics(walltime,[W1,_]),
1321		(packed_visited_expression(_,_), fail ; true),
1322		statistics(walltime,[W2,_]), T1 is W2-W1,
1323		format('Time to inspect all states: ~w ms walltime~n',[T1]),
1324		(visited_expression(_,_), fail ; true),
1325		statistics(walltime,[W3,_]), T2 is W3-W2,
1326		format('Time to inspect and unpack all states: ~w ms walltime~n',[T2]),
1327		(transition(_,_,_,_), fail ; true),
1328		statistics(walltime,[W4,_]), T3 is W4-W3,
1329		format('Time to inspect all transitions: ~w ms walltime~n',[T3]),
1330		(visited_expression(_,E), my_term_hash(E,_), fail ; true),
1331		statistics(walltime,[W5,_]), T4 is W5-W4,
1332		format('Time to inspect, unpack and hash all states: ~w ms walltime~n',[T4]).
1333
1334		% ----------------------------
1335		% COUNTER EXAMPLE MANAGEMENT
1336
1337		% store counter example nodes and transition ids; used by LTL model checking for example
1338
1339
1340		:- dynamic counterexample_node/1.
1341		:- dynamic counterexample_op/1.
1342
1343		add_counterexample_node(NodeID) :- assertz(counterexample_node(NodeID)).
1344		add_counterexample_op(TransID) :-
1345		(counterexample_op(TransID) -> true ; assertz(counterexample_op(TransID))).
1346
1347
1348		reset_counterexample :-
1349		retractall(counterexample_node(_)),
1350		retractall(counterexample_op(_)).
1351
1352		:- register_event_listener(play_counterexample,reset_counterexample,
1353		'Reset marked nodes from previous counterexamples.').
1354
1355		set_counterexample_by_transition_ids(TransIds) :-
1356		set_trace_by_transition_ids(TransIds),
1357		maplist(add_counterexample_op,TransIds),
1358		extract_history_from_transition_ids(TransIds,root,[],[],_Last,History,_OpTrace),
1359		maplist(add_counterexample_node,History).