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