| 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/4, check_transition_pred/5, 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,TransId), | |
| 38 | check_transition_pred(OpSpec,Act,E,TransId,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,TransId), | |
| 61 | check_transition_pred(OpSpec,Act,E,TransId,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). |