| 1 | | % (c) 2009-2026 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 | | :- module(tcltk_interface,[ |
| 7 | | tcltk_goto_state/2, |
| 8 | | tcltk_add_new_transition_transid/6, |
| 9 | | tcltk_add_new_transition/5, |
| 10 | | tcltk_get_options/1, tcltk_get_options_dest_info/1, tcltk_get_state/1, tcltk_get_state/2, |
| 11 | | tcltk_get_options_or_candidates/2, tcltk_get_options_candidate_nr_name/2, |
| 12 | | potentially_enabled_operation/4, |
| 13 | | tcltk_get_options_nr_description/2, |
| 14 | | tcltk_get_history_nr_description/2, |
| 15 | | tcltk_get_history_nr_origin_str/2, tcltk_edit_history_nr_origin_str/1, |
| 16 | | |
| 17 | | tcltk_get_state_errors/1, tcltk_get_detailed_state_error/6, |
| 18 | | tcltk_open_state_error_in_editor/1, |
| 19 | | tcltk_get_line_col/5, |
| 20 | | tcltk_current_state_invariant_violated/0, |
| 21 | | tcltk_get_status/3, |
| 22 | | tcltk_get_ops_with_virtual_timeout/1, |
| 23 | | tcltk_get_ops_with_real_timeout/1, |
| 24 | | tcltk_get_ops_user_interrupt_occurred/0, |
| 25 | | |
| 26 | | tcltk_compute_options/2, |
| 27 | | can_generate_dot_from_last_state_error/0, |
| 28 | | tcltk_initialise/0, tcltk_reset/0, |
| 29 | | |
| 30 | | tcltk_perform_nr/1, tcltk_random_perform/0, tcltk_random_perform/1, |
| 31 | | tcltk_perform_nr_option/3, |
| 32 | | tcltk_perform_action_term/2, |
| 33 | | tcltk_is_sync_event/1, |
| 34 | | |
| 35 | | tcltk_exists_an_open_node/0, tcltk_goto_an_open_node/0, |
| 36 | | tcltk_goto_max_reached_node/0, tcltk_goto_timeout_node/0, |
| 37 | | tcltk_state_exists_with_invariant_violated/0, |
| 38 | | tcltk_goto_an_invariant_violation/0, tcltk_goto_node_with_id/1, |
| 39 | | tcltk_try_goto_node_with_id/1, |
| 40 | | tcltk_current_node_has_no_real_transition/0, tcltk_current_node_has_real_transition/0, |
| 41 | | tcltk_current_node_has_partial_transition/0, |
| 42 | | tcltk_goto_a_non_deterministic_node/1, tcltk_goto_a_non_deterministic_output_node/1, |
| 43 | | tcltk_goto_a_branching_node/0, tcltk_goto_a_non_resetable_node/0, |
| 44 | | tcltk_state_space_only_has_root_node/0, tcltk_no_constants_or_no_inititalisation_found/0, |
| 45 | | tcltk_goto_event_list_property_violation/3, tcltk_goto_state_enabling_operation/2, |
| 46 | | tcltk_find_max_reached_node/0, tcltk_find_max_reached_node/1, |
| 47 | | tcltk_search_among_existing_nodes/6, |
| 48 | | find_invariant_violation_among_not_checked_nodes/1, |
| 49 | | |
| 50 | | tcltk_model_check/11, do_model_check/12, |
| 51 | | tcltk_set_dbf_mode/1, tcltk_dbf_modes/1, |
| 52 | | tcltk_mark_current_node_to_be_recomputed_wo_timeout/0, |
| 53 | | tcltk_mark_current_node_to_be_recomputed_with_random_enum/0, |
| 54 | | tcltk_finish_current_node_to_be_recomputed_with_random_enum/0, |
| 55 | | tcltk_hash_model_checking_imprecise/0, |
| 56 | | tcltk_clear_state_space_and_refocus_to_current_state/0, |
| 57 | | |
| 58 | | tcltk_constraint_based_check/1, |
| 59 | | tcltk_constraint_based_check_op/2, tcltk_constraint_based_check_op/3, |
| 60 | | tcltk_constraint_based_check/2, tcltk_constraint_based_check_with_timeout/2, |
| 61 | | tcltk_cbc_find_trace/2, tcltk_cbc_find_trace/4, |
| 62 | | tcltk_cbc_refinement_check/2, |
| 63 | | tcltk_constraint_find_valid_state/0, |
| 64 | | tcltk_constraint_find_maximal_valid_state/0, |
| 65 | | tcltk_constraint_find_dynamic_assertion_violation/0, |
| 66 | | tcltk_constraint_find_valid_state_with_pred/3, |
| 67 | | tcltk_constraint_find_deadlock_state/1, |
| 68 | | tcltk_constraint_find_deadlock_state_with_goal/2, |
| 69 | | tcltk_constraint_find_deadlock_state_with_goal/3, |
| 70 | | tcltk_constraint_find_static_assertion_violation/1, |
| 71 | | tcltk_check_if_feasible_operation/4, |
| 72 | | cbc_constraint_find_static_assertion_violation/2, |
| 73 | | |
| 74 | | tcltk_can_backtrack/0, tcltk_can_backtrack/1, |
| 75 | | tcltk_can_forward/0, tcltk_can_forward/1, |
| 76 | | tcltk_prepare_for_reload/0, |
| 77 | | tcltk_backtrack/0, tcltk_backtrack/1, tcltk_fast_forward/0, tcltk_forward/0, |
| 78 | | tcltk_execute_trace_to_current_node/0, tcltk_find_shortest_trace_to_current_node/1, |
| 79 | | tcltk_execute_longest_trace_from/1, |
| 80 | | tcltk_get_history/1, |
| 81 | | tcltk_perform_action_string/3, |
| 82 | | tcltk_perform_action/2, |
| 83 | | tcltk_perform_action/4, |
| 84 | | |
| 85 | | tcltk_open_xtl_file/1, |
| 86 | | tcltk_open_z_file/1, tcltk_open_z_tex_file/1, |
| 87 | | tcltk_open_alloy_file/1, tcltk_open_alloy_prolog_ast_file/1, |
| 88 | | tcltk_open_cspm_file/1, |
| 89 | | tcltk_add_csp_file/1, |
| 90 | | tcltk_load_packaged_eventb_file/1, |
| 91 | | |
| 92 | | tcltk_verify_alloy_cmd/4, |
| 93 | | tcltk_get_alloy_cmd_names/1, |
| 94 | | tcltk_load_alloy_cmd_in_current_translation/1, |
| 95 | | |
| 96 | | tcltk_machine_has_assertions/0, |
| 97 | | tcltk_unique_top_level_operation/1, tcltk_top_level_operations/1, |
| 98 | | |
| 99 | | compute_all_transitions_if_necessary/0, |
| 100 | | compute_all_transitions_if_necessary/2, |
| 101 | | compute_state_information_if_necessary/0, % compute transitions and invariant |
| 102 | | compute_invariant_if_necessary/3, |
| 103 | | check_invariantKO/2, |
| 104 | | check_invariantKO/3, |
| 105 | | catch_clpfd_overflow_call_for_state/4, |
| 106 | | compute_ample_set/3, |
| 107 | | compute_all_transitions/2, |
| 108 | | add_transition/4, |
| 109 | | add_trans_id/5, |
| 110 | | add_trans_id_infos/6, |
| 111 | | |
| 112 | | tcltk_has_eventtrace/1, tcltk_show_eventtrace/2, |
| 113 | | tcltk_execute_model/3, |
| 114 | | tcltk_execute_trace_to_node/1, |
| 115 | | find_shortest_trace_to_node/4, |
| 116 | | |
| 117 | | tcltk_explore_csp_process/2, tcltk_visualize_csp_process/2, |
| 118 | | get_csp_process_id/2, get_csp_process_stats/1, |
| 119 | | |
| 120 | | tcltk_add_user_executed_operation/2, tcltk_add_user_executed_operation/3, |
| 121 | | tcltk_add_user_executed_operation_typed/4, tcltk_add_user_executed_operation_typed/6, |
| 122 | | tcltk_add_user_executed_statement/3, |
| 123 | | tcltk_add_user_modify_variable_transition/2, tcltk_add_user_modify_variable_transition/4, |
| 124 | | tk_get_possible_language_specific_top_level_event/3, |
| 125 | | |
| 126 | | tcltk_analyse_option/2, |
| 127 | | tcltk_analyse/6, |
| 128 | | tcltk_show_typing_of_variables_and_constants/1, |
| 129 | | tcltk_show_current_state/1, |
| 130 | | tcltk_eval/4, interruptable_tcltk_eval/4, |
| 131 | | tcltk_eval_as_table/2, |
| 132 | | tcltk_find_value_as_table/3, find_value_in_cur_state/4, |
| 133 | | tcltk_time_call/1, eval_elapsed_time/1, |
| 134 | | tcltk_check_csp_assertions/2, tcltk_check_csp_assertion/4, tcltk_check_csp_assertion/5, |
| 135 | | checkAssertion/5, |
| 136 | | tcltk_get_vacuous_guards/1, |
| 137 | | tcltk_get_vacuous_invariants/1, tcltk_get_vacuous_invariants_table/1, |
| 138 | | tcltk_operations_covered_info/3, operation_name_covered/1, |
| 139 | | tcltk_show_expression_as_dot/2, |
| 140 | | generate_dot_from_formula/2, |
| 141 | | generate_dot_from_invariant/1, generate_dot_from_properties/1, generate_dot_from_assertions/1, |
| 142 | | generate_dot_from_deadlock_po/1, generate_dot_from_goal/1, generate_dot_from_last_span_predicate/1, |
| 143 | | generate_dot_from_operation/2, generate_dot_from_operation_with_params/4, |
| 144 | | write_dot_file_for_pred_expr/2, |
| 145 | | write_dot_file_for_value_as_tree/2, |
| 146 | | evaluate_expression_over_history_to_csv_file/2, tcltk_evaluate_expression_over_history/2, |
| 147 | | translate_error_for_tclk/2, |
| 148 | | tcltk_set_initial_machine/0, tcltk_clear_machine/0, |
| 149 | | % set_tcltk_cspm_mode/0, unset_tcltk_cspm_mode/0, |
| 150 | | tcltk_open_b_file/1, tcltk_open_b_file_for_minor_mode/2, |
| 151 | | tcltk_run_ltsmin/5, |
| 152 | | tcltk_save_history_as_trace_file/1, |
| 153 | | tcltk_animate_until/4, |
| 154 | | |
| 155 | | tcltk_bv_get_tops/1, |
| 156 | | tcltk_bv_get_structure/3, |
| 157 | | tcltk_bv_is_leaf/2, |
| 158 | | tcltk_bv_get_values/3, |
| 159 | | tcltk_bv_get_value/3, |
| 160 | | tcltk_bv_show_formula_as_dot_tree/2, |
| 161 | | tcltk_bv_show_formula_as_dot_graph/2, |
| 162 | | tcltk_bv_show_value_as_dot_tree/2, |
| 163 | | tcltk_bv_get_pp_formula_string/2, |
| 164 | | tcltk_show_identifier_value_as_dot_tree/2, % a version of the above independent of bvisual |
| 165 | | tcltk_bv_get_unlimited_value/3, tcltk_bv_get_unlimited_value_atom/2, |
| 166 | | |
| 167 | | tcltk_get_constants_predicate/1, tcltk_get_constants_predicate/3, |
| 168 | | |
| 169 | | get_cbc_data_base_id_checks/1, get_cbc_data_base_text_checks/1, |
| 170 | | |
| 171 | | tcltk_write_uml_sequence_chart/1, |
| 172 | | |
| 173 | | get_ltl_formulas_from_file/2, |
| 174 | | tcltk_mcts_auto_play/0, tcltk_mcts_auto_play/1, mcts_auto_play_available/0, |
| 175 | | tcltk_simplify_predicate/2 % not used |
| 176 | | |
| 177 | | ]). |
| 178 | | |
| 179 | | |
| 180 | | :- meta_predicate call_pred_on_expanded_state(3,-,-,-). |
| 181 | | :- meta_predicate map_over_history(3,-). |
| 182 | | :- meta_predicate tcltk_time_call(0). |
| 183 | | :- meta_predicate catch_clpfd_overflow_call_for_state(-,-,0,0). |
| 184 | | :- meta_predicate add_csp_process_id1(-,-,1). |
| 185 | | |
| 186 | | %prob_use_module(X) :- load_files(X,[if(changed),load_type(source),compilation_mode(compile)]). |
| 187 | | |
| 188 | | /* load all necessary modules */ |
| 189 | | :- use_module(library(random)). |
| 190 | | :- use_module(library(lists)). |
| 191 | | |
| 192 | | :- use_module(library(ordsets)). |
| 193 | | :- use_module(library(avl)). |
| 194 | | |
| 195 | | :- use_module(module_information). |
| 196 | | :- module_info(group,tcltk). |
| 197 | | :- module_info(description,'Interface between the Tcl/Tk GUI, the CLI and the internal modules.'). |
| 198 | | |
| 199 | | :- use_module(typechecker). |
| 200 | | :- use_module(self_check). |
| 201 | | :- use_module(probsrc(preferences)). |
| 202 | | :- use_module(probsrc(debug)). |
| 203 | | :- use_module(error_manager). |
| 204 | | :- use_module(kernel_waitflags). |
| 205 | | :- use_module(probsrc(tools)). |
| 206 | | :- use_module(probsrc(specfile)). |
| 207 | | :- use_module(probsrc(state_space_exploration_modes)). |
| 208 | | :- use_module(probsrc(translate)). |
| 209 | | :- use_module(probsrc(b_state_model_check)). |
| 210 | | :- use_module(probsrc(bmachine)). |
| 211 | | :- use_module(probsrc(b_interpreter)). |
| 212 | | :- use_module(probsrc(b_trace_checking)). |
| 213 | | :- use_module(probsrc(bsyntaxtree)). |
| 214 | | :- use_module(kernel_objects). |
| 215 | | :- use_module(probsrc(state_space)). |
| 216 | | :- use_module(extension('plspec/plspec/plspec_core'),[set_error_handler/1]). |
| 217 | | :- use_module(extension('plspec/plspec/prettyprinter'),[pretty_print_error/1]). |
| 218 | | prob_plspec_error_handler(ErrTerm) :- pretty_print_error(ErrTerm), |
| 219 | | add_internal_error('Error detected by plspec',ErrTerm). |
| 220 | | :- set_error_handler(tcltk_interface:prob_plspec_error_handler). |
| 221 | | :- use_module(model_checker). |
| 222 | | :- use_module(dotsrc(visualize_graph)). |
| 223 | | :- use_module(dotsrc(state_space_reduction)). |
| 224 | | :- use_module(dotsrc(state_custom_dot_graph)). |
| 225 | | :- use_module(succeed_max). |
| 226 | | %:- use_module(testcase_generator). |
| 227 | | :- use_module(prozsrc(proz),[open_proz_file/2]). |
| 228 | | :- use_module(dotsrc(reduce_graph_state_space)). |
| 229 | | :- use_module(b_read_write_info). |
| 230 | | %:- use_module(flow). |
| 231 | | :- use_module(probltlsrc(ltl),[parse_and_preprocess_formula/3, parse_ltlfile/2, |
| 232 | | pp_ltl_formula/2, ltl_model_check_with_ce1/5, |
| 233 | | is_fairness_implication/1, tcltk_play_ltl_counterexample/2]). |
| 234 | | :- use_module(probltlsrc(ctl),[ctl_model_check_with_ce/6, tcltk_play_ctl_counterexample/2]). |
| 235 | | %:- use_module('promela/promela_ncprinter'). |
| 236 | | :- use_module(extrasrc(bvisual2),[bv_get_top_level/1, bv_expand_formula/3, bv_get_values/3, bv_get_btvalue/4, |
| 237 | | bv_get_stored_formula_expr/2, bv_is_explanation_node/1, bv_get_value_unlimited/3]). |
| 238 | | :- use_module(b_show_history). |
| 239 | | :- use_module(probcspsrc(haskell_csp),[parse_single_csp_declaration/3]). |
| 240 | | %:- use_module(probcspsrc(slicer_csp),[slice_from_program_point/14]). |
| 241 | | :- use_module(value_persistance, [save_constants/1,add_new_transitions_to_cache/1]). |
| 242 | | :- use_module(cbcsrc(cbc_path_solver),[create_testcase_path_nondet/4,verify_alloy_command/5]). |
| 243 | | :- use_module(dotsrc(uml_generator),[write_uml_sequence_chart/1]). |
| 244 | | |
| 245 | | /* main program |
| 246 | | * ============ |
| 247 | | */ |
| 248 | | |
| 249 | | |
| 250 | | /* |
| 251 | | Start server for LTSmin |
| 252 | | */ |
| 253 | | |
| 254 | | :- use_module(extension('ltsmin/ltsmin'),[start_ltsmin/4]). |
| 255 | | |
| 256 | | |
| 257 | | % Backend = symbolic or sequential |
| 258 | | tcltk_run_ltsmin(Backend,NoDead,NoInv,UsePOR,Res) :- |
| 259 | | % in case of POR we can also enable/disable use_cbc_analysis preference |
| 260 | | (UsePOR == true -> MoreFlags = [por] ; MoreFlags=[]), |
| 261 | | start_ltsmin(Backend, [NoDead, NoInv], MoreFlags,Result), |
| 262 | | get_check_name(NoDead,NoInv,Kind), |
| 263 | | process_ltsmin_result(Result,Kind,Res). |
| 264 | | |
| 265 | | % get_check_name(+NoDead,+NoInv,-Kind) |
| 266 | | get_check_name(true,false,Kind) :- Kind = 'INVARIANT'. |
| 267 | | get_check_name(false,true,Kind) :- Kind = 'DEADLOCK'. |
| 268 | | |
| 269 | | :- use_module(tools_printing,[format_with_colour_nl/4]). |
| 270 | | :- use_module(extension('ltsmin/ltsmin_trace'),[csv_to_trace/3]). |
| 271 | | process_ltsmin_result(ltsmin_model_checking_ok,Kind,no_counter_example_found) :- |
| 272 | | format_with_colour_nl(user_output,green,'LTSMin found no ~w Counter Example',Kind). |
| 273 | | process_ltsmin_result(ltsmin_counter_example_found(CsvFile),Kind,counter_example_found) :- |
| 274 | | format_with_colour_nl(user_output,[red,bold],'LTSMin found ~w Counter Example',Kind), |
| 275 | | csv_to_trace(CsvFile,States,Transitions), |
| 276 | | length(Transitions,TLen), format('*** REPLAYING TRACE with length ~w: ~w~n', [TLen, Transitions]), |
| 277 | | % print(States),nl, |
| 278 | | % length(States,SLen), print(state_len(SLen)),nl, |
| 279 | | (replay_ltsmin_trace(States,Transitions) -> true |
| 280 | | ; add_error(process_ltsmin_result,'Could not replay trace:',Transitions)). |
| 281 | | |
| 282 | | replay_ltsmin_trace([],[]). |
| 283 | | replay_ltsmin_trace([State|TS],[TransName|TT]) :- |
| 284 | | (find_successor_state(State,TransName) |
| 285 | | -> replay_ltsmin_trace(TS,TT) |
| 286 | | ; add_error(replay_ltsmin_trace,'Could not execute:',trans_to(TransName,State)),fail). |
| 287 | | |
| 288 | | :- use_module(state_space,[visited_expression/2]). |
| 289 | | find_successor_state(EState,'$init_state') :- !, |
| 290 | | tcltk_reset, |
| 291 | | compute_all_inits, !, |
| 292 | | is_initial_state_id(NewID), |
| 293 | | visited_expression(NewID,State), % print(found_initial(State,EState,NewID)),nl, |
| 294 | | expand_const_and_vars_to_full_store(State,EState), !, |
| 295 | | tcltk_execute_trace_to_node(NewID). |
| 296 | | find_successor_state(EState,TransName) :- |
| 297 | | tcltk_get_options(_), |
| 298 | | current_options(Options), % print(Options),nl, |
| 299 | | member( (_,_Action,ActionOpAsTerm,NewID), Options), |
| 300 | | get_operation_name(ActionOpAsTerm,TransName), |
| 301 | | visited_expression(NewID,State), % print(found_transition(State,EState,NewID,ActionOpAsTerm)),nl, |
| 302 | | expand_const_and_vars_to_full_store(State,EState), !, % TODO: only compare variables |
| 303 | | tcltk_goto_state(ActionOpAsTerm,NewID). |
| 304 | | |
| 305 | | % compute all INITIALISATIONS |
| 306 | | compute_all_inits :- compute_all_transitions_if_necessary(root), fail. |
| 307 | | compute_all_inits :- is_concrete_constants_state_id(ID), compute_all_transitions_if_necessary(ID), fail. |
| 308 | | compute_all_inits. |
| 309 | | |
| 310 | | /* -------------------------------------------------------------------- */ |
| 311 | | |
| 312 | | %tcltk_find_untyped_vars(Vs) :- find_untyped_vars(Vs), Vs \== []. |
| 313 | | |
| 314 | | %tcltk_find_untyped_consts(Vs) :- find_untyped_consts(Vs), Vs \== []. |
| 315 | | |
| 316 | | |
| 317 | ? | tcltk_find_max_reached_node :- tcltk_find_max_reached_node(_). |
| 318 | ? | tcltk_find_max_reached_node(ID) :- max_reached_or_timeout_for_node(ID). |
| 319 | | |
| 320 | | |
| 321 | | tcltk_current_node_has_no_real_transition :- |
| 322 | | \+ tcltk_current_node_has_real_transition. |
| 323 | | tcltk_current_node_has_real_transition :- |
| 324 | | current_state_id(CurID), |
| 325 | | transition(CurID,Trans,_), |
| 326 | | (CurID \= root -> true |
| 327 | | ; Trans = '$partial_setup_constants' |
| 328 | | -> properties_were_filtered(Nr), Nr>0 % we probably have the partial transition due to prob-ignore pragmas |
| 329 | | % TODO: detect whether any of the other non-ignored conjuncts were false/unknown |
| 330 | | ; true),!. |
| 331 | | tcltk_current_node_has_partial_transition :- |
| 332 | | current_state_id(CurID), |
| 333 | | transition(CurID,'$partial_setup_constants',_),!. |
| 334 | | |
| 335 | | /* --------------------------------------------------------------------- */ |
| 336 | | tcltk_goto_state(ActionAsTerm,StateID) :- |
| 337 | | (var(StateID) -> print_message(var_state(tcltk_goto_state(ActionAsTerm,StateID))) ; true), |
| 338 | | (visited_expression_id(StateID) |
| 339 | | -> true |
| 340 | | ; ajoin(['State ',StateID,' does not exist. Could be due to insufficient memory. Transition: '],Msg), |
| 341 | | add_warning(tcltk_goto_state,Msg,ActionAsTerm), |
| 342 | | fail |
| 343 | | ), |
| 344 | | (current_state_id(CurID) -> true ; print('*** no_current_state_id ***'),nl), |
| 345 | ? | ((transition(CurID,ActionAsTerm,OpID,StateID) |
| 346 | | ; ActionAsTerm=jump, % jump is used by ProB2 and eclipse interface; TODO: use $jump or something similar to avoid confusion with real operation names |
| 347 | | transition(CurID,_,OpID,StateID) |
| 348 | | ) |
| 349 | | -> /* ok: proper transition */ |
| 350 | | set_current_state_id(StateID), |
| 351 | | add_to_op_trace_ids(OpID), |
| 352 | | add_id_to_history(CurID) |
| 353 | | ; (CurID=StateID |
| 354 | | -> true |
| 355 | | ; ActionAsTerm=jump, find_id_in_history(StateID,Pos) |
| 356 | | -> tcltk_backtrack(Pos) |
| 357 | | ; ActionAsTerm=jump, find_id_in_forward_history(StateID,Pos) |
| 358 | | -> tcltk_forward(Pos) |
| 359 | | ; set_current_state_id(StateID), |
| 360 | | add_to_op_trace_ids(jump(StateID)), |
| 361 | | add_id_to_history(CurID) |
| 362 | | ) |
| 363 | | ). |
| 364 | | |
| 365 | | find_id_in_history(StateId,Position) :- history(H), nth1(Position,H,StateId). |
| 366 | | find_id_in_forward_history(StateId,Position) :- forward_history(H), nth1(Position,H,forward(StateId,_)). |
| 367 | | |
| 368 | | add_id_to_history(CurID) :- |
| 369 | | (retract(history(History))-> true |
| 370 | | ; add_warning(add_id_to_history,'No history for: ',CurID),History=[]), |
| 371 | | (History=[],CurID\=root |
| 372 | | -> add_message(add_id_to_history,'Adding missing root to history: ',CurID), |
| 373 | | assertz(history([CurID,root])) % fix error in synchronisation between ProB2UI and prolog; should be fixed now |
| 374 | | ; assertz(history([CurID|History])) |
| 375 | | ), |
| 376 | | retractall(forward_history(_)). |
| 377 | | |
| 378 | | |
| 379 | | |
| 380 | | tcltk_add_new_transition(FromID,Action,ToID,ToTempl,TransInfo) :- |
| 381 | | tcltk_add_new_transition_transid(FromID,Action,ToID,ToTempl,TransInfo,_TransId). |
| 382 | | |
| 383 | | tcltk_add_new_transition_transid(FromID,Action,ToID,ToTempl,TransInfo,TransId) :- |
| 384 | | add_new_transition_transid_with_infos(FromID,[],Action,ToID,ToTempl,TransInfo,TransId). |
| 385 | | |
| 386 | | % variation with precomputed infos for the initial id (FromID) |
| 387 | | add_new_transition_transid_with_infos(FromID,PrecomputedInfos,Action,ToID,ToTempl,TransInfo,TransId) :- |
| 388 | | get_operation_internal_name(Action,OpName), % will use $initialise_machine; important for test 961 and PROOF_INFO |
| 389 | | get_id_of_node_and_add_if_required_with_skip_check(ToTempl,ToID,Exists,FromID,OpName,PrecomputedInfos), |
| 390 | | %% print_message(tcltk_add_new_transition(FromID,Action,ToID,Exists)), %% |
| 391 | | ( Exists=exists, |
| 392 | | (preferences:preference(store_only_one_incoming_transition,true), |
| 393 | | \+ operation_not_yet_covered(OpName) % otherwise store at least one transition to achieve coverage |
| 394 | | %-> transition(FromID,_,_,_) % add transition to prevent deadlock being detected |
| 395 | ? | ; transition(FromID,Action,TransId,ToID) |
| 396 | | ) |
| 397 | | -> true % // the transition already exists |
| 398 | | ; % we have a new transition: |
| 399 | | (preferences:preference(forget_state_space,true) |
| 400 | | -> (any_transition(FromID,_,_) -> true |
| 401 | | ; store_transition(FromID,'$NO_DEADLOCK',FromID,TransId)) /* just add dummy transition */ |
| 402 | | ; store_transition(FromID,Action,ToID,TransId |
| 403 | | ), |
| 404 | | (store_transition_infos(TransInfo,TransId) -> true |
| 405 | | ; add_internal_error('storing transition info failed', store_transition_infos(TransInfo,TransId))) |
| 406 | | ), |
| 407 | | mark_operation_as_covered(OpName), |
| 408 | | (FromID \= ToID, b_or_z_mode, not_all_transitions_added(ToID) |
| 409 | | -> add_additional_destination_infos(FromID,OpName,ToID) % e.g., PROOF_INF |
| 410 | | ; true |
| 411 | | ) |
| 412 | | ). |
| 413 | | |
| 414 | | % a version that checks for query/skip operations and then simply returns old id |
| 415 | | get_id_of_node_and_add_if_required_with_skip_check(_ToTempl,ToID,Exists,FromID,OpName,_PrecomputedInfos) :- |
| 416 | | animation_mode(b), % csp_and_b mode is *not* ok ; see test 1701 for example |
| 417 | | b_operation_cannot_modify_state(OpName), |
| 418 | | !, |
| 419 | | Exists=exists,ToID=FromID. |
| 420 | | get_id_of_node_and_add_if_required_with_skip_check(ToTempl,ToID,Exists,FromID,OpName,PrecomputedInfos) :- |
| 421 | | get_id_of_node_and_add_if_required(ToTempl,ToID,Exists,FromID,OpName,PrecomputedInfos). |
| 422 | | |
| 423 | | |
| 424 | | :- use_module(probsrc(bit_sets),[bitset_intersection/3]). |
| 425 | | % will only be called for ToID different from FromID |
| 426 | | add_additional_destination_infos(FromID,ActionName,ToID) :- %print(add_dest(FromID,ActionName,ToID)),nl, |
| 427 | | ( b_operation_preserves_invariant(ActionName,Full), |
| 428 | | \+ invariant_still_to_be_checked(FromID), |
| 429 | | \+ invariant_violated(FromID) % if Invariant does not hold in previous state, |
| 430 | | % we have no idea about invariants in the new state (proof assumes invariant holds before) |
| 431 | | -> |
| 432 | | (retract(specialized_inv(ToID,OldMask)) -> true ; OldMask = empty), |
| 433 | | (Full=full_invariant |
| 434 | | -> assertz(specialized_inv(ToID,invariant_preserved)) |
| 435 | | % unfortunately we cannot yet retract invariant_not_yet_checked |
| 436 | | ; OldMask=invariant_preserved |
| 437 | | -> assertz(specialized_inv(ToID,invariant_preserved)) |
| 438 | | ; b_specialized_invariant_mask_for_op(ActionName,Mask) -> |
| 439 | | (OldMask == empty -> NewMask = Mask ; bitset_intersection(Mask,OldMask,NewMask)), |
| 440 | | assertz(specialized_inv(ToID,NewMask)) |
| 441 | | ; add_internal_error('Illegal operation: ',add_additional_destination_infos(FromID,ActionName,ToID) ), |
| 442 | | assertz(specialized_inv(ToID,OldMask)) |
| 443 | | ) |
| 444 | | ; true |
| 445 | | ). |
| 446 | | /* |
| 447 | | Store names of incoming transitions in an AVL tree |
| 448 | | Used to calculate invariant in presence of proof information |
| 449 | | */ |
| 450 | | % we could store this information to allow us to quickly generate traces from root to any state |
| 451 | | %add_additional_destination_infos(FromID,ActionName,ToID) :- |
| 452 | | % (reached_via(ToID,_,_) -> true ; %TODO: probably we should also store transition id |
| 453 | | % assertz(reached_via(ToID,ActionName,FromID))). |
| 454 | | % TO DO: we could store pge disabling information here disabled_operations |
| 455 | | |
| 456 | | |
| 457 | | |
| 458 | | |
| 459 | | :- use_module(state_space_exploration_modes,[set_depth_breadth_first_mode/1,dbf_modes/3]). |
| 460 | | |
| 461 | | |
| 462 | | tcltk_set_dbf_mode(Nr) :- dbf_modes(Nr,Mode,_),!, |
| 463 | | set_depth_breadth_first_mode(Mode). |
| 464 | | tcltk_set_dbf_mode(Nr) :- add_error(tcltk_set_dbf_mode,'Unknown mode: ',Nr). |
| 465 | | |
| 466 | | tcltk_dbf_modes(list(Names)) :- findall(N,dbf_modes(_,_,N),Names). |
| 467 | | |
| 468 | | |
| 469 | | :- dynamic prev_randomise_enumeration_order/1. |
| 470 | | |
| 471 | | |
| 472 | | tcltk_mark_current_node_to_be_recomputed_wo_timeout :- |
| 473 | | current_state_id(CurID), |
| 474 | | format('Recomputing state id=~w without TIME_OUT~n',[CurID]), |
| 475 | | tcltk_mark_node_for_recomputed(CurID), |
| 476 | | (use_no_timeout(CurID) -> true ; assertz(use_no_timeout(CurID))). |
| 477 | | |
| 478 | | % used for recomputing a state with random enumeration |
| 479 | | tcltk_mark_current_node_to_be_recomputed_with_random_enum :- |
| 480 | | current_state_id(CurID), |
| 481 | | format('Recomputing state id=~w with random enumeration~n',[CurID]), |
| 482 | | tcltk_mark_node_for_recomputed(CurID), |
| 483 | | % retractall(transition(CurID,_,_,_)), % we no longer delete the transitions; this can cause problems with the history |
| 484 | | % (if CurID appears earlier in the history and we remove the transition) and lead to error messages |
| 485 | | % also: for the user it may be good to add new transitions incrementally |
| 486 | | temporary_set_preference(randomise_enumeration_order,true,PREV), |
| 487 | | assertz(prev_randomise_enumeration_order(PREV)). |
| 488 | | |
| 489 | | tcltk_finish_current_node_to_be_recomputed_with_random_enum :- |
| 490 | | retract(prev_randomise_enumeration_order(PREV)), |
| 491 | | reset_temporary_preference(randomise_enumeration_order,PREV). |
| 492 | | |
| 493 | | tcltk_mark_node_for_recomputed(ID) :- |
| 494 | | (not_all_transitions_added(ID) -> true |
| 495 | | ; add_id_at_front(ID)), |
| 496 | | retractall(max_reached_for_node(ID)), |
| 497 | | retractall(time_out_for_node(ID,_,_)), |
| 498 | | % TODO: clear b_operation_cache:operation_cached_time_out for relevant nodes |
| 499 | | (transition(ID,'$partial_setup_constants',ID2) |
| 500 | | -> delete_node(ID2) ; true), |
| 501 | | retractall(state_space:transition(ID,'$partial_setup_constants',_,_)). |
| 502 | | |
| 503 | | transitions_computed_for_node(ID) :- |
| 504 | | \+(not_all_transitions_added(ID)), |
| 505 | | \+ is_not_interesting(ID). |
| 506 | | |
| 507 | | |
| 508 | | |
| 509 | | |
| 510 | | tcltk_set_initial_machine :- |
| 511 | | tcltk_clear_machine, |
| 512 | | b_set_initial_machine, |
| 513 | | set_animation_mode(b). |
| 514 | | |
| 515 | | % new profiler |
| 516 | | %:- use_module('../extensions/profiler/profiler.pl'). |
| 517 | | % old profiler |
| 518 | | %:- use_module(runtime_profiler,[reset_runtime_profiler/0]). |
| 519 | | |
| 520 | | % the following clears the entire state space and uses the current state as now starting initial state |
| 521 | | tcltk_clear_state_space_and_refocus_to_current_state :- |
| 522 | | Op = 'REFOCUS-ANIMATOR', |
| 523 | | current_expression(_CurID,CurState), |
| 524 | | (CurState = const_and_vars(ConstID,VarState) -> |
| 525 | | visited_expression(ConstID,ConstState), |
| 526 | | transition(root,SetupConstantAction,_,ConstID) |
| 527 | | ; ConstState=[]), |
| 528 | | announce_event(reset_specification), |
| 529 | | (ConstState=[] |
| 530 | | -> add_trans_id(root,Op,CurState,NewID,_TransId) |
| 531 | | ; add_trans_id(root,SetupConstantAction,ConstState,NewConstID,_), |
| 532 | | add_trans_id(NewConstID,Op,const_and_vars(NewConstID,VarState),NewID,_), |
| 533 | | (retract_open_node(NewConstID) -> true ; true), |
| 534 | | tcltk_goto_state(Op,NewConstID) |
| 535 | | ), |
| 536 | | tcltk_goto_state(Op,NewID), |
| 537 | | (retract_open_node(root) -> true ; true). |
| 538 | | |
| 539 | | :- use_module(eventhandling, [announce_event/1]). |
| 540 | | tcltk_clear_machine :- |
| 541 | | announce_event(reset_specification), |
| 542 | | announce_event(clear_specification), |
| 543 | | reset_tcltk_interface, |
| 544 | | set_animation_mode(b), |
| 545 | | bmachine:b_set_empty_machine, |
| 546 | | reset_errors, |
| 547 | | % reset_dynamics, % new profiler |
| 548 | | % Now done via event handling: b_interpreter:reset_b_interpreter,reset_model_checker, |
| 549 | | garbage_collect_atoms. % reclaim atoms if possible |
| 550 | | |
| 551 | | :- use_module(prob2_interface, [start_animation/0, update_preferences_from_spec/0]). |
| 552 | | tcltk_initialise :- |
| 553 | | update_preferences_from_spec, |
| 554 | | start_animation, |
| 555 | | tcltk_try_reload. |
| 556 | | |
| 557 | | tcltk_reset :- reset_errors, |
| 558 | | history(H), op_trace_ids(T), |
| 559 | | current_state_id(CurID), |
| 560 | | (forward_history(FH) -> true ; FH=[]), |
| 561 | | state_space_reset, |
| 562 | | gen_forward_history(T,[CurID|H],FH,FwdHist), |
| 563 | | retractall(forward_history(_)), |
| 564 | | assertz(forward_history(FwdHist)). |
| 565 | | |
| 566 | | gen_forward_history([],H,R,R) :- (H=[root] -> true ; print(unexpected_remaining_hist(H)),nl). |
| 567 | | gen_forward_history([A|TT],[ID|TH],Acc,Res) :- |
| 568 | | gen_forward_history(TT,TH,[forward(ID,A)|Acc],Res). |
| 569 | | |
| 570 | | |
| 571 | | |
| 572 | | /* ---- getting available options ----- */ |
| 573 | | |
| 574 | | tcltk_get_options_dest_info(L) :- |
| 575 | | tcltk_get_options_dest_info(L,[]). %[no_query_operations]). |
| 576 | | tcltk_get_options_dest_info(list(DestinationInfos),Options) :- |
| 577 | | debug_println(9,start_tcltk_get_options_dest_info), |
| 578 | | % get a list of all options which are skip events |
| 579 | | current_state_id(CurID), |
| 580 | | compute_all_transitions_if_necessary(CurID), |
| 581 | | tcltk_get_candidates_dest_info(List1), |
| 582 | | findall(Res, (transition(CurID,ActionAsTerm,ID), % check no_query_operations |
| 583 | | (member(no_query_operations,Options) -> \+ query_op_transition(ActionAsTerm) ; true), |
| 584 | | option_dest_info(ID,ActionAsTerm,CurID,Res)), |
| 585 | | DestinationInfos,List1). |
| 586 | | |
| 587 | | option_dest_info(DestID,ActionAsTerm,CurID,Res) :- DestID=CurID,!, |
| 588 | | (query_op_transition(ActionAsTerm) -> Res=query ; Res=skip). |
| 589 | | option_dest_info(DestID,_,_,Res) :- not_all_transitions_added(DestID),!, Res=open. |
| 590 | | option_dest_info(DestID,_,_,Res) :- invariant_violated(DestID),!,Res=invariant_violated. |
| 591 | | option_dest_info(DestID,_,_,Res) :- is_deadlocked(DestID),!,Res=deadlock. |
| 592 | | option_dest_info(DestID,_,_,Res) :- node_satisfies_goal(DestID),!,Res=goal. |
| 593 | | option_dest_info(_DestID,_,_,unknown). |
| 594 | | |
| 595 | | query_op_transition(Term) :- b_or_z_mode, |
| 596 | | get_operation_name(Term,OpName), |
| 597 | | b_operation_cannot_modify_state(OpName). |
| 598 | | |
| 599 | | tcltk_get_options(Options) :- tcltk_get_options(Options,no_desc). |
| 600 | | |
| 601 | | % get list of enabled operations/events: |
| 602 | | tcltk_get_options(list(Options),GetDesc) :- |
| 603 | | current_state_id(CurID), debug_println(9,start_tcltk_get_options(CurID)), |
| 604 | | catch(tcltk_compute_options(CurID,TransSpecs), |
| 605 | | user_interrupt_signal, ( |
| 606 | | assert_time_out_for_node(CurID,'unspecified_operation_interrupted_by_user',user_interrupt_signal), |
| 607 | | tcltk_get_computed_options(CurID,TransSpecs) |
| 608 | | )), |
| 609 | | extract_actions(TransSpecs,CurID,ActionsAndIDs,Actions,GetDesc), |
| 610 | | set_current_options(ActionsAndIDs), |
| 611 | | debug_println(9,finished_tcltk_get_options(CurID)), |
| 612 | | Actions = Options. |
| 613 | | |
| 614 | | :- dynamic current_candidate_options/1. |
| 615 | | |
| 616 | | % a newer version of tcltk_options which returns list of potentially enabled events |
| 617 | | % in case MAX_OPERATIONS is set to 0; these virtual events are appended at the end of the |
| 618 | | % current transitions (which at the start are empty; but can be populated by executed by predicate) |
| 619 | | % if GetDesc = get_desc then it will try to get operation descriptions (e.g., via desc pragma) |
| 620 | | tcltk_get_options_or_candidates(list(List),GetDesc) :- |
| 621 | | retractall(current_candidate_options(_)), |
| 622 | | tcltk_get_options(list(List1),GetDesc), |
| 623 | | current_state_id(CurID), |
| 624 | | (state_can_have_additional_candidates(CurID,List1,Candidates) |
| 625 | | -> assert(current_candidate_options(Candidates)), |
| 626 | | maplist(get_cand_name,Candidates,List2), |
| 627 | | append(List1,List2,List) |
| 628 | | ; List=List1). |
| 629 | | get_cand_name(candidate(OpName,TO),OpNameRes) :- |
| 630 | | (TO==true -> ajoin([OpName,' (*timeout*)'],OpNameRes) ; OpNameRes=OpName). |
| 631 | | |
| 632 | | :- use_module(specfile,[max_operations_zero_for_setup_constants/0,max_operations_zero_for_initialisation/0]). |
| 633 | | % check if a state can have additional, unexplored transition candidates |
| 634 | | % either because of MAX_OPERATIONS or MAX_INITIALISATIONS or because of symbolic XTL transitions |
| 635 | | state_can_have_additional_candidates(CurID,List1,Res) :- List1=[], |
| 636 | | candidate_setup_constants_or_init(CurID,OpName),!, |
| 637 | | Res = [candidate(OpName,false)]. |
| 638 | | state_can_have_additional_candidates(_,_,Res) :- \+ \+ max_op_zero_or_xtl_mode(_), |
| 639 | | tcltk_get_candidate_operations(Res). |
| 640 | | |
| 641 | | % check if SETUP_CONSTANTS or INITIALISATION wre not computed due to MAX_INITIALISATION |
| 642 | | candidate_setup_constants_or_init(root,Candidate) :- !, b_or_z_mode, |
| 643 | | (b_machine_has_constants_or_properties |
| 644 | | -> max_operations_zero_for_setup_constants, |
| 645 | | Candidate = '$setup_constants' |
| 646 | | ; max_operations_zero_for_initialisation, |
| 647 | | Candidate = '$initialise_machine' |
| 648 | | ). |
| 649 | | candidate_setup_constants_or_init(CurID,'$initialise_machine') :- b_or_z_mode, |
| 650 | | is_concrete_constants_state_id(CurID), |
| 651 | | max_operations_zero_for_initialisation. |
| 652 | | |
| 653 | | % in case of MAX_OPERATIONS=0 just show the potentially enabled (regular) operations |
| 654 | | tcltk_get_candidate_operations(Candidates) :- |
| 655 | | current_state_id(CurID), |
| 656 | | findall(candidate(OpName,TimeOutOcc), |
| 657 | | (max_op_zero_or_xtl_mode(OpName), |
| 658 | | potentially_enabled_operation(CurID,OpName,TimeOutOcc,_Precise) |
| 659 | | ),Candidates). |
| 660 | | |
| 661 | | :- use_module(specfile,[max_operations_zero_for_operation/1]). |
| 662 | | max_op_zero_or_xtl_mode(OpName) :- |
| 663 | | xtl_mode,!, |
| 664 | | xtl_transition_parameters(OpName,_Paras). |
| 665 | | max_op_zero_or_xtl_mode(OpName) :- max_operations_zero_for_operation(OpName). |
| 666 | | |
| 667 | | :- use_module(xtl_interface,[xtl_symbolic_transition_potentially_enabled/2]). |
| 668 | | :- use_module(tools_timeout,[time_out_with_factor_call/4]). |
| 669 | | % get operations with MAX_OPERATIONS=0 which are potentially enabled |
| 670 | | potentially_enabled_operation(StateId,OpName,TimeOutOccurred,PreciseGuard) :- b_or_z_mode,!, |
| 671 | | b_top_level_operation(OpName), |
| 672 | | max_operations_zero_for_operation(OpName), |
| 673 | | Simplify=true, |
| 674 | | get_quantified_operation_enabling_condition(OpName, Guard, _, PreciseGuard, Simplify), |
| 675 | | (time_out_with_factor_call( |
| 676 | | eclipse_interface:test_boolean_expression_in_node(StateId,Guard,'operation Guard'), |
| 677 | | 0.1, [max_time_out(2000), |
| 678 | | silent], |
| 679 | | (format('TIME-OUT checking if ~w is enabled; assuming it could be.~n',[OpName]),TimeOutOccurred=true) |
| 680 | | ) |
| 681 | | -> (var(TimeOutOccurred) -> TimeOutOccurred=false ; true)). |
| 682 | | potentially_enabled_operation(StateId,OpName,false,imprecise) :- xtl_mode,!, |
| 683 | | visited_expression(StateId,State), |
| 684 | | xtl_symbolic_transition_potentially_enabled(OpName,State). |
| 685 | | |
| 686 | | % get the name of a currently stored candidate option/operation |
| 687 | | % the option list was empty and we inserted a list of candidate operations |
| 688 | | % (e.g., because MAX_OPERATIONS was 0) |
| 689 | | tcltk_get_options_candidate_nr_name(Nr,OpName) :- |
| 690 | | current_candidate_options(List), |
| 691 | | current_options(List1), length(List1,Len), |
| 692 | | N1 is Nr-Len, % the candidate of potentially enabled events are listed after the regular options |
| 693 | | nth1(N1,List,candidate(OpName,_)). |
| 694 | | |
| 695 | | % get destination info for candidate operations in the Operations View |
| 696 | | tcltk_get_candidates_dest_info(L) :- current_state_id(CurID), |
| 697 | | current_candidate_options(Cands),!, |
| 698 | | maplist(get_cand_dest(CurID),Cands,L). |
| 699 | | tcltk_get_candidates_dest_info([]). |
| 700 | | get_cand_dest(_,candidate(_,true),R) :- !, R=time_out. |
| 701 | | get_cand_dest(CurID,candidate(OpName,_),Res) :- |
| 702 | | transition(CurID,ActionTerm,_ActId,_DestID), |
| 703 | | get_operation_name(ActionTerm,OpName),!, |
| 704 | | % it is a candidate for which we already have a transition |
| 705 | | Res = reached_candidate. |
| 706 | | get_cand_dest(_,_,candidate). |
| 707 | | |
| 708 | | :- use_module(tools_timeout,[time_out_call/2]). |
| 709 | | :- use_module(translate,[translate_event_with_src_and_target_id/4]). |
| 710 | | extract_actions([],_,[],[],_). |
| 711 | | extract_actions([(ActionId,Term,Dst)|T],CurID,[(ActionId,Str,Term,Dst)|Srest],[Str|ET],GetDesc) :- |
| 712 | | extract_action(CurID,Term,Dst,Str,GetDesc), |
| 713 | | extract_actions(T,CurID,Srest,ET,GetDesc). |
| 714 | | |
| 715 | | extract_action(CurID,ActionAsTerm,DestID,Str,get_desc) :- |
| 716 | | tcltk_get_op_desc_for_trans(CurID,ActionAsTerm,DestID,Desc),!, Str=Desc. |
| 717 | | extract_action(CurID,ActionAsTerm,DestID,Str,_) :- |
| 718 | | time_out_call(translate_event_with_src_and_target_id(ActionAsTerm,CurID,DestID,Str), Str='**TIMEOUT**'). |
| 719 | | |
| 720 | | % compute transitions and invariant info |
| 721 | | compute_state_information_if_necessary :- |
| 722 | | current_state_id(CurID), |
| 723 | | compute_state_information_if_necessary(CurID). |
| 724 | | compute_state_information_if_necessary(CurID) :- |
| 725 | | compute_all_transitions_if_necessary(CurID,true). % CheckInvariant=true |
| 726 | | |
| 727 | | tcltk_compute_options(CurID,ActionsAndIDs) :- |
| 728 | | compute_state_information_if_necessary(CurID), |
| 729 | | %print(found_transitions(CurID)),nl, |
| 730 | | tcltk_get_computed_options(CurID,ActionsAndIDs). |
| 731 | | |
| 732 | | tcltk_get_computed_options(CurID,ActionsAndIDs) :- |
| 733 | | findall((ActId,ActionAsTerm,DestID), |
| 734 | | transition(CurID,ActionAsTerm,ActId,DestID), |
| 735 | | % TO DO: sort or group, especially if we randomize transition/3 |
| 736 | | ActionsAndIDs). |
| 737 | | |
| 738 | | tcltk_get_status(INVVIOLATED,MAXREACHED,TIMEOUT) :- debug_println(9,start_tcltk_get_status), |
| 739 | | current_state_id(CurID), |
| 740 | | (time_out_for_invariant(CurID) -> INVVIOLATED = 2 |
| 741 | | ; get_invariant_violated(CurID) -> INVVIOLATED = 1 |
| 742 | | ; not_invariant_checked(CurID) -> INVVIOLATED = 3 |
| 743 | | ; not_interesting(CurID) -> INVVIOLATED = 3 |
| 744 | | ; INVVIOLATED = 0 |
| 745 | | ), |
| 746 | | (max_reached_for_node(CurID) -> MAXREACHED = 1 |
| 747 | | ; not_interesting(CurID) -> MAXREACHED = 2 |
| 748 | | ; MAXREACHED = 0), |
| 749 | | (time_out_for_node(CurID,_,time_out) -> TIMEOUT = 1 |
| 750 | | ; time_out_for_node(CurID,_,user_interrupt_signal) -> TIMEOUT = 3 % CTRL-C |
| 751 | | ; time_out_for_node(CurID,_,virtual_time_out(kodkod_timeout)) -> TIMEOUT = 1 % KODKOD; regular time-out |
| 752 | | ; time_out_for_node(CurID,_,_) -> TIMEOUT = 2 % virtual_time_out |
| 753 | | ; TIMEOUT = 0), |
| 754 | | debug_println(9,got_status(INVVIOLATED,MAXREACHED,TIMEOUT)). |
| 755 | | |
| 756 | | tcltk_get_ops_with_virtual_timeout(OpNameList) :- |
| 757 | | current_state_id(StateId), |
| 758 | | ops_with_timeout(StateId,OpNameList,virtual_time_out(_)). |
| 759 | | tcltk_get_ops_with_real_timeout(OpNameList) :- |
| 760 | | current_state_id(StateId), |
| 761 | | ops_with_timeout(StateId,OpNameList,time_out). |
| 762 | | % Note: possibilities are currently: time_out, user_interrupt_signal, virtual_time_out(_) |
| 763 | | tcltk_get_ops_user_interrupt_occurred :- |
| 764 | | current_state_id(StateId), |
| 765 | | time_out_for_node(StateId,_,user_interrupt_signal). |
| 766 | | ops_with_timeout(StateId,OpNameList,Type) :- |
| 767 | | findall(OpName, time_out_for_node(StateId,OpName,Type), OpNameList). |
| 768 | | |
| 769 | | |
| 770 | | %%fd_copy_term(X,Y,true) :- copy_term(X,Y). |
| 771 | | |
| 772 | | |
| 773 | | |
| 774 | | /* --------------------------------------------------------------------- */ |
| 775 | | |
| 776 | | tcltk_get_history(list(StringHistory)) :- debug_println(9,start_tcltk_get_trace), |
| 777 | | get_action_trace(History), |
| 778 | | convert_trace_to_list_of_strings(History,StringHistory). |
| 779 | | |
| 780 | | convert_trace_to_list_of_strings([],[]). |
| 781 | | convert_trace_to_list_of_strings([action(AS,_)|T],[AS|CT]) :- !, |
| 782 | | %truncate_atom(AS,1000,TruncatedAS), % especially SETUP_CONSTANTS, INITIALISATION can be very large; leading to performance issues |
| 783 | | % get_action_trace now truncates |
| 784 | | convert_trace_to_list_of_strings(T,CT). |
| 785 | | convert_trace_to_list_of_strings([H|T],[H|CT]) :- convert_trace_to_list_of_strings(T,CT). |
| 786 | | |
| 787 | | tcltk_write_uml_sequence_chart(File) :- |
| 788 | | write_uml_sequence_chart(File). |
| 789 | | |
| 790 | | /* --------------------------------------------------------------------- */ |
| 791 | | |
| 792 | | :- dynamic cached_state_as_strings/2. |
| 793 | | :- use_module(probsrc(state_space),[try_compute_depth_of_state_id/2]). |
| 794 | | %tcltk_get_state(list(List)) :- !,List=[]. % comment in to disable State Properties View in ProB Tcl/Tk |
| 795 | | tcltk_get_state(list(List)) :- debug_println(9,start_tcltk_get_state), |
| 796 | | current_expression(CurID,CurState), |
| 797 | | compute_state_information_if_necessary(CurID), |
| 798 | | (time_out_for_invariant(CurID) -> List = [invariant_time_out|List1] |
| 799 | | ; invariant_violated(CurID) -> List = [invariant_violated|List1] |
| 800 | | ; invariant_not_yet_checked(CurID) -> List = [invariant_not_checked|List1] |
| 801 | | ; CurID=root -> List = List1 |
| 802 | | ; CurState = concrete_constants(_) -> List = List1 |
| 803 | | ; specfile:b_or_z_mode -> List=[invariant_ok|List1] |
| 804 | | % only in b_or_z_mode do we add not_invariant_checked facts and check invariant while model checking/animating |
| 805 | | ; List=List1), |
| 806 | | (try_compute_depth_of_state_id(CurID,Depth), |
| 807 | | translate:translate_properties_with_limit(['='(depth,Depth)],[DS]) |
| 808 | | -> List1 = [DS|StateAsStrings] |
| 809 | | ; List1 = StateAsStrings), |
| 810 | | (cached_state_as_strings(CurID,StateAsStrings) % TO DO: separate constant / variable properties ? |
| 811 | | -> true |
| 812 | | ; retractall(cached_state_as_strings(_,_)), |
| 813 | | time_out_call(tcltk_get_state(StateAsStrings,CurState), |
| 814 | | StateAsStrings = ['***TIMEOUT-PROPERTY***']), |
| 815 | | assertz(cached_state_as_strings(CurID,StateAsStrings)) |
| 816 | | ), |
| 817 | | debug_println(9,finished_tcltk_get_state). |
| 818 | | |
| 819 | | tcltk_get_state(StateAsStrings,State) :- |
| 820 | | %print(get_state),nl, |
| 821 | | findall(Prop,property(State,Prop),StateProps), |
| 822 | | %print(translating(StateProps)),nl, |
| 823 | | translate:translate_properties_with_limit(StateProps,StateAsStrings). |
| 824 | | %print(translated(StateAsStrings)),nl. |
| 825 | | |
| 826 | | |
| 827 | | tcltk_get_state_errors(list(ErrorsAsStrings)) :- |
| 828 | | get_current_state_errors(_CurID,Errors), |
| 829 | | translate_state_errors(Errors,ErrorsAsStrings). |
| 830 | | |
| 831 | | get_current_state_errors(CurID,Errors) :- |
| 832 | | current_state_id(CurID), |
| 833 | | findall(Error,( state_error(CurID,_,Error), Error \== invariant_violated ), Errors). |
| 834 | | |
| 835 | | :- dynamic last_detailed_error/3. |
| 836 | | |
| 837 | | reset_tcltk_interface :- debug_println(19,reset_tcltk), |
| 838 | | retractall(cbc_inv_error_found(_,_)), reset_nr_cbc_sols, |
| 839 | | retractall(find_flag(_,_)), |
| 840 | | retractall(resetable_node(_)), |
| 841 | | retractall(non_det_constant(_)), |
| 842 | | retractall(current_candidate_options(_)), |
| 843 | | retractall(cached_state_as_strings(_,_)), |
| 844 | | retractall(last_detailed_error(_,_,_)). |
| 845 | | |
| 846 | | tcltk_get_detailed_state_error(Num,ErrorMsg,Srow,Scol,Erow,Ecol) :- |
| 847 | | retractall(last_detailed_error(_,_,_)), |
| 848 | | get_current_state_errors(CurID,Errors), |
| 849 | | nth0(Num,Errors,Error), |
| 850 | | !, |
| 851 | | explain_state_error(Error,Span,ErrorMsg), |
| 852 | | assertz(last_detailed_error(CurID,Span,ErrorMsg)), % save info, so that we can debug if Span contains a span_predicate |
| 853 | | %(generate_dot_from_last_span_predicate('~/Desktop/err.dot') -> true ; true), |
| 854 | | (extract_line_col_for_main_file(Span,Srow,Scol,Erow,Ecol) |
| 855 | | -> true |
| 856 | | ; Srow= -1, Scol= -1, Erow= -2, Ecol= -2). |
| 857 | | |
| 858 | | |
| 859 | | :- use_module(probsrc(tools_commands),[edit_file/2]). |
| 860 | | :- use_module(specfile,[b_absolute_file_name_relative_to_opened_file/2]). |
| 861 | | % show location of state error in external editor |
| 862 | | tcltk_open_state_error_in_editor(Num) :- |
| 863 | | get_current_state_errors(_,Errors), |
| 864 | | nth0(Num,Errors,Error), |
| 865 | | (get_state_error_span(Error,Span) |
| 866 | | -> (extract_file_line_col(Span,FILE,LINE,_COL,_Erow,_Ecol) |
| 867 | | -> b_absolute_file_name_relative_to_opened_file(FILE,AFILE), |
| 868 | | edit_file(AFILE,LINE) |
| 869 | | ; add_error(tcltk_open_state_error_in_editor,'Could not extract file position: ',Span) |
| 870 | | ) |
| 871 | | ; add_error(tcltk_open_state_error_in_editor,'Could not extract source location for state error: ',Num) |
| 872 | | ). |
| 873 | | |
| 874 | | can_generate_dot_from_last_state_error :- |
| 875 | | last_detailed_error(_CurID,ErrSpan,_),!, |
| 876 | | get_inner_span(ErrSpan,span_predicate(_,_,_)). |
| 877 | | can_generate_dot_from_last_state_error :- |
| 878 | | current_state_id(CurID), state_error(CurID,_,_). % not sure if it is really possible to extract span predicate though |
| 879 | | generate_dot_from_last_span_predicate(FileName) :- |
| 880 | | current_state_id(CurID), |
| 881 | | (last_detailed_error(CurID,ErrSpan,_ErrorMsg) % also works with expressions |
| 882 | | -> true |
| 883 | | ; tcltk_get_detailed_state_error(0,_,_,_,_,_), % try and generate error description |
| 884 | | last_detailed_error(CurID,ErrSpan,_) |
| 885 | | ), |
| 886 | | get_inner_span(ErrSpan,span_predicate(P,LS,State)), |
| 887 | | (State=[], visited_expression(CurID,S), |
| 888 | | state_corresponds_to_initialised_b_machine(S,FullState) |
| 889 | | -> true % span predicates from event trace do not have the current state, add state |
| 890 | | ; FullState=State), |
| 891 | | write_dot_file_for_pred_expr_and_state(P, LS, FullState,FileName). |
| 892 | | |
| 893 | | get_inner_span(pos_context(Span1,_,_),SP) :- !, |
| 894 | | get_inner_span(Span1,SP). |
| 895 | | get_inner_span(SP,SP). |
| 896 | | |
| 897 | | tcltk_current_state_invariant_violated :- |
| 898 | | current_state_id(CurID), |
| 899 | | get_invariant_violated(CurID). |
| 900 | | |
| 901 | | tcltk_state_exists_with_invariant_violated :- |
| 902 | | (invariant_violated(_) -> true). % would be too expensive for XTL mode |
| 903 | | |
| 904 | | % also checks for other formalisms whether something similar to an invariant violation holds |
| 905 | | get_invariant_violated(CurID) :- xtl_mode,!, |
| 906 | | visited_expression(CurID,CurState), |
| 907 | | xtl_invariant_violated(CurState). |
| 908 | | get_invariant_violated(CurID) :- invariant_violated(CurID). |
| 909 | | |
| 910 | | /* --------------------------------------------------------------------- */ |
| 911 | | |
| 912 | | :- use_module(b_trace_checking, [tcltk_save_history_as_trace_file/2]). |
| 913 | | tcltk_save_history_as_trace_file(File) :- |
| 914 | | tcltk_save_history_as_trace_file(prolog,File). |
| 915 | | |
| 916 | | |
| 917 | | /* --------------------------------------------------------------------- */ |
| 918 | | |
| 919 | | :- use_module(translate, [get_bexpression_column_template/4]). |
| 920 | | evaluate_bexpr_over_state(Stream,Expr,ValueTemplate,Columns,ResultColStrings,BState,OpName) :- |
| 921 | | format(Stream,'~w,',[OpName]), |
| 922 | | b_compute_expression_with_prob_ids(Expr,BState,Value), |
| 923 | | copy_term((ValueTemplate,Columns),(Value,ResultCols)), |
| 924 | | my_print_csv_value(ResultCols,Stream), |
| 925 | | maplist(translate:translate_bvalue,ResultCols,ResultColStrings), |
| 926 | | nl(Stream). |
| 927 | | |
| 928 | | % evaluate an expression over the history and save the result to a CSV file |
| 929 | | evaluate_expression_over_history_to_csv_file(Expr,File) :- |
| 930 | | parse_machine_expression(Expr,TypedExpr), |
| 931 | | get_bexpression_column_template(TypedExpr,ValueTemplate,ColHeaders,Columns), |
| 932 | | format('Writing CSV file: ~w~n',[File]), |
| 933 | | open(File,write,Stream), |
| 934 | | format(Stream,'OPERATION,',[]), |
| 935 | | my_print_csv_atoms(ColHeaders,Stream), |
| 936 | | call_cleanup(map_over_history(evaluate_bexpr_over_state(Stream,TypedExpr,ValueTemplate,Columns),_), |
| 937 | | close(Stream)), |
| 938 | | format('Finished writing CSV file: ~w~n',[File]). |
| 939 | | |
| 940 | | |
| 941 | | tcltk_evaluate_expression_over_history(Expr,list([list(['OPERATION','State Id'|ColHeaders])|ColumnLists])) :- |
| 942 | | parse_machine_expression(Expr,TypedExpr), |
| 943 | | get_bexpression_column_template(TypedExpr,ValueTemplate,ColHeaders,Columns), |
| 944 | | map_over_history(evaluate_bexpr_over_state(user_output,TypedExpr,ValueTemplate,Columns), |
| 945 | | ColumnLists). |
| 946 | | |
| 947 | | map_over_history(Pred,ResColumnLists) :- |
| 948 | | history(H), current_state_id(CurID), |
| 949 | | reverse([CurID|H],RH), |
| 950 | | get_action_trace(T), reverse(T,RT), |
| 951 | | maplist(call_pred_on_expanded_state(Pred),RH,[action(root,root)|RT],ColumnLists), |
| 952 | | prune_list(ColumnLists,ResColumnLists). |
| 953 | | % remove unknown elements at front for Tk |
| 954 | | prune_list([unknown|T],Res) :- !, prune_list(T,Res). |
| 955 | | prune_list(R,R). |
| 956 | | |
| 957 | | call_pred_on_expanded_state(_Pred,root,_,ColList) :- !, ColList=unknown. |
| 958 | | call_pred_on_expanded_state(Pred,StateId,action(_,ActionTerm),ResColList) :- print(StateId),nl, |
| 959 | | get_operation_name(ActionTerm,OpName), |
| 960 | | format('Processing state ~w (reached via ~w)~n',[StateId,OpName]), |
| 961 | | visited_expression(StateId,State), |
| 962 | | (state_corresponds_to_initialised_b_machine(State,BState) |
| 963 | | -> call(Pred,ColList,BState,OpName), ResColList = list([OpName,StateId|ColList]) |
| 964 | | ; ResColList = unknown ). |
| 965 | | |
| 966 | | :- use_module(eval_let_store,[extend_state_with_probids_and_lets/2]). |
| 967 | | b_compute_expression_with_prob_ids(Expr,BState,Value) :- |
| 968 | | extend_state_with_probids_and_lets(BState,BState2), |
| 969 | | b_interpreter:b_compute_expression_nowf(Expr,[],BState2,Value,'Tcl/Tk',0). |
| 970 | | |
| 971 | | |
| 972 | | my_print_csv_atoms([A,B|T],Stream) :- !, format(Stream,'"~w",',[A]), |
| 973 | | my_print_csv_atoms([B|T],Stream). |
| 974 | | my_print_csv_atoms([A],Stream) :- format(Stream,'"~w"~n',[A]). |
| 975 | | |
| 976 | | my_print_csv_value([A,B|T],Stream) :- !, |
| 977 | | my_print_csv_value([A],Stream), |
| 978 | | write(Stream,','), |
| 979 | | my_print_csv_value([B|T],Stream). |
| 980 | | my_print_csv_value([V],Stream) :- |
| 981 | | (no_quotes_necessary(V) -> true ; write(Stream,'"')), |
| 982 | | translate:print_bvalue_stream(Stream,V), |
| 983 | | (no_quotes_necessary(V) -> true ; write(Stream,'"')). |
| 984 | | |
| 985 | | no_quotes_necessary(int(_)). |
| 986 | | no_quotes_necessary(pred_false). |
| 987 | | no_quotes_necessary(pred_true). |
| 988 | | |
| 989 | | |
| 990 | | /* --------------------------------------------------------------------- */ |
| 991 | | |
| 992 | | :- use_module(probltlsrc(ltl),[preprocess_formula/2]). |
| 993 | | |
| 994 | | % it is actually more tcltk_animate_until |
| 995 | | tcltk_animate_until(FormulaAsAtom,StepsExecuted,Result) :- |
| 996 | | CheckingType = ltl_state_property, % no_loop means we check entire animation trace from CurID for LTL property |
| 997 | | tcltk_animate_until(FormulaAsAtom,CheckingType,StepsExecuted,Result). |
| 998 | | tcltk_animate_until(FormulaAsAtom,CheckingType,StepsExecuted,Result) :- |
| 999 | | current_state_id(CurID), |
| 1000 | | MaxNrOfSteps = 1000, |
| 1001 | | tcltk_animate_until(FormulaAsAtom,CurID,MaxNrOfSteps,CheckingType,StepsExecuted,Result,_,_). |
| 1002 | | tcltk_animate_until(FormulaAsAtom,CurID,MaxNrOfSteps,CheckingType,StepsExecuted,Result,NewStateId,OpIds) :- |
| 1003 | | parse_and_preprocess_formula(FormulaAsAtom,ltl,Ltl2), |
| 1004 | | % TODO: warn if CheckingType=ltl_state_property and we do not have an atomic state property |
| 1005 | | prob2_interface:find_trace_until_ltl(CurID,random,Ltl2,CheckingType,MaxNrOfSteps,Trace,Result), |
| 1006 | | % Result: ltl_found, maximum_nr_of_steps_reached, deadlock |
| 1007 | | length(Trace,StepsExecuted), |
| 1008 | | (last(Trace,op(_,_,_,NewStateId)) -> true ; NewStateId=CurID), |
| 1009 | | debug_format(19,'Found trace of length ~w to ~w~n',[StepsExecuted,Result]), |
| 1010 | | maplist(get_trans_id,Trace,OpIds), |
| 1011 | | execute_id_trace_from_current(OpIds). |
| 1012 | | |
| 1013 | | get_trans_id(op(OpID,_Name,_CurID,_NextID),OpID). |
| 1014 | | |
| 1015 | | |
| 1016 | | |
| 1017 | | tcltk_random_perform :- tcltk_random_perform2(_,fully_random). |
| 1018 | | tcltk_random_perform(Kind) :- tcltk_random_perform2(_,Kind). |
| 1019 | | |
| 1020 | | % Kind can be fully_random, no_self_loops, explore_open |
| 1021 | | % TODO: other options like out_degree, ... |
| 1022 | | tcltk_random_perform2(ActionId,Kind) :- |
| 1023 | | current_options(Opts), |
| 1024 | | current_state_id(CurID), |
| 1025 | | (Kind=explore_open, exclude(is_already_explored,Opts,Options2), Options2 = [_|_] -> true % try and find unexplored successor |
| 1026 | | ; is_heuristic(Kind), |
| 1027 | | maplist(compute_heuristic(Kind),Opts,HOpts), |
| 1028 | | sort(HOpts,SHOpts), |
| 1029 | | keep_min_heuristic(SHOpts,Opts1) |
| 1030 | | -> |
| 1031 | | (exclude(is_already_explored,Opts1,Options2), Options2 = [_|_] |
| 1032 | | -> true % among the nodes with the lowest heuristic value choose open nodes first; to try find new values |
| 1033 | | ; Options2=Opts1) |
| 1034 | | ; Kind=execute_first_enabled, Opts = [First|_] -> Options2 = [First] |
| 1035 | | ; Kind\=fully_random, |
| 1036 | | exclude(is_self_loop(CurID),Opts,Options2), Options2 = [_|_] -> true % try find different node |
| 1037 | | ; Options2=Opts), |
| 1038 | | length(Options2,Len), |
| 1039 | | (Len>0 |
| 1040 | | -> L1 is Len+1, |
| 1041 | | random(1,L1,RanChoice), |
| 1042 | | tcltk_perform_nr_option(RanChoice,Options2,ActionId) |
| 1043 | | ; true |
| 1044 | | ). |
| 1045 | | |
| 1046 | | is_already_explored((_Id,_Action,_,NextId)) :- \+ not_all_transitions_added(NextId). |
| 1047 | | is_self_loop(CurId,(_Id,_Action,_,CurId)). |
| 1048 | | |
| 1049 | | is_heuristic(heuristic). |
| 1050 | | is_heuristic(min_out_degree). |
| 1051 | | :- use_module(probsrc(state_space_exploration_modes),[compute_heuristic_function_for_state_id/2]). |
| 1052 | | :- use_module(probsrc(state_space),[out_degree/2, compute_transitions_if_necessary/1]). |
| 1053 | | compute_heuristic(Kind,(Id,Action,ActTerm,NextId),heurval(HeurVal,Id,Action,ActTerm,NextId)) :- |
| 1054 | | compute_h2(Kind,NextId,HeurVal). |
| 1055 | | compute_h2(heuristic,NextId,HeurVal) :- |
| 1056 | | compute_heuristic_function_for_state_id(NextId,HeurVal). |
| 1057 | | compute_h2(min_out_degree,NextId,HeurVal) :- |
| 1058 | | compute_transitions_if_necessary(NextId), |
| 1059 | | out_degree(NextId,HeurVal). |
| 1060 | | %compute_h2(out_degree,NextId,HeurVal) :- |
| 1061 | | |
| 1062 | | % only keep the maximal value |
| 1063 | | keep_min_heuristic([heurval(HeurVal,Id,Action,ActTerm,NextId)|HT], |
| 1064 | | [(Id,Action,ActTerm,NextId)|T]) :- keep_min2(HT,HeurVal,T). |
| 1065 | | keep_min2([heurval(HeurVal,Id,Action,ActTerm,NextId)|HT],HeurVal, |
| 1066 | | [(Id,Action,ActTerm,NextId)|T]) :- !, keep_min2(HT,HeurVal,T). |
| 1067 | | keep_min2(_,_,[]). |
| 1068 | | |
| 1069 | | |
| 1070 | | tcltk_get_line_col(Nr,list(StartLine),list(StartCol),list(EndLine),list(EndCol)) :- /* just get the location in the source code */ |
| 1071 | | current_options(Options), |
| 1072 | | nth1(Nr,Options,(_Id,_Action,ActionAsTerm,_NewID)), |
| 1073 | | %print(get_source_text(ActionAsTerm)),nl, |
| 1074 | | time_out_call(get_source_text_positions(ActionAsTerm,StartLine,StartCol,EndLine,EndCol), |
| 1075 | | add_error_and_fail(tcltk_get_line_col,'Timeout determining source code position: ',ActionAsTerm)), |
| 1076 | | StartLine \= []. % otherwise fail |
| 1077 | | % print(startlines(StartLine)),nl,print(startcols(StartCol)),nl, |
| 1078 | | % print(endlines(EndLine)),nl, print(endcol(EndCol)),nl. |
| 1079 | | |
| 1080 | | tcltk_is_sync_event(Nr) :- |
| 1081 | | current_options(Options), |
| 1082 | | nth1(Nr,Options,(_Id,_Action,ActionAsTerm,_NewID)), |
| 1083 | | extract_span_from_event(ActionAsTerm,SPAN,_,_), |
| 1084 | | extract_span_info(SPAN,Info), |
| 1085 | | % print(extracted_span_info_for_sync(Info,SPAN)),nl, |
| 1086 | | member(sharing,Info). |
| 1087 | | |
| 1088 | | % get textual description of nth option in current options |
| 1089 | | % is derived from description pragma attached to operations |
| 1090 | | tcltk_get_options_nr_description(Nr,Desc) :- |
| 1091 | | current_state_id(CurID), |
| 1092 | | current_options(Options), |
| 1093 | | nth1(Nr,Options,(_ActionId,_Action,ActionAsTerm,NewID)), |
| 1094 | | tcltk_get_op_desc_for_trans(CurID,ActionAsTerm,NewID,Desc). |
| 1095 | | |
| 1096 | | :- use_module(probsrc(bmachine),[source_code_for_identifier/6]). |
| 1097 | | % get textual description for entry Nr in the Tk history view |
| 1098 | | tcltk_get_history_nr_description(Nr,Desc) :- |
| 1099 | | get_history_trans(Nr, CurID,ActionAsTerm,DestID), |
| 1100 | | tcltk_get_op_desc_for_trans(CurID,ActionAsTerm,DestID,Desc). |
| 1101 | | |
| 1102 | | get_history_trans(Nr, CurID,ActionAsTerm,DestID) :- |
| 1103 | | op_trace_ids(OpTrace), |
| 1104 | | nth0(Nr,OpTrace,TransId), |
| 1105 | | history(StateIds), |
| 1106 | | nth0(Nr,StateIds,CurID), |
| 1107 | | transition(CurID,ActionAsTerm,TransId,DestID). |
| 1108 | | |
| 1109 | | :- use_module(probsrc(bmachine),[source_code_for_identifier/6]). |
| 1110 | | % show source code origin of entry number Nr in the Tk history view |
| 1111 | | tcltk_get_history_nr_origin_str(Nr,Desc) :- |
| 1112 | | get_history_trans(Nr, _CurID,ActionAsTerm,_DestID), |
| 1113 | | get_operation_name(ActionAsTerm,OpID), |
| 1114 | | source_code_for_identifier(OpID,operation,subst,OriginStr,_,_), |
| 1115 | | Desc=OriginStr. %ajoin([OpID,' ', OriginStr],Desc). |
| 1116 | | |
| 1117 | | |
| 1118 | | :- use_module(probsrc(tools_commands),[edit_file/2]). |
| 1119 | | :- use_module(probsrc(error_manager),[extract_file_line_col/6]). |
| 1120 | | % open source code in external editor for origin of entry number Nr in the history view |
| 1121 | | tcltk_edit_history_nr_origin_str(Nr) :- |
| 1122 | | get_history_trans(Nr, _CurID,ActionAsTerm,_DestID), |
| 1123 | | get_operation_name(ActionAsTerm,OpID), |
| 1124 | | source_code_for_identifier(OpID,operation,subst,_OriginStr,OriginTerm,_), |
| 1125 | | extract_file_line_col(OriginTerm,FILE,LINE,_COL,_Erow,_Ecol), |
| 1126 | | edit_file(FILE,LINE). |
| 1127 | | |
| 1128 | | :- use_module(probsrc(state_space_exploration_modes), |
| 1129 | | [compute_heuristic_function_for_state_id/2]). |
| 1130 | | tcltk_get_op_desc_for_trans(CurID,ActionAsTerm,DestID,Desc) :- |
| 1131 | | ((b_or_z_mode ; xtl_mode), |
| 1132 | | get_operation_description_for_transition(CurID,ActionAsTerm,DestID,Desc) -> true |
| 1133 | | ; compute_heuristic_function_for_state_id(DestID,int(HeuristicVal)), |
| 1134 | | ajoin(['Heuristic=',HeuristicVal],Desc)). % TODO: more infos, like deadlock, GOAL, ... |
| 1135 | | |
| 1136 | | % counter-part to tcltk_get_options, to execute the option/operation number Nr in that list |
| 1137 | | tcltk_perform_nr(Nr) :- |
| 1138 | | current_options(Options), |
| 1139 | | tcltk_perform_nr_option(Nr,Options,_). |
| 1140 | | |
| 1141 | | tcltk_perform_nr_option(Nr,Options,ActionId) :- |
| 1142 | | (nth1(Nr,Options,(ActionId,_Action,ActionAsTerm,NewID)) |
| 1143 | | -> (forward_history([forward(NewID,ActionId)|_FwdHist]) |
| 1144 | | -> tcltk_forward |
| 1145 | | ; tcltk_perform_action_term(ActionAsTerm,NewID), |
| 1146 | | retractall(forward_history(_)) |
| 1147 | | ) |
| 1148 | | ; tcltk_backtrack /* interpret as backtrack */ |
| 1149 | | ). |
| 1150 | | |
| 1151 | | |
| 1152 | | tcltk_can_backtrack :- history([_|_]). |
| 1153 | | tcltk_can_backtrack(Len) :- history(His), length(His,Len),Len>0. |
| 1154 | | |
| 1155 | | tcltk_backtrack :- \+ tcltk_can_backtrack,!, |
| 1156 | | print_message('Cannot backtrack'),fail. |
| 1157 | | tcltk_backtrack :- |
| 1158 | | remove_from_op_trace_ids(LastTraceH), % remove last operation id from op_id trace |
| 1159 | | retract(history(History)), |
| 1160 | | retract(current_state_id(CurID)),!, |
| 1161 | | History= [LastID|EHist], |
| 1162 | | assertz(history(EHist)), |
| 1163 | | %visited_expression(LastID,LastExpr,LastBody), |
| 1164 | | assertz(current_state_id(LastID)), |
| 1165 | | (retract(forward_history(FwdHist)) -> true ; FwdHist=[]), |
| 1166 | | assertz(forward_history([forward(CurID,LastTraceH)|FwdHist])). |
| 1167 | | |
| 1168 | | % used for right-clicks in history |
| 1169 | | tcltk_backtrack(N) :- N =< 0, !. |
| 1170 | | tcltk_backtrack(N) :- % TO DO: more efficient version |
| 1171 | | tcltk_backtrack, N1 is N-1, tcltk_backtrack(N1). |
| 1172 | | |
| 1173 | | :- dynamic saved_forward_history/2. |
| 1174 | | :- volatile saved_forward_history/2. |
| 1175 | | |
| 1176 | | |
| 1177 | | % save certain information to restore when reload is completed: |
| 1178 | | tcltk_prepare_for_reload :- |
| 1179 | | saved_forward_history([_|_],Mode), % tcltk_try_reload not executed; probably reloading failed |
| 1180 | | animation_mode(Mode), |
| 1181 | | current_state_id(root), %user has not performed another trace |
| 1182 | | get_action_trace([]),!, |
| 1183 | | format('Keeping saved forward history~n',[]). % so that user can fix error and re-load again |
| 1184 | | tcltk_prepare_for_reload :- |
| 1185 | | retractall(saved_forward_history(_,_)), |
| 1186 | | get_action_term_trace(TrA),reverse(TrA,Tr), |
| 1187 | | %print(prepare_reloading(Tr)),nl, |
| 1188 | | maplist(gen_unknown_forward,Tr,SavedForwardHistory), |
| 1189 | | animation_mode(Mode), |
| 1190 | | % TO DO: add current forward history as well and restore when doing a reload with fastforward |
| 1191 | | % forward_history(ForwHis), maplist(remove_forward_id,ForwHis,SavedPrevForwHis), |
| 1192 | | assertz(saved_forward_history(SavedForwardHistory,Mode)). |
| 1193 | | |
| 1194 | | %remove_forward_id(forward(_,Step),forward('$UNKNOWN',Step)). |
| 1195 | | gen_unknown_forward(Step,forward('$UNKNOWN',Step)). % the forward ID is unknown |
| 1196 | | |
| 1197 | | % try reloading certain information from previous load of same model |
| 1198 | | tcltk_try_reload :- |
| 1199 | | retract(saved_forward_history(SavedForwardHistory,Mode)), |
| 1200 | | animation_mode(Mode), % we are in the same mode as when saved |
| 1201 | | !, |
| 1202 | | % TO DO: also retractall in other places |
| 1203 | | %print(reloading(SavedForwardHistory)),nl, |
| 1204 | | retractall(forward_history(_)), |
| 1205 | | assertz(forward_history(SavedForwardHistory)). |
| 1206 | | tcltk_try_reload. |
| 1207 | | |
| 1208 | | |
| 1209 | | % go forward while possible |
| 1210 | | tcltk_fast_forward :- tcltk_can_forward,!, tcltk_forward, |
| 1211 | | current_state_id(CurID), |
| 1212 | | compute_state_information_if_necessary(CurID), |
| 1213 | | tcltk_fast_forward. |
| 1214 | | tcltk_fast_forward. |
| 1215 | | |
| 1216 | | tcltk_can_forward :- forward_history([_|_]). |
| 1217 | | tcltk_can_forward(Len) :- forward_history(His), length(His,Len), Len>0. |
| 1218 | | |
| 1219 | | |
| 1220 | | tcltk_forward(N) :- N =< 0, !. |
| 1221 | | tcltk_forward(N) :- % TO DO: more efficient version |
| 1222 | | tcltk_forward, N1 is N-1, tcltk_forward(N1). |
| 1223 | | |
| 1224 | | |
| 1225 | | tcltk_forward :- \+ tcltk_can_forward,!, |
| 1226 | | print_message('Cannot go forward'),fail. |
| 1227 | | tcltk_forward :- |
| 1228 | | retract(forward_history([forward(FwdID,LastTraceH)|FwdHist])), |
| 1229 | | retract(history(EHist)), |
| 1230 | | retract(current_state_id(CurID)),!, |
| 1231 | | go_forward(FwdID,LastTraceH,FwdHist,CurID,EHist). |
| 1232 | | go_forward('$UNKNOWN',ActionAsTerm,FwdHist,CurID,EHist) :- |
| 1233 | | transition(CurID,ActionAsTerm,TransitionID,FwdID),!, |
| 1234 | | %print(found(CurID,ActionAsTerm,TransitionID,FwdID)),nl, |
| 1235 | | go_forward(FwdID,TransitionID,FwdHist,CurID,EHist). |
| 1236 | | % TO DO: try and execute by predicate in case max_reached is true ! |
| 1237 | | go_forward('$UNKNOWN',ActionAsTerm,FwdHist,CurID,EHist) :- |
| 1238 | | is_initialisation_op(ActionAsTerm), |
| 1239 | | % maybe PROPERTIES/INITIALISATION has changed; try and replay with other values |
| 1240 | | transition(CurID,ActionAsTerm2,TransitionID,FwdID), |
| 1241 | | is_initialisation_op(ActionAsTerm2), |
| 1242 | | !, |
| 1243 | | %print(found(CurID,ActionAsTerm,TransitionID,FwdID)),nl, |
| 1244 | | translate_event(ActionAsTerm,Action), |
| 1245 | | format('Could not replay ~w.~nUsing other possible transition instead.~n',[Action]), |
| 1246 | | go_forward(FwdID,TransitionID,FwdHist,CurID,EHist). |
| 1247 | | go_forward('$UNKNOWN',ActionAsTerm,_FwdHist,CurID,EHist) :- !, |
| 1248 | | assertz(forward_history([])), |
| 1249 | | assertz(history(EHist)), |
| 1250 | | assertz(current_state_id(CurID)), |
| 1251 | | translate_event(ActionAsTerm,Action), |
| 1252 | | add_error(tcltk_forward,'Cannot replay step after reload: ',Action). |
| 1253 | | go_forward(FwdID,LastTraceH,FwdHist,CurID,EHist) :- |
| 1254 | | assertz(forward_history(FwdHist)), |
| 1255 | | assertz(history([CurID|EHist])), |
| 1256 | | add_to_op_trace_ids(LastTraceH), |
| 1257 | | assertz(current_state_id(FwdID)), |
| 1258 | | re_execute_transition_if_necessary(CurID,LastTraceH,FwdID). |
| 1259 | | %visited_expression(FwdID,FwdExpr,FwdBody). |
| 1260 | | |
| 1261 | | is_initialisation_op(Op) :- |
| 1262 | | (functor(Op,'$setup_constants',_) ;functor(Op,'$initialise_machine',_)). |
| 1263 | | |
| 1264 | | % re-execute operation with side-effects if necessary and if preference set |
| 1265 | | % TO DO: tie into tcltk_perform so that not only the forward button but also double click |
| 1266 | | % in operations pane works |
| 1267 | | re_execute_transition_if_necessary(FromID,TransitionID,ToID) :- |
| 1268 | | b_or_z_mode, |
| 1269 | | get_preference(re_execute_operations_with_side_effects,true), |
| 1270 | | bmachine_construction:external_procedure_used(_), % TO DO: check if operation itself has side-effects |
| 1271 | | !, |
| 1272 | | (re_execute_transition(FromID,TransitionID,ToID) |
| 1273 | | -> true |
| 1274 | | ; add_error(tcltk_forward,'Could not re-execute operation: ',TransitionID)). |
| 1275 | | re_execute_transition_if_necessary(_,_,_). |
| 1276 | | |
| 1277 | | re_execute_transition(FromID,TransitionID,ToID) :- |
| 1278 | | transition(FromID,ActionTerm,TransitionID,ToID), |
| 1279 | | %%print(trans(ActionTerm)),nl, |
| 1280 | | get_operation_name(ActionTerm,OpName), |
| 1281 | | debug_println(9,re_executing_operation(OpName,FromID,TransitionID,ToID)), |
| 1282 | | visited_expression(FromID,InState), |
| 1283 | | specfile:b_trans(InState,OpName,ActionTerm,_NewState,_TransInfo), |
| 1284 | | debug_println(9,re_executed(OpName)). |
| 1285 | | |
| 1286 | | % a version of tcltk_perform_action_term which can be given only the String (e.g., for trace checking) |
| 1287 | | tcltk_perform_action_string(ActionString,ActionAsTerm,NewID) :- |
| 1288 | | current_state_id(CurID), |
| 1289 | ? | transition(CurID,ActionAsTerm,_,NewID), |
| 1290 | | translate_event_with_src_and_target_id(ActionAsTerm,CurID,NewID,ActionString), |
| 1291 | | tcltk_goto_state(ActionAsTerm,NewID). |
| 1292 | | % 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 |
| 1293 | | %translate_event(ActionAsTerm,ActionString). |
| 1294 | | |
| 1295 | | % perform the Action with term ActionAsTerm leading to new state NewID |
| 1296 | | tcltk_perform_action_term(ActionAsTerm,NewID) :- %print(tcltk_perform_action_term(Action,ActionAsTerm,NewID)),nl, |
| 1297 | | (var(ActionAsTerm) |
| 1298 | | -> add_internal_error('Illegal call: ',tcltk_perform_action_term(ActionAsTerm,NewID)) ; true), |
| 1299 | | tcltk_goto_state(ActionAsTerm,NewID). |
| 1300 | | |
| 1301 | | /* allows one to execute an action in term form, from the current state: */ |
| 1302 | | %tcltk_perform_action(T,Cur) :- print_message(perf(T,Cur)),fail. |
| 1303 | | |
| 1304 | | tcltk_perform_action(ActionAsTerm,NewID) :- |
| 1305 | | current_state_id(CurID), |
| 1306 | | tcltk_perform_action(CurID,ActionAsTerm,NewID). |
| 1307 | | tcltk_perform_action(CurID,ActionAsTerm,NewID) :- |
| 1308 | | tcltk_perform_action(CurID,ActionAsTerm,NewID,_). |
| 1309 | | tcltk_perform_action(CurID,ActionAsTerm,TransitionID,NewStateID) :- |
| 1310 | | transition(CurID,ActionAsTerm,TransitionID,NewStateID), |
| 1311 | | tcltk_goto_state(ActionAsTerm,NewStateID). |
| 1312 | | |
| 1313 | | tcltk_no_constants_or_no_inititalisation_found :- |
| 1314 | | current_state_id(CurID), |
| 1315 | | (CurID=root ; is_concrete_constants_state_id(CurID)), |
| 1316 | | \+ candidate_setup_constants_or_init(CurID,_), |
| 1317 | | current_options([]). |
| 1318 | | |
| 1319 | | |
| 1320 | | |
| 1321 | | /* ------------ */ |
| 1322 | | /* tcltk_open/1 */ |
| 1323 | | /* ------------ */ |
| 1324 | | |
| 1325 | | |
| 1326 | | %prolog_check_load_errors :- |
| 1327 | | % (tcltk_find_untyped_consts(ErrRes) |
| 1328 | | % -> add_error(prolog_open,'These constants were not given a proper type:', ErrRes) |
| 1329 | | % ; true), |
| 1330 | | % (tcltk_find_untyped_vars(ErrRes) |
| 1331 | | % -> add_error(prolog_open,'These variables were not given a proper type:', ErrRes) |
| 1332 | | % ; true). |
| 1333 | | |
| 1334 | | tcltk_open_b_file_for_minor_mode(File,Minor) :- tcltk_open_b_file(File), |
| 1335 | | set_animation_minor_mode(Minor). |
| 1336 | | |
| 1337 | | tcltk_open_b_file(File) :- |
| 1338 | | tcltk_clear_machine, |
| 1339 | | set_animation_mode(b), |
| 1340 | | print_message(loading_b_file(File)),flush_output, |
| 1341 | | set_currently_opening_file(File), |
| 1342 | | % to do: b_load_machine_probfile |
| 1343 | | (b_load_aux(File) |
| 1344 | | -> print_message(loaded), |
| 1345 | | set_currently_opened_b_file(File) |
| 1346 | | ; tcltk_set_failed_to_open_file(File), |
| 1347 | | fail |
| 1348 | | ). |
| 1349 | | |
| 1350 | | tcltk_set_failed_to_open_file(File) :- |
| 1351 | | set_failed_to_open_file(File), |
| 1352 | | copy_current_errors_to_state(root,loading_context(File)). |
| 1353 | | |
| 1354 | | :- use_module(probsrc(bmachine), [b_load_machine_from_file/1,b_load_machine_probfile/1]). |
| 1355 | | :- use_module(tools,[get_filename_extension/2]). |
| 1356 | | b_load_aux(File) :- get_filename_extension(File,'prob'),!, |
| 1357 | | b_load_machine_probfile(File). |
| 1358 | | b_load_aux(File) :- |
| 1359 | | b_load_machine_from_file(File). |
| 1360 | | |
| 1361 | | :- use_module(xtl_interface,[open_xtl_file/1]). |
| 1362 | | tcltk_open_xtl_file(File) :- % TODO: redundant wrt load_xtl_spec_from_prolog_file |
| 1363 | | tcltk_clear_machine, |
| 1364 | | set_animation_mode(xtl), |
| 1365 | | set_currently_opening_file(File), |
| 1366 | | (open_xtl_file(File) |
| 1367 | | -> set_currently_opened_file(File) |
| 1368 | | ; tcltk_set_failed_to_open_file(File), fail). |
| 1369 | | |
| 1370 | | |
| 1371 | | tcltk_open_cspm_file(File) :- |
| 1372 | | tcltk_clear_machine, |
| 1373 | | set_animation_mode(cspm), |
| 1374 | | set_currently_opening_file(File), |
| 1375 | | (xtl_interface:open_cspm_file(File) |
| 1376 | | -> set_currently_opened_file(File) |
| 1377 | | ; tcltk_set_failed_to_open_file(File), fail). |
| 1378 | | |
| 1379 | | :- use_module(xtl_interface). |
| 1380 | | %tcltk_open_promela_file(File) :- |
| 1381 | | % tcltk_clear_machine, |
| 1382 | | % set_animation_mode(promela), set_currently_opening_file(File), |
| 1383 | | % xtl_interface:open_promela_file(File), set_currently_opened_file(File). |
| 1384 | | |
| 1385 | | % disabled because Java parser seems broken |
| 1386 | | %tcltk_open_smv_file(File) :- |
| 1387 | | % tcltk_clear_machine, |
| 1388 | | % set_animation_mode(smv), set_currently_opening_file(File), |
| 1389 | | % xtl_interface:open_smv_file(File), set_currently_opened_file(File). |
| 1390 | | |
| 1391 | | :- use_module(specfile,[type_check_csp_and_b/0]). |
| 1392 | | :- use_module(library(file_systems),[file_exists/1,delete_file/1]). |
| 1393 | | |
| 1394 | | tcltk_add_csp_file(File) :- |
| 1395 | | \+ file_exists(File),!, |
| 1396 | | add_error(csp_guide,'CSP guide file does not exist:',File). |
| 1397 | | tcltk_add_csp_file(File) :- |
| 1398 | | unset_animation_minor_modes(L), % we could be in z or tla or eventb mode |
| 1399 | | set_animation_mode(csp_and_b), |
| 1400 | | reset_animation_minor_modes(L), |
| 1401 | | xtl_interface:open_cspm_file(File), |
| 1402 | | notify_change_of_animation_mode, |
| 1403 | | debug_format(19,'Added csp-guide file ~w~n',[File]), |
| 1404 | | type_check_csp_and_b. |
| 1405 | | |
| 1406 | | notify_change_of_animation_mode :- |
| 1407 | | announce_event(change_of_animation_mode). |
| 1408 | | % clear_applicable_flag. % no done via event handling |
| 1409 | | |
| 1410 | | |
| 1411 | | tcltk_open_z_file(File) :- |
| 1412 | | tcltk_clear_machine, |
| 1413 | | tcltk_open_z_file2(File). |
| 1414 | | tcltk_open_z_file2(File) :- |
| 1415 | | set_currently_opening_file(File), |
| 1416 | ? | open_proz_file(File,BMachine), |
| 1417 | | set_animation_mode(b), set_animation_minor_mode(z), |
| 1418 | | b_set_typed_machine(BMachine,File), |
| 1419 | | !, |
| 1420 | | set_currently_opened_b_file(File). |
| 1421 | | tcltk_open_z_file2(File) :- tcltk_set_failed_to_open_file(File),fail. |
| 1422 | | |
| 1423 | | :- use_module(parsercall,[call_fuzz_parser/2]). |
| 1424 | | tcltk_open_z_tex_file(TexFile) :- |
| 1425 | | tcltk_clear_machine, |
| 1426 | ? | call_fuzz_parser(TexFile,FuzzFile), |
| 1427 | | tcltk_open_z_file2(FuzzFile). |
| 1428 | | |
| 1429 | | |
| 1430 | | :- use_module(eclipse_interface,[load_eventb_file/1]). |
| 1431 | | tcltk_load_packaged_eventb_file(File) :- |
| 1432 | | tcltk_clear_machine, |
| 1433 | | load_eventb_file(File). |
| 1434 | | |
| 1435 | | :- use_module(parsercall,[call_alloy2pl_parser/2]). |
| 1436 | | :- use_module(probsrc('alloy2b/alloy2b')). |
| 1437 | | tcltk_open_alloy_file(AlloyFile) :- |
| 1438 | | tcltk_clear_machine, |
| 1439 | | start_ms_timer(T1), |
| 1440 | | formatsilent('Parsing Alloy file: ~w~n',[AlloyFile]), |
| 1441 | | set_currently_opening_file(AlloyFile), |
| 1442 | | call_alloy2pl_parser(AlloyFile,PrologFile), |
| 1443 | | (silent_mode(off) -> stop_ms_walltimer_with_msg(T1,'parsing and type checking: ') ; true), |
| 1444 | | %printsilent(generated_prolog_ast(PrologFile)),nls, |
| 1445 | | start_ms_timer(T2), |
| 1446 | | ( load_alloy_ast_prolog_file(PrologFile) |
| 1447 | | -> true |
| 1448 | | ; delete_file(PrologFile), % delete parsed Prolog file if model couldn't be loaded |
| 1449 | | fail % since it's potentially empty due to the failure |
| 1450 | | ), |
| 1451 | | !, |
| 1452 | | (silent_mode(off) -> stop_ms_walltimer_with_msg(T2,'loading and translation to B: ') ; true), |
| 1453 | | set_currently_opened_b_file(AlloyFile). |
| 1454 | | tcltk_open_alloy_file(AlloyFile) :- tcltk_set_failed_to_open_file(AlloyFile),fail. |
| 1455 | | |
| 1456 | | |
| 1457 | | tcltk_open_alloy_prolog_ast_file(AlloyPrologFile) :- |
| 1458 | | tcltk_clear_machine, |
| 1459 | | start_ms_timer(T2), |
| 1460 | | load_alloy_ast_prolog_file(AlloyPrologFile), |
| 1461 | | !, |
| 1462 | | (silent_mode(off) -> stop_ms_walltimer_with_msg(T2,'loading B translation of Alloy: ') ; true), |
| 1463 | | set_currently_opened_b_file(AlloyPrologFile). |
| 1464 | | |
| 1465 | | %% tcltk_load_alloy_cmd_in_current_translation(+CmdName). |
| 1466 | | tcltk_load_alloy_cmd_in_current_translation(CmdName) :- |
| 1467 | | alloy2b:load_command_in_current_translation(CmdName). |
| 1468 | | |
| 1469 | | %% tcltk_get_alloy_cmd_names(-CmdNames). |
| 1470 | | tcltk_get_alloy_cmd_names(CmdNames) :- |
| 1471 | | alloy2b:get_command_names(CmdNames). |
| 1472 | | |
| 1473 | | %% tcltk_verify_alloy_cmd(+CmdName, +SolverName, -CmdIsValid, -IsCheckCmd). |
| 1474 | | tcltk_verify_alloy_cmd(CmdName, SolverName, CmdIsValid, IsCheckCmd) :- |
| 1475 | | verify_alloy_command(CmdName, SolverName, CmdIsValid, IsCheckCmd, Res), |
| 1476 | | ( Res = solution(Bindings) |
| 1477 | | -> bindings_to_state(Bindings, State), |
| 1478 | | tcltk_add_cbc_state(State, CmdName) |
| 1479 | | ; true |
| 1480 | | ). |
| 1481 | | |
| 1482 | | bindings_to_state([], []). |
| 1483 | | bindings_to_state([Binding|T], [Bind|NT]) :- |
| 1484 | | (Binding = binding(Id,Val,_); Binding = bind(Id,Val)), |
| 1485 | | Bind = bind(Id,Val), |
| 1486 | | bindings_to_state(T, NT). |
| 1487 | | |
| 1488 | | /* --------------------------------------------------------------------- */ |
| 1489 | | |
| 1490 | | tcltk_exists_an_open_node :- |
| 1491 | | not_all_transitions_added(_) ; not_interesting(_). |
| 1492 | | tcltk_goto_an_open_node :- |
| 1493 | | (not_all_transitions_added(ID) ; not_interesting(ID)),!, |
| 1494 | | tcltk_goto_state(find_open_node,ID). |
| 1495 | | tcltk_goto_max_reached_node :- |
| 1496 | | (max_reached_for_node(ID) ; time_out_for_node(ID)),!, |
| 1497 | | tcltk_execute_trace_to_node(ID). |
| 1498 | | tcltk_goto_timeout_node :- |
| 1499 | | time_out_for_node(ID),!, |
| 1500 | | tcltk_execute_trace_to_node(ID). |
| 1501 | | % tcltk_goto_state(find_max_reached_node,ID). |
| 1502 | | |
| 1503 | | tcltk_goto_an_invariant_violation :- |
| 1504 | | invariant_violated(ID),!, |
| 1505 | | tcltk_goto_state(find_inv_violation,ID). |
| 1506 | | |
| 1507 | | |
| 1508 | | tcltk_goto_node_with_id(ToID) :- |
| 1509 | | current_state_id(ToID),!. |
| 1510 | | tcltk_goto_node_with_id(ID) :- |
| 1511 | | visited_expression_id(ID), |
| 1512 | | tcltk_execute_trace_to_node(ID). |
| 1513 | | |
| 1514 | | tcltk_try_goto_node_with_id(ID) :- |
| 1515 | | (tcltk_goto_node_with_id(ID) -> true |
| 1516 | | ; add_internal_error('Call failed:',tcltk_goto_node_with_id(ID))). |
| 1517 | | |
| 1518 | | /* --------------------------------------------------------------------- */ |
| 1519 | | |
| 1520 | | % TO DO: clean up and move into model_checker module |
| 1521 | | |
| 1522 | ? | tcltk_state_space_only_has_root_node :- transition(root,_,ID), |
| 1523 | | \+ not_all_transitions_added(ID),!,fail. |
| 1524 | | tcltk_state_space_only_has_root_node. |
| 1525 | | |
| 1526 | | tcltk_search_among_existing_nodes(TclTkRes,FindDeadlocks,FindInvViolations, |
| 1527 | | FindGoal,FindAssViolations,FindStateErrors) :- |
| 1528 | | search_among_existing_nodes(Res,FindDeadlocks,FindInvViolations, |
| 1529 | | FindGoal,FindAssViolations,FindStateErrors), |
| 1530 | | translate_error_for_tclk(Res,TclTkRes). |
| 1531 | | |
| 1532 | | % 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 |
| 1533 | | % TODO: process mc_continue_after_error preference |
| 1534 | | search_among_existing_nodes(invariant_violation,_FindDeadlocks,FindInvViolations, |
| 1535 | | _FindGoal,_FindAssViolations,_FindStateErrors) :- |
| 1536 | | (get_state_space_stats(_,_,PrN), PrN>100 |
| 1537 | | -> print_message('Search Among Processed Nodes'), print_message(number_of_nodes(PrN)) ; true), |
| 1538 | | FindInvViolations=1, |
| 1539 | ? | (invariant_violated(ResID) -> true |
| 1540 | | ; find_invariant_violation_among_not_checked_nodes(ResID)), |
| 1541 | | tcltk_execute_trace_to_node(ResID). |
| 1542 | | search_among_existing_nodes(Error,_FindDeadlocks,FindInvViolations, |
| 1543 | | _FindGoal,_FindAssViolations,_FindStateErrors) :- |
| 1544 | | FindInvViolations=1, |
| 1545 | | find_xtl_csp_invariant_violation_among_all_existing_nodes(ResID,Error), % could be xtl_error |
| 1546 | | tcltk_execute_trace_to_node(ResID). |
| 1547 | | search_among_existing_nodes(DEADLOCK,FindDeadlocks,_,_,_,_) :- |
| 1548 | | FindDeadlocks=1, |
| 1549 | ? | visited_expression_id(ResID), |
| 1550 | | transitions_computed_for_node(ResID), |
| 1551 | | is_deadlocked(ResID), |
| 1552 | | (time_out_for_node(ResID) |
| 1553 | | -> DEADLOCK = possible_deadlock_timeout |
| 1554 | | ; get_preference(store_only_one_incoming_transition,true) -> DEADLOCK = possible_deadlock |
| 1555 | | ; DEADLOCK = deadlock), |
| 1556 | | print_message(deadlock_among_existing_nodes(ResID)), |
| 1557 | | tcltk_execute_trace_to_node(ResID). |
| 1558 | | search_among_existing_nodes(goal_found,_,_,FindGoal,_,_) :- |
| 1559 | | FindGoal=1, |
| 1560 | | %visited_expression(ResID,_CurState), |
| 1561 | | %\+(not_all_transitions_added(ResID)), % if commented out: will also look at open nodes |
| 1562 | | node_satisfies_goal(ResID), |
| 1563 | | tcltk_execute_trace_to_node(ResID). |
| 1564 | | search_among_existing_nodes(assertion_violation,_,_,_,FindAssViolations,_) :- |
| 1565 | | FindAssViolations=1, |
| 1566 | | b_machine_has_assertions, |
| 1567 | ? | visited_expression(ResID,CurState), |
| 1568 | | transitions_computed_for_node(ResID), |
| 1569 | | state_violates_assertions(ResID,CurState), |
| 1570 | | tcltk_execute_trace_to_node(ResID). |
| 1571 | | search_among_existing_nodes(ERR,_,_,_,_,FindStateErrors) :- FindStateErrors=1, |
| 1572 | ? | state_space:state_error(ResID,_,Error), Error \== invariant_violated, |
| 1573 | | (Error = abort_error(ERR,_,_,_) -> true ; ERR = state_error(Error)), |
| 1574 | | tcltk_execute_trace_to_node(ResID). |
| 1575 | | search_among_existing_nodes(all,_,_,_,_,_). |
| 1576 | | |
| 1577 | | |
| 1578 | | compute_all_transitions_if_necessary :- |
| 1579 | | current_state_id(CurID), |
| 1580 | | compute_all_transitions_if_necessary(CurID,false). |
| 1581 | | :- public compute_all_transitions_if_necessary/1. |
| 1582 | | compute_all_transitions_if_necessary(CurID) :- |
| 1583 | | compute_all_transitions_if_necessary(CurID,false). |
| 1584 | | |
| 1585 | | compute_all_transitions_if_necessary(CurID,CheckInvariant) :- |
| 1586 | | (retract_open_node(CurID) % will assert not_invariant_checked |
| 1587 | | -> set_context_state(CurID), |
| 1588 | | % first check invariant, relevant if we want to use specialized_inv proof information |
| 1589 | | visited_expression(CurID,State), |
| 1590 | | % TO DO: this does not expand concrete_constants: the expansion may be done twice below: |
| 1591 | | % once for compute_invariant (corresponds_to_b...) and once for compute_all_transitions (prepare_state_for_specfile_trans) |
| 1592 | | prepare_state_for_specfile_trans(State,CurID,PreparedState), |
| 1593 | | (CheckInvariant==true |
| 1594 | | -> compute_invariant_if_necessary_and_requested(CurID,PreparedState) ; true), |
| 1595 | | compute_all_transitions(CurID,PreparedState), |
| 1596 | | clear_context_state |
| 1597 | | ; true). |
| 1598 | | %compute_all_transitions_if_necessary(CurID,CurState) :- |
| 1599 | | % ((not_all_transitions_added(CurID);not_interesting(CurID)) |
| 1600 | | % -> compute_all_transitions(CurID,CurState) ; true). |
| 1601 | | |
| 1602 | | |
| 1603 | | compute_invariant_if_necessary_and_requested(ID,State) :- |
| 1604 | | 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 |
| 1605 | | compute_invariant_if_necessary(ID,State), |
| 1606 | | exit_error_scope(ErrScID,_ErrOcc,compute_invariant_if_necessary_and_requested). % should we do something with error occured result ? |
| 1607 | | |
| 1608 | | compute_invariant_if_necessary(ID,State) :- |
| 1609 | | animation_mode(MODE),compute_invariant_if_necessary(ID,State,MODE). |
| 1610 | | compute_invariant_if_necessary(ID,State,MODE) :- |
| 1611 | | ( check_invariantKO(MODE,ID,State) -> true ; true). |
| 1612 | | |
| 1613 | | check_invariantKO(ID,State) :- |
| 1614 | | animation_mode(MODE),check_invariantKO(MODE,ID,State). |
| 1615 | | check_invariantKO(b,ID,State) :- |
| 1616 | | check_invariantKO2(ID,State). |
| 1617 | | check_invariantKO(csp_and_b,ID,State) :- |
| 1618 | | check_invariantKO2(ID,State). |
| 1619 | | % for XTL we do not use not_invariant_checked/1 facts; one should call xtl_invariant_violated/1 |
| 1620 | | |
| 1621 | | % check invariant for B state |
| 1622 | | check_invariantKO2(ID,_) :- invariant_violated(ID),!. |
| 1623 | | check_invariantKO2(ID,CurState) :- |
| 1624 | ? | set_invariant_checked(ID), % only succeeds if we haven't checked invariant for ID yet |
| 1625 | | % print(check_inv(ID)),nl, |
| 1626 | | state_corresponds_to_initialised_b_machine(CurState), |
| 1627 | | ( preferences:preference(do_invariant_checking,false) -> assertz(not_invariant_checked(ID)) |
| 1628 | | ; force_check_invariantKO(ID,CurState)). |
| 1629 | | |
| 1630 | | |
| 1631 | | force_check_invariantKO(ID,CurBState) :- |
| 1632 | | % Note: this checks the invariant without setting up a new error scope |
| 1633 | | % (Reason: in the model checker it would be relatively expensive to set up an error scope for each state |
| 1634 | | % the model checker stops anyway when the first error is found and then exits its error scope) |
| 1635 | | catch_clpfd_overflow_call_for_state(ID, 'checking invariants', |
| 1636 | | b_state_violates_invariant(ID,CurBState),true) -> |
| 1637 | | %(b_state_violates_invariant(ID,CurBState) -> |
| 1638 | | set_invariant_violated(ID). |
| 1639 | | % TO DO ?: call state_satisfies_negation_of_invariant if double_evaluation_when_analysing is true ? |
| 1640 | | |
| 1641 | | % try and find an invariant violation among those nodes that have not yet been checked |
| 1642 | | find_invariant_violation_among_not_checked_nodes(ID) :- |
| 1643 | ? | retract(not_invariant_checked(ID)), %print(checking_invariant(ID)),nl, |
| 1644 | | visited_expression(ID,State), |
| 1645 | | state_corresponds_to_initialised_b_machine(State), |
| 1646 | | prepare_state_for_specfile_trans(State,ID,CurBState), |
| 1647 | | force_check_invariantKO(ID,CurBState). |
| 1648 | | |
| 1649 | | find_xtl_csp_invariant_violation_among_all_existing_nodes(ID,Error) :- |
| 1650 | | animation_mode(MODE), |
| 1651 | | (MODE=xtl ; MODE=csp), % invariant violations not stored, hence we need to re-check every node |
| 1652 | ? | visited_expression(ID,State), |
| 1653 | | find_invariant_error(MODE,ID,State,Error). % csp_error or xtl_error |
| 1654 | | |
| 1655 | | :- use_module(probporsrc(ample_sets),[compute_ample_set2/3]). |
| 1656 | | % computing ample sets (model_checker.pl) |
| 1657 | | compute_ample_set(CurID,CurState,POROptions) :- |
| 1658 | | catch_clpfd_overflow_call_for_state(CurID,'computing ample sets for POR', |
| 1659 | | compute_ample_set2(CurID,CurState,POROptions),clear_context_state). |
| 1660 | | |
| 1661 | | |
| 1662 | | %compute_all_transitions(CurID,CurState) :- get_preference(use_clpfd_solver,false),!, |
| 1663 | | % compute_all_transitions2(CurID,CurState). % in principle this overflow cannot/should not happen with CLPFD FALSE |
| 1664 | | % but no performance benefit can be measured by removing the catch |
| 1665 | | compute_all_transitions(CurID,CurState) :- |
| 1666 | | catch_clpfd_overflow_call_for_state(CurID,'computing all enabled transitions', |
| 1667 | | compute_all_transitions2(CurID,CurState),clear_context_state). |
| 1668 | | |
| 1669 | | |
| 1670 | | %catch_clpfd_overflow_call_for_state(_CurID, Call,_ExtraCleanUpCode) :- |
| 1671 | | % preferences:preference(use_clpfd_solver,false),!, % Overflow should not occur |
| 1672 | | % call(Call). |
| 1673 | | :- use_module(clpfd_interface,[catch_clpfd_overflow_call2/2]). |
| 1674 | | catch_clpfd_overflow_call_for_state(CurID, Context, Call,ExtraCleanUpCode) :- |
| 1675 | | catch_clpfd_overflow_call2(Call, |
| 1676 | | ( store_state_error(CurID,clpfd_overflow_error(Context),_), |
| 1677 | | call(ExtraCleanUpCode)) ). |
| 1678 | | |
| 1679 | | |
| 1680 | | |
| 1681 | | |
| 1682 | | :- use_module(probsrc(succeed_max),[reset_max_reached/0,max_reached/0, max_reached/1]). |
| 1683 | | compute_all_transitions2(CurID,CurState) :- /* compute all outgoing transitions for a given node */ |
| 1684 | | % set_context_state(CurID), % error_context is set for each operation below anyway. |
| 1685 | | reset_max_reached, |
| 1686 | | prepare_state_for_specfile_trans(CurState,CurID,PreparedCurState), % will perform unpacking of constants just once, for example |
| 1687 | | ((time_out_preference_disabled % e.g., when using probcli -disable_time_out |
| 1688 | | ; use_no_timeout(CurID)) |
| 1689 | | -> add_transitions_fail_loop(CurID,PreparedCurState) |
| 1690 | | ; preferences:preference(time_out,CurTO), |
| 1691 | | add_transitions__with_timeout_fail_loop(CurID,PreparedCurState,CurTO) |
| 1692 | | ), |
| 1693 | | add_partial_transitions(CurID,PreparedCurState), % also copies unsat component infos |
| 1694 | | (max_reached -> assert_max_reached_for_node(CurID),MaxReached=true ; MaxReached=false), |
| 1695 | | % TO DO: use max_reached(OpID) |
| 1696 | | (CurID==root -> save_constants(MaxReached) ; add_new_transitions_to_cache(CurID)) |
| 1697 | | . %,clear_context_state. |
| 1698 | | |
| 1699 | | :- use_module(error_manager,[get_virtual_time_out_from_exception/2]). % used by time_out_with_enum_warning_for_findall |
| 1700 | | % loop to compute successor states without a time_out |
| 1701 | | add_transitions_fail_loop(CurID,CurState) :- |
| 1702 | | catch( |
| 1703 | | add_transitions_fail_loop2(CurID,CurState,TimeOutRes), |
| 1704 | | Exc, |
| 1705 | | get_virtual_time_out_from_exception(Exc,TimeOutRes)), |
| 1706 | | (nonvar(TimeOutRes), |
| 1707 | | (TimeOutRes=operation_time_out(Op,TimeOutRes2) |
| 1708 | | -> assert_time_out_for_node(CurID,Op,TimeOutRes2) |
| 1709 | | ; assert_time_out_for_node(CurID,'unspecified_operation',TimeOutRes)) |
| 1710 | | ; true). |
| 1711 | | |
| 1712 | | add_transitions_fail_loop2(CurID,CurState,_) :- |
| 1713 | ? | possible_trans_name_for_successors(CurState,ActionName), |
| 1714 | | % we could check pge info here (e.g., store one Predecessor ID and look if ActionName can be enabled after) |
| 1715 | | set_error_context(operation(ActionName,CurID)), |
| 1716 | ? | add_transition(CurID,CurState,ActionName,_NewId), % TO DO: transmit animation_mode value? |
| 1717 | | fail. |
| 1718 | | add_transitions_fail_loop2(_,_,OpTimeOutRes) :- |
| 1719 | | (enumeration_warning_occured_in_error_scope |
| 1720 | | -> (virtual_time_out_occured_in_error_scope(TimeOutRes) |
| 1721 | | -> % i.e., critical enumeration warning occurred |
| 1722 | | (get_error_context(operation(ActionName,_)) |
| 1723 | | -> OpTimeOutRes = operation_time_out(ActionName,TimeOutRes) |
| 1724 | | ; OpTimeOutRes = operation_time_out('unspecified_operation',TimeOutRes)) |
| 1725 | | ; true), |
| 1726 | | clear_enumeration_warnings |
| 1727 | | ; true % no warnings: sunshine case |
| 1728 | | ), |
| 1729 | | clear_error_context. |
| 1730 | | |
| 1731 | | possible_trans_name_for_successors(CurState,ActionName) :- |
| 1732 | ? | specfile_possible_trans_name_for_successors(CurState,ActionName), |
| 1733 | | (preference(store_only_one_incoming_transition,true), % SAFETY_MODEL_CHECK |
| 1734 | | nonvar(ActionName), |
| 1735 | | b_or_z_mode, |
| 1736 | | b_operation_cannot_modify_state(ActionName) % we have a skip operation |
| 1737 | | -> operation_not_yet_covered(ActionName) |
| 1738 | | % if operation covered: all we could is create a self-loop, which would not be added to the state space anyway |
| 1739 | | ; true). |
| 1740 | | |
| 1741 | | |
| 1742 | | :- use_module(library(timeout),[time_out/3]). |
| 1743 | | my_timeout_test(1000000) :- write('.'), !, my_timeout_test(0). |
| 1744 | | my_timeout_test(X) :- X1 is X+1, my_timeout_test(X1). |
| 1745 | | :- public my_timeout_test/0. |
| 1746 | | my_timeout_test :- time_out(my_timeout_test(0),500,TO), nl, |
| 1747 | | print(time_out_result(TO)),nl, TO==time_out. |
| 1748 | | :- assert_must_succeed(tcltk_interface:my_timeout_test). |
| 1749 | | |
| 1750 | | add_transitions__with_timeout_fail_loop(CurID,CurState,CurTO) :- |
| 1751 | | enter_new_error_scope(Level,add_transitions__with_timeout_fail_loop), |
| 1752 | | call_cleanup(add_transitions__with_timeout_fail_loop2(Level,CurID,CurState,CurTO), |
| 1753 | | exit_error_scope(Level,_,add_transitions__with_timeout_fail_loop)). |
| 1754 | | |
| 1755 | | % old profiler |
| 1756 | | :- use_module(runtime_profiler,[profile_failure_driven_loop/2]). |
| 1757 | | |
| 1758 | | % the loop to compute all successors of state CurID with a time-out |
| 1759 | | add_transitions__with_timeout_fail_loop2(Level,CurID,CurState,CurTO) :- % statistics(runtime,_), |
| 1760 | | % TO DO: prepare computing the state: expanding const and vars, unpacking, ... |
| 1761 | ? | possible_trans_name_for_successors(CurState,ActionName), |
| 1762 | ? | profile_failure_driven_loop(ActionName,CurID), |
| 1763 | | % Note: we enumerate possible transition names so that we can catch the time-out per name ! |
| 1764 | | % statistics(runtime,[T1,DeltaT]), print(delta_time(ActionName,DeltaT)),nl, %% |
| 1765 | | % first enumerate possible Operations/... to obtain timeout per operation/... |
| 1766 | | % TO DO: divide CurTO by number of transitions ??? |
| 1767 | | % We could also decide to have one time-out per state, only if that one is triggered move to |
| 1768 | | % finer-grained timeouts |
| 1769 | | % 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 |
| 1770 | | % In SICS 4.3.5 the runtime increased from 1.480 to 2.270 seconds = 0.022 ms per timeout call |
| 1771 | | % In SICS 4.4.1 the runtime increased from 1.494 to 3.033 seconds. = 0.044 ms per timeout call. |
| 1772 | | %% statistics(runtime,[T1,_]), print(try(ActionName,T1)),nl,%% |
| 1773 | | set_error_context(operation(ActionName,CurID)), |
| 1774 | | (nonvar(ActionName),translate_operation_name(ActionName,A2), |
| 1775 | | get_specific_time_out_for_operation(A2,RealTimeOut) -> true ; RealTimeOut = CurTO), |
| 1776 | ? | time_out_with_enum_warning_for_findall_in_current_error_scope(Level, |
| 1777 | | (add_transition(CurID,CurState,ActionName,_NewId),fail), % fail inside meta-call; |
| 1778 | | % so that time_out is for entire add_transition loop; not just for each single solution |
| 1779 | | RealTimeOut,TimeOutRes), |
| 1780 | | %% statistics(runtime,[T2,_]), TDiff is T2-T1, print(added_transition(CurID,ActionName,TDiff,TimeOutRes)),nl, %% |
| 1781 | | %% add_transition(CurID,CurState,ActionName,_NewId) , |
| 1782 | | ((TimeOutRes==time_out ; |
| 1783 | | nonvar(TimeOutRes),TimeOutRes=virtual_time_out(_), \+ max_reached(ActionName)) |
| 1784 | | % virtual time outs not relevant if we have already stopped earlier anyway; |
| 1785 | | % TO DO: does not seem to work for INITIALISATION |
| 1786 | | -> (TimeOutRes=virtual_time_out(_) -> true |
| 1787 | | ; print_message('TIME OUT: '),print_message(CurID), |
| 1788 | | print_message(RealTimeOut),print_message(ActionName) |
| 1789 | | ), |
| 1790 | | (var(ActionName) |
| 1791 | | -> assert_time_out_for_node(CurID,'unspecified_operation',TimeOutRes) |
| 1792 | | ; assert_time_out_for_node(CurID,ActionName,TimeOutRes) % TO DO: assert info per ActionSkeleton ? |
| 1793 | | ) |
| 1794 | | ; true |
| 1795 | | ),fail. |
| 1796 | | add_transitions__with_timeout_fail_loop2(_,_,_,_) :- clear_error_context. |
| 1797 | | % statistics(runtime,[_,DeltaT]), print(delta_time(end,DeltaT)),nl. |
| 1798 | | |
| 1799 | | % compute and add transition to next states |
| 1800 | | add_transition(CurID,CurState,ActionName,NewId) :- |
| 1801 | | /* ActionName maybe pre-instantiated */ |
| 1802 | | extract_infos_from_prepared_state(CurState,PrecomputedInfos), |
| 1803 | ? | specfile_trans(CurState,ActionName,Act,NewExpression,TransInfo,Residue), |
| 1804 | | %% print_bt_message(specfile_trans(CurState,ActionName,Act,NewExpression,TransInfo,Residue)), %% |
| 1805 | | add_trans_id_with_infos(CurID,PrecomputedInfos,Act,NewExpression,Residue,NewId,TransInfo,_). |
| 1806 | | |
| 1807 | | |
| 1808 | | % after being computed, add a new transition in the state space; adding the destination state if required |
| 1809 | | add_trans_id_with_infos(CurID,PrecomputedInfos,Act,NewExpression,Residue,NewID,TransInfo,TransId) :- |
| 1810 | | (Residue=[] -> true |
| 1811 | | ; add_error(add_trans_id,'Residue: ',CurID:Act:Residue), |
| 1812 | | tools_printing:print_goal(Residue),nl |
| 1813 | | ), |
| 1814 | | add_new_transition_transid_with_infos(CurID,PrecomputedInfos,Act,NewID,NewExpression,TransInfo,TransId). |
| 1815 | | |
| 1816 | | add_trans_id(CurID,Act,NewExpression,NewID,TransId) :- |
| 1817 | | add_trans_id_with_infos(CurID,[],Act,NewExpression,[],NewID,[],TransId). |
| 1818 | | |
| 1819 | | add_trans_id_infos(CurID,Act,NewExpression,NewID,TransId,TransInfos) :- |
| 1820 | | add_trans_id_with_infos(CurID,[],Act,NewExpression,[],NewID,TransInfos,TransId). |
| 1821 | | |
| 1822 | | add_partial_transitions(root,CurState) :- |
| 1823 | | /* for the moment the only state where partial transitions are computed */ |
| 1824 | ? | \+ any_transition(root,_,_), /* adding normal transitions was not successful */ |
| 1825 | | partial_trans(CurState,Act,NewExpression,Residue), |
| 1826 | | add_trans_id_with_infos(root,[],Act,NewExpression,Residue,_NewID,[],_),fail. |
| 1827 | | add_partial_transitions(_CurID,_). |
| 1828 | | |
| 1829 | | /* --------------------------------------------------------------------- */ |
| 1830 | | |
| 1831 | | /* A bit like AO* algorithm: expands open nodes (i.e., states whose transitions |
| 1832 | | have not yet been computed */ |
| 1833 | | |
| 1834 | | :- use_module(model_checker). |
| 1835 | | |
| 1836 | | tcltk_model_check(Nr,TclTkRes,FindDeadlocks,FindInvViolations,FindGoal,FindAssViolations, |
| 1837 | | FindStateErrors,StopFullCoverage,PartialOrderReduction,TIMELIMIT,TotalTime) :- |
| 1838 | | statistics(walltime,[CurTime,_]), /* get current time in ms */ |
| 1839 | | LimitTime is CurTime+TIMELIMIT, |
| 1840 | | %debug_println(10,start_tcltk_model_check(Nr,TIMELIMIT)), |
| 1841 | | InspectExistingNodes = 0, |
| 1842 | | (do_model_check(Nr,_A,LimitTime,Res,FindDeadlocks,FindInvViolations,FindGoal, |
| 1843 | | FindAssViolations,FindStateErrors,StopFullCoverage, |
| 1844 | | PartialOrderReduction,InspectExistingNodes) |
| 1845 | | -> translate_error_for_tclk(Res,TclTkRes) |
| 1846 | | ; add_internal_error('Call failed: ',do_model_check(Nr,_A,LimitTime,Res,FindDeadlocks,FindInvViolations,FindGoal, |
| 1847 | | FindAssViolations,FindStateErrors,StopFullCoverage, |
| 1848 | | PartialOrderReduction,InspectExistingNodes)), |
| 1849 | | TclTkRes=error), |
| 1850 | | statistics(walltime,[CurTime2,_]), |
| 1851 | | TotalTime is CurTime2-CurTime, |
| 1852 | | debug_println(10,tcltk_model_check(Nr,TotalTime,Res)). |
| 1853 | | |
| 1854 | | translate_error_for_tclk([timeout,Nr],Res) :- !, Res=[timeout,Nr]. |
| 1855 | | translate_error_for_tclk(state_error(S),String) :- !, translate_state_err_for_tcltk(S,String). |
| 1856 | | translate_error_for_tclk(S,R) :- atomic(S),!,R=S. |
| 1857 | | translate_error_for_tclk(S,R) :- nonvar(S), add_error(translate_error_for_tclk,'Unknown Model Check result: ',S), R=unknown. |
| 1858 | | |
| 1859 | | translate_state_err_for_tcltk(abort_error(TYPE,_,_,_),ERR) :- !, ERR = TYPE. |
| 1860 | | translate_state_err_for_tcltk(eventerror(Event,Error,_),ERR) :- !, |
| 1861 | | functor(Error,F,_), |
| 1862 | | ajoin(['event_error:',Event,':',F],ERR). |
| 1863 | | translate_state_err_for_tcltk(Error,ERR) :- |
| 1864 | | functor(Error, StateError, _), atom_concat('state_error:',StateError,ERR). |
| 1865 | | |
| 1866 | | |
| 1867 | | |
| 1868 | | do_model_check(_Nr,NodesAnalysed,_LimitTime,Res,FindDeadlocks,FindInvViolations,FindGoal, |
| 1869 | | FindAssViolations,FindStateErrors,_StopFullCoverage, |
| 1870 | | _PartialOrderReduction,ForceInspectExistingNodes) :- |
| 1871 | | (tcltk_state_space_only_has_root_node -> true % Then also look at the root node |
| 1872 | | ; ForceInspectExistingNodes == 1), |
| 1873 | ? | search_among_existing_nodes(Res,FindDeadlocks,FindInvViolations,FindGoal, |
| 1874 | | FindAssViolations,FindStateErrors), |
| 1875 | | Res \=all, NodesAnalysed=0. |
| 1876 | | do_model_check(LimitNr,NodesAnalysed,LimitTime,Res,FindDeadlocks,FindInvViolations,FindGoal, |
| 1877 | | FindAssViolations,FindStateErrors,StopFullCoverage,PartialOrderReduction,_) :- |
| 1878 | | update_ass(FindAssViolations,FindAssViolations2), |
| 1879 | | open_search(LimitNr,NodesAnalysed,LimitTime,Res,FindDeadlocks,FindInvViolations,FindGoal, |
| 1880 | | FindAssViolations2,FindStateErrors,StopFullCoverage,PartialOrderReduction). |
| 1881 | | |
| 1882 | | update_ass(1,FindAssViol) :- \+ b_machine_has_assertions,!, % no need to check assertions |
| 1883 | | FindAssViol=0. |
| 1884 | | update_ass(X,X). |
| 1885 | | |
| 1886 | | /* --------------------------------------------------- */ |
| 1887 | | |
| 1888 | | /* constraint-based checking of refinements */ |
| 1889 | | :- use_module(symbolic_model_checker(cbc_refinement_checks), [cbc_refinement_check/2]). |
| 1890 | | tcltk_cbc_refinement_check(list(List),ErrorOccured) :- |
| 1891 | ? | cbc_refinement_check(List,ErrorOccured). |
| 1892 | | |
| 1893 | | /* constraint-based/model search for invariant violations */ |
| 1894 | | |
| 1895 | | :- dynamic cbc_inv_error_found/2. |
| 1896 | | |
| 1897 | | tcltk_constraint_based_check(L) :- tcltk_constraint_based_check(L,_). |
| 1898 | | tcltk_constraint_based_check(list(List),ErrorsOrTimeoutWereFound) :- |
| 1899 | | retractall(cbc_inv_error_found(_,_)), |
| 1900 | | findall(Res, (tcltk_constraint_based_check_with_timeout(OpName,ErrorDesc), |
| 1901 | | (ErrorDesc=ok -> true ; assertz(cbc_inv_error_found(OpName,ErrorDesc))), |
| 1902 | | string_concatenate(' == ',ErrorDesc,Res1), |
| 1903 | | string_concatenate(OpName,Res1,Res)), List), |
| 1904 | | %%print(list(List)),nl, %% |
| 1905 | ? | (cbc_inv_error_found(_,_) -> |
| 1906 | ? | (cbc_inv_error_found(_,X),X\=time_out |
| 1907 | | -> ErrorsOrTimeoutWereFound=true ; ErrorsOrTimeoutWereFound=time_out |
| 1908 | | ) |
| 1909 | | ; ErrorsOrTimeoutWereFound = false). |
| 1910 | | |
| 1911 | | % can also be called with uninstantiated OpName |
| 1912 | | tcltk_constraint_based_check_with_timeout(OpName,ErrorDesc) :- |
| 1913 | | preferences:get_computed_preference(debug_time_out,DebugTimeOut), |
| 1914 | ? | valid_operation_or_init(OpName,IOpName), |
| 1915 | | (time_out_with_enum_warning_one_solution(tcltk_constraint_based_check_op(IOpName,ErrorDesc),DebugTimeOut,TimeOutRes) |
| 1916 | | -> (is_time_out_result(TimeOutRes) |
| 1917 | | -> print_message('TIME OUT: '), print_message(OpName), print_message(DebugTimeOut), |
| 1918 | | ErrorDesc = timeout |
| 1919 | | ; true |
| 1920 | | )). |
| 1921 | | valid_operation_or_init(OpName,R) :- OpName=='@INITIALISATION',!,R='$initialise_machine'. |
| 1922 | ? | valid_operation_or_init(OpName,OpName) :- b_get_machine_operation(OpName,_,_,_). |
| 1923 | | valid_operation_or_init('INITIALISATION','$initialise_machine'). % used e.g. in test 1821: -cbc INITIALISATION |
| 1924 | | |
| 1925 | | tcltk_constraint_based_check_op(OpName,ErrorDesc) :- |
| 1926 | | tcltk_constraint_based_check_op(OpName,invariant,ErrorDesc). |
| 1927 | | |
| 1928 | | tcltk_constraint_based_check_op(TclOpName,InvOrAssertion,ErrorDesc) :- |
| 1929 | | adapt_tcl_operation_name(TclOpName,OpName), |
| 1930 | | tcltk_constraint_based_check_op2(OpName,InvOrAssertion,ErrorDesc). |
| 1931 | | |
| 1932 | | % code below because names with $ cause problems in Tcl with eval |
| 1933 | | adapt_tcl_operation_name(X,R) :- var(X),!,R=X. |
| 1934 | | adapt_tcl_operation_name('@PROPERTIES','$setup_constants') :- !. |
| 1935 | | adapt_tcl_operation_name('@INITIALISATION','$initialise_machine') :- !. |
| 1936 | | adapt_tcl_operation_name(X,X). |
| 1937 | | |
| 1938 | | % a version that allows either invariant or assertions check after an Operation OpName |
| 1939 | | tcltk_constraint_based_check_op2(OpName,InvOrAssertion,ErrorDesc) :- |
| 1940 | | call_cbc_command(state_model_check(OpName,InvOrAssertion,State,Operation,NewState)),!, |
| 1941 | | tcltk_add_cbc_state(State,'$JUMP'(constraint_based_check),PriorID), % will also set history |
| 1942 | | translate_event(Operation,Action), |
| 1943 | | tcltk_add_new_transition_transid(PriorID,Operation,NewID,NewState,[],TransId2), |
| 1944 | | set_current_state_id(NewID), |
| 1945 | | add_to_op_trace_ids(TransId2), |
| 1946 | | add_id_to_history(PriorID), |
| 1947 | | ajoin([InvOrAssertion,'_violated_after(',Action,')'],ErrorDesc). |
| 1948 | | tcltk_constraint_based_check_op2(_,_,'ok'). |
| 1949 | | |
| 1950 | | |
| 1951 | | % try to find constants, parameters that make a given trace feasible |
| 1952 | | tcltk_cbc_find_trace(TraceToBeFound,Res) :- |
| 1953 | | tcltk_cbc_find_trace(TraceToBeFound,'',first_solution,Res). |
| 1954 | | |
| 1955 | | %:- public tcltk_cbc_find_invariant_violation/2. |
| 1956 | | %tcltk_cbc_find_invariant_violation(TraceToBeFound,Res) :- |
| 1957 | | % tcltk_cbc_find_trace(TraceToBeFound,'#not_invariant',first_solution,Res). |
| 1958 | | % could also call tcltk_constraint_based_check_op('$initialise_machine',invariant,Res) |
| 1959 | | |
| 1960 | | tcltk_cbc_find_trace(TraceToBeFound,TargetPredString,FindAll,Res) :- |
| 1961 | | b_parse_optional_machine_predicate(TargetPredString,TargetPred), |
| 1962 | | formatsilent('Looking for solution for trace ~w~n',[TraceToBeFound]), |
| 1963 | | split_atom(TraceToBeFound,[',',';',' '],TraceAsList), |
| 1964 | | (maplist(check_valid_operation,TraceAsList) |
| 1965 | | -> start_ms_timer(Timer), |
| 1966 | | tcltk_cbc_find_trace_aux(Timer,TraceAsList,TargetPred,FindAll,Res) |
| 1967 | | ; Res = error). |
| 1968 | | tcltk_cbc_find_trace_aux(Timer,TraceAsList,TargetPred,FindAll,Res) :- |
| 1969 | | preferences:get_computed_preference(debug_time_out,DebugTimeOut), |
| 1970 | | reset_nr_cbc_sols, |
| 1971 | | time_out_with_enum_warning_one_solution( |
| 1972 | | cbc_path_solver:create_testcase_path_nondet(init,TraceAsList,TargetPred,Transitions),DebugTimeOut,TimeOutRes), |
| 1973 | | stop_ms_timer(Timer), |
| 1974 | | (is_time_out_result(TimeOutRes) |
| 1975 | | -> !, |
| 1976 | | print_message('*** TIME OUT: '), print_message(DebugTimeOut), Res = time_out |
| 1977 | | ; FindAll = findall -> inc_nr_cbc_sols, |
| 1978 | | print('% *** FOUND PATH: '), maplist(print_trans,Transitions),nl, |
| 1979 | | fail % backtrack to find further solutions |
| 1980 | | ; !,Res = ok, |
| 1981 | | print('% *** FOUND PATH: '), maplist(print_trans,Transitions),nl, |
| 1982 | | maplist(extract_trans_id,Transitions,TransIds), |
| 1983 | | set_trace_by_transition_ids(TransIds) |
| 1984 | | ). |
| 1985 | | tcltk_cbc_find_trace_aux(Timer,_TraceToBeFound,_TargetPred,findall,R) :- !, stop_ms_timer(Timer), |
| 1986 | | R=nr_cbc_sols(Res), |
| 1987 | | nr_cbc_sols(Res), |
| 1988 | | print_message('*** ALL SOLUTIONS FOUND '). |
| 1989 | | tcltk_cbc_find_trace_aux(Timer,_TraceToBeFound,_TargetPred,_FindAll,no_solution_found) :- |
| 1990 | | stop_ms_timer(Timer), |
| 1991 | | print_message('*** NO SOLUTION FOUND'),nl. |
| 1992 | | |
| 1993 | | :- dynamic nr_cbc_sols/1. |
| 1994 | | nr_cbc_sols(0). |
| 1995 | | reset_nr_cbc_sols :- retractall(nr_cbc_sols(_)), assertz(nr_cbc_sols(0)). |
| 1996 | | inc_nr_cbc_sols :- |
| 1997 | | retract(nr_cbc_sols(N)), N1 is N+1, assertz(nr_cbc_sols(N1)). |
| 1998 | | extract_trans_id( (TransId,_,_,_), TransId). |
| 1999 | | print_trans( (_,Event,_,_)) :- translate_event(Event,S), print(S), print(' '). |
| 2000 | | |
| 2001 | | :- use_module(probsrc(tools_matching), [get_possible_top_level_event_matches_msg/2]). |
| 2002 | | check_valid_operation(Op) :- |
| 2003 | | (get_possible_language_specific_top_level_event(Op,_,_) -> true |
| 2004 | | ; (get_possible_top_level_event_matches_msg(Op,FMsg) |
| 2005 | | -> ajoin(['Unknown operation/event (did you mean ',FMsg,' ?):'],Msg) |
| 2006 | | ; Msg='Unknown operation/event:' |
| 2007 | | ), |
| 2008 | | add_error(cbc_find_sequence,Msg,Op), |
| 2009 | | fail |
| 2010 | | ). |
| 2011 | | |
| 2012 | | tk_get_possible_language_specific_top_level_event(OpName,list(ResultNames),list(ParameterNames)) :- |
| 2013 | | get_possible_language_specific_top_level_event(OpName,ResultNames,ParameterNames). |
| 2014 | | |
| 2015 | | |
| 2016 | | % ------------ |
| 2017 | | |
| 2018 | | :- use_module(bsyntaxtree). |
| 2019 | | tcltk_constraint_find_valid_state_with_pred(ParameterBindList,RestPreCond,UseConstantsFromStateID) :- |
| 2020 | | parse_tclk_parameter_values_and_pred('$initialise_machine',ParameterBindList,RestPreCond,CustomPredicate), |
| 2021 | | UseInvariant=true, |
| 2022 | | call_cbc_command( |
| 2023 | | b_state_model_check:b_set_up_valid_state_with_pred(State,CustomPredicate, |
| 2024 | | UseInvariant,UseConstantsFromStateID)), |
| 2025 | | tcltk_add_cbc_state(State,find_valid_state). |
| 2026 | | tcltk_constraint_find_valid_state :- |
| 2027 | | call_cbc_command(b_set_up_valid_state(State)), |
| 2028 | | tcltk_add_cbc_state(State,find_valid_state). |
| 2029 | | |
| 2030 | | :- use_module(extrasrc(optimizing_solver),[b_set_up_maximally_valid_state/2]). |
| 2031 | | tcltk_constraint_find_maximal_valid_state :- |
| 2032 | | current_state_id(ID), |
| 2033 | | call_cbc_command(b_set_up_maximally_valid_state(ID,State)), |
| 2034 | | tcltk_add_cbc_state(State,find_maximal_valid_state). |
| 2035 | | |
| 2036 | | |
| 2037 | | tcltk_constraint_find_dynamic_assertion_violation :- |
| 2038 | | call_cbc_command(b_find_dynamic_assertion_violation(State)), |
| 2039 | | tcltk_add_cbc_state(State,cbc_dynamic_assertions_check). |
| 2040 | | |
| 2041 | | :- use_module(clpfd_interface,[catch_clpfd_overflow_call1/1]). |
| 2042 | | :- use_module(error_manager,[call_in_fresh_error_scope_for_one_solution/1]). |
| 2043 | | % catch CLPFD overflows and catch other errors |
| 2044 | | call_cbc_command(Command) :- |
| 2045 | | call_in_fresh_error_scope_for_one_solution( |
| 2046 | | (catch_clpfd_overflow_call1(Command) -> true |
| 2047 | | ; translate_events_in_current_scope_to_warnings(cbc,'Warning: '),fail |
| 2048 | | % Maybe we should raise error when Command fails and enumeration warnings are there ? |
| 2049 | | )). |
| 2050 | | |
| 2051 | | |
| 2052 | | tcltk_constraint_find_deadlock_state(Res) :- |
| 2053 | | check_we_are_in_b_mode(cbc_deadlock_freedom_check), |
| 2054 | | create_texpr(truth,pred,[],True), |
| 2055 | | call_cbc_command(cbc_deadlock_freedom_check(State,True,0)), |
| 2056 | | (State == time_out -> Res = time_out |
| 2057 | | ; tcltk_add_cbc_state(State,cbc_deadlock), Res=deadlock). |
| 2058 | | |
| 2059 | | % if Filter=1 we remove guards which are inconsitent with goal |
| 2060 | | tcltk_constraint_find_deadlock_state_with_goal(Filter,Res) :- |
| 2061 | | check_we_are_in_b_mode(cbc_deadlock_freedom_check), |
| 2062 | | (b_get_machine_goal(Goal) -> true ; create_texpr(truth,pred,[],Goal)), |
| 2063 | | call_cbc_command(cbc_deadlock_freedom_check(State,Goal,Filter)), |
| 2064 | | (State == time_out -> Res = time_out |
| 2065 | | ; tcltk_add_cbc_state(State,cbc_deadlock), Res=deadlock). |
| 2066 | | |
| 2067 | | check_we_are_in_b_mode(_) :- b_or_z_mode,!. |
| 2068 | | 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. |
| 2069 | | |
| 2070 | | tcltk_constraint_find_deadlock_state_with_goal(true,_Filter,Res) :- |
| 2071 | | !,tcltk_constraint_find_deadlock_state(Res). |
| 2072 | | tcltk_constraint_find_deadlock_state_with_goal(GoalPred,Filter,Res) :- |
| 2073 | | bmachine:b_set_machine_goal(GoalPred), |
| 2074 | | tcltk_constraint_find_deadlock_state_with_goal(Filter,Res). |
| 2075 | | |
| 2076 | | :- use_module(cbcsrc(enabling_analysis),[check_if_feasible_operation/5]). |
| 2077 | | tcltk_check_if_feasible_operation(OpName,UseInvariant,TimeOutFactor,Result) :- % UseInvariant currently always 1 from Tcl |
| 2078 | | check_if_feasible_operation(OpName,UseInvariant,TimeOutFactor,Result,ResultState), |
| 2079 | | tcltk_add_cbc_state(ResultState,feasibility_check(OpName)). |
| 2080 | | |
| 2081 | | % add a state found by constraint-based verification or other method that tries to jump to a state without all intermediate steps |
| 2082 | | % it will add a separate concrete_constants state if necessary |
| 2083 | | tcltk_add_cbc_state(State,OpName) :- |
| 2084 | | tcltk_add_cbc_state(State,'$JUMP'(OpName),_ToID). |
| 2085 | | |
| 2086 | | tcltk_add_cbc_state('$UNKNOWN_STATE',_,To) :- !,To=none. |
| 2087 | | tcltk_add_cbc_state(State,OpNameTerm,NewID) :- |
| 2088 | | seperate_state_into_const_and_vars(State,Constants,Variables), |
| 2089 | | !, |
| 2090 | | % store the constants separately: important for memory consumption when continuing animation/model checking |
| 2091 | | (Variables=[] -> Op='$initialise_machine' ; Op = OpNameTerm), |
| 2092 | | % if Variables are [] we simply create an initialisation transition |
| 2093 | | (Constants = [] % no need to create SETUP_CONSTANTS transition |
| 2094 | | -> (Variables = [] % probably prior state for INITIALISATION cbc check |
| 2095 | | -> NewID=root, set_cbc_state(root,[],[]) |
| 2096 | | ; FullState = Variables, |
| 2097 | | tcltk_add_new_transition_transid(root,Op,NewID,FullState,[],TransId2), |
| 2098 | | set_cbc_state(NewID,[TransId2],[root]) |
| 2099 | | ) |
| 2100 | | ; tcltk_add_new_transition_transid(root,'$setup_constants',CstID,concrete_constants(Constants),[],TransId1), |
| 2101 | | FullState = const_and_vars(CstID,Variables), |
| 2102 | | tcltk_add_new_transition_transid(CstID,Op,NewID,FullState,[],TransId2), |
| 2103 | | set_cbc_state(NewID,[TransId1,TransId2],[CstID,root]) |
| 2104 | | ). |
| 2105 | | tcltk_add_cbc_state(State,OpNameTerm,NewID) :- |
| 2106 | | tcltk_add_new_transition_transid(root,OpNameTerm,NewID,State,[],TransId), |
| 2107 | | set_cbc_state(NewID,[TransId],[root]). |
| 2108 | | |
| 2109 | | |
| 2110 | | set_cbc_state(NewID,TransIds,His) :- |
| 2111 | | set_current_state_id(NewID), |
| 2112 | | reset_op_trace_ids, |
| 2113 | | maplist(add_to_op_trace_ids,TransIds), |
| 2114 | | retractall(history(_)), |
| 2115 | | retractall(forward_history(_)), |
| 2116 | | assertz(history(His)). %, print(State),nl. |
| 2117 | | |
| 2118 | | is_constant_binding(SortedCsts,bind(ID,_)) :- |
| 2119 | | ord_member(ID,SortedCsts). |
| 2120 | | |
| 2121 | | :- use_module(bsyntaxtree, [get_texpr_ids/2]). |
| 2122 | | seperate_state_into_const_and_vars(concrete_constants(C),Constants,Variables) :- !, |
| 2123 | | Constants=C, Variables=[]. |
| 2124 | | seperate_state_into_const_and_vars(State,Constants,Variables) :- |
| 2125 | | b_get_machine_constants(TCs), get_texpr_ids(TCs,Cs), |
| 2126 | | sort(Cs,SortedCsts), |
| 2127 | | include(is_constant_binding(SortedCsts),State,Constants), |
| 2128 | | Constants \= [], |
| 2129 | | exclude(is_constant_binding(SortedCsts),State,Variables). |
| 2130 | | |
| 2131 | | |
| 2132 | | |
| 2133 | | tcltk_constraint_find_static_assertion_violation(TclResult) :- |
| 2134 | | cbc_constraint_find_static_assertion_violation(Result,[]), |
| 2135 | | functor(Result,TclResult,_). |
| 2136 | | cbc_constraint_find_static_assertion_violation(Result,Options) :- |
| 2137 | | call_cbc_command(cbc_static_assertions_check(State,Options)), |
| 2138 | | ( State = counterexample_found(CE) -> |
| 2139 | | Result = counterexample_found, |
| 2140 | | tcltk_add_cbc_state(CE,static_assertion_check) |
| 2141 | | ; |
| 2142 | | Result = State). |
| 2143 | | |
| 2144 | | /* --------------------------------------------------- */ |
| 2145 | | |
| 2146 | | |
| 2147 | | :- use_module(error_manager,[extract_all_line_col/5]). |
| 2148 | | :- use_module(probcspsrc(haskell_csp),[extract_span_from_event/4,extract_span_info/2]). |
| 2149 | | |
| 2150 | | get_source_text_positions(Event,Line,Col,EndLine,EndCol) :- |
| 2151 | | extract_span_from_action(Event,SPAN), |
| 2152 | | extract_all_line_col(SPAN,Line,Col,EndLine,EndCol). |
| 2153 | | |
| 2154 | | extract_span_from_action(Event,Span) :- csp_mode, |
| 2155 | | extract_span_from_event(Event,Span,_,_). |
| 2156 | | extract_span_from_action(Event,Pos) :- b_or_z_mode, |
| 2157 | | get_operation_name(Event,ID), |
| 2158 | | b_get_machine_operation(ID,_Res,_TParas,_Body,_OType,Pos). |
| 2159 | | |
| 2160 | | |
| 2161 | | /* -------------------------------------------------------------------- */ |
| 2162 | | |
| 2163 | | get_current_option_eventtrace(OptionNum,TraceInfo) :- |
| 2164 | | % the option number starts with 0 (coming from a TK listbox) |
| 2165 | | current_options(ActionsAndIDs), |
| 2166 | | nth0(OptionNum,ActionsAndIDs,(Id,_,_,_)), |
| 2167 | | transition_info(Id,TraceInfo), |
| 2168 | | transition_info_can_be_shown(TraceInfo),!. |
| 2169 | | |
| 2170 | | transition_info_can_be_shown(eventtrace(_)). |
| 2171 | | transition_info_can_be_shown(path(_)). |
| 2172 | | |
| 2173 | | |
| 2174 | | tcltk_has_eventtrace(OptionNum) :- |
| 2175 | | get_current_option_eventtrace(OptionNum,_Trace). |
| 2176 | | |
| 2177 | | tcltk_show_eventtrace(OptionNum,Desc) :- |
| 2178 | | get_current_option_eventtrace(OptionNum,Trace), |
| 2179 | | explain_transition_info(Trace,Desc). |
| 2180 | | |
| 2181 | | |
| 2182 | | |
| 2183 | | /* --------------------------------------------------- */ |
| 2184 | | |
| 2185 | | :- use_module(prob2_interface,[execute_model/5]). |
| 2186 | | |
| 2187 | | tcltk_execute_model(MaxNrSteps,ExecutedSteps,Result) :- |
| 2188 | | current_state_id(CurID), |
| 2189 | | execute_model(CurID,MaxNrSteps,_TransitionInfo,ExecutedSteps,Result). |
| 2190 | | |
| 2191 | | |
| 2192 | | tcltk_find_shortest_trace_to_current_node(list(StringList)) :- |
| 2193 | | find_trace_to_current_node(OpL), |
| 2194 | | translate_events(OpL,StringList). |
| 2195 | | |
| 2196 | | |
| 2197 | | tcltk_execute_trace_to_current_node :- |
| 2198 | | current_state_id(CurID), |
| 2199 | | tcltk_execute_trace_to_node(CurID). |
| 2200 | | |
| 2201 | | tcltk_execute_trace_to_node(ToID) :- /* can be useful for TestCase Generation */ |
| 2202 | | set_target_id(ToID), |
| 2203 | | tcltk_execute_trace_from_to_found_predicate(root,_,_). |
| 2204 | | |
| 2205 | | % execcute longest loop-free trace (no repeated state) |
| 2206 | | tcltk_execute_longest_trace_from(From) :- |
| 2207 | | set_longest_trace_target, |
| 2208 | | tcltk_execute_trace_from_to_found_predicate(From,_,_). |
| 2209 | | |
| 2210 | | % OpL is list of operation ids, IDList is list of state ids |
| 2211 | | tcltk_execute_trace_from_to_found_predicate(From,OpL,IDList) :- |
| 2212 | | debug_println(19,finding_trace_from_to(From)), flush_output(user), |
| 2213 | | find_shortest_path_from_to_found_predicate(From,OpL,IDList,ToID), !, |
| 2214 | | (current_state_id(From) -> true ; state_space_reset), |
| 2215 | | debug_println(9,executing_trace(From,OpL,ToID)), flush_output(user), |
| 2216 | | execute_id_trace_from_current(ToID,OpL,IDList). |
| 2217 | | |
| 2218 | | |
| 2219 | | find_trace_to_current_node(Trace) :- |
| 2220 | | current_state_id(CurID), |
| 2221 | | find_shortest_path_from_to(root,CurID,L,_), |
| 2222 | | extract_term_trace_from_transition_ids(L,Trace). |
| 2223 | | |
| 2224 | | :- use_module(state_space_dijkstra). |
| 2225 | | |
| 2226 | | find_shortest_trace_to_node(FromID,ToID,OpIDListe,StateIDList) :- |
| 2227 | | find_shortest_path_from_to(FromID,ToID,OpIDListe,StateIDList). |
| 2228 | | |
| 2229 | | |
| 2230 | | /* --------------------------------------------------- */ |
| 2231 | | |
| 2232 | | |
| 2233 | | |
| 2234 | | tcltk_goto_a_non_deterministic_node(Msg) :- /* same transition leads to different resulting state */ |
| 2235 | | visited_expression_id(ID), |
| 2236 | | external_functions:non_det_transition(ID,_OpName,TID1,TID2), |
| 2237 | | tcltk_execute_trace_to_node(ID), |
| 2238 | | transition(ID,Op1,TID1,ID1), |
| 2239 | | transition(ID,_Op2,TID2,ID2), |
| 2240 | | translate_event_with_src_and_target_id(Op1,ID,ID1,OpStr), |
| 2241 | | ajoin(['Operation leads to at least two different states (ids ', ID1,', ',ID2, |
| 2242 | | ') for same arguments: ', OpStr], Msg). |
| 2243 | | |
| 2244 | | tcltk_goto_a_non_deterministic_output_node(Msg) :- /* same transition leads to different outputs */ |
| 2245 | | visited_expression_id(ID), |
| 2246 | | external_functions:non_det_output_transition(ID,_OpName,TID1,TID2), |
| 2247 | | tcltk_execute_trace_to_node(ID), |
| 2248 | | transition(ID,Op1,TID1,ID1), |
| 2249 | | transition(ID,Op2,TID2,ID2), |
| 2250 | | translate_event_with_src_and_target_id(Op1,ID,ID1,OpStr1), |
| 2251 | | translate_event_with_src_and_target_id(Op2,ID,ID2,OpStr2), |
| 2252 | | ajoin(['Operation has at least two different results for same arguments: ', OpStr1, |
| 2253 | | '\n and ',OpStr2], Msg). |
| 2254 | | |
| 2255 | | dif_ID(ID1,ID2) :- (number(ID1),number(ID2) -> ID2>ID1 ; ID1 \= ID2). |
| 2256 | | |
| 2257 | | tcltk_goto_a_branching_node :- /* two different events/operations enabled */ |
| 2258 | | transition(ID,X,ID2), get_operation_name(X,NX), |
| 2259 | | transition(ID,Y,ID3), dif_ID(ID2,ID3), get_operation_name(Y,NY), NX\=NY, |
| 2260 | | print_message(found_branching_op(ID,NX,NY)), |
| 2261 | | %tcltk_goto_state(find_branching_node,ID), |
| 2262 | | tcltk_execute_trace_to_node(ID). |
| 2263 | | |
| 2264 | | tcltk_goto_a_non_resetable_node :- |
| 2265 | | find_resetable_nodes, |
| 2266 | | visited_expression_id(ID), |
| 2267 | | \+(resetable_node(ID)), |
| 2268 | | \+(not_all_transitions_added(ID)), !, |
| 2269 | | %tcltk_goto_state(find_non_resetable_node,ID). |
| 2270 | | tcltk_execute_trace_to_node(ID). |
| 2271 | | |
| 2272 | | :- use_module(bmachine,[b_get_machine_operation_for_animation/4]). |
| 2273 | | operation_name_covered(OpName) :- operation_name_covered(OpName,_). |
| 2274 | | operation_name_covered(OpName,Template) :- |
| 2275 | | b_get_machine_operation_for_animation(OpName,Results,Par,_), |
| 2276 | | \+ operation_not_yet_covered(OpName), |
| 2277 | | length(Par,Arity), |
| 2278 | | functor(Op,OpName,Arity), |
| 2279 | | (Results\=[] -> Template = '-->'(Op,_) ; Template = Op). |
| 2280 | | |
| 2281 | | tcltk_goto_event_list_property_violation(Property,EventSelection,list(OperationList)) :- |
| 2282 | | % first translate Tk EventSelection Number list into Events |
| 2283 | | sap:get_selected_events(EventSelection,_AllEvents,OperationList), |
| 2284 | | include(operation_name_covered,OperationList,_,EnabledOpList), % only keep operations that can be enabled anyway |
| 2285 | | maplist(operation_name_covered,EnabledOpList,TemplateList), % replace by template |
| 2286 | | print(find_property_violation_for_template(Property,TemplateList)),nl, |
| 2287 | | visited_expression(ID,S), ID \= root, S\= concrete_constants(_), |
| 2288 | | \+(not_all_transitions_added(ID)), |
| 2289 | | \+( check_event_list_property(Property,ID,TemplateList) ), |
| 2290 | | print(found_event_list_property_violation(Property,ID)),nl, |
| 2291 | | tcltk_execute_trace_to_node(ID). |
| 2292 | | |
| 2293 | | check_event_list_property(relative_deadlock_freedom,ID,TemplateList) :- |
| 2294 | | relative_deadlock_freedom(ID,TemplateList). |
| 2295 | | check_event_list_property(valid_controller,ID,TemplateList) :- |
| 2296 | | is_valid_controller_state(ID,TemplateList). |
| 2297 | | check_event_list_property(det_controller,ID,TemplateList) :- |
| 2298 | | is_det_controller_state(ID,TemplateList). |
| 2299 | | |
| 2300 | | relative_deadlock_freedom(ID,TemplateList) :- member(Template,TemplateList), |
| 2301 | | transition(ID,Template,_). |
| 2302 | | is_valid_controller_state(ID,TemplateList) :- % check that exactly one event from TemplateList is enabled |
| 2303 | | append(_,[LiveEvent|RestTemplate],TemplateList), |
| 2304 | | transition(ID,LiveEvent,_),!, % we found one enabled event |
| 2305 | | \+ relative_deadlock_freedom(ID,RestTemplate). % all other events from list must be disabled |
| 2306 | | is_det_controller_state(ID,TemplateList) :- % check that *at most* one event from TemplateList is enabled |
| 2307 | | append(_,[LiveEvent|RestTemplate],TemplateList), |
| 2308 | | transition(ID,LiveEvent,_),!, % we found one enabled event from list |
| 2309 | | \+ relative_deadlock_freedom(ID,RestTemplate). % all other events from list must be disabled |
| 2310 | | is_det_controller_state(_,_) :- true. % no event enabled is also ok |
| 2311 | | |
| 2312 | | |
| 2313 | | tcltk_goto_state_enabling_operation(TclOpName,FromCurrent) :- |
| 2314 | | adapt_tcl_operation_name(TclOpName,OpName), |
| 2315 | | operation_name_covered(OpName,Template), % does cater for Event-B any vars |
| 2316 | | set_found_predicate(ID, transition(ID,Template,_)), |
| 2317 | | print_message('Computing trace to node'), |
| 2318 | | (FromCurrent=1 |
| 2319 | | -> current_state_id(FromID) % inefficient: better to do one dijkstra from FromID ! |
| 2320 | | ; FromID = root |
| 2321 | | ), |
| 2322 | | tcltk_execute_trace_from_to_found_predicate(FromID,_,_). |
| 2323 | | % tcltk_goto_state(find_enabled(OpName),ID). |
| 2324 | | |
| 2325 | | |
| 2326 | | :- use_module(tools_lists,[count_occurences/2]). |
| 2327 | | % quickly compute which operations have already been covered and which ones not |
| 2328 | | tcltk_operations_covered_info(list([list(['Operation','Covered'])|OpCov]),list(Occurences),Precise) :- |
| 2329 | | findall(list([OpName,Cov]), |
| 2330 | | (specfile:get_possible_event(OpName), |
| 2331 | | (operation_name_not_yet_covered(OpName) |
| 2332 | | -> not_yet_covered_info(Precise,OpName,Cov) |
| 2333 | | ; Cov = 'yes')),OpCov), |
| 2334 | | (maplist(get_cov,OpCov,Cov2), |
| 2335 | | count_occurences(Cov2,Occ2), |
| 2336 | | maplist(construct_list,Occ2,Occurences) -> true ; Occurences=[]). |
| 2337 | | |
| 2338 | | get_cov(list([_,Cov|_]),Cov). |
| 2339 | | construct_list(Kind-Nr,list([Kind,Nr])). |
| 2340 | | |
| 2341 | | :- use_module(cbcsrc(enabling_analysis),[feasible_operation/2]). |
| 2342 | | not_yet_covered_info(precise,OpName,Cov) :- |
| 2343 | | feasible_operation(OpName,Res),!, Res=Cov. |
| 2344 | | not_yet_covered_info(precise,_,R) :- !, R='unknown'. |
| 2345 | | not_yet_covered_info(_,_,'uncovered'). |
| 2346 | | |
| 2347 | | :- dynamic resetable_node/1. |
| 2348 | | |
| 2349 | | resetable_node(a). |
| 2350 | | |
| 2351 | | :- public find_resetable_nodes/0. |
| 2352 | | :- dynamic find_flag/2. |
| 2353 | | find_resetable_nodes :- |
| 2354 | | retractall(find_flag(_,_)), |
| 2355 | | retractall(resetable_node(_)), |
| 2356 | | any_transition(root,_,ID), /* add nodes reachable from root */ |
| 2357 | | assertz(find_flag(ID,0)), |
| 2358 | | fail. |
| 2359 | | find_resetable_nodes :- |
| 2360 | | visited_expression(CID,concrete_constants(_C)), |
| 2361 | | any_transition(CID,_,ID), /* add nodes reachable after a setup_constants */ |
| 2362 | | assertz(find_flag(ID,0)), |
| 2363 | | fail. |
| 2364 | | find_resetable_nodes :- find_resetable_nodes_loop, |
| 2365 | | print_message('Not resetable:'), |
| 2366 | | visited_expression_id(ID), |
| 2367 | | \+(resetable_node(ID)), |
| 2368 | | print_message(ID), |
| 2369 | | fail. |
| 2370 | | find_resetable_nodes :- |
| 2371 | | print_message('Done'). |
| 2372 | | |
| 2373 | | |
| 2374 | | find_resetable_nodes_loop :- |
| 2375 | | retract(find_flag(ID,N)), !, find_resetable_nodes_loop(ID,N). |
| 2376 | | find_resetable_nodes_loop. |
| 2377 | | |
| 2378 | | find_resetable_nodes_loop(ID,N) :- N1 is N+1, |
| 2379 | | assertz(resetable_node(ID)), |
| 2380 | | any_transition(NewID,_,ID), |
| 2381 | | \+(resetable_node(NewID)), |
| 2382 | | \+(find_flag(NewID,_)), |
| 2383 | | assertz(find_flag(NewID,N1)), |
| 2384 | | fail. |
| 2385 | | find_resetable_nodes_loop(_,_) :- find_resetable_nodes_loop. |
| 2386 | | |
| 2387 | | |
| 2388 | | :- use_module(specfile, [get_current_state_for_b_formula/2]). |
| 2389 | | |
| 2390 | | tcltk_show_expression_as_dot(VorE,File) :- |
| 2391 | | parse_machine_expression(VorE,TypedExpr), |
| 2392 | | tcltk_show_typed_expression_as_dot_graph(TypedExpr,File). |
| 2393 | | tcltk_show_expression_as_dot(_VorE,File) :- |
| 2394 | | add_error(tcltk_show_expression_as_dot,'Computing Value Dot Representation Failed for: ',File), |
| 2395 | | fail. |
| 2396 | | |
| 2397 | | :- use_module(dotsrc(state_as_dot_graph),[print_cstate_graph/2]). |
| 2398 | | :- use_module(dotsrc(state_custom_dot_graph),[tcltk_generate_state_custom_dot_graph_for_expr/2, is_valid_custom_dot_graph_record/1]). |
| 2399 | | |
| 2400 | | tcltk_show_typed_expression_as_dot_graph(TypedExpr,File) :- |
| 2401 | | is_valid_custom_dot_graph_record(TypedExpr), |
| 2402 | | !, % use the more powerful custom_dot_graph mechanism |
| 2403 | | tcltk_generate_state_custom_dot_graph_for_expr(TypedExpr,File). |
| 2404 | | tcltk_show_typed_expression_as_dot_graph(TypedExpr,File) :- |
| 2405 | | get_current_state_for_b_formula(TypedExpr,BState), |
| 2406 | | extend_state_with_probids_and_lets(BState,BState1), |
| 2407 | | decompose_expression_for_dot(TypedExpr,ExprList,[]), % decompose pairs so that user can provide multiple values/graphs |
| 2408 | | compute_for_dot(ExprList,BState1,GraphState), % compute value for each sub-component |
| 2409 | | format('Writing value to DOT file: ~w~n',[File]), |
| 2410 | | print_cstate_graph(GraphState,File), |
| 2411 | | format('Finished writing value to DOT file: ~w~n',[File]). |
| 2412 | | |
| 2413 | | |
| 2414 | | :- use_module(eval_let_store,[extend_typing_scope_for_stored_lets/2]). |
| 2415 | | :- use_module(bmachine, [b_parse_machine_expression_from_codes_with_prob_ids/2, type_with_errors/4]). |
| 2416 | | parse_machine_expression(RawAST,TypedExpr) :- compound(RawAST),!, % allow to pass raw AST as well |
| 2417 | | extend_typing_scope_for_stored_lets([prob_ids(visible),variables,external_library(safe_available_libraries)],Scope), |
| 2418 | | type_with_errors(RawAST,Scope,Type,TypedExpr), |
| 2419 | | % TODO: get_stored_let_typing_scope and add values to state returned by get_current_state_for_b_formula |
| 2420 | | ((Type=pred ; Type=subst) |
| 2421 | | -> add_error(parse_machine_expression,'Expected expression formula but obtained: ',Type),fail |
| 2422 | | ; true ). |
| 2423 | | parse_machine_expression(VorE,TypedExpr) :- |
| 2424 | | atom_codes(VorE,VorECodes), |
| 2425 | | b_parse_machine_expression_from_codes_with_prob_ids(VorECodes,TypedExpr). |
| 2426 | | |
| 2427 | | compute_for_dot([],_,[]). |
| 2428 | | compute_for_dot([String,TypedExpr|Tail],BState,[bind(Str,Value)|TS]) :- |
| 2429 | | % allow user to specify labels for graphs ("lbl1", e1, "lbl2", e2, ...) |
| 2430 | | get_texpr_expr(String,string(Str)),!, |
| 2431 | | translate:translate_bexpression_with_limit(TypedExpr,100,EStr), |
| 2432 | | format('Computing value for expression: ~w~n',[EStr]), |
| 2433 | | b_compute_expression_with_prob_ids(TypedExpr,BState,Value), |
| 2434 | | compute_for_dot(Tail,BState,TS). |
| 2435 | | compute_for_dot([TypedExpr|Tail],BState,[bind(Str,Value)|TS]) :- |
| 2436 | | translate:translate_bexpression_with_limit(TypedExpr,100,Str), |
| 2437 | | format('Computing value for expression: ~w~n',[Str]), |
| 2438 | | b_compute_expression_with_prob_ids(TypedExpr,BState,Value), |
| 2439 | | compute_for_dot(Tail,BState,TS). |
| 2440 | | |
| 2441 | | :- use_module(bsyntaxtree, [replace_ids_by_exprs/4]). |
| 2442 | | |
| 2443 | | % decompose_expression_for_dot ensures that |
| 2444 | | % ("label1",graph1,"lbl2",graph2) or rec(label:graph) is decomposed and we can associate labels with multiple graphs |
| 2445 | | decompose_expression_for_dot(b(couple(A,B),_,_)) --> !, |
| 2446 | | decompose_expression_for_dot(A), decompose_expression_for_dot(B). |
| 2447 | | decompose_expression_for_dot(b(rec(Fields),_,_)) --> !,decompose_fields_for_dot(Fields). |
| 2448 | | decompose_expression_for_dot(b(let_expression(Ids,Exprs,Body),couple(_,_),_)) --> !, |
| 2449 | | % this can happen when OPTIMIZE_AST is set to FALSE and the Jupyter kernel adds LETs; lift string out of let |
| 2450 | | % :dot expr_as_graph ("h",h,"hh",(h;h)) |
| 2451 | | {replace_ids_by_exprs(Body,Ids,Exprs,Body2)}, |
| 2452 | | decompose_expression_for_dot(Body2). |
| 2453 | | decompose_expression_for_dot(X) --> [X]. |
| 2454 | | |
| 2455 | | |
| 2456 | | decompose_fields_for_dot([]) --> []. |
| 2457 | | decompose_fields_for_dot([field(Name,Val)|T]) --> [b(string(Name),string,[]),Val], decompose_fields_for_dot(T). |
| 2458 | | |
| 2459 | | /* ------------------------------------------------------------------ */ |
| 2460 | | |
| 2461 | | % aka Execute by Predicate |
| 2462 | | tcltk_add_user_executed_operation(TclOpName,CustomPredicate) :- |
| 2463 | | tcltk_add_user_executed_operation(TclOpName,[],CustomPredicate). |
| 2464 | | |
| 2465 | | tcltk_add_user_executed_operation(TclOpName,ParameterBindList,RestPreCond) :- |
| 2466 | | adapt_tcl_operation_name(TclOpName,OpName), |
| 2467 | | parse_tclk_parameter_values_and_pred(OpName,ParameterBindList,RestPreCond,CustomPredicate), |
| 2468 | | current_state_id(CurID), |
| 2469 | | get_computed_preference(debug_time_out,DTO), |
| 2470 | | time_out_with_enum_warning_one_solution(b_trans_one_solution_with_pred(OpName,CustomPredicate,CurID,_,_,_), |
| 2471 | | DTO,TimeOutRes), |
| 2472 | | (is_time_out_result(TimeOutRes) |
| 2473 | | -> add_warning(execute_by_predicate,'Timeout occured trying to execute operation with predicate: ',TclOpName),fail |
| 2474 | | ; true). |
| 2475 | | |
| 2476 | | parse_tclk_parameter_values_and_pred(OpName,ParameterBindList,RestPreCond,CustomPredicate) :- |
| 2477 | | GenParseErrors=true, ExtraScope=[], |
| 2478 | | b_parse_machine_operation_pre_post_predicate(RestPreCond,ExtraScope,RestTypedPred,OpName,GenParseErrors), |
| 2479 | | (ParameterBindList=[] -> CustomPredicate = RestTypedPred |
| 2480 | | ; get_animation_operation_parameters(OpName,Parameters), |
| 2481 | | % print(tcltk_add_user_executed_operation(OpName,ParameterBindList,Parameters)),nl, |
| 2482 | | parse_parameter_values(ParameterBindList,OpName,Parameters,List), |
| 2483 | | conjunct_predicates([RestTypedPred|List],CustomPredicate) |
| 2484 | | ). |
| 2485 | | |
| 2486 | | :- use_module(bmachine,[b_get_machine_operation_for_animation/7]). |
| 2487 | | get_animation_operation_parameters('$setup_constants',Parameters) :- !, |
| 2488 | | b_get_machine_operation_typed_parameters('$setup_constants',Parameters). |
| 2489 | | get_animation_operation_parameters(OpName,FullParameters) :- xtl_mode,!, |
| 2490 | | xtl_transition_parameters(OpName,ParaNames), |
| 2491 | | maplist(make_string_id,ParaNames,FullParameters). |
| 2492 | | get_animation_operation_parameters(OpName,FullParameters) :- |
| 2493 | | TopLevel=true, % otherwise ANY parameters not added when show_eventb_any_arguments is true |
| 2494 | | b_get_machine_operation_for_animation(OpName,_Results,Parameters,_Body,_OType,TopLevel,_OpPos), |
| 2495 | | b_get_operation_non_det_modifies(OpName,NonDetVars), % also allow setting non-deterministically assigned vars |
| 2496 | | b_get_machine_variables(Vars), |
| 2497 | | include(non_det_modified(NonDetVars),Vars,ParaVars), |
| 2498 | | append(ParaVars,Parameters,FullParameters). |
| 2499 | | |
| 2500 | | make_string_id(ID,b(identifier(ID),string,[])). |
| 2501 | | non_det_modified(NonDetVars,TID) :- get_texpr_id(TID,ID), ord_member(ID,NonDetVars). |
| 2502 | | |
| 2503 | | % parse a list of variable names and expressions and turn into equal predicates |
| 2504 | | % Motivation: this can also deal with Z-style identifiers like in?, ... which cannot be parsed |
| 2505 | | :- use_module(btypechecker, [unify_types_strict/2, coerce_type/4]). |
| 2506 | | :- use_module(extrasrc(before_after_predicates),[prime_dollar0_bexpr_for_ids/3]). |
| 2507 | | :- use_module(probsrc(b_read_write_info), [b_get_read_write/3]). |
| 2508 | | |
| 2509 | | parse_parameter_values([],_,_,Res) :- !,Res=[]. |
| 2510 | | parse_parameter_values(['='(ParameterID,ExpressionStr)|T],OpName,Parameters,[Pred|PT]) :- |
| 2511 | | atom_codes(ExpressionStr,Codes), |
| 2512 | | format('Parsing for parameter ~w : ~w~n',[ParameterID,ExpressionStr]), |
| 2513 | | !, |
| 2514 | | b_parse_machine_expression_from_codes_with_prob_ids(Codes,TypedExpr), |
| 2515 | | get_texpr_type(TypedExpr,Type), |
| 2516 | | TID = b(identifier(ParameterID),ExpectedType,[]), |
| 2517 | | % if we reference a modified variable in the expression, we replace id by id$0 : |
| 2518 | | (b_or_z_mode -> b_get_read_write(OpName,_,Written) ; Written=[]), |
| 2519 | | prime_dollar0_bexpr_for_ids(TypedExpr,Written,PrimedTypedExpr0), |
| 2520 | | (xtl_mode |
| 2521 | | -> (Type=string -> PrimedTypedExpr1=PrimedTypedExpr0 |
| 2522 | | ; coerce_type(Type,string,PrimedTypedExpr0,PrimedTypedExpr1)), |
| 2523 | | PrimedTypedExpr=b(external_function_call('STRING_TO_TERM',[PrimedTypedExpr1]),string,[]), |
| 2524 | | Type2=string |
| 2525 | | ; PrimedTypedExpr=PrimedTypedExpr0, Type2=Type), |
| 2526 | | (member(b(identifier(ParameterID),ExpectedType,_),Parameters) |
| 2527 | | -> (unify_types_strict(Type2,ExpectedType) |
| 2528 | | -> safe_create_texpr(equal(TID,PrimedTypedExpr),pred,Pred), |
| 2529 | | parse_parameter_values(T,OpName,Parameters,PT) |
| 2530 | | ; coerce_type(Type2,ExpectedType,PrimedTypedExpr,NewTypedExpr) |
| 2531 | | -> safe_create_texpr(equal(TID,NewTypedExpr),pred,Pred), |
| 2532 | | add_message(parse_parameter_values,'Coercion of provided parameter value: ',NewTypedExpr), |
| 2533 | | parse_parameter_values(T,OpName,Parameters,PT) |
| 2534 | | ; |
| 2535 | | pretty_type(Type2,String1), pretty_type(ExpectedType,String2), |
| 2536 | | ajoin(['Value for parameter ',ParameterID,' has unexpected type ',String1,', expected: '],Msg), |
| 2537 | | add_error(parse_parameter_values,Msg,String2), |
| 2538 | | fail |
| 2539 | | ) |
| 2540 | | ; add_error(parse_parameter_values,'Unknown operation parameter: ',ParameterID), |
| 2541 | | fail). |
| 2542 | | parse_parameter_values(PB,OpName,P,_) :- |
| 2543 | | add_internal_error('Illegal parameter binding: ',parse_parameter_values(PB,OpName,P,_)),fail. |
| 2544 | | |
| 2545 | | |
| 2546 | | % just as above but with typed predicate |
| 2547 | | tcltk_add_user_executed_operation_typed(OpName,Operation,TypedCustomPredicate,NewID) :- |
| 2548 | | current_state_id(CurID), |
| 2549 | | tcltk_add_user_executed_operation_typed(OpName,CurID,Operation,TypedCustomPredicate,_,NewID). |
| 2550 | | tcltk_add_user_executed_operation_typed(OpName,CurID,Operation,TypedCustomPredicate,TransID,NewID) :- |
| 2551 | | b_trans_one_solution_with_pred(OpName,TypedCustomPredicate,CurID,Operation,TransID,NewID). |
| 2552 | | |
| 2553 | | % allows the user to arbitrarily change variable values |
| 2554 | | % Attention: this can of course violate the invariant |
| 2555 | | tcltk_add_user_modify_variable_transition(VarID,ValueStr) :- |
| 2556 | | current_state_id(CurID), |
| 2557 | | tcltk_add_user_modify_variable_transition(CurID,VarID,ValueStr,_). |
| 2558 | | tcltk_add_user_modify_variable_transition(CurID,VarID,ValueStr,NewID) :- |
| 2559 | | get_id_type(VarID,Kind,Type),!, |
| 2560 | | format('Trying to update ~w ~w to new value: ~w~n',[Kind,VarID,ValueStr]), |
| 2561 | | eval_string_in_cur_state(ValueStr,ValTyped,Value), |
| 2562 | | get_texpr_type(ValTyped,ValType), |
| 2563 | | check_types(Kind,VarID,Type,ValType), |
| 2564 | | visited_expression(CurID,CurState), |
| 2565 | | update_variable(CurState,VarID,Value,NewState), |
| 2566 | | Residue=[], TransInfo=[], |
| 2567 | | Operation = '$modify'(string(VarID),string(ValueStr)), |
| 2568 | | add_trans_id_with_infos(CurID,[],Operation,NewState,Residue,NewID,TransInfo,_), |
| 2569 | | tcltk_goto_state(Operation,NewID). |
| 2570 | | |
| 2571 | | check_types(_,_,Type,ValType) :- |
| 2572 | | unify_types_strict(Type,ValType),!. |
| 2573 | | check_types(Kind,VarID,Type,ValType) :- |
| 2574 | | pretty_type(ValType,VTS), pretty_type(Type,TS), |
| 2575 | | ajoin(['Unexpected type of value (', VTS, ' instead of ',TS,') for ',Kind,' :'],Msg), |
| 2576 | | add_error(check_types,Msg,VarID), |
| 2577 | | fail. |
| 2578 | | |
| 2579 | | :- use_module(bmachine,[b_is_variable/2, b_is_constant/2]). |
| 2580 | | get_id_type(ID,variable,Type) :- b_is_variable(ID,Type). |
| 2581 | | get_id_type(ID,constant,Type) :- b_is_constant(ID,Type). |
| 2582 | | % update variable value or constant value in concrete_constants state |
| 2583 | | update_variable([],VarID,_,[]) :- add_error(update_variable,'Identifier does not exist in state:',VarID),fail. |
| 2584 | | update_variable([bind(VarID,_)|T],VarID,NewVal,Res) :- !, Res = [bind(VarID,NewVal)|T]. |
| 2585 | | update_variable([H|T],VarID,NewVal,[H|UT]) :- !, update_variable(T,VarID,NewVal,UT). |
| 2586 | | update_variable(const_and_vars(ConstID,Old),VarID,NewVal,const_and_vars(ConstID,New)) :- !, |
| 2587 | | update_variable(Old,VarID,NewVal,New). |
| 2588 | | update_variable(concrete_constants(Old),VarID,NewVal,concrete_constants(New)) :- !, |
| 2589 | | update_variable(Old,VarID,NewVal,New). % here we allow updating constants |
| 2590 | | |
| 2591 | | % execute operation by predicate finding just one solution |
| 2592 | | b_trans_one_solution_with_pred(OpName,TypedCustomPredicate,CurID,Operation,TransId,NewID) :- |
| 2593 | | catch( |
| 2594 | | ( |
| 2595 | | call_cleanup(b_trans_one_solution_with_pred2(OpName,TypedCustomPredicate,CurID,Operation,TransId,NewID), |
| 2596 | | bmachine:reset_temp_predicate) |
| 2597 | | ), |
| 2598 | | enumeration_warning(Cause,_,_,_,_), |
| 2599 | | ( |
| 2600 | | add_warning(b_trans_one_solution_with_pred, |
| 2601 | | 'Enumeration warning prevented finding solution for operation: ',Cause), |
| 2602 | | fail |
| 2603 | | ) |
| 2604 | | ). |
| 2605 | | |
| 2606 | | % find one solution from current state using OpName and respecting temp_predicate |
| 2607 | | % Note: the predicate is evaluated in post-state, use $0 to access values in current state |
| 2608 | | b_trans_one_solution_with_pred2(OpName,TypedCustomPredicate,CurID,Operation,TransId,NewID) :- |
| 2609 | | (b_or_z_mode -> b_top_level_operation(OpName) ; true), |
| 2610 | | !, |
| 2611 | | visited_expression(CurID,InState), |
| 2612 | | set_error_context(operation(OpName,CurID)), |
| 2613 | | set_context_state(CurID,b_trans_one_solution_with_pred), |
| 2614 | | debug_format(19,'Executing ~w in state ~w by predicate~n',[OpName,CurID]), |
| 2615 | ? | call_cleanup(execute_operation_by_predicate_in_state(InState,OpName,TypedCustomPredicate,Operation,NewState,TransInfo), |
| 2616 | | (clear_context_state,clear_error_context)), |
| 2617 | | !, |
| 2618 | | debug_format(19,'Executed by predicate: ~w~n',[OpName]), |
| 2619 | | add_trans_id_infos(CurID,Operation,NewState,NewID,TransId,TransInfo), |
| 2620 | | tcltk_goto_state(Operation,NewID). |
| 2621 | | b_trans_one_solution_with_pred2(OpName,TypedCustomPredicate,CurID,Operation,TransId,NewID) :- |
| 2622 | | assert_temp_predicate_with_prob_def_set_elements(TypedCustomPredicate), |
| 2623 | | visited_expression(CurID,InState), |
| 2624 | | set_error_context(operation(OpName,CurID)), |
| 2625 | | set_context_state(CurID,b_trans_one_solution_with_pred), |
| 2626 | | temporary_set_preference(maxNrOfEnablingsPerOperation,1,Max), |
| 2627 | | temporary_set_preference(maxNrOfInitialisations,1,MaxI), |
| 2628 | | start_ms_timer(Timer), |
| 2629 | | call_cleanup((specfile:b_trans(InState,OpName,Operation,NewState,TransInfo) -> true), |
| 2630 | | (stop_ms_timer(Timer), |
| 2631 | | reset_temporary_preference(maxNrOfEnablingsPerOperation,Max), |
| 2632 | | reset_temporary_preference(maxNrOfInitialisations,MaxI), |
| 2633 | | clear_context_state,clear_error_context) |
| 2634 | | ), |
| 2635 | | debug_println(9,found_solution(NewState)),nl, |
| 2636 | | % now add a transition to the state space: |
| 2637 | | Residue=[], |
| 2638 | | add_trans_id_with_infos(CurID,[],Operation,NewState,Residue,NewID,TransInfo,TransId), |
| 2639 | | tcltk_goto_state(Operation,NewID). |
| 2640 | | |
| 2641 | | :- use_module(b_global_sets,[inline_prob_deferred_set_elements_into_bexpr/2]). |
| 2642 | | assert_temp_predicate_with_prob_def_set_elements(CustomPredicate) :- |
| 2643 | | inline_prob_deferred_set_elements_into_bexpr(CustomPredicate,CompiledPred), |
| 2644 | | bmachine:assert_temp_typed_predicate(CompiledPred). |
| 2645 | | |
| 2646 | | |
| 2647 | | % allow user to execute any statement |
| 2648 | | % TO DO: catch operation_calls and route them differently |
| 2649 | | % translate operation_call arguments into predicate and call tcltk_add_user_executed_operation_typed(OpName,Operation,TypedCustomPredicate,NewID) |
| 2650 | | tcltk_add_user_executed_statement(Statement,Updates,NewID) :- |
| 2651 | | current_expression(CurID,InState), |
| 2652 | | state_corresponds_to_initialised_b_machine(InState,BState), |
| 2653 | | set_context_state(CurID,tcltk_add_user_executed_statement), |
| 2654 | | %start_ms_timer(Timer), |
| 2655 | | call_cleanup((tcltk_interface:b_full_execute_top_level_statement_with_probids(Statement,BState,Updates,NewState)->true), |
| 2656 | | clear_context_state), |
| 2657 | | % TO DO: do we need to catch enumeration warnings ? |
| 2658 | | %stop_ms_timer(Timer), |
| 2659 | | Residue=[], TransInfo = [], |
| 2660 | | debug_println(4,executed(Updates,NewState)), |
| 2661 | | 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 |
| 2662 | | (get_id_of_node_and_add_if_required(NewState,NewID,Exists,CurID,'$unknown_operation',[]), |
| 2663 | | Exists=exists, |
| 2664 | | transition(CurID,Action,TransId,NewID) |
| 2665 | | -> debug_println(4,transition_exists_already(Action,TransId)) |
| 2666 | | ; translate:translate_substitution(Statement,OpLabel), |
| 2667 | | add_trans_id_with_infos(CurID,[],'$USER'(OpLabel),NewState,Residue,NewID,TransInfo,_), |
| 2668 | | format('Added new user-initiated transition to ~w via: ~w~n',[NewID,OpLabel]) |
| 2669 | | ), |
| 2670 | | tcltk_goto_state(OpLabel,NewID). |
| 2671 | | |
| 2672 | | :- use_module(eval_let_store,[extend_state_with_probids_and_lets/2]). |
| 2673 | | :- use_module(kernel_waitflags,[init_wait_flags_with_call_stack/2, ground_wait_flags/1]). |
| 2674 | | %% allows one to execute any statement (not just operations). |
| 2675 | | b_full_execute_top_level_statement_with_probids(Body,InState,Updates,NewState) :- |
| 2676 | | extend_state_with_probids_and_lets(InState,InState1), |
| 2677 | | init_wait_flags_with_call_stack(WF,[prob_command_context(user_executed_statement,unknown)]), |
| 2678 | | b_execute_top_level_statement(Body,[],InState1,Updates,WF,_Path1,output_not_required), |
| 2679 | | ground_wait_flags(WF), |
| 2680 | | store:store_updates_and_normalise(Updates,InState,NewState). |
| 2681 | | |
| 2682 | | % -------------------------------------------------------------------------------------- |
| 2683 | | |
| 2684 | | |
| 2685 | | :- use_module(bmachine). |
| 2686 | | :- use_module(specfile). |
| 2687 | | :- use_module(tools). |
| 2688 | | :- use_module(library(lists)). |
| 2689 | | :- use_module(store). |
| 2690 | | :- use_module(self_check). |
| 2691 | | :- use_module(b_global_sets). |
| 2692 | | :- use_module(translate). |
| 2693 | | |
| 2694 | | |
| 2695 | | /* --------------------------------------------------------- */ |
| 2696 | | /* --------------------------------------------------------- */ |
| 2697 | | |
| 2698 | | |
| 2699 | | /* ----------------------------------*/ |
| 2700 | | /* b_analyse_conjunction */ |
| 2701 | | /* ----------------------------------*/ |
| 2702 | | |
| 2703 | | |
| 2704 | | /* provide list of possible options for analysis */ |
| 2705 | | tcltk_analyse_option(invariant,'INVARIANT') :- b_or_z_mode. |
| 2706 | | tcltk_analyse_option(properties,S) :- b_or_z_mode, |
| 2707 | | get_specification_description(properties,S). |
| 2708 | | tcltk_analyse_option(assertions,S) :- (b_or_z_mode ; csp_mode), |
| 2709 | | get_specification_description(assertions,S). |
| 2710 | | tcltk_analyse_option(deadlock,'DEADLOCKED') :- b_or_z_mode. |
| 2711 | | |
| 2712 | | |
| 2713 | | :- use_module(predicate_evaluator). |
| 2714 | | /* perform the various analysis */ |
| 2715 | | tcltk_analyse(Mode,Type,ListWithResults,Total,False,Unknown) :- |
| 2716 | | (Mode == unicode |
| 2717 | | -> set_unicode_mode, |
| 2718 | | call_cleanup(tcltk_analyse2(Type,ListWithResults,Summary),unset_unicode_mode) |
| 2719 | | ; tcltk_analyse2(Type,ListWithResults,Summary)), |
| 2720 | | (member(total/Total,Summary) -> true ; Total=0), |
| 2721 | | (member(false/False,Summary) -> true ; False=0), |
| 2722 | | (member(unknown/Unknown,Summary) -> true ; Unknown=0). |
| 2723 | | tcltk_analyse2(invariant,L,Summary) :- !,tcltk_analyse_invariant(L,Summary). |
| 2724 | | tcltk_analyse2(properties,L,Summary) :- !,tcltk_analyse_properties(L,Summary). |
| 2725 | | tcltk_analyse2(assertions,L,Summary) :- !,tcltk_analyse_assertions(L,Summary). |
| 2726 | | tcltk_analyse2(deadlock,L,Summary) :- !,tcltk_analyse_deadlock(L,Summary). |
| 2727 | | tcltk_analyse2(X,L,Summary) :- add_error(tcltk_analyse, 'Unknown type of formula: ', X), |
| 2728 | | L=[], Summary=[]. |
| 2729 | | |
| 2730 | | |
| 2731 | | /* --------------------------------- */ |
| 2732 | | |
| 2733 | | tcltk_show_current_state(TransBState) :- |
| 2734 | | current_b_expression(B), |
| 2735 | | translate_bstate(B,TransBState). |
| 2736 | | |
| 2737 | | |
| 2738 | | tcltk_show_typing_of_variables_and_constants(list(List)) :- |
| 2739 | | b_get_machine_variables(TypedVarList), |
| 2740 | | convert_typed_varlist(TypedVarList,VarList,Types), |
| 2741 | | generate_typing_list(VarList,Types,VList,VarCard), |
| 2742 | | length(VarList,NrVars), |
| 2743 | | format_to_codes(' VARIABLES [nr=~w,card=~w]',[NrVars,VarCard],Codes1),atom_codes(VARAtom,Codes1), |
| 2744 | | |
| 2745 | | b_get_machine_all_constants(TypedCstList), |
| 2746 | | convert_typed_varlist(TypedCstList,CVarList,CTypes), |
| 2747 | | find_non_det_constants, |
| 2748 | | generate_typing_list(CVarList,CTypes,CList,CCard), |
| 2749 | | ( CList = [] |
| 2750 | | -> List = [VARAtom|VList] |
| 2751 | | ; length(CVarList,NrCsts), |
| 2752 | | format_to_codes(' CONSTANTS [nr=~w,card=~w]',[NrCsts,CCard],Codes2),atom_codes(CstAtom,Codes2), |
| 2753 | | append([CstAtom|CList],[VARAtom|VList],List) |
| 2754 | | ),!. |
| 2755 | | tcltk_show_typing_of_variables_and_constants(list(['TYPE ERROR in MACHINE'])). |
| 2756 | | |
| 2757 | | |
| 2758 | | %%% Used to get the constant values for the currently loaded B machine in form of a B predicate. |
| 2759 | | %%% In case that the constants in the model has not been set up then all possible constants' |
| 2760 | | %%% evaluations will be provided in form of a predicate in Disjunctive Normal Form. |
| 2761 | | %%% Predicate used for setting up constants when model checking with TLC. (TLA) |
| 2762 | | |
| 2763 | | tcltk_get_constants_predicate(Pred) :- |
| 2764 | | tcltk_get_constants_predicate(root,Pred,_PredComplete). |
| 2765 | | tcltk_get_constants_predicate(CurID,Pred,PredComplete) :- |
| 2766 | | (CurID=root |
| 2767 | | -> get_constants_as_disjoint_predicate(Pred), |
| 2768 | | (max_reached_or_timeout_for_node(root) -> PredComplete = incomplete ; PredComplete = complete) |
| 2769 | | ; PredComplete=complete, |
| 2770 | | prob2_interface:get_state(CurID,EState), |
| 2771 | | filter_constants_bindings(EState,X), % this will only get current constants values |
| 2772 | | translate_bstate_to_pred(X,Pred) |
| 2773 | | ). |
| 2774 | | |
| 2775 | | get_constants_as_disjoint_predicate(Pred) :- |
| 2776 | | findall(R,get_set_up_constants_solution(R),PredList), |
| 2777 | | add_or_between_constant_predicates(PredList,Pred). |
| 2778 | | |
| 2779 | | %get_a_part_of_the_found_solutions(L,N,Part,PredComplete) :- |
| 2780 | | % length(L,Length), |
| 2781 | | % (N>=Length |
| 2782 | | % -> Part=L, PredComplete=complete |
| 2783 | | % ; sublist(L,Part,_B,N,_A), PredComplete=incomplete |
| 2784 | | % ). |
| 2785 | | |
| 2786 | | translate_bstate_to_pred(State,P) :- |
| 2787 | | temporary_set_preference(expand_avl_upto,-1,CHNG2), |
| 2788 | | translate: translate_bstate(State,P), |
| 2789 | | reset_temporary_preference(expand_avl_upto,CHNG2). |
| 2790 | | |
| 2791 | | get_set_up_constants_solution(R) :- |
| 2792 | | compute_transitions_if_necessary(root), |
| 2793 | | %\+ max_reached_or_timeout_for_node(root),!, % then lookup constants rather than computing them |
| 2794 | | transition(root,_,Dst), |
| 2795 | | visited_expression(Dst,concrete_constants(X)), |
| 2796 | | translate_bstate_to_pred(X,R). |
| 2797 | | %get_set_up_constants_solution(R) :- |
| 2798 | | % b_interpreter: b_set_up_concrete_constants(X,_), |
| 2799 | | % translate:translate_bstate(X,R). |
| 2800 | | |
| 2801 | | add_or_between_constant_predicates([],'1=1'). |
| 2802 | | add_or_between_constant_predicates(L,Res) :- |
| 2803 | | tools: ajoin_with_sep(L,' or ',Res). |
| 2804 | | |
| 2805 | | filter_constants_bindings(EState,R) :- |
| 2806 | | b_get_machine_all_constants(C), |
| 2807 | | convert_typed_varlist(C,CVarList,_CTypes), |
| 2808 | | filter_constants_bindings1(EState,CVarList,R). |
| 2809 | | |
| 2810 | | filter_constants_bindings1([],_,[]). |
| 2811 | | filter_constants_bindings1([bind(Ident,Val)|T],CVarList,Res) :- |
| 2812 | | (member(Ident,CVarList) -> Res = [bind(Ident,Val)|Rest]; Res = Rest), |
| 2813 | | filter_constants_bindings1(T,CVarList,Rest). |
| 2814 | | |
| 2815 | | convert_typed_varlist([],[],[]). |
| 2816 | | convert_typed_varlist([b(identifier(ID),Type,_)|T],[ID|IT],[Type|TT]) :- |
| 2817 | | %print(ID), print(' : '), print(Type),nl, |
| 2818 | | % db : set(couple(global(Name),global(Code))) a : set(integer) boolean |
| 2819 | | convert_typed_varlist(T,IT,TT). |
| 2820 | | %-------------------------------------- |
| 2821 | | |
| 2822 | | |
| 2823 | | :- use_module(symsrc(symmetry_marker),[type_allows_for_precise_marker/1]). |
| 2824 | | :- use_module(bmachine,[b_is_unused_constant/1]). |
| 2825 | | :- use_module(library(codesio),[format_to_codes/3]). |
| 2826 | | :- use_module(kernel_card_arithmetic,[safe_mul/3]). |
| 2827 | | generate_typing_list([],[],[],1). |
| 2828 | | generate_typing_list([Var|VT],[BasicType|TT],[Translation|Rest],TotCard) :- |
| 2829 | | pretty_type(BasicType,PrettyType), |
| 2830 | | (kernel_objects:max_cardinality(BasicType,Card) -> true ; Card='??'), |
| 2831 | | (b_get_constant_represented_inside_global_set(Var,BasicType) |
| 2832 | | -> Imp='(treated as enumerated) ' |
| 2833 | | ; (preference(symmetry_mode,hash), |
| 2834 | | \+type_allows_for_precise_marker(BasicType)) |
| 2835 | | -> Imp = '(IMPRECISE for HASH) ' |
| 2836 | | ; Imp = '' |
| 2837 | | ), |
| 2838 | | (non_det_constant(Var) |
| 2839 | | -> MulSol ='[multiple solutions in SETUP_CONSTANTS]' |
| 2840 | | ; MulSol=''), |
| 2841 | | (b_is_unused_constant(Var) -> Unused=' (unused)' ; Unused=''), |
| 2842 | | % translate:translate_bexpression(b(member(identifier(Var),BasicType),pred,[]),Translation), |
| 2843 | | format_to_codes('~w:~w [card=~w]~w~w~w',[Var,PrettyType,Card,MulSol,Imp,Unused],Codes), |
| 2844 | | atom_codes(Translation,Codes), |
| 2845 | | generate_typing_list(VT,TT,Rest,RestCard), |
| 2846 | | safe_mul(RestCard,Card,TotCard). |
| 2847 | | |
| 2848 | | :- use_module(symsrc(symmetry_marker),[hash_model_checking_imprecise/2]). |
| 2849 | | :- use_module(translate,[pretty_type/2]). |
| 2850 | | |
| 2851 | | tcltk_hash_model_checking_imprecise :- |
| 2852 | | get_preference(symmetry_mode,hash), |
| 2853 | | hash_model_checking_imprecise(ID,BasicType),!, |
| 2854 | | print(' * Note: Hashing may be imprecise for: '), |
| 2855 | | print(ID), print(' : '),translate:pretty_type(BasicType,S),print(S), print(' !'),nl. |
| 2856 | | |
| 2857 | | |
| 2858 | | /* find constants which are assigned multiple values */ |
| 2859 | | :- dynamic non_det_constant/1. |
| 2860 | | find_non_det_constants :- |
| 2861 | | retractall(non_det_constant(_)), |
| 2862 | | findall(Csts,visited_expression(_,concrete_constants(Csts),_),CL), |
| 2863 | | (CL=[Valuation1|O],O=[_|_] -> find_non_det_constants1(Valuation1,O) |
| 2864 | | ; true /* 0 or 1 valuation only */ |
| 2865 | | ). |
| 2866 | | |
| 2867 | | find_non_det_constants1([],_). |
| 2868 | | find_non_det_constants1([bind(C,Value)|T],Other) :- check_cst(Other, C, Value, PeeledOther), |
| 2869 | | find_non_det_constants1(T,PeeledOther). |
| 2870 | | |
| 2871 | | check_cst([],_,_,[]). |
| 2872 | | check_cst([ [bind(C,OtherVal)|T1] | TT], C, Value, [ T1 | PTT]) :- |
| 2873 | | (Value=OtherVal -> check_cst(TT,C,Value,PTT) |
| 2874 | | ; assertz(non_det_constant(C)), peel2(TT,PTT)). |
| 2875 | | peel2([],[]). |
| 2876 | | peel2([ [_|T1] | TT], [ T1 | PTT]) :- peel2(TT,PTT). |
| 2877 | | |
| 2878 | | |
| 2879 | | /* --------------------------------- */ |
| 2880 | | |
| 2881 | | |
| 2882 | | /* --------------------------------- */ |
| 2883 | | |
| 2884 | | %% |
| 2885 | | % Visualize Invariant... |
| 2886 | | % |
| 2887 | | % Siehe bvisual.pl |
| 2888 | | |
| 2889 | | :- use_module(dotsrc(bvisual),[get_tree_from_expr/4, write_dot_graph_to_file/2]). |
| 2890 | | |
| 2891 | | |
| 2892 | | generate_dot_from_invariant(FileName):- |
| 2893 | | bmachine:b_get_invariant_from_machine(BExpr), |
| 2894 | | write_dot_file_for_pred_expr(BExpr,FileName). |
| 2895 | | |
| 2896 | | |
| 2897 | | :- use_module(b_operation_guards,[get_quantified_operation_enabling_condition/5]). |
| 2898 | | generate_dot_from_operation(TclOpName,FileName) :- |
| 2899 | | adapt_tcl_operation_name(TclOpName,OpName), |
| 2900 | | Simplify=false, |
| 2901 | | get_quantified_operation_enabling_condition(OpName, BExpr, _BecomesSuchVars, _Precise, Simplify), |
| 2902 | | write_dot_file_for_pred_expr(BExpr,FileName). |
| 2903 | | %generate_tree_from_boolean_expression(BExpr, Tree,BecomesSuchVars), |
| 2904 | | %write_dot_graph_to_file(Tree,FileName). |
| 2905 | | |
| 2906 | | % a version with additional parameters and additional pre condition / guard predicate |
| 2907 | | generate_dot_from_operation_with_params(TclOpName,ParameterBindList,RestPreCond, FileName) :- |
| 2908 | | adapt_tcl_operation_name(TclOpName,OpName), |
| 2909 | | Simplify=false, |
| 2910 | | get_quantified_operation_enabling_condition(OpName, BExpr, BecomesSuchVars,_Precise,Simplify), |
| 2911 | | parse_tclk_parameter_values_and_pred(OpName,ParameterBindList,RestPreCond,CustomPredicate), |
| 2912 | | insert_custom_predicate_into_guard(BExpr,CustomPredicate,FullPred), |
| 2913 | | %translate:nested_print_bexpr(FullPred),nl, |
| 2914 | | % TODO: probably allow all variables to be primed in CustomPredicate: |
| 2915 | | b_ast_cleanup:annotate_becomes_such_vars(BecomesSuchVars,CustomPredicate,BSV2), |
| 2916 | | write_dot_file_for_pred_expr(FullPred,FileName,BSV2). |
| 2917 | | |
| 2918 | | insert_custom_predicate_into_guard(b(exists(Para,Body),pred,Info),Pred,Res) :- !, |
| 2919 | | Res = b(exists(Para,BodyRes),pred,Info), % TODO: update wd infos |
| 2920 | | insert_custom_predicate_into_guard(Body,Pred,BodyRes). |
| 2921 | | insert_custom_predicate_into_guard(Guard,CustomPred,FullPred) :- |
| 2922 | | % put CustomPred first so that bvisual prioritises solutions coming from user values/predicate |
| 2923 | | % TODO: we could try and force equalities in CustomPred before calling bvisual |
| 2924 | | conjunct_predicates([CustomPred,Guard],FullPred). |
| 2925 | | |
| 2926 | | :- use_module(bmachine, [ |
| 2927 | | b_get_properties_from_machine/1, |
| 2928 | | b_get_machine_constants/1, |
| 2929 | | b_machine_has_constants_or_properties/0 ]). |
| 2930 | | :- use_module(bsyntaxtree,[create_or_merge_exists/3]). |
| 2931 | | get_properties(BExpr,CreateExists):- |
| 2932 | | b_get_properties_from_machine(Condition), |
| 2933 | | ( (CreateExists=true,b_machine_has_constants_or_properties) -> |
| 2934 | | b_get_machine_constants(IDs), |
| 2935 | | create_or_merge_exists(IDs, Condition, BExpr) |
| 2936 | | ; |
| 2937 | | BExpr = Condition |
| 2938 | | ). |
| 2939 | | |
| 2940 | | generate_dot_from_properties(FileName) :- |
| 2941 | | (current_state_corresponds_to_fully_setup_b_machine -> CreateExists=false; CreateExists=true), |
| 2942 | | get_properties(BExpr,CreateExists), |
| 2943 | | write_dot_file_for_pred_expr(BExpr,FileName). |
| 2944 | | |
| 2945 | | :- use_module(bsyntaxtree,[conjunct_predicates/2]). |
| 2946 | | |
| 2947 | | generate_dot_from_assertions(FileName) :- |
| 2948 | | (current_state_corresponds_to_setup_constants_b_machine, |
| 2949 | | bmachine:b_get_dynamic_assertions_from_machine(BExpr), BExpr \=[] |
| 2950 | | -> true |
| 2951 | | ; bmachine:b_get_static_assertions_from_machine(BExpr) |
| 2952 | | ), |
| 2953 | | conjunct_predicates(BExpr,BE), |
| 2954 | | write_dot_file_for_pred_expr(BE,FileName). |
| 2955 | | |
| 2956 | | generate_dot_from_goal(FileName) :- |
| 2957 | | b_get_machine_goal(BExpr),!, |
| 2958 | | write_dot_file_for_pred_expr(BExpr,FileName,all_primed_vars). |
| 2959 | | generate_dot_from_goal(FileName) :- |
| 2960 | | write_dot_file_for_pred_expr_and_state(b(string('No GOAL DEFINITION available'),string,[]),[],[],FileName). |
| 2961 | | |
| 2962 | | generate_dot_from_deadlock_po(FileName) :- |
| 2963 | | b_state_model_check:get_unsorted_all_guards_false_pred(BExpr), |
| 2964 | | %print('% CHECKING: '),translate_bexpression(BExpr,PT), print(PT),nl, |
| 2965 | | write_dot_file_for_pred_expr(BExpr,FileName). % we do not check it is a predicate anymore |
| 2966 | | |
| 2967 | | |
| 2968 | | generate_dot_from_formula(Pred,FileName) :- |
| 2969 | | debug_format(19,'Parsing formula ~w~n',[Pred]), |
| 2970 | | parse_machine_formula(Pred,TypedExpr), |
| 2971 | | debug_format(19,'Writing dot formula ~w~n',[Pred]), |
| 2972 | ? | write_dot_file_for_pred_expr(TypedExpr,FileName,all_primed_vars). |
| 2973 | | |
| 2974 | | |
| 2975 | | :- use_module(bmachine, [b_parse_machine_formula/3, type_with_errors/4, get_primed_machine_variables/1]). |
| 2976 | | parse_machine_formula(RawAST,TypedPred) :- compound(RawAST),!, % allow to pass raw AST as well |
| 2977 | | get_primed_machine_variables(PV), |
| 2978 | | type_with_errors(RawAST,[prob_ids(visible),identifier(PV),variables],_Type,TypedPred). |
| 2979 | | parse_machine_formula(PredStr,TypedExpr) :- |
| 2980 | | get_primed_machine_variables(PV), |
| 2981 | | b_parse_machine_formula(PredStr,[prob_ids(visible),identifier(PV),variables],TypedExpr). |
| 2982 | | |
| 2983 | | |
| 2984 | | write_dot_file_for_pred_expr(BExpr,FileName) :- |
| 2985 | | write_dot_file_for_pred_expr(BExpr,FileName,[]). |
| 2986 | | write_dot_file_for_pred_expr(BExpr,FileName,BecomesSuchVars) :- |
| 2987 | ? | generate_tree_in_cur_state(BExpr, Tree,BecomesSuchVars), |
| 2988 | | printsilent('% Writing to: '), printsilent(FileName),nls, |
| 2989 | | write_dot_graph_to_file(Tree,FileName). |
| 2990 | | write_dot_file_for_pred_expr_and_state(BExpr, LocalState, State,FileName) :- |
| 2991 | | get_tree_from_expr(Tree, BExpr, LocalState, State), |
| 2992 | | printsilent('% Writing to: '), printsilent(FileName),nls, |
| 2993 | | write_dot_graph_to_file(Tree,FileName). |
| 2994 | | |
| 2995 | | :- use_module(probsrc(state_space),[get_current_predecessor_state_id/1]). |
| 2996 | | :- use_module(probsrc(specfile),[extract_variables_from_state_as_primed/2]). |
| 2997 | | |
| 2998 | | generate_tree_in_cur_state(BExpr,Tree,all_primed_vars) :- |
| 2999 | | (get_current_predecessor_state_id(PredID), |
| 3000 | | visited_expression(PredID,SrcState), |
| 3001 | | extract_variables_from_state_as_primed(SrcState,PrimedVarBindings) |
| 3002 | | -> true |
| 3003 | | ; PrimedVarBindings=[] |
| 3004 | | ), |
| 3005 | | get_current_state_for_b_formula(BExpr,CurState0), |
| 3006 | | extend_state_with_probids_and_lets(CurState0,CurState1), |
| 3007 | | append(PrimedVarBindings,CurState1,CurState), |
| 3008 | | get_tree_from_expr(Tree, BExpr, [], CurState). |
| 3009 | | generate_tree_in_cur_state(BExpr,Tree,BecomesSuchVars) :- |
| 3010 | | get_current_state_for_b_formula(BExpr,CurState0), |
| 3011 | | extend_state_with_probids_and_lets(CurState0,CurState1), |
| 3012 | | % print(cur(CurState1)),nl, |
| 3013 | | insert_before_substitution_variables(BecomesSuchVars,[],CurState1,CurState1,CurState), |
| 3014 | | !, |
| 3015 | | get_tree_from_expr(Tree, BExpr, [], CurState). |
| 3016 | | |
| 3017 | | % generate a dot tree representation for a value; mostly useful for symbolic values |
| 3018 | | write_dot_file_for_value_as_tree(Value,FileName) :- |
| 3019 | | transform_value_to_expr(Value,BExpr), |
| 3020 | | temporary_set_preference(formula_tree_minimal_timeout,5,Prev1), |
| 3021 | | temporary_set_preference(formula_tree_maximal_timeout,30,Prev2), |
| 3022 | | call_cleanup(generate_tree_in_cur_state(BExpr, Tree,[]), |
| 3023 | | (reset_temporary_preference(formula_tree_minimal_timeout,Prev1), |
| 3024 | | reset_temporary_preference(formula_tree_maximal_timeout,Prev2))), |
| 3025 | | printsilent('% Writing to: '), printsilent(FileName),nls, |
| 3026 | | write_dot_graph_to_file(Tree,FileName). |
| 3027 | | |
| 3028 | | :- use_module(probsrc(bsyntaxtree),[create_typed_ids/3]). |
| 3029 | | :- use_module(library(lists),[maplist/4]). |
| 3030 | | transform_value_to_expr(closure(P,T,B),E) :- |
| 3031 | | create_typed_ids(P,T,Parameters),!, |
| 3032 | | E=b(comprehension_set(Parameters,B),set(any),[]). % TO DO: we could create typing |
| 3033 | | transform_value_to_expr(Val,b(value(Val),any,[])). |
| 3034 | | |
| 3035 | | :- use_module(tools,[maplist5/5]). |
| 3036 | | tcltk_bv_get_tops(Tops) :- |
| 3037 | | bv_get_top_level(Tops). |
| 3038 | | tcltk_bv_get_structure(Id,Label,list(Subs)) :- |
| 3039 | | bv_expand_formula(Id,Label,Subs). |
| 3040 | | tcltk_bv_is_leaf(Id,Label) :- |
| 3041 | | bv_expand_formula(Id,Label,[]). |
| 3042 | | tcltk_bv_get_values(Ids,list(RTexts),list(Tags)) :- |
| 3043 | | current_state_id(StateId), |
| 3044 | | bv_get_values(Ids,StateId,Values), |
| 3045 | | maplist5(tcltk_interface:retrieve_tag_adapted_text_for_id,Ids,Values,Tags,RTexts). |
| 3046 | | tcltk_bv_get_value(Id,RText,Tag) :- |
| 3047 | | tcltk_bv_get_values([Id],list([RText]),list([Tag])). |
| 3048 | | tcltk_bv_show_formula_as_dot_tree(Id,File) :- |
| 3049 | | bv_get_stored_formula_expr(Id,TExpr), |
| 3050 | | write_dot_file_for_pred_expr(TExpr,File). |
| 3051 | | tcltk_bv_get_pp_formula_string(Id,PPFormula) :- |
| 3052 | | bv_get_stored_formula_expr(Id,TExpr), |
| 3053 | | translate:translate_bexpression(TExpr,PPFormula). |
| 3054 | | |
| 3055 | | tcltk_bv_show_formula_as_dot_graph(Id,File) :- |
| 3056 | | bv_get_stored_formula_expr(Id,TExpr), |
| 3057 | | get_texpr_type(TExpr,Type), |
| 3058 | | Type \= pred, Type \= subst, |
| 3059 | | % tcltk_show_typed_expression_as_dot_graph decomposes expressions and shows value as graph: could be useful for pre-configured DEFINITIONS |
| 3060 | | tcltk_show_typed_expression_as_dot_graph(TExpr,File). |
| 3061 | | |
| 3062 | | tcltk_bv_show_value_as_dot_tree(Id,File) :- % useful for symbolic values |
| 3063 | | current_state_id(StateId), |
| 3064 | | bv_get_btvalue(Id,StateId,_E,Value), |
| 3065 | | write_dot_file_for_value_as_tree(Value,File). |
| 3066 | | |
| 3067 | | % a variation of tcltk_bv_show_value_as_dot_tree without dependence on bvisual2 |
| 3068 | | tcltk_show_identifier_value_as_dot_tree(RawId,File) :- % this also works if bvisual2 is not set up and entry active |
| 3069 | | get_identifier(RawId,Id), |
| 3070 | | current_expression(_ID,CurState), |
| 3071 | | expand_const_and_vars_to_full_store(CurState,EState), |
| 3072 | | (EState=[] -> add_error(tcltk_show_identifier_value_as_dot_tree,'Initialise machine first, cannot retrieve value for identifier:',Id) |
| 3073 | | ; lookup_value_for_existing_id(Id,EState,Value) |
| 3074 | | -> write_dot_file_for_value_as_tree(Value,File) |
| 3075 | | ; add_error(tcltk_show_identifier_value_as_dot_tree,'Cannot retrieve value for identifier:',Id)). |
| 3076 | | |
| 3077 | | get_identifier(AtomicID,Res) :- atom(AtomicID), valid_id(AtomicID), !,Res=AtomicID. |
| 3078 | | get_identifier(identifier(_,ID),Res) :- valid_id(ID),!, Res=ID. % raw ID from prob2_interface |
| 3079 | | get_identifier(RawFormula,_) :- |
| 3080 | | add_error(tcltk_show_identifier_value_as_dot_tree,'Please provide valid identifier of constant or variable:',RawFormula), |
| 3081 | | fail. |
| 3082 | | valid_id(ID) :- b_is_variable(ID). |
| 3083 | | valid_id(ID) :- b_is_constant(ID). |
| 3084 | | |
| 3085 | | retrieve_tag_adapted_text_for_id(Id,Value,Tag,RText) :- |
| 3086 | | retrieve_tag_text_for_id(Id,Value,Tag,Text), |
| 3087 | | (Text = '[]' -> RText = '[ ]' ; RText=Text). % for some reason the empty sequence translation [] gets transformed into '' by the tcltk library |
| 3088 | | |
| 3089 | | retrieve_tag_text_for_id(Id,Value,FullTag,Text) :- |
| 3090 | | retrieve_tag_text(Value,Tag,Text), |
| 3091 | | (bv_is_explanation_node(Id) -> convert_explain_tag(Tag,FullTag) ; FullTag=Tag). |
| 3092 | | retrieve_tag_text(i, inac, ''). |
| 3093 | | retrieve_tag_text(e(Text), error, Text). |
| 3094 | | retrieve_tag_text(v(Text), value, Text). |
| 3095 | | retrieve_tag_text(p(true), ptrue, true). |
| 3096 | | retrieve_tag_text(p(false),pfalse, false). |
| 3097 | | retrieve_tag_text(bv_info(Text), inac, Text). |
| 3098 | | |
| 3099 | | |
| 3100 | | tcltk_bv_get_unlimited_value(Id,Text,Tag) :- |
| 3101 | | current_state_id(StateId), |
| 3102 | | bv_get_value_unlimited(Id,StateId,Value), |
| 3103 | | retrieve_tag_text_for_id(Id,Value,Tag,Text1), |
| 3104 | | atom_codes(Text1,Text). % TODO: In the end, the result was converted from codes to atom and back |
| 3105 | | |
| 3106 | | % a version which returns just the value as an atom: |
| 3107 | | tcltk_bv_get_unlimited_value_atom(Id,AtomText) :- |
| 3108 | | current_state_id(StateId), |
| 3109 | | bv_get_value_unlimited(Id,StateId,Value), |
| 3110 | | retrieve_tag_text_for_id(Id,Value,_Tag,AtomText). |
| 3111 | | |
| 3112 | | convert_explain_tag(ptrue,explaintrue). |
| 3113 | | convert_explain_tag(pfalse,explainfalse). |
| 3114 | | convert_explain_tag(X,X). |
| 3115 | | |
| 3116 | | % ----------------------------------------- |
| 3117 | | |
| 3118 | | % STILL TO DO: refactor eval from here and probcli into separate module |
| 3119 | | |
| 3120 | | :- dynamic eval_elapsed_time/1. |
| 3121 | | tcltk_time_call(Call) :- |
| 3122 | | cputime(T1),Call,cputime(T2),ElapsedTime is T2-T1, |
| 3123 | | retractall(eval_elapsed_time(_)),assertz(eval_elapsed_time(ElapsedTime)). |
| 3124 | | |
| 3125 | | :- use_module(eval_strings). |
| 3126 | | |
| 3127 | | |
| 3128 | | tcltk_eval(String,StringResult,EnumWarning,Solution) :- |
| 3129 | | get_computed_preference(debug_time_out,DTO), |
| 3130 | | %print(debug_time_out(DTO)),nl, |
| 3131 | | time_out_with_enum_warning_one_solution(eval_string(String,StringResult,EnumWarning,LocalState),DTO,TimeOutRes), |
| 3132 | | (LocalState=[] -> Solution='' ; translate_bstate(LocalState,Solution)), |
| 3133 | | (is_time_out_result(TimeOutRes) -> |
| 3134 | | StringResult = '**** TIME-OUT ****', print(StringResult), print(' ('),print(DTO), print('ms)'),nl, |
| 3135 | | EnumWarning = no |
| 3136 | | ; print_last_info). |
| 3137 | | |
| 3138 | | :- public tcltk_eval_string_in_cur_state/2. |
| 3139 | | tcltk_eval_string_in_cur_state(String,TclValue) :- |
| 3140 | | eval_string_in_cur_state(String,_,Value), |
| 3141 | | convert_value_to_tcl(Value,TclValue). |
| 3142 | | convert_value_to_tcl(int(X),R) :- !, R=X. |
| 3143 | | convert_value_to_tcl(pred_true,R) :- !, R=1. |
| 3144 | | convert_value_to_tcl(pred_false,R) :- !, R=0. |
| 3145 | | convert_value_to_tcl(string(X),R) :- !, R=X. |
| 3146 | | % TO DO: add sets,... |
| 3147 | | convert_value_to_tcl(R,R) :- print(cannot_convert_to_tcl(R,R)),nl. |
| 3148 | | |
| 3149 | | eval_string_in_cur_state(String,Typed,Value) :- |
| 3150 | | %format('Parsing : "~w"~n',[String]), |
| 3151 | | bmachine:parse_expression_raw_or_atom_with_prob_ids(String,Typed), |
| 3152 | | current_state_id(CurID), prob2_interface:get_state(CurID,EState), |
| 3153 | | %print(evaluating_in_state(CurID)),nl, |
| 3154 | | b_compute_expression_with_prob_ids(Typed,EState,Value). |
| 3155 | | |
| 3156 | | % code to translate an expression into a list of lists that can be displayed as a table in Tk |
| 3157 | | % TO DO: make more robust and add more fancy translations |
| 3158 | | :- use_module(extrasrc(table_tools),[expand_and_translate_to_table_for_expr/5]). |
| 3159 | | tcltk_eval_as_table(String,Res) :- |
| 3160 | | eval_string_in_cur_state(String,Typed,Value), |
| 3161 | | Res = list([list(Header)|Table]), |
| 3162 | | expand_and_translate_to_table_for_expr(Typed,Value,Header,Table,['no-row-numbers']). |
| 3163 | | |
| 3164 | | :- use_module(user_interrupts,[interruptable_call/1]). |
| 3165 | | interruptable_tcltk_eval(String,StringResult,EnumWarning,Solution) :- |
| 3166 | | if(interruptable_call(tcltk_eval(String,StringResult,EnumWarning,Solution)),true, |
| 3167 | | (StringResult = 'Error or User-Interrupt', EnumWarning=unknown, Solution='')). |
| 3168 | | |
| 3169 | | % ----------------------------------------- |
| 3170 | | |
| 3171 | | tcltk_find_value_as_table(String,Options,list([Header|Matches])) :- |
| 3172 | | eval_string_in_cur_state(String,Typed,GoalValue), |
| 3173 | | Header = list(['ID','Kind','MatchPath']), |
| 3174 | | get_texpr_type(Typed,Type), |
| 3175 | | findall(list([ID,Kind,MatchMsg]), |
| 3176 | | (find_value_in_cur_state(GoalValue,Type,Options,match(Kind,ID,Path)), |
| 3177 | | format_to_codes('~w',[Path],MatchMsgC), |
| 3178 | | format('* match inside ~w ~w @ path: ~w~n',[Kind,ID,Path]), |
| 3179 | | atom_codes(MatchMsg,MatchMsgC)),Matches). |
| 3180 | | |
| 3181 | | % find a given value somewhere in a constant or variable value |
| 3182 | | |
| 3183 | | find_value_in_cur_state(GoalValue,Type,Options,match(Kind,ID,Path)) :- |
| 3184 | | translate:translate_bvalue(GoalValue,VS), |
| 3185 | | get_current_state_for_b_formula(requires_variables,State), % produce full state |
| 3186 | | member(bind(ID,Value),State), |
| 3187 | | ( bmachine:b_is_variable(ID,IDType), Kind=variable |
| 3188 | | ; bmachine:b_is_constant(ID,IDType), Kind=constant), |
| 3189 | | debug_format(19,'Searching id ~w for ~w~n',[ID,VS]), |
| 3190 | | % TODO check if Type occurs in type of ID |
| 3191 | | find_value(Value,IDType,GoalValue,Type,Options,Path). |
| 3192 | | |
| 3193 | | |
| 3194 | | :- use_module(probsrc(kernel_freetypes),[registered_freetype/2]). |
| 3195 | | :- use_module(bsyntaxtree,[is_set_type/2]). |
| 3196 | | :- use_module(kernel_strings,[to_b_string/2]). |
| 3197 | | find_value(Val,Type,GoalVal,Type,Options,Path) :- !, % target and goal type match; to do: unify_types |
| 3198 | | (kernel_objects:equal_object(Val,GoalVal) -> Path = '*' |
| 3199 | | ; fuzzy_find_value(Val,Type,GoalVal,Type,Options,Path)). |
| 3200 | | find_value((A,B),couple(TA,TB),GoalVal,Type,Options,Path) :- !, |
| 3201 | | ( find_value(A,TA,GoalVal,Type,Options,PA), |
| 3202 | | Path=','(PA,BS), translate:translate_bvalue(B,BS) |
| 3203 | | ; find_value(B,TB,GoalVal,Type,Options,PB), |
| 3204 | | Path=','(AS,PB), translate:translate_bvalue(A,AS)). |
| 3205 | | find_value(rec(Fields),record(FieldTypes),GoalVal,Type,Options,rec(Field,Path)) :- !, |
| 3206 | | member(field(Field,Val),Fields), |
| 3207 | | member(field(Field,TVal),FieldTypes), |
| 3208 | | find_value(Val,TVal,GoalVal,Type,Options,Path). |
| 3209 | | find_value(avl_set(AVL),AType,GoalVal,Type,Options,'{}'(Path)) :- !, |
| 3210 | | is_set_type(AType,TA), |
| 3211 | | custom_explicit_sets:avl_member_opt(Value,AVL), % TODO: provide a more proper interface predicate |
| 3212 | | find_value(Value,TA,GoalVal,Type,Options,Path). |
| 3213 | | find_value([H|T],set(TA),GoalVal,Type,Options,'{}'(Path)) :- !, |
| 3214 | | member(Value,[H|T]), |
| 3215 | | find_value(Value,TA,GoalVal,Type,Options,Path). |
| 3216 | | find_value(freeval(ID,Case,Val),freetype(ID),GoalVal,Type,Options,freeval(Case,Path)) :- !, |
| 3217 | | (registered_freetype(ID,Cases), |
| 3218 | | member(case(Case,TVal),Cases) -> true |
| 3219 | | ; add_error(find_value,'Illegal freeval:',freeval(ID,Case,Val)),fail |
| 3220 | | ), |
| 3221 | | find_value(Val,TVal,GoalVal,Type,Options,Path). |
| 3222 | | find_value(Val,TypeVal,GoalVal,Type,Options,Path) :- |
| 3223 | | fuzzy_find_value(Val,TypeVal,GoalVal,Type,Options,Path). |
| 3224 | | |
| 3225 | | fuzzy_find_value(Val,_Type,string(GoalAtom),string,[Option],'**'(TargetAtom)) :- |
| 3226 | | GoalAtom \= '', |
| 3227 | | simple_value_to_match(Val), |
| 3228 | | to_b_string(Val,string(TargetAtom)), |
| 3229 | | find_match_string(Option,TargetAtom,GoalAtom). |
| 3230 | | |
| 3231 | | simple_value_to_match(fd(_,_)). |
| 3232 | | simple_value_to_match(string(_)). |
| 3233 | | simple_value_to_match(int(_)). |
| 3234 | | simple_value_to_match(term(_)). |
| 3235 | | simple_value_to_match(freeval(_,_Case,Val)) :- ground(Val), Val=term(_). |
| 3236 | | |
| 3237 | | :- use_module(tools_matching,[fuzzy_match_codes_lower_case/2]). |
| 3238 | | |
| 3239 | | % check whether TargetAtom matches GoalAtom given match option |
| 3240 | | find_match_string(exact,GoalAtom,GoalAtom). |
| 3241 | | find_match_string(prefix,TargetAtom,GoalAtom) :- |
| 3242 | | atom_concat(GoalAtom,_,TargetAtom). % use sub_atom ? |
| 3243 | | find_match_string(suffix,TargetAtom,GoalAtom) :- |
| 3244 | | atom_concat(_,GoalAtom,TargetAtom). |
| 3245 | | find_match_string(infix,TargetAtom,GoalAtom) :- |
| 3246 | | sub_atom(TargetAtom,_Before,Length,_After,GoalAtom), Length>0. |
| 3247 | | find_match_string(fuzzy,TargetAtom,GoalAtom) :- |
| 3248 | | atom_codes(TargetAtom,TC), |
| 3249 | | atom_codes(GoalAtom,GC), |
| 3250 | | fuzzy_match_codes_lower_case(TC,GC). |
| 3251 | | % TODO: regex |
| 3252 | | |
| 3253 | | % ----------------------------------------- |
| 3254 | | % B Simplifier |
| 3255 | | :- use_module(probporsrc(b_simplifier),[tcltk_simplify_b_predicate/2]). |
| 3256 | | tcltk_simplify_predicate(String,StringResult) :- |
| 3257 | | tcltk_simplify_b_predicate(String,StringResult). |
| 3258 | | |
| 3259 | | |
| 3260 | | % ----------------------------------------- |
| 3261 | | % CBC Check |
| 3262 | | |
| 3263 | | get_cbc_data_base_id_checks(IDs) :- |
| 3264 | | findall(ID,b_state_model_check: cbc_check(ID,_Text,_Call,_Res,_Ok),IDs). |
| 3265 | | get_cbc_data_base_text_checks(Strings) :- |
| 3266 | | findall(Text1,(b_state_model_check: cbc_check(_ID,Text,_Call,_Res,_Ok),tools: string_concatenate(Text,';',Text1)),Strings). |
| 3267 | | |
| 3268 | | |
| 3269 | | % ----------------------------------------- |
| 3270 | | |
| 3271 | | % CSP Refinement Search |
| 3272 | | |
| 3273 | | %:- dynamic tcltk_cspm_mode/0. |
| 3274 | | %set_tcltk_cspm_mode :- assertz(tcltk_cspm_mode). |
| 3275 | | %unset_tcltk_cspm_mode :- retractall(tcltk_cspm_mode). |
| 3276 | | |
| 3277 | | |
| 3278 | | %get_new_csp_process_id(E,File,ID) :- |
| 3279 | | % ( parse_single_csp_expression_file(E,File,Proc) -> |
| 3280 | | % haskell_csp: check_compiled_term(Proc), add_csp_process_id1(Proc,ID,haskell_csp:animatable_process) |
| 3281 | | % ; add_error(parse_single_csp_expression_file,'Invalid process expression: ',E),fail |
| 3282 | | % ). |
| 3283 | | |
| 3284 | | %parse_and_analyze_process_expression(ProcExp,File,Proc) :- |
| 3285 | | % ( parse_single_csp_expression_file(ProcExp,File,Proc) -> true |
| 3286 | | % ; add_error(parse_single_csp_expression_file,'Invalid process expression: ',ProcExp),fail |
| 3287 | | % ). |
| 3288 | | |
| 3289 | | get_csp_process_id(Process,ID) :- get_start_transition_term(Process,Trans), |
| 3290 | | transition(root,Trans,ID). |
| 3291 | | |
| 3292 | | :- use_module(probcspsrc(haskell_csp),[animatable_process_without_arguments/1,animatable_process_cli/1]). |
| 3293 | | add_csp_process_id(Process,NewID) :- |
| 3294 | | add_csp_process_id1(Process,NewID,animatable_process_cli). |
| 3295 | | |
| 3296 | | add_csp_process_id1(Process,NewID,Pred) :- |
| 3297 | | (call(Pred,Process) |
| 3298 | | -> get_start_transition_term(Process,Trans), |
| 3299 | | (transition(root,Trans,_,DestID) -> NewID=DestID % process already set up |
| 3300 | | ; xtl_interface:get_start_expr(Process,NewState), |
| 3301 | | add_trans_id(root,Trans,NewState,NewID,_) |
| 3302 | | ) |
| 3303 | | ; add_error_fail(add_csp_process_id,'Not an animatable CSP Process: ',Process)). |
| 3304 | | |
| 3305 | | get_start_transition_term('MAIN',R) :- !, R= start_cspm_MAIN. |
| 3306 | | get_start_transition_term(agent_call(_Src,'MAIN',[]),R) :- !, R= start_cspm_MAIN. |
| 3307 | | get_start_transition_term(P,start_cspm(P)). |
| 3308 | | |
| 3309 | | add_csp_general_process_id(val_of(Process,_),ID) :- !, |
| 3310 | | ( animatable_process_without_arguments(Process) % in case the called processes is one without arguments, then we don't have to parse the expression |
| 3311 | | -> add_csp_process_id(Process,ID) |
| 3312 | | % code below not covered; loaded_main_file only defined for probcli entry point ! |
| 3313 | | %; animation_mode(cspm), |
| 3314 | | % loaded_main_file(CSPFile), |
| 3315 | | % parse_and_analyze_process_expression(Process,CSPFile,Proc), |
| 3316 | | % (transition(root,start_cspm(Proc),_TransID,ID) -> true |
| 3317 | | % ; otherwise -> add_trans_id(root,start_cspm(Proc),Proc,ID,_) |
| 3318 | | % ) |
| 3319 | | ). |
| 3320 | | add_csp_general_process_id(GenProcExpr,ID) :- |
| 3321 | | % stripping out the source-loc info |
| 3322 | | haskell_csp_analyzer: clear_span(GenProcExpr,GenProcExpr1), |
| 3323 | | get_start_transition_term(GenProcExpr1,Trans), |
| 3324 | ? | (transition(root,Trans,_TransID,ID) |
| 3325 | | -> true |
| 3326 | | ; add_trans_id(root,Trans,GenProcExpr1,ID,_) |
| 3327 | | ). |
| 3328 | | |
| 3329 | | :- public tcltk_csp_in_situ_refinement/4. |
| 3330 | | tcltk_csp_in_situ_refinement(ImplProcess,AbsProcess,ResTrace,Style) :- |
| 3331 | | format('Checking ~w ~w ~w~n',[AbsProcess,Style,ImplProcess]), |
| 3332 | | tcltk_csp_in_situ_refinement(ImplProcess,AbsProcess,ResTrace,Style,10000000). |
| 3333 | | csp_ref_style('[T=',trace). % Trace Refinement |
| 3334 | | csp_ref_style('T',trace). % Trace Refinement |
| 3335 | | csp_ref_style('[SF=',singleton_failures). % Singleton Failures Refinement |
| 3336 | | csp_ref_style('[F=',failures). % Failures Refinement |
| 3337 | | csp_ref_style('[R=',refusals). % Refusals Refinement |
| 3338 | | csp_ref_style('[RD=',refusals_div). % Refusals-Divergence Refinement |
| 3339 | | csp_ref_style('F',failures). % Failures Refinement |
| 3340 | | csp_ref_style('[FD=',X) :- csp_ref_style('FailureDivergence',X). |
| 3341 | | csp_ref_style('FD',X) :- csp_ref_style('FailureDivergence',X). |
| 3342 | | csp_ref_style('Trace',trace). |
| 3343 | | csp_ref_style('Failure',failures). |
| 3344 | | csp_ref_style('FailureDivergence',failure_divergences). |
| 3345 | | csp_ref_style('RefusalTesting',refusals). |
| 3346 | | csp_ref_style('RefusalTestingDiv',refusals_div). |
| 3347 | | csp_ref_style('RevivalTesting',revival) :- add_error(unsupported_refinement_operator,'[V= refinement not yet supported.'). |
| 3348 | | csp_ref_style('RevivalTestingDiv',revival_div) :- add_error(unsupported_refinement_operator,'[VD= refinement not yet supported.'). |
| 3349 | | |
| 3350 | | translate_csp_ref_style(Style,RefStyle) :- (csp_ref_style(Style,RefStyle) -> true ; |
| 3351 | | add_error_fail(csp,'Unknown refinement style: ',Style)). |
| 3352 | | |
| 3353 | | :- use_module(extrasrc(refinement_checker),[in_situ_ref_search/5]). |
| 3354 | | |
| 3355 | | % tcltk_csp_in_situ_refinement('P','Q',R,0,1000). tcltk_csp_in_situ_refinement('Q','P',R,1000). |
| 3356 | | tcltk_csp_in_situ_refinement(ImplProcess,AbsProcess,ResTrace,Style,MaxNrOfNewNodes) :- |
| 3357 | | add_csp_process_id(ImplProcess,ImplNodeID), |
| 3358 | | add_csp_process_id(AbsProcess,SpecNodeID), |
| 3359 | | translate_csp_ref_style(Style,RefStyle), |
| 3360 | | in_situ_ref_search(ImplNodeID,SpecNodeID,ResTrace,RefStyle,MaxNrOfNewNodes). |
| 3361 | | |
| 3362 | | :- use_module(probcspsrc(haskell_csp),[get_csp_assertions/1,translate_csp_assertion/2]). |
| 3363 | | |
| 3364 | | tcltk_check_csp_assertions(List,Summary) :- get_csp_assertions(Assertions), |
| 3365 | | treat_csp_ass(Assertions,List,0,0,0,Summary). % TO DO: display _List |
| 3366 | | |
| 3367 | | treat_csp_ass([],[],T,F,U,[total/Tot, true/T, false/F, unknown/U]) :- Tot is T+F+U. |
| 3368 | | treat_csp_ass([Assertion|T],['='(PP,Ok)|TPP],True,False,U,Summary) :- !, |
| 3369 | | (checkAssertion(Assertion,PP,_,Ok,_) |
| 3370 | | -> ( Ok=true -> T1 is True+1, F1=False, U1=U |
| 3371 | | ; Ok=false -> T1=True, F1 is False+1, U1=U |
| 3372 | | ; T1=True, F1=False, U1 is U+1) |
| 3373 | | ; U1 is U+1, T1=True, PP = '??', |
| 3374 | | F1=False,Ok=unknown |
| 3375 | | ), |
| 3376 | | treat_csp_ass(T,TPP,T1,F1,U1,Summary). |
| 3377 | | treat_csp_ass([H|T],TP,T1,F1,U,Summary) :- |
| 3378 | | add_error(treat_csp_ass,'Unknown CSP assertion: ',H), |
| 3379 | | U1 is U+1, treat_csp_ass(T,TP,T1,F1,U1,Summary). |
| 3380 | | |
| 3381 | | % assertModelCheckExt(False,val_of(P3,src_span(25,8,25,10,562,2)),DeadlockFree,F) |
| 3382 | | |
| 3383 | | :- use_module(extrasrc(refinement_checker),[in_situ_model_check/5, reset_refinement_checker/0]). |
| 3384 | | |
| 3385 | | run_assertion_check(assertModelCheckExt(Negated,Spec,Type,ModelStyle),Negated,ResTrace) :- |
| 3386 | ? | haskell_csp_analyzer: compile_body(Spec,'assertModelCheck',[],[],CSpec), |
| 3387 | | debug_println(9,assertModelCheckExt(Negated,CSpec,Type,ModelStyle)), |
| 3388 | | add_csp_general_process_id(CSpec,SpecNodeID), |
| 3389 | | translate_csp_ref_style(ModelStyle,RefStyle), |
| 3390 | | in_situ_model_check(SpecNodeID,ResTrace,Type,RefStyle,10000000), |
| 3391 | | formatsilent('Result trace for assertModelCheck: ~w~n',[ResTrace]). |
| 3392 | | run_assertion_check(assertModelCheck(Negated,Spec,Style),Negated,ResTrace) :- |
| 3393 | ? | run_assertion_check(assertModelCheckExt(Negated,Spec,Style,'FailureDivergence'),Negated,ResTrace). |
| 3394 | | run_assertion_check(assertRef(Negated,Spec,Style,Impl,Span),Negated,ResTrace) :- |
| 3395 | ? | haskell_csp_analyzer: compile_body(Spec,'assertRef',[],[],CSpec), |
| 3396 | ? | haskell_csp_analyzer: compile_body(Impl,'assertRef',[],[],CImpl), |
| 3397 | | debug_println(9,assertRef(Negated,CSpec,Style,CImpl,Span)), |
| 3398 | | add_csp_general_process_id(CSpec,SpecNodeID), |
| 3399 | | add_csp_general_process_id(CImpl,ImplNodeID), |
| 3400 | | translate_csp_ref_style(Style,RefStyle), |
| 3401 | | refinement_checker:in_situ_ref_search(ImplNodeID,SpecNodeID,ResTrace,RefStyle,10000000). |
| 3402 | | run_assertion_check(assertLtl(Negated,Spec,FormulaAsAtom,_Span),Negated,ResTrace) :- |
| 3403 | | add_csp_process_id_normalized(Spec,'assertLtl',CSpec,CSpecNodeID), |
| 3404 | | %% print(add_csp_general_process_id(Spec,CSpec,SpecNodeID)),nl, |
| 3405 | | tcltk_reset, |
| 3406 | | ltl_model_check_with_ce1(CSpec,FormulaAsAtom,-1,specific_node(CSpecNodeID),Result), |
| 3407 | | translate_ltl_result(Result,ResTrace), |
| 3408 | | debug_println(9,ltl_result(Negated,CSpec,CSpecNodeID,FormulaAsAtom,Result)). |
| 3409 | | run_assertion_check(assertCtl(Negated,Spec,FormulaAsAtom,_Span),Negated,ResTrace) :- |
| 3410 | | add_csp_process_id_normalized(Spec,'assertCtl',CSpec,CSpecNodeID), |
| 3411 | | tcltk_reset, |
| 3412 | | ctl_model_check_with_ce(CSpec,FormulaAsAtom,-1,specific_node(CSpecNodeID),Result,Trace), |
| 3413 | | debug_println(9,ctl_result(Negated,CSpec,CSpecNodeID,FormulaAsAtom,Result)), |
| 3414 | | translate_ctl_result(Result,Trace,ResTrace). |
| 3415 | | |
| 3416 | | checkAssertion(Assertion,PP,Negated,Ok,ResTrace) :- |
| 3417 | | translate_csp_assertion(Assertion,PP), |
| 3418 | | formatsilent('CHECKING ~w~n',[PP]), |
| 3419 | | debug_println(9,checkAssertion(Assertion)), |
| 3420 | | reset_refinement_checker, |
| 3421 | ? | (run_assertion_check(Assertion,Negated,ResTrace) |
| 3422 | | -> debug_println(9,result(ResTrace)), |
| 3423 | | (ResTrace=no_counter_example |
| 3424 | | -> (Negated = 'False' -> Ok=true ; Ok=false) |
| 3425 | | ; ResTrace=no_counter_example_found |
| 3426 | | -> Ok=interrupted |
| 3427 | | ; ResTrace=[interrupted|_] |
| 3428 | | -> Ok=interrupted, print('*** Execution interrupted by user ***'),nl |
| 3429 | | ; Negated = 'False' -> Ok=false |
| 3430 | | ; Ok=true |
| 3431 | | ), |
| 3432 | | (Ok=true -> printsilent('OK'),nls |
| 3433 | | ; Ok=interrupted -> print('*** UNKNOWN ***'),nl |
| 3434 | | ; print('*** FALSE ***'),nl |
| 3435 | | ) |
| 3436 | | ; add_error_fail(checkAssertion,'Internal Error, Assertion Checking Failed for: ',PP) |
| 3437 | | ). |
| 3438 | | |
| 3439 | | add_csp_process_id_normalized(Spec,Functor,CSpec,CSpecNodeID) :- |
| 3440 | | % stripping out the src_span info |
| 3441 | | haskell_csp_analyzer: clear_span(Spec,SpecNoSpan), |
| 3442 | | haskell_csp_analyzer: compile_body(SpecNoSpan,Functor,[],[],CSpec), |
| 3443 | | add_csp_general_process_id(CSpec,CSpecNodeID). |
| 3444 | | |
| 3445 | | translate_ltl_result(ok,Res) :- !, |
| 3446 | | Res = no_counter_example. |
| 3447 | | translate_ltl_result(no,Res) :- !, |
| 3448 | | Res = no. |
| 3449 | | translate_ltl_result(ce(Atom),Res) :- |
| 3450 | | !, % we have a counter-example for the LTL formula |
| 3451 | | Res=Atom. |
| 3452 | | translate_ltl_result(interrupted,Res) :- |
| 3453 | | !, |
| 3454 | | Res=[interrupted]. |
| 3455 | | translate_ltl_result(Status,_Res) :- |
| 3456 | | add_error_fail(ltl_assertions_result, 'Internal Error: unknown LTL assertion result ', Status). |
| 3457 | | |
| 3458 | | translate_ctl_result(true,_Trace,ResTrace) :- !, |
| 3459 | | ResTrace = no_counter_example. |
| 3460 | | translate_ctl_result(false,ce(Atom),ResTrace) :- !, |
| 3461 | | ResTrace = Atom. |
| 3462 | | translate_ctl_result(interrupted,_TRace,ResTrace) :- |
| 3463 | | !, |
| 3464 | | ResTrace=[interrupted]. |
| 3465 | | translate_ctl_result(Status,_Trace,_ResTrace) :- |
| 3466 | | add_error_fail(ctl_assertions_result, 'Internal Error: unknown CTL assertion result ', Status). |
| 3467 | | |
| 3468 | | |
| 3469 | | tcltk_check_csp_assertion(Assertion,CSPFile,Negated,Result) :- |
| 3470 | | tcltk_check_csp_assertion(Assertion,CSPFile,Negated,_PlTerm,Result). |
| 3471 | | |
| 3472 | | tcltk_check_csp_assertion(Assertion,CSPFile,Negated,PlTerm,Result) :- |
| 3473 | | parse_single_csp_declaration(Assertion,CSPFile,PlTerm), |
| 3474 | | checkAssertion(PlTerm,_PP,Negated,_Ok,Result). |
| 3475 | | |
| 3476 | | :- public tcltk_play_ltl_ctl_counterexample_trace/4. |
| 3477 | | tcltk_play_ltl_ctl_counterexample_trace(Assertion,CSPFile,Type,FairnessChecked) :- |
| 3478 | | announce_event(play_counterexample), |
| 3479 | | ( Type == ltl -> Functor = assertLtl |
| 3480 | | ; Type == ctl -> Functor = assertCtl |
| 3481 | | ; add_error_fail(ltl_ctl_counterexample, 'Internal Error: Model checker type unknown: ',Type)), |
| 3482 | | % constructing the prolog declaration term |
| 3483 | | PlDeclTerm =.. [Functor,_Negated,Spec,FormulaAsAtom,_Span], |
| 3484 | | parse_single_csp_declaration(Assertion,CSPFile,PlDeclTerm), |
| 3485 | | haskell_csp_analyzer: clear_span(Spec,SpecNoSpan), |
| 3486 | | haskell_csp_analyzer: compile_body(SpecNoSpan,'assertLtl',[],[],CSpec), |
| 3487 | | % parsing and preprocessing the LTL/CTL formula |
| 3488 | | parse_and_preprocess_formula(FormulaAsAtom,Type,PF), |
| 3489 | | (is_fairness_implication(PF) -> FairnessChecked='yes'; FairnessChecked='no'), |
| 3490 | | % need to reset history and current state before loading the counter-example |
| 3491 | | tcltk_reset, |
| 3492 | | tcltk_play_counterexample(Type,CSpec,PF). |
| 3493 | | |
| 3494 | | tcltk_play_counterexample(ltl,Spec,Formula) :- !, |
| 3495 | | tcltk_play_ltl_counterexample(Spec,Formula). |
| 3496 | | tcltk_play_counterexample(ctl,Spec,Formula) :- !, |
| 3497 | | tcltk_play_ctl_counterexample(Spec,Formula). |
| 3498 | | tcltk_play_counterexample(Type,Spec,Formula) :- |
| 3499 | | add_error_fail(ltl_ctl_counterexample, 'Internal Error: Unknown domain type: ', (Type,Spec,Formula)). |
| 3500 | | |
| 3501 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 3502 | | |
| 3503 | | |
| 3504 | | %%%% Parse and get LTL formulas from LTL File %%%% |
| 3505 | | get_ltl_formulas_from_file(Filename,Text) :- |
| 3506 | | parse_ltlfile(Filename, Formulas), print(Formulas),nl, |
| 3507 | | translate_ltl_formulas(Formulas,Text). |
| 3508 | | |
| 3509 | | translate_ltl_formulas(Formulas,Text) :- |
| 3510 | | maplist(translate_ltl_formula,Formulas,Strings), |
| 3511 | | haskell_csp: concatenate_string_list(Strings,Text). |
| 3512 | | |
| 3513 | | translate_ltl_formula(formula(_Name,Formula),Text) :- !, |
| 3514 | | pp_ltl_formula(Formula,T), |
| 3515 | | string_concatenate(T,'$',Text). |
| 3516 | | translate_ltl_formula(F,'') :- add_error(get_ltl_formulas_from_file,'Illegal formula: ',F). |
| 3517 | | |
| 3518 | | |
| 3519 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 3520 | | |
| 3521 | | |
| 3522 | | tcltk_explore_csp_process(ProcString,SpecNodeID) :- |
| 3523 | | haskell_csp: parse_single_csp_expression(ltl,ProcString,Res), |
| 3524 | | haskell_csp_analyzer: clear_span(Res,ResNoSpan), |
| 3525 | | haskell_csp_analyzer: compile_body(ResNoSpan,'assertLtl',[],[],CRes), |
| 3526 | | add_csp_general_process_id(CRes,SpecNodeID), |
| 3527 | | refinement_checker:dfs_check(SpecNodeID,_ResTrace,false,false). |
| 3528 | | |
| 3529 | | tcltk_visualize_csp_process(SpecNodeID,F) :- |
| 3530 | | visualize_graph: tcltk_print_csp_process_states_for_dot(F,SpecNodeID). |
| 3531 | | |
| 3532 | | :- dynamic nr_csp_process_state/1. |
| 3533 | | get_csp_process_stats(NrNodes) :- |
| 3534 | | assertz(nr_csp_process_state(0)), |
| 3535 | | count_nodes, |
| 3536 | | nr_csp_process_state(NrNodes), |
| 3537 | | retractall(nr_csp_process_state(_)). |
| 3538 | | |
| 3539 | | count_nodes :- |
| 3540 | | refinement_checker: dvisited(_NodeID), |
| 3541 | | nr_csp_process_state(NrNodes), |
| 3542 | | NewNrNodes is NrNodes +1, |
| 3543 | | retractall(nr_csp_process_state(_)), |
| 3544 | | assertz(nr_csp_process_state(NewNrNodes)), |
| 3545 | | fail. |
| 3546 | | count_nodes. |
| 3547 | | |
| 3548 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 3549 | | |
| 3550 | | tcltk_machine_has_assertions :- |
| 3551 | | ( b_get_static_assertions_from_machine([_|_]); b_get_dynamic_assertions_from_machine([_|_]) ), !. |
| 3552 | | |
| 3553 | | tcltk_unique_top_level_operation(Name) :- b_top_level_operation(Name), |
| 3554 | | \+ (b_top_level_operation(N2), N2 \= Name). |
| 3555 | | |
| 3556 | | tcltk_top_level_operations(list(Res)) :- |
| 3557 | | findall(Name,b_top_level_operation(Name),Names), |
| 3558 | | length(Names,L), |
| 3559 | | (L>5 -> sort(Names,Res) ; Res=Names). |
| 3560 | | |
| 3561 | | tcltk_get_vacuous_guards(list(R)) :- |
| 3562 | | eclipse_interface:get_vacuous_guards(L), % to do: add source column |
| 3563 | | (L=[] -> R = ['No vacuous guards'] |
| 3564 | | ; R=L). |
| 3565 | | |
| 3566 | | tcltk_get_vacuous_invariants(list(L)) :- |
| 3567 | | eclipse_interface:get_vacuous_invariants(LP), |
| 3568 | | (LP=[] -> L = ['No vacuous invariants'] |
| 3569 | | ; maplist(translate:translate_bexpression,LP,L)). |
| 3570 | | |
| 3571 | | tcltk_get_vacuous_invariants_table(list([list(['LHS','Op','RHS','Source'])|L])) :- |
| 3572 | | eclipse_interface:get_vacuous_invariants(LP), |
| 3573 | | LP \= [], !, |
| 3574 | | maplist(get_expr_and_source,LP,L). |
| 3575 | | tcltk_get_vacuous_invariants_table(list(['No vacuous invariants'])). |
| 3576 | | |
| 3577 | | :- use_module(translate,[translate_bexpression_with_limit/3]). |
| 3578 | | :- use_module(error_manager,[get_tk_table_position_info/2]). |
| 3579 | | get_expr_and_source(P,list([TS1,Op,TS2,Src])) :- |
| 3580 | | decompose(P,LHS,Op,RHS), |
| 3581 | | translate_bexpression_with_limit(LHS,150,TS1), |
| 3582 | | translate_bexpression_with_limit(RHS,60,TS2), |
| 3583 | | get_tk_table_position_info(P,Src). |
| 3584 | | |
| 3585 | | decompose(b(implication(LHS,RHS),pred,_),LHS,'=>',RHS) :- !. |
| 3586 | | decompose(b(disjunction(LHS,RHS),pred,_),LHS,'or',RHS) :- !. |
| 3587 | | decompose(LHS,LHS,'?',b(truth,pred,[])). |
| 3588 | | |
| 3589 | | |
| 3590 | | % ------------------- |
| 3591 | | |
| 3592 | | |
| 3593 | | :- use_module(extrasrc(mcts_game_play), [mcts_auto_play/4, mcts_auto_play_available/0]). |
| 3594 | | |
| 3595 | | tcltk_mcts_auto_play :- tcltk_mcts_auto_play(_). |
| 3596 | | tcltk_mcts_auto_play(TransID) :- |
| 3597 | | mcts_auto_play_available, |
| 3598 | | current_state_id(CurID), |
| 3599 | | mcts_auto_play(CurID,ActionAsTerm,TransID,State2), |
| 3600 | | (tcltk_perform_action(CurID,ActionAsTerm,TransID,State2) |
| 3601 | | -> true |
| 3602 | | ; add_error(tcltk_mcts_auto_play,'Cannot perform chosen action:',ActionAsTerm),fail). |