| 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 | % LTL model checking | |
| 6 | ||
| 7 | :- module(ltl,[ltl_model_check/4,ltl_model_check2/4, | |
| 8 | ltl_model_check_ast/4, | |
| 9 | ltl_check_assertions/2, parse_ltlfile/2, | |
| 10 | ltl_model_check_with_ce/4, ltl_model_check_with_ce1/5, | |
| 11 | parse_and_pp_ltl_formula/2, % imported from ltl_tools.pl | |
| 12 | ltl_formula_structure/3, | |
| 13 | pp_ltl_formula/2, | |
| 14 | counterexample_node/1, counterexample_op/1, | |
| 15 | preprocess_formula/2, | |
| 16 | extract_formulas/4, | |
| 17 | %% reset_ltl/0, | |
| 18 | find_atomic_property_formula/2, | |
| 19 | init_states/1, | |
| 20 | executetrace/1,set_trace_to_init/1, | |
| 21 | parse_and_preprocess_formula/3, | |
| 22 | is_fairness_implication/1, | |
| 23 | tcltk_play_ltl_counterexample/2 | |
| 24 | ]). | |
| 25 | ||
| 26 | /* SICSTUS libraries */ | |
| 27 | :- use_module(library(lists)). | |
| 28 | :- use_module(library(ordsets)). | |
| 29 | ||
| 30 | /* ProB standard libraries */ | |
| 31 | % B | |
| 32 | :- use_module(probsrc(bsyntaxtree), [get_texpr_expr/2,get_texpr_pos/2,predicate_identifiers/2]). | |
| 33 | :- use_module(probsrc(bmachine),[ | |
| 34 | b_definition_prefixed/4, b_get_typed_definition/3, b_top_level_operation/1]). | |
| 35 | % CSP | |
| 36 | :- use_module(probcspsrc(haskell_csp),[filter_formulas_from_pragmas/3]). | |
| 37 | % utility modules | |
| 38 | :- use_module(probsrc(tools)). | |
| 39 | :- use_module(probsrc(translate)). | |
| 40 | :- use_module(probsrc(debug)). | |
| 41 | :- use_module(probsrc(error_manager)). | |
| 42 | :- use_module(probsrc(tools_printing), [print_error/1]). | |
| 43 | :- use_module(probsrc(preferences),[get_preference/2]). | |
| 44 | % state space relevant modules | |
| 45 | :- use_module(probsrc(specfile),[animation_mode/1]). | |
| 46 | :- use_module(probsrc(state_space),[set_max_nr_of_new_impl_trans_nodes/1, impl_trans_term/3, | |
| 47 | current_state_id/1,visited_expression/2, visited_expression_id/1, | |
| 48 | transition/4, | |
| 49 | %retract_visited_expression/2, % used for test cases | |
| 50 | impl_trans_term_all/2,state_space_reset/0, | |
| 51 | execute_id_trace_from_current/3, set_context_state/1, | |
| 52 | state_space_initialise/0, | |
| 53 | %compute_transitions_if_necessary_saved/1, % NOT EXPORTED | |
| 54 | not_all_transitions_added/1]). | |
| 55 | :- use_module(probsrc(state_space_exploration_modes),[depth_breadth_first_mode/1,set_depth_breadth_first_mode/1]). | |
| 56 | % Optimisations (POR and PGE) | |
| 57 | :- use_module(probporsrc(ample_sets),[stutter_action/1, visible_action/1,check_cycle_proviso/0,reset_runtime_dynamic_predicates_POR/0]). | |
| 58 | :- use_module(probporsrc(static_analysis),[compute_dependendency_relation_of_all_events_in_the_model/3]). | |
| 59 | :- use_module(probpgesrc(pge_algo), [is_pge_opt_on/0]). | |
| 60 | % static analyses | |
| 61 | :- use_module(probsrc(b_read_write_info),[b_get_read_write/3,b_get_operation_read_guard_vars/3]). | |
| 62 | ||
| 63 | ||
| 64 | /* ProB LTL modules */ | |
| 65 | :- use_module(probltlsrc(ltl_fairness)). | |
| 66 | :- use_module(probltlsrc(ltl_verification)). | |
| 67 | :- use_module(probltlsrc(ltl_safety)). | |
| 68 | :- use_module(probltlsrc(ltl_tools)). | |
| 69 | :- use_module(probltlsrc(ltl_translate)). | |
| 70 | :- use_module(probltlsrc(ltl_propositions)). | |
| 71 | :- use_module(probltlsrc(state_space_explorer)). | |
| 72 | ||
| 73 | :- use_module(probsrc(module_information),[module_info/2]). | |
| 74 | :- module_info(group,ltl). | |
| 75 | :- module_info(description,'This module provides LTL model checking on models.'). | |
| 76 | ||
| 77 | /* LTL relevant PL modules */ | |
| 78 | % import the low-level C-library wrapper | |
| 79 | :- use_module(extension('ltlc/ltlc')). | |
| 80 | ||
| 81 | parse_and_preprocess_formula(FormulaAsAtom,Type,Result) :- | |
| 82 | temporal_parser(FormulaAsAtom,Type,ParseResult), | |
| 83 | preprocess_formula(ParseResult,Result). | |
| 84 | ||
| 85 | % a utility to find a node satisfying a restricted atomic LTL property | |
| 86 | find_atomic_property_formula(AtomFormula,NodeID) :- | |
| 87 | parse_and_preprocess_formula(AtomFormula,ltl,PF), | |
| 88 | visited_expression_id(NodeID), | |
| 89 | check_atomic_property_formula(PF,NodeID). | |
| 90 | ||
| 91 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 92 | % get LTL formulas from 'DEFINITIONS' for B machines and | |
| 93 | % from pragmas ({-# ... #-}) for CSP-M specifications | |
| 94 | :- dynamic ltl_formula_cache/2. | |
| 95 | ||
| 96 | get_ltl_formulas(Names,Strings,Formulas) :- | |
| 97 | (animation_mode(b) | |
| 98 | -> get_ltl_formula_strings(Names,Strings) | |
| 99 | ; animation_mode(cspm) | |
| 100 | -> filter_formulas_from_pragmas(ltl,Names,Strings) | |
| 101 | ; animation_mode(csp_and_b) | |
| 102 | -> get_ltl_formula_strings(BNames,BStrings), | |
| 103 | filter_formulas_from_pragmas(ltl,CSPNames,CSPStrings), | |
| 104 | append(BNames,CSPNames,Names), | |
| 105 | append(BStrings,CSPStrings,Strings) | |
| 106 | ), | |
| 107 | (ltl_formula_cache(Strings,Formulas) -> true | |
| 108 | ; otherwise -> | |
| 109 | retractall(ltl_formula_cache(_,_)), | |
| 110 | temporal_parser_l(Strings,ltl,Formulas), | |
| 111 | assert(ltl_formula_cache(Strings,Formulas))). | |
| 112 | ||
| 113 | get_ltl_formula_strings(Names,Formulas) :- | |
| 114 | findall(ltl_assertion(Name,F),get_ltl_formula_string(Name,F),Assertions), | |
| 115 | findall(N,member(ltl_assertion(N,_),Assertions),Names), | |
| 116 | findall(F,member(ltl_assertion(_,F),Assertions),Formulas). | |
| 117 | get_ltl_formula_string(Tail,S) :- | |
| 118 | b_definition_prefixed(_,'ASSERT_LTL',Tail,DefName), | |
| 119 | b_get_typed_definition(DefName,[],F), | |
| 120 | ( get_texpr_expr(F,string(S)) -> true | |
| 121 | ; get_texpr_pos(F,Pos) -> | |
| 122 | add_all_perrors([error('Expected String for LTL formula',Pos)]), | |
| 123 | fail). | |
| 124 | ||
| 125 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 126 | % check all LTL assertions in a machine | |
| 127 | ||
| 128 | ltl_check_assertions(Limit,Outcome) :- | |
| 129 | get_ltl_formulas(Names,Strings,Formulas), | |
| 130 | extract_expectations(Names,Exp), | |
| 131 | ltl_check_assertions2(Names,Strings,Formulas,Exp,Limit,Outcomes), | |
| 132 | merge_outcomes(Outcomes,Outcome). | |
| 133 | ||
| 134 | ltl_check_assertions2([],[],[],[],_,[]). | |
| 135 | ltl_check_assertions2([Name|Nrest],[String|Srest],[Formula|Frest],[Exp|Erest],Limit,[Outcome|Orest]) :- | |
| 136 | print('Checking LTL formula '),print(Name),print(': '),print(String),nl, | |
| 137 | flush_output(user_output), | |
| 138 | catch( ltl_model_check2(Formula,Limit,init,Status), | |
| 139 | E, | |
| 140 | Status = exception(E)), | |
| 141 | ( Exp=pass, Status=ok -> Outcome=pass, print('no counter-example found, test passed\n') | |
| 142 | ; Exp=fail, Status=no -> Outcome=pass, print('counter-example found, test passed\n') | |
| 143 | ; Status=exception(E) -> | |
| 144 | add_error(ltl,'Caught exception: ',E),Outcome=error | |
| 145 | ; Exp=pass, Status=no -> | |
| 146 | Outcome=fail, add_error(ltl, 'Expected correct formula, but found counter-example') | |
| 147 | ; Exp=fail, Status=ok -> | |
| 148 | Outcome=fail, add_error(ltl, 'Expected counter-example, but model checker found none') | |
| 149 | ; otherwise -> | |
| 150 | add_error(ltl,'Unexpected result: ',(Exp,Status)),Outcome=fail), | |
| 151 | ltl_check_assertions2(Nrest,Srest,Frest,Erest,Limit,Orest). | |
| 152 | ||
| 153 | extract_expectations([],[]). | |
| 154 | extract_expectations([N|Nrest],[E|Erest]) :- | |
| 155 | ( atom(N),atom_codes(N,Codes),append(_,"FAIL",Codes) | |
| 156 | -> E=fail ; E=pass), | |
| 157 | extract_expectations(Nrest,Erest). | |
| 158 | ||
| 159 | merge_outcomes(List,Result) :- | |
| 160 | merge_outcomes2(List,no_tests,Result). | |
| 161 | merge_outcomes2([],R,R). | |
| 162 | merge_outcomes2([O|Rest],P,R) :- | |
| 163 | merge_outcomes3(P,O,I), | |
| 164 | merge_outcomes2(Rest,I,R). | |
| 165 | merge_outcomes3(no_tests,X,X) :- !. | |
| 166 | merge_outcomes3(_,error,error) :- !. | |
| 167 | merge_outcomes3(P,fail,fail) :- P\=error,!. | |
| 168 | merge_outcomes3(P,pass,P). | |
| 169 | ||
| 170 | %******************************************************************************* | |
| 171 | ||
| 172 | % ltl_model_check(FormulaAsAtom,Max,Mode,Status): | |
| 173 | % FormulaAsAtom: The LTL formula as an atom | |
| 174 | % Max: The maximum number of states that should be newly calculated | |
| 175 | % Mode: Where to start the search in state space | |
| 176 | % starthere: start the evaluation of the formula in the current state | |
| 177 | % init: start in the (possible several) initialisation states of the model | |
| 178 | % checkhere: start the search as in init, but check the formula F in the | |
| 179 | % current state by constructing a new formula (current -> F) "makes sense only for Past-LTL" | |
| 180 | % Status: | |
| 181 | % no: the model does not fulfil the formula, a counter-example is shown by | |
| 182 | % modifying the history | |
| 183 | % ok: the model does fulfil the formula | |
| 184 | % incomplete: the search was stopped (usually because the limit Max was reached) | |
| 185 | % before finding a counter-example or guarantee the absent of a counter-example | |
| 186 | ltl_model_check(FormulaAsAtom,Max,Mode,Status) :- | |
| 187 | debug_println(19,parsing_ltl_formula), | |
| 188 | retractall(counterexample_node(_)), | |
| 189 | retractall(counterexample_op(_)), | |
| 190 | ( temporal_parser(FormulaAsAtom,ltl,Ltl) -> | |
| 191 | ltl_model_check2(Ltl,Max,Mode,Status) | |
| 192 | ; otherwise -> | |
| 193 | add_error(ltl,'LTL Parser failed: ',FormulaAsAtom),fail | |
| 194 | ). | |
| 195 | ||
| 196 | ltl_model_check2(Ltl,Max,Mode,Status) :- | |
| 197 | debug_println(19,initialising_ltlc(Ltl,Max,Mode)), | |
| 198 | ( Ltl=syntax_error -> | |
| 199 | Status=syntax_error | |
| 200 | ; otherwise -> | |
| 201 | ltl_model_check_ast(Ltl,Max,Mode,Result), | |
| 202 | convert_result(Result,Mode,Status)). | |
| 203 | ||
| 204 | ltl_model_check_ast(Ltl,Max,Mode,Result) :- | |
| 205 | perform_static_analyses_if_necessary(Ltl), | |
| 206 | set_max_nr_of_new_impl_trans_nodes(Max), | |
| 207 | % initialising all given fairness constraints | |
| 208 | initialise_fairness_assumptions(Ltl,WeakFairnessAssumption,StrongFairnessAssumption,LtlFormula), | |
| 209 | debug_println(9,fairness_constraints(weak(WeakFairnessAssumption),strong(StrongFairnessAssumption))), | |
| 210 | select_ltl_mode(Mode,LtlFormula,Startnodes,Ltl2), | |
| 211 | preprocess_formula(Ltl2,Ltl3), | |
| 212 | debug_println(9,preprocess_formula(LtlFormula,Ltl3)), | |
| 213 | ltl_model_check4(Ltl3,Startnodes,WeakFairnessAssumption,StrongFairnessAssumption,Result), | |
| 214 | % validating the counter-example returned by the model-checker | |
| 215 | % if it fails, then this is a bug in the model-checker | |
| 216 | call_ltl_verification(Result,Ltl3), | |
| 217 | % the same to check if the counter-example is a fair counter-example (if fairness set) | |
| 218 | call_ltl_fairness_verification(Result,WeakFairnessAssumption,StrongFairnessAssumption), | |
| 219 | debug_println(9,ltl_result(Result)). | |
| 220 | ||
| 221 | % deciding whether to run the safety model checker or the ordinary LTL model checker | |
| 222 | ltl_model_check4(Ltl,Startnodes,WeakFairnessAssumption,StrongFairnessAssumption,Result) :- | |
| 223 | % checkig whether the property is a safety LTL formula | |
| 224 | ((is_ltl2ba_tool_installed,is_safety_property(Ltl,NLtl)) | |
| 225 | -> debug_println(9,'Formula is a safety property'), | |
| 226 | debug_println(9,normalized(NLtl)), | |
| 227 | ltl_mc_safety_property(Ltl,Startnodes,Result) | |
| 228 | ; call_c_initialisation, | |
| 229 | ltl_model_check5(Startnodes,Ltl,WeakFairnessAssumption,StrongFairnessAssumption,Result) | |
| 230 | ). | |
| 231 | ||
| 232 | ltl_model_check5([],_Ltl,_WeakFairnessAssumption,_StrongFairnessAssumption,nostart) :- !. | |
| 233 | ltl_model_check5(Startnodes,Ltl,WeakFairnessAssumption,StrongFairnessAssumption,Result) :- | |
| 234 | (get_preference(por,ample_sets);get_preference(por,ample_sets2)),!, | |
| 235 | % explore state space without performing any checks | |
| 236 | %((get_preference(pge,Pref), Pref\=off) -> PGE=1; PGE=0), | |
| 237 | depth_breadth_first_mode(DFMODE), | |
| 238 | set_depth_breadth_first_mode(depth_first), % set to depth-first mode | |
| 239 | print_message('******** starting a static LTL model check with partial order reduction ********'), | |
| 240 | statistics(runtime,[T1,_]), | |
| 241 | explore_state_space(0,-1,NodesAnalysed,_LimitTime,Res), | |
| 242 | statistics(runtime,[T2,_]), | |
| 243 | D is T2-T1, | |
| 244 | debug_println(9,statspace_stats(NodesAnalysed,Res)), | |
| 245 | format('state space exploration needed ~w ms to explore ~w states\n',[D,NodesAnalysed]), | |
| 246 | print_message('******** state space explored using partial order reduction ********'), | |
| 247 | set_depth_breadth_first_mode(DFMODE), % reset to previous mode | |
| 248 | print_message('******** start LTL model checking on the explored state space ********'), | |
| 249 | ltl_model_check_core(Ltl,Startnodes,WeakFairnessAssumption,StrongFairnessAssumption,Result). | |
| 250 | ltl_model_check5(Startnodes,Ltl,WeakFairnessAssumption,StrongFairnessAssumption,Result) :- | |
| 251 | ltl_model_check_core(Ltl,Startnodes,WeakFairnessAssumption,StrongFairnessAssumption,Result). | |
| 252 | ||
| 253 | ltl_model_check_core(Ltl,Startnodes,WeakFairnessAssumption,StrongFairnessAssumption,Result) :- | |
| 254 | % checking first whether some fairness constraints have been set up | |
| 255 | (fairness_check_on(WeakFairnessAssumption,StrongFairnessAssumption) -> | |
| 256 | c_ltl_modelcheck(Ltl, Startnodes, Result, ltl:cltl_callback, none, | |
| 257 | ltl_fairness:cltl_get_transition_ids_callback, ltl_fairness:cltl_get_enabled_actions_callback, WeakFairnessAssumption,StrongFairnessAssumption) | |
| 258 | ; c_ltl_modelcheck(Ltl, Startnodes, Result, ltl:cltl_callback) % no fairness assumptions have been imposed | |
| 259 | ). | |
| 260 | ||
| 261 | call_c_initialisation :- ltlc_init,!. | |
| 262 | call_c_initialisation :- | |
| 263 | add_error(ltl,'Initialisation of LTL-C module failed'), | |
| 264 | fail. | |
| 265 | ||
| 266 | select_ltl_mode(starthere,Ltl,[Startnode],not(Ltl)) :- | |
| 267 | !,current_state_id(Startnode). | |
| 268 | select_ltl_mode(init,Ltl,Startnodes,not(Ltl)) :- | |
| 269 | !,init_states(Startnodes). | |
| 270 | select_ltl_mode(checkhere,Ltl,Startnodes,not(globally(implies(ap(current),Ltl)))) :- | |
| 271 | !,init_states(Startnodes). | |
| 272 | select_ltl_mode(specific_node(Startnode),Ltl,[Startnode],not(Ltl)) :- !. | |
| 273 | select_ltl_mode(Mode,Ltl,[],Ltl) :- | |
| 274 | add_error(ltl,'Internal error: Unexpected mode: ', Mode), | |
| 275 | fail. | |
| 276 | ||
| 277 | %:- use_module(probsrc(model_checker),[model_checking_is_incomplete/6]). | |
| 278 | % 'nostart' means no initialisation state found (safety properties are true, but plain liveness properties are not true) | |
| 279 | convert_result(nostart,_,Result) :- !,Result=nostart. | |
| 280 | convert_result(none,_,Result) :- !, Result=ok. | |
| 281 | % TO DO: maybe return different result when model_checking_is_incomplete(0,1,0,0,_Msg,_Term) is true | |
| 282 | % limit 'Max' reached (possibly there are unexplored states that have not been checked yet) | |
| 283 | convert_result(incomplete,_,Result) :- !,Result=incomplete. | |
| 284 | % model/2 means counter-example has been found, if Entry=no_loop then we have a finite path (safety property or deadlock) | |
| 285 | % if Entry=loop(Idx) then we have a counter-example in lasso form with entry node of the loop on the Idx-position (starting from 0) | |
| 286 | convert_result(model(CE,_Entry),Mode,Result) :- !, Result=no, | |
| 287 | translate_ctrace(CE,Op,N,Dest), | |
| 288 | ( (Mode=init; Mode=checkhere) -> | |
| 289 | ce_get_first_state(CE,UsedInitState), | |
| 290 | set_trace_to_init(UsedInitState) | |
| 291 | ; Mode=specific_node(InitState) -> | |
| 292 | set_trace_to_init(InitState) | |
| 293 | ; otherwise -> | |
| 294 | true), | |
| 295 | execute_id_trace_from_current(Dest,Op,N). | |
| 296 | convert_result(Result,_,_) :- | |
| 297 | add_internal_error('Unexpected LTL result: ', convert_result(Result,_,_)), | |
| 298 | fail. | |
| 299 | ||
| 300 | ce_get_first_state([atom(State,_,_)|_],State). | |
| 301 | ||
| 302 | :- dynamic counterexample_node/1. | |
| 303 | :- dynamic counterexample_op/1. | |
| 304 | ||
| 305 | reset_ltl :- | |
| 306 | retractall(counterexample_node(_)), | |
| 307 | retractall(counterexample_op(_)), | |
| 308 | retractall(ltl_formula_cache(_,_)), | |
| 309 | retractall(ltl_counter_examples_cache(_,_,_,_)). | |
| 310 | ||
| 311 | :- use_module(probsrc(eventhandling),[register_event_listener/3]). | |
| 312 | :- register_event_listener(reset_specification,reset_ltl, | |
| 313 | 'Reset LTL Model Checker.'). | |
| 314 | ||
| 315 | translate_ctrace(Atoms,OpIds,StateIds,Dest) :- | |
| 316 | translate_ctrace2(Atoms,beginning,OpIds,StateIds,Dest). | |
| 317 | translate_ctrace2([atom(StartNode,_,OpId)|RestAtoms],_PreviousState,Ops,Nodes,Dest) :- | |
| 318 | assert(counterexample_node(StartNode)), | |
| 319 | assert(counterexample_op(OpId)), | |
| 320 | ( OpId = none -> Ops=[],Nodes=[],Dest=StartNode | |
| 321 | ; otherwise -> | |
| 322 | transition(StartNode,_Op,OpId,NextNode), | |
| 323 | Ops=[OpId|OpRest], Nodes=[NextNode|NextRest], | |
| 324 | translate_ctrace2(RestAtoms,NextNode,OpRest,NextRest,Dest)). | |
| 325 | translate_ctrace2([],Dest,[],[],Dest). | |
| 326 | ||
| 327 | % replacing unparsed/1 by atomic propositions | |
| 328 | % DEAD CODE | |
| 329 | %% unparsed_ap(ap(P),ap(P)) --> !. | |
| 330 | %% unparsed_ap(action(unparsed_b(OpName/Arity/Types,Exprs)),action(b(OpName/Arity,Es))) --> !, | |
| 331 | %% add_unparsed_exprs(Exprs,Types,Es). | |
| 332 | %% unparsed_ap(action(b(OpName/Arity/_Types)),action(b(OpName/Arity))) --> !. | |
| 333 | %% unparsed_ap(action(Op),action(Op)) --> !. | |
| 334 | %% unparsed_ap(unparsed(Unparsed),ap(P)) --> !,[pred(Unparsed,P)]. | |
| 335 | %% unparsed_ap(F,N) --> {F =..[Functor|Args]},unparsed_ap_l(Args,NArgs),{N=..[Functor|NArgs]}. | |
| 336 | %% unparsed_ap_l([],[]) --> []. | |
| 337 | %% unparsed_ap_l([F|Rest],[N|NRest]) --> unparsed_ap(F,N), unparsed_ap_l(Rest,NRest). | |
| 338 | ||
| 339 | %% add_unparsed_exprs([],[],[]) --> []. | |
| 340 | %% add_unparsed_exprs([expr(P,U)|UR],[T|TR],[expr(P,E)|ER]) --> | |
| 341 | %% [expr(U,T,E)], add_unparsed_exprs(UR,TR,ER). | |
| 342 | ||
| 343 | %******************************************************************************* | |
| 344 | % set current trace | |
| 345 | ||
| 346 | executetrace(Trace) :- | |
| 347 | translate_trace(Trace,OpIds,Ids,Dest), | |
| 348 | debug_println(9,exec(Dest,OpIds,Ids)), | |
| 349 | execute_id_trace_from_current(Dest,OpIds,Ids),!. | |
| 350 | executetrace(Trace) :- add_internal_error('Could not execute counter-example: ',executetrace(Trace)). | |
| 351 | ||
| 352 | translate_trace([Dest],[],[],Dest) :- | |
| 353 | assert(counterexample_node(Dest)). | |
| 354 | translate_trace([Start,Id|RestNodes],[OpId|OpRest],[Id|IdRest],Dest) :- | |
| 355 | !,transition(Start,_Op,OpId,Id), | |
| 356 | assert(counterexample_node(Start)), | |
| 357 | assert(counterexample_op(OpId)), | |
| 358 | translate_trace([Id|RestNodes],OpRest,IdRest,Dest). | |
| 359 | ||
| 360 | %******************************************************************************* | |
| 361 | % find initialised states | |
| 362 | % TODO: does NOT work with XTL (CSP?) and constants | |
| 363 | ||
| 364 | init_states(Init) :- | |
| 365 | animation_mode(Mode), | |
| 366 | ( mode_cst_init(Mode) -> | |
| 367 | findall(I,find_init(root,I,_),Init) | |
| 368 | ; mode_one_step(Mode) -> | |
| 369 | next_states(root,Init) | |
| 370 | ; otherwise -> | |
| 371 | fail). | |
| 372 | ||
| 373 | mode_cst_init(b). | |
| 374 | mode_cst_init(z). | |
| 375 | mode_cst_init(csp_and_b). | |
| 376 | ||
| 377 | mode_one_step(csp). | |
| 378 | mode_one_step(cspm). | |
| 379 | mode_one_step(xtl). | |
| 380 | %mode_one_step(promela). | |
| 381 | ||
| 382 | next_states(Start,States) :- | |
| 383 | impl_trans_term_all(Start,Ops), | |
| 384 | findall(S, member(op(_Id,_,S),Ops), States). | |
| 385 | ||
| 386 | find_init(Start,Init,Trace) :- Start==Init,!,Trace=[]. % usually called with Start=Init=root | |
| 387 | find_init(Start,Init,[State|Rest]) :- | |
| 388 | impl_trans_term(Start,O,State), | |
| 389 | find_init2(O,State,Init,Rest). | |
| 390 | find_init2(O,Init,Init,[]) :- | |
| 391 | has_functor_and_maybe_tau(O,'$initialise_machine'). | |
| 392 | find_init2(O,State,Init,Path) :- | |
| 393 | has_functor_and_maybe_tau(O,'$setup_constants'), | |
| 394 | find_init(State,Init,Path). | |
| 395 | find_init2(start_cspm_MAIN,State,Init,Path) :- | |
| 396 | find_init(State,Init,Path). | |
| 397 | find_init2(start_cspm(_Proc),State,Init,Path) :- | |
| 398 | find_init(State,Init,Path). | |
| 399 | ||
| 400 | % has_functor_and_maybe_tau(Term,Functor) | |
| 401 | % checks if Term has the form "Functor(...)" or "tau(Functor(...))" | |
| 402 | % this is used for CSP||B specification where the initialisation is wrapped with | |
| 403 | % in a tau operator | |
| 404 | has_functor_and_maybe_tau(tau(Term),Functor) :- | |
| 405 | has_functor_and_maybe_tau(Term,Functor),!. | |
| 406 | has_functor_and_maybe_tau(Term,Functor) :- | |
| 407 | functor(Term,Functor,_). | |
| 408 | ||
| 409 | ||
| 410 | set_trace_to_init(Initstate) :- | |
| 411 | animation_mode(Mode), | |
| 412 | find_trace_to_init(Mode,Initstate,Trace),!, | |
| 413 | state_space_reset, | |
| 414 | executetrace(Trace). | |
| 415 | set_trace_to_init(Initstate) :- add_internal_error('Could not replay counter-example: ',set_trace_to_init(Initstate)). | |
| 416 | ||
| 417 | find_trace_to_init(Mode,Target,[root,Target]) :- | |
| 418 | mode_one_step(Mode). | |
| 419 | find_trace_to_init(Mode,Target,[root|Trace]) :- | |
| 420 | mode_cst_init(Mode), | |
| 421 | find_init(root,Target,Trace). | |
| 422 | ||
| 423 | perform_static_analyses_if_necessary(Ltl) :- | |
| 424 | % currently only for B and Event-B | |
| 425 | (animation_mode(b) -> perform_static_analyses_if_necessary2(Ltl); true). | |
| 426 | ||
| 427 | perform_static_analyses_if_necessary2(Ltl) :- | |
| 428 | get_preference(por,PORMethod), | |
| 429 | (PORMethod==ample_sets; PORMethod==ample_sets2), | |
| 430 | prepare_ltl_model_checker_for_por(Ltl), | |
| 431 | fail. | |
| 432 | perform_static_analyses_if_necessary2(_Ltl) :- | |
| 433 | is_pge_opt_on, | |
| 434 | pge_algo: compute_operation_relations_for_pge(0), % 0 for not including the invariant into the analysis | |
| 435 | fail. | |
| 436 | perform_static_analyses_if_necessary2(_Ltl). | |
| 437 | ||
| 438 | %%% Predicates for determining which actions are visible and which are stutter in regard to the given LTL formula. | |
| 439 | %%% An operation Op in a B machine should be identified as visible for a given LTL formula f, if Op writes variables used | |
| 440 | %%% in the predicates in f or writes variables read in guard of operations inside the e(-) atoms in f. | |
| 441 | %%% In case the respective LTL formula f contains a X (next) operator then M_{POR} |= f and M |= f are not equivalent. | |
| 442 | %%% It is not clear how to handle LTL formulae containing transition propositions ([-]). (investigate e.g. LTL formulae of the form: ([Op] => g)) | |
| 443 | prepare_ltl_model_checker_for_por(Ltl) :- | |
| 444 | debug_println(9,prepare_ltl_model_checker_for_por(Ltl)), | |
| 445 | % state space should be reseted every time when a new LTL_X formula is checked, | |
| 446 | % because of the stutter condition | |
| 447 | state_space_initialise, | |
| 448 | reset_runtime_dynamic_predicates_POR, | |
| 449 | get_stutter_visible_actions(Ltl,StutterActions,VisibleActions,NextOrTP), | |
| 450 | (NextOrTP -> pp_ltl_formula(Ltl,LTLString),add_warning(ltl_mc_por, 'LTL formula contains X or Y operator, or [-] connstruct: ', LTLString); true), | |
| 451 | debug_println(9,get_stutter_visible_actions(Ltl,stutter(StutterActions),visible(VisibleActions),next_tps(NextOrTP))), | |
| 452 | assert_all_visible_stutter_actions(StutterActions,VisibleActions), | |
| 453 | % if the model is not reloaded _EnableGraph will not be computed every time a new LTL formula is checked | |
| 454 | get_por_preferences(POROptions), | |
| 455 | assert(check_cycle_proviso), | |
| 456 | compute_dependendency_relation_of_all_events_in_the_model(0,POROptions,_EnableGraph). | |
| 457 | ||
| 458 | % get_stutter_visible_actions(+Ltl,-StutterActions,-VisibleActions) | |
| 459 | % Ltl: the parsed Ltl formula presented as Prolog term. | |
| 460 | % StutterActions: the set of stutter actions in regard to Ltl | |
| 461 | % VisibleActions: the set of visible actions in regard to Ltl | |
| 462 | get_stutter_visible_actions(Ltl,StutterActions,VisibleActions,NextOrTP) :- | |
| 463 | findall(Op,b_top_level_operation(Op),Ops), | |
| 464 | list_to_ord_set(Ops,Operations), | |
| 465 | look_up_for_visible_actions(Ltl,Operations,VisActions,NextOrTP), | |
| 466 | list_to_ord_set(VisActions,VisibleActions), | |
| 467 | ord_subtract(Operations,VisibleActions,StutterActions). | |
| 468 | ||
| 469 | look_up_for_visible_actions(Ltl,Operations,VisActions,NextOrTP) :- | |
| 470 | look_up_for_visible_actions1(Ltl,Operations,VisActions,NextOrTPs), | |
| 471 | (NextOrTPs = [] -> NextOrTP=fail;NextOrTP=true). | |
| 472 | ||
| 473 | look_up_for_visible_actions1(ap(bpred(Pred)),Ops,Acts,[]) :- !, | |
| 474 | predicate_identifiers(Pred,Ids), | |
| 475 | list_to_ord_set(Ids,Vars), | |
| 476 | get_actions_modifying_variables(Vars,Ops,Acts). | |
| 477 | look_up_for_visible_actions1(action(bop(Name,_NArgs,_NRes,_Args,_Outputs)),_Ops,[Name],[true]) :- !. | |
| 478 | %% in case of [evt], 'evt' will be recognised as visible | |
| 479 | % All actions that can enable or disable an action checked for enabledness should be | |
| 480 | % asserted as visible. This means that every action that writes the variables of action | |
| 481 | % "a" which is checked for enabledness (e(a)) in the LTL-formula. | |
| 482 | look_up_for_visible_actions1(enabled(bop(Name,_NArgs,_NRes,_Args,_Outputs)),Ops,Acts,[]) :- !, | |
| 483 | b_get_operation_read_guard_vars(Name,true,GuardReads), | |
| 484 | list_to_ord_set(GuardReads,Vars), | |
| 485 | get_actions_modifying_variables(Vars,Ops,Acts). | |
| 486 | look_up_for_visible_actions1(next(F),Ops,Acts,[true|NextOrTPs]) :- !, | |
| 487 | look_up_for_visible_actions1(F,Ops,Acts,NextOrTPs). | |
| 488 | look_up_for_visible_actions1(yesterday(F),Ops,Acts,[true|NextOrTPs]) :- !, | |
| 489 | look_up_for_visible_actions1(F,Ops,Acts,NextOrTPs). | |
| 490 | look_up_for_visible_actions1(Term,_Ops,[],[]) :- % atomic can be deadlock or sink | |
| 491 | atomic(Term),!. % can Term be a variable??? | |
| 492 | % the recursive clause | |
| 493 | look_up_for_visible_actions1(Term,Ops,Actions,NextOrTPs) :- | |
| 494 | compound(Term),!, | |
| 495 | functor(Term,_Functor,N), | |
| 496 | look_up_for_visible_actions_args(N,Term,Ops,Acts,NOrTPs), | |
| 497 | append(Acts,Actions),append(NOrTPs,NextOrTPs). | |
| 498 | ||
| 499 | look_up_for_visible_actions_args(0,_,_,[],[]) :- !. | |
| 500 | look_up_for_visible_actions_args(N,Term,Ops,Actions,NextOrTPs) :- | |
| 501 | N>0,!, | |
| 502 | arg(N,Term,Arg), | |
| 503 | look_up_for_visible_actions1(Arg,Ops,Acts,NTPs), | |
| 504 | Actions = [Acts|ActsRest], NextOrTPs = [NTPs|NTPsRest], | |
| 505 | N1 is N-1, | |
| 506 | look_up_for_visible_actions_args(N1,Term,Ops,ActsRest,NTPsRest). | |
| 507 | ||
| 508 | get_actions_modifying_variables(Vars,Ops,Actions) :- | |
| 509 | maplist(variable_modified_by_action(Vars),Ops,Acts), | |
| 510 | append(Acts,Actions). | |
| 511 | ||
| 512 | variable_modified_by_action(Vars,Op,Res) :- | |
| 513 | b_get_read_write(Op,_Read,Write), | |
| 514 | (ord_intersect(Vars,Write) | |
| 515 | -> Res=[Op] | |
| 516 | ; Res=[] | |
| 517 | ). | |
| 518 | ||
| 519 | % asserting all stutter and visible actions before starting the LTL model checker | |
| 520 | assert_all_visible_stutter_actions(StutterActions,VisibleActions) :- | |
| 521 | maplist(assert_stutter_action,StutterActions), | |
| 522 | maplist(assert_visible_action,VisibleActions). | |
| 523 | ||
| 524 | assert_stutter_action(Act) :- | |
| 525 | assert(stutter_action(Act)). | |
| 526 | ||
| 527 | assert_visible_action(Act) :- | |
| 528 | assert(visible_action(Act)). | |
| 529 | ||
| 530 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 531 | % callback from LTLc: | |
| 532 | ||
| 533 | % cltl_callback(+Node, -Aps, -Out, +Queries, +Specs): | |
| 534 | % Callback predicate that evaluates for a state "Node" all atomic | |
| 535 | % propositions and returns a list of outgoing transitions. | |
| 536 | % It evaluates if each of the transitions met the propositions on transistions. | |
| 537 | % "Queries" is a list of atomic propositions (ap), "Aps" is a lists where | |
| 538 | % each entry is 0 resp 1 if the corresponding atomic proposition is true resp. false. | |
| 539 | % "Specs" is a list of propositions on transitions (tp). | |
| 540 | % "Out" is a list of outgoing transitions, for details, see below check_tps/4. | |
| 541 | :- public cltl_callback/5. | |
| 542 | cltl_callback(Node, Aps, Out, Queries, Specs) :- | |
| 543 | check_aps(Queries,Node,Aps), % generate a list of 0s and 1s, depending on whether the AP is met or not | |
| 544 | impl_trans_term_all1(Node,Trans), % find all outgoing transitions | |
| 545 | check_tps(Trans,Specs,Node,Out), % evaluate the TP on each transition and generate a list of transitions, each | |
| 546 | % annotated with 0s and 1s, depending on whether the TP is met or not | |
| 547 | debug_println(9,cltl_callback(Node, Aps, Out, Queries, Specs)). | |
| 548 | ||
| 549 | impl_trans_term_all1(Node,Trans) :- | |
| 550 | % In case that sink/deadlock is checked or the e(-) predicate is used in the LTL formula, | |
| 551 | % the state will be completely explored by execution of the check_aps/3 predicate (see implementation of trans/3). | |
| 552 | ( (animation_mode(b), is_pge_opt_on, not_all_transitions_added(Node)) | |
| 553 | -> set_context_state(Node), | |
| 554 | visited_expression(Node,CurState), | |
| 555 | pge_algo: compute_transitions_pge(Node,CurState), | |
| 556 | findall(op(Id,ActionAsTerm,To), | |
| 557 | transition(Node,ActionAsTerm,Id,To), | |
| 558 | Trans) | |
| 559 | ; impl_trans_term_all(Node,Trans) | |
| 560 | ). | |
| 561 | ||
| 562 | :- public cltl_callback_reexplore/5. | |
| 563 | % predicate used only in case POR is enabled | |
| 564 | % to satisfy the cycle condition | |
| 565 | % at this moment of the call the node has already been explored | |
| 566 | % and we need to apply the rest of the enabled events at node | |
| 567 | % to force the full exploration of it | |
| 568 | cltl_callback_reexplore(Node,Aps,Out,Queries,Specs) :- | |
| 569 | check_aps(Queries,Node,Aps), | |
| 570 | impl_trans_term_rest(Node,Trans), | |
| 571 | check_tps(Trans,Specs,Node,Out), | |
| 572 | debug_println(8,cltl_callback_reexplore(Node,Aps,Out,Queries,Specs)). | |
| 573 | ||
| 574 | impl_trans_term_rest(Node,Trans) :- | |
| 575 | get_all_already_explored_transitions(Node,Ops_so_far), | |
| 576 | state_space: compute_transitions_if_necessary_saved(From), | |
| 577 | findall(op(Id,ActionAsTerm,To), | |
| 578 | (transition(From,ActionAsTerm,Id,To),nonmember(op(Id,ActionAsTerm,To),Ops_so_far)), | |
| 579 | Trans). | |
| 580 | ||
| 581 | get_all_already_explored_transitions(Node,Ops) :- | |
| 582 | findall(op(Id,ActionAsTerm,To), | |
| 583 | transition(Node,ActionAsTerm,Id,To),Ops). | |
| 584 | ||
| 585 | % check list of atomic propositions (ap) | |
| 586 | check_aps([],_,[]). | |
| 587 | check_aps([Query|QRest],Node,[Result|RRest]) :- | |
| 588 | (check_ap(Query,Node) -> !,Result=1; Result=0), | |
| 589 | check_aps(QRest,Node,RRest). | |
| 590 | ||
| 591 | % check list of transition properties: | |
| 592 | % check_tps(+Transitions, +Specifications, +State, -Result): | |
| 593 | % "Transitions" is a list of terms of the form op(Id,Operation,NextState) | |
| 594 | % each term represents a transition from "State" to "NextState", | |
| 595 | % with the id "Id" and operation "Operation" | |
| 596 | % "Specifications" is a list of propositions on transistions (tp) | |
| 597 | % "Result" is a list where each element corresponds to a transition in "Transitions" | |
| 598 | % each entry has the form "trans(Next,Id,ResVector)" where "Next" and "Id" | |
| 599 | % are the destination state and the id of the transition, respectively, and | |
| 600 | % "ResVector" a list where each element corresponds to a proposition (tp) | |
| 601 | % in "Specifications". It is 0 resp. 1 if the proposition is false resp. true. | |
| 602 | check_tps([],_,_,[]). | |
| 603 | check_tps([op(Id,Op,Next)|OpRest],Specs,Node,[trans(Next,Id,Tp)|TpRest]) :- | |
| 604 | check_tps2(Specs,Node,Next,Op,Tp), | |
| 605 | check_tps(OpRest,Specs,Node,TpRest). | |
| 606 | check_tps2([],_,_,_,[]). | |
| 607 | check_tps2([Spec|SRest],SrcNode,DstNode,Op,[Result|RRest]) :- | |
| 608 | (check_transition(Spec,Op,SrcNode,DstNode) -> !,Result=1; Result=0), | |
| 609 | check_tps2(SRest,SrcNode,DstNode,Op,RRest). | |
| 610 | ||
| 611 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 612 | % | |
| 613 | ||
| 614 | ltl_formula_structure(Formula,Atomics,Structure) :- | |
| 615 | c_ltl_aptp(Formula,ApTp), | |
| 616 | pp_formulas(ApTp,Atomics), | |
| 617 | ltl_structure(Formula,ApTp,Structure). | |
| 618 | ||
| 619 | ltl_structure(fairnessimplication(_FAssumptions,F),Subformulas,Structure) :- !, | |
| 620 | ltl_structure(F,Subformulas,Structure). | |
| 621 | ltl_structure(ap(AP),Subformulas,ap(N)) :- | |
| 622 | !,nth0(N,Subformulas,ap(AP)),!. | |
| 623 | ltl_structure(action(TP),Subformulas,tp(N)) :- | |
| 624 | !,nth0(N,Subformulas,action(TP)),!. | |
| 625 | ltl_structure(F,ApTp,N) :- | |
| 626 | F =.. [Functor|Args], | |
| 627 | same_length(Args,NewArgs), | |
| 628 | N =.. [Functor|NewArgs], | |
| 629 | ltl_structure_l(Args,ApTp,NewArgs). | |
| 630 | ltl_structure_l([],_,[]). | |
| 631 | ltl_structure_l([F|Frest],ApTp,[N|Nrest]) :- | |
| 632 | ltl_structure(F,ApTp,N), | |
| 633 | ltl_structure_l(Frest,ApTp,Nrest). | |
| 634 | ||
| 635 | ltl_model_check_with_ce(Formula,Max,Mode,Result) :- | |
| 636 | ltl_model_check_ast(Formula,Max,Mode,R1), | |
| 637 | ce_result(R1,Formula,Result). | |
| 638 | ||
| 639 | ce_result(nostart,_,nostart) :- !. | |
| 640 | ce_result(none,_,ok) :- !. | |
| 641 | ce_result(incomplete,_,incomplete) :- !. | |
| 642 | ce_result(model(CE,LoopEntry),Formula,counterexample(Counterexample,LoopEntry,PathToCE)) :- !, | |
| 643 | ce_result_initpath(CE,PathToCE), | |
| 644 | c_ltl_aptp(Formula,ApTp), | |
| 645 | length(ApTp,N), | |
| 646 | convert_counterexample(CE,N,Counterexample). | |
| 647 | ce_result(Result,_,_) :- | |
| 648 | add_error(ltl,'Internal error: Unexpected result: ', Result), | |
| 649 | fail. | |
| 650 | ||
| 651 | ce_result_initpath(CE,Path) :- | |
| 652 | ce_get_first_state(CE,InitState), | |
| 653 | find_init(root,InitState,StatePath), | |
| 654 | find_operation_ids(StatePath,root,Path). | |
| 655 | find_operation_ids([],_,[]). | |
| 656 | find_operation_ids([Dst|Srest],Src,[(Id,Op,Dst)|Irest]) :- | |
| 657 | transition(Src,Op,Id,Dst), | |
| 658 | find_operation_ids(Srest,Dst,Irest). | |
| 659 | ||
| 660 | /* just restrict the evaluation bits to the atomic formulas */ | |
| 661 | convert_counterexample([],_N,[]). | |
| 662 | convert_counterexample([atom(State,Evals,NextOp) |Arest],N, | |
| 663 | [atom(State,NEvals,OpTuple)|Erest]) :- | |
| 664 | prefix_length(Evals,NEvals,N), | |
| 665 | ( NextOp = none -> OpTuple = none | |
| 666 | ; otherwise -> transition(State,Action,NextOp,Dst),OpTuple=(NextOp,Action,Dst)), | |
| 667 | convert_counterexample(Arest,N,Erest). | |
| 668 | ||
| 669 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 670 | ||
| 671 | % dynamic predicate for saving the LTL counterexamples for the Tcl/Tk interface | |
| 672 | :- dynamic ltl_counter_examples_cache/4. | |
| 673 | ||
| 674 | ltl_model_check_with_ce1(Proc,FormulaAsAtom,Max,Mode,Result) :- | |
| 675 | debug_println(19,parsing_ltl_formula), | |
| 676 | ( temporal_parser(FormulaAsAtom,ltl,Ltl) -> | |
| 677 | true | |
| 678 | ; otherwise -> | |
| 679 | add_error_fail(ltl,'LTL Parser failed: ',FormulaAsAtom)), | |
| 680 | ltl_model_check_with_ce2(Proc,Ltl,Max,Mode,Result). | |
| 681 | ||
| 682 | ltl_model_check_with_ce2(Proc,Ltl,Max,Mode,ActionTrace) :- | |
| 683 | debug_println(19,initialising_ltlc2(Max,Mode)), | |
| 684 | ( Ltl=syntax_error -> | |
| 685 | ActionTrace=syntax_error | |
| 686 | ; otherwise -> | |
| 687 | interruptable_ltl_model_check_ast(Ltl,Max,Mode,Result), | |
| 688 | convert_counterexample_to_action_trace(Proc,Result,Mode,Ltl,ActionTrace) | |
| 689 | ). | |
| 690 | ||
| 691 | :- use_module(probsrc(user_interrupts),[catch_interrupt_assertion_call/1]). | |
| 692 | :- use_module(extension('user_signal/user_signal'), [user_interruptable_call_det/2]). | |
| 693 | interruptable_ltl_model_check_ast(Ltl,Max,Mode,Result) :- | |
| 694 | user_interruptable_call_det(catch_interrupt_assertion_call(ltl: ltl_model_check_ast(Ltl,Max,Mode,Result)),InterruptResult), | |
| 695 | (InterruptResult=interrupted -> | |
| 696 | Result=interrupted | |
| 697 | ; (real_error_occurred -> | |
| 698 | print_error('% *** Errors occurred while LTL model checking ! ***'),nl,nl,fail | |
| 699 | ; print('LTL assertion check completed.'),nl)). | |
| 700 | ||
| 701 | convert_counterexample_to_action_trace(Proc,Result,Mode,Ltl,ActionTrace) :- | |
| 702 | ( Result = model(CE,LoopEntry) -> | |
| 703 | pp_ltl_counterexample(LoopEntry,CE,ActionTrace), | |
| 704 | (ltl_counter_examples_cache(Proc,Ltl,Mode,_) -> true; assert(ltl_counter_examples_cache(Proc,Ltl,Mode,Result))) | |
| 705 | ; Result = interrupted -> | |
| 706 | ActionTrace = interrupted | |
| 707 | ; otherwise -> | |
| 708 | convert_result(Result,Mode,ActionTrace)). | |
| 709 | ||
| 710 | pp_ltl_counterexample(deadlock,Counterexample,ce(Trace)) :- !, | |
| 711 | length(Counterexample,N), | |
| 712 | (N >= 2 -> | |
| 713 | maplist(get_operation_name,Counterexample,Trace1), | |
| 714 | ajoin_with_sep(Trace1,' -> ',Trace) | |
| 715 | ; otherwise -> | |
| 716 | Trace = deadlock). | |
| 717 | pp_ltl_counterexample(no_loop,Counterexample,ce(Trace)) :- !, | |
| 718 | maplist(get_operation_name,Counterexample,Trace1), | |
| 719 | ajoin_with_sep(Trace1,' -> ',Trace). | |
| 720 | pp_ltl_counterexample(loop(N),Counterexample,ce(Trace)) :- !, | |
| 721 | prefix_length(Counterexample,PathToCE,N), | |
| 722 | maplist(get_operation_name,PathToCE,PrefixTrace), | |
| 723 | ajoin_with_sep(PrefixTrace,' -> ',PrefixTrace1), | |
| 724 | append(PathToCE,CEPath,Counterexample), | |
| 725 | maplist(get_operation_name,CEPath,SuffixTrace), | |
| 726 | ajoin_with_sep(SuffixTrace,' -> ',SuffixTrace1), | |
| 727 | ajoin([PrefixTrace1,' -> (',SuffixTrace1,')+'],Trace). | |
| 728 | pp_ltl_counterexample(LoopEntry,_Counterexample,_CE) :- | |
| 729 | add_error_fail(ltl, 'Internal error: unknown loop entry type: ', LoopEntry). | |
| 730 | ||
| 731 | get_operation_name(atom(State,NEvasl,OpId),Res) :- | |
| 732 | (OpId = none | |
| 733 | -> Res = '|' | |
| 734 | ; transition(State,Op,OpId,_NextState) -> | |
| 735 | translate_event(Op,Res) | |
| 736 | ; otherwise | |
| 737 | -> add_error_fail(ltl_assertions_result, 'Internal Error: unknown operation in CE trace ', atom(State,NEvasl,OpId))). | |
| 738 | ||
| 739 | reset_ce_marked_nodes :- | |
| 740 | retractall(counterexample_node(_)), | |
| 741 | retractall(counterexample_op(_)). | |
| 742 | ||
| 743 | :- register_event_listener(play_counterexample,reset_ce_marked_nodes, | |
| 744 | 'Reset marked nodes from previous counterexamples.'). | |
| 745 | ||
| 746 | tcltk_play_ltl_counterexample(Proc,Ltl) :- | |
| 747 | ltl_counter_examples_cache(Proc,Ltl,Mode,model(CE,_Entry)), | |
| 748 | translate_ctrace(CE,Op,N,Dest), | |
| 749 | ( (Mode = init; Mode = checkhere) -> | |
| 750 | ce_get_first_state(CE,UsedInitState), | |
| 751 | set_trace_to_init(UsedInitState) | |
| 752 | ; Mode = specific_node(NodeID) -> | |
| 753 | set_trace_to_init(NodeID) | |
| 754 | ; otherwise -> | |
| 755 | true | |
| 756 | ),execute_id_trace_from_current(Dest,Op,N). | |
| 757 | tcltk_play_ltl_counterexample(Proc,Ltl) :- | |
| 758 | add_error_fail(ltl_counter_example, 'Internal error: No counterexample has been asserted for the following configuration: ',(Proc,Ltl)). | |
| 759 | ||
| 760 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 761 | % verify a counter-example | |
| 762 | ||
| 763 | callback_tp(TP,StateId,TransId) :- | |
| 764 | ( transition(StateId,Op,TransId,DestId) -> | |
| 765 | check_transition(TP,Op,StateId,DestId) | |
| 766 | ; otherwise -> | |
| 767 | add_error(ltl,'Internal error: callback_tp called for unknown transition: ', | |
| 768 | state_trans(StateId,TransId)), | |
| 769 | fail | |
| 770 | ). | |
| 771 | ||
| 772 | call_ltl_verification(model(Atoms,Status),Formula) :- | |
| 773 | !,call_ltl_verification2(Status,Atoms,Formula). | |
| 774 | call_ltl_verification(_,_Formula). | |
| 775 | call_ltl_verification2(Status,Atoms,Formula) :- | |
| 776 | maplist(convert_atom_to_statetransition,Atoms,StateTransitions), | |
| 777 | ( evaluate_ltl_formula(Formula,StateTransitions,Status, | |
| 778 | check_ap,callback_tp,Result) -> | |
| 779 | ( Result = true -> true | |
| 780 | ; otherwise -> | |
| 781 | add_error(ltl,'Evaluation of LTL yielded unexpected result: ',Result)) | |
| 782 | ; otherwise -> | |
| 783 | add_error(ltl,'Evaluation of LTL formula failed: ',Formula)). | |
| 784 | ||
| 785 | convert_atom_to_statetransition(atom(NodeId,_,TransId),strans(NodeId,TransId)). | |
| 786 | ||
| 787 | ||
| 788 | % fairness | |
| 789 | is_fairness_implication(fairnessimplication(_FAssumptions,_F)). | |
| 790 | ||
| 791 | call_ltl_fairness_verification(model(Atoms,Status),WeakDNF,StrongDNF) :- | |
| 792 | !,maplist(convert_atom_to_statetransition,Atoms,ST), | |
| 793 | call_ltl_fairness_verification1(WeakDNF,weak,ST,Status), | |
| 794 | call_ltl_fairness_verification1(StrongDNF,strong,ST,Status). | |
| 795 | call_ltl_fairness_verification(_,_WeakDNF,_StrongDNF). | |
| 796 | ||
| 797 | call_ltl_fairness_verification1([],_Type,_ST,_Status) :- !. | |
| 798 | call_ltl_fairness_verification1(all,Type,ST,Status) :- !, | |
| 799 | get_fairness_specification(Status,ST,Assumption), | |
| 800 | call_ltl_fairness_verification1(Assumption,Type,ST,Status). | |
| 801 | call_ltl_fairness_verification1(DNF,Type,ST,Status) :- | |
| 802 | ( call_ltl_fairness_verification2(DNF,Type,ST,Status,Result) -> | |
| 803 | true | |
| 804 | ; otherwise -> | |
| 805 | add_error(ltl,'Evalutation of LTL fairness failed: ',Type/DNF)), | |
| 806 | ( Result = fair -> true | |
| 807 | ; otherwise -> | |
| 808 | print(Type/DNF),nl, | |
| 809 | add_error(ltl,'Evaluation of LTL yields that the result violates fairness: ',Type/Result)). | |
| 810 | ||
| 811 | call_ltl_fairness_verification2([],_Type,_ST,_Status,unfair([])). | |
| 812 | call_ltl_fairness_verification2([Clause|CRest],Type,ST,Status,Result) :- | |
| 813 | call_ltl_fairness_verification3(Clause,Type,ST,Status,CResult), | |
| 814 | ( CResult = fair -> Result=fair | |
| 815 | ; CResult = unfair(Cause) -> | |
| 816 | call_ltl_fairness_verification2(CRest,Type,ST,Status,RResult), | |
| 817 | ( RResult = fair -> Result=fair | |
| 818 | ; RResult = unfair(Causes) -> Result=unfair([Cause|Causes]))). | |
| 819 | call_ltl_fairness_verification3([],_Type,_ST,_Status,fair). | |
| 820 | call_ltl_fairness_verification3([Spec|SRest],Type,ST,Status,Result) :- | |
| 821 | evaluate_ltl_fairness(Type,ST,Status,ev_fairness_id(Spec),ev_fairness_id(Spec),LResult), | |
| 822 | ( LResult = fair -> | |
| 823 | call_ltl_fairness_verification3(SRest,Type,ST,Status,Result) | |
| 824 | ; LResult = unfair(Id) -> | |
| 825 | Result = unfair(Id) | |
| 826 | ; otherwise -> | |
| 827 | add_error_fail(ltl,'Unknown result after fairness verification check: ', evaluate_ltl_fairness(Type,ST,Status,ev_fairness_id(Spec),LResult))). |