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 | */ |