1		% (c) 2009-2025 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(refinement_checker,[
6		% tcltk_save_implementation_state_for_refinement/1,
7		tcltk_save_specification_state_for_refinement/1,
8		tcltk_load_refine_spec_file/1,
9		tcltk_refinement_search/3, in_situ_ref_search/5, in_situ_model_check/5,
10		reset_refinement_checker/0,
11		%% impl_trans/3,
12		%generate_new_tau_div_collapsed_state/3,
13		%search_for_divergence/5,
14		dvisited/1,
15		valid_failures_model/2,
16
17		tcltk_nested_dfs_goal_cycle_check/1,
18		nested_dfs_cycle_check/3
19		]).
20
21		:- use_module(probsrc(module_information),[module_info/2]).
22		:- module_info(group,csp).
23		:- module_info(description,'A CSP refinement checker, along with determinism, deadlock and livelock checking.').
24
25		:- use_module(library(lists)).
26
27		:- use_module(probsrc(tools)).
28		:- use_module(probsrc(self_check)).
29		:- use_module(probsrc(debug)).
30		:- use_module(probsrc(error_manager)).
31		%:- use_module(probsrc(preferences).
32		:- use_module(probsrc(translate),[translate_event/2, print_state/1]).
33		:- use_module(probsrc(tools_printing), [print_error/1, format_error/2]).
34
35		:- use_module(probsrc(state_space)).
36
37		:- use_module(library(random)).
38		:- use_module(probsrc(tools_meta),[safe_on_exception/3]).
39
40		user_consult_without_redefine_warning(File) :-
41		get_set_optional_prolog_flag(redefine_warnings, Old, off),
42		get_set_optional_prolog_flag(single_var_warnings, Old2, off),
43		(safe_on_exception(Exc,
44		load_files(File,[compilation_mode(assert_all)]),
45		(nl,print('Exception occurred:'),print(Exc),nl,fail))
46		-> OK=true ; OK=false),
47		get_set_optional_prolog_flag(redefine_warnings, _, Old),
48		get_set_optional_prolog_flag(single_var_warnings, _, Old2),
49		OK=true.
50
51		tcltk_save_specification_state_for_refinement(File) :-
52		printsilent('saving XSB Specification state to: '), printsilent(File),nls,
53		tell(File), print_specification_state_space_for_refinement, told, printsilent(done),nls.
54
55		print_specification_state_space_for_refinement :-
56		ref_transition(From,Label,To),
57		write_term(spec_trans(From,Label,To),[quoted(true)]),
58		write('.'),nl,
59		fail.
60		print_specification_state_space_for_refinement :-
61		not_all_transitions_added(ID),
62		write_term(spec_not_all_transitions_added(ID),[quoted(true)]),
63		write('.'),nl,
64		fail.
65		print_specification_state_space_for_refinement :-
66		max_reached_or_timeout_for_node(ID),
67		write_term(spec_max_reached_for_node(ID),[quoted(true)]),
68		write('.'),nl,
69		fail.
70		print_specification_state_space_for_refinement :-
71		(not_all_transitions_added(_) -> true ;
72		portray_clause((spec_not_all_transitions_added(_) :- fail))
73		),
74		(max_reached_or_timeout_for_node(_) -> true ;
75		portray_clause((spec_max_reached_for_node(_) :- fail))
76		),
77		((max_reached_or_timeout_for_node(_); not_all_transitions_added(_))
78		-> portray_clause((spec_completely_explored :- fail))
79		; portray_clause((spec_completely_explored :- true))
80		).
81		% TO DO: also generate facts for spec_stable (as we eliminate the tau transitions in ref_transition)
82
83		ref_transition(From,Label,To) :- ref_transition(From,Label,To,[From]).
84
85		ref_transition(From,Label,To,_TauList) :-
86		transition(From,Action1,To1),
87		(functor(Action1,'$setup_constants',_)
88		-> ref_transition(To1,Label,To)
89		; ref_generate_label(Action1,Label1),
90		%(Label1 = tau % we now now longer expand tau transitions in spec_trans
91		% -> \+ member(To1,TauList), /* no loop */
92		% ref_transition(To1,Label,To,[To1|TauList])
93		% ;
94		Label=Label1, To=To1
95		%)
96		).
97
98		:- use_module(probsrc(specfile),[animation_mode/1,csp_mode/0,csp_with_bz_mode/0]).
99		ref_generate_label(Action,Label) :-
100		((functor(Action,'$initialise_machine',_) ; functor(Action,start_cspm_MAIN,_))
101		-> Label = '$initialise_machine'
102		; (Action=tau(_),
103		\+ animation_mode(b)
104		-> Label=tau
105		; translate_event(Action,Label))
106		).
107
108		% these facts can also be found in the _refine_spec.P files
109		:- volatile spec_trans/3.
110		:- dynamic spec_trans/3.
111		:- dynamic spec_max_reached_for_node/1, spec_not_all_transitions_added/1, spec_completely_explored/0.
112		reset_refine_spec :-
113		retractall(spec_trans(_,_,_)),
114		retractall(spec_max_reached_for_node(_)),
115		retractall(spec_not_all_transitions_added(_)),
116		retractall(spec_completely_explored),
117		(csp_with_bz_mode -> debug_println(10,csp_and_b_mode),
118		assertz((spec_trans(From,Label,To) :- impl_trans_cspb(From,Label,To)))
119		; % use same transition system for abstraction and implementation
120		assertz((spec_trans(From,Label,To) :- impl_trans(From,Label,To)))
121		),
122		assertz((spec_not_all_transitions_added(From) :- not_all_transitions_added(From))),
123		assertz((spec_max_reached_for_node(From) :- max_reached_or_timeout_for_node(From))),
124		assertz((spec_completely_explored :- max_reached_or_timeout_for_node(_); not_all_transitions_added(_))).
125
126		:- public impl_trans_cspb/3. % asserted above in spec_trans
127		impl_trans_cspb(From,Label,To) :-
128		impl_trans(From,X,To),translate_csp_b_event(X,X1),
129		% print(translated_event(X1)),nl,
130		(var(Label) -> Label=X
131		; translate_csp_b_event(Label,Label1),X1==Label1).
132
133		%spec_trans(From,Label,To) :- impl_trans(From,Label,To).
134		%spec_trans(_,_,_) :- fail.
135		spec_max_reached_for_node(_) :- fail.
136		spec_not_all_transitions_added(_) :- fail.
137		spec_completely_explored :- fail.
138		% spec_stable(_).
139
140		% summaring of the set closures
141		reduce_channel_set(_Actions,closure([]),[]).
142		reduce_channel_set(Actions,closure([tuple([Channel])|Tail]),List) :-
143		expand_symbolic_set(closure([tuple([Channel])]),HdList,_C),
144		return_csp_closure_value(HdList,AllChannelEvents),
145		list_to_ord_set(AllChannelEvents,HdSet),
146		ord_intersection(HdSet,Actions,InterSet),
147		( ord_seteq(InterSet,HdSet) ->
148		reduce_channel_set(Actions,closure(Tail),T),
149		ord_union([Channel],T,List)
150		;
151		reduce_channel_set(Actions,closure(Tail),T),
152		ord_union(InterSet,T,List)
153		).
154		reduce_channel_set(_Actions,Cl,_L) :-
155		add_internal_error('Internal Error: Type error; expected closure: ',Cl),fail.
156
157		/* --------------------------------------------------- */
158		/* REFINEMENT CHECKING */
159
160		%:- table not_refines/3.
161
162		:- use_module(probcspsrc(haskell_csp), [evaluate_argument/2,is_not_infinite_type/1,ignore_infinite_datatypes/0]).
163		:- use_module(probcspsrc(csp_sets), [expand_symbolic_set/3]).
164		:- use_module(probsrc(translate), [return_csp_closure_value/2]).
165
166		:- dynamic not_refines_table/3,not_refusals_table/3.
167
168		%not_failure_refines(F,X,YList,C) :- print(not_failure_refines(F,X,YList,C)),nl,fail.
169		not_failure_refines(singleton_failures,X,YList,[not_enabled(A)|_T]) :- % Singleton Failures
170		spec_trans_all(YList,A),
171		\+(impl_trans(X,A,_)), /* TO DO: handle tau for CSP */
172		check_impl_trans_complete(X),
173		print_message(cannot_do(A)).
174		not_failure_refines(failures,X,YList,[cannot_refuse_compl(AllXActions),cannot_refuse(ReducedRefuseSet)|_T]) :-
175		% CSP Failures
176		impl_stable(X), % only need to check if X is stable
177		impl_all_possible_actions(X,AllXActions),
178		\+ find_failure_abstraction(YList,AllXActions), % if satisfied => an X action can be refused at the current state of Y
179		check_impl_trans_complete(X), % AllXActions are not complete, counter-example could be spurios !
180		% note: we can use ord_subset since setof returns sorted lists
181		get_reduced_refused_set(AllXActions,ReducedRefuseSet),
182		debug_println(19,cannot_refuse_compl(AllXActions)),
183		debug_println(19,cannot_refuse(ReducedRefuseSet)).
184		not_failure_refines(failure_divergences,X,YList,T) :-
185		(not_failure_refines(failures,X,YList,T)
186		-> true /* not we have already checked for divergence in YList in not_refines */
187		; impl_diverges(X), T=[spec_cannot_diverge|_T]).
188
189
190		:- dynamic ref_check_incomplete/0.
191		check_impl_trans_complete(X) :- impl_trans_not_complete(X),!,
192		assert_ref_check_incomplete(X).
193		check_impl_trans_complete(_).
194
195		assert_ref_check_incomplete(ID) :-
196		(ref_check_incomplete -> true ; assertz(ref_check_incomplete)),
197		format(user_error,'Refinement check incomplete for state: ~w~n',[ID]).
198
199		:- use_module(library(ordsets)).
200		find_failure_abstraction([AbsState|_T],AllXActions) :-
201		spec_stable(AbsState),
202		spec_all_possible_actions(AbsState,AllAbsActions),
203		% note: we can use ord_subset as setof returns sorted lists
204		ord_subset(AllAbsActions,AllXActions),
205		!. % we have found an abstract state whose failures is a superset of X's failures
206		find_failure_abstraction([_|T],AllXActions) :-
207		find_failure_abstraction(T,AllXActions).
208
209
210		get_reduced_refused_set(_,RefusedSet) :- animation_mode(b),!,
211		RefusedSet = ['$UNKNOWN']. % TODO: get all operations at list and build complement ??
212		get_reduced_refused_set(AllXActions,ReducedRefuseSet) :-
213		get_refused_set3(AllXActions,Closure,RefusedSet),
214		reduce_channel_set(RefusedSet,Closure,ReducedRefuseSet).
215
216		get_refused_set(_,RefusedSet) :- animation_mode(b),!,
217		RefusedSet = ['$UNKNOWN'].
218		get_refused_set(AllXActions,RefusedSet) :-
219		get_refused_set3(AllXActions,_,RefusedSet).
220
221		get_refused_set3(AllXActions,R,RefusedSet) :-
222		evaluate_argument('Events',R),
223		expand_symbolic_set(R,R1,_C),
224		(csp_with_bz_mode ->
225		l_translate_csp_b_event(AllXActions,AllXActionsNew),
226		l_translate_csp_b_event(R1,R2)
227		; AllXActionsNew=AllXActions,
228		R2=R1
229		),
230		return_csp_closure_value(R2,AllPossibleEvents),
231		list_to_ord_set(AllPossibleEvents,AllEventsSet),
232		list_to_ord_set(AllXActionsNew,AllXActionsSet),
233		ord_subtract(AllEventsSet,AllXActionsSet,RefusedSet).
234
235		spec_stable(State) :-
236		get_tau_closure(State,_,stable,_).
237		% \+ spec_trans(State,tau,_).
238		impl_stable(State) :-
239		get_tau_closure(State,_,stable,_).
240		% \+ impl_trans(State,tau,_).
241		spec_possible_action(State,Action) :-
242		setof(A,NState^spec_trans(State,A,NState),As), member(Action,As).
243		spec_all_possible_actions(State,ActionList) :-
244		(setof(A,NState^spec_trans(State,A,NState),ActionList) -> true ; ActionList=[]).
245		impl_all_possible_actions(State,ActionList) :-
246		(setof(A,NState^impl_trans(State,A,NState),ActionList) -> true ; ActionList=[]).
247
248		spec_trans_all([State|MoreStates],Action) :-
249		spec_possible_action(State,Action),
250		spec_trans_all2(MoreStates,Action).
251
252		spec_trans_all2([],_ANY).
253		spec_trans_all2([State|T],Action) :-
254		spec_trans(State,Action,_),!,
255		spec_trans_all2(T,Action).
256
257		% We check for the following assertion Spec [m= Impl, where m : {T,F,FD}
258		% X is a current node from the implementation process Impl, and YList is
259		% the current list of nodes of the specification process Spec.
260		% The predicate not_refines(X,Y,TrX,TrY,EList,Model) can be read as follow:
261		% Chech if X is not a Model-refinement of Y.
262		% (TRUE => X does not refine Y ---> producing a counter example)
263		% (FALSE (Failure Loop) => explore and search through the state spaces of Spec and Impl until a counter example is found or Spec is completelly explored)
264
265		not_refines(X,Y,Tr,_,_YEnabled,_) :- % print_message(nr(X,Y,Tr)), %%
266		% the configuration is already in the memo table: do not look for a counter-example here
267		not_refines_table(X,Y,Tr),!,fail.
268		not_refines(X,YList,TraceX,_,_,_) :-
269		assertz(not_refines_table(X,YList,TraceX)), % add to memo table
270		YList=[X|_],csp_mode,!,fail. % simple check if X appears in the list; if so we will never find a counter example; we could do a full member check (but not sure about performance)
271		% in non csp_mode: root state of impl and spec are different
272		not_refines(_X,YList,_TraceX,_TraceY,_YEnabled,_) :-
273		\+(spec_completely_explored),
274		spec_list_contains_unexplored_node(YList),!, %YEnabled=['$unknown'],
275		fail.
276		/* we don't know what the spec can do */
277		/* to do: improve for max_reached_for_node (if we know max>0) */
278		not_refines(X,YList,TraceX,_TraceY,YEnabledList,FailuresModel) :- /* use failure refinement */
279		not_failure_refines(FailuresModel,X,YList,TraceX),
280		findall(AA,spec_par_trans(YList,AA,_),YEnabledList).
281		not_refines(X,YList,TraceX,TraceY,YEnabledList,FailuresModel) :-
282		get_tau_closure(X,_Closure,Stable,_Diverges),
283		Stable=unstable_prio(Dest),!, % only perform tau priority action
284		TraceX = [go(tau,X2)|TX], member(X2,Dest),
285		not_refines(X2,YList,TX,TraceY,YEnabledList,FailuresModel).
286		not_refines(X,YList,TraceX,TraceY,YEnabledList,FailuresModel) :-
287		do_one_trace_step_ahead(X,YList,TraceX,TraceY,YEnabledList,FailuresModel).
288
289		do_one_trace_step_ahead(X,YList,TraceX,TraceY,YEnabledList,FailuresModel) :-
290		TraceX = [go(A,X2)|TX],
291		impl_trans(X,A,X2),
292		(A = tau
293		-> not_refines(X2,YList,TX,TraceY,YEnabledList,FailuresModel)
294		; (setof(Y2,spec_par_trans(YList,A,Y2),YS)
295		-> TraceY = [go(A,_)|TY],
296		spec_tau_closure(YS,YTS,FailuresModel), % diamond compression of the LTS of the Spec process
297		not_refines(X2,YTS,TX,TY,YEnabledList,FailuresModel)
298		; findall(AA,(spec_par_trans(YList,AA,_),AA\=tau),YListChoices), /* no transition: refinement false */
299		remove_dups(YListChoices,YEnabledList) % do we need to remove duplicated enabled actions here?
300		)
301		).
302
303		% Refusal traces are of the form <X1,a1,X2,a2,...,Xn>
304		% where X1..Xn are the refused sets, a1 -> a2 -> ... -> an is the event trace beginning from the initial state.
305		% We need to keep track of the whole refusal trace beginning from the initial state
306		% in order to prove if the Impl process is a refusal refinement of the Spec process.
307
308		% Notion: At each point we must check if Impl has the same refusal trace prefix as Spec in
309		% order to continue checking of the refusal trace.
310
311		% TODO: Comments, which explain the refusal based refinement algorithm, are missing!!!
312
313		not_refusals(X,Y,_TrX,_TrY,RefusalTraceX,_RefusalTraceY,_YEnabled,_RefusalModel) :-
314		not_refusals_table(X,Y,RefusalTraceX),!,fail.
315		not_refusals(X,YList,_TrX,_TrY,RefusalTrace,_RefusalTraceY,_YEnabled,_RefusalModel) :-
316		assertz(not_refusals_table(X,YList,RefusalTrace)),
317		YList=[X|_],csp_mode,!,fail.
318		not_refusals(_X,YList,_TraceX,_TraceY,_RefusalTraceX,_RefusalTraceY,_YEnabled,_RefusalModel) :-
319		\+(spec_completely_explored),
320		spec_list_contains_unexplored_node(YList),!,
321		fail.
322		not_refusals(X,_YList,_TraceX,TraceY,_RefusalTraceX,RefusalTraceY,_YEnabledList,RefusalModel) :-
323		(RefusalModel == refusals_div ->
324		impl_diverges(X),
325		append(TraceY,[spec_cannot_diverge],RefusalTraceY)
326		; fail
327		).
328		not_refusals(X,YList,TraceX,TraceY,RefusalTraceX,RefusalTraceY,YEnabledList,_RefusalModel) :-
329		impl_stable(X),
330		prefix(TraceX,TraceY),
331		\+impl_trans(X,_A,_X2), % we have a deadlock here
332		spec_does_not_deadlock(YList),
333		%print('Deadlock in SpecY does not occur => FAILURE!'),nl,
334		append(TraceX,[refuse('Sigma')],RefusalTraceX),
335		findall(AA,(spec_stable_par_trans(YList,AA,_),AA\=tau),YListChoices),
336		remove_dups(YListChoices,YEnabledList),
337		get_refused_set(YEnabledList,RefusedSetY),
338		append(TraceY,[refuse(RefusedSetY)],RefusalTraceY).
339		not_refusals(X,YList,TraceX,TraceY,RefusalTraceX,RefusalTraceY,YEnabledList,RefusalModel) :-
340		impl_stable(X),
341		prefix(TraceX,TraceY),
342		impl_trans(X,A,X2),
343		impl_all_possible_actions(X,AllXActions),
344		get_refused_set(AllXActions,RefusedSet),
345		append(TraceX,[refuse(RefusedSet),go(A,X2)],NTX),
346		check_go_step_refusal(A,RefusedSet,X2,YList,NTX,TraceY,RefusalTraceX,RefusalTraceY,YEnabledList,RefusalModel).
347		not_refusals(X,YList,TraceX,TraceY,RefusalTraceX,RefusalTraceY,YEnabledList,RefusalModel) :-
348		unstable_state_with_enabled_visible_actions(X),
349		prefix(TraceX,TraceY),
350		%print(unstable_state_with_enabled_visible_actions),nl,
351		RefusedSet=bullet, % the bullet set
352		impl_non_tau_trans(X,A,X2),
353		append(TraceX,[refuse(RefusedSet),go(A,X2)],NTX),
354		check_go_step_refusal(A,RefusedSet,X2,YList,NTX,TraceY,RefusalTraceX,RefusalTraceY,YEnabledList,RefusalModel).
355		not_refusals(X,YList,TraceX,TraceY,RefusalTraceX,RefusalTraceY,YEnabledList,RefusalModel) :-
356		impl_trans(X,tau,X2),
357		append(TraceX,[refuse(bullet),go(tau_direct,X2)],NTX),
358		append(TraceY,[refuse(bullet),go(tau_direct,_)],NTY),
359		not_refusals(X2,YList,NTX,NTY,RefusalTraceX,RefusalTraceY,YEnabledList,RefusalModel).
360
361		check_go_step_refusal(Action,RefusedSet,NextXState,YList,NTX,TraceY,RefusalTraceX,RefusalTraceY,YEnabledList,RefusalModel) :-
362		(setof(Y2,spec_par_trans_bullet(YList,RefusedSet,Action,Y2),YS) ->
363		append(TraceY,[refuse(RefusedSet),go(Action,_)],NTY),
364		spec_tau_closure(YS,YTS,failures),
365		not_refusals(NextXState,YTS,NTX,NTY,RefusalTraceX,RefusalTraceY,YEnabledList,RefusalModel)
366		;
367		RefusalTraceX=NTX,
368		findall(AA,(spec_stable_par_trans(YList,AA,_),AA\=tau),YListChoices),
369		remove_dups(YListChoices,YEnabledList),
370		get_refused_set(YEnabledList,YRefusedSet),
371		append(TraceY,[refuse(YRefusedSet)],RefusalTraceY)
372		).
373
374		spec_does_not_deadlock([]).
375		spec_does_not_deadlock([Y|Ys]) :-
376		(impl_trans(Y,_A,_Y1) -> spec_does_not_deadlock(Ys) ; fail).
377
378		spec_list_contains_unexplored_node([ID|T]) :- % TO DO: we could do this check when generating YList ?
379		(spec_trans_not_complete(ID) -> assert_ref_check_incomplete(ID)
380		; spec_list_contains_unexplored_node(T)).
381
382		spec_trans_not_complete(ID) :- spec_not_all_transitions_added(ID).
383		spec_trans_not_complete(ID) :- spec_max_reached_for_node(ID).
384
385		check_spec_trans_complete(ID) :-
386		(spec_trans_not_complete(ID) -> assert_ref_check_incomplete(ID) ; true).
387
388		spec_par_trans_bullet([Y|_],RefusedSetX,A,Y2) :-
389		spec_stable(Y),
390		spec_all_possible_actions(Y,AllYActions),
391		get_refused_set(AllYActions,RefusedSetY),
392		special_ord_subset(RefusedSetX,RefusedSetY),
393		spec_trans(Y,A,Y2).
394		spec_par_trans_bullet([Y|_],RefusedSetX,A,Y2) :-
395		unstable_spec_state_with_enabled_visible_actions(Y),
396		RefusedSetY=bullet,
397		special_ord_subset(RefusedSetX,RefusedSetY),
398		spec_trans(Y,A,Y2).
399		spec_par_trans_bullet([_Y|YT],RefusedSetX,A,Y2) :-
400		spec_par_trans_bullet(YT,RefusedSetX,A,Y2).
401
402		special_ord_subset(SubSet,Set) :-
403		%print(special_ord_subset(SubSet,Set)),nl,
404		( SubSet == bullet ->
405		true
406		; Set == bullet ->
407		fail
408		;
409		ord_subset(SubSet,Set)
410		).
411
412		% in case we have a state with enabled visible and non-visible actions
413		% e.g. a -> STOP [> b -> STOP
414		unstable_state_with_enabled_visible_actions(State) :-
415		\+impl_stable(State),
416		impl_trans(State,A,_),
417		A\=tau.
418		impl_non_tau_trans(X,A,X2) :-
419		impl_trans(X,A,X2),
420		A\=tau.
421
422		unstable_spec_state_with_enabled_visible_actions(State) :-
423		\+spec_stable(State),
424		spec_trans(State,A,_),
425		A\=tau.
426
427		spec_stable_par_trans([Y|_],A,Y2) :-
428		impl_stable(Y),
429		spec_trans(Y,A,Y2).
430		spec_stable_par_trans([_|YT],A,Y2) :-
431		spec_stable_par_trans(YT,A,Y2).
432
433		spec_par_trans([Y|_],A,Y2) :-
434		spec_trans(Y,A,Y2).
435		spec_par_trans([_|YT],A,Y2) :-
436		spec_par_trans(YT,A,Y2).
437
438		%:- block translate_csp_b_event(-,?).
439		translate_csp_b_event(Event,R) :-
440		( with_csp_label(Event) -> remove_label_from_event(Event,'CSP',R)
441		; convert_to_csp_event(Event,R) % unified event in B mode (e.g. 'link(a,b)' instead of 'link.a.b')
442		).
443
444		l_translate_csp_b_event([],[]).
445		l_translate_csp_b_event([Event|T],[TEvent|R]) :- translate_csp_b_event(Event,TEvent),l_translate_csp_b_event(T,R).
446
447		:- assert_must_succeed((remove_label_from_event('CSP:in','CSP',R),R=='in')).
448		:- assert_must_succeed((remove_label_from_event('B:in','B',R),R=='in')).
449
450		remove_label_from_event(Event,Label,R) :- split_atom(Event,[':'],List),remove(List,Label,RList),ajoin(RList,R).
451
452		with_csp_label(Event) :- split_atom(Event,[':'],['CSP'|_]).
453
454		convert_to_csp_event(Event,CSPEvent) :- split_atom(Event, ['(',',',')'], DotEls),ajoin_with_sep(DotEls,'.',CSPEvent).
455
456		% compute tau closure of list of abstract nodes; fails if there is divergence in FD mode
457		% (as no refine check counter-example will be found)
458		spec_tau_closure(SpecList,TauClosure,FailuresModel) :-
459		spec_tau_closure_aux(SpecList,[],TauClosure,no_div,DIV),
460		%print(spec_tau_closure(SpecList,DIV,TauClosure, FailuresModel)),nl,
461		(FailuresModel = failure_divergences
462		-> DIV = no_div % if an abstract node diverges: it can do anything -> fail as no counter-example can be found
463		% note: fail after computing; to be able to store information for other checks
464		; /* WARNING: if DIV=div then could it be that not all successor nodes will be in TauClosure ??
465		Maybe with internal choice & tau_skip we are safe ??
466		if so TO DO : fix */
467		true
468		).
469
470		spec_tau_closure_aux([],Acc,Acc,D,D).
471		spec_tau_closure_aux([SpecState|T],Acc,Res,DivSoFar,DIVRes) :-
472		get_tau_closure(SpecState,SpecClosure,_,DIV),
473		comb_div(DIV,DivSoFar,NewDivSoFar),
474		ord_union(SpecClosure,Acc,NewAcc),
475		spec_tau_closure_aux(T,NewAcc,Res,NewDivSoFar,DIVRes).
476
477		%%%%%%%% DEAD CODE %%%%%%%%%
478		/*
479		old_spec_tau_closure(SpecList,Res) :-
480		tau_closure2(SpecList,SpecList,Res). %, print(tau_closure(SpecList,Res)),nl.
481
482
483		tau_closure2([],X,X).
484		tau_closure2([H|T],Acc,Res) :- setof(Succ,new_tau_succ(H,Acc,Succ),Succs),!,
485		ord_union(Succs,Acc,NewAcc), tau_closure2(Succs,NewAcc,NewAcc2),
486		tau_closure2(T,NewAcc2,Res).
487		tau_closure2([_|T],Acc,Res) :- tau_closure2(T,Acc,Res).
488
489		% find a new tau successor which is not yet in the accumulator list
490		new_tau_succ(H,Acc,Succ) :- spec_trans(H,tau,Succ), \+ member(Succ,Acc).
491		% TO DO if Succ in Acc --> return info that there is divergence
492		*/
493
494
495		impl_trans(From,Label,To) :- /* need to improve efficiency of that : */
496		impl_trans_term(From,Action1,To1),
497		(functor(Action1,'$setup_constants',_)
498		-> impl_trans(To1,Label,To)
499		; ref_generate_label(Action1,Label), To=To1 % for in-situ refinement we do not need the overhead of this !
500		).
501
502		in_situ_model_check(SpecNodeID,ResTrace,Type,ModelStyle,MaxNrOfNewNodes) :-
503		set_max_nr_of_new_impl_trans_nodes(MaxNrOfNewNodes),
504		interruptable_perform_mc(Type,ModelStyle,SpecNodeID,ResTrace).
505
506		:- use_module(probsrc(user_interrupts),[catch_interrupt_assertion_call/1]).
507		:- use_module(extension('user_signal/user_signal'), [user_interruptable_call_det/2]).
508
509		interruptable_perform_mc(Type,ModelStyle,SpecNodeID,ResTrace) :-
510		evaluate_argument('Events',R),
511		(is_not_infinite_type(R) -> true; assertz(haskell_csp:ignore_infinite_datatypes)),
512		user_interruptable_call_det(catch_interrupt_assertion_call(
513		refinement_checker: perform_mc(Type,ModelStyle,SpecNodeID,ResTrace)),InterruptResult),
514		(InterruptResult=interrupted -> ResTrace=[interrupted], print('Assertion check was interrupted by user!!!'),nl
515		; printsilent('Assertion check completed.'),nls),
516		retractall(haskell_csp:ignore_infinite_datatypes).
517
518		:- public perform_mc/4.
519		perform_mc('Deterministic',ModelStyle,X,T) :- !,deterministic_check(X,ModelStyle,T).
520		perform_mc('DeadlockFree',ModelStyle,X,T) :- !, deadlock_check(X,ModelStyle,T).
521		perform_mc('LivelockFree',_ModelStyle,X,T) :- !, divergence_check(X,T).
522		perform_mc(Style,_ModelStyle,_X,T) :- add_internal_error('Internal Error: Unknown checking style: ',Style), T=none_so_far.
523
524		% -----------------------
525
526		% DETERMINISM CHECKING
527
528		deterministic_check(X,ModelStyle,ResTrace) :-
529		det_check(X,TraceX,TraceY,YEnabledList,ModelStyle),
530		(TraceX==no_counter_example
531		-> ResTrace=no_counter_example %,print_message('No refinement counter example found') used to be all return value
532		; inst_list(TraceX,ResTrace0),
533		inst_list(TraceY,ResTrace1), /* convert pending free var into [] + go */
534		tcltk_execute_string_trace(X,TraceX),
535		append(ResTrace0,[' At_last_step_specification_can_do_one_of:'|YEnabledList],ResTraceX),
536		append(ResTraceX,[' Trace_of_the_left_specification:'|ResTrace1],ResTrace)
537		).
538
539		det_check(X,TraceX,TraceY,YEnabledList,ModelStyle) :-
540		reset_all_dynamic_state_predicates_for_determinism_check,
541		cputime(T1),
542		assertz(cur_det_id(X)),
543		% computing the pre-deterministic refinement P' of P
544		compute_predeterministic_process(X,PredRootId,ModelStyle),
545		cputime(T2),
546		%tcltk_interface: add_new_visited_expression(PredRootId,_Hash,[],root,off),
547		spec_tau_closure([PredRootId],InitialsRootId,failures),
548		( ModelStyle=failure_divergences,determinism_check_div_found(PredRootId) ->
549		dfs_search(PredRootId,false,true,TraceX),cputime(T3),print_state_from_id(X),
550		print(' reaches a divergence.'),nl,
551		print(TraceX),nl,TraceY=TraceX
552		% after computing P' we check wheter P' is refinement of P: P' [F= P
553		% if P' [F= P is true we proved that P is deterministic, otherwise P is not deterministic
554		;not_refines(X,InitialsRootId,TraceX,TraceY,YEnabledList,ModelStyle) ->
555		cputime(T3),print_state_from_id(X), print(' reaches a '), print('non deterministic choice'),nl,
556		print(TraceX),nl
557		; cputime(T3),print_state_from_id(X),print(' is '),print('deterministic'),nl,TraceX=no_counter_example
558		),
559		printsilent('% Generating P\' Time : '), D1 is T2-T1, printsilent(D1), printsilent(' ms'),nls,
560		printsilent('% Checking P\' [F= P Time: '), D2 is T3-T2, printsilent(D2), printsilent(' ms'),nls,
561		printsilent('% Overall Checking Time: '), D is T3-T1, printsilent(D), printsilent(' ms'),nls.
562
563		reset_all_dynamic_state_predicates_for_determinism_check :-
564		retractall(predet_node_presentation(_,_)),
565		retractall(cur_det_id(_)),
566		retractall(not_all_det_transitions_added(_)).
567
568		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
569		%%%%%%%% Generating the pre-deterministic refinement P' of P %%%%%%%%
570		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
571
572		:- dynamic generated_predeterministic_refinement/3,determinism_check_div_found/1.
573
574
575		% initialising the root state of P'
576		compute_predeterministic_process(RootNode,NewRootNode,ModelStyle) :-
577		generated_predeterministic_refinement(RootNode,ModelStyle,NewRootNode),
578		debug_println(9,'%%%% Pre-deterministic Refinement P\' has been already generated.'),!.
579		compute_predeterministic_process(RootNode,NewRootNode,ModelStyle) :-
580		(ModelStyle = failure_divergences -> CheckDIV=true; CheckDIV=false),
581		get_tau_loop_closure1(RootNode,Closure,false),
582		get_predeterministic_node_id1(NewRootNode),
583		assertz(predet_node_presentation(NewRootNode,Closure)),
584		debug_println(9,tau_closure(NewRootNode,Closure)),
585		add_id_to_stack(NewRootNode),
586		generate_predeterministic_process_state_space(NewRootNode,CheckDIV),
587		assertz(generated_predeterministic_refinement(RootNode,ModelStyle,NewRootNode)).
588
589		generate_predeterministic_process_state_space(RootNode,CheckDIV) :-
590		% in case we found div state and we check for divergence as well then
591		% do not explore the pre-deterministic state space any more.
592		(CheckDIV=true,determinism_check_div_found(RootNode) -> fail; true),
593		% otherwise explore the pre-deterministic state space until stack is empty
594		pop_id_from_stack(NodeId),!,
595		predet_node_presentation(NodeId,Closure), % tau loop closure already explored
596		add_all_predeterministic_transitions_fail_loop(NodeId,Closure,CheckDIV,RootNode),
597		debug_println(9,tau_closure(NodeId,Closure)),
598		generate_predeterministic_process_state_space(RootNode,CheckDIV).
599		generate_predeterministic_process_state_space(_RootNode,_CheckDIV).
600
601
602		% simple stack implementation used for generating the pre-deterministic refienement P' of P
603		:- dynamic not_all_det_transitions_added/1.
604
605		add_id_to_stack(NewNodeId) :-
606		asserta(not_all_det_transitions_added(NewNodeId)).
607
608		pop_id_from_stack(NodeId) :-
609		retract(not_all_det_transitions_added(NodeId)).
610
611		:- use_module(probsrc(gensym),[gensym/2]).
612		get_predeterministic_node_id1(NewId) :-
613		cur_det_id(ID),
614		ID1 is ID + 1,
615		gensym('det',NewId),
616		retract(cur_det_id(ID)),
617		assertz(cur_det_id(ID1)).
618
619		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
620		%%%%%%%% Computing SCCs %%%%%%%%
621		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
622
623
624		:- dynamic predet_node_presentation/2, cur_det_id/1.
625
626		get_tau_loop_closure1(State,Closure,Test) :-
627		get_max_tau_loop_closure([State],[],[],Closure,Test).
628
629		get_max_tau_loop_closure([],_LV,Closure,Closure,_Test).
630		get_max_tau_loop_closure(Waiting,LoopVisited,Closure_so_far,MaxClosure,Test) :-
631		Waiting=[State|Rest],
632		(\+member(State,LoopVisited) ->
633		get_tau_loop_closure(State,Closure,LoopVisited,Test),
634		ord_add_element(LoopVisited, State, LoopVisited1),
635		ord_union(Closure_so_far,Closure,Closure1),
636		ord_intersection(LoopVisited1,Closure1,Visited,NewToClosure),
637		ord_union(NewToClosure,Rest,Waiting2),
638		ord_intersection(Visited,Waiting2,_Inter,Waiting1)
639		;
640		Waiting1=Rest,LoopVisited1=LoopVisited,Closure1=Closure_so_far
641		),
642		get_max_tau_loop_closure(Waiting1,LoopVisited1,Closure1,MaxClosure,Test).
643
644		get_tau_loop_closure(State,Closure,LoopVisited,Test) :-
645		setof(SCC,compute_tau_scc(State,State,LoopVisited,[],SCC,Test),SCCs),
646		append(SCCs,Closure1),
647		list_to_ord_set(Closure1,Closure).
648
649		compute_tau_scc(State,RootState,LoopVisited,SCC,SCCRes,Test) :-
650		\+memberchk(State,LoopVisited),
651		\+memberchk(State,SCC),
652		impl_trans_test(Test,State,tau,Succ),
653		(Succ=RootState ->
654		SCCRes=[State|SCC]
655		;
656		compute_tau_scc(Succ,RootState,LoopVisited,[State|SCC],SCCRes,Test)
657		).
658		compute_tau_scc(RootState,RootState,_LoopVisited,_SCC,[RootState],_Test).
659
660		%-----------------------------------------------------------
661		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
662		%%%%%%%% Computing all possible transitions from the current pre-deterministic state %%%%%%%%
663		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
664
665
666		add_all_predeterministic_transitions_fail_loop(CurState,CurClosure,CheckDIV,RootNode) :-
667		specify_possible_transition(CurState,CurClosure,Action,SuccClosure,CheckDIV,RootNode),
668		add_predeterministic_transitions(CurState,CurClosure,Action,SuccClosure,_SuccState),fail.
669		add_all_predeterministic_transitions_fail_loop(_NewRootNode,_Closure,_CheckDIV,_RootNode).
670
671		specify_possible_transition(CurState,CurClosure,Action,SuccClosure,CheckDIV,RootNode) :-
672		((CheckDIV=true,length(CurClosure,N),N>1) ->
673		% more than two states in closure means that we have tau loop scc in the original state space,
674		% which is definitely a case of divergence
675		assertz(determinism_check_div_found(RootNode)),
676		assertz(transition(CurState,tau,no_id,CurState)),
677		debug_println(9,transition(CurState,tau,specify,CurState))
678		; true
679		),
680		(impl_tau_transition_from_closure(CurClosure,SuccNode) ->
681		% we add a random single tau transition leading to a state outside the closure of the current SCC
682		% to the state space of P'
683		Action=tau,
684		debug_println(9,add_transition(CurState,tau)),
685		get_tau_loop_closure1(SuccNode,SuccClosure,false),! /* no more transitions should be added */
686		;
687		% if state is stable then add a single visible event to the pre-deterministic refinement P'
688		% for each visible event that the closure of states in P can perform
689		get_visible_transition(CurState,CurClosure,Action,SuccNode),
690		get_tau_loop_closure1(SuccNode,SuccClosure,false)
691		).
692
693		impl_tau_transition_from_closure(Closure,SuccNode) :-
694		%random_select(Node,Closure,_Rest), % random_select inserts a cut after unifying Node
695		random_permutation(Closure,Closure1),!,
696		member(Node,Closure1),
697		impl_trans(Node,tau,SuccNode),
698		\+memberchk(SuccNode,Closure). %
699
700		get_visible_transition(State,Closure,Action,SuccNode) :-
701		%random_select(Node,Closure,_Rest),
702		random_permutation(Closure,Closure1),!,
703		member(Node,Closure1),
704		impl_trans(Node,Action,SuccNode),
705		Action\=tau,
706		% adding only one visible transition to the pre-deterministic state
707		\+transition(State,Action,_TransID,_CurState).
708
709		add_predeterministic_transitions(CurState,CurClosure,Action,SuccClosure,NextState) :-
710		(ord_seteq(CurClosure,SuccClosure) ->
711		(\+transition(CurState,Action,_TransID,CurState) ->
712		assertz(transition(CurState,Action,no_id,CurState)),
713		debug_println(9,transition(CurState,Action,pred1,CurState))
714		; true % do not add any transition
715		)
716		;
717		(predet_node_presentation(NextState,SuccClosure) -> % state already added to state space of the pre-deterministic refinement P'
718		assertz(transition(CurState,Action,no_id,NextState)),
719		debug_println(9,transition(CurState,Action,pred2,NextState))
720		;
721		get_predeterministic_node_id1(NextState),
722		assertz(transition(CurState,Action,no_id,NextState)),
723		debug_println(9,transition(CurState,Action,pred3,NextState)),
724		assertz(predet_node_presentation(NextState,SuccClosure)),
725		add_id_to_stack(NextState)
726		)
727		).
728
729		%-----------------------------------------------------------------------------
730
731		impl_trans_test(IsTestCase,From,Label,To) :-
732		(IsTestCase=true -> test_transition(From,Label,To) ; impl_trans(From,Label,To)).
733
734		/* Examples for testing the implementation of get_tau_loop_closure1/3. */
735		%% :- discontiguous test_transition/3.
736		:- dynamic test_transition/3.
737
738		:- assert_must_succeed((
739		assertz(test_transition(2,tau,4)),
740		assertz(test_transition(2,tau,3)),
741		assertz(test_transition(3,tau,5)),
742		assertz(test_transition(3,tau,11)),
743		assertz(test_transition(4,b,6)),
744		assertz(test_transition(5,tau,3)),
745		assertz(test_transition(5,c,8)),
746		assertz(test_transition(5,c,9)),
747		assertz(test_transition(5,k,10)),
748		assertz(test_transition(11,v,12)),
749		assertz(test_transition(11,tau,13)),
750		assertz(test_transition(11,tau,3)),
751		assertz(test_transition(13,tau,11)),
752		assertz(test_transition(13,w,15)),
753		refinement_checker: reset_all_dynamic_state_predicates_for_determinism_check,
754		refinement_checker: get_tau_loop_closure1(2,Closure1,true), Closure1==[2],
755		refinement_checker: reset_all_dynamic_state_predicates_for_determinism_check,
756		refinement_checker: get_tau_loop_closure1(3,Closure2,true), Closure2==[3,5,11,13],
757		refinement_checker: reset_all_dynamic_state_predicates_for_determinism_check,
758		refinement_checker: get_tau_loop_closure1(4,Closure3,true), Closure3==[4],
759		retractall(test_transition(_,_,_)))).
760
761		:- assert_must_succeed((
762		assertz(test_transition(22,tau,23)),
763		assertz(test_transition(22,tau,24)),
764		assertz(test_transition(23,a,28)),
765		assertz(test_transition(23,tau,26)),
766		assertz(test_transition(24,tau,25)),
767		assertz(test_transition(25,tau,30)),
768		assertz(test_transition(26,tau,27)),
769		assertz(test_transition(27,tau,26)),
770		assertz(test_transition(27,a,28)),
771		assertz(test_transition(30,tau,24)),
772		assertz(test_transition(30,a,27)),
773		refinement_checker: reset_all_dynamic_state_predicates_for_determinism_check,
774		refinement_checker: get_tau_loop_closure1(22,Closure1,true), Closure1==[22],
775		refinement_checker: reset_all_dynamic_state_predicates_for_determinism_check,
776		refinement_checker: get_tau_loop_closure1(26,Closure2,true), Closure2==[26,27],
777		refinement_checker: reset_all_dynamic_state_predicates_for_determinism_check,
778		refinement_checker: get_tau_loop_closure1(25,Closure3,true), Closure3==[24,25,30],
779		refinement_checker: reset_all_dynamic_state_predicates_for_determinism_check,
780		refinement_checker: get_tau_loop_closure1(30,Closure4,true), Closure4==[24,25,30],
781		retractall(test_transition(_,_,_)))).
782
783		:- assert_must_succeed((
784		assertz(test_transition(32,tau,34)),
785		assertz(test_transition(34,a,36)),
786		assertz(test_transition(34,tau,35)),
787		assertz(test_transition(35,tau,37)),
788		assertz(test_transition(35,tau,38)),
789		assertz(test_transition(37,tau,35)),
790		assertz(test_transition(37,b,40)),
791		assertz(test_transition(38,v,39)),
792		assertz(test_transition(38,tau,32)),
793		refinement_checker: reset_all_dynamic_state_predicates_for_determinism_check,
794		refinement_checker: get_tau_loop_closure1(32,Closure1,true), Closure1==[32,34,35,37,38],
795		refinement_checker: reset_all_dynamic_state_predicates_for_determinism_check,
796		refinement_checker: get_tau_loop_closure1(38,Closure2,true), Closure2==[32,34,35,37,38],
797		retractall(test_transition(_,_,_)))).
798
799		:- assert_must_succeed((
800		assertz(test_transition(102,tau,103)),
801		assertz(test_transition(103,tau,102)),
802		assertz(test_transition(103,tau,104)),
803		assertz(test_transition(104,tau,103)),
804		assertz(test_transition(104,tau,107)),
805		assertz(test_transition(107,tau,104)),
806		assertz(test_transition(102,tau,105)),
807		assertz(test_transition(105,tau,102)),
808		assertz(test_transition(105,w,106)),
809		refinement_checker: reset_all_dynamic_state_predicates_for_determinism_check,
810		refinement_checker: get_tau_loop_closure1(102,Closure1,true), Closure1==[102,103,104,105,107],
811		refinement_checker: reset_all_dynamic_state_predicates_for_determinism_check,
812		refinement_checker: get_tau_loop_closure1(107,Closure2,true), Closure2==[102,103,104,105,107],
813		refinement_checker: reset_all_dynamic_state_predicates_for_determinism_check,
814		refinement_checker: get_tau_loop_closure1(105,Closure3,true), Closure3==[102,103,104,105,107],
815		retractall(test_transition(_,_,_)))).
816
817		:- assert_must_succeed((
818		assertz(test_transition(202,tau,203)),
819		assertz(test_transition(203,tau,202)),
820		assertz(test_transition(203,tau,204)),
821		assertz(test_transition(204,tau,203)),
822		refinement_checker: reset_all_dynamic_state_predicates_for_determinism_check,
823		refinement_checker: get_tau_loop_closure1(202,Closure,true), Closure==[202,203,204],
824		retractall(test_transition(_,_,_)))).
825		%-------------------------------------------------------------------------------------------------
826
827		:- dynamic dvisited/1. % true if a node has been seen during dfs traversal
828
829		% -----------------------
830
831		% DEADLOCK CHECKING
832
833
834		deadlock_check(X,ModelStyle,Trace) :- DLK=true,
835		(ModelStyle=failure_divergences -> DIV=true ;
836		ModelStyle=trace -> add_error(deadlock_check,'Trace model cannot be used for deadlock checking'), DIV=false
837		; DIV=false),
838		dfs_check(X,Trace,DLK,DIV).
839
840		:- dynamic dincomplete/0.
841		dfs_check(X,ResTrace,DLK,DIV) :-
842		retractall(dvisited(_)), retractall(tau_closure(_,_,_,_)),retractall(dincomplete),
843		cputime(T1),
844		(dfs_search(X,DLK,DIV,Trace1) ->
845		cputime(T2),print_state_from_id(X), print(' reaches a '), printDD(DLK,DIV),nl,
846		printsilent(Trace1),nls,
847		inst_list(Trace1,ResTrace),
848		tcltk_execute_string_trace(X,Trace1)
849		; dincomplete -> cputime(T2),print('No '),printDD(DLK,DIV), print('found so far for :'),
850		print_state_from_id(X),nl, ResTrace=none_so_far
851		; cputime(T2),print_state_from_id(X), print(' is '),printDD(DLK,DIV), print('free'),nl,ResTrace=no_counter_example
852		),
853		(silent_mode(on) -> true ; print('% Checking Time: '), D is T2-T1, print(D), print(' ms'),nl).
854
855		dfs_search(X,_,_DIV,_) :- dvisited(X),!, %print(already_visited(X)),nl,
856		% (DIV\=true, TO DO: check that we have not ignored tau or visible transitions in this loop)
857		fail.
858		%dfs_search(X,_,_DIV,_) :- % comment this clause in if you do not want omega to count as deadlock; FDR does !
859		% visited_expression(X,omega),!, assertz(dvisited(X)),fail. % this is a termination node; do not look for deadlock or other errors from it
860		dfs_search(X,DLK,_,[deadlocks]) :- DLK=true,\+ impl_trans_term(X,_,_),!, % will compute transitions if necessary
861		(not_all_transitions_added(X) -> (dincomplete -> assertz(dincomplete),fail) ; true).
862		dfs_search(X,DLK,DIV,Result) :-
863		get_tau_closure(X,Closure,Stable,Diverges),
864		assertz(dvisited(X)),
865		(DIV=true, Diverges=div
866		-> Result = [diverges], debug_println(19,diverges(X,Closure))
867		; Stable=unstable_prio(Dest) -> /* only perform the first priority tau transitions */
868		Result=[go(tau,Y)|R2],
869		member(Y,Dest), dfs_search(Y,DLK,DIV,R2)
870		; % Stable=[X] ->
871		Result=[go(A,Y)|R2], impl_trans(X,A,Y), dfs_search(Y,DLK,DIV,R2)
872		% ; Result=[go(tau,Y)|R2], member(Y,Stable), dfs_search(Y,DLK,DIV,R2)
873		).
874
875
876		printDD(DLK,DIV) :- (DLK=true -> print('deadlock ') ; true),
877		(DIV=true -> print('divergence ') ; true).
878
879		% -----------------------
880
881		% DIVERGENCE CHECKING
882
883		divergence_check(X,Trace) :- DLK=false,DIV=true,dfs_check(X,Trace,DLK,DIV).
884
885
886		:- dynamic tau_visited/2,tau_closure/4, tau_loop_back_node/1.
887
888		impl_diverges(State) :- get_tau_closure(State,_,_,div).
889
890		% we could provide an optimized version of the code below for just checking divergence
891		% this would be sufficient in FD mode for refinement checking and in deadlock/livelock checking
892		get_tau_closure(State,Closure,Stable,DIV) :- tau_closure(State,C,S,D),!,Closure=C, Stable=S,DIV=D.
893		get_tau_closure(State,Closure,Stable,DIV) :- retractall(tau_visited(_,_)),
894		compute_tau_closure(State,Closure,Stable,DIV).
895
896		get_tau_closure2(State,Closure,Stable,DIV) :- tau_closure(State,C,S,D),!,Closure=C, Stable=S,DIV=D.
897		get_tau_closure2(State,Closure,Stable,DIV) :- compute_tau_closure(State,Closure,Stable,DIV).
898
899		compute_tau_closure(State,Closure,Stable,DIV) :-
900		(tau_priority_transition(State,Span,_)
901		-> Prio = prio, findall(To,tau_priority_transition(State,Span,To),Dest), sort(Dest,SDest),
902		assertz(tau_visited(State,SDest)) % remember that we did not inspect all tau successors, only Dest
903		; Prio = all, findall(To,tau_transition(State,_,To),Dest),
904		assertz(tau_visited(State,[]))
905		),
906		%print(visiting(State,Dest,Prio)),nl,
907		(Dest=[]
908		-> /* stable state */
909		DivOccurred = no_div, TauClosure=[State],
910		DStable = stable
911		; /* unstable state */
912		sort(Dest,SDest),
913		comp_dest_tau_clos(SDest,[],DestTauClosure,no_div,DivOccurred),
914		(((DivOccurred=no_div ; \+ tau_loop_back_node(State)),
915		Prio=prio)
916		-> DStable = unstable_prio(SDest), % it is safe to only treat the priority tau transitions in this node
917		TauClosure = DestTauClosure % also: we do not need to add this node to the tau-closure
918		; DStable = unstable,
919		ord_union([State],DestTauClosure,TauClosure) % also add node itself
920		)
921		),
922		assertz(tau_closure(State,TauClosure,DStable,DivOccurred)),
923		check_spec_trans_complete(State),
924		Closure=TauClosure, DIV=DivOccurred, Stable=DStable.
925
926		comp_dest_tau_clos([],CLOS,CLOS,DIV,DIV).
927		comp_dest_tau_clos([Dest|T],CLOS_sofar,CLOS_RES,DIV_sofar,DIVRES) :-
928		((tau_visited(Dest,PriorList), /* we have seen the node before */
929		\+ tau_closure(Dest,_,_,_)) /* its treatment is not complete; i.e., we have a loop */
930		-> /* we have divergence */
931		% print(tau_loop(Dest,PriorList)),nl,
932		% ord_union([Dest],CLOS_sofar,CLOS_RES) % Dest already in closure
933		DIV_sofar2=div,
934		(PriorList=[] -> CLOS_sofar2=CLOS_sofar
935		; /* we did not add all successors of Dest yet */
936		retract(tau_visited(Dest,_)),
937		assertz(tau_visited(Dest,[])),
938		assertz(tau_loop_back_node(Dest)),
939		findall(To,tau_transition(Dest,_,To),AllDestSuccs),
940		sort([Dest|AllDestSuccs],SADS), % also add Dest; it was not yet added ?? <------- TODO: check
941		ord_subtract(SADS,PriorList,DestIgnored),
942		% print(adding_ignored_succs(Dest,DestIgnored)),nl,
943		comp_dest_tau_clos(DestIgnored,CLOS_sofar,CLOS_sofar2,div,_)
944		),
945		comp_dest_tau_clos(T,CLOS_sofar2,CLOS_RES,DIV_sofar2,DIVRES)
946		; get_tau_closure2(Dest,DClos,_DStable,DIV),
947		comb_div(DIV,DIV_sofar,DIV_sofar2),
948		ord_union(CLOS_sofar,DClos,CLOS_sofar2), % combine states reachable via tau
949		comp_dest_tau_clos(T,CLOS_sofar2,CLOS_RES,DIV_sofar2,DIVRES)).
950
951		comb_div(div,_,div).
952		comb_div(no_div,D,D).
953
954		%%% size_of_tables/0 have only debugging purpose
955		/*
956		:- public size_of_tables/0.
957		size_of_tables :- print_size_of_table(refinement_checker:not_refines_table/3).
958		*/
959
960		reset_refinement_checker :-
961		retractall(abstract_spec_file(_)),
962		retractall(tau_visited(_,_)),
963		retractall(tau_loop_back_node(_)),
964		retractall(not_refusals_table(_,_,_)),
965		retractall(not_refines_table(_,_,_)),
966		retractall(dvisited(_)), retractall(tau_closure(_,_,_,_)),retractall(dincomplete),
967		retractall(generated_predeterministic_refinement(_,_,_)),
968		retractall(determinism_check_div_found(_)).
969
970		:- use_module(probsrc(eventhandling),[register_event_listener/3]).
971		:- register_event_listener(clear_specification,reset_refinement_checker,
972		'Reset Refinement Checker.').
973		:- register_event_listener(specification_initialised,reset_refine_spec,
974		'Start-up Refinement Checker.'). % reset_refine_spec needs to know B mode or CSP mode
975		:- register_event_listener(change_of_animation_mode,reset_refine_spec,
976		'Start-up Refinement Checker.'). % reset_refine_spec needs to know B mode or CSP mode
977
978
979		refine_check(X,SpecY,TraceX,TraceY,YEnabledList,FailuresModel) :-
980		retractall(ref_check_incomplete),
981		retractall(not_refusals_table(_,_,_)),
982		retractall(not_refines_table(_,_,_)),
983		% ( (not_refines(X,InitialsY,TraceX,YEnabledList,FailuresModel) , TraceY=TraceX)
984		(csp_mode ->
985		evaluate_argument('Events',R),
986		/* Needed for the Trace Debugger of the Refinement Checker.
987		It prohibits to expand an infinite data type structures when a counter example has been found.
988		TODO: Consider a more sophisticated solution. This code fragment adds unnecessary overhead to every assertion check.*/
989		(is_not_infinite_type(R) -> true ; assertz(haskell_csp:ignore_infinite_datatypes))
990		; true),
991		(spec_tau_closure([SpecY],InitialsY,FailuresModel),
992		not_refines_or_refusals(X,InitialsY,TraceX0,TraceY,YEnabledList,FailuresModel)
993		->
994		nl,print_state_from_id(X),
995		(ref_check_incomplete -> write(' may *not* be ') ; write(' is *not* a ')),
996		print_ref(FailuresModel),
997		print_abstract_spec_state_from_id(SpecY),nl,
998		(debug_mode(off) -> true
999		; print('Trace of implementation '), print_state_from_id(X),nl,print(TraceX0),nl,
1000		print('Trace of abstraction '), print_abstract_spec_state_from_id(SpecY),nl,print(TraceY),nl,
1001		print('Events enabled at last step of '),print_abstract_spec_state_from_id(SpecY),nl,
1002		print(YEnabledList),nl,
1003		(impl_trans_not_complete(ID1) -> format('Impl. not complete, e.g., for ~w~n',[ID1]) ; true),
1004		(spec_trans_not_complete(ID2) -> format('Abst. not complete, e.g., for ~w~n',[ID2]) ; true)
1005		),
1006		(ref_check_incomplete -> TraceX=no_counter_example_found ; TraceX = TraceX0)
1007		;
1008		(silent_mode(on) -> true
1009		; print_state_from_id(X), print(' is a '), print_ref(FailuresModel),
1010		print_abstract_spec_state_from_id(SpecY),nl
1011		),
1012		(ref_check_incomplete -> TraceX=no_counter_example_found ; TraceX = no_counter_example)
1013		), retractall(haskell_csp:ignore_infinite_datatypes).
1014
1015		not_refines_or_refusals(X,InitialsY,TraceX,TraceY,YEnabledList,FailuresModel) :-
1016		((FailuresModel == refusals ; FailuresModel == refusals_div) ->
1017		not_refusals(X,InitialsY,[],[],RefusalTraceX,RefusalTraceY,YEnabledList,FailuresModel),
1018		TraceX=RefusalTraceX,
1019		TraceY=RefusalTraceY
1020		;
1021		not_refines(X,InitialsY,TraceX,TraceY,YEnabledList,FailuresModel)
1022		).
1023
1024		:- use_module(probsrc(tools),[get_tail_filename/2]).
1025		% print state from abstract specification:
1026		print_abstract_spec_state_from_id(ID) :- abstract_spec_file(File),!,
1027		write_file(File),
1028		(ID=root -> true ; write(':'), print_state_from_id(ID)).
1029		print_abstract_spec_state_from_id(ID) :- print_state_from_id(ID).
1030
1031		:- use_module(probsrc(specfile),[currently_opened_file/1]).
1032		print_state_from_id(root) :- !,
1033		(currently_opened_file(File) -> write_file(File) ; write(root)).
1034		print_state_from_id(ID) :- visited_expression(ID,State),
1035		print_state(State).
1036		print_ref(FailuresModel) :- print(FailuresModel), print(' refinement of ').
1037
1038		write_file(File) :- (debug_mode(on) -> write(File)
1039		; get_tail_filename(File,TF), write(TF)).
1040
1041		:- dynamic abstract_spec_file/1.
1042		tcltk_load_refine_spec_file(SpecFile) :-
1043		print_message(loading_refine_spec(SpecFile)),
1044		retractall(abstract_spec_file(_)),
1045		user_consult_without_redefine_warning(SpecFile),
1046		assert(abstract_spec_file(SpecFile)). % TODO: maybe store model name in refine_spec file
1047
1048		tcltk_refinement_search(ResTrace,FailuresModel,MaxNrOfNewNodes) :-
1049		refinement_search(root,root,ResTrace,FailuresModel,MaxNrOfNewNodes).
1050
1051		% A Procedure to do in_situ_refinement search: impl_trans & spec_trans are represented in the same state_space
1052		% FailuresModel : {singleton_failures, failures, failure_divergences, trace}
1053		in_situ_ref_search(ImplNode,SpecNode,ResTrace,FailuresModel,MaxNrOfNewNodes) :-
1054		% TO DO: redirect spec_trans,... to impl_trans ....
1055		% retractall(spec_trans(_,_,_)),
1056		% assertz((spec_trans(From,Label,To) :- impl_trans(From,Label,To))),
1057		interruptable_refinement_search(ImplNode,SpecNode,ResTrace,FailuresModel,MaxNrOfNewNodes).
1058
1059
1060		interruptable_refinement_search(ImplNode,SpecNode,ResTrace,FailuresModel,MaxNrOfNewNodes) :-
1061		get_total_number_of_errors(Tot1),
1062		user_interruptable_call_det(
1063		catch_interrupt_assertion_call(
1064		refinement_checker: refinement_search(ImplNode,SpecNode,ResTrace,FailuresModel,MaxNrOfNewNodes)),
1065		InterruptResult),
1066		get_total_number_of_errors(Tot2), NrErrs is Tot2-Tot1,
1067		(InterruptResult=interrupted
1068		-> ResTrace=[interrupted], print("Refinement check was interrupted by user!!!"),nl
1069		; NrErrs>0 -> % real_error_occurred
1070		add_error(refinement_check_fails,'Errors occurred while refinement checking:',NrErrs)
1071		% we no longer fail; the error could also be a CSP type error, or something caused by the user spec
1072		; printsilent('Refinement check completed.'),nls
1073		).
1074
1075
1076		valid_failures_model(failures,'F').
1077		valid_failures_model(failure_divergences,'FD').
1078		valid_failures_model(singleton_failures,'SF').
1079		valid_failures_model(trace,'T').
1080		valid_failures_model(refusals,'R').
1081		valid_failures_model(refusals_div,'RD').
1082		valid_failures_model(revival,'V').
1083		valid_failures_model(revival_div,'VD'). % not yet supported
1084
1085		check_valid_failures_model(FailuresModel,ShortCut) :-
1086		(valid_failures_model(FailuresModel,S) -> ShortCut=S
1087		; ShortCut='T',
1088		add_warning(refinement_checker,'Invalid failures model: ',FailuresModel)
1089		).
1090
1091		:- use_module(probsrc(debug)).
1092		%:- use_module(probcspsrc(haskell_csp),[channel_type_list/2]).
1093		refinement_search(ImplNode,SpecNode,ResTrace,FailuresModel,MaxNrOfNewNodes) :-
1094		debug_println(9,refinement_search(ImplNode,SpecNode,ResTrace,FailuresModel,MaxNrOfNewNodes)),
1095		check_valid_failures_model(FailuresModel,ShortCut),
1096		set_max_nr_of_new_impl_trans_nodes(MaxNrOfNewNodes),
1097		cputime(T1),
1098		refine_check(ImplNode,SpecNode,TraceX,TraceY,YEnabledList,FailuresModel),
1099		cputime(T2),
1100		D is T2-T1, formatsilent('% Refinement Check [~w=] CPU Time: ~w ms~n',[ShortCut,D]),
1101		(possible_atomic_ref_check_result(TraceX)
1102		-> ResTrace=TraceX %,print_message('No refinement counter example found') used to be all return value
1103		; inst_list(TraceX,ResTrace0),
1104		inst_list(TraceY,ResTrace1), /* convert pending free var into [] + go */
1105		(tcltk_execute_string_trace(ImplNode,TraceX) -> true
1106		; add_warning(refinement_checker,'Could not execute trace in animator: ',TraceX)
1107		),
1108		append(ResTrace0,[' At_last_step_specification_can_do_one_of:'|YEnabledList],ResTraceX),
1109		append(ResTraceX,[' Trace_of_the_left_specification:'|ResTrace1],ResTrace)
1110		%,print('Result trace: '),print(ResTrace),nl
1111		). %size_of_tables.
1112
1113		possible_atomic_ref_check_result(V) :- var(V),!,fail. % the checker returns open-ended lists
1114		possible_atomic_ref_check_result(no_counter_example).
1115		possible_atomic_ref_check_result(no_counter_example_found).
1116
1117		inst_list([],R) :- !,R=[].
1118		inst_list([go(tau_direct,_ID)|T],['GO:',tau|IT]) :- !, inst_list(T,IT). % NOTE : can be multiple taus now
1119		inst_list([go(Op,_ID)|T],['GO:',Op|IT]) :- csp_mode,!, inst_list(T,IT).
1120		inst_list([go(Op,_ID)|T],[Op|IT]) :- !, inst_list(T,IT).
1121		inst_list([spec_cannot_diverge|T],['DIVERGES'|IT]) :- !, inst_list(T,IT).
1122		inst_list([diverges|T],['DIVERGES'|IT]) :- !, inst_list(T,IT).
1123		inst_list([deadlocks|T],['DEADLOCKS'|IT]) :- !, inst_list(T,IT).
1124		inst_list([not_enabled(Op)|T],['NOT_ENABLED:',Op|IT]) :- !,inst_list(T,IT).
1125		inst_list([determ(Op1,_ID1,Op2,_ID2)|T],['DETERMINISM_BY_EVENT:',Op1,Op2|IT]) :- !,inst_list(T,IT).
1126		inst_list([cannot_refuse_compl(Ops)|T],Res) :-
1127		append(['CANNOT_REFUSE_COMPL:'|Ops],IT,Res),
1128		inst_list(T,IT).
1129		inst_list([cannot_refuse(Ops)|T],Res) :-
1130		append(['CANNOT_REFUSE:'|Ops],IT,Res),
1131		inst_list(T,IT).
1132		inst_list([refuse('Sigma')|T],Res) :-
1133		append(['REFUSED_SET:','Sigma'],IT,Res),
1134		inst_list(T,IT).
1135		inst_list([refuse(bullet)|T],Res) :-
1136		append(['REFUSED_SET:',bullet],IT,Res),
1137		inst_list(T,IT).
1138		inst_list([refuse(Ops)|T],Res) :-
1139		append(['REFUSED_SET:'|Ops],IT,Res),
1140		inst_list(T,IT).
1141
1142
1143		tcltk_execute_string_trace(StartNode,Trace) :- /* can be useful for TestCase Generation */
1144		%state_space_reset,
1145		tcltk_interface:tcltk_execute_trace_to_node(StartNode),
1146		% TO DO: check if not too expensive; usually StartNode will be root or an immediate successor of root
1147		execute_string_trace_to_node(Trace),!.
1148		tcltk_execute_string_trace(StartNode,Trace) :-
1149		format_error('Could not execute trace from state ~w: ~w~n',[StartNode,Trace]).
1150
1151		execute_string_trace_to_node([]) :- !.
1152		execute_string_trace_to_node([spec_cannot_diverge|T]) :- !, execute_string_trace_to_node(T).
1153		execute_string_trace_to_node([deadlocks|T]) :- !, execute_string_trace_to_node(T).
1154		execute_string_trace_to_node([diverges|T]) :-
1155		current_state_id(CurID),
1156		find_tau_trace_to(CurID,divergence,NewTrace,T),!,
1157		execute_string_trace_to_node(NewTrace).
1158		execute_string_trace_to_node([not_enabled(_)|T]) :- !, execute_string_trace_to_node(T).
1159		execute_string_trace_to_node([cannot_refuse_compl(_)|T]) :- !, execute_string_trace_to_node(T).
1160		execute_string_trace_to_node([cannot_refuse(_)|T]) :- !, execute_string_trace_to_node(T).
1161		execute_string_trace_to_node([refuse(_)|T]) :- !, execute_string_trace_to_node(T).
1162		execute_string_trace_to_node([go('$initialise_machine',ID)|T]) :-
1163		current_state_id(CurID),
1164		transition(CurID,Action,ID),
1165		functor(Action,'$initialise_machine',_),!,
1166		tcltk_interface:tcltk_perform_action(Action,ID),
1167		execute_string_trace_to_node(T).
1168		execute_string_trace_to_node([go('$initialise_machine',ID)|T]) :-
1169		/* special case for CurID=root, as setup_constants get merged
1170		into initialise_machine by refinement checker */
1171		current_state_id(CurID), CurID=root,
1172		transition(CurID,Action1,ID1),
1173		functor(Action1,'$setup_constants',_),
1174		transition(ID1,Action2,ID),
1175		functor(Action2,'$initialise_machine',_),!,
1176		tcltk_interface:tcltk_perform_action(Action1,ID1),
1177		tcltk_interface:tcltk_perform_action(Action2,ID),
1178		execute_string_trace_to_node(T).
1179		execute_string_trace_to_node([go('$initialise_machine',ID)|T]) :-
1180		current_state_id(root),
1181		transition(root,start_cspm_MAIN,ID),!,
1182		tcltk_interface:tcltk_perform_action(start_cspm_MAIN,ID),
1183		execute_string_trace_to_node(T).
1184		execute_string_trace_to_node([go('$setup_constants',ID)|T]) :-
1185		current_state_id(CurID),
1186		transition(CurID,Action,ID),
1187		functor(Action,'$setup_constants',_),!,
1188		tcltk_interface:tcltk_perform_action(Action,ID),
1189		execute_string_trace_to_node(T).
1190		execute_string_trace_to_node([go(tau,DestID)|T]) :- % could now be multiple taus ! adapt
1191		current_state_id(CurID),
1192		find_tau_trace_to(CurID,DestID,NewTrace,T),!,
1193		execute_string_trace_to_node(NewTrace).
1194		execute_string_trace_to_node([go(tau_direct,ID)|T]) :-
1195		current_state_id(CurID),
1196		tau_transition(CurID,Action,ID),!,
1197		tcltk_interface:tcltk_perform_action(Action,ID),
1198		execute_string_trace_to_node(T).
1199		execute_string_trace_to_node([go(Action,ID)|T]) :- /* <---- Node ID's have to be added to avoid problems !! */
1200		current_state_id(CurID),
1201		transition(CurID,Ev,TransitionId,ID),
1202		translate_event(Ev,Action),
1203		tcltk_interface:tcltk_perform_action(CurID,Ev,TransitionId,ID),
1204		!,
1205		execute_string_trace_to_node(T).
1206		execute_string_trace_to_node([go(Action,ID)|_T]) :- silent_mode(off),
1207		current_state_id(CurID),
1208		format('Could not replay event ~w (reaching state id ~w) in state ~w~n',[Action,ID,CurID]),
1209		debug_mode(on),
1210		portray_state(CurID),
1211		fail.
1212
1213		portray_state(CurID) :-
1214		current_expression(CurID,State),
1215		format('State ~w : ~w~n',[CurID,State]),
1216		transition(CurID,Ev,TransitionId,ID),
1217		translate_event(Ev,Action),
1218		format(' -- ~w : ~w --> ~w~n',[TransitionId,Action,ID]),
1219		fail.
1220		portray_state(CurID) :-
1221		not_all_transitions_added(CurID), write(' not_all_transitions_added'),nl,fail.
1222		portray_state(CurID) :-
1223		max_reached_or_timeout_for_node(CurID), write(' max_reached_or_timeout_for_node'),nl,fail.
1224		portray_state(_).
1225
1226		tau_priority_transition(CurID,Span,ID) :- impl_trans_term(CurID,tau(TAUINFO),ID), priority_tau(TAUINFO,Span).
1227		priority_tau(rep_int_choice(Span),rep_int_choice(Span)). % add wrapper in case Span is unknown
1228		%priority_tau(tick(S),tick(S)). % can also hide choices: tick was visible; resolves external choice
1229		priority_tau(int_choice_left(Span,_),int_choice(Span)). % TO DO: check span
1230		priority_tau(int_choice_right(Span,_),int_choice(Span)).
1231		% TO DO: hide if only taus possible; same with link parallel
1232		% TO DO: replace span by position insisde CSP expression (in case of multiple copies of same operator)
1233
1234		% first execute prioritized tau transitions from a source location if possible; otherwise any tau is ok
1235		%%%%%%%%%%% DEAD CODE %%%%%%%%%%%%
1236		/*
1237		prioritized_tau_trans(CurID,ID,prio) :- tau_priority_transition(CurID,Span,_),!,
1238		tau_priority_transition(CurID,Span,ID).
1239		prioritized_tau_trans(CurID,ID,all) :- tau_transition(CurID,_Action,ID).
1240		*/
1241
1242		tau_transition(CurID,Action,ID) :- impl_trans_term(CurID,Action,ID), functor(Action,tau,_).
1243
1244		% find a tau trace to a give id; id can also be 'divergence'; last arg is trace as difference list
1245		:- volatile tau_trace_visited/1.
1246		:- dynamic tau_trace_visited/1.
1247		find_tau_trace_to(CurID,DestID,Trace,TraceTail) :- retractall(tau_trace_visited(_)),
1248		find_tau_trace_to_aux(CurID,DestID,Trace,TraceTail).
1249
1250		find_tau_trace_to_aux(CurID,DestID,T,Tail) :-
1251		tau_trace_visited(CurID),!,DestID=divergence,T=Tail.
1252		find_tau_trace_to_aux(CurID,ID,T,Tail) :- ID=CurID,!,T=Tail.
1253		find_tau_trace_to_aux(CurID,ID,[go(tau_direct,ID2)|T],Tail) :- assertz(tau_trace_visited(CurID)),
1254		tau_transition(CurID,_,ID2),
1255		find_tau_trace_to_aux(ID2,ID,T,Tail).
1256
1257		/* ---------------------------------
1258		Printing gluing invariant is not used anywhere in the source code (DEAD CODE).
1259		--------------------------------- */
1260		/*
1261		:- public pgt/0.
1262
1263		pgt :- print_gluing_invariant.
1264		print_gluing_invariant :- print('GLUING INVARIANT'),nl,
1265		not_refines_table(X,Y,_),
1266		X \= root,
1267		X \= concrete_constants(_),
1268		print_state_as_expression(X),
1269		print(' => '),nl,
1270		print_states_as_disjunction(Y),nl,
1271		print(' & '),nl,
1272		fail.
1273		print_gluing_invariant :- print(' TRUE'),nl.
1274
1275		print_state_as_expression(ID) :-
1276		visited_expression(ID,State),
1277		print(' ('),
1278		print_bindings(State),
1279		print(') ').
1280		*/
1281		%print_spec_state_as_expression(ID) :-
1282		/* need to be able to access state of specification machine ! */
1283		% print('not yet implemented, ID:'), print(ID).
1284		/*
1285		print_states_as_disjunction([]) :- print(' FALSE'),nl.
1286		print_states_as_disjunction([S]) :- !, print_spec_state_as_expression(S).
1287		print_states_as_disjunction([S|T]) :- !, print_spec_state_as_expression(S),
1288		print(' or '), print_states_as_disjunction(T).
1289
1290		:- use_module(probsrc(translate)).
1291		print_bindings([]) :- print('TRUE').
1292		print_bindings([bind(Var,Val)]) :- !,
1293		translate_bvalue(Var,TV), print(TV),
1294		print('='),
1295		translate_bvalue(Val,TVal), print(TVal).
1296		print_bindings([bind(Var,Val)|T]) :-
1297		translate_bvalue(Var,TV), print(TV),
1298		print('='),
1299		translate_bvalue(Val,TVal), print(TVal),
1300		print_bindings(T).
1301		*/
1302
1303
1304		% -----------------------------------
1305
1306
1307		% TO DO: try use_module(library(mutdict)) from SICStus 4.7
1308
1309		:- dynamic outer_visited/2, inner_visited/2. % true if a node has been seen during inner dfs traversal for cycle detection
1310		reset_nfs :- retractall(outer_visited(_,_)), retractall(inner_visited(_,_)).
1311		assert_outer_visited(From,NBA) :- assertz(outer_visited(From,NBA)).
1312		assert_inner_visited(From,NBA) :- assertz(inner_visited(From,NBA)).
1313
1314
1315		% -----------------------------------
1316
1317		% use_module(extrasrc(refinement_checker)), refinement_checker:nested_dfs_cycle_check(Pre,X,Loop).
1318
1319		tcltk_nested_dfs_goal_cycle_check(Msg) :-
1320		nested_dfs_cycle_check(Prefix,State,Loop),!,
1321		length(Prefix,LP), length(Loop,LL),
1322		ajoin(['GOAL predicate can be satisfied infinitely often, reached state with id ',State,
1323		' after ',LP, ' transitions and loop with ',LL,' transitions.'],Msg).
1324		tcltk_nested_dfs_goal_cycle_check('GOAL predicate cannot be satisfied infinitely often.').
1325
1326
1327		:- use_module(probsrc(tools),[start_ms_timer/1, stop_ms_timer_with_msg/2, minimize_lasso/4]).
1328
1329		% look for a cycle where infinitely often GOAL holds
1330		nested_dfs_cycle_check(Prefix,State,Loop) :-
1331		reset_nfs,
1332		start_ms_timer(T1),
1333		initial_nba_state(NBAInit),
1334		(reachable_cycle(root,NBAInit,Prefix,State,Loop)
1335		->
1336		stop_ms_timer_with_msg(T1,'Nested-DFS found cycle'),
1337		print_state_from_id(State), print(' satisfies GOAL and can be executed infinitely often '),nl,
1338		printsilent('Path to state: '),printsilent(Prefix),nls,
1339		printsilent('Loop: '),printsilent(Loop),nls,
1340		(minimize_lasso(Prefix,Loop,NP,NL), append(NP,NL,Trace),
1341		set_counterexample_by_transition_ids(Trace)
1342		-> true ; add_error(nested_dfs_cycle_check,'Could not set counter example:',Prefix))
1343		;
1344		stop_ms_timer_with_msg(T1,'Nested-DFS found no cycle'),
1345		format('No infinite loop with state statisfying GOAL found~n',[]),fail
1346		).
1347
1348
1349		:- use_module(probsrc(state_space),[impl_trans_id/4, set_counterexample_by_transition_ids/1]).
1350
1351		% Implementation of Algorithm 8 from Modelchecking Book
1352
1353		reachable_cycle(From,NBA,_,_,_) :- outer_visited(From,NBA),!,fail.
1354		reachable_cycle(From,NBA,[Action1|T],State,Loop) :- assert_outer_visited(From,NBA),
1355		% format('Processing edges for ~w~n',[From]),
1356		b_nba_transition(From,NBA,Action1,To1,NBA1),
1357		reachable_cycle(To1,NBA1,T,State,Loop).
1358		reachable_cycle(From,NBA,[],From,Loop) :-
1359		accepting_state(NBA,From),
1360		% we now look for a cycle back to From
1361		Loop = [_|_],
1362		%format('Finished processing edges for ~w, GOAL satisfied, looking for cycle.~n',[From]),
1363		cycle_check(From,NBA,Loop,From,NBA).
1364
1365		cycle_check(From,NBA,[],From,NBA) :- !. % Loop found
1366		cycle_check(From,NBA,_,_,_) :- inner_visited(From,NBA),!,fail. % already explored
1367		cycle_check(From,NBA,[ActionID|TLoop],TargetB,TargetNBA) :- assert_inner_visited(From,NBA),
1368		% format('Looking for cycle from ~w to target ~w : ~w~n',[From,TargetB,TargetNBA]),
1369		b_nba_transition(From,NBA,ActionID,ToB,ToNBA),
1370		cycle_check(ToB,ToNBA,TLoop,TargetB,TargetNBA).
1371
1372		b_nba_transition(FromB,FromNBA,ActionID,ToB,ToNBA) :-
1373		impl_trans_id(FromB,Term1,ActionID,ToB),
1374		nba_trans(FromNBA,Term1,ToB,ToNBA).
1375
1376
1377		% NBA: Non-Deterministic Büchi Automata
1378
1379		% TODO: make dynamic and flexible
1380
1381		:- use_module(probsrc(model_checker),[node_satisfies_goal/1]).
1382		initial_nba_state(1).
1383		nba_trans(1,_,_,1). % :- print(A),nl.
1384		accepting_state(_,From) :- node_satisfies_goal(From). % look for GF GOAL
1385
1386		%nba_trans(1,_,To,Dest) :- (node_satisfies_goal(To) -> Dest=2 ; Dest=1).
1387		%nba_trans(2,_,_,2).
1388		%accepting_state(2,_). % look for F GOAL
1389
1390		% example NBA for Mutex.mch
1391		%nba_trans(1,'RequestCS'(int(1)),R) :- !, R=2.
1392		%nba_trans(1,_,_,1).
1393		%nba_trans(2,'EnterCS'(int(1)),_,R) :- !, fail.
1394		%nba_trans(2,_,_,2).
1395		%accepting_state(2,_).
1396		% one could also use a CSP || B process;
1397		% but: CSP||B: cannot store B states independently (w/o CSP) because CSP process prunes and sets parameters