1		% (c) 2009-2024 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(ctl,[ctl_model_check/4, ctl_model_check_with_ce/6, ctl_model_check_with_ast/6, tcltk_play_ctl_counterexample/2]).
6
7		/* SICSTUS Libraries */
8		:- use_module(library(avl)).
9
10		/* ProB Libraries */
11		:- use_module(probsrc(error_manager)).
12		:- use_module(probsrc(state_space), [set_max_nr_of_new_impl_trans_nodes/1,
13		current_state_id/1, not_all_transitions_added/1,
14		transition/4]).
15		:- use_module(probsrc(tools),[print_size_of_table/1]).
16		:- use_module(probsrc(tools_printing), [print_error/1]).
17		:- use_module(probsrc(debug)).
18
19		:- use_module(probltlsrc(ltl)).
20		:- use_module(probltlsrc(ltl_propositions), [trans/3, check_transition/4, check_ap/2]).
21
22		:- use_module(probsrc(module_information),[module_info/2]).
23		:- module_info(group,ltl).
24		:- module_info(description,'This module provides CTL model checking on models.').
25
26		:- meta_predicate printtime(0).
27
28		/* CTL Model Checker */
29
30		/* sample formula: ef(e(b(stop_Moat/0))) */
31
32		sat(true,_E,T,R) :- !, T=[], R=true.
33		sat(false,_E,T,R) :- !, T=[], R=false.
34		sat(not(F),E,T,Res) :- !, sat(F,E,T,Res1), negate_result(Res1,Res).
35		sat(ap(P),E,[],Res) :- !, (check_ap(P,E) -> Res=true ; Res=false). /* elementary atomic proposition */
36		sat(action(OpSpec),E,T,Res) :- !, /* transition proposition */
37		(trans(E,E2,Act),
38		check_transition(OpSpec,Act,E,E2)
39		-> Res=true, T=[E2]
40		; Res=false, T=[]).
41		sat(and(F,G),E,T,Res) :- !,
42		sat(F,E,T1,Res1),
43		(Res1=false -> Res=false,T=T1
44		; sat(G,E,T,Res)).
45		sat(or(F,G),E,T,Res) :- !,
46		sat(F,E,T1,Res1), %print(sat_or1(F,E,T1,Res1)),nl,
47		(Res1=true -> Res=true,T=T1
48		; sat(G,E,T,Res) %, print(sat_or2(G,E,T,Res)),nl
49		).
50		sat(implies(A,B),E,T,Res) :- !, sat( or(not(A),B),E,T,Res).
51		sat(equivalent(A,B),E,T,Res) :- !, sat( and(implies(A,B),implies(B,A)),E,T,Res).
52		sat(an(F),E,T,Res) :- !, sat(not(en(not(F))),E,T,Res).
53		sat(en(F),E,T,Res) :- !, /* exists next */
54		(trans(E,E2,_),
55		sat(F,E2,T2,true)
56		-> Res=true, T=[E2|T2]
57		; Res=false, T=[]).
58		sat(action(OpSpec,F),E,T,Res) :- !, /* exists next with predicate on transition; ena renamed to action by preprocess_formula2 */
59		(trans(E,E2,Act),
60		check_transition(OpSpec,Act,E,E2),sat(F,E2,T2,true)
61		-> Res=true, T=[E2|T2]
62		; Res=false, T=[]).
63		sat(eu(F,G),E,T,Res) :- !, /* exists until */
64		sat_eu(E,F,G,T,Res).
65		sat(ef(F),E,T,Res) :- !, /* exists future */
66		sat(eu(true,F),E,T,Res).
67		sat(ag(F),E,T,Res) :- !, sat(not(ef(not(F))),E,T,Res).
68		sat(af(F),E,T,Res) :- !, sat(not(eg(not(F))),E,T,Res).
69		sat(eg(F),E,T,Res) :- !, sat_eg(E,F,T,Res).
70		sat(X,State,T,R) :- add_internal_error('Uncovered CTL Formula: ',sat(X,State,T,R)),fail.
71
72		negate_result(true,false).
73		negate_result(false,true).
74		negate_result(incomplete,incomplete).
75
76		:- dynamic sat_eg_table/3.
77		% TO DO: also use Ids generated by formula_to_id to store in sat_eg_table
78		% TO DO: try and use mutarry or mutdict from SICStus 4.7
79		sat_eg(E,F,[],R) :-
80		sat_eg_table(E,F,Res),!,
81		R=Res. % loop found
82		sat_eg(E,F,[],R) :- sat(F,E,_T,false),!,
83		assertz(sat_eg_table(E,F,false)),
84		R=false.
85		sat_eg(E,F,[E2|T],R) :- %print(true(E,F)),nl,
86		assertz(sat_eg_table(E,F,true)),
87		trans(E,E2,_Act),
88		(\+ (trans(E,E3,_), E2 \= E3) % deterministic transition: extend counter example; no need to backtrack
89		-> %!, % this cut causes to recognise already visited states as the begining of a loop
90		% since it skips the retracting-clause of sat_eg
91		sat_eg(E2,F,T,R)
92		; sat_eg(E2,F,T,true),!,R=true
93		).
94		sat_eg(E,F,T,R) :- retract(sat_eg_table(E,F,_)),assertz(sat_eg_table(E,F,false)),
95		T=[],R=false.
96
97
98		reset_ctl :-
99		retractall(sat_eg_table(_,_,_)),
100		retractall(sat_eu_table(_,_,_,_,_)),
101		retractall(formula_registry(_,_)),
102		retractall(next_id(_)),
103		assertz(next_id(0)).
104
105		% to minimize storage used for sat_eu_table and speedup lookup: we store formulas/subformulas with ids
106		% TO DO: sat_eu_table : store formula ids using term_hash
107		:- dynamic formula_registry/2, next_id/1.
108		next_id(0).
109
110		formula_to_id(Formula,Id) :- formula_registry(Formula,R),!,R=Id.
111		formula_to_id(Formula,Id) :- retract(next_id(R)),
112		R1 is R+1, assertz(next_id(R1)),
113		assertz(formula_registry(Formula,R)),
114		Id = R.
115
116
117		:- dynamic sat_eu_table/5.
118		sat_eu(E,F,G,T,R) :- formula_to_id(F,Fid), formula_to_id(G,Gid),
119		sat_eu1(E,F,Fid,G,Gid,T,R).
120		sat_eu1(E,F,Fid,G,Gid,T,R) :-
121		empty_avl(Computing), %print(start_eu(E,F,G,T,R)),nl,
122		sat_eu2(E,F,Fid,G,Gid,Computing,OutComputing,T,Res), % print(res(Res)),nl,
123		( Res = computing ->
124		% we found only false and computing (i.e. cycles) nodes,
125		% there is no true node to encounter
126		assertz(sat_eu_table(E,Fid,Gid,[],false)),
127		% we know that all visited nodes must be false, too
128		mark_all_computing_nodes_as_false(Fid,Gid,OutComputing),
129		R=false
130		;
131		R = Res).
132		% sat_eu2/9 is used recursively to find a reachable node where G is true
133		% A set of elements that have already been checked is passed (InComputing and
134		% OutComputing)
135		sat_eu2(E,_F,_,_G,_,InComputing,OutComputing,T,R) :-
136		% the node has already been checked, Result is "computing"
137		avl_fetch(E,InComputing),!,R=computing,T=[],OutComputing = InComputing.
138		sat_eu2(E,_F,Fid,_G,Gid,InComputing,OutComputing,T,R) :-
139		% the value for this node has already been computed
140		sat_eu_table(E,Fid,Gid,TT,Res),!, %print(sat_eu_table(E,F,G,TT,Res)),nl,
141		R=Res,T=TT,OutComputing=InComputing.
142		sat_eu2(E,_F,Fid,G,Gid,InComputing,OutComputing,T,Res) :- % print(sat_eu_eval(E,F,G)),nl,
143		% the goal is true in this node
144		Res=true,
145		/* exists until */
146		sat(G,E,T,true),!,
147		% print(set_eu_g_true(G,T)),nl,
148		assertz(sat_eu_table(E,Fid,Gid,T,true)),
149		%% assertz(sat_eu_table(E,Fid,Gid,[],true)),
150		InComputing = OutComputing.
151		sat_eu2(E,F,Fid,G,Gid,InComputing,OutComputing,T,Res) :- /* exists until */
152		% the goal is not true
153		% sat(not(G),E,_), /* added to avoid extra answers */
154		sat(F,E,T1,Res1),
155		% print(sat_eu_loop(E,F,T1,Res1)),nl,
156		(
157		Res1=true ->
158		avl_store(E,InComputing,true,Computing),
159		sat_eu_step(E,F,Fid,G,Gid,Computing,OutComputing,T2,Res2),
160		( Res2 = true ->
161		% we found a node with the goal, mark this as true
162		assertz(sat_eu_table(E,Fid,Gid,T2,true)), %% < ------------- T2
163		Res=true, T=T2
164		; Res2 = computing ->
165		Res=computing, T=[]
166		;
167		% we found only false or incomplete nodes, mark this as false / incomplete
168		assertz(sat_eu_table(E,Fid,Gid,[],Res2)),
169		Res=Res2, T=[]
170		)
171		; /* Res1 = false or incomplete */
172		% if F is false the result is false anyhow - we do not have to look into the future
173		assertz(sat_eu_table(E,Fid,Gid,[],Res1)),
174		Res=Res1, T=T1, OutComputing=InComputing
175		).
176		sat_eu_step(E,F,Fid,G,Gid,InComputing,OutComputing,T,R) :-
177		findall(N,trans(E,N,_),Nexts), % Nexts can be [] when max_nr_of_new_nodes reached; TO DO: catch error occuring in decrease_max_nr_of_new_nodes and set Result to incomplete
178		(Nexts = [], not_all_transitions_added(E) -> InResult=incomplete ; InResult = false),
179		sat_eu_step2(Nexts,F,Fid,G,Gid,InComputing,OutComputing,T,InResult,R).
180		sat_eu_step2([],_F,_,_G,_,InComputing,OutComputing,T,In,Out) :- !,In=Out,T=[],InComputing=OutComputing.
181		sat_eu_step2([Next|Nrest],F,Fid,G,Gid,InComputing,OutComputing,T,In,R) :-
182		sat_eu2(Next,F,Fid,G,Gid,InComputing,Computing,_T2,Res),
183		( Res=true -> R=true, T=eu(Fid,Gid,Next), % --> we now store link to next node and not full trace: T=[Next|T2],
184		OutComputing=Computing
185		;
186		combine_result(In,Res,New),
187		sat_eu_step2(Nrest,F,Fid,G,Gid,Computing,OutComputing,T,New,R)).
188		combine_result(false,false,R) :- !,R=false.
189		combine_result(incomplete,_,R) :- !,R=incomplete.
190		combine_result(_,incomplete,R) :- !,R=incomplete.
191		combine_result(_,_,computing).
192
193		expand_trace([],R) :- !, R=[].
194		expand_trace([H|T],[H|ET]) :- !, expand_trace(T,ET).
195		expand_trace(eu(Fid,Gid,Next),[Next|ET]) :- !,
196		sat_eu_table(Next,Fid,Gid,T,_),
197		expand_trace(T,ET).
198		expand_trace(T,R) :- add_internal_error('Unknown trace: ',expand_trace(T,R)), T=R.
199
200		mark_all_computing_nodes_as_false(Fid,Gid,Computing) :-
201		avl_member(E,Computing),
202		assertz(sat_eu_table(E,Fid,Gid,[],false)),
203		fail.
204		mark_all_computing_nodes_as_false(_F,_G,_Computing).
205
206
207		% check CTL formula for all initial States (or for a single given start state)
208		% (Note: a model/transition system satisfies a CTL formula iff the formula holds in all initial states.)
209		ctl_sat_for_all(Formula,States,Trace,Res) :-
210		length(States,Len),
211		(Len>1 -> formatsilent('Checking CTL formula for ~w initial states~n',[Len]) ; true),
212		% one can also use Mode=specific_node(NodeID), but then Len=1
213		ctl_sat_for_all2(States,Formula,[],unknown,Trace1,Res1),
214		(Res1 = unknown -> Res=true, Trace=[] ; Res=Res1, Trace=Trace1).
215		ctl_sat_for_all2([],_Formula,Trace,Res,Trace,Res).
216		ctl_sat_for_all2([State|Srest],Formula,PrevTrace,PrevRes,Trace,Res) :-
217		sat(Formula,State,Trace1,Res1),
218		debug_format(19,'CTL result for state ~w: ~w~n',[State,Res1]),
219		NewTrace = [State|Trace1],
220		( Res1=false ->
221		% Counter-example found, use it and stop
222		Res=false, Trace=NewTrace
223		; Res1=incomplete ->
224		Res=incomplete, Trace=NewTrace
225		; PrevRes=unknown ->
226		% First witness found, store and continue
227		ctl_sat_for_all2(Srest,Formula,NewTrace,true,Trace,Res)
228		;
229		% Another witness found, ignore it and use the old
230		ctl_sat_for_all2(Srest,Formula,PrevTrace,true,Trace,Res)).
231
232
233		:- use_module(probsrc(tools),[retract_with_statistics/2]).
234		ctl_model_check2(Formula,Mode,InitStates,Res) :-
235		reset_ctl,
236		debug_println(4,ctl_preprocessing),
237		ltl: preprocess_formula(Formula,PFormula),
238		debug:debug_println(5,starting_ctl_model_check(PFormula,Mode,InitStates)),
239		( printtime(ctl_sat_for_all(PFormula,InitStates,Trace,Res)),
240		debug_format(9,'CTL internal trace: ~w~n',[Trace]),
241		Trace = [Initstate|_] ->
242		( Mode=init -> ltl: set_trace_to_init(Initstate) % we need to go to the initialised state
243		% before the counterexample itself is shown
244		; Mode = specific_node(NodeID) -> ltl: set_trace_to_init(NodeID)
245		; true),
246		expand_trace(Trace,ETrace), %debug_println(4,expanded(ETrace)),
247		print_trace(Res,ETrace),
248		ltl: executetrace(ETrace),
249		(debug_mode(off)
250		-> reset_ctl
251		; reset_ctl_with_stats
252		)
253		%,(formula_registry(F,Id),format('Formula ~w = ~w~n',[Id,F]),fail ; true)
254		%, nl, findall(T,sat_eu_table(_,_,_,T,_),Ts), lists:max_member(Mx,Ts), print(max_trace_length(Mx)),nl
255		%, (sat_eu_table(E,Fid,Gid,T2,R), print(sat_eu_table(E,Fid,Gid,T2,R)),nl,fail ; true)
256		;
257		add_internal_error('CTL model check failed: ',PFormula),
258		print_size_of_table(ctl: sat_eu_table/5),fail
259		).
260
261		reset_ctl_with_stats :-
262		print_size_of_table(ctl: sat_eg_table/3),
263		print_size_of_table(ctl: sat_eu_table/5),
264		print_size_of_table(ctl: formula_registry/2),
265		retract_with_statistics(ctl,[sat_eg_table(_,_,_),sat_eu_table(_,_,_,_,_)]).
266
267		print_trace(_,_) :- silent_mode(on),!.
268		print_trace(Res,Trace) :-
269		(length(Trace,Len) -> true ; Len=0),
270		( Res = true -> format('CTL Witness of length ~w found~n',[Len])
271		; Res = false -> format('CTL counterexample of length ~w found~n',[Len])
272		; format('Could not decide CTL property, checking result: ~w~n',[Res])
273		),
274		(debug_mode(on) -> format('Trace: ~w~n',[Trace]) ; true).
275
276		:- use_module(ltl_tools,[temporal_parser/3]).
277
278		ctl_model_check(Formula,MaxNodes,Mode,Res) :-
279		(temporal_parser(Formula,ctl,Ctl) -> true ; add_error(ctl,'CTL Parser failed: ',Formula),fail),
280		set_max_nr_of_new_impl_trans_nodes(MaxNodes),
281		select_ctl_mode(Mode,Ctl,Startnodes,Ctl2),
282		ctl_model_check2(Ctl2,Mode,Startnodes,Res).
283
284		:- use_module(probsrc(state_space),[find_initialised_states/1]).
285
286		select_ctl_mode(starthere,Ctl,[Startnode],Ctl) :-
287		!, current_state_id(Startnode),
288		debug_format(19,'Checking CTL formula from current state: ~w~n',[Startnode]).
289		select_ctl_mode(init,Ctl,Startnodes,Ctl) :-
290		!, find_initialised_states(Startnodes),
291		debug_format(19,'Checking CTL formula from all initial states: ~w~n',[Startnodes]).
292		select_ctl_mode(specific_node(Startnode),Ctl,[Startnode],Ctl) :-
293		!,
294		debug_format(19,'Checking CTL formula from specific state: ~w~n',[Startnode]).
295		select_ctl_mode(Mode,Ctl,[],Ctl) :-
296		add_error(ltl,'Internal error: Unexpected mode', Mode),
297		fail.
298
299		/* --------------------------- */
300
301		:- use_module(probsrc(debug),[formatsilent/2]).
302		printtime(C) :-
303		statistics(runtime,[Start|_]), statistics(walltime,[StartW|_]),
304		(call(C) -> Res=ok ; Res=failure),
305		statistics(runtime,[End|_]), statistics(walltime,[EndW|_]),
306		T is End - Start, TW is EndW - StartW,
307		formatsilent('CTL check took ~3d seconds walltime (~3d seconds runtime) ~n', [TW,T]),
308		Res=ok.
309
310		:- public parse_and_pp_ctl_formula/2.
311		parse_and_pp_ctl_formula(FormulaAsAtom,Text) :-
312		temporal_parser(FormulaAsAtom,ctl,Ctl),
313		( ltl: pp_ltl_formula(Ctl,Text)
314		-> true
315		; add_error_fail(ctl, 'Failed to pretty print CTL formula: ', Ctl)
316		).
317
318		%%%%%%%%%%%%%%%%%%%% Used for the CSP-M Assertions Viewer %%%%%%%%%%%%%%%%%%%%%%
319		:- dynamic ctl_counter_examples_cache/4.
320
321		:- use_module(probsrc(user_interrupts),[catch_interrupt_assertion_call/1]).
322		:- use_module(extension('user_signal/user_signal'), [user_interruptable_call_det/2]).
323		interruptable_ctl_model_check_with_ce2(Proc,Formula,Mode,InitStates,Res,CE) :-
324		user_interruptable_call_det(catch_interrupt_assertion_call(ctl: ctl_model_check_with_ce2(Proc,Formula,Mode,InitStates,Res,CE)),InterruptResult),
325		(InterruptResult=interrupted ->
326		Res=interrupted
327		; real_error_occurred ->
328		print_error('% *** Errors occurred while CTL model checking ! ***'),nl,nl,fail
329		; formatsilent('CTL assertion check completed.~n',[])
330		).
331
332		:- public ctl_model_check_with_ce2/6.
333		ctl_model_check_with_ce2(Proc,Formula,Mode,InitStates,Res,CE) :-
334		reset_ctl,
335		ltl: preprocess_formula(Formula,PFormula),
336		( printtime(ctl_sat_for_all(PFormula,InitStates,Trace,Res)) ->
337		( Res = true -> CE=none, printsilent('Witness found: '),nls
338		; Res = false -> print('CTL counterexample found: '),nl, convert_ctl_trace(Proc,PFormula,Mode,false,Trace,CE)
339		; CE=unexpected_result, print('Could not decide property: '), print(Res), print(': '),nl),
340		(debug_mode(on) -> print(Trace),nl ; true),
341		(silent_mode(on) -> reset_ctl
342		; reset_ctl_with_stats
343		)
344		;
345		add_internal_error('CTL model check failed: ',PFormula),
346		print_size_of_table(ctl: sat_eu_table/5),fail
347		),nl.
348
349		%%%%%%%%%%%%%%%%%%%% Used by ProB2 Interface %%%%%%%%%%%%%%%%%%%%%%
350		interruptable_ctl_model_check_with_ce3(Proc,Formula,Mode,InitStates,Res,CE) :-
351		user_interruptable_call_det(catch_interrupt_assertion_call(ctl: ctl_model_check_with_ce3(Proc,Formula,Mode,InitStates,Res,CE)),InterruptResult),
352		(InterruptResult=interrupted ->
353		Res=interrupted
354		; real_error_occurred ->
355		print_error('% *** Errors occurred while CTL model checking ! ***'),nl,nl,fail
356		; formatsilent('CTL assertion check completed.~n',[])
357		).
358
359		:- public ctl_model_check_with_ce3/6.
360		ctl_model_check_with_ce3(Proc,Formula,Mode,InitStates,Res,CE) :-
361		reset_ctl,
362		ltl: preprocess_formula(Formula,PFormula),
363		( printtime(ctl_sat_for_all(PFormula,InitStates,Trace,Res)) ->
364		( Res = true -> CE=none, printsilent('Witness found: '),nls
365		; Res = false -> format('CTL counterexample found (~w)~n',[Mode]),
366		convert_ctl_trace(Proc,PFormula,Mode,true,Trace,CE)
367		; CE=unexpected_result, print('Could not decide property: '), print(Res), print(': '),nl),
368		(debug_mode(on) -> print(Trace),nl ; true),
369		%expand_trace(Trace,ETrace), print(expanded(ETrace)),nl,
370		(silent_mode(on) -> reset_ctl
371		; reset_ctl_with_stats
372		)
373		;
374		add_internal_error('CTL model check failed: ',PFormula),
375		print_size_of_table(ctl: sat_eu_table/5),fail
376		),nl.
377
378
379
380		:- use_module(probsrc(eventhandling),[register_event_listener/3]).
381		:- register_event_listener(reset_specification,reset_ctl_ce_cache,
382		'Reset CTL Counterexamples Cache.').
383		:- register_event_listener(reset_prob,reset_ctl_ce_cache,
384		'Reset CTL Counterexamples Cache.').
385
386		reset_ctl_ce_cache :-
387		retractall(ctl_counter_examples_cache(_,_,_,_)).
388
389		% TODO: for returning action traces of CTL counter-examples more
390		% information is needed for determinig the entry loop
391		convert_ctl_trace(Proc,Ctl,Mode,UseTransitionIDs,Trace,CE) :-
392		expand_trace(Trace,Result),
393		%% convert_ctl_trace1(ETrace,Result),
394		(ctl_counter_examples_cache(Proc,Ctl,Mode,_) -> true; assertz(ctl_counter_examples_cache(Proc,Ctl,Mode,Result))),
395		(UseTransitionIDs = true -> get_event_trace_transitions(Mode,Result,EventTrace)
396		; get_event_trace(Result,EventTrace)),
397		CE=ce(EventTrace).
398
399		get_event_trace(Trace,ETrace) :-
400		get_event_trace1(Trace,Res),
401		tools: ajoin_with_sep(Res,' -> ',ETrace).
402
403		:- use_module(probsrc(translate),[translate_event/2]).
404		get_event_trace1([],['']).
405		get_event_trace1([_NodeID],['']).
406		get_event_trace1([Src,Dest|Rest], [Event|Res]) :-
407		transition(Src,Op,_OpId,Dest),
408		translate_event(Op,Event),
409		get_event_trace1([Dest|Rest],Res).
410
411		:- use_module(probsrc(specfile),[get_operation_name/2]).
412		% for ProB2-UI
413		% TODO: the counter example is just a list of state ids, not the transition ids
414		% for some counter examples it could be useful to actually enforce the right transitions to be used EX with action,...
415		get_event_trace_transitions(init,[StartNode|T],CE) :-
416		(transition(root,_,_,StartNode) ->
417		get_event_trace_transitions2([root,StartNode|T],CE)
418		; transition(root,_,_,N1), transition(N1,_,_,StartNode) -> % setup constants first
419		get_event_trace_transitions2([root,N1,StartNode|T],CE)
420		;
421		get_event_trace_transitions2([root,StartNode|T],CE)).
422		get_event_trace_transitions(specific_node(Start),Trace,CE) :- % do we need a trace from root to Start ?
423		get_event_trace_transitions2([Start|Trace],CE).
424		get_event_trace_transitions2([], Res) :- !, Res=[].
425		get_event_trace_transitions2([_NodeID],Res) :- !, Res=[].
426		get_event_trace_transitions2([Src,Dest|Rest], [transition(OpId,OpName,Src,Dest)|Res]) :-
427		transition(Src,Op,OpId,Dest),!,
428		get_operation_name(Op,OpName),
429		get_event_trace_transitions2([Dest|Rest],Res).
430		get_event_trace_transitions2([Src,Dest|_],[]) :-
431		add_error(ctl_model_check,'Cannot replay counter example, no transition for:',(Src,Dest)).
432
433
434		tcltk_play_ctl_counterexample(Proc,Ctl) :-
435		ctl_counter_examples_cache(Proc,Ctl,Mode,ETrace),
436		ETrace = [Initstate|_],
437		( Mode=init -> ltl: set_trace_to_init(Initstate)
438		; Mode = specific_node(NodeID) -> ltl: set_trace_to_init(NodeID)
439		; true),
440		ltl: executetrace(ETrace).
441		tcltk_play_ctl_counterexample(Proc,Ctl) :-
442		add_error_fail(ctl_counter_example, 'Internal error: No counterexample has been asserted for the following configuration: ',(Proc,Ctl)).
443
444		ctl_model_check_with_ce(Proc,Formula,MaxNodes,Mode,Res,CE) :-
445		(temporal_parser(Formula,ctl,Ctl) -> true ; add_error_fail(ctl,'CTL Parser failed: ',Formula)),
446		set_max_nr_of_new_impl_trans_nodes(MaxNodes),
447		select_ctl_mode(Mode,Ctl,Startnodes,Ctl2),
448		interruptable_ctl_model_check_with_ce2(Proc,Ctl2,Mode,Startnodes,Res,CE).
449
450
451		%%%%%%%%%%%%%%%%%%%% Used by ProB2 Interface %%%%%%%%%%%%%%%%%%%%%%
452		ctl_model_check_with_ast(Proc,Ctl,MaxNodes,Mode,Res,CE) :-
453		set_max_nr_of_new_impl_trans_nodes(MaxNodes),
454		select_ctl_mode(Mode,Ctl,Startnodes,Ctl2),
455		interruptable_ctl_model_check_with_ce3(Proc,Ctl2,Mode,Startnodes,Res,CE).