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