| 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 | % tcltk_interface.pl | |
| 6 | ||
| 7 | % do we still need this ? | |
| 8 | prob_use_module(X) :- load_files(X,[if(changed),load_type(source),compilation_mode(compile)]). | |
| 9 | ||
| 10 | /* load all necessary modules */ | |
| 11 | :- use_module(library(random)). | |
| 12 | :- use_module(library(lists)). | |
| 13 | :- use_module(library(system)). | |
| 14 | ||
| 15 | :- use_module(library(ordsets)). | |
| 16 | :- use_module(library(avl)). | |
| 17 | :- use_module(library(process)). | |
| 18 | ||
| 19 | :- prob_use_module(typechecker). | |
| 20 | :- prob_use_module(self_check). | |
| 21 | :- prob_use_module(kernel_waitflags). | |
| 22 | ||
| 23 | :- use_module(probsrc(specfile)). | |
| 24 | :- use_module(probsrc(translate)). | |
| 25 | :- use_module(probsrc(tools)). | |
| 26 | :- use_module(probsrc(b_enumerate)). | |
| 27 | :- use_module(probsrc(b_state_model_check)). | |
| 28 | :- use_module(probsrc(bmachine)). | |
| 29 | ||
| 30 | ||
| 31 | :- use_module(probsrc(debug)). | |
| 32 | :- use_module(probsrc(preferences)). | |
| 33 | :- prob_use_module(version). | |
| 34 | :- use_module(probsrc(b_interpreter)). | |
| 35 | :- use_module(probsrc(predicate_debugger)). | |
| 36 | :- use_module(probsrc(b_trace_checking)). | |
| 37 | :- prob_use_module(gensym). | |
| 38 | :- use_module(delay). | |
| 39 | :- use_module(probsrc(bsyntaxtree)). | |
| 40 | ||
| 41 | :- prob_use_module(kernel_objects). | |
| 42 | :- prob_use_module(bsets_clp). | |
| 43 | ||
| 44 | :- use_module(probsrc(state_space)). | |
| 45 | :- use_module(probsrc(state_space_exploration_modes)). | |
| 46 | ||
| 47 | ||
| 48 | :- prob_use_module(b_compiler). | |
| 49 | :- prob_use_module(error_manager). | |
| 50 | :- use_module(extension('plspec/plspec/plspec_core'),[set_error_handler/1]). | |
| 51 | :- use_module(extension('plspec/plspec/prettyprinter'),[pretty_print_error/1]). | |
| 52 | prob_plspec_error_handler(ErrTerm) :- plspec:pretty_print_error(ErrTerm), | |
| 53 | add_internal_error('Error detected by plspec',ErrTerm). | |
| 54 | :- set_error_handler(user:prob_plspec_error_handler). | |
| 55 | :- prob_use_module(model_checker). | |
| 56 | ||
| 57 | :- prob_use_module(visualize_graph). | |
| 58 | :- prob_use_module(state_space_reduction). | |
| 59 | :- prob_use_module(state_custom_dot_graph). | |
| 60 | :- prob_use_module(fdr_csp_generator). | |
| 61 | :- prob_use_module(coverage_statistics). | |
| 62 | :- prob_use_module(succeed_max). | |
| 63 | :- prob_use_module(tools_commands). | |
| 64 | ||
| 65 | %:- prob_use_module(testcase_generator). | |
| 66 | ||
| 67 | :- use_module(prozsrc(proz),[open_proz_file/2]). | |
| 68 | ||
| 69 | :- use_module(extension('ltsmin/ltsmin')). | |
| 70 | ||
| 71 | ||
| 72 | :- prob_use_module(reduce_graph_state_space). | |
| 73 | :- prob_use_module(b_read_write_info). | |
| 74 | %:- prob_use_module(flow). | |
| 75 | ||
| 76 | :- use_module(probltlsrc(ltl)). | |
| 77 | :- use_module(probltlsrc(ctl)). | |
| 78 | :- use_module(kodkodsrc(kodkod)). | |
| 79 | :- prob_use_module(graph_canon). | |
| 80 | %:- prob_use_module('promela/promela_ncprinter'). | |
| 81 | ||
| 82 | :- prob_use_module(sap). | |
| 83 | ||
| 84 | :- use_module(probsrc(system_call),[generate_temporary_cspm_file/2, get_writable_compiled_filename/3, system_call_keep_open/7, system_call_keep_open_no_pipes/4]). | |
| 85 | ||
| 86 | :- prob_use_module(bvisual2). | |
| 87 | :- prob_use_module(b_show_history). | |
| 88 | :- prob_use_module(enabling_analysis). | |
| 89 | :- prob_use_module(mcdc_coverage). | |
| 90 | :- prob_use_module(prologTasks). | |
| 91 | :- prob_use_module(meta_interface). | |
| 92 | ||
| 93 | % Modules from por folder | |
| 94 | :- use_module(probporsrc(dot_graphs_static_analysis)). | |
| 95 | :- use_module(probporsrc(static_analysis)). | |
| 96 | :- use_module(probporsrc(ample_sets)). | |
| 97 | :- use_module(probpgesrc(pge_algo)). | |
| 98 | ||
| 99 | :- use_module(probcspsrc(haskell_csp),[parse_and_load_cspm_file/1, | |
| 100 | get_csp_assertions_as_string/2,get_csp_processes/1, | |
| 101 | parse_and_load_cspm_file_into_specific_pl_file/2, load_cspm_pl_file/1, | |
| 102 | evaluate_csp_expression/2,evaluate_csp_expression/3, | |
| 103 | parse_single_csp_expression_file/3, parse_single_csp_declaration/3]). | |
| 104 | %:- use_module(probcspsrc(slicer_csp),[slice_from_program_point/14]). | |
| 105 | ||
| 106 | :- use_module(value_persistance, [save_constants/1,add_new_transitions_to_cache/1]). | |
| 107 | ||
| 108 | %:- use_module(ast_inspector). | |
| 109 | :- use_module(tcltk_tree_inspector). | |
| 110 | ||
| 111 | :- use_module(state_viewer_images). | |
| 112 | ||
| 113 | :- prob_use_module(symbolic_model_checker(cbc_ba)). | |
| 114 | :- prob_use_module(symbolic_model_checker(bmc)). | |
| 115 | :- prob_use_module(symbolic_model_checker(kinduction)). | |
| 116 | :- prob_use_module(symbolic_model_checker(ic3)). | |
| 117 | :- prob_use_module(symbolic_model_checker(ctigar)). | |
| 118 | :- use_module(probsrc(unsat_cores)). | |
| 119 | ||
| 120 | /* main program | |
| 121 | * ============ | |
| 122 | */ | |
| 123 | ||
| 124 | % use module_info/3 because we are not in a module here | |
| 125 | :- use_module(module_information). | |
| 126 | :- module_info(tcltk_interface,group,infrastructure). | |
| 127 | :- module_info(tcltk_interface,description,'Interface between the Tcl/Tk GUI, the CLI and the internal modules.'). | |
| 128 | ||
| 129 | /* | |
| 130 | Start server for LTSmin | |
| 131 | */ | |
| 132 | ||
| 133 | :- use_module(extension('ltsmin/ltsmin'),[start_ltsmin/4]). | |
| 134 | ||
| 135 | :- public tcltk_run_ltsmin/5. | |
| 136 | % Backend = symbolic or sequential | |
| 137 | tcltk_run_ltsmin(Backend,NoDead,NoInv,UsePOR,Res) :- | |
| 138 | % in case of POR we can also enable/disable use_cbc_analysis preference | |
| 139 | (UsePOR == true -> MoreFlags = [por] ; MoreFlags=[]), | |
| 140 | start_ltsmin(Backend, [NoDead, NoInv], MoreFlags,Result), | |
| 141 | get_check_name(NoDead,NoInv,Kind), | |
| 142 | process_ltsmin_result(Result,Kind,Res). | |
| 143 | ||
| 144 | get_check_name(true,false,Kind) :- Kind = 'INVARIANT'. | |
| 145 | get_check_name(false,true,Kind) :- Kind = 'DEADLOCK'. | |
| 146 | ||
| 147 | :- use_module(tools_printing,[format_with_colour/4]). | |
| 148 | :- use_module(extension('ltsmin/ltsmin_trace'),[csv_to_trace/3]). | |
| 149 | process_ltsmin_result(ltsmin_model_checking_ok,Kind,no_counter_example_found) :- | |
| 150 | format_with_colour(user_output,green,'LTSMin found no ~w Counter Example\n',Kind). | |
| 151 | process_ltsmin_result(ltsmin_counter_example_found(CsvFile),Kind,counter_example_found) :- | |
| 152 | format_with_colour(user_output,[red,bold],'LTSMin found ~w Counter Example\n',Kind), | |
| 153 | csv_to_trace(CsvFile,States,Transitions), | |
| 154 | print('*** REPLAYING TRACE: '),nl,print(Transitions),nl, | |
| 155 | %print(States),nl, | |
| 156 | length(Transitions,TLen), length(States,SLen), print(len(TLen,SLen)),nl, | |
| 157 | (replay_ltsmin_trace(States,Transitions) -> true | |
| 158 | ; add_error(process_ltsmin_result,'Could not replay trace:',Transitions)). | |
| 159 | ||
| 160 | replay_ltsmin_trace([],[]). | |
| 161 | replay_ltsmin_trace([State|TS],[TransName|TT]) :- | |
| 162 | (find_successor_state(State,TransName) | |
| 163 | -> replay_ltsmin_trace(TS,TT) | |
| 164 | ; add_error(replay_ltsmin_trace,'Could not execute:',TransName),fail). | |
| 165 | ||
| 166 | find_successor_state(EState,'$init_state') :- !, | |
| 167 | compute_all_inits, | |
| 168 | is_initial_state_id(NewID), | |
| 169 | state_space:visited_expression(NewID,State), | |
| 170 | %print(try_init(NewID,State)),nl, print(EState),nl, | |
| 171 | expand_const_and_vars_to_full_store(State,EState1), | |
| 172 | %print(EState1),nl, | |
| 173 | EState1=EState, | |
| 174 | tcltk_reset, | |
| 175 | tcltk_execute_trace_to_node(NewID). | |
| 176 | find_successor_state(EState,TransName) :- | |
| 177 | user:tcltk_get_options(_), | |
| 178 | current_options(Options), % print(Options),nl, | |
| 179 | member( (_,_Action,ActionOpAsTerm,NewID), Options), | |
| 180 | get_operation_name(ActionOpAsTerm,TransName), | |
| 181 | state_space:visited_expression(NewID,State), | |
| 182 | expand_const_and_vars_to_full_store(State,EState), % TO DO: only compare variables | |
| 183 | tcltk_goto_state(ActionOpAsTerm,NewID). | |
| 184 | ||
| 185 | % compute all INITIALISATIONS | |
| 186 | compute_all_inits :- is_concrete_constants_state_id(ID), compute_all_transitions_if_necessary(ID),fail. | |
| 187 | compute_all_inits. | |
| 188 | ||
| 189 | /* -------------------------------------------------------------------- */ | |
| 190 | ||
| 191 | %tcltk_find_untyped_vars(Vs) :- find_untyped_vars(Vs), Vs \== []. | |
| 192 | ||
| 193 | %tcltk_find_untyped_consts(Vs) :- find_untyped_consts(Vs), Vs \== []. | |
| 194 | ||
| 195 | :- public tcltk_find_max_reached_node/0. | |
| 196 | tcltk_find_max_reached_node :- tcltk_find_max_reached_node(_). | |
| 197 | tcltk_find_max_reached_node(ID) :- max_reached_or_timeout_for_node(ID). | |
| 198 | ||
| 199 | :- public tcltk_current_node_has_no_real_transition/0. | |
| 200 | tcltk_current_node_has_no_real_transition :- | |
| 201 | \+ tcltk_current_node_has_real_transition. | |
| 202 | tcltk_current_node_has_real_transition :- | |
| 203 | current_state_id(CurID), | |
| 204 | transition(CurID,Trans,_), | |
| 205 | (CurID \= root ; Trans \= '$partial_setup_constants'),!. | |
| 206 | tcltk_current_node_has_partial_transition :- | |
| 207 | current_state_id(CurID), | |
| 208 | transition(CurID,'$partial_setup_constants',_),!. | |
| 209 | ||
| 210 | /* --------------------------------------------------------------------- */ | |
| 211 | tcltk_goto_state(ActionAsTerm,StateID) :- | |
| 212 | (var(StateID) -> print_message(var_state(tcltk_goto_state(ActionAsTerm,StateID))) ;true), | |
| 213 | (visited_expression_id(StateID) | |
| 214 | -> true | |
| 215 | ; ajoin(['State ',StateID,' does not exist. Could be due to insufficient memory. Transition: '],Msg), | |
| 216 | add_warning(tcltk_goto_state,Msg,ActionAsTerm), | |
| 217 | fail | |
| 218 | ), | |
| 219 | (retract(current_state_id(CurID))->true;print(no_current_state_id),nl), | |
| 220 | assert(current_state_id(StateID)), | |
| 221 | (transition(CurID,ActionAsTerm,OpID,StateID) | |
| 222 | -> /* ok: proper transition */ | |
| 223 | add_to_op_trace_ids(OpID), | |
| 224 | add_id_to_history(CurID) | |
| 225 | ; (CurID=StateID | |
| 226 | -> true | |
| 227 | ; debug_println(19,jumping(CurID,ActionAsTerm,StateID)), | |
| 228 | add_to_op_trace_ids(jump(StateID)), | |
| 229 | add_id_to_history(CurID) | |
| 230 | ) | |
| 231 | ). | |
| 232 | ||
| 233 | add_id_to_history(CurID) :- | |
| 234 | (retract(history(History))->true), | |
| 235 | assert(history([CurID|History])), retractall(forward_history(_)). | |
| 236 | ||
| 237 | initialise_operation_not_yet_covered :- retractall(operation_not_yet_covered(_)), | |
| 238 | b_or_z_mode, | |
| 239 | ? | b_top_level_operation(Name), |
| 240 | % b_get_machine_operation(Name,_,Par,_), length(Par,Arity), functor(Op,Name,Arity), | |
| 241 | % Note: no '-->' added | |
| 242 | assert(operation_not_yet_covered(Name)), | |
| 243 | debug_println(operation_not_yet_covered(Name)), | |
| 244 | fail. | |
| 245 | /* Missing: treat operations with return values */ | |
| 246 | initialise_operation_not_yet_covered. | |
| 247 | ||
| 248 | ||
| 249 | tcltk_add_new_transition(FromID,Action,ToID,ToTempl,TransInfo) :- | |
| 250 | tcltk_add_new_transition_transid(FromID,Action,ToID,ToTempl,TransInfo,_TransId). | |
| 251 | ||
| 252 | tcltk_add_new_transition_transid(FromID,Action,ToID,ToTempl,TransInfo,TransId) :- | |
| 253 | get_id_of_node_and_add_if_required(ToTempl,ToID,Exists,FromID), | |
| 254 | %% print_message(tcltk_add_new_transition(FromID,Action,ToID,Exists)), %% | |
| 255 | (Exists=exists, | |
| 256 | (preferences:preference(store_only_one_incoming_transition,true) | |
| 257 | %-> transition(FromID,_,_,_) % add transition to prevent deadlock being detected | |
| 258 | ; transition(FromID,Action,TransId,ToID)) | |
| 259 | -> true %,print(not_adding(FromID,ToID,Exists)),nl | |
| 260 | ; (preferences:preference(forget_state_space,true) | |
| 261 | -> (any_transition(FromID,_,_) -> true | |
| 262 | ; store_transition(FromID,'$NO_DEADLOCK',FromID,TransId)) /* just add dummy transition */ | |
| 263 | ; store_transition(FromID,Action,ToID,TransId), | |
| 264 | (store_transition_infos(TransInfo,TransId) -> true | |
| 265 | ; add_internal_error('storing transition info failed', store_transition_infos(TransInfo,TransId))) | |
| 266 | ), | |
| 267 | add_cover(Action,OpName), | |
| 268 | animation_mode(Mode), | |
| 269 | (FromID \= ToID, b_or_z_mode(Mode), not_all_transitions_added(ToID) | |
| 270 | -> add_additional_destination_infos(FromID,OpName,ToID) | |
| 271 | ; true | |
| 272 | ) | |
| 273 | ). | |
| 274 | ||
| 275 | add_cover('-->'(Action1,_),OpName) :- !,add_cover_aux(Action1,OpName). | |
| 276 | add_cover(Action1,OpName) :- add_cover_aux(Action1,OpName). | |
| 277 | add_cover_aux(Action1,OpName) :- functor(Action1,OpName,_), | |
| 278 | (retract(operation_not_yet_covered(OpName)) | |
| 279 | -> (preferences:get_preference(provide_trace_information,true) | |
| 280 | -> print(cover(OpName)),nl ; true), | |
| 281 | ? | (operation_not_yet_covered(_) -> true ; formatsilent('~nALL OPERATIONS COVERED~n',[])) |
| 282 | ; true | |
| 283 | ). | |
| 284 | ||
| 285 | ||
| 286 | add_additional_destination_infos(FromID,ActionName,ToID) :- | |
| 287 | preference(try_operation_reuse,true), | |
| 288 | ToID \= FromID, | |
| 289 | animation_mode(b), | |
| 290 | preference(symmetry_mode,MODE), (MODE=off ; MODE=flood), | |
| 291 | % TO DO: can we enable this trick in symmetry mode ? | |
| 292 | bmachine:reuse_operation_effect(ActionName,OtherAction), | |
| 293 | \+ reuse_operation(ToID,OtherAction,_,_), | |
| 294 | assert(reuse_operation(ToID,OtherAction,FromID,ActionName)), | |
| 295 | % print(reuse_operation(ToID,OtherAction,FromID,ActionName)),nl, %% | |
| 296 | fail. | |
| 297 | add_additional_destination_infos(FromID,ActionName,ToID) :- %print(add_dest(FromID,ActionName,ToID)),nl, | |
| 298 | ( b_specialized_invariant_for_op(ActionName,_), | |
| 299 | \+ invariant_not_yet_checked(FromID), | |
| 300 | \+ invariant_violated(FromID) % if Invariant does not hold in previous state, we have no idea about invariants in the new state (proof assumes invariant holds before) | |
| 301 | -> | |
| 302 | (retract(specialized_inv(ToID,OldAVL)) -> true ; empty_avl(OldAVL)), | |
| 303 | avl_store(ActionName,OldAVL,nothing,NewAVL), | |
| 304 | % TO DO: provide a special value if an operation preserves the entire invariant ?? | |
| 305 | %print(specialized_inv(ToID,NewAVL)),nl, | |
| 306 | assert(specialized_inv(ToID,NewAVL)) | |
| 307 | ; true | |
| 308 | ). | |
| 309 | /* | |
| 310 | Store names of incoming transitions in an AVL tree | |
| 311 | Used to calculate invariant in presence of proof information | |
| 312 | */ | |
| 313 | ||
| 314 | ||
| 315 | ||
| 316 | ||
| 317 | ||
| 318 | :- use_module(state_space_exploration_modes,[set_depth_breadth_first_mode/1,dbf_modes/3]). | |
| 319 | ||
| 320 | ||
| 321 | tcltk_set_dbf_mode(Nr) :- dbf_modes(Nr,Mode,_),!, | |
| 322 | set_depth_breadth_first_mode(Mode). | |
| 323 | tcltk_set_dbf_mode(Nr) :- add_error(tcltk_set_dbf_mode,'Unknown mode: ',Nr). | |
| 324 | ||
| 325 | tcltk_dbf_modes(list(Names)) :- findall(N,dbf_modes(_,_,N),Names). | |
| 326 | ||
| 327 | ||
| 328 | :- dynamic prev_randomise_enumeration_order/1. | |
| 329 | ||
| 330 | :- public tcltk_mark_current_node_to_be_recomputed_wo_timeout/0. | |
| 331 | tcltk_mark_current_node_to_be_recomputed_wo_timeout :- | |
| 332 | current_state_id(CurID), print(recomputing(CurID)),nl, | |
| 333 | tcltk_mark_node_for_recomputed(CurID), | |
| 334 | (use_no_timeout(CurID) -> true ; assert(use_no_timeout(CurID))). | |
| 335 | :- public tcltk_mark_current_node_to_be_recomputed_with_random_enum/0. % used for recomputing a state with random enumeration | |
| 336 | tcltk_mark_current_node_to_be_recomputed_with_random_enum :- | |
| 337 | current_state_id(CurID), print(recomputing(CurID)),nl, | |
| 338 | tcltk_mark_node_for_recomputed(CurID), | |
| 339 | % TO DO: delete all destinations only reached by CurID | |
| 340 | retractall(transition(CurID,_,_,_)), | |
| 341 | temporary_set_preference(randomise_enumeration_order,true,PREV), | |
| 342 | assert(prev_randomise_enumeration_order(PREV)). | |
| 343 | :- public tcltk_finish_current_node_to_be_recomputed_with_random_enum/0. | |
| 344 | tcltk_finish_current_node_to_be_recomputed_with_random_enum :- | |
| 345 | retract(prev_randomise_enumeration_order(PREV)), | |
| 346 | reset_temporary_preference(randomise_enumeration_order,PREV). | |
| 347 | ||
| 348 | tcltk_mark_node_for_recomputed(ID) :- | |
| 349 | (not_all_transitions_added(ID) -> true | |
| 350 | ; add_id_at_front(ID)), | |
| 351 | retractall(max_reached_for_node(ID)), | |
| 352 | retractall(time_out_for_node(ID,_,_)), | |
| 353 | (transition(ID,'$partial_setup_constants',ID2) | |
| 354 | -> delete_node(ID2) ; true), | |
| 355 | retractall(state_space:transition(ID,'$partial_setup_constants',_,_)). | |
| 356 | ||
| 357 | transitions_computed_for_node(ID) :- | |
| 358 | \+(not_all_transitions_added(ID)), | |
| 359 | \+ is_not_interesting(ID). | |
| 360 | ||
| 361 | ||
| 362 | ||
| 363 | ||
| 364 | ||
| 365 | ||
| 366 | equivalent_states(S1,true,S2,true) :- \+(\+(S1=S2)). /* IMPROVE, may even | |
| 367 | allow hash functions */ | |
| 368 | ||
| 369 | :- public tcltk_set_initial_machine/0. | |
| 370 | tcltk_set_initial_machine :- | |
| 371 | tcltk_clear_machine, | |
| 372 | b_set_initial_machine, | |
| 373 | set_animation_mode(b). | |
| 374 | ||
| 375 | % new profiler | |
| 376 | %:- use_module('../extensions/profiler/profiler.pl'). | |
| 377 | ||
| 378 | % old profiler | |
| 379 | :- use_module(runtime_profiler,[reset_runtime_profiler/0]). | |
| 380 | ||
| 381 | % the following clears the entire state space and uses the current state as now starting initial state | |
| 382 | tcltk_clear_state_space_and_refocus_to_current_state :- | |
| 383 | Op = 'REFOCUS-ANIMATOR', | |
| 384 | current_expression(_CurID,CurState), | |
| 385 | (CurState = const_and_vars(ConstID,VarState) -> | |
| 386 | visited_expression(ConstID,ConstState), | |
| 387 | transition(root,SetupConstantAction,_,ConstID) | |
| 388 | ; ConstState=[]), | |
| 389 | announce_event(reset_specification), | |
| 390 | (ConstState=[] | |
| 391 | -> add_trans_id(root,Op,CurState,[],NewID,[],_TransId) | |
| 392 | ; add_trans_id(root,SetupConstantAction,ConstState,[],NewConstID,[],_), | |
| 393 | add_trans_id(NewConstID,Op,const_and_vars(NewConstID,VarState),[],NewID,[],_), | |
| 394 | (retract_open_node(NewConstID) -> true ; true), | |
| 395 | tcltk_goto_state(Op,NewConstID) | |
| 396 | ), | |
| 397 | tcltk_goto_state(Op,NewID), | |
| 398 | (retract_open_node(root) -> true ; true). | |
| 399 | ||
| 400 | :- use_module(eval_strings,[reset_eval_strings/0]). | |
| 401 | :- use_module(eventhandling, [announce_event/1]). | |
| 402 | tcltk_clear_machine :- | |
| 403 | announce_event(reset_specification), | |
| 404 | announce_event(clear_specification), | |
| 405 | retractall(cached_state_as_strings(_,_)), | |
| 406 | set_animation_mode(b), | |
| 407 | bmachine:b_set_empty_machine, | |
| 408 | reset_errors, | |
| 409 | reset_eval_strings, | |
| 410 | % reset_dynamics, % new profiler | |
| 411 | % Now done via event handling: b_interpreter:reset_b_interpreter,reset_model_checker, | |
| 412 | % bmachine:b_machine_reset, | |
| 413 | % haskell_csp:clear_cspm_spec, state_space_initialise, reduce_graph_state_space:reduce_graph_reset, reset_runtime_profiler reset_refinement_checker | |
| 414 | % b_machine_hierarchy:reset_hierarchy, reset_all_temporary_preferences, | |
| 415 | % retractall(refinement_checker: generated_predeterministic_refinement(_,_,_)), | |
| 416 | % retractall(refinement_checker: determinism_check_div_found(_)), | |
| 417 | % retractall(counterexample_node(_)), retractall(counterexample_op(_)) | |
| 418 | % clear_dynamic_predicates_for_POR, | |
| 419 | % clear_dynamic_predicates_for_PGE, | |
| 420 | garbage_collect_atoms. % reclaim atoms if possible | |
| 421 | ||
| 422 | :- use_module(prob2_interface, [start_animation/0, update_preferences_from_spec/0]). | |
| 423 | :- public tcltk_initialise/0. | |
| 424 | tcltk_initialise :- | |
| 425 | prob2_interface:update_preferences_from_spec, | |
| 426 | prob2_interface:start_animation, | |
| 427 | tcltk_try_reload. | |
| 428 | ||
| 429 | :- public tcltk_reset/0. | |
| 430 | tcltk_reset :- reset_errors, | |
| 431 | history(H), op_trace_ids(T), | |
| 432 | current_state_id(CurID), | |
| 433 | (forward_history(FH) -> true ; FH=[]), | |
| 434 | state_space_reset, | |
| 435 | gen_forward_history(T,[CurID|H],FH,FwdHist), | |
| 436 | retractall(forward_history(_)), | |
| 437 | assert(forward_history(FwdHist)). | |
| 438 | ||
| 439 | gen_forward_history([],H,R,R) :- (H=[root] -> true ; print(unexpected_remaining_hist(H)),nl). | |
| 440 | gen_forward_history([A|TT],[ID|TH],Acc,Res) :- | |
| 441 | gen_forward_history(TT,TH,[forward(ID,A)|Acc],Res). | |
| 442 | ||
| 443 | ||
| 444 | ||
| 445 | /* ---- getting available options ----- */ | |
| 446 | ||
| 447 | :- public tcltk_get_options_dest_info/1. | |
| 448 | tcltk_get_options_dest_info(L) :- | |
| 449 | tcltk_get_options_dest_info(L,[]). %[no_query_operations]). | |
| 450 | tcltk_get_options_dest_info(list(DestinationInfos),Options) :- | |
| 451 | debug_println(9,start_tcltk_get_options_dest_info), | |
| 452 | % get a list of all options which are skip events | |
| 453 | current_state_id(CurID), | |
| 454 | compute_all_transitions_if_necessary(CurID), | |
| 455 | findall(Res, (transition(CurID,ActionAsTerm,ID), % check no_query_operations | |
| 456 | (member(no_query_operations,Options) -> \+ query_op_transition(ActionAsTerm) ; true), | |
| 457 | option_dest_info(ID,ActionAsTerm,CurID,Res)),DestinationInfos). | |
| 458 | ||
| 459 | option_dest_info(DestID,ActionAsTerm,CurID,Res) :- DestID=CurID,!, | |
| 460 | (query_op_transition(ActionAsTerm) -> Res=query ; Res=skip). | |
| 461 | option_dest_info(DestID,_,_,Res) :- not_all_transitions_added(DestID),!, Res=open. | |
| 462 | option_dest_info(DestID,_,_,Res) :- invariant_violated(DestID),!,Res=invariant_violated. | |
| 463 | option_dest_info(DestID,_,_,Res) :- is_deadlocked(DestID),!,Res=deadlock. | |
| 464 | option_dest_info(_DestID,_,_,unknown). | |
| 465 | ||
| 466 | query_op_transition(Term) :- b_or_z_mode, | |
| 467 | get_operation_name(Term,OpName), | |
| 468 | b_operation_cannot_modify_state(OpName). | |
| 469 | ||
| 470 | :- public tcltk_get_options/1. | |
| 471 | tcltk_get_options(O) :- | |
| 472 | tcltk_get_options(O,[]). %[no_query_operations]). | |
| 473 | tcltk_get_options(list(Options),Parameters) :- | |
| 474 | current_state_id(CurID), debug_println(9,start_tcltk_get_options(CurID)), | |
| 475 | on_exception(user_interrupt_signal, | |
| 476 | tcltk_compute_options(CurID,TransSpecs), | |
| 477 | (assert_time_out_for_node(CurID,'unspecified_operation_interrupted_by_user',user_interrupt_signal), | |
| 478 | tcltk_get_computed_options(CurID,TransSpecs)) | |
| 479 | ), | |
| 480 | extract_actions(TransSpecs,CurID,Parameters,ActionsAndIDs,Actions), | |
| 481 | set_current_options(ActionsAndIDs), | |
| 482 | %print(Actions),nl, | |
| 483 | debug_println(9,finished_tcltk_get_options(CurID)), | |
| 484 | Actions = Options. | |
| 485 | ||
| 486 | :- use_module(tools_timeout,[time_out_call/2]). | |
| 487 | :- use_module(translate,[translate_event_with_src_and_target_id/4]). | |
| 488 | extract_actions([],_,_,[],[]). | |
| 489 | extract_actions([(_,Term,_)|T],CurID,Parameters,Srest,ET) :- | |
| 490 | member(no_query_operations,Parameters), | |
| 491 | query_op_transition(Term), | |
| 492 | !, | |
| 493 | extract_actions(T,CurID,Parameters,Srest,ET). | |
| 494 | extract_actions([(ActionId,Term,Dst)|T],CurID,Parameters,[(ActionId,Str,Term,Dst)|Srest],[Str|ET]) :- | |
| 495 | time_out_call(translate_event_with_src_and_target_id(Term,CurID,Dst,Str), | |
| 496 | Str='**TIMEOUT**'), | |
| 497 | extract_actions(T,CurID,Parameters,Srest,ET). | |
| 498 | ||
| 499 | ||
| 500 | compute_state_information_if_necessary(CurID) :- | |
| 501 | compute_all_transitions_if_necessary(CurID,true). | |
| 502 | ||
| 503 | :- public tcltk_compute_options/2. | |
| 504 | tcltk_compute_options(CurID,ActionsAndIDs) :- | |
| 505 | compute_state_information_if_necessary(CurID), | |
| 506 | %print(found_transitions(CurID)),nl, | |
| 507 | tcltk_get_computed_options(CurID,ActionsAndIDs). | |
| 508 | ||
| 509 | tcltk_get_computed_options(CurID,ActionsAndIDs) :- | |
| 510 | findall((ActId,ActionAsTerm,DestID), | |
| 511 | transition(CurID,ActionAsTerm,ActId,DestID), | |
| 512 | % TO DO: sort or group, especially if we randomize transition/3 | |
| 513 | ActionsAndIDs). | |
| 514 | ||
| 515 | :- public tcltk_get_status/3. | |
| 516 | tcltk_get_status(INVVIOLATED,MAXREACHED,TIMEOUT) :- debug_println(9,start_tcltk_get_status), | |
| 517 | current_state_id(CurID), | |
| 518 | (time_out_for_invariant(CurID) -> INVVIOLATED = 2 | |
| 519 | ; invariant_violated(CurID) -> INVVIOLATED = 1 | |
| 520 | ; not_invariant_checked(CurID) -> INVVIOLATED = 3 | |
| 521 | ; otherwise -> INVVIOLATED = 0 | |
| 522 | ), | |
| 523 | (max_reached_for_node(CurID) -> MAXREACHED = 1 ; MAXREACHED = 0), | |
| 524 | (time_out_for_node(CurID,_,time_out) -> TIMEOUT = 1 | |
| 525 | ; time_out_for_node(CurID,_,user_interrupt_signal) -> TIMEOUT = 3 % CTRL-C | |
| 526 | ; time_out_for_node(CurID,_,virtual_time_out(kodkod_timeout)) -> TIMEOUT = 1 % KODKOD; regular time-out | |
| 527 | ; time_out_for_node(CurID,_,_) -> TIMEOUT = 2 % virtual_time_out | |
| 528 | ; TIMEOUT = 0), | |
| 529 | debug_println(9,got_status(INVVIOLATED,MAXREACHED,TIMEOUT)). | |
| 530 | ||
| 531 | ||
| 532 | %%fd_copy_term(X,Y,true) :- copy_term(X,Y). | |
| 533 | ||
| 534 | ||
| 535 | ||
| 536 | /* --------------------------------------------------------------------- */ | |
| 537 | :- public tcltk_get_history/1. | |
| 538 | tcltk_get_history(list(StringHistory)) :- debug_println(9,start_tcltk_get_trace), | |
| 539 | get_action_trace(History), | |
| 540 | convert_trace_to_list_of_strings(History,StringHistory). | |
| 541 | ||
| 542 | convert_trace_to_list_of_strings([],[]). | |
| 543 | convert_trace_to_list_of_strings([action(AS,_)|T],[AS|CT]) :- !, | |
| 544 | %truncate_atom(AS,1000,TruncatedAS), % especially SETUP_CONSTANTS, INITIALISATION can be very large; leading to performance issues | |
| 545 | % get_action_trace now truncates | |
| 546 | convert_trace_to_list_of_strings(T,CT). | |
| 547 | convert_trace_to_list_of_strings([H|T],[H|CT]) :- convert_trace_to_list_of_strings(T,CT). | |
| 548 | ||
| 549 | ||
| 550 | /* --------------------------------------------------------------------- */ | |
| 551 | ||
| 552 | :- dynamic cached_state_as_strings/2. | |
| 553 | :- public tcltk_get_state/1. | |
| 554 | %tcltk_get_state(list(List)) :- !,List=[]. % comment in to disable State Properties View in ProB Tcl/Tk | |
| 555 | tcltk_get_state(list(List)) :- debug_println(9,start_tcltk_get_state), | |
| 556 | current_expression(CurID,CurState), | |
| 557 | compute_state_information_if_necessary(CurID), | |
| 558 | (time_out_for_invariant(CurID) -> List = [invariant_time_out|StateAsStrings] | |
| 559 | ; invariant_violated(CurID) -> List = [invariant_violated|StateAsStrings] | |
| 560 | ; invariant_not_yet_checked(CurID) -> List = [invariant_not_checked|StateAsStrings] | |
| 561 | ; CurID=root -> List = StateAsStrings | |
| 562 | ; CurState = concrete_constants(_) -> List = StateAsStrings | |
| 563 | ; specfile:b_or_z_mode -> List=[invariant_ok|StateAsStrings] % only in b_or_z_mode do we add not_invariant_checked facts and check invariant while model checking/animating | |
| 564 | ; List=StateAsStrings), | |
| 565 | (cached_state_as_strings(CurID,StateAsStrings) % TO DO: separate constant / variable properties ? | |
| 566 | -> true | |
| 567 | ; retractall(cached_state_as_strings(_,_)), | |
| 568 | time_out_call(tcltk_get_state(StateAsStrings,CurState), | |
| 569 | StateAsStrings = ['***TIMEOUT-PROPERTY***']), | |
| 570 | assert(cached_state_as_strings(CurID,StateAsStrings)) | |
| 571 | ), | |
| 572 | debug_println(9,finished_tcltk_get_state). | |
| 573 | ||
| 574 | :- public tcltk_get_state/2. | |
| 575 | tcltk_get_state(StateAsStrings,State) :- | |
| 576 | %print(get_state),nl, | |
| 577 | findall(Prop,property(State,Prop),StateProps), | |
| 578 | %print(translating(StateProps)),nl, | |
| 579 | translate:translate_properties_with_limit(StateProps,StateAsStrings). | |
| 580 | %print(translated(StateAsStrings)),nl. | |
| 581 | ||
| 582 | :- dynamic current_state_errors/1. | |
| 583 | ||
| 584 | :- public tcltk_get_state_errors/1. | |
| 585 | tcltk_get_state_errors(list(ErrorsAsStrings)) :- | |
| 586 | current_state_id(CurID), | |
| 587 | findall(Error,( state_error(CurID,_,Error), Error \== invariant_violated ), Errors), | |
| 588 | ~~mnf(tcltk_get_state,translate:translate_state_errors(Errors,ErrorsAsStrings)), | |
| 589 | retractall(current_state_errors(_)), | |
| 590 | assert(current_state_errors(Errors)). | |
| 591 | ||
| 592 | :- dynamic last_detailed_error/2. | |
| 593 | :- public tcltk_get_detailed_state_error/6. | |
| 594 | tcltk_get_detailed_state_error(Num,ErrorMsg,Srow,Scol,Erow,Ecol) :- | |
| 595 | retractall(last_detailed_error(_,_)), | |
| 596 | current_state_errors(Errors), | |
| 597 | nth0(Num,Errors,Error), | |
| 598 | !, %print(explaining(Error)),nl, | |
| 599 | explain_state_error(Error,Span,ErrorMsg), %print(span(Span)),nl, | |
| 600 | assert(last_detailed_error(Span,ErrorMsg)), % save info, so that we can debug if Span contains a span_predicate | |
| 601 | %(generate_dot_from_last_span_predicate('~/Desktop/err.dot') -> true ; true), | |
| 602 | (extract_line_col_for_main_file(Span,Srow,Scol,Erow,Ecol) | |
| 603 | -> true | |
| 604 | ; Srow= -1, Scol= -1, Erow= -2, Ecol= -2). | |
| 605 | ||
| 606 | can_generate_dot_from_last_state_error :- last_detailed_error(span_predicate(_,_,_),_). | |
| 607 | generate_dot_from_last_span_predicate(FileName) :- | |
| 608 | last_detailed_error(span_predicate(P,LS,State),_ErrorMsg), % also works with expressions | |
| 609 | write_dot_file_for_pred_expr_and_state(P, LS, State,FileName). | |
| 610 | ||
| 611 | :- public tcltk_current_state_invariant_violated/0. | |
| 612 | tcltk_current_state_invariant_violated :- | |
| 613 | current_state_id(CurID), | |
| 614 | invariant_violated(CurID). | |
| 615 | ||
| 616 | tcltk_state_exists_with_invariant_violated :- | |
| 617 | (invariant_violated(_) -> true). | |
| 618 | ||
| 619 | /* --------------------------------------------------------------------- */ | |
| 620 | ||
| 621 | :- public tcltk_save_history_as_trace_file/1. | |
| 622 | :- use_module(b_trace_checking, [tcltk_save_history_as_trace_file/2]). | |
| 623 | tcltk_save_history_as_trace_file(File) :- | |
| 624 | tcltk_save_history_as_trace_file(prolog,File). | |
| 625 | ||
| 626 | ||
| 627 | /* --------------------------------------------------------------------- */ | |
| 628 | ||
| 629 | :- use_module(translate, [get_bexpression_column_template/4]). | |
| 630 | :- meta_predicate call_pred_on_expanded_state(3,-,-,-). | |
| 631 | :- meta_predicate map_over_history(3,-). | |
| 632 | ||
| 633 | evaluate_bexpr_over_state(Stream,Expr,ValueTemplate,Columns,ResultColStrings,BState,OpName) :- | |
| 634 | format(Stream,'~w,',[OpName]), | |
| 635 | b_compute_expression_with_prob_ids(Expr,BState,Value), | |
| 636 | copy_term((ValueTemplate,Columns),(Value,ResultCols)), | |
| 637 | my_print_csv_value(ResultCols,Stream), | |
| 638 | maplist(translate:translate_bvalue,ResultCols,ResultColStrings), | |
| 639 | nl(Stream). | |
| 640 | ||
| 641 | :- public evaluate_expression_over_history_to_csv_file/2. | |
| 642 | % evaluate an expression over the history and save the result to a CSV file | |
| 643 | evaluate_expression_over_history_to_csv_file(Expr,File) :- | |
| 644 | parse_machine_expression(Expr,TypedExpr), | |
| 645 | get_bexpression_column_template(TypedExpr,ValueTemplate,ColHeaders,Columns), | |
| 646 | format('Writing CSV file: ~w~n',[File]), | |
| 647 | open(File,write,Stream), | |
| 648 | format(Stream,'OPERATION,',[]), | |
| 649 | my_print_csv_atoms(ColHeaders,Stream), | |
| 650 | call_cleanup(map_over_history(evaluate_bexpr_over_state(Stream,TypedExpr,ValueTemplate,Columns),_), | |
| 651 | close(Stream)), | |
| 652 | format('Finished writing CSV file: ~w~n',[File]). | |
| 653 | ||
| 654 | :- public tcltk_evaluate_expression_over_history/2. | |
| 655 | tcltk_evaluate_expression_over_history(Expr,list([list(['OPERATION','State Id'|ColHeaders])|ColumnLists])) :- | |
| 656 | parse_machine_expression(Expr,TypedExpr), | |
| 657 | get_bexpression_column_template(TypedExpr,ValueTemplate,ColHeaders,Columns), | |
| 658 | map_over_history(evaluate_bexpr_over_state(user_output,TypedExpr,ValueTemplate,Columns), | |
| 659 | ColumnLists). | |
| 660 | ||
| 661 | map_over_history(Pred,ResColumnLists) :- | |
| 662 | history(H), current_state_id(CurID), | |
| 663 | reverse([CurID|H],RH), | |
| 664 | state_space:trace(T), reverse(T,RT), | |
| 665 | maplist(call_pred_on_expanded_state(Pred),RH,[action(root,root)|RT],ColumnLists), | |
| 666 | prune_list(ColumnLists,ResColumnLists). | |
| 667 | % remove unknown elements at front for Tk | |
| 668 | prune_list([unknown|T],Res) :- !, prune_list(T,Res). | |
| 669 | prune_list(R,R). | |
| 670 | ||
| 671 | call_pred_on_expanded_state(_Pred,root,_,ColList) :- !, ColList=unknown. | |
| 672 | call_pred_on_expanded_state(Pred,StateId,action(_,ActionTerm),ResColList) :- print(StateId),nl, | |
| 673 | specfile:get_operation_name(ActionTerm,OpName), | |
| 674 | format('Processing state ~w (reached via ~w)~n',[StateId,OpName]), | |
| 675 | visited_expression(StateId,State), | |
| 676 | (state_corresponds_to_initialised_b_machine(State,BState) | |
| 677 | -> call(Pred,ColList,BState,OpName), ResColList = list([OpName,StateId|ColList]) | |
| 678 | ; ResColList = unknown ). | |
| 679 | ||
| 680 | :- use_module(b_global_sets,[add_prob_deferred_set_elements_to_store/3]). | |
| 681 | b_compute_expression_with_prob_ids(Expr,BState,Value) :- | |
| 682 | add_prob_deferred_set_elements_to_store(BState,BState1,visible), | |
| 683 | b_interpreter:b_compute_expression_nowf(Expr,[],BState1,Value). | |
| 684 | ||
| 685 | ||
| 686 | my_print_csv_atoms([A,B|T],Stream) :- !, format(Stream,'"~w",',[A]), | |
| 687 | my_print_csv_atoms([B|T],Stream). | |
| 688 | my_print_csv_atoms([A],Stream) :- format(Stream,'"~w"~n',[A]). | |
| 689 | ||
| 690 | my_print_csv_value([A,B|T],Stream) :- !, | |
| 691 | my_print_csv_value([A],Stream), | |
| 692 | write(Stream,','), | |
| 693 | my_print_csv_value([B|T],Stream). | |
| 694 | my_print_csv_value([V],Stream) :- | |
| 695 | (no_quotes_necessary(V) -> true ; write(Stream,'"')), | |
| 696 | translate:print_bvalue_stream(Stream,V), | |
| 697 | (no_quotes_necessary(V) -> true ; write(Stream,'"')). | |
| 698 | ||
| 699 | no_quotes_necessary(int(_)). | |
| 700 | no_quotes_necessary(pred_false). | |
| 701 | no_quotes_necessary(pred_true). | |
| 702 | ||
| 703 | ||
| 704 | /* --------------------------------------------------------------------- */ | |
| 705 | ||
| 706 | :- public tcltk_execute_until/1. | |
| 707 | tcltk_execute_until(FormulaAsAtom) :- | |
| 708 | (ltl_tools: temporal_parser(FormulaAsAtom,ltl,Ltl) -> | |
| 709 | true | |
| 710 | ; otherwise -> | |
| 711 | add_error(ltl,'LTL Parser failed: ',FormulaAsAtom),fail), | |
| 712 | ( Ltl=syntax_error -> | |
| 713 | add_error(ltl,'Syntax error while parsing: ',FormulaAsAtom),fail | |
| 714 | ; otherwise -> | |
| 715 | preprocess_formula(Ltl,Ltl2) | |
| 716 | ), | |
| 717 | current_state_id(CurID), | |
| 718 | prob2_interface: find_trace1(CurID,Ltl2,no_loop,1000,Trace,_Result), | |
| 719 | %TODO: check if result is deadlock. Will not fail. | |
| 720 | update_history_from_trace(Trace). | |
| 721 | ||
| 722 | update_history_from_trace([]). % TODO: Can we get an empty trace from find_trace predicate? | |
| 723 | update_history_from_trace([op(OpID,_Name,CurID,NextID)]) :- | |
| 724 | add_id_to_history(CurID), | |
| 725 | add_to_op_trace_ids(OpID), | |
| 726 | add_id_to_history(NextID), | |
| 727 | set_id_as_current_state(NextID). | |
| 728 | update_history_from_trace([op(OpID,_Name,CurID,NextID)|T]) :- | |
| 729 | add_id_to_history(CurID), | |
| 730 | add_to_op_trace_ids(OpID), | |
| 731 | add_id_to_history(NextID), | |
| 732 | update_history_from_trace(T). | |
| 733 | ||
| 734 | set_id_as_current_state(CurID) :- | |
| 735 | retract(current_state_id(_ID)), | |
| 736 | assert(current_state_id(CurID)). | |
| 737 | ||
| 738 | :- public tcltk_random_perform/0. | |
| 739 | tcltk_random_perform :- tcltk_random_perform(_). | |
| 740 | tcltk_random_perform(ActionId) :- | |
| 741 | current_options(Options), | |
| 742 | length(Options,Len), | |
| 743 | (Len>0 | |
| 744 | -> L1 is Len+1, | |
| 745 | random(1,L1,RanChoice), | |
| 746 | tcltk_perform_nr_option(RanChoice,Options,ActionId) | |
| 747 | ; true | |
| 748 | ). | |
| 749 | ||
| 750 | :- public tcltk_get_line_col/5. | |
| 751 | tcltk_get_line_col(Nr,list(StartLine),list(StartCol),list(EndLine),list(EndCol)) :- /* just get the location in the source code */ | |
| 752 | current_options(Options), | |
| 753 | nth1(Nr,Options,(_Id,_Action,ActionAsTerm,_NewID)), | |
| 754 | %print(get_source_text(ActionAsTerm)),nl, | |
| 755 | time_out_call(get_source_text_positions(ActionAsTerm,StartLine,StartCol,EndLine,EndCol), | |
| 756 | add_error_and_fail(tcltk_get_line_col,'Timeout determining source code position: ',ActionAsTerm)), | |
| 757 | StartLine \= []. % otherwise fail | |
| 758 | % print(startlines(StartLine)),nl,print(startcols(StartCol)),nl, | |
| 759 | % print(endlines(EndLine)),nl, print(endcol(EndCol)),nl. | |
| 760 | ||
| 761 | tcltk_is_sync_event(Nr) :- | |
| 762 | current_options(Options), | |
| 763 | nth1(Nr,Options,(_Id,_Action,ActionAsTerm,_NewID)), | |
| 764 | extract_span_from_event(ActionAsTerm,SPAN,_,_), | |
| 765 | extract_span_info(SPAN,Info), | |
| 766 | % print(extracted_span_info_for_sync(Info,SPAN)),nl, | |
| 767 | member(sharing,Info). | |
| 768 | ||
| 769 | % counter-part to tcltk_get_options, to execute the option/operation number Nr in that list | |
| 770 | tcltk_perform_nr(Nr) :- | |
| 771 | current_options(Options), | |
| 772 | tcltk_perform_nr_option(Nr,Options,_). | |
| 773 | ||
| 774 | :- public tcltk_perform_nr_option/3. | |
| 775 | tcltk_perform_nr_option(Nr,Options,ActionId) :- | |
| 776 | (nth1(Nr,Options,(ActionId,_Action,ActionAsTerm,NewID)) | |
| 777 | -> (forward_history([forward(NewID,ActionId)|_FwdHist]) | |
| 778 | -> tcltk_forward | |
| 779 | ; tcltk_perform_action_term(ActionAsTerm,NewID), | |
| 780 | retractall(forward_history(_)) | |
| 781 | ) | |
| 782 | ; tcltk_backtrack /* interpret as backtrack */ | |
| 783 | ). | |
| 784 | ||
| 785 | ||
| 786 | tcltk_can_backtrack :- history([_|_]). | |
| 787 | ||
| 788 | :- public tcltk_backtrack/0. | |
| 789 | tcltk_backtrack :- \+ tcltk_can_backtrack,!, | |
| 790 | print_message('Cannot backtrack'),fail. | |
| 791 | tcltk_backtrack :- | |
| 792 | remove_from_op_trace_ids(LastTraceH), | |
| 793 | retract(history(History)), | |
| 794 | retract(current_state_id(CurID)),!, | |
| 795 | History= [LastID|EHist], | |
| 796 | assert(history(EHist)), | |
| 797 | %visited_expression(LastID,LastExpr,LastBody), | |
| 798 | assert(current_state_id(LastID)), | |
| 799 | (retract(forward_history(FwdHist)) -> true ; FwdHist=[]), | |
| 800 | assert(forward_history([forward(CurID,LastTraceH)|FwdHist])). | |
| 801 | :- public tcltk_backtrack/1. % used for right-clicks in history | |
| 802 | tcltk_backtrack(N) :- N =< 0, !. | |
| 803 | tcltk_backtrack(N) :- tcltk_backtrack, N1 is N-1, tcltk_backtrack(N1). | |
| 804 | ||
| 805 | :- dynamic saved_forward_history/2. | |
| 806 | :- volatile saved_forward_history/2. | |
| 807 | ||
| 808 | :- public tcltk_prepare_for_reload/0. | |
| 809 | % save certain information to restore when reload is completed: | |
| 810 | tcltk_prepare_for_reload :- retractall(saved_forward_history(_,_)), | |
| 811 | get_action_term_trace(TrA),reverse(TrA,Tr), | |
| 812 | %print(prepare_reloading(Tr)),nl, | |
| 813 | maplist(gen_unknown_forward,Tr,SavedForwardHistory), | |
| 814 | % TO DO: add current forward history as well | |
| 815 | animation_mode(Mode), | |
| 816 | assert(saved_forward_history(SavedForwardHistory,Mode)). | |
| 817 | ||
| 818 | gen_unknown_forward(Step,forward('$UNKNOWN',Step)). | |
| 819 | ||
| 820 | % try reloading certain information from previous load of same model | |
| 821 | tcltk_try_reload :- | |
| 822 | retract(saved_forward_history(SavedForwardHistory,Mode)), | |
| 823 | animation_mode(Mode), % we are in the same mode as when saved | |
| 824 | !, | |
| 825 | % TO DO: also retractall in other places | |
| 826 | %print(reloading(SavedForwardHistory)),nl, | |
| 827 | retractall(forward_history(_)), | |
| 828 | assert(forward_history(SavedForwardHistory)). | |
| 829 | tcltk_try_reload. | |
| 830 | ||
| 831 | :- public tcltk_fast_forward/0. | |
| 832 | % go forward while possible | |
| 833 | tcltk_fast_forward :- tcltk_can_forward,!, tcltk_forward, | |
| 834 | current_state_id(CurID), | |
| 835 | compute_state_information_if_necessary(CurID), | |
| 836 | tcltk_fast_forward. | |
| 837 | tcltk_fast_forward. | |
| 838 | ||
| 839 | tcltk_can_forward :- forward_history([_|_]). | |
| 840 | tcltk_forward :- \+ tcltk_can_forward,!, | |
| 841 | print_message('Cannot go forward'),fail. | |
| 842 | tcltk_forward :- | |
| 843 | retract(forward_history([forward(FwdID,LastTraceH)|FwdHist])), | |
| 844 | % TO DO: check if FwdID is '$UNKNOWN' -> then try to find successor which can be reached via LastTraceH | |
| 845 | retract(history(EHist)), | |
| 846 | retract(current_state_id(CurID)),!, | |
| 847 | go_forward(FwdID,LastTraceH,FwdHist,CurID,EHist). | |
| 848 | go_forward('$UNKNOWN',ActionAsTerm,FwdHist,CurID,EHist) :- | |
| 849 | transition(CurID,ActionAsTerm,TransitionID,FwdID),!, | |
| 850 | %print(found(CurID,ActionAsTerm,TransitionID,FwdID)),nl, | |
| 851 | go_forward(FwdID,TransitionID,FwdHist,CurID,EHist). | |
| 852 | % TO DO: try and execute by predicat in case max_reached is true ! | |
| 853 | go_forward('$UNKNOWN',ActionAsTerm,FwdHist,CurID,EHist) :- | |
| 854 | is_initialisation_op(ActionAsTerm), | |
| 855 | % maybe PROPERTIES/INITIALISATION has changed; try and replay with other values | |
| 856 | transition(CurID,ActionAsTerm2,TransitionID,FwdID), | |
| 857 | is_initialisation_op(ActionAsTerm2), | |
| 858 | !, | |
| 859 | %print(found(CurID,ActionAsTerm,TransitionID,FwdID)),nl, | |
| 860 | translate_event(ActionAsTerm,Action), | |
| 861 | format('Could not replay ~w.~nUsing other possible transition instead.~n',[Action]), | |
| 862 | go_forward(FwdID,TransitionID,FwdHist,CurID,EHist). | |
| 863 | go_forward('$UNKNOWN',ActionAsTerm,_FwdHist,CurID,EHist) :- !, | |
| 864 | assert(forward_history([])), | |
| 865 | assert(history(EHist)), | |
| 866 | assert(current_state_id(CurID)), | |
| 867 | translate_event(ActionAsTerm,Action), | |
| 868 | add_error(tcltk_forward,'Cannot replay step after reload: ',Action). | |
| 869 | go_forward(FwdID,LastTraceH,FwdHist,CurID,EHist) :- | |
| 870 | assert(forward_history(FwdHist)), | |
| 871 | assert(history([CurID|EHist])), | |
| 872 | add_to_op_trace_ids(LastTraceH), | |
| 873 | assert(current_state_id(FwdID)), | |
| 874 | re_execute_transition_if_necessary(CurID,LastTraceH,FwdID). | |
| 875 | %visited_expression(FwdID,FwdExpr,FwdBody). | |
| 876 | ||
| 877 | is_initialisation_op(Op) :- | |
| 878 | (functor(Op,'$setup_constants',_) ;functor(Op,'$initialise_machine',_)). | |
| 879 | ||
| 880 | % re-execute operation with side-effects if necessary and if preference set | |
| 881 | % TO DO: tie into tcltk_perform so that not only the forward button but also double click | |
| 882 | % in operations pane works | |
| 883 | re_execute_transition_if_necessary(FromID,TransitionID,ToID) :- | |
| 884 | b_or_z_mode, | |
| 885 | get_preference(re_execute_operations_with_side_effects,true), | |
| 886 | bmachine_construction:external_procedure_used(_), % TO DO: check if operation itself has side-effects | |
| 887 | !, | |
| 888 | (re_execute_transition(FromID,TransitionID,ToID) | |
| 889 | -> true | |
| 890 | ; add_error(tcltk_forward,'Could not re-execute operation: ',TransitionID)). | |
| 891 | re_execute_transition_if_necessary(_,_,_). | |
| 892 | ||
| 893 | re_execute_transition(FromID,TransitionID,ToID) :- | |
| 894 | transition(FromID,ActionTerm,TransitionID,ToID), | |
| 895 | %%print(trans(ActionTerm)),nl, | |
| 896 | specfile:get_operation_name(ActionTerm,OpName), | |
| 897 | debug_println(9,re_executing_operation(OpName,FromID,TransitionID,ToID)), | |
| 898 | visited_expression(FromID,InState), | |
| 899 | specfile:b_trans(InState,OpName,ActionTerm,_NewState,_TransInfo), | |
| 900 | debug_println(9,re_executed(OpName)). | |
| 901 | ||
| 902 | :- public tcltk_perform_action_string/3. | |
| 903 | % a version of tcltk_perform_action_term which can be given only the String (e.g., for trace checking) | |
| 904 | tcltk_perform_action_string(ActionString,ActionAsTerm,NewID) :- | |
| 905 | current_state_id(CurID), | |
| 906 | transition(CurID,ActionAsTerm,_,NewID), | |
| 907 | translate_event_with_src_and_target_id(ActionAsTerm,CurID,NewID,ActionString), | |
| 908 | tcltk_goto_state(ActionAsTerm,NewID). | |
| 909 | % translate_event_with_limit(ActionAsTerm,5000,ActionString). % should use same limit as below; otherwise trace checking will fail; ideally we should check ActionString is prefix | |
| 910 | %translate_event(ActionAsTerm,ActionString). | |
| 911 | ||
| 912 | :- public tcltk_perform_action_term/2. | |
| 913 | % perform the Action with term ActionAsTerm leading to new state NewID | |
| 914 | tcltk_perform_action_term(ActionAsTerm,NewID) :- %print(tcltk_perform_action_term(Action,ActionAsTerm,NewID)),nl, | |
| 915 | (var(ActionAsTerm) | |
| 916 | -> add_internal_error('Illegal call: ',tcltk_perform_action_term(ActionAsTerm,NewID)) ; true), | |
| 917 | tcltk_goto_state(ActionAsTerm,NewID). | |
| 918 | ||
| 919 | /* allows one to execute an action in term form, from the current state: */ | |
| 920 | %tcltk_perform_action(T,Cur) :- print_message(perf(T,Cur)),fail. | |
| 921 | ||
| 922 | :- public tcltk_perform_action/2. | |
| 923 | tcltk_perform_action(ActionAsTerm,NewID) :- | |
| 924 | current_state_id(CurID), | |
| 925 | tcltk_perform_action(CurID,ActionAsTerm,NewID). | |
| 926 | tcltk_perform_action(CurID,ActionAsTerm,NewID) :- | |
| 927 | tcltk_perform_action(CurID,ActionAsTerm,NewID,_). | |
| 928 | tcltk_perform_action(CurID,ActionAsTerm,TransitionID,NewStateID) :- | |
| 929 | transition(CurID,ActionAsTerm,TransitionID,NewStateID), | |
| 930 | tcltk_goto_state(ActionAsTerm,NewStateID). | |
| 931 | ||
| 932 | tcltk_no_constants_or_no_inititalisation_found :- | |
| 933 | (current_expression(root,_) ; current_expression(_,concrete_constants(_))), | |
| 934 | current_options([]). | |
| 935 | ||
| 936 | /* ------------ */ | |
| 937 | /* tcltk_open/1 */ | |
| 938 | /* ------------ */ | |
| 939 | ||
| 940 | ||
| 941 | %prolog_check_load_errors :- | |
| 942 | % (tcltk_find_untyped_consts(ErrRes) | |
| 943 | % -> add_error(prolog_open,'These constants were not given a proper type:', ErrRes) | |
| 944 | % ; true), | |
| 945 | % (tcltk_find_untyped_vars(ErrRes) | |
| 946 | % -> add_error(prolog_open,'These variables were not given a proper type:', ErrRes) | |
| 947 | % ; true). | |
| 948 | ||
| 949 | :- public tcltk_open_b_file_for_minor_mode/2. | |
| 950 | tcltk_open_b_file_for_minor_mode(File,Minor) :- tcltk_open_b_file(File), | |
| 951 | set_animation_minor_mode(Minor). | |
| 952 | ||
| 953 | :- public tcltk_open_b_file/1. | |
| 954 | tcltk_open_b_file(File) :- print(tcltk_open_b_file(File)),nl, | |
| 955 | tcltk_clear_machine, | |
| 956 | set_animation_mode(b), | |
| 957 | print_message(loading(File)),flush_output, | |
| 958 | (bmachine:b_load_machine_from_file(File) | |
| 959 | -> print_message(loaded), | |
| 960 | set_currently_opened_file(File) | |
| 961 | ; set_failed_to_open_file(File), | |
| 962 | fail | |
| 963 | ). | |
| 964 | ||
| 965 | :- public tcltk_open_xtl_file/1. | |
| 966 | :- use_module(xtl_interface,[open_xtl_file/1]). | |
| 967 | tcltk_open_xtl_file(File) :- | |
| 968 | tcltk_clear_machine, | |
| 969 | set_animation_mode(xtl), | |
| 970 | open_xtl_file(File), set_currently_opened_file(File). | |
| 971 | ||
| 972 | ||
| 973 | :- public tcltk_open_cspm_file/1. | |
| 974 | tcltk_open_cspm_file(File) :- | |
| 975 | tcltk_clear_machine, | |
| 976 | set_animation_mode(cspm), | |
| 977 | xtl_interface:open_cspm_file(File), set_currently_opened_file(File). | |
| 978 | ||
| 979 | :- prob_use_module(xtl_interface). | |
| 980 | %tcltk_open_promela_file(File) :- | |
| 981 | % tcltk_clear_machine, | |
| 982 | % set_animation_mode(promela), | |
| 983 | % xtl_interface:open_promela_file(File), set_currently_opened_file(File). | |
| 984 | ||
| 985 | % disabled because Java parser seems broken | |
| 986 | %tcltk_open_smv_file(File) :- | |
| 987 | % tcltk_clear_machine, | |
| 988 | % set_animation_mode(smv), | |
| 989 | % xtl_interface:open_smv_file(File), set_currently_opened_file(File). | |
| 990 | ||
| 991 | :- use_module(specfile,[type_check_csp_and_b/0]). | |
| 992 | :- public tcltk_add_csp_file/1. | |
| 993 | tcltk_add_csp_file(File) :- | |
| 994 | unset_animation_minor_modes(L), % we could be in z or tla or eventb mode | |
| 995 | set_animation_mode(csp_and_b), | |
| 996 | reset_animation_minor_modes(L), | |
| 997 | xtl_interface:open_cspm_file(File), | |
| 998 | notify_change_of_animation_mode, | |
| 999 | type_check_csp_and_b. | |
| 1000 | ||
| 1001 | notify_change_of_animation_mode :- | |
| 1002 | announce_event(change_of_animation_mode). | |
| 1003 | % clear_applicable_flag. % no done via event handling | |
| 1004 | ||
| 1005 | ||
| 1006 | :- public tcltk_open_z_file/1. | |
| 1007 | tcltk_open_z_file(File) :- | |
| 1008 | tcltk_clear_machine, | |
| 1009 | tcltk_open_z_file2(File). | |
| 1010 | tcltk_open_z_file2(File) :- | |
| 1011 | open_proz_file(File,BMachine), | |
| 1012 | set_animation_mode(b), set_animation_minor_mode(z), | |
| 1013 | b_set_typed_machine(BMachine), | |
| 1014 | set_currently_opened_file(File). | |
| 1015 | ||
| 1016 | :- use_module(parsercall,[call_fuzz_parser/2]). | |
| 1017 | tcltk_open_z_tex_file(TexFile) :- | |
| 1018 | tcltk_clear_machine, | |
| 1019 | call_fuzz_parser(TexFile,FuzzFile), | |
| 1020 | tcltk_open_z_file2(FuzzFile). | |
| 1021 | ||
| 1022 | ||
| 1023 | :- use_module(eclipse_interface,[load_eventb_file/1]). | |
| 1024 | :- public tcltk_load_packaged_eventb_file/1. | |
| 1025 | tcltk_load_packaged_eventb_file(File) :- | |
| 1026 | tcltk_clear_machine, | |
| 1027 | load_eventb_file(File). | |
| 1028 | ||
| 1029 | :- use_module(parsercall,[call_alloy2pl_parser/2]). | |
| 1030 | :- use_module(probsrc('alloy2b/alloy2b'),[load_alloy_ast_prolog_file/1]). | |
| 1031 | tcltk_open_alloy_file(AlloyFile) :- | |
| 1032 | tcltk_clear_machine, | |
| 1033 | start_ms_timer(T1), | |
| 1034 | formatsilent('Parsing Alloy file: ~w~n',[AlloyFile]), | |
| 1035 | call_alloy2pl_parser(AlloyFile,PrologFile), | |
| 1036 | (silent_mode(off) -> stop_ms_walltimer_with_msg(T1,'parsing and type checking: ') ; true), | |
| 1037 | %printsilent(generated_prolog_ast(PrologFile)),nls, | |
| 1038 | start_ms_timer(T2), | |
| 1039 | load_alloy_ast_prolog_file(PrologFile), | |
| 1040 | (silent_mode(off) -> stop_ms_walltimer_with_msg(T2,'loading and translation to B: ') ; true), | |
| 1041 | set_currently_opened_file(AlloyFile). | |
| 1042 | ||
| 1043 | /* --------------------------------------------------------------------- */ | |
| 1044 | ||
| 1045 | tcltk_exists_an_open_node :- | |
| 1046 | not_all_transitions_added(_) ; not_interesting(_). | |
| 1047 | tcltk_goto_an_open_node :- | |
| 1048 | (not_all_transitions_added(ID) ; not_interesting(ID)),!, | |
| 1049 | tcltk_goto_state(find_open_node,ID). | |
| 1050 | tcltk_goto_max_reached_node :- | |
| 1051 | (max_reached_for_node(ID) ; time_out_for_node(ID)),!, | |
| 1052 | tcltk_goto_state(find_max_reached_node,ID). | |
| 1053 | ||
| 1054 | tcltk_goto_an_invariant_violation :- | |
| 1055 | invariant_violated(ID),!, | |
| 1056 | tcltk_goto_state(find_inv_violation,ID). | |
| 1057 | ||
| 1058 | ||
| 1059 | tcltk_goto_node_with_id(ToID) :- | |
| 1060 | current_state_id(ToID),!. | |
| 1061 | tcltk_goto_node_with_id(ID) :- | |
| 1062 | visited_expression_id(ID), | |
| 1063 | tcltk_execute_trace_to_node(ID). | |
| 1064 | /* --------------------------------------------------------------------- */ | |
| 1065 | ||
| 1066 | % TO DO: clean up and move into model_checker module | |
| 1067 | ||
| 1068 | tcltk_state_space_only_has_root_node :- transition(root,_,ID), | |
| 1069 | \+ not_all_transitions_added(ID),!,fail. | |
| 1070 | tcltk_state_space_only_has_root_node. | |
| 1071 | ||
| 1072 | tcltk_search_among_existing_nodes(TclTkRes,FindDeadlocks,FindInvViolations, | |
| 1073 | FindGoal,FindAssViolations) :- | |
| 1074 | search_among_existing_nodes(Res,FindDeadlocks,FindInvViolations, | |
| 1075 | FindGoal,FindAssViolations), | |
| 1076 | translate_error_for_tclk(Res,TclTkRes). | |
| 1077 | ||
| 1078 | % if tcltk_state_space_only_has_root_node is true: then we should call search_among_existing_nodes before doing open_search to ensure that we uncover state_errors in the root node | |
| 1079 | search_among_existing_nodes(invariant_violation,_FindDeadlocks,FindInvViolations, | |
| 1080 | _FindGoal,_FindAssViolations) :- | |
| 1081 | (get_state_space_stats(_,_,PrN), PrN>100 | |
| 1082 | -> print_message('Search Among Processed Nodes'), print_message(number_of_nodes(PrN)) ; true), | |
| 1083 | FindInvViolations=1, | |
| 1084 | (invariant_violated(ResID) -> true | |
| 1085 | ; find_invariant_violation_among_not_checked_nodes(ResID)), | |
| 1086 | tcltk_execute_trace_to_node(ResID). | |
| 1087 | search_among_existing_nodes(DEADLOCK,FindDeadlocks,_,_,_) :- | |
| 1088 | FindDeadlocks=1, | |
| 1089 | visited_expression_id(ResID), | |
| 1090 | transitions_computed_for_node(ResID), | |
| 1091 | is_deadlocked(ResID), | |
| 1092 | (time_out_for_node(ResID) | |
| 1093 | -> DEADLOCK = possible_deadlock_timeout ; DEADLOCK = deadlock), | |
| 1094 | print_message(deadlock_among_existing_nodes(ResID)), | |
| 1095 | tcltk_execute_trace_to_node(ResID). | |
| 1096 | search_among_existing_nodes(goal_found,_,_,FindGoal,_) :- | |
| 1097 | FindGoal=1, | |
| 1098 | %visited_expression(ResID,_CurState), | |
| 1099 | %\+(not_all_transitions_added(ResID)), % if commented out: will also look at open nodes | |
| 1100 | test_goal_in_node(ResID), | |
| 1101 | tcltk_execute_trace_to_node(ResID). | |
| 1102 | search_among_existing_nodes(assertion_violation,_,_,_,FindAssViolations) :- | |
| 1103 | FindAssViolations=1, | |
| 1104 | b_machine_has_assertions, | |
| 1105 | visited_expression(ResID,CurState), | |
| 1106 | transitions_computed_for_node(ResID), | |
| 1107 | state_violates_assertions(ResID,CurState), | |
| 1108 | tcltk_execute_trace_to_node(ResID). | |
| 1109 | search_among_existing_nodes(ERR,_,_,_,_) :- | |
| 1110 | state_space:state_error(ResID,_,Error), Error \== invariant_violated, | |
| 1111 | (Error = abort_error(ERR,_,_,_) -> true ; ERR = state_error), | |
| 1112 | tcltk_execute_trace_to_node(ResID). | |
| 1113 | search_among_existing_nodes(all,_,_,_,_). | |
| 1114 | ||
| 1115 | :- public test_goal_in_node/1. | |
| 1116 | test_goal_in_node(ResID) :- b_get_machine_goal(Goal), | |
| 1117 | eclipse_interface:test_boolean_expression_in_node(ResID,Goal). | |
| 1118 | ||
| 1119 | :- public compute_all_transitions_if_necessary/0. | |
| 1120 | compute_all_transitions_if_necessary :- | |
| 1121 | current_state_id(CurID), | |
| 1122 | compute_all_transitions_if_necessary(CurID,false). | |
| 1123 | :- public compute_all_transitions_if_necessary/1. | |
| 1124 | compute_all_transitions_if_necessary(CurID) :- | |
| 1125 | compute_all_transitions_if_necessary(CurID,false). | |
| 1126 | ||
| 1127 | compute_all_transitions_if_necessary(CurID,CheckInvariant) :- | |
| 1128 | (retract_open_node(CurID) % will assert not_invariant_checked | |
| 1129 | -> set_context_state(CurID), | |
| 1130 | % first check invariant, relevant if we want to use specialized_inv proof information | |
| 1131 | visited_expression(CurID,State), | |
| 1132 | % TO DO: this does not expand concrete_constants: the expansion may be done twice below: | |
| 1133 | % once for compute_invariant (corresponds_to_b...) and once for compute_all_transitions (prepare_state_for_specfile_trans) | |
| 1134 | prepare_state_for_specfile_trans(State,PreparedState), | |
| 1135 | (CheckInvariant==true | |
| 1136 | -> compute_invariant_if_necessary_and_requested(CurID,PreparedState) ; true), | |
| 1137 | compute_all_transitions(CurID,PreparedState), | |
| 1138 | clear_context_state | |
| 1139 | ; true). | |
| 1140 | %compute_all_transitions_if_necessary(CurID,CurState) :- | |
| 1141 | % ((not_all_transitions_added(CurID);not_interesting(CurID)) | |
| 1142 | % -> compute_all_transitions(CurID,CurState) ; true). | |
| 1143 | ||
| 1144 | ||
| 1145 | compute_invariant_if_necessary_and_requested(ID,State) :- | |
| 1146 | enter_new_error_scope(ErrScID,compute_invariant_if_necessary_and_requested), % here we setup a new error scope; see comment for force_check_invariantKO below | |
| 1147 | compute_invariant_if_necessary(ID,State), | |
| 1148 | exit_error_scope(ErrScID,_ErrOcc,compute_invariant_if_necessary_and_requested). % should we do something with error occured result ? | |
| 1149 | ||
| 1150 | compute_invariant_if_necessary(ID,State) :- | |
| 1151 | animation_mode(MODE),compute_invariant_if_necessary(ID,State,MODE). | |
| 1152 | compute_invariant_if_necessary(ID,State,MODE) :- | |
| 1153 | ( check_invariantKO(MODE,ID,State) -> true ; true). | |
| 1154 | ||
| 1155 | check_invariantKO(ID,State) :- | |
| 1156 | animation_mode(MODE),check_invariantKO(MODE,ID,State). | |
| 1157 | check_invariantKO(b,ID,State) :- | |
| 1158 | check_invariantKO2(ID,State). | |
| 1159 | check_invariantKO(csp_and_b,ID,State) :- | |
| 1160 | check_invariantKO2(ID,State). | |
| 1161 | ||
| 1162 | ||
| 1163 | check_invariantKO2(ID,_) :- invariant_violated(ID),!. | |
| 1164 | check_invariantKO2(ID,CurState) :- | |
| 1165 | set_invariant_checked(ID), % only succeeds if we haven't checked invariant for ID yet | |
| 1166 | % print(check_inv(ID)),nl, | |
| 1167 | state_corresponds_to_initialised_b_machine(CurState,CurBState), | |
| 1168 | ( preferences:preference(do_invariant_checking,false) -> assert(not_invariant_checked(ID)) | |
| 1169 | ; force_check_invariantKO(ID,CurBState)). | |
| 1170 | ||
| 1171 | :- meta_predicate catch_clpfd_overflow_call_for_state(-,0,0). | |
| 1172 | ||
| 1173 | force_check_invariantKO(ID,CurBState) :- | |
| 1174 | % Note: this checks the invariant without setting up a new error scope | |
| 1175 | % (Reason: in the model checker it would be relatively expensive to set up an error scope for each state | |
| 1176 | % the model checker stops anyway when the first error is found and then exits its error scope) | |
| 1177 | catch_clpfd_overflow_call_for_state(ID, | |
| 1178 | b_state_violates_invariant(ID,CurBState),true) -> | |
| 1179 | %(b_state_violates_invariant(ID,CurBState) -> | |
| 1180 | set_invariant_violated(ID). | |
| 1181 | % TO DO ?: call state_satisfies_negation_of_invariant if double_evaluation_when_analysing is true ? | |
| 1182 | ||
| 1183 | % try and find an invariant violation among those nodes that have not yet been checked | |
| 1184 | find_invariant_violation_among_not_checked_nodes(ID) :- | |
| 1185 | retract(not_invariant_checked(ID)), %print(checking_invariant(ID)),nl, | |
| 1186 | visited_expression(ID,State), | |
| 1187 | state_corresponds_to_initialised_b_machine(State,CurBState), | |
| 1188 | force_check_invariantKO(ID,CurBState). | |
| 1189 | ||
| 1190 | % computing ample sets (model_checker.pl) | |
| 1191 | compute_ample_set(CurID,CurState,POROptions) :- | |
| 1192 | catch_clpfd_overflow_call_for_state(CurID,compute_ample_set2(CurID,CurState,POROptions),clear_context_state). | |
| 1193 | ||
| 1194 | % preferences:preference(use_clpfd_solver,false) | |
| 1195 | compute_all_transitions(CurID,CurState) :- | |
| 1196 | catch_clpfd_overflow_call_for_state(CurID,compute_all_transitions2(CurID,CurState),clear_context_state). | |
| 1197 | ||
| 1198 | ||
| 1199 | %catch_clpfd_overflow_call_for_state(_CurID, Call,_ExtraCleanUpCode) :- | |
| 1200 | % preferences:preference(use_clpfd_solver,false),!, % Overflow should not occur | |
| 1201 | % call(Call). | |
| 1202 | :- use_module(clpfd_interface,[catch_clpfd_overflow_call2/2]). | |
| 1203 | catch_clpfd_overflow_call_for_state(CurID, Call,ExtraCleanUpCode) :- | |
| 1204 | catch_clpfd_overflow_call2(Call, | |
| 1205 | ( store_state_error(CurID,'CLPFD_integer_overflow',_), | |
| 1206 | call(ExtraCleanUpCode)) ). | |
| 1207 | ||
| 1208 | ||
| 1209 | ||
| 1210 | ||
| 1211 | :- use_module(probsrc(succeed_max),[reset_max_reached/0,max_reached/0, max_reached/1]). | |
| 1212 | compute_all_transitions2(CurID,CurState) :- /* compute all outgoing transitions for a given node */ | |
| 1213 | % set_context_state(CurID), % error_context is set for each operation below anyway. | |
| 1214 | reset_max_reached, | |
| 1215 | prepare_state_for_specfile_trans(CurState,PreparedCurState), % will perform unpacking of constants just once, for example | |
| 1216 | ((time_out_preference_disabled % e.g., when using probcli -disable_time_out | |
| 1217 | ; use_no_timeout(CurID)) | |
| 1218 | -> add_transitions_fail_loop(CurID,PreparedCurState) | |
| 1219 | ; preferences:preference(time_out,CurTO), | |
| 1220 | add_transitions__with_timeout_fail_loop(CurID,PreparedCurState,CurTO) | |
| 1221 | ), | |
| 1222 | add_partial_transitions(CurID,PreparedCurState), % also copies unsat component infos | |
| 1223 | (max_reached -> assert_max_reached_for_node(CurID),MaxReached=true ; MaxReached=false), % TO DO: use max_reached(OpID) | |
| 1224 | (CurID==root -> save_constants(MaxReached) ; add_new_transitions_to_cache(CurID)) | |
| 1225 | . %,clear_context_state. | |
| 1226 | ||
| 1227 | add_transitions_fail_loop(CurID,CurState) :- | |
| 1228 | specfile_possible_trans_name_for_successors(CurState,ActionName), | |
| 1229 | %print(adding_transition_no_timeout(CurID,ActionName)),nl, | |
| 1230 | set_error_context(operation(ActionName,CurID)), | |
| 1231 | add_transition(CurID,CurState,ActionName,_NewId), % TO DO: transmit animation_mode value? | |
| 1232 | fail. | |
| 1233 | add_transitions_fail_loop(_,_) :- clear_error_context. | |
| 1234 | ||
| 1235 | :- use_module(library(timeout),[time_out/3]). | |
| 1236 | my_timeout_test(1000000) :- print('.'), !, my_timeout_test(0). | |
| 1237 | my_timeout_test(X) :- X1 is X+1, my_timeout_test(X1). | |
| 1238 | :- public my_timeout_test/0. | |
| 1239 | my_timeout_test :- time_out(my_timeout_test(0),500,TO), nl, | |
| 1240 | print(time_out_result(TO)),nl, TO==time_out. | |
| 1241 | :- assert_must_succeed(user:my_timeout_test). | |
| 1242 | ||
| 1243 | add_transitions__with_timeout_fail_loop(CurID,CurState,CurTO) :- | |
| 1244 | enter_new_error_scope(Level,add_transitions__with_timeout_fail_loop), | |
| 1245 | call_cleanup(add_transitions__with_timeout_fail_loop2(Level,CurID,CurState,CurTO), | |
| 1246 | exit_error_scope(Level,_,add_transitions__with_timeout_fail_loop)). | |
| 1247 | ||
| 1248 | % new profiler | |
| 1249 | %:- use_module('../extensions/profiler/profiler.pl'). | |
| 1250 | %:- use_module('../extensions/profiler/profiler_te.pl'). | |
| 1251 | %:- enable_profiling(add_transions__with_timeout_fail_loop2/4). | |
| 1252 | ||
| 1253 | % old profiler | |
| 1254 | :- use_module(runtime_profiler,[profile_failure_driven_loop/2]). | |
| 1255 | ||
| 1256 | add_transitions__with_timeout_fail_loop2(Level,CurID,CurState,CurTO) :- % statistics(runtime,_), | |
| 1257 | % TO DO: prepare computing the state: expanding const and vars, unpacking, ... | |
| 1258 | ? | specfile_possible_trans_name_for_successors(CurState,ActionName), |
| 1259 | profile_failure_driven_loop(ActionName,CurID), | |
| 1260 | % Note: we enumerate possible transition names so that we can catch the time-out per name ! | |
| 1261 | % statistics(runtime,[T1,DeltaT]), print(delta_time(ActionName,DeltaT)),nl, %% | |
| 1262 | % first enumerate possible Operations/... to obtain timeout per operation/... | |
| 1263 | % TO DO: divide CurTO by number of transitions ??? | |
| 1264 | % We could also decide to have one time-out per state, only if that one is triggered move to | |
| 1265 | % finer-grained timeouts | |
| 1266 | % For probcli ../prob_examples/public_examples/B/Benchmarks/Cruise_finite1.mch --model-check, there are 35360 calls to timeout/3 (one per state the model checker reached and per transition group), with -disable-timeout none | |
| 1267 | % In SICS 4.3.5 the runtime increased from 1.480 to 2.270 seconds = 0.022 ms per timeout call | |
| 1268 | % In SICS 4.4.1 the runtime increased from 1.494 to 3.033 seconds. = 0.044 ms per timeout call. | |
| 1269 | %% statistics(runtime,[T1,_]), print(try(ActionName,T1)),nl,%% | |
| 1270 | set_error_context(operation(ActionName,CurID)), | |
| 1271 | ? | time_out_with_enum_warning_for_findall_in_current_error_scope(Level,add_transition(CurID,CurState,ActionName,_NewId),CurTO,TimeOutRes), |
| 1272 | %% statistics(runtime,[T2,_]), TDiff is T2-T1, print(added_transition(CurID,ActionName,TDiff,TimeOutRes)),nl, %% | |
| 1273 | %% add_transition(CurID,CurState,ActionName,_NewId) , | |
| 1274 | ((TimeOutRes==time_out ; nonvar(TimeOutRes),TimeOutRes=virtual_time_out(_), \+ max_reached(ActionName)) | |
| 1275 | % virtual time outs not relevant if we have already stopped earlier anyway; TO DO: does not seem to work for INITIALISATION | |
| 1276 | -> (TimeOutRes=virtual_time_out(_) -> true | |
| 1277 | ; print_message('TIME OUT: '),print_message(CurID), | |
| 1278 | print_message(CurTO),print_message(ActionName) | |
| 1279 | ), | |
| 1280 | (var(ActionName) | |
| 1281 | -> assert_time_out_for_node(CurID,'unspecified_operation',TimeOutRes) | |
| 1282 | ; assert_time_out_for_node(CurID,ActionName,TimeOutRes)) % TO DO: assert info per ActionSkeleton ? | |
| 1283 | ; true | |
| 1284 | ),fail. | |
| 1285 | add_transitions__with_timeout_fail_loop2(_,_,_,_) :- clear_error_context. | |
| 1286 | % statistics(runtime,[_,DeltaT]), print(delta_time(end,DeltaT)),nl. | |
| 1287 | ||
| 1288 | ||
| 1289 | add_transition(CurID,CurState,ActionName,PreviousSuccessorID) :- | |
| 1290 | %(var(ActionName) -> add_error_fail(add_transition,'ActionName is a variable: ',CurID) ; true), | |
| 1291 | nonvar(ActionName), % can happen in CSP, CSP||B, XTL, ... modes but also in B mode | |
| 1292 | candidate_operation_for_reuse(ActionName), % can only be true when try_operation_reuse preference is true | |
| 1293 | retract(reuse_operation(CurID,ActionName,PreviousID,_FromOp)),!, | |
| 1294 | % we don't have to compute the operation again; simply reuse pre-computed effect | |
| 1295 | b_get_operation_normalized_read_write_info(ActionName,_Read,WrittenVariables), | |
| 1296 | build_up_b_real_operation(ActionName,ActionTemplate), % missing add any parameters | |
| 1297 | % print(reusing_operation(ActionName,ActionTemplate, from(PreviousID), for(CurID),via(FromOp))),nl, | |
| 1298 | transition(PreviousID,ActionTemplate,TransID,PreviousSuccessorID), | |
| 1299 | findall(Info,transition_info(TransID,Info),TransInfos), | |
| 1300 | visited_expression(PreviousSuccessorID,PreviousExpression,true), | |
| 1301 | ~~mnf(patch_state(CurState,WrittenVariables,PreviousExpression,NewExpression)), | |
| 1302 | % (specfile_trans(CurState,ActionName,ActionTemplate,NewExpression,_,_) | |
| 1303 | % -> true ; add_error(add_transition,'Mismatch in operation reuse',ActionName), | |
| 1304 | % print(CurID),nl, print(ActionName), print(' via '), print(via(PrevOp)),nl), | |
| 1305 | ~~mnf(add_trans_id(CurID,ActionTemplate,NewExpression,[],_NewID,TransInfos,_)). | |
| 1306 | :- if(debug:global_debug_flag). | |
| 1307 | add_transition(CurID,CurState,ActionName,NewId) :- | |
| 1308 | %debug:watch(30,specfile:specfile_trans(CurState,ActionName,Act,NewExpression,TransInfo,Residue)), | |
| 1309 | %debug:watch(30,user:add_trans_id(CurID,Act,NewExpression,Residue,_NewId,TransInfo,_)). | |
| 1310 | debug:timer_call(ActionName,specfile:specfile_trans(CurState,ActionName,Act,NewExpression,TransInfo,Residue)), | |
| 1311 | debug:timer_call(user:add_trans_id(CurID,Act,NewExpression,Residue,NewId,TransInfo,_)). | |
| 1312 | :- else. | |
| 1313 | add_transition(CurID,CurState,ActionName,NewId) :- | |
| 1314 | /* ActionName maybe pre-instantiated */ | |
| 1315 | ? | specfile_trans(CurState,ActionName,Act,NewExpression,TransInfo,Residue), |
| 1316 | %% print_bt_message(specfile_trans(CurState,ActionName,Act,NewExpression,TransInfo,Residue)), %% | |
| 1317 | add_trans_id(CurID,Act,NewExpression,Residue,NewId,TransInfo,_). | |
| 1318 | :- endif. | |
| 1319 | ||
| 1320 | patch_state(const_and_vars(ConstID,Vars),WrittenVariables,PrevState, | |
| 1321 | const_and_vars(ConstID,PatchedVars)) :- !, | |
| 1322 | patch_state(Vars,WrittenVariables,PrevState,PatchedVars). | |
| 1323 | patch_state(expanded_const_and_vars(ConstID,Vars,_FullState),WrittenVariables,PrevState, | |
| 1324 | const_and_vars(ConstID,PatchedVars)) :- !, | |
| 1325 | patch_state(Vars,WrittenVariables,PrevState,PatchedVars). | |
| 1326 | %patch_state(FullState,WrittenVariables,PrevState,PatchedFullState). % do we need to patch both ? | |
| 1327 | patch_state([],_Write,_Prev,[]) :- !. | |
| 1328 | patch_state([bind(Variable,Value)|T],WrittenVariables,PrevState,[bind(Variable,NewValue)|PT]) :- !, | |
| 1329 | (ord_member(Variable,WrittenVariables) | |
| 1330 | -> lookup_variable(PrevState,Variable,NewValue) | |
| 1331 | ; NewValue=Value | |
| 1332 | ), patch_state(T,WrittenVariables,PrevState,PT). | |
| 1333 | patch_state(S,WV,PS,Res) :- add_internal_error('Illegal state: ',patch_state(S,WV,PS,Res)), Res=S. | |
| 1334 | ||
| 1335 | lookup_variable(const_and_vars(_ConstID,Vars),Var,Val) :- !, | |
| 1336 | lookup_value_for_existing_id(Var,Vars,Val). | |
| 1337 | lookup_variable(expanded_const_and_vars(_ConstID,Vars,_FullState),Var,Val) :- !, | |
| 1338 | lookup_value_for_existing_id(Var,Vars,Val). | |
| 1339 | lookup_variable(Store,Var,Val) :- lookup_value_for_existing_id(Var,Store,Val). | |
| 1340 | ||
| 1341 | ||
| 1342 | add_trans_id(CurID,Act,NewExpression,Residue,NewID,TransInfo,TransId) :- | |
| 1343 | (Residue=[] -> true ; add_error(add_trans_id,'Residue: ',CurID:Act:Residue)), | |
| 1344 | tcltk_add_new_transition_transid(CurID,Act,NewID,NewExpression,TransInfo,TransId). | |
| 1345 | ||
| 1346 | ||
| 1347 | add_partial_transitions(root,CurState) :- | |
| 1348 | /* for the moment the only state where partial transitions are computed */ | |
| 1349 | \+ any_transition(root,_,_), /* adding normal transitions was not successful */ | |
| 1350 | partial_trans(CurState,Act,NewExpression,Residue), | |
| 1351 | add_trans_id(root,Act,NewExpression,Residue,_NewID,[],_),fail. | |
| 1352 | add_partial_transitions(_CurID,_). | |
| 1353 | ||
| 1354 | /* --------------------------------------------------------------------- */ | |
| 1355 | ||
| 1356 | /* A bit like AO* algorithm: expands open nodes (i.e., states whose transitions | |
| 1357 | have not yet been computed */ | |
| 1358 | ||
| 1359 | %:- use_module(linda_slave). | |
| 1360 | :- use_module(model_checker). | |
| 1361 | :- public tcltk_model_check/11. | |
| 1362 | tcltk_model_check(Nr,TclTkRes,FindDeadlocks,FindInvViolations,FindGoal,FindAssViolations,StopFullCoverage,PartialOrderReduction,PartialGuardsEvaluation,TIMELIMIT,TotalTime) :- | |
| 1363 | statistics(walltime,[CurTime,_]), /* get current time in ms */ | |
| 1364 | LimitTime is CurTime+TIMELIMIT, | |
| 1365 | %debug_println(10,start_tcltk_model_check(Nr,TIMELIMIT)), | |
| 1366 | InspectExistingNodes = 0, | |
| 1367 | (do_model_check(Nr,_A,LimitTime,Res,FindDeadlocks,FindInvViolations,FindGoal, | |
| 1368 | FindAssViolations,StopFullCoverage,PartialOrderReduction,PartialGuardsEvaluation,InspectExistingNodes) | |
| 1369 | -> translate_error_for_tclk(Res,TclTkRes) | |
| 1370 | ; add_internal_error('Call failed: ',do_model_check(Nr,_A,LimitTime,Res,FindDeadlocks,FindInvViolations,FindGoal, | |
| 1371 | FindAssViolations,StopFullCoverage,PartialOrderReduction,PartialGuardsEvaluation,InspectExistingNodes)), | |
| 1372 | TclTkRes=error), | |
| 1373 | statistics(walltime,[CurTime2,_]), | |
| 1374 | TotalTime is CurTime2-CurTime, | |
| 1375 | debug_println(10,tcltk_model_check(Nr,TotalTime,Res)). | |
| 1376 | ||
| 1377 | translate_error_for_tclk([timeout,Nr],Res) :- !, Res=[timeout,Nr]. | |
| 1378 | translate_error_for_tclk(state_error(S),String) :- !, translate_state_err_for_tcltk(S,String). | |
| 1379 | translate_error_for_tclk(S,R) :- atomic(S),!,R=S. | |
| 1380 | translate_error_for_tclk(S,R) :- nonvar(S), add_error(translate_error_for_tclk,'Unknown Model Check result: ',S), R=unknown. | |
| 1381 | ||
| 1382 | translate_state_err_for_tcltk(abort_error(TYPE,_,_,_),ERR) :- !, ERR = TYPE. | |
| 1383 | translate_state_err_for_tcltk(eventerror(Event,Error,_),ERR) :- !, | |
| 1384 | functor(Error,F,_), | |
| 1385 | ajoin(['event_error:',Event,':',F],ERR). | |
| 1386 | translate_state_err_for_tcltk(Error,ERR) :- | |
| 1387 | functor(Error, StateError, _), atom_concat('state_error:',StateError,ERR). | |
| 1388 | ||
| 1389 | ||
| 1390 | :- public do_model_check/12. | |
| 1391 | do_model_check(_Nr,NodesAnalysed,_LimitTime,Res,FindDeadlocks,FindInvViolations,FindGoal, | |
| 1392 | FindAssViolations,_StopFullCoverage,_PartialOrderReduction,_PartialGuardsEvaluation,ForceInspectExistingNodes) :- | |
| 1393 | (tcltk_state_space_only_has_root_node -> true % Then also look at the root node | |
| 1394 | ; ForceInspectExistingNodes == 1), | |
| 1395 | search_among_existing_nodes(Res,FindDeadlocks,FindInvViolations,FindGoal, | |
| 1396 | FindAssViolations), Res \=all, NodesAnalysed=0. | |
| 1397 | do_model_check(LimitNr,NodesAnalysed,LimitTime,Res,FindDeadlocks,FindInvViolations,FindGoal, | |
| 1398 | FindAssViolations,StopFullCoverage,PartialOrderReduction,PartialGuardsEvaluation,_) :- | |
| 1399 | update_ass(FindAssViolations,FindAssViolations2), | |
| 1400 | open_search(LimitNr,NodesAnalysed,LimitTime,Res,FindDeadlocks,FindInvViolations,FindGoal, | |
| 1401 | FindAssViolations2,StopFullCoverage,PartialOrderReduction,PartialGuardsEvaluation). | |
| 1402 | ||
| 1403 | update_ass(1,FindAssViol) :- \+ b_machine_has_assertions,!, % no need to check assertions | |
| 1404 | FindAssViol=0. | |
| 1405 | update_ass(X,X). | |
| 1406 | ||
| 1407 | /* --------------------------------------------------- */ | |
| 1408 | ||
| 1409 | /* constraint-based checking of refinements */ | |
| 1410 | :- use_module(cbc_refinement_checks). | |
| 1411 | tcltk_cbc_refinement_check(list(List),ErrorOccured) :- | |
| 1412 | cbc_refinement_check(List,ErrorOccured). | |
| 1413 | ||
| 1414 | /* constraint-based/model search for invariant violations */ | |
| 1415 | ||
| 1416 | :- dynamic cbc_inv_error_found/2. | |
| 1417 | :- public tcltk_constraint_based_check/1. | |
| 1418 | tcltk_constraint_based_check(L) :- tcltk_constraint_based_check(L,_). | |
| 1419 | tcltk_constraint_based_check(list(List),ErrorsOrTimeoutWereFound) :- | |
| 1420 | retractall(cbc_inv_error_found(_,_)), | |
| 1421 | findall(Res, (tcltk_constraint_based_check_with_timeout(OpName,ErrorDesc), | |
| 1422 | (ErrorDesc=ok -> true ; assert(cbc_inv_error_found(OpName,ErrorDesc))), | |
| 1423 | string_concatenate(' == ',ErrorDesc,Res1), | |
| 1424 | string_concatenate(OpName,Res1,Res)), List), | |
| 1425 | %%print(list(List)),nl, %% | |
| 1426 | (cbc_inv_error_found(_,_) -> | |
| 1427 | (cbc_inv_error_found(_,X),X\=time_out | |
| 1428 | -> ErrorsOrTimeoutWereFound=true ; ErrorsOrTimeoutWereFound=time_out | |
| 1429 | ) | |
| 1430 | ; ErrorsOrTimeoutWereFound = false). | |
| 1431 | ||
| 1432 | % can also be called with uninstantiated OpName | |
| 1433 | tcltk_constraint_based_check_with_timeout(OpName,ErrorDesc) :- | |
| 1434 | preferences:get_computed_preference(debug_time_out,DebugTimeOut), | |
| 1435 | valid_operation_or_init(OpName), | |
| 1436 | (time_out_with_enum_warning_one_solution(tcltk_constraint_based_check_op(OpName,ErrorDesc),DebugTimeOut,TimeOutRes) | |
| 1437 | -> (is_time_out_result(TimeOutRes) | |
| 1438 | -> print_message('TIME OUT: '), print_message(OpName), print_message(DebugTimeOut), | |
| 1439 | ErrorDesc = timeout | |
| 1440 | ; true | |
| 1441 | )). | |
| 1442 | valid_operation_or_init(OpName) :- b_get_machine_operation(OpName,_,_,_). | |
| 1443 | valid_operation_or_init('INITIALISATION'). | |
| 1444 | ||
| 1445 | tcltk_constraint_based_check_op(OpName,ErrorDesc) :- | |
| 1446 | (OpName == 'INITIALISATION' ; OpName = '$initialise_machine'), | |
| 1447 | !, | |
| 1448 | (call_cbc_command(tcltk_cbc_find_invariant_violation('',Res)) | |
| 1449 | -> (Res = no_solution_found -> ErrorDesc = 'ok' | |
| 1450 | ; Res = time_out -> ErrorDesc = time_out | |
| 1451 | ; ajoin(['invariant_violated_after(',OpName,')'],ErrorDesc) | |
| 1452 | ) | |
| 1453 | ; ErrorDesc = 'internal_error' | |
| 1454 | ). | |
| 1455 | tcltk_constraint_based_check_op(OpName,ErrorDesc) :- | |
| 1456 | call_cbc_command(state_model_check(OpName,State,Operation,NewState)),!, | |
| 1457 | %fd_copy_term(NewState,ResTempl,ResBody), print(ResTempl),print(ResBody),nl, | |
| 1458 | %fd_copy_term(State,PriorTempl,PriorBody), | |
| 1459 | tcltk_add_new_transition_transid(root,'$JUMP'(constraint_based_check),PriorID,State,[],TransId1), | |
| 1460 | translate_event(Operation,Action), | |
| 1461 | tcltk_add_new_transition_transid(PriorID,Operation,NewID,NewState,[],TransId2), | |
| 1462 | retractall(current_state_id(_)), | |
| 1463 | assert(current_state_id(NewID)), | |
| 1464 | reset_op_trace_ids, | |
| 1465 | add_to_op_trace_ids(TransId1), add_to_op_trace_ids(TransId2), | |
| 1466 | retractall(history(_)), | |
| 1467 | retractall(forward_history(_)), | |
| 1468 | assert(history([PriorID,root])), | |
| 1469 | ajoin(['invariant_violated_after(',Action,')'],ErrorDesc). | |
| 1470 | tcltk_constraint_based_check_op(_,'ok'). | |
| 1471 | ||
| 1472 | :- public tcltk_cbc_find_trace/2. | |
| 1473 | % try to find constants, parameters that make a given trace feasible | |
| 1474 | tcltk_cbc_find_trace(TraceToBeFound,Res) :- | |
| 1475 | tcltk_cbc_find_trace(TraceToBeFound,'',first_solution,Res). | |
| 1476 | :- public tcltk_cbc_find_invariant_violation/2. | |
| 1477 | tcltk_cbc_find_invariant_violation(TraceToBeFound,Res) :- | |
| 1478 | tcltk_cbc_find_trace(TraceToBeFound,'#not_invariant',first_solution,Res). | |
| 1479 | ||
| 1480 | tcltk_cbc_find_trace(TraceToBeFound,TargetPredString,FindAll,Res) :- | |
| 1481 | b_parse_optional_machine_predicate(TargetPredString,TargetPred), | |
| 1482 | formatsilent('Looking for solution for trace ~w~n',[TraceToBeFound]), | |
| 1483 | split_atom(TraceToBeFound,[',',';',' '],TraceAsList), | |
| 1484 | (maplist(check_valid_operation,TraceAsList) | |
| 1485 | -> start_ms_timer(Timer), | |
| 1486 | tcltk_cbc_find_trace_aux(Timer,TraceAsList,TargetPred,FindAll,Res) | |
| 1487 | ; Res = error). | |
| 1488 | tcltk_cbc_find_trace_aux(Timer,TraceAsList,TargetPred,FindAll,Res) :- | |
| 1489 | preferences:get_computed_preference(debug_time_out,DebugTimeOut), | |
| 1490 | reset_nr_cbc_sols, | |
| 1491 | time_out_with_enum_warning_one_solution(sap:create_testcase_path_nondet(init,TraceAsList,TargetPred,Transitions),DebugTimeOut,TimeOutRes), | |
| 1492 | stop_ms_timer(Timer), | |
| 1493 | (is_time_out_result(TimeOutRes) | |
| 1494 | -> !, | |
| 1495 | print_message('*** TIME OUT: '), print_message(DebugTimeOut), Res = time_out | |
| 1496 | ; FindAll = findall -> inc_nr_cbc_sols, | |
| 1497 | print('% *** FOUND PATH: '), maplist(print_trans,Transitions),nl, | |
| 1498 | fail % backtrack to find further solutions | |
| 1499 | ; !,Res = ok, | |
| 1500 | print('% *** FOUND PATH: '), maplist(print_trans,Transitions),nl, | |
| 1501 | maplist(extract_trans_id,Transitions,TransIds), | |
| 1502 | set_trace_by_transition_ids(TransIds) | |
| 1503 | ). | |
| 1504 | tcltk_cbc_find_trace_aux(Timer,_TraceToBeFound,_TargetPred,findall,R) :- !, stop_ms_timer(Timer), | |
| 1505 | R=nr_cbc_sols(Res), | |
| 1506 | nr_cbc_sols(Res), | |
| 1507 | print_message('*** ALL SOLUTIONS FOUND '). | |
| 1508 | tcltk_cbc_find_trace_aux(Timer,_TraceToBeFound,_TargetPred,_FindAll,no_solution_found) :- | |
| 1509 | stop_ms_timer(Timer), | |
| 1510 | print_message('*** NO SOLUTION FOUND'),nl. | |
| 1511 | ||
| 1512 | :- dynamic nr_cbc_sols/1. | |
| 1513 | nr_cbc_sols(0). | |
| 1514 | reset_nr_cbc_sols :- retractall(nr_cbc_sols(_)), assert(nr_cbc_sols(0)). | |
| 1515 | inc_nr_cbc_sols :- | |
| 1516 | retract(nr_cbc_sols(N)), N1 is N+1, assert(nr_cbc_sols(N1)). | |
| 1517 | extract_trans_id( (TransId,_,_,_), TransId). | |
| 1518 | print_trans( (_,Event,_,_)) :- translate_event(Event,S), print(S), print(' '). | |
| 1519 | check_valid_operation(Op) :- | |
| 1520 | (get_possible_language_specific_top_level_event(Op,_,_) -> true | |
| 1521 | ; add_error(cbc_find_sequence,'Unknown operation/event: ',Op),fail). | |
| 1522 | ||
| 1523 | ||
| 1524 | ||
| 1525 | % ------------ | |
| 1526 | ||
| 1527 | :- use_module(bsyntaxtree). | |
| 1528 | tcltk_constraint_find_valid_state_with_pred(ParameterBindList,RestPreCond,UseConstantsFromStateID) :- | |
| 1529 | parse_tclk_parameter_values_and_pred('$initialise_machine',ParameterBindList,RestPreCond,CustomPredicate), | |
| 1530 | UseInvariant=true, | |
| 1531 | call_cbc_command( | |
| 1532 | b_state_model_check:b_set_up_valid_state_with_pred(State,CustomPredicate, | |
| 1533 | UseInvariant,UseConstantsFromStateID)), | |
| 1534 | tcltk_add_cbc_state(State,find_valid_state). | |
| 1535 | tcltk_constraint_find_valid_state :- | |
| 1536 | call_cbc_command(b_set_up_valid_state(State)), | |
| 1537 | tcltk_add_cbc_state(State,find_valid_state). | |
| 1538 | ||
| 1539 | :- use_module(clpfd_interface,[catch_clpfd_overflow_call1/1]). | |
| 1540 | :- use_module(error_manager,[call_in_fresh_error_scope_for_one_solution/1]). | |
| 1541 | % catch CLPFD overflows and catch other errors | |
| 1542 | call_cbc_command(Command) :- | |
| 1543 | call_in_fresh_error_scope_for_one_solution( | |
| 1544 | (catch_clpfd_overflow_call1(Command) -> true | |
| 1545 | ; translate_events_in_current_scope_to_warnings(cbc,'Warning: '),fail | |
| 1546 | % Maybe we should raise error when Command fails and enumeration warnings are there ? | |
| 1547 | )). | |
| 1548 | ||
| 1549 | :- public tcltk_constraint_find_deadlock_state/1. | |
| 1550 | tcltk_constraint_find_deadlock_state(Res) :- | |
| 1551 | check_we_are_in_b_mode(cbc_deadlock_freedom_check), | |
| 1552 | create_texpr(truth,pred,[],True), | |
| 1553 | call_cbc_command(cbc_deadlock_freedom_check(State,True,0)), | |
| 1554 | (State == time_out -> Res = time_out | |
| 1555 | ; tcltk_add_cbc_state(State,cbc_deadlock), Res=deadlock). | |
| 1556 | :- public tcltk_constraint_find_deadlock_state_with_goal/2. | |
| 1557 | tcltk_constraint_find_deadlock_state_with_goal(Filter,Res) :- | |
| 1558 | check_we_are_in_b_mode(cbc_deadlock_freedom_check), | |
| 1559 | ( b_get_machine_goal(Goal) -> true | |
| 1560 | ; otherwise -> create_texpr(truth,pred,[],Goal)), | |
| 1561 | call_cbc_command(cbc_deadlock_freedom_check(State,Goal,Filter)), | |
| 1562 | (State == time_out -> Res = time_out | |
| 1563 | ; tcltk_add_cbc_state(State,cbc_deadlock), Res=deadlock). | |
| 1564 | ||
| 1565 | check_we_are_in_b_mode(_) :- b_or_z_mode,!. | |
| 1566 | check_we_are_in_b_mode(Cmd) :- add_error(check_we_are_in_b_mode,'This command can only be performed in B,Z or TLA+ mode: ',Cmd),fail. | |
| 1567 | ||
| 1568 | tcltk_constraint_find_deadlock_state_with_goal(true,_Filter,Res) :- | |
| 1569 | !,tcltk_constraint_find_deadlock_state(Res). | |
| 1570 | tcltk_constraint_find_deadlock_state_with_goal(GoalPred,Filter,Res) :- | |
| 1571 | bmachine:b_set_machine_goal(GoalPred), | |
| 1572 | tcltk_constraint_find_deadlock_state_with_goal(Filter,Res). | |
| 1573 | ||
| 1574 | :- use_module(enabling_analysis,[check_if_feasible_operation/5]). | |
| 1575 | tcltk_check_if_feasible_operation(OpName,UseInvariant,TimeOutFactor,Result) :- % UseInvariant currently always 1 from Tcl | |
| 1576 | check_if_feasible_operation(OpName,UseInvariant,TimeOutFactor,Result,ResultState), | |
| 1577 | tcltk_add_cbc_state(ResultState,feasibility_check(OpName)). | |
| 1578 | ||
| 1579 | tcltk_add_cbc_state('$UNKNOWN_STATE',_) :- !. | |
| 1580 | tcltk_add_cbc_state(State,OpName) :- | |
| 1581 | seperate_state_into_const_and_vars(State,Constants,Variables), | |
| 1582 | !, | |
| 1583 | % store the constants separately: important for memory consumption when continuing animation/model checking | |
| 1584 | tcltk_add_new_transition_transid(root,'$setup_constants',CstID,concrete_constants(Constants),[],TransId1), | |
| 1585 | FullState = const_and_vars(CstID,Variables), | |
| 1586 | tcltk_add_new_transition_transid(CstID,'$JUMP'(OpName),NewID,FullState,[],TransId2), | |
| 1587 | set_cbc_state(NewID,[TransId1,TransId2],[CstID,root]). | |
| 1588 | tcltk_add_cbc_state(State,OpName) :- | |
| 1589 | tcltk_add_new_transition_transid(root,'$JUMP'(OpName),NewID,State,[],TransId), | |
| 1590 | set_cbc_state(NewID,[TransId],[root]). | |
| 1591 | ||
| 1592 | set_cbc_state(NewID,TransIds,His) :- | |
| 1593 | retractall(current_state_id(_)), | |
| 1594 | assert(current_state_id(NewID)), | |
| 1595 | reset_op_trace_ids, | |
| 1596 | maplist(add_to_op_trace_ids,TransIds), | |
| 1597 | retractall(history(_)), | |
| 1598 | retractall(forward_history(_)), | |
| 1599 | assert(history(His)). %, print(State),nl. | |
| 1600 | ||
| 1601 | is_constant_binding(SortedCsts,bind(ID,_)) :- | |
| 1602 | ord_member(ID,SortedCsts). | |
| 1603 | ||
| 1604 | :- use_module(bsyntaxtree, [get_texpr_ids/2]). | |
| 1605 | seperate_state_into_const_and_vars(State,Constants,Variables) :- | |
| 1606 | b_get_machine_constants(TCs), get_texpr_ids(TCs,Cs), | |
| 1607 | sort(Cs,SortedCsts), | |
| 1608 | include(is_constant_binding(SortedCsts),State,Constants), | |
| 1609 | Constants \= [], | |
| 1610 | exclude(is_constant_binding(SortedCsts),State,Variables). | |
| 1611 | ||
| 1612 | ||
| 1613 | ||
| 1614 | :- public tcltk_constraint_find_static_assertion_violation/1. | |
| 1615 | tcltk_constraint_find_static_assertion_violation(TclResult) :- | |
| 1616 | cbc_constraint_find_static_assertion_violation(Result,[]), | |
| 1617 | functor(Result,TclResult,_). | |
| 1618 | cbc_constraint_find_static_assertion_violation(Result,Options) :- | |
| 1619 | call_cbc_command(cbc_static_assertions_check(State,Options)), | |
| 1620 | ( State = counterexample_found(CE) -> | |
| 1621 | Result = counterexample_found, | |
| 1622 | tcltk_add_cbc_state(CE,static_assertion_check) | |
| 1623 | ; otherwise -> | |
| 1624 | Result = State). | |
| 1625 | ||
| 1626 | /* --------------------------------------------------- */ | |
| 1627 | ||
| 1628 | ||
| 1629 | :- use_module(error_manager,[extract_all_line_col/5]). | |
| 1630 | :- use_module(probcspsrc(haskell_csp),[extract_span_from_event/4,extract_span_info/2]). | |
| 1631 | ||
| 1632 | get_source_text_positions(Event,Line,Col,EndLine,EndCol) :- | |
| 1633 | extract_span_from_action(Event,SPAN), | |
| 1634 | extract_all_line_col(SPAN,Line,Col,EndLine,EndCol). | |
| 1635 | ||
| 1636 | extract_span_from_action(Event,Span) :- csp_mode, | |
| 1637 | extract_span_from_event(Event,Span,_,_). | |
| 1638 | extract_span_from_action(Event,Pos) :- b_or_z_mode, | |
| 1639 | get_operation_name(Event,ID), | |
| 1640 | b_get_machine_operation(ID,_Res,_TParas,_Body,_OType,Pos). | |
| 1641 | ||
| 1642 | ||
| 1643 | /* -------------------------------------------------------------------- */ | |
| 1644 | ||
| 1645 | get_current_option_eventtrace(OptionNum,Trace) :- | |
| 1646 | % the option number starts with 0 (coming from a TK listbox) | |
| 1647 | current_options(ActionsAndIDs), | |
| 1648 | nth0(OptionNum,ActionsAndIDs,(Id,_,_,_)), | |
| 1649 | transition_info(Id,eventtrace(Trace)),!. | |
| 1650 | ||
| 1651 | :- public tcltk_has_eventtrace/1. | |
| 1652 | tcltk_has_eventtrace(OptionNum) :- | |
| 1653 | get_current_option_eventtrace(OptionNum,_Trace). | |
| 1654 | ||
| 1655 | :- public tcltk_show_eventtrace/2. | |
| 1656 | tcltk_show_eventtrace(OptionNum,Desc) :- | |
| 1657 | get_current_option_eventtrace(OptionNum,Trace), | |
| 1658 | explain_event_trace(Trace,Desc). | |
| 1659 | ||
| 1660 | ||
| 1661 | ||
| 1662 | /* --------------------------------------------------- */ | |
| 1663 | ||
| 1664 | :- use_module(prob2_interface,[execute_model/5]). | |
| 1665 | ||
| 1666 | tcltk_execute_model(MaxNrSteps,ExecutedSteps,Result) :- | |
| 1667 | current_state_id(CurID), | |
| 1668 | execute_model(CurID,MaxNrSteps,_TransitionInfo,ExecutedSteps,Result). | |
| 1669 | ||
| 1670 | ||
| 1671 | :- public tcltk_find_shortest_trace_to_current_node/1. | |
| 1672 | tcltk_find_shortest_trace_to_current_node(list(StringList)) :- | |
| 1673 | find_trace_to_current_node(OpL), | |
| 1674 | translate_events(OpL,StringList). | |
| 1675 | ||
| 1676 | :- public tcltk_execute_trace_to_current_node/0. | |
| 1677 | tcltk_execute_trace_to_current_node :- | |
| 1678 | current_state_id(CurID), | |
| 1679 | tcltk_execute_trace_to_node(CurID). | |
| 1680 | ||
| 1681 | tcltk_execute_trace_to_node(ToID) :- /* can be useful for TestCase Generation */ | |
| 1682 | set_target_id(ToID), | |
| 1683 | tcltk_execute_trace_from_to_found_predicate(root,_,_). | |
| 1684 | ||
| 1685 | tcltk_execute_trace_from_to_found_predicate(From,OpL,IDList) :- | |
| 1686 | printsilent(finding_trace_from_to(From)),nls, flush_output(user), | |
| 1687 | find_shortest_path_from_to_found_predicate(From,OpL,IDList,ToID), !, | |
| 1688 | /* mal: replaced by shortest 5/12/2006 */ | |
| 1689 | (current_state_id(From) -> true ; state_space_reset), | |
| 1690 | debug_println(9,executing_trace(From,OpL,ToID)), flush_output(user), | |
| 1691 | execute_id_trace_from_current(ToID,OpL,IDList). | |
| 1692 | % print(executing_trace_to(ID,OpL,IDList)),nl, | |
| 1693 | %compute_history(OpL,IDList,History), print(new_history(History)),nl, | |
| 1694 | ||
| 1695 | ||
| 1696 | find_trace_to_current_node(Trace) :- | |
| 1697 | current_state_id(CurID), | |
| 1698 | find_shortest_path_from_to(root,CurID,L,_), | |
| 1699 | extract_term_trace_from_transition_ids(L,Trace). | |
| 1700 | ||
| 1701 | :- use_module(state_space_dijkstra). | |
| 1702 | ||
| 1703 | find_shortest_trace_to_node(FromID,ToID,OpIDListe,StateIDList) :- | |
| 1704 | find_shortest_path_from_to(FromID,ToID,OpIDListe,StateIDList). | |
| 1705 | ||
| 1706 | ||
| 1707 | /* --------------------------------------------------- */ | |
| 1708 | ||
| 1709 | ||
| 1710 | ||
| 1711 | :- public tcltk_goto_a_non_deterministic_node/0. | |
| 1712 | tcltk_goto_a_non_deterministic_node :- /* same transition leads to different resulting state */ | |
| 1713 | transition(ID,X,ID2), | |
| 1714 | transition(ID,X,ID3), dif_ID(ID2,ID3), | |
| 1715 | print_message(found_non_det_op(X)), | |
| 1716 | %tcltk_goto_state(find_non_det_node,ID). | |
| 1717 | tcltk_execute_trace_to_node(ID). | |
| 1718 | ||
| 1719 | dif_ID(ID1,ID2) :- (number(ID1),number(ID2) -> ID2>ID1 ; ID1 \= ID2). | |
| 1720 | ||
| 1721 | :- public tcltk_goto_a_branching_node/0. | |
| 1722 | tcltk_goto_a_branching_node :- /* two different events/operations enabled */ | |
| 1723 | transition(ID,X,ID2), get_operation_name(X,NX), | |
| 1724 | transition(ID,Y,ID3), dif_ID(ID2,ID3), get_operation_name(Y,NY), NX\=NY, | |
| 1725 | print_message(found_branching_op(ID,NX,NY)), | |
| 1726 | %tcltk_goto_state(find_branching_node,ID), | |
| 1727 | tcltk_execute_trace_to_node(ID). | |
| 1728 | ||
| 1729 | :- public tcltk_goto_a_non_resetable_node/0. | |
| 1730 | tcltk_goto_a_non_resetable_node :- | |
| 1731 | find_resetable_nodes, | |
| 1732 | visited_expression_id(ID), | |
| 1733 | \+(resetable_node(ID)), | |
| 1734 | \+(not_all_transitions_added(ID)), !, | |
| 1735 | %tcltk_goto_state(find_non_resetable_node,ID). | |
| 1736 | tcltk_execute_trace_to_node(ID). | |
| 1737 | ||
| 1738 | operation_name_covered(OpName) :- operation_name_covered(OpName,_). | |
| 1739 | operation_name_covered(OpName,Template) :- b_get_machine_operation(OpName,Results,Par,_), | |
| 1740 | \+ operation_not_yet_covered(OpName), | |
| 1741 | length(Par,Arity), | |
| 1742 | functor(Op,OpName,Arity), | |
| 1743 | (Results\=[] -> Template = '-->'(Op,_) ; Template = Op). | |
| 1744 | ||
| 1745 | :- public tcltk_goto_event_list_property_violation/3. | |
| 1746 | tcltk_goto_event_list_property_violation(Property,EventSelection,list(OperationList)) :- | |
| 1747 | % first translate Tk EventSelection Number list into Events | |
| 1748 | sap:get_selected_events(EventSelection,_AllEvents,OperationList), | |
| 1749 | include(operation_name_covered,OperationList,_,EnabledOpList), % only keep operations that can be enabled anyway | |
| 1750 | maplist(operation_name_covered,EnabledOpList,TemplateList), % replace by template | |
| 1751 | print(find_property_violation_for_template(Property,TemplateList)),nl, | |
| 1752 | visited_expression(ID,S), ID \= root, S\= concrete_constants(_), | |
| 1753 | \+(not_all_transitions_added(ID)), | |
| 1754 | \+( check_event_list_property(Property,ID,TemplateList) ), | |
| 1755 | print(found_event_list_property_violation(Property,ID)),nl, | |
| 1756 | tcltk_execute_trace_to_node(ID). | |
| 1757 | ||
| 1758 | check_event_list_property(relative_deadlock_freedom,ID,TemplateList) :- | |
| 1759 | relative_deadlock_freedom(ID,TemplateList). | |
| 1760 | check_event_list_property(valid_controller,ID,TemplateList) :- | |
| 1761 | is_valid_controller_state(ID,TemplateList). | |
| 1762 | check_event_list_property(det_controller,ID,TemplateList) :- | |
| 1763 | is_det_controller_state(ID,TemplateList). | |
| 1764 | ||
| 1765 | relative_deadlock_freedom(ID,TemplateList) :- member(Template,TemplateList), | |
| 1766 | transition(ID,Template,_). | |
| 1767 | is_valid_controller_state(ID,TemplateList) :- % check that exactly one event from TemplateList is enabled | |
| 1768 | append(_,[LiveEvent|RestTemplate],TemplateList), | |
| 1769 | transition(ID,LiveEvent,_),!, % we found one enabled event | |
| 1770 | \+ relative_deadlock_freedom(ID,RestTemplate). % all other events from list must be disabled | |
| 1771 | is_det_controller_state(ID,TemplateList) :- % check that *at most* one event from TemplateList is enabled | |
| 1772 | append(_,[LiveEvent|RestTemplate],TemplateList), | |
| 1773 | transition(ID,LiveEvent,_),!, % we found one enabled event from list | |
| 1774 | \+ relative_deadlock_freedom(ID,RestTemplate). % all other events from list must be disabled | |
| 1775 | is_det_controller_state(_,_) :- true. % no event enabled is also ok | |
| 1776 | ||
| 1777 | :- public tcltk_goto_state_enabling_operation/2. | |
| 1778 | tcltk_goto_state_enabling_operation(TclOpName,FromCurrent) :- | |
| 1779 | predicate_debugger:adapt_tcl_operation_name(TclOpName,OpName), | |
| 1780 | operation_name_covered(OpName,Template), | |
| 1781 | set_found_predicate(ID, transition(ID,Template,_)), | |
| 1782 | print(template(Template,FromCurrent)),nl, | |
| 1783 | print_message('Computing trace to node'), | |
| 1784 | (FromCurrent=1 | |
| 1785 | -> current_state_id(FromID) % inefficient: better to do one dijkstra from FromID ! | |
| 1786 | ; FromID = root | |
| 1787 | ), | |
| 1788 | tcltk_execute_trace_from_to_found_predicate(FromID,_,_). | |
| 1789 | % tcltk_goto_state(find_enabled(OpName),ID). | |
| 1790 | ||
| 1791 | :- public tcltk_operations_covered_info/2. | |
| 1792 | % quickly compute which operations have already been covered and which ones not | |
| 1793 | tcltk_operations_covered_info(list([list(['Operation','Covered'])|OpCov]),Precise) :- | |
| 1794 | findall(list([OpName,Cov]), | |
| 1795 | (specfile:get_possible_event(OpName), | |
| 1796 | (operation_name_not_yet_covered(OpName) | |
| 1797 | -> not_yet_covered_info(Precise,OpName,Cov) | |
| 1798 | ; Cov = 'yes')),OpCov). | |
| 1799 | ||
| 1800 | not_yet_covered_info(precise,OpName,Cov) :- | |
| 1801 | enabling_analysis:feasible_operation(OpName,Res),!, Res=Cov. | |
| 1802 | not_yet_covered_info(precise,_,R) :- !, R='unknown'. | |
| 1803 | not_yet_covered_info(_,_,'uncovered'). | |
| 1804 | ||
| 1805 | :- dynamic resetable_node/1. | |
| 1806 | ||
| 1807 | resetable_node(a). | |
| 1808 | ||
| 1809 | :- public find_resetable_nodes/0. | |
| 1810 | :- dynamic find_flag/2. | |
| 1811 | find_resetable_nodes :- | |
| 1812 | retractall(find_flag(_,_)), | |
| 1813 | retractall(resetable_node(_)), | |
| 1814 | any_transition(root,_,ID), /* add nodes reachable from root */ | |
| 1815 | assert(find_flag(ID,0)), | |
| 1816 | fail. | |
| 1817 | find_resetable_nodes :- | |
| 1818 | visited_expression(CID,concrete_constants(_C)), | |
| 1819 | any_transition(CID,_,ID), /* add nodes reachable after a setup_constants */ | |
| 1820 | assert(find_flag(ID,0)), | |
| 1821 | fail. | |
| 1822 | find_resetable_nodes :- find_resetable_nodes_loop, | |
| 1823 | print_message('Not resetable:'), | |
| 1824 | visited_expression_id(ID), | |
| 1825 | \+(resetable_node(ID)), | |
| 1826 | print_message(ID), | |
| 1827 | fail. | |
| 1828 | find_resetable_nodes :- | |
| 1829 | print_message('Done'). | |
| 1830 | ||
| 1831 | ||
| 1832 | find_resetable_nodes_loop :- | |
| 1833 | retract(find_flag(ID,N)), !, find_resetable_nodes_loop(ID,N). | |
| 1834 | find_resetable_nodes_loop. | |
| 1835 | ||
| 1836 | find_resetable_nodes_loop(ID,N) :- N1 is N+1, | |
| 1837 | assert(resetable_node(ID)), | |
| 1838 | any_transition(NewID,_,ID), | |
| 1839 | \+(resetable_node(NewID)), | |
| 1840 | \+(find_flag(NewID,_)), | |
| 1841 | assert(find_flag(NewID,N1)), | |
| 1842 | fail. | |
| 1843 | find_resetable_nodes_loop(_,_) :- find_resetable_nodes_loop. | |
| 1844 | ||
| 1845 | ||
| 1846 | :- use_module(bmachine, [determine_type_of_formula/2]). | |
| 1847 | :- public tcltk_show_expression_as_dot/2. | |
| 1848 | tcltk_show_expression_as_dot(VorE,File) :- | |
| 1849 | parse_machine_expression(VorE,TypedExpr), | |
| 1850 | tcltk_show_typed_expression_as_dot_graph(TypedExpr,File). | |
| 1851 | tcltk_show_expression_as_dot(_VorE,File) :- | |
| 1852 | add_error(tcltk_show_expression_as_dot,'Computing Value Dot Representation Failed for: ',File), | |
| 1853 | fail. | |
| 1854 | ||
| 1855 | tcltk_show_typed_expression_as_dot_graph(TypedExpr,File) :- | |
| 1856 | determine_type_of_formula(TypedExpr,Type), | |
| 1857 | get_state(Type,BState), | |
| 1858 | decompose_expression_for_dot(TypedExpr,ExprList,[]), % decompose pairs so that user can provide multiple values/graphs | |
| 1859 | compute_for_dot(ExprList,BState,GraphState), % compute value for each sub-component | |
| 1860 | format('Writing value to DOT file: ~w~n',[File]), | |
| 1861 | graph_canon:print_cstate_graph(GraphState,File), | |
| 1862 | format('Finished writing value to DOT file: ~w~n',[File]). | |
| 1863 | ||
| 1864 | get_state(requires_nothing,[]). | |
| 1865 | get_state(requires_constants,BState) :- | |
| 1866 | current_expression(_CurID,State), | |
| 1867 | (state_corresponds_to_set_up_constants(State,BState) -> true ; | |
| 1868 | add_error(tcltk_show_expression_as_dot,'Please setup constants or initialise machine first: '),fail). | |
| 1869 | get_state(requires_variables,BState) :- | |
| 1870 | current_expression(_CurID,State), | |
| 1871 | (state_corresponds_to_initialised_b_machine(State,BState) -> true ; | |
| 1872 | add_error(tcltk_show_expression_as_dot,'Please initialise machine first: '),fail). | |
| 1873 | ||
| 1874 | :- use_module(bmachine, [b_parse_machine_expression_from_codes_with_prob_ids/2, type_with_errors/4]). | |
| 1875 | parse_machine_expression(RawAST,TypedExpr) :- compound(RawAST),!, % allow to pass raw AST as well | |
| 1876 | type_with_errors(RawAST,[prob_ids(visible),variables],Type,TypedExpr), | |
| 1877 | ((Type=pred ; Type=subst) | |
| 1878 | -> add_error(state_space_reduction,'Expected expression formula but obtained: ',Type),fail | |
| 1879 | ; true ). | |
| 1880 | parse_machine_expression(VorE,TypedExpr) :- | |
| 1881 | atom_codes(VorE,VorECodes), | |
| 1882 | b_parse_machine_expression_from_codes_with_prob_ids(VorECodes,TypedExpr). | |
| 1883 | ||
| 1884 | compute_for_dot([],_,[]). | |
| 1885 | compute_for_dot([String,TypedExpr|Tail],BState,[bind(Str,Value)|TS]) :- | |
| 1886 | % allow user to specify labels for graphs ("lbl1", e1, "lbl2", e2, ...) | |
| 1887 | get_texpr_expr(String,string(Str)),!, | |
| 1888 | translate:translate_bexpression_with_limit(TypedExpr,100,EStr), | |
| 1889 | format('Computing value for expression: ~w~n',[EStr]), | |
| 1890 | b_compute_expression_with_prob_ids(TypedExpr,BState,Value), | |
| 1891 | compute_for_dot(Tail,BState,TS). | |
| 1892 | compute_for_dot([TypedExpr|Tail],BState,[bind(Str,Value)|TS]) :- | |
| 1893 | translate:translate_bexpression_with_limit(TypedExpr,100,Str), | |
| 1894 | format('Computing value for expression: ~w~n',[Str]), | |
| 1895 | b_compute_expression_with_prob_ids(TypedExpr,BState,Value), | |
| 1896 | compute_for_dot(Tail,BState,TS). | |
| 1897 | ||
| 1898 | ||
| 1899 | ||
| 1900 | decompose_expression_for_dot(b(couple(A,B),_,_)) --> !, | |
| 1901 | decompose_expression_for_dot(A), decompose_expression_for_dot(B). | |
| 1902 | decompose_expression_for_dot(b(rec(Fields),_,_)) --> !,decompose_fields_for_dot(Fields). | |
| 1903 | decompose_expression_for_dot(X) --> [X]. | |
| 1904 | ||
| 1905 | decompose_fields_for_dot([]) --> []. | |
| 1906 | decompose_fields_for_dot([field(Name,Val)|T]) --> [b(string(Name),string,[]),Val], decompose_fields_for_dot(T). | |
| 1907 | ||
| 1908 | /* ------------------------------------------------------------------ */ | |
| 1909 | ||
| 1910 | ||
| 1911 | ||
| 1912 | print_property_partitions :- print('PARTITIONS OF PROPERTIES'),nl, | |
| 1913 | b_interpreter:b_get_properties_from_machine(Properties), | |
| 1914 | bsyntaxtree:predicate_components(Properties,Comp), | |
| 1915 | length(Comp,Len), print(Len), print(' partitions found'),nl, | |
| 1916 | member(component(P,Vars),Comp), nl,print(Vars),nl,translate:print_bexpr(P),nl,fail. | |
| 1917 | print_property_partitions :- nl, print(' ============== '),nl. | |
| 1918 | ||
| 1919 | :- public tcltk_add_user_executed_operation/2. | |
| 1920 | tcltk_add_user_executed_operation(TclOpName,CustomPredicate) :- | |
| 1921 | tcltk_add_user_executed_operation(TclOpName,[],CustomPredicate). | |
| 1922 | ||
| 1923 | tcltk_add_user_executed_operation(TclOpName,ParameterBindList,RestPreCond) :- | |
| 1924 | predicate_debugger:adapt_tcl_operation_name(TclOpName,OpName), | |
| 1925 | parse_tclk_parameter_values_and_pred(OpName,ParameterBindList,RestPreCond,CustomPredicate), | |
| 1926 | b_trans_one_solution_with_pred(OpName,CustomPredicate,_,_). | |
| 1927 | ||
| 1928 | parse_tclk_parameter_values_and_pred(OpName,ParameterBindList,RestPreCond,CustomPredicate) :- | |
| 1929 | b_parse_machine_operation_pre_post_predicate(RestPreCond,RestTypedPred,OpName), | |
| 1930 | get_animation_operation_parameters(OpName,Parameters), | |
| 1931 | % print(tcltk_add_user_executed_operation(OpName,ParameterBindList,Parameters)),nl, | |
| 1932 | parse_parameter_values(ParameterBindList,Parameters,List), | |
| 1933 | conjunct_predicates([RestTypedPred|List],CustomPredicate). | |
| 1934 | ||
| 1935 | get_animation_operation_parameters('$setup_constants',Parameters) :- | |
| 1936 | b_get_machine_operation_typed_parameters('$setup_constants',Parameters). | |
| 1937 | get_animation_operation_parameters(OpName,FullParameters) :- | |
| 1938 | b_get_machine_operation_for_animation(OpName,_Results,Parameters,_Body,_OType,_TopLevel), | |
| 1939 | b_get_operation_non_det_modifies(OpName,NonDetVars), % also allow setting non-deterministically assigned vars | |
| 1940 | b_get_machine_variables(Vars), | |
| 1941 | include(non_det_modified(NonDetVars),Vars,ParaVars), | |
| 1942 | append(ParaVars,Parameters,FullParameters). | |
| 1943 | ||
| 1944 | non_det_modified(NonDetVars,TID) :- get_texpr_id(TID,ID), ord_member(ID,NonDetVars). | |
| 1945 | ||
| 1946 | % parse a list of variable names and expressions and turn into equal predicates | |
| 1947 | % Motivation: this can also deal with Z-style identifiers like in?, ... which cannot be parsed | |
| 1948 | :- use_module(btypechecker, [unify_types_strict/2]). | |
| 1949 | parse_parameter_values([],_,Res) :- !,Res=[]. | |
| 1950 | parse_parameter_values(['='(ParameterID,ExpressionStr)|T],Parameters,[Pred|PT]) :- | |
| 1951 | atom_codes(ExpressionStr,Codes), | |
| 1952 | format('Parsing for ~w : ~w~n',[ParameterID,ExpressionStr]), | |
| 1953 | !, | |
| 1954 | b_parse_machine_expression_from_codes_with_prob_ids(Codes,TypedExpr), | |
| 1955 | get_texpr_type(TypedExpr,Type), | |
| 1956 | TID = b(identifier(ParameterID),Type,[]), | |
| 1957 | (member(b(identifier(ParameterID),Type2,_),Parameters) | |
| 1958 | -> (unify_types_strict(Type,Type2) | |
| 1959 | -> Pred = b(equal(TID,TypedExpr),pred,[]), | |
| 1960 | translate:print_bexpr(Pred),nl, | |
| 1961 | parse_parameter_values(T,Parameters,PT) | |
| 1962 | ; | |
| 1963 | pretty_type(Type,String1), pretty_type(Type2,String2), | |
| 1964 | ajoin(['Value for parameter ',ParameterID,' has unexpected type ',String1,', expected: '],Msg), | |
| 1965 | add_error(parse_parameter_values,Msg,String2), | |
| 1966 | fail | |
| 1967 | ) | |
| 1968 | ; add_error(parse_parameter_values,'Unknown operation parameter: ',ParameterID), | |
| 1969 | fail). | |
| 1970 | parse_parameter_values(PB,P,_) :- add_internal_error('Illegal parameter binding: ',parse_parameter_values(PB,P,_)),fail. | |
| 1971 | ||
| 1972 | ||
| 1973 | :- public tcltk_add_user_executed_operation_typed/3. | |
| 1974 | % just as above but with typed predicate | |
| 1975 | tcltk_add_user_executed_operation_typed(OpName,TypedCustomPredicate,NewID) :- | |
| 1976 | tcltk_add_user_executed_operation_typed(OpName,_,TypedCustomPredicate,NewID). | |
| 1977 | tcltk_add_user_executed_operation_typed(OpName,Operation,TypedCustomPredicate,NewID) :- | |
| 1978 | b_trans_one_solution_with_pred(OpName,TypedCustomPredicate,Operation,NewID). | |
| 1979 | ||
| 1980 | b_trans_one_solution_with_pred(OpName,TypedCustomPredicate,Operation,NewID) :- | |
| 1981 | call_cleanup(b_trans_one_solution_with_pred2(OpName,TypedCustomPredicate,Operation,NewID), | |
| 1982 | bmachine:reset_temp_predicate). | |
| 1983 | ||
| 1984 | % find one solution from current state using OpName and respecting temp_predicate | |
| 1985 | b_trans_one_solution_with_pred2(OpName,TypedCustomPredicate,Operation,NewID) :- | |
| 1986 | b_top_level_operation(OpName), | |
| 1987 | !, | |
| 1988 | current_expression(CurID,InState), | |
| 1989 | set_context_state(CurID), | |
| 1990 | call_cleanup(execute_operation_by_predicate_in_state(InState,OpName,TypedCustomPredicate,Operation,NewState), | |
| 1991 | clear_context_state), | |
| 1992 | !, | |
| 1993 | debug_format(19,'Executed by predicate: ~w~n',[OpName]), | |
| 1994 | %debug_format(19,'Executed ~w: ~w~nOut=~w~n',[OpName,Operation,NewState]), | |
| 1995 | add_trans_id(CurID,Operation,NewState,[],NewID,[],_TransId), | |
| 1996 | tcltk_goto_state(Operation,NewID). | |
| 1997 | b_trans_one_solution_with_pred2(OpName,TypedCustomPredicate,Operation,NewID) :- | |
| 1998 | bmachine:assert_temp_typed_predicate(TypedCustomPredicate), | |
| 1999 | current_expression(CurID,InState), | |
| 2000 | set_context_state(CurID), | |
| 2001 | temporary_set_preference(maxNrOfEnablingsPerOperation,1,Max), | |
| 2002 | temporary_set_preference(maxNrOfInitialisations,1,MaxI), | |
| 2003 | start_ms_timer(Timer), | |
| 2004 | call_cleanup((specfile:b_trans(InState,OpName,Operation,NewState,TransInfo) -> true), | |
| 2005 | (stop_ms_timer(Timer), | |
| 2006 | reset_temporary_preference(maxNrOfEnablingsPerOperation,Max), | |
| 2007 | reset_temporary_preference(maxNrOfInitialisations,MaxI), | |
| 2008 | clear_context_state) | |
| 2009 | ), | |
| 2010 | debug_println(9,found_solution(NewState)),nl, | |
| 2011 | % now add a transition to the state space: | |
| 2012 | Residue=[], | |
| 2013 | add_trans_id(CurID,Operation,NewState,Residue,NewID,TransInfo,_), | |
| 2014 | tcltk_goto_state(Operation,NewID). | |
| 2015 | ||
| 2016 | % allow user to execute any statement | |
| 2017 | % TO DO: catch operation_calls and route them differently | |
| 2018 | % translate operation_call arguments into predicate and call tcltk_add_user_executed_operation_typed(OpName,Operation,TypedCustomPredicate,NewID) | |
| 2019 | tcltk_add_user_executed_statement(Statement,Updates,NewID) :- | |
| 2020 | current_expression(CurID,InState), | |
| 2021 | state_corresponds_to_initialised_b_machine(InState,BState), | |
| 2022 | set_context_state(CurID), | |
| 2023 | %start_ms_timer(Timer), | |
| 2024 | call_cleanup((user:b_full_execute_top_level_statement_with_probids(Statement,BState,Updates,NewState)->true), | |
| 2025 | clear_context_state), | |
| 2026 | % TO DO: do we need to catch enumeration warnings ? | |
| 2027 | %stop_ms_timer(Timer), | |
| 2028 | Residue=[], TransInfo = [], | |
| 2029 | debug_println(4,executed(Updates,NewState)), | |
| 2030 | compute_all_transitions_if_necessary(CurID), % first ensure we have already computed outgoing transitions as usual, so that we can detect if a new state is added | |
| 2031 | (get_id_of_node_and_add_if_required(NewState,NewID,Exists,CurID), | |
| 2032 | Exists=exists, | |
| 2033 | transition(CurID,Action,TransId,NewID) | |
| 2034 | -> debug_println(4,transition_exists_already(Action,TransId)) | |
| 2035 | ; translate:translate_substitution(Statement,OpLabel), | |
| 2036 | add_trans_id(CurID,'$USER'(OpLabel),NewState,Residue,NewID,TransInfo,_), | |
| 2037 | format('Added new user-initiated transition to ~w via: ~w~n',[NewID,OpLabel]) | |
| 2038 | ), | |
| 2039 | tcltk_goto_state(OpLabel,NewID). | |
| 2040 | ||
| 2041 | :- use_module(kernel_waitflags,[init_wait_flags/1, ground_wait_flags/1]). | |
| 2042 | %% allows one to execute any statement (not just operations). | |
| 2043 | b_full_execute_top_level_statement_with_probids(Body,InState,Updates,NewState) :- | |
| 2044 | add_prob_deferred_set_elements_to_store(InState,InState1,visible), | |
| 2045 | init_wait_flags(WF), | |
| 2046 | b_execute_top_level_statement(Body,[],InState1,Updates,WF,_Path1,output_not_required), | |
| 2047 | ground_wait_flags(WF), | |
| 2048 | store:store_updates_and_normalise(Updates,InState,NewState). | |
| 2049 | ||
| 2050 | % -------------------------------------------------------------------------------------- | |
| 2051 | ||
| 2052 | ||
| 2053 | :- use_module(bmachine). | |
| 2054 | :- use_module(specfile). | |
| 2055 | :- use_module(tools). | |
| 2056 | :- use_module(library(lists)). | |
| 2057 | :- use_module(store). | |
| 2058 | :- use_module(self_check). | |
| 2059 | :- use_module(b_global_sets). | |
| 2060 | :- use_module(translate). | |
| 2061 | :- use_module(predicate_debugger). | |
| 2062 | ||
| 2063 | ||
| 2064 | /* --------------------------------------------------------- */ | |
| 2065 | /* --------------------------------------------------------- */ | |
| 2066 | ||
| 2067 | ||
| 2068 | /* ----------------------------------*/ | |
| 2069 | /* b_analyse_conjunction */ | |
| 2070 | /* ----------------------------------*/ | |
| 2071 | ||
| 2072 | :- public tcltk_analyse_option/2. | |
| 2073 | /* provide list of possible options for analysis */ | |
| 2074 | tcltk_analyse_option(invariant,'INVARIANT') :- b_or_z_mode. | |
| 2075 | tcltk_analyse_option(properties,S) :- b_or_z_mode, | |
| 2076 | get_specification_description(properties,S). | |
| 2077 | tcltk_analyse_option(assertions,S) :- (b_or_z_mode ; csp_mode), | |
| 2078 | get_specification_description(assertions,S). | |
| 2079 | tcltk_analyse_option(deadlock,'DEADLOCKED') :- b_or_z_mode. | |
| 2080 | ||
| 2081 | :- public tcltk_analyse/6. | |
| 2082 | :- use_module(predicate_evaluator). | |
| 2083 | /* perform the various analysis */ | |
| 2084 | tcltk_analyse(Mode,Type,ListWithResults,Total,False,Unknown) :- | |
| 2085 | (Mode == unicode | |
| 2086 | -> set_unicode_mode, | |
| 2087 | call_cleanup(tcltk_analyse2(Type,ListWithResults,Summary),unset_unicode_mode) | |
| 2088 | ; tcltk_analyse2(Type,ListWithResults,Summary)), | |
| 2089 | (member(total/Total,Summary) -> true ; Total=0), | |
| 2090 | (member(false/False,Summary) -> true ; False=0), | |
| 2091 | (member(unknown/Unknown,Summary) -> true ; Unknown=0). | |
| 2092 | tcltk_analyse2(invariant,L,Summary) :- !,tcltk_analyse_invariant(L,Summary). | |
| 2093 | tcltk_analyse2(properties,L,Summary) :- !,tcltk_analyse_properties(L,Summary). | |
| 2094 | tcltk_analyse2(assertions,L,Summary) :- !,tcltk_analyse_assertions(L,Summary). | |
| 2095 | tcltk_analyse2(deadlock,L,Summary) :- !,tcltk_analyse_deadlock(L,Summary). | |
| 2096 | tcltk_analyse2(X,L,Summary) :- add_error(tcltk_analyse, 'Unknown type of formula: ', X), | |
| 2097 | L=[], Summary=[]. | |
| 2098 | ||
| 2099 | ||
| 2100 | /* --------------------------------- */ | |
| 2101 | ||
| 2102 | :- public tcltk_show_current_state/1. | |
| 2103 | tcltk_show_current_state(TransBState) :- | |
| 2104 | current_b_expression(B), | |
| 2105 | mnf(translate_bstate(B,TransBState)). | |
| 2106 | ||
| 2107 | :- public tcltk_show_typing_of_variables_and_constants/1. | |
| 2108 | tcltk_show_typing_of_variables_and_constants(list(List)) :- | |
| 2109 | b_get_machine_variables(TypedVarList), | |
| 2110 | convert_typed_varlist(TypedVarList,VarList,Types), | |
| 2111 | generate_typing_list(VarList,Types,VList,VarCard), | |
| 2112 | length(VarList,NrVars), | |
| 2113 | format_to_codes(' VARIABLES [nr=~w,card=~w]',[NrVars,VarCard],Codes1),atom_codes(VARAtom,Codes1), | |
| 2114 | ||
| 2115 | b_get_machine_all_constants(TypedCstList), | |
| 2116 | convert_typed_varlist(TypedCstList,CVarList,CTypes), | |
| 2117 | find_non_det_constants, | |
| 2118 | generate_typing_list(CVarList,CTypes,CList,CCard), | |
| 2119 | ( CList = [] | |
| 2120 | -> List = [VARAtom|VList] | |
| 2121 | ; length(CVarList,NrCsts), | |
| 2122 | format_to_codes(' CONSTANTS [nr=~w,card=~w]',[NrCsts,CCard],Codes2),atom_codes(CstAtom,Codes2), | |
| 2123 | append([CstAtom|CList],[VARAtom|VList],List) | |
| 2124 | ),!. | |
| 2125 | tcltk_show_typing_of_variables_and_constants(list(['TYPE ERROR in MACHINE'])). | |
| 2126 | ||
| 2127 | :- public tcltk_get_constants_predicate/2. | |
| 2128 | %%% Used to get the constant values for the currently loaded B machine in form of a B predicate. | |
| 2129 | %%% In case that the constants in the model has not been set up then all possible constants' | |
| 2130 | %%% evaluations will be provided in form of a predicate in Disjunctive Normal Form. | |
| 2131 | %%% Predicate used for setting up constants when model checking with TLC. (TLA) | |
| 2132 | tcltk_get_constants_predicate(P,N) :- | |
| 2133 | current_state_id(CurID), | |
| 2134 | (CurID==root | |
| 2135 | -> get_constants_as_disjoint_predicate(N,P) | |
| 2136 | ; prob2_interface:get_state(CurID,EState), | |
| 2137 | filter_constants_bindings(EState,X), % this will only get current constants values | |
| 2138 | translate: translate_bstate(X,P) | |
| 2139 | ). | |
| 2140 | ||
| 2141 | get_constants_as_disjoint_predicate(N,Res) :- | |
| 2142 | findall(R,get_set_up_constants_solution(R),L), | |
| 2143 | get_a_part_of_the_found_solutions(L,N,Part), | |
| 2144 | add_or_between_constant_predicates(Part,Res). | |
| 2145 | ||
| 2146 | get_a_part_of_the_found_solutions(L,N,Part) :- | |
| 2147 | length(L,Length), | |
| 2148 | (N>=Length | |
| 2149 | -> Part=L | |
| 2150 | ; sublist(L,Part,_B,N,_A)). | |
| 2151 | ||
| 2152 | ||
| 2153 | get_set_up_constants_solution(R) :- | |
| 2154 | %\+ max_reached_or_timeout_for_node(root),!, % then lookup constants rather than computing them | |
| 2155 | transition(root,_,Dst), | |
| 2156 | visited_expression(Dst,concrete_constants(X)), | |
| 2157 | translate:translate_bstate(X,R). | |
| 2158 | %get_set_up_constants_solution(R) :- | |
| 2159 | % b_interpreter: b_set_up_concrete_constants(X), | |
| 2160 | % translate:translate_bstate(X,R). | |
| 2161 | ||
| 2162 | add_or_between_constant_predicates([],'1=1'). | |
| 2163 | add_or_between_constant_predicates(L,Res) :- | |
| 2164 | tools: ajoin_with_sep(L,' or ',Res). | |
| 2165 | ||
| 2166 | filter_constants_bindings(EState,R) :- | |
| 2167 | b_get_machine_all_constants(C), | |
| 2168 | convert_typed_varlist(C,CVarList,_CTypes), | |
| 2169 | filter_constants_bindings1(EState,CVarList,R). | |
| 2170 | ||
| 2171 | filter_constants_bindings1([],_,[]). | |
| 2172 | filter_constants_bindings1([bind(Ident,Val)|T],CVarList,Res) :- | |
| 2173 | (member(Ident,CVarList) -> Res = [bind(Ident,Val)|Rest]; Res = Rest), | |
| 2174 | filter_constants_bindings1(T,CVarList,Rest). | |
| 2175 | ||
| 2176 | convert_typed_varlist([],[],[]). | |
| 2177 | convert_typed_varlist([b(identifier(ID),Type,_)|T],[ID|IT],[Type|TT]) :- | |
| 2178 | %print(ID), print(' : '), print(Type),nl, | |
| 2179 | % db : set(couple(global(Name),global(Code))) a : set(integer) boolean | |
| 2180 | convert_typed_varlist(T,IT,TT). | |
| 2181 | %-------------------------------------- | |
| 2182 | ||
| 2183 | ||
| 2184 | :- use_module(symmetry_marker,[type_allows_for_precise_marker/1]). | |
| 2185 | :- use_module(bmachine,[b_is_unused_constant/1]). | |
| 2186 | :- use_module(library(codesio),[format_to_codes/3]). | |
| 2187 | generate_typing_list([],[],[],1). | |
| 2188 | generate_typing_list([Var|VT],[BasicType|TT],[Translation|Rest],TotCard) :- | |
| 2189 | pretty_type(BasicType,PrettyType), | |
| 2190 | (kernel_objects:max_cardinality(BasicType,Card) -> true ; Card='??'), | |
| 2191 | (b_get_constant_represented_inside_global_set(Var,BasicType) | |
| 2192 | -> Imp='(treated as enumerated) ' | |
| 2193 | ; (preference(symmetry_mode,hash), | |
| 2194 | \+type_allows_for_precise_marker(BasicType)) | |
| 2195 | -> Imp = '(IMPRECISE for HASH) ' | |
| 2196 | ; Imp = '' | |
| 2197 | ), | |
| 2198 | (non_det_constant(Var) | |
| 2199 | -> MulSol ='[multiple solutions in SETUP_CONSTANTS]' | |
| 2200 | ; MulSol=''), | |
| 2201 | (b_is_unused_constant(Var) -> Unused=' (unused)' ; Unused=''), | |
| 2202 | % mnf(translate:translate_bexpression(b(member(identifier(Var),BasicType),pred,[]),Translation)), | |
| 2203 | format_to_codes('~w:~w [card=~w]~w~w~w',[Var,PrettyType,Card,MulSol,Imp,Unused],Codes), | |
| 2204 | atom_codes(Translation,Codes), | |
| 2205 | generate_typing_list(VT,TT,Rest,RestCard), | |
| 2206 | kernel_objects:safe_mul(RestCard,Card,TotCard). | |
| 2207 | ||
| 2208 | :- use_module(symmetry_marker,[hash_model_checking_imprecise/2]). | |
| 2209 | :- use_module(translate,[pretty_type/2]). | |
| 2210 | :- public tcltk_hash_model_checking_imprecise/0. | |
| 2211 | tcltk_hash_model_checking_imprecise :- | |
| 2212 | hash_model_checking_imprecise(ID,BasicType),!, | |
| 2213 | print(' * Note: Hashing may be imprecise for: '), | |
| 2214 | print(ID), print(' : '),translate:pretty_type(BasicType,S),print(S), print(' !'),nl. | |
| 2215 | ||
| 2216 | ||
| 2217 | /* find constants which are assigned multiple values */ | |
| 2218 | :- dynamic non_det_constant/1. | |
| 2219 | find_non_det_constants :- | |
| 2220 | retractall(non_det_constant(_)), | |
| 2221 | findall(Csts,visited_expression(_,concrete_constants(Csts),_),CL), | |
| 2222 | (CL=[Valuation1|O],O=[_|_] -> find_non_det_constants1(Valuation1,O) | |
| 2223 | ; true /* 0 or 1 valuation only */ | |
| 2224 | ). | |
| 2225 | ||
| 2226 | find_non_det_constants1([],_). | |
| 2227 | find_non_det_constants1([bind(C,Value)|T],Other) :- check_cst(Other, C, Value, PeeledOther), | |
| 2228 | find_non_det_constants1(T,PeeledOther). | |
| 2229 | ||
| 2230 | check_cst([],_,_,[]). | |
| 2231 | check_cst([ [bind(C,OtherVal)|T1] | TT], C, Value, [ T1 | PTT]) :- | |
| 2232 | (Value=OtherVal -> check_cst(TT,C,Value,PTT) | |
| 2233 | ; assert(non_det_constant(C)), peel2(TT,PTT)). | |
| 2234 | peel2([],[]). | |
| 2235 | peel2([ [_|T1] | TT], [ T1 | PTT]) :- peel2(TT,PTT). | |
| 2236 | ||
| 2237 | ||
| 2238 | /* --------------------------------- */ | |
| 2239 | ||
| 2240 | ||
| 2241 | /* for tcltk: */ | |
| 2242 | :- use_module(pref_definitions,[b_get_definition_string_list_from_spec/2, b_get_definition_string_from_spec/2]). | |
| 2243 | /* --------------------------------- */ | |
| 2244 | ||
| 2245 | %% | |
| 2246 | % Visualize Invariant... | |
| 2247 | % | |
| 2248 | % Siehe bvisual.pl | |
| 2249 | ||
| 2250 | :- use_module(bvisual). | |
| 2251 | ||
| 2252 | :- public generate_dot_from_invariant/1. | |
| 2253 | generate_dot_from_invariant(FileName):- | |
| 2254 | bmachine:b_get_invariant_from_machine(BExpr), | |
| 2255 | write_dot_file_for_pred_expr(BExpr,FileName). | |
| 2256 | ||
| 2257 | ||
| 2258 | :- public generate_dot_from_operation/2. | |
| 2259 | generate_dot_from_operation(TclOpName,FileName) :- | |
| 2260 | predicate_debugger:adapt_tcl_operation_name(TclOpName,OpName), | |
| 2261 | bvisual:get_operation_pre(OpName, BExpr, _BecomesSuchVars), | |
| 2262 | write_dot_file_for_pred_expr(BExpr,FileName). | |
| 2263 | %generate_tree_from_boolean_expression(BExpr, Tree,BecomesSuchVars), | |
| 2264 | %write_dot_graph_to_file(Tree,FileName). | |
| 2265 | ||
| 2266 | ||
| 2267 | generate_dot_from_properties(FileName) :- | |
| 2268 | (current_state_corresponds_to_fully_setup_b_machine -> CreateExists=false; CreateExists=true), | |
| 2269 | bvisual:get_properties(BExpr,CreateExists), | |
| 2270 | write_dot_file_for_pred_expr(BExpr,FileName). | |
| 2271 | ||
| 2272 | :- use_module(bsyntaxtree,[conjunct_predicates/2]). | |
| 2273 | ||
| 2274 | generate_dot_from_assertions(FileName) :- | |
| 2275 | (current_state_corresponds_to_setup_constants_b_machine, | |
| 2276 | bmachine:b_get_dynamic_assertions_from_machine(BExpr), BExpr \=[] | |
| 2277 | -> true | |
| 2278 | ; bmachine:b_get_static_assertions_from_machine(BExpr) | |
| 2279 | ), | |
| 2280 | conjunct_predicates(BExpr,BE), | |
| 2281 | write_dot_file_for_pred_expr(BE,FileName). | |
| 2282 | ||
| 2283 | generate_dot_from_goal(FileName) :- | |
| 2284 | b_get_machine_goal(BExpr),!, | |
| 2285 | write_dot_file_for_pred_expr(BExpr,FileName). | |
| 2286 | generate_dot_from_goal(FileName) :- | |
| 2287 | write_dot_file_for_pred_expr_and_state(b(string('No GOAL DEFINITION available'),string,[]),[],[],FileName). | |
| 2288 | ||
| 2289 | generate_dot_from_deadlock_po(FileName) :- | |
| 2290 | b_state_model_check:get_unsorted_all_guards_false_pred(BExpr), | |
| 2291 | %print('% CHECKING: '),translate_bexpression(BExpr,PT), print(PT),nl, | |
| 2292 | write_dot_file_for_pred_expr(BExpr,FileName). % we do not check it is a predicate anymore | |
| 2293 | ||
| 2294 | ||
| 2295 | generate_dot_from_formula(Pred,FileName) :- | |
| 2296 | format('Parsing formula ~w~n',[Pred]), | |
| 2297 | parse_machine_formula(Pred,TypedExpr), | |
| 2298 | format('Writing dot formula ~w~n',[TypedExpr]), | |
| 2299 | write_dot_file_for_pred_expr(TypedExpr,FileName). | |
| 2300 | ||
| 2301 | ||
| 2302 | :- use_module(bmachine, [b_parse_machine_formula/3, type_with_errors/4]). | |
| 2303 | parse_machine_formula(RawAST,TypedPred) :- compound(RawAST),!, % allow to pass raw AST as well | |
| 2304 | type_with_errors(RawAST,[prob_ids(visible),variables],_Type,TypedPred). | |
| 2305 | parse_machine_formula(PredStr,TypedExpr) :- | |
| 2306 | b_parse_machine_formula(PredStr,[prob_ids(visible),variables],TypedExpr). | |
| 2307 | ||
| 2308 | ||
| 2309 | write_dot_file_for_pred_expr(BExpr,FileName) :- | |
| 2310 | generate_tree_in_cur_state(BExpr, Tree,[]), | |
| 2311 | printsilent('% Writing to: '), printsilent(FileName),nls, | |
| 2312 | mnf(write_dot_graph_to_file(Tree,FileName)). | |
| 2313 | write_dot_file_for_pred_expr_and_state(BExpr, LocalState, State,FileName) :- | |
| 2314 | mnf(get_tree_from_expr(Tree, BExpr, LocalState, State)), | |
| 2315 | printsilent('% Writing to: '), printsilent(FileName),nls, | |
| 2316 | mnf(write_dot_graph_to_file(Tree,FileName)). | |
| 2317 | ||
| 2318 | generate_tree_in_cur_state(BExpr,Tree,BSVars):- | |
| 2319 | ( current_state_corresponds_to_setup_constants_b_machine, | |
| 2320 | current_b_expression(CurState0), | |
| 2321 | % print(cur(CurState0)),nl, | |
| 2322 | insert_before_substitution_variables(BSVars,[],CurState0,CurState0,CurState) | |
| 2323 | ; | |
| 2324 | CurState = [] | |
| 2325 | ),!, | |
| 2326 | mnf(get_tree_from_expr(Tree, BExpr, [], CurState)). | |
| 2327 | ||
| 2328 | tcltk_bv_get_tops(Tops) :- | |
| 2329 | bv_get_top_level(Tops). | |
| 2330 | tcltk_bv_get_structure(Id,Label,list(Subs)) :- | |
| 2331 | bv_expand_formula(Id,Label,Subs). | |
| 2332 | tcltk_bv_is_leaf(Id,Label) :- | |
| 2333 | bv_expand_formula(Id,Label,[]). | |
| 2334 | tcltk_bv_get_values(Ids,list(RTexts),list(Tags)) :- | |
| 2335 | current_state_id(StateId), | |
| 2336 | bv_get_values(Ids,StateId,Values), | |
| 2337 | predicate_debugger:maplist5(user:retrieve_tag_adapted_text_for_id,Ids,Values,Tags,RTexts). | |
| 2338 | tcltk_bv_get_value(Id,RText,Tag) :- | |
| 2339 | tcltk_bv_get_values([Id],list([RText]),list([Tag])). | |
| 2340 | tcltk_bv_show_formula_as_dot_tree(Id,File) :- | |
| 2341 | bv_get_stored_formula_expr(Id,TExpr), | |
| 2342 | write_dot_file_for_pred_expr(TExpr,File). | |
| 2343 | tcltk_bv_show_formula_as_dot_graph(Id,File) :- | |
| 2344 | bv_get_stored_formula_expr(Id,TExpr), | |
| 2345 | get_texpr_type(TExpr,Type), | |
| 2346 | Type \= pred, Type \= subst, | |
| 2347 | % tcltk_show_typed_expression_as_dot_graph decomposes expressions and shows value as graph: could be useful for pre-configured DEFINITIONS | |
| 2348 | tcltk_show_typed_expression_as_dot_graph(TExpr,File). | |
| 2349 | ||
| 2350 | retrieve_tag_adapted_text_for_id(Id,Value,Tag,RText) :- | |
| 2351 | retrieve_tag_text_for_id(Id,Value,Tag,Text), | |
| 2352 | (Text = '[]' -> RText = '[ ]' ; RText=Text). % for some reason the empty sequence translation [] gets transformed into '' by the tcltk library | |
| 2353 | ||
| 2354 | retrieve_tag_text_for_id(Id,Value,FullTag,Text) :- | |
| 2355 | retrieve_tag_text(Value,Tag,Text), | |
| 2356 | (bv_is_explanation_node(Id) -> convert_explain_tag(Tag,FullTag) ; FullTag=Tag). | |
| 2357 | retrieve_tag_text(i, inac, ''). | |
| 2358 | retrieve_tag_text(e(Text), error, Text). | |
| 2359 | retrieve_tag_text(v(Text), value, Text). | |
| 2360 | retrieve_tag_text(p(true), ptrue, true). | |
| 2361 | retrieve_tag_text(p(false),pfalse, false). | |
| 2362 | ||
| 2363 | :- public tcltk_bv_get_unlimited_value/3. | |
| 2364 | tcltk_bv_get_unlimited_value(Id,Text,Tag) :- | |
| 2365 | current_state_id(StateId), | |
| 2366 | bv_get_value_unlimited(Id,StateId,Value), | |
| 2367 | retrieve_tag_text_for_id(Id,Value,Tag,Text1), | |
| 2368 | atom_codes(Text1,Text). % TODO: In the end, the result was converted from codes to atom and back | |
| 2369 | ||
| 2370 | convert_explain_tag(ptrue,explaintrue). | |
| 2371 | convert_explain_tag(pfalse,explainfalse). | |
| 2372 | convert_explain_tag(X,X). | |
| 2373 | ||
| 2374 | % ----------------------------------------- | |
| 2375 | ||
| 2376 | % STILL TO DO: refactor eval from here and probcli into separate module | |
| 2377 | ||
| 2378 | :- dynamic eval_elapsed_time/1. | |
| 2379 | :- meta_predicate tcltk_time_call(0). | |
| 2380 | tcltk_time_call(Call) :- | |
| 2381 | cputime(T1),Call,cputime(T2),ElapsedTime is T2-T1, | |
| 2382 | retractall(eval_elapsed_time(_)),assert(eval_elapsed_time(ElapsedTime)). | |
| 2383 | ||
| 2384 | :- use_module(eval_strings). | |
| 2385 | ||
| 2386 | :- public tcltk_eval/4. | |
| 2387 | tcltk_eval(String,StringResult,EnumWarning,Solution) :- | |
| 2388 | get_computed_preference(debug_time_out,DTO), | |
| 2389 | %print(debug_time_out(DTO)),nl, | |
| 2390 | time_out_with_enum_warning_one_solution(eval_string(String,StringResult,EnumWarning,LocalState),DTO,TimeOutRes), | |
| 2391 | (LocalState=[] -> Solution='' ; translate_bstate(LocalState,Solution)), | |
| 2392 | (is_time_out_result(TimeOutRes) -> | |
| 2393 | StringResult = '**** TIME-OUT ****', print(StringResult), print(' ('),print(DTO), print('ms)'),nl, | |
| 2394 | EnumWarning = no | |
| 2395 | ; print_last_info). | |
| 2396 | ||
| 2397 | :- public tcltk_eval_string_in_cur_state/2. | |
| 2398 | tcltk_eval_string_in_cur_state(String,TclValue) :- | |
| 2399 | eval_string_in_cur_state(String,_,Value), | |
| 2400 | convert_value_to_tcl(Value,TclValue). | |
| 2401 | convert_value_to_tcl(int(X),R) :- !, R=X. | |
| 2402 | convert_value_to_tcl(pred_true,R) :- !, R=1. | |
| 2403 | convert_value_to_tcl(pred_false,R) :- !, R=0. | |
| 2404 | convert_value_to_tcl(string(X),R) :- !, R=X. | |
| 2405 | % TO DO: add sets,... | |
| 2406 | convert_value_to_tcl(R,R) :- print(cannot_convert_to_tcl(R,R)),nl. | |
| 2407 | ||
| 2408 | eval_string_in_cur_state(String,Typed,Value) :- | |
| 2409 | %format('Parsing : "~w"~n',[String]), | |
| 2410 | bmachine:parse_expression_raw_or_atom_with_prob_ids(String,Typed), | |
| 2411 | current_state_id(CurID), prob2_interface:get_state(CurID,EState), | |
| 2412 | %print(evaluating_in_state(CurID)),nl, | |
| 2413 | b_compute_expression_with_prob_ids(Typed,EState,Value). | |
| 2414 | ||
| 2415 | % code to translate an expression into a list of lists that can be displayed as a table in Tk | |
| 2416 | % TO DO: make more robust and add more fancy translations | |
| 2417 | :- use_module(table_tools). | |
| 2418 | tcltk_eval_as_table(String,Res) :- | |
| 2419 | eval_string_in_cur_state(String,Typed,Value), | |
| 2420 | Res = list([list(Header)|Table]), | |
| 2421 | expand_and_translate_to_table_for_expr(Typed,Value,Header,Table,['no-row-numbers']). | |
| 2422 | ||
| 2423 | :- use_module(user_interrupts,[interruptable_call/1, interruptable_call/2]). | |
| 2424 | interruptable_tcltk_eval(String,StringResult,EnumWarning,Solution) :- | |
| 2425 | if(interruptable_call(tcltk_eval(String,StringResult,EnumWarning,Solution)),true, | |
| 2426 | (StringResult = 'Error or User-Interrupt', EnumWarning=unknown, Solution='')). | |
| 2427 | ||
| 2428 | % ----------------------------------------- | |
| 2429 | % B Simplifier | |
| 2430 | :- use_module(probporsrc(b_simplifier),[tcltk_simplify_b_predicate/2]). | |
| 2431 | tcltk_simplify_predicate(String,StringResult) :- | |
| 2432 | tcltk_simplify_b_predicate(String,StringResult). | |
| 2433 | ||
| 2434 | ||
| 2435 | % ----------------------------------------- | |
| 2436 | % CBC Check | |
| 2437 | ||
| 2438 | get_cbc_data_base_id_checks(IDs) :- | |
| 2439 | findall(ID,b_state_model_check: cbc_check(ID,_Text,_Call,_Res,_Ok),IDs). | |
| 2440 | get_cbc_data_base_text_checks(Strings) :- | |
| 2441 | findall(Text1,(b_state_model_check: cbc_check(_ID,Text,_Call,_Res,_Ok),tools: string_concatenate(Text,';',Text1)),Strings). | |
| 2442 | ||
| 2443 | ||
| 2444 | % ----------------------------------------- | |
| 2445 | ||
| 2446 | % CSP Refinement Search | |
| 2447 | ||
| 2448 | :- dynamic tcltk_cspm_mode/0. | |
| 2449 | ||
| 2450 | set_tcltk_cspm_mode :- assert(tcltk_cspm_mode). | |
| 2451 | unset_tcltk_cspm_mode :- retractall(tcltk_cspm_mode). | |
| 2452 | ||
| 2453 | :- meta_predicate add_csp_process_id1(-,-,1). | |
| 2454 | ||
| 2455 | get_new_csp_process_id(E,File,ID) :- | |
| 2456 | ( parse_single_csp_expression_file(E,File,Proc) -> | |
| 2457 | haskell_csp: check_compiled_term(Proc), add_csp_process_id1(Proc,ID,animatable_process) | |
| 2458 | ; add_error(parse_single_csp_expression_file,'Invalid process expression: ',E),fail | |
| 2459 | ). | |
| 2460 | ||
| 2461 | %parse_and_analyze_process_expression(ProcExp,File,Proc) :- | |
| 2462 | % ( parse_single_csp_expression_file(ProcExp,File,Proc) -> true | |
| 2463 | % ; add_error(parse_single_csp_expression_file,'Invalid process expression: ',ProcExp),fail | |
| 2464 | % ). | |
| 2465 | ||
| 2466 | :- use_module(refinement_checker). | |
| 2467 | get_csp_process_id(Process,ID) :- get_start_transition_term(Process,Trans), | |
| 2468 | transition(root,Trans,ID). | |
| 2469 | ||
| 2470 | :- use_module(probcspsrc(haskell_csp),[animatable_process_without_arguments/1,animatable_process/1,animatable_process_cli/1]). | |
| 2471 | add_csp_process_id(Process,NewID) :- | |
| 2472 | add_csp_process_id1(Process,NewID,animatable_process_cli). | |
| 2473 | ||
| 2474 | add_csp_process_id1(Process,NewID,Pred) :- | |
| 2475 | (call(Pred,Process) | |
| 2476 | -> get_start_transition_term(Process,Trans), | |
| 2477 | (transition(root,Trans,_,DestID) -> NewID=DestID % process already set up | |
| 2478 | ; xtl_interface:get_start_expr(Process,NewState), | |
| 2479 | add_trans_id(root,Trans,NewState,[],NewID,[],_) | |
| 2480 | ) | |
| 2481 | ; add_error_fail(add_csp_process_id,'Not an animatable CSP Process: ',Process)). | |
| 2482 | ||
| 2483 | get_start_transition_term('MAIN',R) :- !, R= start_cspm_MAIN. | |
| 2484 | get_start_transition_term(agent_call(_Src,'MAIN',[]),R) :- !, R= start_cspm_MAIN. | |
| 2485 | get_start_transition_term(P,start_cspm(P)). | |
| 2486 | ||
| 2487 | add_csp_general_process_id(val_of(Process,_),ID) :- !, | |
| 2488 | ( animatable_process_without_arguments(Process) % in case the called processes is one without arguments, then we don't have to parse the expression | |
| 2489 | -> add_csp_process_id(Process,ID) | |
| 2490 | % code below not covered; loaded_main_file only defined for probcli entry point ! | |
| 2491 | %; animation_mode(cspm), | |
| 2492 | % loaded_main_file(CSPFile), | |
| 2493 | % parse_and_analyze_process_expression(Process,CSPFile,Proc), | |
| 2494 | % (transition(root,start_cspm(Proc),_TransID,ID) -> true | |
| 2495 | % ; otherwise -> add_trans_id(root,start_cspm(Proc),Proc,[],ID,[],_) | |
| 2496 | % ) | |
| 2497 | ). | |
| 2498 | add_csp_general_process_id(GenProcExpr,ID) :- | |
| 2499 | % stripping out the source-loc info | |
| 2500 | haskell_csp_analyzer: clear_span(GenProcExpr,GenProcExpr1), | |
| 2501 | get_start_transition_term(GenProcExpr1,Trans), | |
| 2502 | (transition(root,Trans,_TransID,ID) | |
| 2503 | -> true | |
| 2504 | ; add_trans_id(root,Trans,GenProcExpr1,[],ID,[],_) | |
| 2505 | ). | |
| 2506 | ||
| 2507 | :- public tcltk_csp_in_situ_refinement/4. | |
| 2508 | tcltk_csp_in_situ_refinement(ImplProcess,AbsProcess,ResTrace,Style) :- | |
| 2509 | format('Checking ~w ~w ~w~n',[AbsProcess,Style,ImplProcess]), | |
| 2510 | tcltk_csp_in_situ_refinement(ImplProcess,AbsProcess,ResTrace,Style,10000000). | |
| 2511 | csp_ref_style('[T=',trace). % Trace Refinement | |
| 2512 | csp_ref_style('T',trace). % Trace Refinement | |
| 2513 | csp_ref_style('[SF=',singleton_failures). % Singleton Failures Refinement | |
| 2514 | csp_ref_style('[F=',failures). % Failures Refinement | |
| 2515 | csp_ref_style('[R=',refusals). % Refusals Refinement | |
| 2516 | csp_ref_style('[RD=',refusals_div). % Refusals-Divergence Refinement | |
| 2517 | csp_ref_style('F',failures). % Failures Refinement | |
| 2518 | csp_ref_style('[FD=',X) :- csp_ref_style('FailureDivergence',X). | |
| 2519 | csp_ref_style('FD',X) :- csp_ref_style('FailureDivergence',X). | |
| 2520 | csp_ref_style('Trace',trace). | |
| 2521 | csp_ref_style('Failure',failures). | |
| 2522 | csp_ref_style('FailureDivergence',failure_divergences). | |
| 2523 | csp_ref_style('RefusalTesting',refusals). | |
| 2524 | csp_ref_style('RefusalTestingDiv',refusals_div). | |
| 2525 | csp_ref_style('RevivalTesting',revival) :- add_error(unsupported_refinement_operator,'[V= refinement not yet supported.'). | |
| 2526 | csp_ref_style('RevivalTestingDiv',revival_div) :- add_error(unsupported_refinement_operator,'[VD= refinement not yet supported.'). | |
| 2527 | ||
| 2528 | translate_csp_ref_style(Style,RefStyle) :- (csp_ref_style(Style,RefStyle) -> true ; | |
| 2529 | add_error_fail(csp,'Unknown refinement style: ',Style)). | |
| 2530 | ||
| 2531 | % tcltk_csp_in_situ_refinement('P','Q',R,0,1000). tcltk_csp_in_situ_refinement('Q','P',R,1000). | |
| 2532 | tcltk_csp_in_situ_refinement(ImplProcess,AbsProcess,ResTrace,Style,MaxNrOfNewNodes) :- | |
| 2533 | add_csp_process_id(ImplProcess,ImplNodeID), | |
| 2534 | add_csp_process_id(AbsProcess,SpecNodeID), | |
| 2535 | translate_csp_ref_style(Style,RefStyle), | |
| 2536 | refinement_checker:in_situ_ref_search(ImplNodeID,SpecNodeID,ResTrace,RefStyle,MaxNrOfNewNodes). | |
| 2537 | ||
| 2538 | :- use_module(probcspsrc(haskell_csp),[get_csp_assertions/1,translate_csp_assertion/2]). | |
| 2539 | :- public tcltk_check_csp_assertions/2. | |
| 2540 | tcltk_check_csp_assertions([],Summary) :- get_csp_assertions(Assertions), | |
| 2541 | treat_csp_ass(Assertions,_List,0,0,0,Summary). % TO DO: display _List | |
| 2542 | ||
| 2543 | treat_csp_ass([],[],T,F,U,[total/Tot, true/T, false/F, unknown/U]) :- Tot is T+F+U. | |
| 2544 | treat_csp_ass([Assertion|T],['='(PP,Ok)|TPP],True,False,U,Summary) :- !, | |
| 2545 | (checkAssertion(Assertion,PP,_,Ok,_) | |
| 2546 | -> U1=U, (Ok=true -> T1 is True+1, F1=False ; T1=True, F1 is False+1) | |
| 2547 | ; U1 is U+1, T1=True, F1=False,Ok=unknown), | |
| 2548 | treat_csp_ass(T,TPP,T1,F1,U1,Summary). | |
| 2549 | treat_csp_ass([H|T],TP,T1,F1,U,Summary) :- add_error(treat_csp_ass,'Unknown CSP assertion: ',H), | |
| 2550 | U1 is U+1, treat_csp_ass(T,TP,T1,F1,U1,Summary). | |
| 2551 | ||
| 2552 | % assertModelCheckExt(False,val_of(P3,src_span(25,8,25,10,562,2)),DeadlockFree,F) | |
| 2553 | ||
| 2554 | run_assertion_check(assertModelCheckExt(Negated,Spec,Type,ModelStyle),Negated,ResTrace) :- | |
| 2555 | haskell_csp_analyzer: compile_body(Spec,'assertModelCheck',[],[],CSpec), | |
| 2556 | debug_println(9,assertModelCheckExt(Negated,CSpec,Type,ModelStyle)), | |
| 2557 | add_csp_general_process_id(CSpec,SpecNodeID), | |
| 2558 | translate_csp_ref_style(ModelStyle,RefStyle), | |
| 2559 | refinement_checker:in_situ_model_check(SpecNodeID,ResTrace,Type,RefStyle,10000000), | |
| 2560 | print(result_trace),nl,print(ResTrace),nl. | |
| 2561 | run_assertion_check(assertModelCheck(Negated,Spec,Style),Negated,ResTrace) :- | |
| 2562 | run_assertion_check(assertModelCheckExt(Negated,Spec,Style,'FailureDivergence'),Negated,ResTrace). | |
| 2563 | run_assertion_check(assertRef(Negated,Spec,Style,Impl,Span),Negated,ResTrace) :- | |
| 2564 | haskell_csp_analyzer: compile_body(Spec,'assertRef',[],[],CSpec), | |
| 2565 | haskell_csp_analyzer: compile_body(Impl,'assertRef',[],[],CImpl), | |
| 2566 | debug_println(9,assertRef(Negated,CSpec,Style,CImpl,Span)), | |
| 2567 | add_csp_general_process_id(CSpec,SpecNodeID), | |
| 2568 | add_csp_general_process_id(CImpl,ImplNodeID), | |
| 2569 | translate_csp_ref_style(Style,RefStyle), | |
| 2570 | refinement_checker:in_situ_ref_search(ImplNodeID,SpecNodeID,ResTrace,RefStyle,10000000). | |
| 2571 | run_assertion_check(assertLtl(Negated,Spec,FormulaAsAtom,_Span),Negated,ResTrace) :- | |
| 2572 | add_csp_process_id_normalized(Spec,'assertLtl',CSpec,CSpecNodeID), | |
| 2573 | %% print(add_csp_general_process_id(Spec,CSpec,SpecNodeID)),nl, | |
| 2574 | tcltk_reset, | |
| 2575 | ltl:ltl_model_check_with_ce1(CSpec,FormulaAsAtom,-1,specific_node(CSpecNodeID),Result), | |
| 2576 | translate_ltl_result(Result,ResTrace), | |
| 2577 | debug_println(9,ltl_result(Negated,CSpec,CSpecNodeID,FormulaAsAtom,Result)). | |
| 2578 | run_assertion_check(assertCtl(Negated,Spec,FormulaAsAtom,_Span),Negated,ResTrace) :- | |
| 2579 | add_csp_process_id_normalized(Spec,'assertCtl',CSpec,CSpecNodeID), | |
| 2580 | tcltk_reset, | |
| 2581 | ctl: ctl_model_check_with_ce(CSpec,FormulaAsAtom,-1,specific_node(CSpecNodeID),Result,Trace), | |
| 2582 | debug_println(9,ctl_result(Negated,CSpec,CSpecNodeID,FormulaAsAtom,Result)), | |
| 2583 | translate_ctl_result(Result,Trace,ResTrace). | |
| 2584 | ||
| 2585 | checkAssertion(Assertion,PP,Negated,Ok,ResTrace) :- | |
| 2586 | (silent_mode(on) -> true | |
| 2587 | ; print('CHECKING '), | |
| 2588 | translate_csp_assertion(Assertion,PP), | |
| 2589 | print(PP),nl | |
| 2590 | ), | |
| 2591 | debug_println(9,checkAssertion(Assertion)), | |
| 2592 | reset_refinement_checker, | |
| 2593 | (run_assertion_check(Assertion,Negated,ResTrace) | |
| 2594 | -> debug_println(9,result(ResTrace)), | |
| 2595 | (ResTrace=no_counter_example | |
| 2596 | -> (Negated = 'False' -> Ok=true | |
| 2597 | ; %add_error(check_assertRef,'Assertion FAILS (expected refinement not to hold): ',PP), | |
| 2598 | Ok=false) | |
| 2599 | ; (ResTrace=[interrupted|_] | |
| 2600 | -> Ok=interrupted | |
| 2601 | ; (Negated = 'False' -> %add_error(check_assertRef,'Assertion FAILS: ',PP), | |
| 2602 | Ok=false ; Ok=true) | |
| 2603 | ) | |
| 2604 | ), | |
| 2605 | (Ok=true -> printsilent('OK'),nls | |
| 2606 | ; Ok=interrupted -> print('*** Execution interrupted by user ***'),nl | |
| 2607 | ; print('*** FALSE ***'),nl | |
| 2608 | ) | |
| 2609 | ; add_error_fail(checkAssertion,'Internal Error, Assertion Checking Failed for: ',PP) | |
| 2610 | ). | |
| 2611 | ||
| 2612 | add_csp_process_id_normalized(Spec,Functor,CSpec,CSpecNodeID) :- | |
| 2613 | % stripping out the src_span info | |
| 2614 | haskell_csp_analyzer: clear_span(Spec,SpecNoSpan), | |
| 2615 | haskell_csp_analyzer: compile_body(SpecNoSpan,Functor,[],[],CSpec), | |
| 2616 | add_csp_general_process_id(CSpec,CSpecNodeID). | |
| 2617 | ||
| 2618 | translate_ltl_result(ok,Res) :- !, | |
| 2619 | Res = no_counter_example. | |
| 2620 | translate_ltl_result(no,Res) :- !, | |
| 2621 | Res = no. | |
| 2622 | translate_ltl_result(ce(Atom),Res) :- | |
| 2623 | !, % we have a counter-example for the LTL formula | |
| 2624 | Res=Atom. | |
| 2625 | translate_ltl_result(interrupted,Res) :- | |
| 2626 | !, | |
| 2627 | Res=[interrupted]. | |
| 2628 | translate_ltl_result(Status,_Res) :- | |
| 2629 | add_error_fail(ltl_assertions_result, 'Internal Error: unknown LTL assertion result ', Status). | |
| 2630 | ||
| 2631 | translate_ctl_result(true,_Trace,ResTrace) :- !, | |
| 2632 | ResTrace = no_counter_example. | |
| 2633 | translate_ctl_result(false,ce(Atom),ResTrace) :- !, | |
| 2634 | ResTrace = Atom. | |
| 2635 | translate_ctl_result(interrupted,_TRace,ResTrace) :- | |
| 2636 | !, | |
| 2637 | ResTrace=[interrupted]. | |
| 2638 | translate_ctl_result(Status,_Trace,_ResTrace) :- | |
| 2639 | add_error_fail(ctl_assertions_result, 'Internal Error: unknown CTL assertion result ', Status). | |
| 2640 | ||
| 2641 | :- public tcltk_check_csp_assertion/4. | |
| 2642 | tcltk_check_csp_assertion(Assertion,CSPFile,Negated,Result) :- | |
| 2643 | tcltk_check_csp_assertion(Assertion,CSPFile,Negated,_PlTerm,Result). | |
| 2644 | ||
| 2645 | tcltk_check_csp_assertion(Assertion,CSPFile,Negated,PlTerm,Result) :- | |
| 2646 | parse_single_csp_declaration(Assertion,CSPFile,PlTerm), | |
| 2647 | checkAssertion(PlTerm,_PP,Negated,_Ok,Result). | |
| 2648 | ||
| 2649 | :- public tcltk_play_ltl_ctl_counterexample_trace/4. | |
| 2650 | tcltk_play_ltl_ctl_counterexample_trace(Assertion,CSPFile,Type,FairnessChecked) :- | |
| 2651 | announce_event(play_counterexample), | |
| 2652 | ( Type == ltl -> Functor = assertLtl | |
| 2653 | ; Type == ctl -> Functor = assertCtl | |
| 2654 | ; otherwise -> add_error_fail(ltl_ctl_counterexample, 'Internal Error: Model checker type unknown: ',Type)), | |
| 2655 | % constructing the prolog declaration term | |
| 2656 | PlDeclTerm =.. [Functor,_Negated,Spec,FormulaAsAtom,_Span], | |
| 2657 | parse_single_csp_declaration(Assertion,CSPFile,PlDeclTerm), | |
| 2658 | haskell_csp_analyzer: clear_span(Spec,SpecNoSpan), | |
| 2659 | haskell_csp_analyzer: compile_body(SpecNoSpan,'assertLtl',[],[],CSpec), | |
| 2660 | % parsing and preprocessing the LTL/CTL formula | |
| 2661 | parse_and_preprocess_formula(FormulaAsAtom,Type,PF), | |
| 2662 | (is_fairness_implication(PF) -> FairnessChecked='yes'; FairnessChecked='no'), | |
| 2663 | % need to reset history and current state before loading the counter-example | |
| 2664 | tcltk_reset, | |
| 2665 | tcltk_play_counterexample(Type,CSpec,PF). | |
| 2666 | ||
| 2667 | tcltk_play_counterexample(ltl,Spec,Formula) :- !, | |
| 2668 | ltl: tcltk_play_ltl_counterexample(Spec,Formula). | |
| 2669 | tcltk_play_counterexample(ctl,Spec,Formula) :- !, | |
| 2670 | ctl: tcltk_play_ctl_counterexample(Spec,Formula). | |
| 2671 | tcltk_play_counterexample(Type,Spec,Formula) :- | |
| 2672 | add_error_fail(ltl_ctl_counterexample, 'Internal Error: Unknown domain type: ', (Type,Spec,Formula)). | |
| 2673 | ||
| 2674 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 2675 | ||
| 2676 | :- public get_ltl_formulas_from_file/2. | |
| 2677 | %%%% Parse and get LTL formulas from LTL File %%%% | |
| 2678 | get_ltl_formulas_from_file(Filename,Text) :- | |
| 2679 | parse_ltlfile(Filename, Formulas), | |
| 2680 | extract_formulas(Formulas,Fs,_,_), | |
| 2681 | translate_ltl_formulas(Fs,Text). | |
| 2682 | ||
| 2683 | translate_ltl_formulas(Formulas,Text) :- | |
| 2684 | maplist(translate_ltl_formula,Formulas,Strings), | |
| 2685 | haskell_csp: concatenate_string_list(Strings,Text). | |
| 2686 | ||
| 2687 | translate_ltl_formula(Formula,Text) :- | |
| 2688 | pp_ltl_formula(Formula,T), | |
| 2689 | string_concatenate(T,'$',Text). | |
| 2690 | ||
| 2691 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 2692 | ||
| 2693 | :- public tcltk_explore_csp_process/2. | |
| 2694 | tcltk_explore_csp_process(ProcString,SpecNodeID) :- | |
| 2695 | haskell_csp: parse_single_csp_expression(ltl,ProcString,Res), | |
| 2696 | haskell_csp_analyzer: clear_span(Res,ResNoSpan), | |
| 2697 | haskell_csp_analyzer: compile_body(ResNoSpan,'assertLtl',[],[],CRes), | |
| 2698 | add_csp_general_process_id(CRes,SpecNodeID), | |
| 2699 | refinement_checker:dfs_check(SpecNodeID,_ResTrace,false,false). | |
| 2700 | ||
| 2701 | tcltk_visualize_csp_process(SpecNodeID,F) :- | |
| 2702 | visualize_graph: tcltk_print_csp_process_states_for_dot(F,SpecNodeID). | |
| 2703 | ||
| 2704 | :- public get_csp_process_stats/1. | |
| 2705 | :- dynamic nr_csp_process_state/1. | |
| 2706 | get_csp_process_stats(NrNodes) :- | |
| 2707 | assert(nr_csp_process_state(0)), | |
| 2708 | count_nodes, | |
| 2709 | nr_csp_process_state(NrNodes), | |
| 2710 | retractall(nr_csp_process_state(_)). | |
| 2711 | ||
| 2712 | count_nodes :- | |
| 2713 | refinement_checker: dvisited(_NodeID), | |
| 2714 | nr_csp_process_state(NrNodes), | |
| 2715 | NewNrNodes is NrNodes +1, | |
| 2716 | retractall(nr_csp_process_state(_)), | |
| 2717 | assert(nr_csp_process_state(NewNrNodes)), | |
| 2718 | fail. | |
| 2719 | count_nodes. | |
| 2720 | ||
| 2721 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 2722 | ||
| 2723 | tcltk_machine_has_assertions :- | |
| 2724 | ( b_get_static_assertions_from_machine([_|_]); b_get_dynamic_assertions_from_machine([_|_]) ), !. | |
| 2725 | ||
| 2726 | tcltk_unique_top_level_operation(Name) :- b_top_level_operation(Name), | |
| 2727 | \+ (b_top_level_operation(N2), N2 \= Name). | |
| 2728 | ||
| 2729 | tcltk_top_level_operations(list(Res)) :- | |
| 2730 | findall(Name,b_top_level_operation(Name),Names), | |
| 2731 | length(Names,L), | |
| 2732 | (L>5 -> sort(Names,Res) ; Res=Names). | |
| 2733 | ||
| 2734 | tcltk_get_vacuous_guards(list(R)) :- | |
| 2735 | eclipse_interface:get_vacuous_guards(L), | |
| 2736 | (L=[] -> R = ['No vacuous guards'] | |
| 2737 | ; R=L). | |
| 2738 | ||
| 2739 | tcltk_get_vacuous_invariants(list(L)) :- | |
| 2740 | eclipse_interface:get_vacuous_invariants(LP), | |
| 2741 | (LP=[] -> L = ['No vacuous invariants'] | |
| 2742 | ; maplist(translate:translate_bexpression,LP,L)). |