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