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