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