1		% (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(state_space,
6		[get_state_space_stats/3, gen_new_state_id/1,
7		history/1, forward_history/1,
8		get_action_trace/1, % old trace/1
9		get_action_term_trace/1,
10		op_trace_ids/1, add_to_op_trace_ids/1, remove_from_op_trace_ids/1, reset_op_trace_ids/0,
11		get_state_id_trace/1,
12		current_state_id/1, current_expression/2,
13		current_options/1, set_current_options/1,
14
15		add_id_at_front/1, add_id_at_end/1,
16		add_id_random/1, /* from state_space_open_nodes_c */
17		add_id_with_weight/2, add_id_to_process/3,
18		pop_id_from_front/1, pop_id_from_end/1, pop_id_oldest/1,
19		retract_open_node/1, open_ids_empty/0,
20
21		visited_expression/3, visited_expression/2, visited_expression_id/1,
22		find_hashed_packed_visited_expression/3,
23		retract_visited_expression/2,
24		not_all_transitions_added/1,
25		not_invariant_checked/1, set_invariant_checked/1,
26		invariant_not_yet_checked/1,
27		not_interesting/1,max_reached_for_node/1,
28		max_reached_or_timeout_for_node/1,
29		use_no_timeout/1, time_out_for_node/1, time_out_for_node/3,
30		hash_to_id/2,id_to_marker/2, hash_to_nauty_id/2,
31		invariant_violated/1, time_out_for_invariant/1, time_out_for_assertions/1,
32		set_invariant_violated/1,
33
34		state_error_exists/0, state_error/3, store_state_error/3,
35		set_context_state/1, clear_context_state/0, get_current_context_state/1,
36		store_error_for_context_state/2,
37		store_abort_error_for_context_state_if_possible/4,
38
39		transition/3,transition/4, any_transition/3,
40		store_transition/4,
41		deadlocked_state/1, % no outgoing edge
42		is_initial_state_id/1, is_concrete_constants_state_id/1,
43		multiple_concrete_constants_exist/0,
44		out_degree/2,
45		operation_not_yet_covered/1, operation_name_not_yet_covered/1,
46
47		transition_info/2, store_transition_infos/2,
48		compute_transitions_if_necessary/1,
49
50		state_space_initialise/0, state_space_initialise_with_stats/0,
51		state_space_reset/0,
52		state_space_add/2, state_space_packed_add/2,
53		delete_node/1,
54
55		current_state_corresponds_to_initialised_b_machine/0,
56		current_state_corresponds_to_fully_setup_b_machine/0,
57		current_state_corresponds_to_setup_constants_b_machine/0,
58
59		specialized_inv/2, reuse_operation/4,
60		assert_max_reached_for_node/1, assert_time_out_for_node/3,
61		assert_time_out_for_invariant/1, assert_time_out_for_assertions/1,
62
63		set_max_nr_of_new_impl_trans_nodes/1,
64		get_max_nr_of_new_impl_trans_nodes/1,
65		impl_trans_term/3, impl_trans_term_all/2,
66		compute_transitions_if_necessary_saved/1,
67		max_nr_of_new_nodes_limit_not_reached/0,
68
69		tcltk_save_state/1, tcltk_load_state/1,
70		compute_full_state_space_hash/1,
71
72		execute_id_trace_from_current/3,
73		set_trace_by_transition_ids/1,
74		extract_term_trace_from_transition_ids/2]).
75
76		:- use_module(library(lists)).
77
78		:- use_module(self_check).
79		:- use_module(error_manager).
80		:- use_module(gensym).
81		:- use_module(preferences).
82		:- use_module(tools).
83		%:- use_module(state_space_exploration_modes,[compute_hash/3]).
84
85		:- use_module(extension('counter/counter')).
86
87		:- use_module(module_information).
88		:- module_info(group,animator).
89		:- module_info(description,'This module keeps track of the visited states by the animator/model checker.').
90
91		% ----------------------------------
92
93		:- load_files(library(system), [when(compile_time), imports([environ/2])]).
94		:- if(environ(prob_myheap,false)).
95		:- use_module(state_space_open_nodes). %% comment in to use only Prolog datastructures
96		:- else.
97		:- use_module(state_space_open_nodes_c). %% comment in to use C++ multimap queue; can make use of HEURISTIC_FUNCTION
98		:- endif.
99
100		% ----------------------------------
101
102		get_state_space_stats(NrNodes,NrTransitions,ProcessedNodes) :-
103		get_counter(states,N), NrNodes is N+1,
104		get_counter(transitions,NrTransitions),
105		get_counter(processed_nodes,ProcessedNodes).
106
107		gen_new_state_id(Nr) :-
108		inc_counter(states,N1), Nr is N1-1. % only one C call
109		%get_counter(states,Nr), inc_counter(states).
110		reset_state_counter :- reset_counter(states).
111		reset_state_counter(Nr) :- set_counter(states,Nr).
112
113		get_state_id_trace(StateIds) :-
114		history(History),
115		current_state_id(CurID),
116		reverse([CurID|History],StateIds).
117
118		:- dynamic history/1.
119		history([]).
120
121
122		:- dynamic forward_history/1.
123
124		:- dynamic current_state_id/1.
125		current_state_id(root).
126		/* INITIAL STATE, third arg: clp(fd) constraints as generated
127		by fd_copy_term */
128
129		current_expression(ID,State) :- current_state_id(ID),
130		visited_expression(ID,State).
131
132		:- use_module(specfile,[state_corresponds_to_initialised_b_machine/1,
133		state_corresponds_to_fully_setup_b_machine/1,
134		state_corresponds_to_set_up_constants/1]).
135		current_state_corresponds_to_initialised_b_machine:-
136		current_expression(_,State),
137		state_corresponds_to_initialised_b_machine(State).
138
139		current_state_corresponds_to_fully_setup_b_machine :-
140		current_expression(_,State),
141		state_corresponds_to_fully_setup_b_machine(State).
142
143		current_state_corresponds_to_setup_constants_b_machine :-
144		current_expression(_,State),
145		state_corresponds_to_set_up_constants(State).
146
147
148		:- dynamic current_options/1.
149		current_options([]).
150
151		set_current_options(Options) :-
152		retractall( current_options(_) ),
153		assert( current_options(Options) ).
154
155		:- dynamic packed_visited_expression/2.
156		%packed_visited_expression(v_0,true).
157
158		:- use_module(state_packing).
159
160		retract_visited_expression(ID,State) :- retract(packed_visited_expression(ID,PState)),
161		unpack_state(PState,State).
162
163		retractall_visited_expression(ID) :- retractall(packed_visited_expression(ID,_)).
164
165		state_space_packed_add(Id,PackedTerm) :- assert(packed_visited_expression(Id,PackedTerm)).
166
167		state_space_add(Id,Term) :-
168		(pack_state(Term,PackedTerm) -> assert(packed_visited_expression(Id,PackedTerm))
169		; add_internal_error('State packing failed: ',pack_state(Term,_)),
170		assert(packed_visited_expression(Id,Term))).
171
172		% deprecated:
173		visited_expression(ID,State,true) :- visited_expression(ID,State).
174		% not call(CurBody); for the moment we always have true as last argument
175
176	?	visited_expression(A,B) :- packed_visited_expression(A,PB),
177		(unpack_state(PB,R) -> B=R ; add_internal_error('Unpacking state failed: ',unpack_state(PB,R)),R=A).
178
179		visited_expression_id(A) :- packed_visited_expression(A,_). % avoid unpacking state
180
181
182
183		% given a hash and a packed state: find ID (fail if does not exist)
184		find_hashed_packed_visited_expression(Hash,PackedState,ID) :-
185		hash_to_id(Hash,ID),
186		(packed_visited_expression(ID,PackedState)
187		-> true /* warning: may instantiate State if not ground */
188		; print(hash_collision(Hash,ID)),nl,fail
189		).
190
191
192		:- dynamic not_invariant_checked/1.
193		set_invariant_checked(ID) :- %print(inv_checked(ID)),nl,
194		retract(not_invariant_checked(ID)).
195
196		invariant_not_yet_checked(ID) :-
197		not_all_transitions_added(ID) ; /* assumption: if not all transitions added then we haven't checked invariant yet */
198		not_invariant_checked(ID).
199
200		:- dynamic not_interesting/1.
201		%not_interesting(v_0).
202
203		:- dynamic max_reached_for_node/1.
204		/* true if not all outgoing transistions were computed due to the limit
205		on the number of operations/initialisations computed */
206		:- dynamic time_out_for_node/3, use_no_timeout/1, time_out_for_invariant/1, time_out_for_assertions/1.
207
208		time_out_for_node(ID) :- (var(ID) -> packed_visited_expression(ID,_) ; true),
209		(time_out_for_node(ID,_,_) -> true ; fail).
210
211		:- dynamic transition/4.
212		%transition(v_0,a,1,v_1).
213
214		store_transition(Org,Action,Dest,Id) :-
215		%get_counter(transitions,Id), inc_counter(transitions),
216		inc_counter(transitions,Id1), Id is Id1-1, % only one C call
217		assert(transition(Org,Action,Id,Dest)).
218
219		deadlocked_state(Origin) :- \+ any_transition(Origin,_,_).
220
221		is_concrete_constants_state_id(ID) :-
222		transition(root,_,ID),
223		packed_visited_expression(ID,concrete_constants(_)).
224
225		% check if we have multiple constant setups
226		multiple_concrete_constants_exist :-
227		is_concrete_constants_state_id(ID),
228		is_concrete_constants_state_id(ID2), ID2 \= ID,!.
229
230
231		is_initial_state_id(InitialStateID) :-
232		transition(root,_,State),
233		packed_visited_expression(State,P),
234		(P = concrete_constants(_)
235		-> state_space:transition(State,_,InitialStateID)
236		; InitialStateID=State).
237
238		any_transition(Origin,TransID,Destination) :- transition(Origin,_,TransID,Destination).
239
240		transition(Origin,Action,Destination) :- transition(Origin,Action,_TransID,Destination).
241
242		:- dynamic transition_info/2.
243		store_transition_infos([],_TransId).
244		store_transition_infos([Info|Irest],TransId) :-
245		store_transition_info(Info,TransId),
246		store_transition_infos(Irest,TransId).
247		store_transition_info(Info,TransId) :- %print(info(Info,TransId)),nl,
248		(keep_transition_info(Info)
249		-> assert(transition_info(TransId,Info))
250		; true).
251
252		% Do not store path info by default
253		keep_transition_info(path(_)) :- !,fail.
254		keep_transition_info(eventtrace(_)) :- !,preference(eventtrace,true).
255		keep_transition_info(event(_)) :- !,preference(store_event_transinfo,true).
256		keep_transition_info(_). % store everything else
257
258		reset_transition_store :-
259		retractall(transition(_,_,_,_)),
260		retractall(transition_info(_,_)),
261		reset_counter(transitions).
262
263		/*
264		Version with packing of transitions:
265		store_transition(Org,Action,Dest,Id) :-
266		retract(transition_counter(Id)),
267		NewId is Id+1,
268		assert(transition_counter(NewId)),
269		Action =.. [ActionName|Parameters],
270		pack_values(Parameters,PackedParameters),
271		assert(packed_transition(Org,ActionName,PackedParameters,Id,Dest)).
272
273		transition(Origin,Action,TransID,Destination) :- nonvar(Action),!,
274		Action =.. [ActionName|Parameters],
275		packed_transition(Origin,ActionName,PackedParameters,TransID,Destination),
276		unpack_values(PackedParameters,Parameters).
277		transition(Origin,Action,TransID,Destination) :-
278		packed_transition(Origin,ActionName,PackedParameters,TransID,Destination),
279		unpack_values(PackedParameters,Parameters),
280		Action =.. [ActionName|Parameters].
281		any_transition(Origin,TransID,Destination) :- packed_transition(Origin,_,_,TransID,Destination).
282		*/
283
284		% compute out-degree of a node
285		out_degree(ID,OutDegree) :- findall(0, transition(ID,_,_,_), L), length(L,OutDegree).
286
287		operation_name_not_yet_covered(OpName) :- operation_not_yet_covered(OpName).
288
289		:- dynamic operation_not_yet_covered/1.
290		%operation_not_yet_covered(b).
291
292		state_error_exists :- state_error(_,_,_),!.
293		:- dynamic state_error/3, context_state/2.
294
295		%state_error([],invariant_violated).
296
297		reset_next_state_error_id_counter :- reset_counter(next_state_error_id).
298		:- use_module(tools_printing, [print_error/1]).
299		:- use_module(error_manager,[print_error_span/1]).
300		store_state_error(State,Error,Id) :- state_error(State,Id,Error),!. % do not store identical error twice
301		store_state_error(State,Error,Id) :-
302		%retract( next_state_error_id(Id) ),
303		inc_counter(next_state_error_id,Id),
304		assert( state_error(State,Id,Error) ).
305		store_error_for_context_state(Error,Id) :-
306		( retract(context_state(State,Errs)) ->
307		(Errs<25 -> store_state_error(State,Error,Id), E1 is Errs+1,assert(context_state(State,E1))
308		; store_state_error(State,max_state_errors_reached(25),Id),assert(context_state(State,25))
309		)
310		; otherwise ->
311		add_internal_error('No known context when calling store_error_for_context_state: ',store_error_for_context_state(Error,Id)),
312		fail).
313		store_abort_error_for_context_state_if_possible(ErrType,Msg,Term,Span) :-
314		%print(store(Msg,Term,Span)),nl,
315		( context_state(State,_Errs) ->
316		error_manager:get_error_context(Context),
317		(abort_error_for_same_location_exists(State,Id1,ErrType,Msg,Span),
318		abort_error_for_same_location_exists(State,Id2,ErrType,Msg,Span),
319		Id2>Id1
320		-> /* two errors of same type, for same state and same source location exists */
321		/* TO DO: maybe merge state errors */
322		simplify_span(Span,Span2),
323		store_state_error(State,abort_error(ErrType,'Further identical errors occurred (not stored !)',Term,span_context(Span2,Context)),_)
324		;
325		print_error('An abort error occurred !'), print_error(ErrType),
326		print_error(Msg),
327		print_error_term(Term),
328		print_error(context_state_id(State)),
329		print_error_span(Span),
330		store_state_error(State,abort_error(ErrType,Msg,Term,span_context(Span,Context)),_)
331		),
332		(add_new_event_in_error_scope(abort_error(ErrType)) -> true ; true),
333		assert_real_error_occurred
334		; otherwise ->
335		add_error(ErrType,Msg,Term,Span)).
336
337		:- use_module(translate, [translate_error_term/2]).
338		print_error_term(Term) :- translate_error_term(Term,S), print_error(S).
339
340		abort_error_for_same_location_exists(State,Id,ErrType,Msg,Span) :-
341		state_error(State,Id,abort_error(ErrType,Msg,_Term2,span_context(Span2,_Ctxt2))),
342		same_span_location(Span2,Span).
343		% should be moved to error_manager ?
344		same_span_location(span_predicate(Pred,_,_),span_predicate(Pred,_,_)) :- !.
345		same_span_location(X,X).
346
347		% remove state information; quite often the same WD error occurs with slightly different stores
348		simplify_span(span_predicate(Pred,_,_),R) :- !, R=Pred.
349		simplify_span(X,X).
350
351		clear_context_state :-
352		retractall(context_state(_,_)).
353		set_context_state(State) :-
354		%print(setting_ctxt_state(State,Event)),nl,
355		retractall(context_state(_,_)), assert(context_state(State,0)).
356		get_current_context_state(ID) :- context_state(ID,_).
357
358		retractall_invariant_violated(State) :-
359		retractall(state_error(State,_,invariant_violated)).
360		invariant_violated(State) :-
361	?	state_error(State,_,invariant_violated).
362		set_invariant_violated(State) :-
363		( invariant_violated(State) -> true
364		; time_out_for_invariant(ID) -> print('Timeout for node: '), print(ID),nl,
365		print('Not setting invariant violation status'),nl
366		; store_state_error(State,invariant_violated,_)
367		).
368
369		%:- set_invariant_violated([]). % why is this ??
370
371
372		:- dynamic hash_to_id/2.
373		:- dynamic id_to_marker/2.
374
375		:- dynamic hash_to_nauty_id/2. % used in nauty mode to map nauty id's to hash values
376
377		:- dynamic specialized_inv/2. /* stores whether for a node a specialized invariant
378		version could be computed */
379
380		:- dynamic reuse_operation/4. /* when for a state and given operation name we can reuse the operation computed for another state */
381
382		:- use_module(hashing).
383		state_space_startup :- % call once at startup to ensure all counters exist
384		counter_init,
385		new_counter(states), new_counter(processed_nodes), new_counter(transitions),
386		new_counter(next_state_error_id),
387		reset_open_ids. % also calls myheap init
388		state_space_initialise :- counter_init, reset_gennum, reset_gensym,
389		new_counter(states), new_counter(processed_nodes), new_counter(transitions),
390		new_counter(next_state_error_id),
391		reset_state_counter, reset_processed_nodes_counter, reset_next_state_error_id_counter,
392		retractall_visited_expression(_),
393		reset_open_ids, reset_stored_values,
394		retractall(not_invariant_checked(_)),
395		retractall(not_interesting(_)),
396		retractall(max_reached_for_node(_)),
397		retractall(time_out_for_node(_,_,_)),
398		retractall(time_out_for_invariant(_)),
399		retractall(time_out_for_assertions(_)),
400		retractall(use_no_timeout(_)),
401		retractall(state_error(_,_,_)),
402		clear_context_state,
403		reset_transition_store,
404		retractall(operation_not_yet_covered(_)),
405		retractall(hash_to_id(_,_)),
406		retractall(hash_to_nauty_id(_,_)),
407		retractall(id_to_marker(_,_)),
408		retractall(specialized_inv(_,_)),
409		retractall(reuse_operation(_,_,_,_)),
410		state_space_add(root,root),
411		add_id_at_front(root),
412		hashing:my_term_hash(root,RootHash),
413		assert(hash_to_id(RootHash,root)),
414		%assert(not_invariant_checked(root)),
415		state_space_reset.
416
417		:- use_module(eventhandling,[register_event_listener/3]).
418		:- register_event_listener(startup_prob,state_space_startup,
419		'Initialise Statespace Counters.').
420		:- register_event_listener(reset_specification,state_space_initialise,
421		'Reset Statespace.').
422		:- register_event_listener(change_of_animation_mode,state_space_initialise,
423		'Reset Statespace.').
424
425		/* A version of reset which checks how much memory is used by each fact */
426		/* state_space:init_with_stats */
427		state_space_initialise_with_stats :-
428		reset_gennum, reset_gensym, reset_state_counter, reset_processed_nodes_counter,
429		reset_next_state_error_id_counter,
430		retract_open_ids_with_statistics,
431		retract_with_statistics(state_space,[packed_visited_expression(_,_),
432		not_invariant_checked(_),
433		not_interesting(_),
434		max_reached_for_node(_),
435		time_out_for_node(_,_,_),
436		time_out_for_invariant(_),
437		time_out_for_assertions(_),
438		use_no_timeout(_),
439		state_error(_,_,_),
440		transition(_,_,_,_),
441		transition_info(_,_),
442		operation_not_yet_covered(_),
443		hash_to_id(_,_),
444		hash_to_nauty_id(_,_),
445		id_to_marker(_,_),
446		specialized_inv(_,_),
447		reuse_operation(_,_,_,_),
448		history(_), forward_history(_), op_trace_ids(_)]),
449		retract_stored_values_with_statistics,
450		clear_context_state,
451		reset_transition_store,
452		state_space_add(root,root),
453		add_id_at_front(root),
454		%assert(not_invariant_checked(root)),
455		state_space_reset.
456
457
458
459		:- dynamic op_trace_ids/1.
460		reset_trace :- retractall(op_trace_ids(_)), assert(op_trace_ids([])).
461		get_action_trace(T) :- trace(T).
462		get_action_term_trace(PT) :- trace_with_limit(0,T), project_on_action_term(T,PT).
463		trace(Trace) :- trace_with_limit(500,Trace).
464		trace_with_limit(Limit,Trace) :-
465		op_trace_ids(IDT), reverse(IDT,RIDT),
466		extract_trace_from_transition_ids(RIDT,root,Limit,[],Trace).
467
468		reset_op_trace_ids :- retractall(op_trace_ids(_)), assert(op_trace_ids([])).
469		add_to_op_trace_ids(OpID) :- retract(op_trace_ids(OpIDS)), assert(op_trace_ids([OpID|OpIDS])).
470		remove_from_op_trace_ids(OpID) :- retract(op_trace_ids(OpIDS)),
471		(OpIDS = [R|Rest] -> assert(op_trace_ids(Rest)), OpID = R
472		; assert(op_trace_ids(OpIDS)),fail).
473
474		% translate a list of transition ids (from root) into a list of operation terms
475		extract_term_trace_from_transition_ids(TransIDListFromRoot,Trace) :-
476		extract_trace_from_transition_ids(TransIDListFromRoot,root,0,[],ActionTrace),
477		reverse_and_project_on_action_term(ActionTrace,[],Trace).
478
479		reverse_and_project_on_action_term([],A,A).
480		reverse_and_project_on_action_term([action(_,Term)|T],Acc,Res) :- !,
481		reverse_and_project_on_action_term(T,[Term|Acc],Res).
482		reverse_and_project_on_action_term([H|T],Acc,Res) :-
483		add_error(reverse_and_project_on_action_term,'Illegal action: ',H),
484		reverse_and_project_on_action_term(T,[H|Acc],Res).
485
486		project_on_action_term([],[]).
487		project_on_action_term([action(_,Term)|T],Res) :- !, Res=[Term|TR],
488		project_on_action_term(T,TR).
489		project_on_action_term([H|T],Res) :-
490		add_error(project_on_action_term,'Illegal action: ',H),
491		project_on_action_term(T,Res).
492
493		extract_trace_from_transition_ids([],_CurrentState,_,Trace,Trace).
494		extract_trace_from_transition_ids([TransId|Rest],CurrentState,Limit,AccTrace,Trace) :-
495		compute_op_string(TransId,CurrentState,Limit,OpTerm,OpString,DestState),!,
496		extract_trace_from_transition_ids(Rest,DestState,Limit,
497		[action(OpString,OpTerm)|AccTrace],Trace).
498		extract_trace_from_transition_ids([TransId|_],CurrentState,_,_,_Trace) :-
499		add_error(state_space,'Could not execute transition id: ', TransId:from(CurrentState)),fail.
500
501		:- use_module(translate,[translate_event_with_src_and_target_id/5]).
502		compute_op_string(jump(TO),_CurID,_,Term,String,DestID) :- !, Term=jump,String=jump,DestID=TO.
503		compute_op_string(TransId,CurID,Limit,Term,String,DestID) :- transition(CurID,Term,TransId,DestID),
504		translate_event_with_src_and_target_id(Term,CurID,DestID,Limit,String).
505
506		state_space_reset :-
507		reset_trace,
508		retractall(history(_)),
509		retractall(forward_history(_)),
510		retractall(current_state_id(_)),
511		retractall(current_options(_)),
512		assert(history([])),
513		assert(current_state_id(root)).
514
515
516		state_space_clean_all :-
517		retractall(state_space_version_in_file(_)),
518		retractall_visited_expression(_),
519		reset_open_ids,
520		retractall(not_invariant_checked(_)),
521		retractall(not_interesting(_)),
522		retractall(max_reached_for_node(_)),
523		retractall(time_out_for_node(_,_,_)),
524		retractall(time_out_for_invariant(_)),
525		retractall(time_out_for_assertions(_)),
526		retractall(use_no_timeout(_)),
527		retractall(state_error(_,_,_)),
528		clear_context_state,
529		reset_transition_store,
530		retractall(operation_not_yet_covered(_)),
531		retractall(hash_to_id(_,_)),
532		retractall(hash_to_nauty_id(_,_)),
533		retractall(id_to_marker(_,_)),
534		retractall(specialized_inv(_,_)),
535		retractall(reuse_operation(_,_,_,_)),
536		retractall(history(_)),
537		retractall(forward_history(_)),
538		retractall(op_trace_ids(_)),
539		retractall(current_state_id(_)),
540		retractall(current_options(_)).
541
542		% this is only used from within the Tcl/Tk animator at the moment:
543		delete_node(ID) :- print(deleting(ID)),nl,
544		retractall_visited_expression(ID),
545		retractall_invariant_violated(ID),
546		retract_open_node_and_update_processed_nodes(ID),
547		retractall(not_invariant_checked(ID)),
548		retractall(not_interesting(ID)),
549		retractall(max_reached_for_node(ID)),
550		retractall(time_out_for_node(ID,_,_)),
551		retractall(time_out_for_invariant(ID)),
552		retractall(time_out_for_assertions(ID)),
553		retractall(use_no_timeout(ID)),
554		retractall(state_error(ID,_,_)),
555		retractall(transition(ID,_,_,_)),
556		% to do: check if operation_not_yet_covered(_) changes
557		retract_hash(ID),
558		retractall(id_to_marker(ID,_)).
559
560		retract_hash(ID) :- retract(hash_to_id(Hash,ID)), retractall(hash_to_nauty_id(_TermHash,Hash)),fail.
561		retract_hash(_).
562
563		assert_max_reached_for_node(Id) :- %print_message(max_reached_for_node(Id)),
564		(max_reached_for_node(Id) -> true ; assert(max_reached_for_node(Id))).
565
566		assert_time_out_for_node(Id,OpName,TypeOfTimeOut) :- print_message(time_out_for_node(Id,OpName,TypeOfTimeOut)),
567		(time_out_for_node(Id,OpName,_) -> true ; assert(time_out_for_node(Id,OpName,TypeOfTimeOut))).
568		assert_time_out_for_invariant(Id) :- print_message(time_out_for_invariant(Id)),
569		(time_out_for_invariant(Id) -> true ; assert(time_out_for_invariant(Id))).
570		assert_time_out_for_assertions(Id) :- print_message(time_out_for_assertions(Id)),
571		(time_out_for_assertions(Id) -> true ; assert(time_out_for_assertions(Id))).
572
573		max_reached_or_timeout_for_node(Id) :-
574		(max_reached_for_node(Id) ; time_out_for_node(Id,_,_)).
575		/* ---------------------- */
576		/* state space saving */
577		/* ---------------------- */
578
579		:- dynamic state_space_version_in_file/1. %
580		state_space_version(1).
581
582		check_state_space_version :- state_space_version(V),
583		(state_space_version_in_file(F) -> true ; F=0),
584		(V>F -> add_message(state_space,'Warning: saved state_space may be incompatible with current version: ',F:V) ; true).
585
586		tcltk_save_state(File) :-
587		print('% saving state to: '), print(File),nl,
588		tell(File),
589		print_state_space,
590		told,
591		print_message(done).
592
593
594		:- use_module(tools_printing, [print_dynamic_fact/1,print_dynamic_pred/3]).
595		print_state_space :-
596		state_space_version(V),
597		print_dynamic_fact(state_space_version_in_file(V)),
598		% TO DO: maybe also save some important preferences, and warn user and/or propose to adapt preferences ?
599		print_dynamic_pred(state_space,history,1),
600		print_dynamic_pred(state_space,forward_history,1),
601		print_dynamic_pred(state_space,op_trace_ids,1),
602		print_dynamic_pred(state_space,current_state_id,1),
603		print_dynamic_pred(state_space,current_options,1),
604		print_dynamic_pred(state_space,packed_visited_expression,2),
605		print_dynamic_pred(state_space,not_invariant_checked,1),
606		print_dynamic_pred(state_space,not_interesting,1),
607		print_dynamic_pred(state_space,max_reached_for_node,1),
608		print_dynamic_pred(state_space,time_out_for_node,3),
609		print_dynamic_pred(state_space,use_no_timeout,1),
610		print_dynamic_pred(state_space,transition,4),
611		print_dynamic_pred(state_space,transition_info,2),
612		print_dynamic_pred(state_space,operation_not_yet_covered,1),
613		print_dynamic_pred(state_space,state_error,3),
614		print_state_space_open_nodes,
615		print_stored_values,
616		get_counter(states,X),
617		write_term(saved_gennum_count(X),[quoted(true)]),print('.'),nl.
618
619		saved_gennum_count(99999).
620
621		/* ---------------------- */
622		/* state space loading */
623		/* ---------------------- */
624
625		tcltk_load_state(File) :- state_space_clean_all,
626		print('Loading: '), print(File),nl,
627		user_consult_without_redefine_warning(File), % this will read in bind_skeleton/2, ..., next_value_id/1
628		check_state_space_version,
629		print('Generating open node info'),nl,
630		transfer_open_node_info,
631		print('Transfer state packing info'),nl,
632		transfer_state_packing_info,
633		print('Recomputing hash index'),nl,
634		recompute_all_hash,
635		(saved_gennum_count(X) -> reset_state_counter(X) ; true),
636		reset_processed_nodes_counter, % TO DO: restore or save it
637		reset_next_state_error_id_counter, % DITTO
638		print('Done'),nl,!.
639		tcltk_load_state(File) :-
640		add_error(tcltk_load_state,'Could not load state from file: ',File),
641		state_space_initialise.
642
643		:- dynamic not_all_z_saved/1, not_all_transitions_added_saved/1.
644		:- dynamic bind_skeleton/2, stored_value/2, stored_value_hash_to_id/2, next_value_id/1.
645
646		% transfer facts read into state_space into other modules:
647		transfer_open_node_info :- retract(not_all_z_saved(X)), %print(not_all_z(X)),nl,
648		assert_not_all_z(X),fail.
649		transfer_open_node_info :- retract(not_all_transitions_added_saved(X)),
650		assert_not_all_transitions_added(X),fail.
651		transfer_open_node_info.
652		% now for transferring to state_packing module info generated by print_stored_values
653		transfer_state_packing_info :- retract(bind_skeleton(X,Y)), %print(skel(X)),nl,
654		assert(state_packing:bind_skeleton(X,Y)),fail.
655		transfer_state_packing_info :- retract(stored_value(X,Y)),
656		assert(state_packing:stored_value(X,Y)),fail.
657		transfer_state_packing_info :- retract(stored_value_hash_to_id(X,Y)),
658		assert(state_packing:stored_value_hash_to_id(X,Y)),fail.
659		transfer_state_packing_info :- retract(next_value_id(X)),
660		assert(state_packing:next_value_id(X)),fail.
661		transfer_state_packing_info.
662
663		recompute_all_hash :-
664		retractall(hash_to_id(_,_)),retractall(id_to_marker(_,_)),
665		retractall(hash_to_nauty_id(_,_)),
666		visited_expression(ID,StateTemplate),
667		state_space_exploration_modes:compute_hash(StateTemplate,Hash,Marker),
668		assert(hash_to_id(Hash,ID)),
669		assert(id_to_marker(ID,Marker)),
670		fail.
671		recompute_all_hash.
672
673		:- use_module(hashing,[my_term_hash/2]).
674		% generates a hash for the entire state space not depending on the order in which states where added
675		compute_full_state_space_hash(Hash) :-
676		findall(Hash,hash_to_id(Hash,_),ListOfHashCodes),
677		sort(ListOfHashCodes,SortedList),
678		my_term_hash(SortedList,Hash).
679		% TO DO: also provide transition hashes
680
681		:- use_module(tools_meta,[safe_on_exception/3]).
682		user_consult_without_redefine_warning(File) :-
683		prolog_flag(redefine_warnings, Old, off),
684		prolog_flag(single_var_warnings, Old2, off),
685		(safe_on_exception(Exc,consult(File),(nl,print('Exception occurred:'),print(Exc),nl,fail))
686		-> OK=true ; OK=false),
687		prolog_flag(redefine_warnings, _, Old),
688		prolog_flag(single_var_warnings, _, Old2),
689		OK=true.
690
691
692
693		execute_id_trace_from_current(ID,OpIDL,StateIDList) :-
694		current_state_id(CurID),
695		reverse([CurID|StateIDList],Rev),
696		Rev = [Dest|TRev], (Dest==ID -> true ; (print(not_eq(Dest,ID)),nl)),
697		retract(history(H)), retractall(forward_history(_)),
698		append(TRev,H,NewH),
699		assert(history(NewH)),
700		retract(op_trace_ids(OldTrace)),
701		reverse(OpIDL,NewTrace),
702		append(NewTrace,OldTrace,Trace),
703		assert(op_trace_ids(Trace)),
704		retractall(current_state_id(_)),
705		assert(current_state_id(ID)).
706		%execute_trace_to_node(OpL,StateIDList). /* <----- BOTTLENECK FOR LONG SEQUENCES */
707		%generate_trace([],Acc,Acc).
708		%generate_trace([OpTerm|T],Acc,Res) :-
709		% translate:translate_event(OpTerm,OpString),
710		% generate_trace(T,[action(OpString,OpTerm)|Acc],Res).
711
712		set_trace_by_transition_ids(TransitionIds) :-
713		extract_history_from_transition_ids(TransitionIds,root,[],[],Last,History,OpTrace),
714		%visited_expression(Last,LastState,LastCond),
715		retractall(history(_)), retractall(forward_history(_)),
716		retractall(current_state_id(_)),
717		retractall(op_trace_ids(_)),
718		assert(history(History)), assert(op_trace_ids(OpTrace)),
719		assert(current_state_id(Last)).
720
721		extract_history_from_transition_ids([],CurrentState,History,Trace,CurrentState,History,Trace).
722		extract_history_from_transition_ids([TransId|Rest],CurrentState,AccHist,AccTrace,Last,History,Trace) :-
723		transition(CurrentState,_,TransId,DestState),!,
724		extract_history_from_transition_ids(Rest,DestState,[CurrentState|AccHist],
725		[TransId|AccTrace],Last,History,Trace).
726		extract_history_from_transition_ids([TransId|_],CurrentState,_,_,_,_,_Trace) :-
727		add_error(state_space,'Could not execute transition id: ', TransId:from(CurrentState)),fail.
728
729
730
731		/* --------------------------------- */
732		:- dynamic max_nr_of_new_nodes/1.
733
734		% negative number or non-number signifies no limit
735		set_max_nr_of_new_impl_trans_nodes(MaxNrOfNewNodes) :-
736		retractall(max_nr_of_new_nodes(_)),
737		(number(MaxNrOfNewNodes), MaxNrOfNewNodes>=0
738		-> assert(max_nr_of_new_nodes(MaxNrOfNewNodes))
739		; true). % no need to store limit
740
741		get_max_nr_of_new_impl_trans_nodes(MaxNrOfNewNodes) :-
742		(max_nr_of_new_nodes(Max) -> MaxNrOfNewNodes=Max; MaxNrOfNewNodes = 0).
743
744		impl_trans_term(From,ActionAsTerm,To) :-
745		compute_transitions_if_necessary_saved(From),
746		transition(From,ActionAsTerm,_TID,To).
747
748		impl_trans_term_all(From,Ops) :-
749		compute_transitions_if_necessary_saved(From),
750		findall(op(Id,ActionAsTerm,To),
751		transition(From,ActionAsTerm,Id,To),
752		Ops).
753
754		compute_transitions_if_necessary_saved(From) :-
755		on_exception(error(forced_interrupt_error('User has interrupted the current execution'),_),
756		compute_transitions_if_necessary(From),
757		user:process_interrupted_error_message).
758
759		compute_transitions_if_necessary(From) :-
760		not_all_transitions_added(From),!,
761		decrease_max_nr_of_new_nodes(From),
762		%user:do_one_gui_event,
763		user:compute_all_transitions_if_necessary(From,false).
764		compute_transitions_if_necessary(_From).
765
766		decrease_max_nr_of_new_nodes(ID) :-
767		retract(max_nr_of_new_nodes(Max)),!,
768		( Max>0 ->
769		NewMax is Max-1,
770		assert(max_nr_of_new_nodes(NewMax))
771		; Max=0 -> NM is -1,
772		assert(max_nr_of_new_nodes(NM)),
773		add_warning(state_space,'Maximum number of new nodes reached for CTL/LTL/refinement check, node id = ',ID),
774		%trace,
775		fail
776		; otherwise -> % negative number: re-assert and fail
777		assert(max_nr_of_new_nodes(Max)),
778		fail).
779		decrease_max_nr_of_new_nodes(_). % no limit stored; just proceed
780
781		% will be called from TCL/TK side
782		max_nr_of_new_nodes_limit_not_reached :-
783		max_nr_of_new_nodes(N),N>0.
784
785		:- use_module(specfile,[b_or_z_mode/0]).
786		retract_open_node(NodeID) :- retract_open_node_and_update_processed_nodes(NodeID),
787		(b_or_z_mode -> assert(not_invariant_checked(NodeID)) ; true).
788
789		reset_processed_nodes_counter :- reset_counter(processed_nodes).
790		%reset_processed_nodes_counter(Nr) :- set_counter(processed_nodes,Nr).
791
792		retract_open_node_and_update_processed_nodes(NodeID) :-
793		retract_open_node_direct(NodeID),
794		inc_processed.
795
796		inc_processed :-
797		inc_counter(processed_nodes).
798
799		pop_id_from_front(ID) :- pop_id_from_front_direct(ID), inc_processed.
800		pop_id_from_end(ID) :- pop_id_from_end_direct(ID), inc_processed.
801		pop_id_oldest(ID) :- pop_id_oldest_direct(ID), inc_processed.
802
803		/* --------------------------------- */
804
805		%
806		% Code to compute equivalence classes
807		% using the standard DFA minimization algorithm
808
809		:- dynamic equivalent/2.
810		% state_space:compute_equivalence_classes
811		:- public compute_equivalence_classes/0.
812
813		compute_equivalence_classes :- init_equi,
814		split_equivalence_classes,nl,
815		print_equi.
816
817		print_equi :- state_space:equivalent(A,B), visited_expression(A,State),
818		visited_expression(B,StateB),
819		nl,
820		print(A), print(' : '), print(State),nl,
821		print(B), print(' : '), print(StateB),nl,fail.
822		print_equi.
823
824		init_equi :- retractall(equivalent(_,_)),
825		packed_visited_expression(ID,_State),
826		\+ not_all_transitions_added(ID),
827		findall(Action,transition(ID,Action,_,_),List),
828		packed_visited_expression(ID2,_S2), ID2 @> ID,
829		\+ not_all_transitions_added(ID2),
830		findall(Action,transition(ID2,Action,_,_),List),
831		assert(equivalent(ID,ID2)), % they have the same signature
832		%print(equivalent(ID,ID2)),nl,
833		fail.
834		init_equi :- print(finished_initialising),nl.
835
836		split_equivalence_classes :- retractall(echange),
837		equivalent(ID1,ID2),
838		transition(ID1,A,_,Dest1),
839		transition(ID2,A,_,Dest2),
840		\+ check_equi(Dest1,Dest2),
841		retract(equivalent(ID1,ID2)), % splitting class
842		% print(diff(ID1,ID2, A, Dest1, Dest2)),nl,
843		assert_echange,
844		fail.
845		split_equivalence_classes :- echange -> split_equivalence_classes ; true.
846
847		:- dynamic echange/0.
848		assert_echange :- echange -> true ; assert(echange),print('.'),flush_output.
849
850		check_equi(A,B) :- A=B -> true ; A @<B -> equivalent(A,B) ; equivalent(B,A).
851
852		/*
853		% benchmark how much time it takes to copy the state space state_space:bench_state_space.
854		bench_state_space :-
855		statistics(walltime,_),
856		(state_space:packed_visited_expression(ID,S), assert(pve(ID,S)),fail ; true),
857		statistics(walltime,[_,Delta]), format('Time to copy packed_visited_expression: ~w ms~n',[Delta]),
858		(state_space:transition(A,B,C,D), assert(tr(A,B,C,D)),fail ; true),
859		statistics(walltime,[_,Delta2]), format('Time to copy transition: ~w ms~n',[Delta2]),
860		(state_packing:stored_value(A,B), assert(sv(A,B)),fail ; true),
861		(state_packing:stored_value_hash_to_id(A,B), assert(svhi(A,B)),fail ; true),
862		statistics(walltime,[_,Delta3]), format('Time to copy stored_value: ~w ms~n',[Delta3]).
863		*/
864