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