| 1 | % Heinrich Heine Universitaet Duesseldorf | |
| 2 | % (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
| 3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
| 4 | ||
| 5 | :- module(prob2_interface, | |
| 6 | [initialise_specification/0, | |
| 7 | get_version/7, get_user_signal_reference/1, | |
| 8 | get_prob_total_number_of_errors/1, | |
| 9 | ||
| 10 | load_classical_b_from_list_of_facts/2, | |
| 11 | update_preferences_from_spec/0, update_preferences_from_spec/1, | |
| 12 | ||
| 13 | load_event_b_project/4, | |
| 14 | ||
| 15 | load_cspm_spec_from_cspm_file/1, | |
| 16 | load_z_spec_from_fuzz_file/1, | |
| 17 | load_z_spec_from_tex_file/1, | |
| 18 | load_xtl_spec_from_prolog_file/1, | |
| 19 | load_alloy_spec_from_term/2, | |
| 20 | ||
| 21 | prob2_reset_prob/0, | |
| 22 | reset_animator/0, clear_animator/0, start_animation/0, | |
| 23 | ||
| 24 | serialize/2, | |
| 25 | deserialize/2, | |
| 26 | ||
| 27 | get_state/2, | |
| 28 | get_b_state/2, | |
| 29 | ||
| 30 | compute_operations_for_state/2, | |
| 31 | compute_additional_candidate_operations_for_state/2, | |
| 32 | prob2_execute_custom_operations/6, | |
| 33 | ||
| 34 | get_op_from_id/4, | |
| 35 | ||
| 36 | is_initialised_state/1, | |
| 37 | is_initialised_b_state/1, | |
| 38 | state_property/3, | |
| 39 | op_timeout_occurred/2, | |
| 40 | ||
| 41 | prob2_get_state_errors/2, | |
| 42 | ||
| 43 | prob2_evaluate_formulas/3, | |
| 44 | register_prob2_formulas/2, | |
| 45 | unregister_prob2_formulas/1, | |
| 46 | get_animation_image_list/1, get_animation_image_matrix_for_state/6, | |
| 47 | get_react_to_item_right_click_options_for_state/4, | |
| 48 | react_to_item_right_click_option_for_state/6, | |
| 49 | ||
| 50 | prob2_get_formula_type/3, | |
| 51 | ||
| 52 | get_states_for_predicate/3, | |
| 53 | ||
| 54 | filter_states_for_predicate/3, | |
| 55 | ||
| 56 | get_top_level_formulas/1, | |
| 57 | insert_formula_for_expansion/2, | |
| 58 | prob2_evaluate_bvisual2_formulas/3, | |
| 59 | prob2_evaluate_bvisual2_formulas/4, | |
| 60 | prob2_expand_bvisual2_formula/3, | |
| 61 | ||
| 62 | do_modelchecking/5, | |
| 63 | set_goal_for_model_checking/1, | |
| 64 | reset_goal_for_model_checking/0, | |
| 65 | compute_efficient_statespace_stats/3, | |
| 66 | compute_coverage/5, | |
| 67 | get_modelchecking_coverage/5, | |
| 68 | get_statistics/2, | |
| 69 | prob2_deadlock_freedom_check/2, | |
| 70 | prob2_invariant_check/2, | |
| 71 | prob2_redundant_invariants/2, | |
| 72 | ||
| 73 | ||
| 74 | ||
| 75 | get_enable_matrix/2, | |
| 76 | ||
| 77 | prob2_do_ltl_modelcheck/3, | |
| 78 | prob2_do_ltl_modelcheck/4, | |
| 79 | prob2_do_ctl_modelcheck/4, | |
| 80 | prob2_do_ctl_modelcheck/6, | |
| 81 | ||
| 82 | find_trace_to_node/2, | |
| 83 | find_trace_from_node_to_node/3, | |
| 84 | find_state_for_predicate/3, | |
| 85 | ||
| 86 | cbc_disprove/5, cbc_disprove/6, | |
| 87 | cbc_solve_with_opts/5, | |
| 88 | cbc_timed_solve_with_opts/6, | |
| 89 | pretty_print_predicate/3, | |
| 90 | cbc_generate_test_cases/3, | |
| 91 | prob2_find_test_path/4, | |
| 92 | ||
| 93 | ast_leaf_walks/2, | |
| 94 | ||
| 95 | ||
| 96 | check_csp_assertions/3, | |
| 97 | ||
| 98 | list_eclipse_preferences/1, | |
| 99 | list_all_eclipse_preferences/1, % also includes advanced eclipse preferences | |
| 100 | list_current_eclipse_preferences/1, | |
| 101 | get_eclipse_preference/2, | |
| 102 | set_eclipse_preference/2, | |
| 103 | ||
| 104 | get_signature_merge_state_space/2, | |
| 105 | get_transition_diagram/2, | |
| 106 | ||
| 107 | write_dotty_transition_diagram/2, | |
| 108 | write_dotty_signature_merge/2, | |
| 109 | write_dot_for_state_viz/2, | |
| 110 | write_dotty_state_space/1, | |
| 111 | is_dotty_command/1, write_dotty/2, | |
| 112 | is_dotty_command_for_expr/1, write_dotty_for_expr/3, | |
| 113 | get_dot_commands_in_state/2, call_dot_command_in_state/4, | |
| 114 | get_dot_commands_with_trace/2, call_dot_command_with_trace/4, | |
| 115 | get_plantuml_commands_in_state/2, call_plantuml_command_in_state/4, | |
| 116 | get_plantuml_commands_with_trace/2, call_plantuml_command_with_trace/4, | |
| 117 | get_table_commands_in_state/2, call_table_command_in_state/4, | |
| 118 | get_table_commands_with_trace/2, call_table_command_with_trace/4, | |
| 119 | ||
| 120 | get_error_messages_with_span_info/1, | |
| 121 | ||
| 122 | generate_trace_until_condition_fulfilled/4, | |
| 123 | execute_model/5, execute_model/6, | |
| 124 | get_unsat_core_with_fixed_conjuncts/3, | |
| 125 | get_minimum_unsat_core_with_fixed_conjuncts/3, | |
| 126 | ||
| 127 | prob2_construct_trace/6, | |
| 128 | prob2_find_trace/5, | |
| 129 | prob2_refine_trace/8, | |
| 130 | ||
| 131 | symbolic_model_check/2, | |
| 132 | ||
| 133 | % synthesis | |
| 134 | start_synthesis_from_ui_/13, | |
| 135 | start_synthesis_single_operation_from_ui_/11, | |
| 136 | get_valid_and_invalid_equality_predicates_for_operation_/6, | |
| 137 | get_valid_and_invalid_equality_predicates_for_invariants_/4, | |
| 138 | get_invariant_violating_vars_from_examples_/3, | |
| 139 | adapt_machine_code_for_operations_/2, | |
| 140 | reset_synthesis_context_/0, | |
| 141 | generate_data_from_machine_operation_/6, | |
| 142 | generate_synthesis_data_from_predicate_untyped_/5, | |
| 143 | generate_operation_data_from_machine_path_/4, | |
| 144 | ||
| 145 | get_pretty_print/1, get_pretty_print_unicode/1, | |
| 146 | get_machine_internal_representation/2, | |
| 147 | ||
| 148 | get_operations_and_names/2, | |
| 149 | ||
| 150 | get_primed_predicate/2, | |
| 151 | get_nonquantifying_primed_predicate/2, | |
| 152 | get_weakest_precondition/3, | |
| 153 | before_after_predicate/2, | |
| 154 | ||
| 155 | get_machine_operation_names/1, get_machine_operation_infos/1, get_machine_operation_infos_typed/1, | |
| 156 | get_machine_identifiers/2, | |
| 157 | get_machine_files/1, | |
| 158 | ||
| 159 | get_possible_completions/3, get_possible_completion/3, | |
| 160 | get_possible_fuzzy_matches/2, | |
| 161 | ||
| 162 | prob2_extended_static_check/1, | |
| 163 | prob2_check_well_definedness/2, | |
| 164 | prob2_ensure_wd/2, | |
| 165 | ||
| 166 | prob2_load_visb_file/1, | |
| 167 | prob2_get_loaded_visb_file/1, | |
| 168 | prob2_visb_file_loaded/2, | |
| 169 | prob2_visb_attributes_for_state/2, | |
| 170 | prob2_visb_click_events_and_hovers/2, prob2_visb_perform_click/4, | |
| 171 | prob2_visb_items/1, prob2_visb_svg_objects/1, prob2_visb_default_svg_file_contents/1, | |
| 172 | prob2_read_visb_path_from_definitions/1, | |
| 173 | prob2_export_visb_html_for_history/2, | |
| 174 | prob2_export_visb_html_for_history/3, | |
| 175 | prob2_export_visb_for_current_state/1, | |
| 176 | prob2_export_visb_html_for_states/3, | |
| 177 | prob2_get_visb_html_for_states/3, | |
| 178 | ||
| 179 | prob2_replay_json_trace_file/4, | |
| 180 | ||
| 181 | get_constants_predicate/1, | |
| 182 | replay_state_trace_from_file/3 | |
| 183 | ]). | |
| 184 | ||
| 185 | :- use_module(module_information). | |
| 186 | :- module_info(group,cli). | |
| 187 | :- module_info(description,'This module provides the new ProB2 Prolog interface to Java and other languages (usually called via socket server).'). | |
| 188 | ||
| 189 | :- use_module(library(sets)). % list_to_set | |
| 190 | :- use_module(state_space, [time_out_for_node/1, time_out_for_node/3, | |
| 191 | time_out_for_invariant/1, max_reached_for_node/1, | |
| 192 | max_reached_or_timeout_for_node/1, | |
| 193 | visited_expression/2, transition/4, visited_expression_id/1, | |
| 194 | set_context_state/2, clear_context_state/0, | |
| 195 | state_error/3, current_state_id/1, set_current_state_id/1, | |
| 196 | get_state_space_stats/3, | |
| 197 | try_set_trace_by_transition_ids/1 | |
| 198 | ]). | |
| 199 | :- use_module(external_functions,[set_current_state_for_external_fun/1, clear_state_for_external_fun/0]). | |
| 200 | % new profiler | |
| 201 | %:- use_module('../extensions/profiler/profiler.pl'). | |
| 202 | ||
| 203 | ||
| 204 | :- use_module(eventhandling, [announce_event/1]). | |
| 205 | :- use_module(version, [version/4, revision/1, lastchangeddate/1]). | |
| 206 | :- use_module(pref_definitions, [b_get_preferences_from_specification/0, b_get_preferences_from_specification/1]). | |
| 207 | :- use_module(bsyntaxtree, [conjunct_predicates/2, get_texpr_type/2, | |
| 208 | get_texpr_expr/2, | |
| 209 | find_identifier_uses/3]). | |
| 210 | :- use_module(state_space_exploration_modes,[set_depth_breadth_first_mode/1]). | |
| 211 | :- use_module(bmachine, [b_type_expression/5, b_get_machine_operation/4, b_get_machine_operation/6, | |
| 212 | b_type_open_predicate/5, b_top_level_operation/1, | |
| 213 | get_machine_operation_additional_identifiers/2, | |
| 214 | b_load_machine_from_list_of_facts/2, | |
| 215 | b_set_eventb_project_flat/3, load_additional_information/1, | |
| 216 | b_machine_precompile/0, other_spec_precompile/0, | |
| 217 | b_set_parsed_typed_machine_goal/1, | |
| 218 | b_is_variable/2, b_is_constant/1, b_is_variable/1, b_is_constant/2 | |
| 219 | ]). | |
| 220 | :- use_module(probltlsrc(ctl), [ctl_model_check_with_ast/6]). | |
| 221 | :- use_module(probltlsrc(ltl), [ltl_model_check_with_ce/4,preprocess_formula/2]). | |
| 222 | :- use_module(probltlsrc(ltl_tools), [typecheck_temporal_formula/3]). | |
| 223 | :- use_module(probltlsrc(ltl_verification), [evaluate_ltl_formula/6]). | |
| 224 | :- use_module(b_interpreter, [b_test_boolean_expression_cs/5, b_compute_expression_nowf/6]). | |
| 225 | :- use_module(b_global_sets, [add_prob_deferred_set_elements_to_store/3]). | |
| 226 | :- use_module(extension('user_signal/user_signal'), [user_interruptable_call_det/2, | |
| 227 | ignore_user_interrupt_det/1]). | |
| 228 | :- use_module(library(lists), [maplist/2, maplist/3, maplist/4]). | |
| 229 | :- use_module(library(codesio), [read_from_codes/2, write_term_to_codes/4]). | |
| 230 | :- use_module(specfile, [expand_const_and_vars_to_full_store/2, animation_mode/1, | |
| 231 | csp_mode/0, | |
| 232 | b_or_z_mode/0, xtl_mode/0, | |
| 233 | set_currently_opened_file/1, set_currently_opened_b_file/1, | |
| 234 | set_minor_animation_mode_from_file/1, | |
| 235 | set_currently_opening_file/1, set_failed_to_open_file/1, | |
| 236 | set_currently_opened_package/1, animation_minor_mode/1, | |
| 237 | set_animation_mode/1, set_animation_minor_mode/1]). | |
| 238 | :- use_module(translate, [with_translation_mode/2, get_language_mode/1, with_language_mode/2, | |
| 239 | translate_bvalue_for_expression/3, | |
| 240 | suppress_rodin_positions/1, reset_suppress_rodin_positions/1, | |
| 241 | translate_event/2, translate_bstate/2, translate_state_error/2, | |
| 242 | translate_bexpression/2, translate_bvalue_with_limit/3, | |
| 243 | translate_event_error/2, explain_event_trace/3, explain_state_error/3]). | |
| 244 | :- use_module(error_manager, [add_error_and_fail/3, | |
| 245 | get_all_errors_with_span_info_and_reset/1, | |
| 246 | get_all_errors_with_span_and_context_and_reset/1, | |
| 247 | add_error/3, add_error/2, | |
| 248 | add_message/2, add_message/3, reset_errors/0, | |
| 249 | add_warning/3, | |
| 250 | add_all_perrors/1, | |
| 251 | no_real_perror_occurred/1, | |
| 252 | get_error/2, | |
| 253 | catch_enumeration_warning_exceptions/2, | |
| 254 | real_error_occurred/0, | |
| 255 | warning_occurred/0]). | |
| 256 | :- use_module(tools, [string_concatenate/3, split_atom/3, | |
| 257 | safe_atom_codes/2,ajoin/2]). | |
| 258 | :- use_module(extrasrc(bvisual2), [bv_get_top_level/1, | |
| 259 | bv_insert_formula/3, bv_expand_formula/3, | |
| 260 | bv_formula_description/2, bv_formula_discharged_info/2, | |
| 261 | bv_get_values/3, bv_get_values_unlimited/3, | |
| 262 | bv_get_formula_functor_symbol/2, bv_formula_labels/2, | |
| 263 | bv_is_typed_predicate/1, bv_is_typed_formula/1]). | |
| 264 | :- use_module(preferences, [eclipse_preference/2, get_preference/2, | |
| 265 | preference_description/2, preference_val_type/2, | |
| 266 | preference_default_value/2, preference_category/2, | |
| 267 | set_preference/2, advanced_eclipse_preference/2, | |
| 268 | deprecated_eclipse_preference/4, | |
| 269 | obsolete_eclipse_preference/1]). | |
| 270 | :- use_module(disproversrc(disprover), [disprove/5, disprove_with_opts/6]). | |
| 271 | :- use_module(solver_interface, [solve_predicate/5, | |
| 272 | call_with_smt_mode_enabled/1]). | |
| 273 | :- use_module(probcspsrc(haskell_csp), [parse_and_load_cspm_file/1]). | |
| 274 | :- use_module(dotsrc(state_space_reduction),[reset_ignored_events/0, set_ignored_events/1, | |
| 275 | compute_signature_merge/0, compute_transition_diagram/1, | |
| 276 | get_reduced_node/4, reduced_trans/5, | |
| 277 | generate_node_color/5, generate_node_labels/3, | |
| 278 | generate_transition_label/3, generate_transition_color_and_style/6, | |
| 279 | write_signature_merge_to_dotfile/2]). | |
| 280 | :- use_module(dotsrc(state_as_dot_graph),[print_cstate_graph/2]). | |
| 281 | :- use_module(debug, [debug_println/2]). | |
| 282 | :- use_module(extrasrc(unsat_cores), [unsat_chr_core_with_fixed_conjuncts_auto_time_limit/4, | |
| 283 | minimum_unsat_core_with_fixed_conjuncts/3]). | |
| 284 | :- use_module(smt_solvers_interface(smt_solvers_interface), [smt_solve_predicate_in_state/5, smt_solve_predicate/4]). | |
| 285 | ||
| 286 | :- use_module(typechecker). | |
| 287 | :- use_module(self_check). | |
| 288 | ||
| 289 | :- use_module(synthesis('deep_learning/predicate_data_generator'), [generate_synthesis_data_from_predicate_untyped/5]). | |
| 290 | :- use_module(synthesis('deep_learning/operation_data_generator'), [generate_operation_data_from_machine_path/4, | |
| 291 | generate_data_from_machine_operation/6]). | |
| 292 | ||
| 293 | :- use_module(synthesis(b_synthesis),[start_synthesis_from_ui/13, | |
| 294 | start_synthesis_single_operation_from_ui/11, | |
| 295 | reset_synthesis_context/0]). | |
| 296 | :- use_module(synthesis(synthesis_util),[get_valid_and_invalid_equality_predicates_for_operation/6, | |
| 297 | get_valid_and_invalid_equality_predicates_for_invariants/4, | |
| 298 | get_invariant_violating_vars_from_examples/3, | |
| 299 | adapt_machine_code_for_operations/2]). | |
| 300 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 301 | ||
| 302 | /** | |
| 303 | Access information about the current version of the ProB core. | |
| 304 | ||
| 305 | #### called by: | |
| 306 | * ProB 2.0: GetVersionCommand | |
| 307 | */ | |
| 308 | get_version(Major,Minor,Service,Qualifier,GitRevision,LastChangedDate,PrologInfo) :- | |
| 309 | version(Major,Minor,Service,Qualifier), | |
| 310 | revision(GitRevision), lastchangeddate(LastChangedDate), current_prolog_flag(version,PrologInfo). | |
| 311 | ||
| 312 | :- use_module(extension('user_signal/user_signal'),[get_user_signal_ref/1]). | |
| 313 | % only used by probproxy: | |
| 314 | get_user_signal_reference(Ref) :- get_user_signal_ref(Ref). | |
| 315 | ||
| 316 | % get the total number of errors of ProB's Prolog code; cannot be accidentally reset | |
| 317 | % useful for validation reports,... | |
| 318 | :- use_module(error_manager,[get_total_number_of_errors/1]). | |
| 319 | get_prob_total_number_of_errors(X) :- get_total_number_of_errors(X). | |
| 320 | ||
| 321 | /* ------------------------- */ | |
| 322 | /* B Loading Interface */ | |
| 323 | /* ------------------------- */ | |
| 324 | ||
| 325 | /** | |
| 326 | load_classical_b_from_list_of_facts(+MainFilename,+ListOfFacts) | |
| 327 | ||
| 328 | Loads a classical b model. | |
| 329 | ||
| 330 | #### called by: | |
| 331 | * ProB 2.0: LoadBProjectCommand | |
| 332 | */ | |
| 333 | load_classical_b_from_list_of_facts(MainFilename,ListOfFacts) :- | |
| 334 | clear_animator, | |
| 335 | set_animation_mode(b), | |
| 336 | set_currently_opening_file(MainFilename), | |
| 337 | (b_load_machine_from_list_of_facts(MainFilename,ListOfFacts) | |
| 338 | -> set_currently_opened_b_file(MainFilename), | |
| 339 | update_preferences_from_spec | |
| 340 | ; set_failed_to_open_file(MainFilename), fail). | |
| 341 | ||
| 342 | /** | |
| 343 | update preferences from SET_PREF Definitions in B machines: | |
| 344 | should be called after loading a model and before start_animation | |
| 345 | */ | |
| 346 | update_preferences_from_spec :- | |
| 347 | ((b_or_z_mode ; xtl_mode) -> b_get_preferences_from_specification ; true). | |
| 348 | update_preferences_from_spec(List) :- | |
| 349 | ((b_or_z_mode ; xtl_mode) -> b_get_preferences_from_specification(List) ; List=[]). | |
| 350 | ||
| 351 | /* ------------------------- */ | |
| 352 | /* Event-B Loading Interface */ | |
| 353 | /* ------------------------- */ | |
| 354 | ||
| 355 | /** | |
| 356 | Loads an Event-B model. | |
| 357 | ||
| 358 | #### called by: | |
| 359 | * ProB Plugin: de.prob.eventb.translator.internal.EventBTranslator, DisproverLoadCommand | |
| 360 | * ProB 2.0: de.prob.model.eventb.translate.EventBModelTranslator (LoadEventBProjectCommand) | |
| 361 | */ | |
| 362 | load_event_b_project(Machines,Contexts,Proofs,Errors) :- | |
| 363 | clear_animator, | |
| 364 | % set_animation_mode(b), set_animation_minor_mode(eventb), now done in b_set_eventb_project_flat | |
| 365 | b_set_eventb_project_flat(Machines,Contexts,Proofs), | |
| 366 | load_additional_information(Proofs), | |
| 367 | Errors = [], | |
| 368 | set_currently_opened_package(event_b_project). | |
| 369 | ||
| 370 | /* ------------------------- */ | |
| 371 | /* CSP Loading Interface */ | |
| 372 | /* ------------------------- */ | |
| 373 | ||
| 374 | /** | |
| 375 | load_cspm_spec_from_cspm_file(+CSPMFile) | |
| 376 | ||
| 377 | Takes a path to a CSPM specification and loads the file using the CSPM parser. | |
| 378 | ||
| 379 | #### called by: | |
| 380 | * ProB 2.0: LoadCSPCommand | |
| 381 | */ | |
| 382 | load_cspm_spec_from_cspm_file(CSPMFile) :- | |
| 383 | clear_animator, | |
| 384 | set_animation_mode(cspm), | |
| 385 | set_currently_opening_file(CSPMFile), | |
| 386 | parse_and_load_cspm_file(CSPMFile), | |
| 387 | !, | |
| 388 | set_currently_opened_file(CSPMFile). | |
| 389 | load_cspm_spec_from_cspm_file(CSPMFile) :- set_failed_to_open_file(CSPMFile),fail. | |
| 390 | ||
| 391 | ||
| 392 | /* ------------------------- */ | |
| 393 | /* Z Loading Interface */ | |
| 394 | /* ------------------------- */ | |
| 395 | ||
| 396 | :- use_module(bmachine,[b_set_typed_machine/2]). | |
| 397 | :- use_module(parsercall,[call_fuzz_parser/2]). | |
| 398 | :- use_module(prozsrc(proz),[open_proz_file/2]). | |
| 399 | load_fuzz_file_internal(FuzzFile) :- | |
| 400 | open_proz_file(FuzzFile,BMachine), | |
| 401 | b_set_typed_machine(BMachine,FuzzFile). | |
| 402 | ||
| 403 | load_z_spec_from_fuzz_file(FuzzFile) :- | |
| 404 | clear_animator, | |
| 405 | set_animation_mode(b), set_animation_minor_mode(z), | |
| 406 | set_currently_opening_file(FuzzFile), | |
| 407 | (load_fuzz_file_internal(FuzzFile) | |
| 408 | -> set_currently_opened_b_file(FuzzFile) | |
| 409 | ; set_failed_to_open_file(FuzzFile),fail | |
| 410 | ). | |
| 411 | ||
| 412 | load_z_spec_from_tex_file(TexFile) :- | |
| 413 | clear_animator, | |
| 414 | call_fuzz_parser(TexFile,FuzzFile), | |
| 415 | load_z_spec_from_fuzz_file(FuzzFile). | |
| 416 | ||
| 417 | /* ------------------------- */ | |
| 418 | /* XTL Loading Interface */ | |
| 419 | /* ------------------------- */ | |
| 420 | ||
| 421 | :- use_module(xtl_interface,[open_xtl_file/1]). | |
| 422 | :- use_module(bmachine,[b_set_empty_machine/0]). | |
| 423 | load_xtl_spec_from_prolog_file(PrologFile) :- | |
| 424 | clear_animator, | |
| 425 | set_animation_mode(xtl), | |
| 426 | b_set_empty_machine, | |
| 427 | set_currently_opening_file(PrologFile), | |
| 428 | (open_xtl_file(PrologFile) | |
| 429 | -> set_currently_opened_file(PrologFile), | |
| 430 | update_preferences_from_spec | |
| 431 | ; set_failed_to_open_file(PrologFile),fail | |
| 432 | ). | |
| 433 | ||
| 434 | :- use_module(probsrc('alloy2b/alloy2b'),[load_alloy_model/2]). | |
| 435 | load_alloy_spec_from_term(PrologTerm,AlloyFile) :- | |
| 436 | clear_animator, | |
| 437 | load_alloy_model(PrologTerm,AlloyFile). | |
| 438 | /* ------------------------- */ | |
| 439 | /* Animation */ | |
| 440 | /* ------------------------- */ | |
| 441 | ||
| 442 | reset_animator :- announce_event(reset_specification). % just reset; keeping same spec | |
| 443 | clear_animator :- reset_animator,announce_event(clear_specification). | |
| 444 | ||
| 445 | /** | |
| 446 | prob2_reset_prob | |
| 447 | ||
| 448 | Reset ProB to a clean state as if it was newly started | |
| 449 | (except for total_number_of_errors). | |
| 450 | ||
| 451 | #### called by: | |
| 452 | * ProB 2.0: ResetProBCommand | |
| 453 | */ | |
| 454 | prob2_reset_prob :- announce_event(clear_specification), announce_event(reset_prob). | |
| 455 | ||
| 456 | start_animation :- %reset_errors, % we no longer reset_errors here ! | |
| 457 | initialise_specification,!. | |
| 458 | start_animation :- add_error(start_animation,'Start Animation Failed'). | |
| 459 | %NOW done by events: reset_flow, state_space_initialise, reduce_graph_reset, reset_runtime_profiler, | |
| 460 | % reset_refinement_checker reset_model_checker, | |
| 461 | % reset_dynamics, % new profiler | |
| 462 | ||
| 463 | %:- use_module(eventhandling,[register_event_listener/3]). | |
| 464 | %:- register_event_listener(clear_specification,reset_prob2_interface, | |
| 465 | % 'Reset prob2_interface caches.'). | |
| 466 | %reset_prob2_interface. | |
| 467 | ||
| 468 | ||
| 469 | initialise_specification :- /* call once before starting animation or model checking */ | |
| 470 | announce_event(start_initialising_specification), | |
| 471 | ( b_or_z_mode -> b_machine_precompile | |
| 472 | ; | |
| 473 | preferences:get_preference(symmetry_mode,X), | |
| 474 | ( X=off -> true | |
| 475 | ; | |
| 476 | add_message(initialise_specification,'Symmetry can only be used for B & Z specifications'), | |
| 477 | preferences:set_preference(symmetry_mode,off) /* Turn symmetry off */ | |
| 478 | ), | |
| 479 | %tools:print_bt_message(other_spec_precompile), | |
| 480 | other_spec_precompile | |
| 481 | ), | |
| 482 | %TODO(DP,11.8.2008) | |
| 483 | % now done in state_space: user:initialise_operation_not_yet_covered, | |
| 484 | % now done via event_handline: reset_external_functions, | |
| 485 | announce_event(specification_initialised). | |
| 486 | ||
| 487 | /* ------------------------- */ | |
| 488 | /* Handling States */ | |
| 489 | /* ------------------------- */ | |
| 490 | ||
| 491 | /** | |
| 492 | serialize(+Id,-SerializedState) | |
| 493 | ||
| 494 | Produces a prolog serialization of a given state id | |
| 495 | ||
| 496 | #### called by: | |
| 497 | * ProB 2.0: SerializeStateCommand | |
| 498 | */ | |
| 499 | serialize(Id,SerializedState) :- | |
| 500 | visited_expression(Id,State), | |
| 501 | write_term_to_codes(State,Codes,[0'.],[quoted(true)]), %' | |
| 502 | atom_codes(SerializedState,Codes). | |
| 503 | ||
| 504 | /** | |
| 505 | deserialize(-NewId,+SerializedState) | |
| 506 | ||
| 507 | Deserialize a state and add it if necessary | |
| 508 | ||
| 509 | #### called by: | |
| 510 | * ProB 2.0: DeserializeStateCommand | |
| 511 | */ | |
| 512 | :- use_module(state_space_exploration_modes,[get_id_of_node_and_add_if_required/6]). | |
| 513 | deserialize(NewId,SerializedState) :- | |
| 514 | atom_codes(SerializedState,Codes), | |
| 515 | read_from_codes(Codes,State), | |
| 516 | get_id_of_node_and_add_if_required(State,NewId,_Res,root,'$unknown_operation',[]). | |
| 517 | ||
| 518 | get_state(ID,BState) :- get_state(ID,BState,_,_). | |
| 519 | get_state(ID,BState,Kind,ConstID) :- | |
| 520 | if(visited_expression(ID,State),true,(ID=root,State=root)), | |
| 521 | get_state2(State,BState,Kind), | |
| 522 | get_constants_id(State,ID,ConstID). | |
| 523 | get_state2(csp_and_b(CSPState,BState),[bind('CSP_CONTROLLER',CSPState)|ExpandedBState],Kind) :- !, | |
| 524 | get_state2(BState,ExpandedBState,Kind). | |
| 525 | get_state2(concrete_constants(BState),BState,constants_only_state) :- !. | |
| 526 | get_state2(root,BState,empty_state) :- !, BState=[]. | |
| 527 | get_state2(State,Res,full_initialised_state) :- | |
| 528 | expand_const_and_vars_to_full_store(State,BState), | |
| 529 | (BState=[_|_] -> Res=BState ; Res=[] /* we have [] or a CSP process or similar */). | |
| 530 | ||
| 531 | get_constants_id(const_and_vars(ConstID,_),_,Res) :- !,Res=ConstID. | |
| 532 | get_constants_id(concrete_constants(_),ConstID,Res) :- !,Res=ConstID. | |
| 533 | get_constants_id(_,_,-1). | |
| 534 | ||
| 535 | /** | |
| 536 | Get the predicate representation of a BState | |
| 537 | ||
| 538 | #### called by: | |
| 539 | * ProB 2.0: GetBStateCommand | |
| 540 | */ | |
| 541 | get_b_state(StateId, BState) :- | |
| 542 | get_state(StateId, S), translate_bstate(S, BState). | |
| 543 | ||
| 544 | /** | |
| 545 | compute_operations_for_state(+StateID,-Transitions) | |
| 546 | ||
| 547 | Compute the enabled operations (without the backtrack options) for a given state id. | |
| 548 | Transitions is a list of operation tuples with the form op(TransitionId, Name,SrcId,DestId) | |
| 549 | ||
| 550 | #### called by: | |
| 551 | * ProB 2.0: GetEnabledOperationsCommand | |
| 552 | */ | |
| 553 | compute_operations_for_state(StateID, Transitions) :- | |
| 554 | visited_expression_id(StateID), | |
| 555 | tcltk_interface:tcltk_compute_options(StateID,OpsSTAndIDs), | |
| 556 | (create_simple_op_terms(OpsSTAndIDs,StateID,Transitions) -> true | |
| 557 | ; add_error_and_fail(prob2_interface, 'Creating op terms failed', OpsSTAndIDs)). | |
| 558 | ||
| 559 | create_simple_op_terms([],_,[]). | |
| 560 | create_simple_op_terms([(Id,Op,Dst)|T],StateID,[op(Id,Name,StateID,Dst)|FT]) :- | |
| 561 | extract_op_name(Op,Name), | |
| 562 | create_simple_op_terms(T,StateID,FT). | |
| 563 | ||
| 564 | set_current_state(ID) :- current_state_id(ID),!. % no need to jump | |
| 565 | set_current_state(ID) :- /* jumps to the given node; can be backtracked */ | |
| 566 | visited_expression_id(ID), | |
| 567 | tcltk_interface:tcltk_goto_state(jump,ID). | |
| 568 | ||
| 569 | :- use_module(specfile,[max_operations_zero_for_operation/1]). | |
| 570 | :- use_module(tcltk_interface,[potentially_enabled_operation/4]). | |
| 571 | % in case of MAX_OPERATIONS=0 just show the additional potentially enabled operations after compute_operations_for_state | |
| 572 | % GuardPrecise is either precise or imprecise | |
| 573 | % TimeOutOccurred is either true or false | |
| 574 | compute_additional_candidate_operations_for_state(StateID, Candidates) :- | |
| 575 | findall(candidate(OpName,TimeOutOccurred,GuardPrecise), | |
| 576 | (b_or_z_mode, | |
| 577 | max_operations_zero_for_operation(OpName), | |
| 578 | potentially_enabled_operation(StateID,OpName,TimeOutOccurred,GuardPrecise)),Candidates). | |
| 579 | ||
| 580 | /** | |
| 581 | prob2_execute_custom_operations(+CurID, +OpName, +ParsedPredicate, +MaxNrOfSolutions, -TOperations, -Errors) | |
| 582 | ||
| 583 | Calculates an operation given a predicate from the user. | |
| 584 | ||
| 585 | #### called by: | |
| 586 | * ProB 2.0: GetOperationByPredicateCommand | |
| 587 | */ | |
| 588 | :- use_module(bmachine,[b_is_operation_name/1, b_is_initialisation_name/1]). | |
| 589 | prob2_execute_custom_operations(_CurID, _OpName, _Pred, MaxNrOfSolutions, TOps, Errs) :- | |
| 590 | MaxNrOfSolutions < 1, | |
| 591 | !, | |
| 592 | TOps = [],Errs = ['max nr of solutions too small']. | |
| 593 | prob2_execute_custom_operations(_CurID, OpName, _Pred, _Max, TOps, Errs) :- | |
| 594 | \+ valid_op_name(OpName), | |
| 595 | !, | |
| 596 | TOps = [], | |
| 597 | (b_is_operation_name(OpName) -> ajoin(['Not a Top-Level Operation ', OpName], Msg) | |
| 598 | ; ajoin(['Unknown Operation ', OpName], Msg)), | |
| 599 | Errs = [Msg]. | |
| 600 | prob2_execute_custom_operations(CurID, OpName, ParsedPredicate, MaxNrOfSolutions, TOperations, ErrorsOut) :- | |
| 601 | set_current_state(CurID), | |
| 602 | prob2_execute_custom_operations_aux(CurID, OpName, ParsedPredicate, MaxNrOfSolutions, TOperations, ErrorsOut). | |
| 603 | ||
| 604 | % special case for TRUE=TRUE predicate to avoid parser overhead | |
| 605 | prob2_execute_custom_operations_aux(CurID, OpName, Pred, MaxNrOfSolutions, TOperations, ErrorsOut) :- | |
| 606 | raw_truth(Pred),!, | |
| 607 | findall(TO, prob2_execute_custom_operation(CurID,OpName,TO,MaxNrOfSolutions), TOperations), | |
| 608 | (TOperations = [] | |
| 609 | -> gen_exec_error_message(CurID,OpName,truth,Msg), | |
| 610 | ErrorsOut = [Msg] | |
| 611 | ; ErrorsOut = []). | |
| 612 | prob2_execute_custom_operations_aux(CurID, OpName, ParsedPredicate, MaxNrOfSolutions, TOperations, ErrorsOut) :- | |
| 613 | ( is_special_op(OpName,_) | |
| 614 | -> Scope = [prob_ids(visible),variables,external_library(all_available_libraries)] | |
| 615 | ; %b_top_level_operation(OpName), | |
| 616 | get_machine_operation_additional_identifiers(OpName,AdditionalIds), | |
| 617 | % adds parameters, results and x$0 refers to variable value of variable x before operation | |
| 618 | Scope = [identifier(AdditionalIds),prob_ids(visible),variables,external_library(all_available_libraries)] | |
| 619 | % prob scope allows one to use identifiers for deferred set elements | |
| 620 | ), | |
| 621 | b_type_expression(ParsedPredicate, Scope, _, TypedPred, Errors), | |
| 622 | (Errors = [] -> | |
| 623 | findall(TO, prob2_execute_custom_operation_with_predicate(CurID,OpName,TypedPred,TO,MaxNrOfSolutions), | |
| 624 | TOperations), | |
| 625 | retractall(bmachine:b_machine_temp_predicate(_)), | |
| 626 | (TOperations = [] | |
| 627 | -> gen_exec_error_message(CurID,OpName,TypedPred,Msg), | |
| 628 | ErrorsOut = [Msg] | |
| 629 | ; ErrorsOut = []) | |
| 630 | ; TOperations = [], | |
| 631 | ErrorsOut = [typechecker_errors(Errors)] | |
| 632 | ). | |
| 633 | ||
| 634 | :- use_module(specfile,[get_operation_name/2]). | |
| 635 | :- use_module(state_space,[is_concrete_constants_state_id/1]). | |
| 636 | gen_exec_error_message(root,OpName,_,Msg) :- \+ is_special_op(OpName,_),!, | |
| 637 | ajoin(['Machine is not initialised, could not execute operation ', OpName], Msg). | |
| 638 | gen_exec_error_message(CurID,OpName,_,Msg) :- is_concrete_constants_state_id(CurID), | |
| 639 | \+ is_special_op(OpName,_),!, | |
| 640 | ajoin(['Machine is not initialised, could not execute operation ', OpName], Msg). | |
| 641 | gen_exec_error_message(CurID,'$setup_constants',_,Msg) :- is_concrete_constants_state_id(CurID), | |
| 642 | !, | |
| 643 | Msg = 'Constants are already set up, could not execute SETUP_CONSTANTS '. | |
| 644 | gen_exec_error_message(CurID,OpName,_,Msg) :- | |
| 645 | CurID \= root, | |
| 646 | \+ is_concrete_constants_state_id(CurID), | |
| 647 | is_special_op(OpName,OpS), !, | |
| 648 | ajoin(['Machine is already initialised, cannot execute ', OpS], Msg). | |
| 649 | gen_exec_error_message(ID,OpName,truth,Msg) :- !, | |
| 650 | (is_special_op(OpName,OpS) -> true ; OpS=OpName), | |
| 651 | ajoin(['Could not execute operation ', OpS, ' in state ', ID], Msg). | |
| 652 | gen_exec_error_message(ID,OpName,_,Msg) :- (is_special_op(OpName,OpS) -> true ; OpS=OpName), | |
| 653 | (transition(ID,Op,_,_), get_operation_name(Op,OpName) | |
| 654 | -> M2 = ' (but a transition for operation exists)' ; M2 = ''), | |
| 655 | ajoin(['Could not execute operation ', OpS, ' in state ', ID, ' with additional predicate',M2], Msg). | |
| 656 | is_special_op('$setup_constants','SETUP_CONSTANTS'). | |
| 657 | is_special_op('$initialise_machine','INITIALISATION'). | |
| 658 | ||
| 659 | % true if a raw expression definitely represents truth | |
| 660 | raw_truth(equal(_,E1,E2)) :- raw_equals(E1,E2). | |
| 661 | raw_equals(boolean_true(_),boolean_true(_)). | |
| 662 | raw_equals(boolean_false(_),boolean_false(_)). | |
| 663 | raw_equals(integer(_,I),integer(_,I)). | |
| 664 | valid_op_name('$initialise_machine'). | |
| 665 | valid_op_name('$setup_constants'). | |
| 666 | valid_op_name(OpName) :- b_top_level_operation(OpName). | |
| 667 | %valid_op_name(OpName) :- b_get_promoted_machine_operations(OpName). | |
| 668 | ||
| 669 | ||
| 670 | ||
| 671 | prob2_find_trace(CurId,Names,Preds,OpsOut,ErrOut) :- | |
| 672 | find_trace(CurId,Names,Preds,[],OpsOut,[],ErrOut),!, | |
| 673 | print(OpsOut),nl. | |
| 674 | ||
| 675 | ||
| 676 | find_trace_iterator([], _Names,_Preds, CurOut, CurOut,CurErrOut,CurErrOut ). | |
| 677 | ||
| 678 | find_trace_iterator([CurID|RestID], NameList, PredList, [CurOps | RestCandidates], [CurOpsOut|RestCandidatesOut], CurErrOut, ErrOut):- | |
| 679 | find_trace(CurID, NameList, PredList, CurOps, CurOpsOut, CurErrOut, ErrOut1), | |
| 680 | find_trace_iterator(RestID, NameList, PredList, RestCandidates, RestCandidatesOut, CurErrOut, ErrOut2), | |
| 681 | append(ErrOut1, ErrOut2, ErrOut). | |
| 682 | ||
| 683 | %expects result of length 1 | |
| 684 | find_trace(_CurId,[],[],OpsOutIn,OpsOutIn,ErrOut,ErrOut). | |
| 685 | find_trace(CurId,[Name|Names],[Pred|Preds],CurOpsOut,OpsOut,CurErrOut,ErrOut) :- | |
| 686 | prob2_execute_custom_operations(CurId,Name,Pred,10,ListOfListOfOps,SingleErr), | |
| 687 | (ListOfListOfOps = [] -> | |
| 688 | OpsOut=CurOpsOut, | |
| 689 | append(CurErrOut, SingleErr, ErrOut) %% No transitions found -> return with the current state | |
| 690 | ; | |
| 691 | find_new_ids(ListOfListOfOps, IdsList), | |
| 692 | pack_as_list(ListOfListOfOps, ListOfListOfOpsPacked), %%Start a new exploration path for each solution | |
| 693 | maplist(append(CurOpsOut),ListOfListOfOpsPacked,NewOpsOut), | |
| 694 | append(CurErrOut,SingleErr,NewErrOut), | |
| 695 | find_trace_iterator(IdsList,Names,Preds,NewOpsOut,OpsOutIn,NewErrOut,ErrOut), | |
| 696 | longest_match(OpsOutIn,[], OpsOut) | |
| 697 | ). | |
| 698 | ||
| 699 | ||
| 700 | refine_trace_start_kick_off(CurID, [OP|RestOP], [Preds|RestPreds], RefineAlternatives, RefinesSkip, Result, MaxDepth, MaxBreadth) :- | |
| 701 | refine_trace_step(CurID, OP, Preds, RefineAlternatives, RefinesSkip, [], TransitionTakenOut, [], Solutions, IdsList, MaxDepth, MaxBreadth), | |
| 702 | create_traces(IdsList, Solutions, TransitionTakenOut, AllTraces), | |
| 703 | refine_trace_main_loop(AllTraces, RestOP, RestPreds, RefineAlternatives, RefinesSkip, Result, MaxDepth, MaxBreadth). | |
| 704 | ||
| 705 | refine_trace_main_loop(AllTraces, [], [], _RefineAlternatives, _RefinesSkip, AllTraces, _MaxDepth, _MaxBreadth). | |
| 706 | ||
| 707 | refine_trace_main_loop(AllTraces, [OP | RestOP], [Preds | RestPred], RefineAlternatives, RefinesSkip, Result, MaxDepth, MaxBreadth) :- | |
| 708 | find_path(AllTraces, OP, Preds, RefineAlternatives, RefinesSkip, Results, MaxDepth, MaxBreadth), | |
| 709 | strip_ID(Results, StrippedIDs), | |
| 710 | list_to_set(StrippedIDs, Set), | |
| 711 | select_with_ID(Set, Results, MinimizedResults), | |
| 712 | (MinimizedResults = [] -> Result = []; | |
| 713 | take_best(MinimizedResults, BestResults), | |
| 714 | (BestResults = [] -> | |
| 715 | refine_trace_main_loop(MinimizedResults, [OP | RestOP], [Preds | RestPred], RefineAlternatives, RefinesSkip, Result, MaxDepth, MaxBreadth); % Skip/Stuttering step | |
| 716 | (refine_trace_main_loop(BestResults, RestOP, RestPred, RefineAlternatives, RefinesSkip, PreResult, MaxDepth, MaxBreadth) -> % Normal step | |
| 717 | Result = PreResult; | |
| 718 | refine_trace_main_loop(MinimizedResults, [OP | RestOP], [Preds | RestPred], RefineAlternatives, RefinesSkip, Result, MaxDepth, MaxBreadth) % Skip/Stuttering after normal step led to dead end | |
| 719 | ) | |
| 720 | ) | |
| 721 | ). | |
| 722 | ||
| 723 | ||
| 724 | ||
| 725 | select_with_ID([], _, []). | |
| 726 | ||
| 727 | select_with_ID([First | Rest], [trace(First, R,B)|TraceRest], [trace(First, R,B)| RestResult]) :- | |
| 728 | select_with_ID(Rest, TraceRest, RestResult). | |
| 729 | ||
| 730 | select_with_ID([First | Rest], [trace(Second, _,_)|TraceRest], RestResult) :- | |
| 731 | First \= Second, | |
| 732 | select_with_ID([First | Rest], TraceRest, RestResult). | |
| 733 | ||
| 734 | ||
| 735 | strip_ID([], []). | |
| 736 | ||
| 737 | strip_ID([trace(ID, _, _) | List], [ID | Rest]):- | |
| 738 | strip_ID(List, Rest). | |
| 739 | ||
| 740 | ||
| 741 | find_path([], _OP, _Preds, _RefineAlternatives, _RefinesSkip, [], _MaxDepth, _MaxBreadth). | |
| 742 | ||
| 743 | find_path([trace(CurID, TraceInput, TransitionTakenIn) | RestTraces], OP, Preds, RefineAlternatives, RefinesSkip, AllTraces, MaxDepth, MaxBreadth) :- | |
| 744 | refine_trace_step(CurID, OP, Preds, RefineAlternatives, RefinesSkip, TransitionTakenIn, TransitionTakenOut, TraceInput, Solutions, IdsList, MaxDepth, MaxBreadth), | |
| 745 | create_traces(IdsList, Solutions, TransitionTakenOut, Traces), | |
| 746 | take_best(Traces, NextResult), | |
| 747 | find_path(RestTraces, OP, Preds, RefineAlternatives, RefinesSkip, Results, MaxDepth, MaxBreadth), | |
| 748 | (NextResult = [] -> | |
| 749 | append(Results, Traces, AllTraces); | |
| 750 | append(Results, NextResult, AllTraces)). | |
| 751 | ||
| 752 | ||
| 753 | create_traces([],[],[],[]). | |
| 754 | ||
| 755 | create_traces([FIds |Ids], [FSolutions | Solutions], [FSkips | Skips], [trace(FIds, FSolutions, FSkips) | Rest]) :- | |
| 756 | create_traces(Ids, Solutions, Skips, Rest). | |
| 757 | ||
| 758 | ||
| 759 | take_best([], []). | |
| 760 | ||
| 761 | take_best([trace(FIds, FSolutions, []) | Rest], [trace(FIds, FSolutions, [])| ORest]) :- !, | |
| 762 | take_best(Rest, ORest). | |
| 763 | ||
| 764 | take_best([trace(_, _, _) | Rest], ORest) :- | |
| 765 | take_best(Rest, ORest). | |
| 766 | ||
| 767 | ||
| 768 | refine_trace_step(_CurId, [], [], _RefineAlternatives, _RefinesSkip, _TransitionTakenIn, _TransitionTakenOut, Trace, Trace, [], _MaxDepth, _MaxBreadth) :- !. | |
| 769 | ||
| 770 | %Skip/Normal Step | |
| 771 | refine_trace_step(CurId, Op, Pred, _RefineAlternatives, _RefinesSkip, _TransitionTakenInput, TransitionTakenOutput, TraceInput, TraceOutput, IdsList, _MaxDepth, MaxBreadth) :- | |
| 772 | apply_refinement_variants(CurId, Op, Pred, PossiblePaths, MaxBreadth), | |
| 773 | PossiblePaths \= [],!, | |
| 774 | find_new_ids(PossiblePaths, IdsList), | |
| 775 | pack_as_list(PossiblePaths, PossiblePathsPacked), | |
| 776 | maplist(append(TraceInput), PossiblePathsPacked, TraceOutput), | |
| 777 | create_map_of_maps(TraceOutput, TransitionTakenOutput). | |
| 778 | ||
| 779 | %Skip/Stuttering Step | |
| 780 | refine_trace_step(CurID, Op, _Pred, RefineAlternatives, RefinesSkip, TransitionTakenInput, TransitionTakenOutput, TraceInput, TraceOutput, IdsList, MaxDepth, _MaxBreadth) :- | |
| 781 | \+ length(TransitionTakenInput, MaxDepth),!, %%Current max depth | |
| 782 | compute_operations_for_state(CurID, SuitableOperations), | |
| 783 | clean_targets(SuitableOperations, RefinesSkip, PossibleSkipTargetsSkip), | |
| 784 | clean_targets(SuitableOperations, RefineAlternatives, RefiningOps), | |
| 785 | clean_targets(RefiningOps, Op, PossibleTargetsRefines), | |
| 786 | append(PossibleTargetsRefines, PossibleSkipTargetsSkip, PossibleTargets), | |
| 787 | (PossibleTargets = [] -> | |
| 788 | TraceOutput = [], | |
| 789 | TransitionTakenOutput = TransitionTakenInput, | |
| 790 | IdsList = []; | |
| 791 | find_new_ids(PossibleTargets, IdsList), | |
| 792 | pack_as_list(PossibleTargets, CleansedPacked), | |
| 793 | maplist(append(TransitionTakenInput), CleansedPacked, TransitionTakenOutput), | |
| 794 | maplist(append(TraceInput), CleansedPacked, TraceOutput) | |
| 795 | ). | |
| 796 | ||
| 797 | ||
| 798 | ||
| 799 | ||
| 800 | clean_targets([], _RefinesOrSkip, []). | |
| 801 | ||
| 802 | clean_targets([op(Trans, Name, From, Id)|Rest], RefinesOrSkip, [op(Trans, Name, From, Id)|RestOPs]) :- | |
| 803 | memberchk(Name, RefinesOrSkip), | |
| 804 | clean_targets(Rest, RefinesOrSkip, RestOPs). | |
| 805 | ||
| 806 | clean_targets([op(_Trans, Name, _From, _Id)|Rest], RefinesOrSkip, RestOPs) :- | |
| 807 | \+ memberchk(Name, RefinesOrSkip), | |
| 808 | clean_targets(Rest, RefinesOrSkip, RestOPs). | |
| 809 | ||
| 810 | create_map_of_maps([],[]). | |
| 811 | ||
| 812 | create_map_of_maps([_|Rest], [[]|SRest]) :- | |
| 813 | create_map_of_maps(Rest, SRest). | |
| 814 | ||
| 815 | ||
| 816 | %% StartingPoint, Operations, Predicates, 1:n refinemets, Refinements that are actually use refines, Skip events, Results, Maximum search depth | |
| 817 | prob2_refine_trace(CurId, OPs, Preds, RefineAlternatives, RefinesSkip, Result, MaxDepth, MaxBreadth) :- | |
| 818 | refine_trace_start_kick_off(CurId,OPs,Preds, RefineAlternatives, RefinesSkip, ShortestResults, MaxDepth, MaxBreadth), | |
| 819 | (ShortestResults = [] -> Result = ShortestResults; | |
| 820 | select_solution(ShortestResults, Result) | |
| 821 | ). | |
| 822 | ||
| 823 | ||
| 824 | ||
| 825 | ||
| 826 | select_solution([trace(_, T, _) | _], T). | |
| 827 | ||
| 828 | select_solution([_ | Rest], Solution) :- | |
| 829 | select_solution(Rest, Solution). | |
| 830 | ||
| 831 | ||
| 832 | apply_refinement_variants( _CurId, [], _Pred, [], _MaxBreadth). | |
| 833 | apply_refinement_variants( CurID, [Name | Names], Pred, Result, MaxBreadth) :- | |
| 834 | prob2_execute_custom_operations(CurID, Name, Pred, MaxBreadth, AcResult, _SingleErr), %% We want to catch all possiblities, we do not care for an failing option | |
| 835 | apply_refinement_variants(CurID, Names, Pred, OtherResults, MaxBreadth), | |
| 836 | append(AcResult, OtherResults, Result). | |
| 837 | ||
| 838 | ||
| 839 | pack_as_list([], []) . | |
| 840 | pack_as_list([First | Rest], [[First]| Rest2]) :- | |
| 841 | pack_as_list(Rest, Rest2). | |
| 842 | ||
| 843 | longest_match([], Current, Current):-!. | |
| 844 | longest_match([First|Rest], Current, Result) :- | |
| 845 | length(Current, CL), | |
| 846 | length(First, FL), | |
| 847 | (CL >= FL -> longest_match(Rest, Current, Result) ; longest_match(Rest, First, Result)). | |
| 848 | ||
| 849 | find_new_ids([], []). | |
| 850 | find_new_ids([First|Rest], [Id | RestIds]):- | |
| 851 | First = op(_Trans,_Name,_From,Id), | |
| 852 | find_new_ids(Rest, RestIds). | |
| 853 | ||
| 854 | ||
| 855 | /** | |
| 856 | ||
| 857 | Calculates a trace given a list of operation names and a list of guards. | |
| 858 | In case of errors, a partial trace is generated that jumps over the errornous operation / event. | |
| 859 | In addition, a list of integers should be given as argument that make possible to execute some | |
| 860 | operations in the oprations list multiple times or as long as they are disabled (in this case one should give -1). | |
| 861 | E.g. by calling prob2_construct_trace(0,[e1,e2,e3],[TRUE,TRUE,TRUE],[2,1,-1],OpsOut,ErrOut) the predicate calculates | |
| 862 | a trace starting at the state with the ID 0 where e1 is executed sequentially 2 times, after that e2 once, | |
| 863 | and finally e3 until it becomes disabled. | |
| 864 | ||
| 865 | #### called by: | |
| 866 | * ProB 2.0: ConstructTraceCommand | |
| 867 | */ | |
| 868 | ||
| 869 | prob2_construct_trace(CurId,Names,Preds,Nrs,OpsOut,ErrOut) :- | |
| 870 | construct_trace(CurId,Names,Preds,Nrs,[],OpsOut,[],ErrOut). | |
| 871 | ||
| 872 | construct_trace(_CurId,[],[],[],OpsOut,OpsOut,ErrOut,ErrOut). | |
| 873 | construct_trace(CurId,[Name|Names],[Pred|Preds],[NrName|NrNames],CurOpsOut,OpsOut,CurErrOut,ErrOut) :- | |
| 874 | execute_nr_of_custom_operations(CurId,Name,Pred,NrName,NewId,ListOfOps,ListOfErrs), | |
| 875 | append(CurOpsOut,ListOfOps,NewOpsOut), | |
| 876 | append(CurErrOut,ListOfErrs,NewErrOut), | |
| 877 | construct_trace(NewId,Names,Preds,NrNames,NewOpsOut,OpsOut,NewErrOut,ErrOut). | |
| 878 | ||
| 879 | execute_nr_of_custom_operations(CurId,_Name,_Pred,0,CurId,[],[]). | |
| 880 | execute_nr_of_custom_operations(CurId,Name,Pred,Nr,NewId,ListOfOps,ListOfErrs) :- | |
| 881 | ( Nr = -1 -> | |
| 882 | execute_until_disabled(CurId,Name,Pred,NewId,ListOfOps,ListOfErrs) | |
| 883 | ; % Nr is greater than 0 | |
| 884 | prob2_execute_custom_operations(CurId,Name,Pred,1,ListContainingSingleOp,SingleErr), | |
| 885 | ( ListContainingSingleOp = [] -> | |
| 886 | NextId=CurId | |
| 887 | ; ListContainingSingleOp = [op(_Trans,_Name,_From,To)], | |
| 888 | NextId = To | |
| 889 | ), | |
| 890 | append(ListContainingSingleOp,Ops,ListOfOps), | |
| 891 | append(SingleErr,Errs,ListOfErrs), | |
| 892 | NewNr is Nr - 1, | |
| 893 | execute_nr_of_custom_operations(NextId,Name,Pred,NewNr,NewId,Ops,Errs) | |
| 894 | ). | |
| 895 | ||
| 896 | ||
| 897 | execute_until_disabled(CurId,OpName,Pred,NewId,ListOfOps,ListOfErrs) :- | |
| 898 | execute_until_disabled(CurId,OpName,Pred,NewId,[],ListOfOps,ListOfErrs). | |
| 899 | ||
| 900 | execute_until_disabled(CurId,OpName,Pred,NewId,CurListOfOps,ListOfOps,ListOfErrs) :- | |
| 901 | prob2_execute_custom_operations(CurId,OpName,Pred,1,ListContainingSingleOp,SingleErr), | |
| 902 | ( ListContainingSingleOp = [] -> % reached a state where OpName is not executed | |
| 903 | NewId=CurId, | |
| 904 | ListOfOps=CurListOfOps, | |
| 905 | ajoin(['Could not execute Operation ', OpName, ' with additional predicate'], Msg), | |
| 906 | (member(Msg,SingleErr) -> % Error message generated because OpName is disabled at some state | |
| 907 | ListOfErrs = [] | |
| 908 | ; % unexpected error occurred, need to be reported | |
| 909 | ListOfErrs = SingleErr | |
| 910 | ) | |
| 911 | ; ListContainingSingleOp = [op(Trans,Name,From,To)], | |
| 912 | ( member(op(_T,_N,To,_To),CurListOfOps) -> % in case of a loop we terminate, otherwise we will go forever | |
| 913 | ListOfOps = CurListOfOps, | |
| 914 | NewId=From | |
| 915 | ; | |
| 916 | NextId = To, | |
| 917 | append(CurListOfOps,[op(Trans,Name,From,To)],NewCurListOfOps), | |
| 918 | execute_until_disabled(NextId,OpName,Pred,NewId,NewCurListOfOps,ListOfOps,ListOfErrs) | |
| 919 | ) | |
| 920 | ). | |
| 921 | ||
| 922 | % TO DO: check if we need to recompute the operation effect: if the ParsedPredicate is TRUE | |
| 923 | % (TRUE = equal(none,integer(none,1),integer(none,1)) ) & MaxNrOfSolutions <= | |
| 924 | % what has already been used previously, we can simply reuse transition from the state space | |
| 925 | ||
| 926 | prob2_execute_custom_operation(CurID,OpName,Transition,Max) :- | |
| 927 | set_context_state(CurID,prob2_execute_custom_operation), % errors will be added to state space as state errors | |
| 928 | call_cleanup(prob2_exec_custom_aux(CurID,OpName,Transition,Max), | |
| 929 | clear_context_state). | |
| 930 | prob2_exec_custom_aux(CurID,OpName,Transition,Max) :- | |
| 931 | visited_expression(CurID,InState), | |
| 932 | %add_prob_deferred_set_elements_to_store(InState1, InState, visible), % does not work for root, const_and_vars | |
| 933 | specfile:compute_operation_effect_max(InState,OpName,Operation,NewState,_TransPathInfo,Max), | |
| 934 | % logger:writeln_log(sol(OpName,NewState)), %% | |
| 935 | tcltk_interface:add_trans_id(CurID,Operation,NewState,NewID,TransId), | |
| 936 | % logger:writeln_log(ids(OpName,Operation,NewID,TransId)), %% | |
| 937 | Transition = op(TransId,OpName,CurID,NewID). | |
| 938 | ||
| 939 | :- use_module(succeed_max,[succeed_max_call_id/3]). | |
| 940 | :- use_module(b_state_model_check,[execute_operation_by_predicate_in_state/5]). | |
| 941 | :- use_module(b_global_sets,[inline_prob_deferred_set_elements_into_bexpr/2]). | |
| 942 | :- use_module(bmachine,[assert_temp_typed_predicate/1,reset_temp_predicate/0]). | |
| 943 | prob2_execute_custom_operation_with_predicate(CurID,OpName,Predicate,Transition,Max) :- | |
| 944 | set_context_state(CurID,prob2_execute_custom_operation_with_predicate), | |
| 945 | call_cleanup(prob2_exec_custom_pred_aux(CurID,OpName,Predicate,Transition,Max), | |
| 946 | clear_context_state). | |
| 947 | prob2_exec_custom_pred_aux(CurID,OpName,Predicate,Transition,Max) :- | |
| 948 | catch( | |
| 949 | prob2_execute_custom_operation_with_predicate_aux(CurID,OpName,Predicate,Transition,Max), | |
| 950 | enumeration_warning(_,_,_,_,_), | |
| 951 | (add_warning(prob2_execute_custom_operation_with_predicate,'Enumeration warning when executing operation with predicate: ',OpName), | |
| 952 | fail)). | |
| 953 | prob2_execute_custom_operation_with_predicate_aux(CurID,OpName,Predicate,Transition,Max) :- | |
| 954 | b_top_level_operation(OpName), | |
| 955 | !, | |
| 956 | visited_expression(CurID,InState), | |
| 957 | succeed_max_call_id(prob2_execute_custom_operation, | |
| 958 | execute_operation_by_predicate_in_state(InState,OpName,Predicate,Operation,NewState),Max), | |
| 959 | tcltk_interface:add_trans_id(CurID,Operation,NewState,NewID,TransId), | |
| 960 | Transition = op(TransId,OpName,CurID,NewID). | |
| 961 | prob2_execute_custom_operation_with_predicate_aux(CurID,OpName,Predicate,Transition,MaxNrOfSolutions) :- | |
| 962 | % temporary fix: old style execution for INIT, setup_constants; INIT does not work yet for Event-B ! | |
| 963 | inline_prob_deferred_set_elements_into_bexpr(Predicate,CP), | |
| 964 | %translate:print_bexpr(CP),nl, | |
| 965 | assert_temp_typed_predicate(CP), | |
| 966 | call_cleanup(prob2_execute_custom_operation(CurID,OpName,Transition,MaxNrOfSolutions), | |
| 967 | reset_temp_predicate). | |
| 968 | ||
| 969 | /** | |
| 970 | get_op_from_id(+Id,+Options,-Params,-RetVals) | |
| 971 | ||
| 972 | Extracts information about the parameters and return values for the | |
| 973 | specified transition. | |
| 974 | ||
| 975 | #### called by: | |
| 976 | * ProB 2.0: GetOpFromId | |
| 977 | */ | |
| 978 | get_op_from_id(Id,Options,Params,RetVals) :- | |
| 979 | (is_list(Options) -> | |
| 980 | % The eval-related options aren't actually used by this predicate. | |
| 981 | parse_eval_opts(_EvalOpts, Options, Options1), | |
| 982 | parse_pp_opts(PPOpts, Options1, []) | |
| 983 | ; | |
| 984 | PPOpts = pp_opts(Options,ascii,_) | |
| 985 | ), | |
| 986 | transition(_Src,Op,Id,_Dest), | |
| 987 | create_op_tuple(Op,PPOpts,Params,RetVals). | |
| 988 | ||
| 989 | /** | |
| 990 | create_op_tuple(+OpTerm, +PPOpts, -Params, -RetVals) | |
| 991 | ||
| 992 | Creates an operation tuple from transition id, source id, an op term, and a destination id. | |
| 993 | If creation is unsuccessful, an error is added and the predicate fails. | |
| 994 | See comment for extract_op_tuple for a description of OpTuple | |
| 995 | */ | |
| 996 | create_op_tuple(OpTerm, PPOpts, Params, RetVals) :- | |
| 997 | (extract_op_tuple(OpTerm, PPOpts, Params, RetVals) -> true; | |
| 998 | add_error_and_fail(prob2_interface, 'Could not create OpTuple ', extract_op_tuple(OpTerm, Params, RetVals))). | |
| 999 | ||
| 1000 | /** | |
| 1001 | extract_op_tuple(+OpTerm, +PPOpts, -Params, -RetVals) | |
| 1002 | ||
| 1003 | Extracts the parameters and return values of the operations | |
| 1004 | */ | |
| 1005 | extract_op_tuple(OpTerm, PPOpts, Params, RetVals) :- | |
| 1006 | (animation_mode(cspm) -> | |
| 1007 | extract_csp_op(OpTerm, Params, RetVals) | |
| 1008 | ; extract_b_op(OpTerm, PPOpts, Params, RetVals) | |
| 1009 | ). | |
| 1010 | ||
| 1011 | /** | |
| 1012 | extract_csp_op(+OpTerm, -Params, -RetVals) | |
| 1013 | ||
| 1014 | Extracts information for a CSP operation. | |
| 1015 | */ | |
| 1016 | extract_csp_op(OpTerm, Params, []) :- | |
| 1017 | %OpTuple = op(TransId, Src, Dest, Name, params(Source, Pretty), return([],[]), TargetState), /* TODO: CSP operations do not have return types, is this correct??? */ | |
| 1018 | %extract_csp_name_and_args(OpTerm, _Name, _Source), | |
| 1019 | translate_event(OpTerm, PPEvent), | |
| 1020 | split_atom(PPEvent,['.','!'],[_Op|Params]). | |
| 1021 | ||
| 1022 | %! extract_csp_name_and_args(+OpTerm, -Name, -Args) | |
| 1023 | extract_csp_name_and_args(io(Args,ChName,_SPAN),ChName,Args). | |
| 1024 | extract_csp_name_and_args(start_cspm(Name), Name, []). | |
| 1025 | extract_csp_name_and_args(start_cspm_MAIN,'start_cspm_MAIN',[]). | |
| 1026 | extract_csp_name_and_args(tick(_),tick,[]). | |
| 1027 | extract_csp_name_and_args(tau(_),tau,[]). | |
| 1028 | extract_csp_name_and_args(_OP,'?',[]). | |
| 1029 | ||
| 1030 | /** | |
| 1031 | extract_b_op(+OpTerm, +PPOpts, -Params, -RetVals) | |
| 1032 | ||
| 1033 | Extracts information for a B operation. | |
| 1034 | */ | |
| 1035 | extract_b_op(OpTerm, PPOpts, Params, RetVals) :- | |
| 1036 | extract_b_op_infos(OpTerm, _Name, PSource, RSource), | |
| 1037 | maplist(pretty_print_bvalue(PPOpts), PSource, Params), | |
| 1038 | maplist(pretty_print_bvalue(PPOpts), RSource, RetVals). | |
| 1039 | ||
| 1040 | %! extract_b_op_infos(+Term, -Name, -Arguments, -RetVals) | |
| 1041 | extract_b_op_infos(Term, Name, Arguments, RetVals) :- | |
| 1042 | (Term = '-->'(OpTerm,RetVals) -> true; | |
| 1043 | OpTerm = Term, RetVals = []), | |
| 1044 | OpTerm =.. [Name|Arguments]. | |
| 1045 | ||
| 1046 | extract_op_name(OpTerm,Name) :- | |
| 1047 | (animation_mode(cspm) -> | |
| 1048 | extract_csp_name_and_args(OpTerm, Name, _Args) | |
| 1049 | ; extract_b_op_infos(OpTerm, Name, _Params, _RetVals) | |
| 1050 | ). | |
| 1051 | ||
| 1052 | set_default_eval_opts(eval_opts(_StateId, ProvideLets, EvalExpand, TimeoutMs)) :- | |
| 1053 | % Fill in any unbound arguments with default values. | |
| 1054 | % StateId is currently required and has no automatic default. | |
| 1055 | (var(ProvideLets) -> ProvideLets = false ; true), | |
| 1056 | (var(EvalExpand) -> EvalExpand = force ; true), % for compatibility - this isn't a good default... | |
| 1057 | (var(TimeoutMs) -> TimeoutMs = 30000 ; true). | |
| 1058 | default_eval_opts(EvalOpts) :- | |
| 1059 | EvalOpts = eval_opts(_,_,_,_), | |
| 1060 | set_default_eval_opts(EvalOpts). | |
| 1061 | ||
| 1062 | /** | |
| 1063 | parse_eval_opts(-EvalOpts, +Options, -Options0) | |
| 1064 | ||
| 1065 | Supported options: | |
| 1066 | * state(StateId): state in which to evaluate the formulas | |
| 1067 | * provide_stored_let_values: make stored let values visible to the formulas (see eval_let_store module) | |
| 1068 | * eval_expand(EvalExpand): any of the expand modes supported by store:normalise_value_for_var/4 | |
| 1069 | * timeout(TimeoutMs): per-formula evaluation timeout in milliseconds | |
| 1070 | */ | |
| 1071 | parse_eval_opts(eval_opts(StateId,ProvideLets,EvalExpand,TimeoutMs), Options, Options4) :- | |
| 1072 | (selectchk(state(StateId), Options, Options1) -> true ; Options1 = Options), | |
| 1073 | (selectchk(provide_stored_let_values, Options1, Options2) -> ProvideLets = true ; Options2 = Options1), | |
| 1074 | (selectchk(eval_expand(EvalExpand), Options2, Options3) -> true ; Options3 = Options2), | |
| 1075 | (selectchk(timeout(TimeoutMs), Options3, Options4) -> true ; Options4 = Options3). | |
| 1076 | ||
| 1077 | set_default_pp_opts(pp_opts(Truncate, TransMode, Language)) :- | |
| 1078 | % Fill in any unbound arguments with default values. | |
| 1079 | (var(Truncate) -> Truncate = truncate ; true), | |
| 1080 | (var(TransMode) -> TransMode = unicode ; true), | |
| 1081 | (var(Language) -> get_language_mode(Language) ; true). | |
| 1082 | ||
| 1083 | /** | |
| 1084 | parse_pp_opts(-PPOpts, +Options, -Options0) | |
| 1085 | ||
| 1086 | Supported options: | |
| 1087 | * truncate(Truncate): either truncate or expand - controls whether result strings are truncated | |
| 1088 | * translation_mode(TransMode): any of the modes supported by set_translation_mode/1 | |
| 1089 | * language(Language): any of the languages supported by set_language_mode/1 | |
| 1090 | */ | |
| 1091 | parse_pp_opts(pp_opts(Truncate,TransMode,Language),Options,Options3) :- | |
| 1092 | (selectchk(truncate(Truncate), Options, Options1) -> true ; Options1 = Options), | |
| 1093 | % TODO Allow requesting multiple translation modes at once (would be useful for Jupyter) | |
| 1094 | (selectchk(translation_mode(TransMode), Options1, Options2) -> true ; Options2 = Options1), | |
| 1095 | (selectchk(language(Language), Options2, Options3) -> true ; Options3 = Options2). | |
| 1096 | ||
| 1097 | limit_for_pretty_print(truncate,600). | |
| 1098 | limit_for_pretty_print(expand,-1). | |
| 1099 | ||
| 1100 | pretty_print_bvalue(pp_opts(Truncate,TransMode,Lang),Formula,Result) :- | |
| 1101 | set_default_pp_opts(pp_opts(Truncate,TransMode,Lang)), | |
| 1102 | limit_for_pretty_print(Truncate, Limit), | |
| 1103 | with_translation_mode(TransMode, | |
| 1104 | with_language_mode(Lang, | |
| 1105 | translate_bvalue_with_limit(Formula,Limit,Result))). | |
| 1106 | ||
| 1107 | /* ------------------------- */ | |
| 1108 | /* Boolean Properties */ | |
| 1109 | /* ------------------------- */ | |
| 1110 | ||
| 1111 | :- use_module(state_space,[visited_state_corresponds_to_setup_constants_b_machine/1]). | |
| 1112 | is_constants_set_up_state(ID) :- | |
| 1113 | b_or_z_mode | |
| 1114 | -> visited_state_corresponds_to_setup_constants_b_machine(ID) | |
| 1115 | ; true. | |
| 1116 | ||
| 1117 | is_initialised_state(ID) :- b_or_z_mode,!, | |
| 1118 | is_initialised_b_state(ID). | |
| 1119 | is_initialised_state(ID) :- | |
| 1120 | visited_expression_id(ID), ID \= root. | |
| 1121 | ||
| 1122 | :- use_module(state_space,[visited_state_corresponds_to_initialised_b_machine/1]). | |
| 1123 | is_initialised_b_state(ID) :- | |
| 1124 | visited_state_corresponds_to_initialised_b_machine(ID). | |
| 1125 | ||
| 1126 | :- use_module(xtl_interface,[xtl_invariant_violated/1]). | |
| 1127 | invariantKO(StateID) :- xtl_mode,!, | |
| 1128 | visited_expression(StateID,State), | |
| 1129 | xtl_invariant_violated(State). | |
| 1130 | invariantKO(StateID) :- is_initialised_state(StateID), | |
| 1131 | get_state(StateID,State), | |
| 1132 | tcltk_interface:check_invariantKO(StateID,State), | |
| 1133 | state_space:invariant_violated(StateID). % test redundant for B | |
| 1134 | ||
| 1135 | /** | |
| 1136 | Takes a state id and finds all of the operations for which a timeout occurred | |
| 1137 | ||
| 1138 | #### called by: | |
| 1139 | * ProB Plugin: GetTimeoutedOperationsCommand | |
| 1140 | * ProB 2.0: GetOperationsWithTimeout | |
| 1141 | */ | |
| 1142 | op_timeout_occurred(StateID,OpNameList) :- | |
| 1143 | findall(OpName,time_out_for_node(StateID,OpName,_Type),OpNameList). | |
| 1144 | ||
| 1145 | inv_timeout_occurred(StateID) :- time_out_for_invariant(StateID). | |
| 1146 | timeout_occurred(StateID) :- time_out_for_node(StateID). | |
| 1147 | max_operations_reached(StateID) :- max_reached_for_node(StateID). | |
| 1148 | ||
| 1149 | /** | |
| 1150 | state_property(+Property,+StateId,-Status) | |
| 1151 | ||
| 1152 | Finds the status for a given property | |
| 1153 | Properties can be: invariantKO, timeout_occurred, max_operations_reached, initialised | |
| 1154 | Statuses are expected to be boolean values: either true or false | |
| 1155 | ||
| 1156 | #### called by: | |
| 1157 | * ProB Plugin: CheckBooleanPropertyCommand | |
| 1158 | * ProB 2.0: CheckBooleanPropertyCommand | |
| 1159 | */ | |
| 1160 | state_property(Property,StateId,Status) :- | |
| 1161 | (state_property2(Property,StateId) -> Status = true ; Status = false). | |
| 1162 | state_property2(invariantKO,StateId) :- invariantKO(StateId). | |
| 1163 | state_property2(timeout_occurred,StateId) :- inv_timeout_occurred(StateId) ; timeout_occurred(StateId). | |
| 1164 | state_property2(max_operations_reached,StateId) :- max_operations_reached(StateId). | |
| 1165 | state_property2(valid_state,StateId) :- visited_expression_id(StateId). | |
| 1166 | state_property2(constants_set_up,StateId) :- is_constants_set_up_state(StateId). | |
| 1167 | state_property2(initialised,StateId) :- | |
| 1168 | (specfile:csp_mode -> | |
| 1169 | true % in CSP the content of the state is irrelevant for the semantic of the state space | |
| 1170 | ; is_initialised_state(StateId) | |
| 1171 | ). | |
| 1172 | ||
| 1173 | ||
| 1174 | /** | |
| 1175 | prob2_get_state_errors(+StateId,-Errors) | |
| 1176 | ||
| 1177 | Takes a id for a given state in the state space and produces a list of all | |
| 1178 | state based errors. | |
| 1179 | ||
| 1180 | #### called by: | |
| 1181 | * ProB 2.0: GetStateBasedErrorsCommand | |
| 1182 | */ | |
| 1183 | prob2_get_state_errors(StateId,Errors) :- | |
| 1184 | findall(E, (state_error(StateId,_,Error), convert_error(Error,E)), Errors). | |
| 1185 | ||
| 1186 | :- use_module(error_manager,[extract_span_description/2]). | |
| 1187 | convert_error(invariant_violated,_) :- !, fail. | |
| 1188 | convert_error(eventerror(Event,EError,Trace),error([event(Event),description(Short),long_description(Long)])) :- | |
| 1189 | !, | |
| 1190 | translate_event_error(EError,Short), | |
| 1191 | explain_event_trace(Trace,LongStr,_Span), | |
| 1192 | safe_atom_codes(Long,LongStr). | |
| 1193 | convert_error(Error,error([description(Short),long_description(Long)|Tail])) :- | |
| 1194 | translate_state_error(Error,Short), | |
| 1195 | explain_state_error(Error,Span,LongStr), | |
| 1196 | safe_atom_codes(Long,LongStr), | |
| 1197 | % TODO Also return Span as structured error locations, not just a text description | |
| 1198 | (extract_span_description(Span,SDescr) -> | |
| 1199 | Tail = [span_description(SDescr)] | |
| 1200 | ; | |
| 1201 | Tail = [] | |
| 1202 | ). | |
| 1203 | ||
| 1204 | /* ------------------------- */ | |
| 1205 | /* Evaluate Formulas */ | |
| 1206 | /* ------------------------- */ | |
| 1207 | ||
| 1208 | % term in string (see String argument) should be terminated by full-stop!!! | |
| 1209 | evaluate_csp_expression_string(PlClause,R) :- | |
| 1210 | read_from_codes(PlClause,PlTerm), | |
| 1211 | evaluate_csp_expression_aux(PlTerm,R). | |
| 1212 | ||
| 1213 | :- use_module(probcspsrc(haskell_csp), [evaluate_parsed_csp_expression_with_timing/2]). | |
| 1214 | evaluate_csp_expression_aux(PlTerm,R) :- | |
| 1215 | evaluate_parsed_csp_expression_with_timing(PlTerm,Res), | |
| 1216 | translate:translate_cspm_expression(Res, R). | |
| 1217 | evaluate_csp_expression_aux(Other,_R) :- | |
| 1218 | add_error_and_fail(prob2_interface, 'Unexpected CSP Expression: ', Other). | |
| 1219 | ||
| 1220 | :- assert_must_succeed((X=identifier(none,x), | |
| 1221 | prob2_evaluate_formulas( | |
| 1222 | [bexpr(comprehension_set(none,[X],greater(none,mult_or_cart(none,X,X),integer(none,2))))], | |
| 1223 | [state(root)], | |
| 1224 | Res | |
| 1225 | ), | |
| 1226 | Res = [result(Str,[],_)], | |
| 1227 | (Str == '/*@symbolic*/ {x|x * x > 2}' ; Str == '{x|x * x > 2}'))). | |
| 1228 | ||
| 1229 | /** | |
| 1230 | prob2_evaluate_formulas(+Formulas, +Options, -Results) | |
| 1231 | ||
| 1232 | Evaluate a list of formulas. | |
| 1233 | This is more efficient than evaluating each formula individually, | |
| 1234 | because some calculations (e. g. expanding the current state) don't have to be repeated for each formula. | |
| 1235 | ||
| 1236 | Supported formula types: | |
| 1237 | * bpred(Raw) | |
| 1238 | * bexpr(Raw) | |
| 1239 | * csp(TermCodes) | |
| 1240 | ||
| 1241 | Supported options: | |
| 1242 | * all options supported by parse_eval_opts/3 | |
| 1243 | * all options supported by parse_pp_opts/3 | |
| 1244 | ||
| 1245 | Possible results: | |
| 1246 | * result(Value,Solutions,Errors): evaluation succeeded | |
| 1247 | * Value: String rep of the value calculated by ProB | |
| 1248 | * Solutions: List of solutions as a triple: bind(Name,PPSol) | |
| 1249 | * Name: Free variable from formula | |
| 1250 | * PPSol: String representation of the solution bound to the name | |
| 1251 | * Errors: List of error/3 terms for non-fatal errors (warnings or messages) that occurred during evaluation | |
| 1252 | * errors(Value,Errors): Typechecking or evaluation failed | |
| 1253 | * Value: Short description of error type (e. g. 'NOT-WELL-DEFINED', 'UNKNOWN') | |
| 1254 | * Errors: List of error/3 terms for all errors that occurred | |
| 1255 | * enum_warning: An enumeration warning was thrown during evaluation | |
| 1256 | */ | |
| 1257 | prob2_evaluate_formulas(Formulas, Options, Results) :- | |
| 1258 | parse_eval_opts(EvalOpts, Options, Options1), | |
| 1259 | set_default_eval_opts(EvalOpts), | |
| 1260 | EvalOpts = eval_opts(StateId,ProvideLets,_,_), | |
| 1261 | parse_pp_opts(PPOpts,Options1,[]), | |
| 1262 | % useful for certain external functions in LibraryMeta.def, e.g., ENABLED, EVAL_OVER_HISTORY, CHANGED, ...: | |
| 1263 | set_current_state_for_external_fun(StateId), | |
| 1264 | ? | call_cleanup( |
| 1265 | (get_bstate_with_deferred_sets(StateId,ProvideLets,State,StateKind,ConstID), | |
| 1266 | % _Machine is shared across all calls so that full_b_machine only needs to be computed once. | |
| 1267 | maplist(evaluate_formula_in_state(EvalOpts,PPOpts,StateKind,State,ConstID,_Machine),Formulas,Results) | |
| 1268 | ), | |
| 1269 | clear_state_for_external_fun). | |
| 1270 | ||
| 1271 | evaluate_formula_in_state(EvalOpts, PPOpts, StateKind, State, ConstID, Machine, Formula, Result) :- | |
| 1272 | ? | evaluate_formula_in_state_aux(Formula, EvalOpts, PPOpts, StateKind, State, ConstID, Machine, Result). |
| 1273 | ||
| 1274 | evaluate_formula_in_state_aux(csp(Raw), _EvalOpts, _PPOpts, _StateKind, _State, _ConstID, _Machine, R) :- !, | |
| 1275 | ( evaluate_csp_expression_string(Raw,Res) -> | |
| 1276 | R = result(Res,[],[]); | |
| 1277 | R = errors('UNKNOWN',[error('Unexpected CSP Expression',internal_error,[])])). | |
| 1278 | evaluate_formula_in_state_aux(registered(FormulaID), EvalOpts, PPOpts, StateKind, State, _ConstID, _Machine, R) :- | |
| 1279 | !, | |
| 1280 | (prob2_formula(FormulaID, Typed, Requirements) -> | |
| 1281 | evaluate_typechecked_b_formula_in_state(StateKind, Requirements, State, Typed, EvalOpts, PPOpts, R) | |
| 1282 | ; | |
| 1283 | R = errors('ERROR', [error('No formula registered with this UUID',internal_error,[])]) | |
| 1284 | ). | |
| 1285 | evaluate_formula_in_state_aux(Formula, EvalOpts, PPOpts, StateKind, State, _ConstID, Machine, R) :- | |
| 1286 | %logger:writeln_log_time(typechecking_raw(PredOrExpr)), | |
| 1287 | (formula_typecheck_for_eval(Formula,EvalOpts,Machine,Typed) -> | |
| 1288 | %logger:writeln_log_time(evaluate_typechecked_b_formula_in_state(StateKind)), | |
| 1289 | %print('EVAL:'),nl,translate:print_bexpr(Typed),nl, | |
| 1290 | ? | prob2_interface:evaluate_typechecked_b_formula_in_state(StateKind,formula(Typed),State,Typed,EvalOpts,PPOpts,R) |
| 1291 | ; | |
| 1292 | get_all_errors_with_span_info_and_reset(Errors), | |
| 1293 | R = errors('ERROR',Errors) | |
| 1294 | ). | |
| 1295 | ||
| 1296 | :- use_module(eval_let_store, [extend_state_with_stored_lets/2]). | |
| 1297 | get_bstate_with_deferred_sets(StateId,ProvideLets,State,Kind,ConstID) :- | |
| 1298 | get_state(StateId, State1,Kind,ConstID), % TO DO: we could try and get only those identifiers that are really used | |
| 1299 | add_prob_deferred_set_elements_to_store(State1, State2, visible), | |
| 1300 | (ProvideLets = true -> extend_state_with_stored_lets(State2, State) ; State = State2). | |
| 1301 | ||
| 1302 | /** | |
| 1303 | prob2_get_formula_type(+Formula,-PPType,-Errors) | |
| 1304 | ||
| 1305 | Type checks the given untyped formula to determine its type and any type errors. | |
| 1306 | ||
| 1307 | #### Params: | |
| 1308 | * Formula - bexpr(Raw) or bpred(Raw), where Raw is the Prolog representation of non-typechecked expression or predicate | |
| 1309 | * PPType - pretty-printed type of formula | |
| 1310 | * Errors - any errors that have occured during typechecking | |
| 1311 | ||
| 1312 | #### called by: | |
| 1313 | ProB 2.0: FormulaTypecheckCommand | |
| 1314 | */ | |
| 1315 | prob2_get_formula_type(Formula,PPType,Errors) :- | |
| 1316 | default_eval_opts(EvalOpts), | |
| 1317 | formula_typecheck2_for_eval(Formula,EvalOpts,_,TypedFormula,PErrors), | |
| 1318 | add_all_perrors(PErrors), | |
| 1319 | get_texpr_type(TypedFormula,Type), | |
| 1320 | translate:pretty_type(Type,PPType), | |
| 1321 | get_all_errors_with_span_info_and_reset(Errors). | |
| 1322 | ||
| 1323 | formula_typecheck_for_eval(Formula,EvalOpts,M,TypedFormula) :- | |
| 1324 | formula_typecheck2_for_eval(Formula,EvalOpts,M,TypedFormula,PErrors), | |
| 1325 | add_all_perrors(PErrors), | |
| 1326 | no_real_perror_occurred(PErrors). | |
| 1327 | ||
| 1328 | % this predicate returns the internal Prolog type: | |
| 1329 | %! formula_typecheck2_for_eval(+PredOrExpr,+EvalOpts,?Machine,+RawFormula,-TypedFormula,-Type,-Errors) | |
| 1330 | formula_typecheck2_for_eval(bpred(Raw),EvalOpts,M,Typed,PErrors) :- | |
| 1331 | !, predicate_typecheck_for_eval(M,Raw,EvalOpts,Typed,PErrors). | |
| 1332 | formula_typecheck2_for_eval(bexpr(Raw),EvalOpts,M,Typed,PErrors) :- | |
| 1333 | !, expression_typecheck_for_eval(M,Raw,EvalOpts,Typed,PErrors). | |
| 1334 | formula_typecheck2_for_eval(Else,_,_M,_Typed,_PErrors) :- | |
| 1335 | add_error_and_fail(prob2_interface,'Unsupported formula term:', Else),fail. | |
| 1336 | ||
| 1337 | predicate_typecheck_for_eval(Raw,Typed) :- | |
| 1338 | predicate_typecheck_for_eval(_,Raw,Typed). | |
| 1339 | predicate_typecheck_for_eval(M,Raw,Typed) :- | |
| 1340 | set_default_eval_opts(EvalOpts), | |
| 1341 | predicate_typecheck_for_eval(M,Raw,EvalOpts,Typed,PErrors), | |
| 1342 | add_all_perrors(PErrors), | |
| 1343 | no_real_perror_occurred(PErrors). | |
| 1344 | predicate_typecheck_for_eval(M,Raw,EvalOpts,Typed,PErrors) :- | |
| 1345 | get_eval_scope_with_opts(EvalOpts,Scope), % TODO: pass options | |
| 1346 | bmachine:b_type_open_predicate_for_full_b_machine(M,open(exists),Raw,Scope,Typed,PErrors). | |
| 1347 | ||
| 1348 | :- use_module(bmachine,[b_is_variable/2, b_is_constant/2, b_type_expression_for_full_b_machine/6]). | |
| 1349 | expression_typecheck_for_eval(Raw,Typed) :- | |
| 1350 | expression_typecheck_for_eval(_,Raw,Typed). | |
| 1351 | expression_typecheck_for_eval(M,Raw,Typed) :- | |
| 1352 | set_default_eval_opts(EvalOpts), | |
| 1353 | expression_typecheck_for_eval(M,Raw,EvalOpts,Typed,PErrors), | |
| 1354 | add_all_perrors(PErrors), | |
| 1355 | no_real_perror_occurred(PErrors). | |
| 1356 | expression_typecheck_for_eval(_,identifier(Pos,ID),_,Typed,PErrors) :- | |
| 1357 | (b_is_variable(ID,Type) ; b_is_constant(ID,Type)), | |
| 1358 | !, % hack to avoid type-checking simple identifiers which just need to be looked up in state | |
| 1359 | PErrors=[], Typed = b(identifier(ID),Type,[nodeid(Pos)]). | |
| 1360 | expression_typecheck_for_eval(M,Raw,EvalOpts,Typed,PErrors) :- | |
| 1361 | get_eval_scope_with_opts(EvalOpts,Scope), % TODO: pass options | |
| 1362 | b_type_expression_for_full_b_machine(M,Raw,Scope,_Type,Typed,PErrors). | |
| 1363 | ||
| 1364 | :- use_module(eval_let_store,[get_stored_let_typing_scope/1, reset_let_values/0]). | |
| 1365 | ||
| 1366 | % a more conservative version, only add external libraries if requested | |
| 1367 | get_eval_scope_with_opts(eval_opts(_,ProvideLets,_,_),Scope) :- !, | |
| 1368 | (ProvideLets=true -> get_eval_scope_with_opts([provide_stored_let_values],Scope) | |
| 1369 | ; get_eval_scope_with_opts([],Scope)). | |
| 1370 | get_eval_scope_with_opts(Options,Scope) :- | |
| 1371 | (member(provide_stored_let_values,Options), | |
| 1372 | reset_let_values, % purge all invalid values | |
| 1373 | get_stored_let_typing_scope(Scope1) % make stored values available; TODO: they also need to be added to the state with extend_state_with_stored_lets | |
| 1374 | -> Scope = [Scope1|Scope2] | |
| 1375 | ; Scope=Scope2), | |
| 1376 | (member(all_available_libraries,Options) -> get_eval_scope(all,Scope2) ; get_eval_scope(safe,Scope2)). | |
| 1377 | ||
| 1378 | % get scope for typechecker: | |
| 1379 | get_eval_scope(Scope) :- get_eval_scope(all,Scope). | |
| 1380 | get_eval_scope(ExtKind,[prob_ids(visible),Scope, | |
| 1381 | external_library(Libs)]) :- | |
| 1382 | % external_library for VisB and Debugging; TODO: should we only make it available in some contexts | |
| 1383 | % Note: the external_library entries must come after Scope | |
| 1384 | get_main_eval_scope(Scope), | |
| 1385 | get_libraries(ExtKind,Libs). | |
| 1386 | get_main_eval_scope(assertions_scope_and_additional_defs) :- | |
| 1387 | get_preference(allow_operation_calls_in_expr,true),!. | |
| 1388 | get_main_eval_scope(variables_and_additional_defs). | |
| 1389 | ||
| 1390 | get_libraries(all,all_available_libraries). | |
| 1391 | get_libraries(_,safe_available_libraries). | |
| 1392 | ||
| 1393 | ||
| 1394 | % TODO Can the evaluation code be integrated with eval_strings again, and/or merged with bvisual2? | |
| 1395 | ||
| 1396 | :- use_module(tools_meta,[safe_time_out/3]). | |
| 1397 | % NOTE: This predicate always resets the error manager. | |
| 1398 | % Any errors, warnings, etc. that occurred will be returned inside Result, | |
| 1399 | % including any errors that occurred *before* this predicate is called! | |
| 1400 | evaluate_typechecked_b_formula_in_state(StateKind,Requirements,State,Typed,EvalOpts,PPOpts,Result) :- | |
| 1401 | (requirements_met(Requirements,StateKind) -> | |
| 1402 | ? | evaluate_typechecked_b_formula_in_state(State,Typed,EvalOpts,PPOpts,Result) |
| 1403 | ; | |
| 1404 | get_all_errors_with_span_info_and_reset(Errors), | |
| 1405 | Result = errors('NOT-INITIALISED',Errors) | |
| 1406 | ). | |
| 1407 | evaluate_typechecked_b_formula_in_state(State,Typed,eval_opts(_StateId,_ProvideLets,EvalExpand,TO),PPOpts,Result) :- | |
| 1408 | safe_time_out( | |
| 1409 | catch_enumeration_warning_exceptions( | |
| 1410 | evaluate_formula_eval(State,Typed,EvalExpand,Res,Solution), | |
| 1411 | Res = enum_warning), | |
| 1412 | TO,TimeOutRes), | |
| 1413 | (TimeOutRes=time_out -> Res=error(time_out) ; true), | |
| 1414 | (real_error_occurred -> RealError = real_error ; RealError = no_real_error), | |
| 1415 | get_all_errors_with_span_info_and_reset(Errors), | |
| 1416 | ? | extract_result(Res,Solution,PPOpts,Errors,RealError,Result). |
| 1417 | ||
| 1418 | extract_result(enum_warning,_,_,_,_,R) :- !, R=enum_warning. | |
| 1419 | extract_result(error(ErrDesc),_Sol,_PPOpts,Errors,_RealError,Result) :- !, | |
| 1420 | Result = errors(ErrDesc, Errors). | |
| 1421 | extract_result(value(Term),Solutions,PPOpts,Errors,RealError,Result) :- !, | |
| 1422 | pretty_print_bvalue(PPOpts,Term,R), | |
| 1423 | (RealError == no_real_error -> | |
| 1424 | ? | prettyprint_solutions(PPOpts,Solutions,PPSol), |
| 1425 | Result = result(R,PPSol,Errors) | |
| 1426 | ; | |
| 1427 | Result = errors(R,Errors) | |
| 1428 | ). | |
| 1429 | ||
| 1430 | %:- use_module(eval_strings,[eval_predicate/5]). % TODO: export and refactor | |
| 1431 | % TO DO: move this into another more general module: | |
| 1432 | evaluate_formula_eval(State,Typed,_EvalExpand,Res,LocalState) :- | |
| 1433 | get_texpr_type(Typed,pred), | |
| 1434 | !, | |
| 1435 | eval_predicate(State,Typed,Res,LocalState). | |
| 1436 | evaluate_formula_eval(State,Typed,EvalExpand,Res,[]) :- | |
| 1437 | evaluate_expression(State,Typed,EvalExpand,Res). | |
| 1438 | ||
| 1439 | :- use_module(clpfd_interface,[catch_clpfd_overflow_call2/2]). | |
| 1440 | :- use_module(error_manager,[enter_new_error_scope/2, exit_error_scope/3,clear_all_errors_in_error_scope/1, | |
| 1441 | event_occurred_in_error_scope/1, abort_error_occured_in_error_scope/0]). | |
| 1442 | :- use_module(store,[normalise_value_for_var/4]). | |
| 1443 | % a simplified/modified version of eval_strings:eval_expression | |
| 1444 | % evaluate an expression Typed in an expanded state EState giving string result Result and Prolog value NValue | |
| 1445 | evaluate_expression(EState,Typed,EvalExpand,Term) :- | |
| 1446 | enter_new_error_scope(ScopeID,evaluate_expression), | |
| 1447 | clear_all_errors_in_error_scope(ScopeID), | |
| 1448 | %replace_expression_by_kodkod_if_enabled(Typed,Typed2), | |
| 1449 | catch_clpfd_overflow_call2(b_interpreter:b_compute_expression_nowf(Typed,[],EState,Value,'ProB2',0),fail), % We could return CLPFD overflow error result | |
| 1450 | !, | |
| 1451 | %logger:writeln_log_time(normalise_value_for_var(evaluate_expression)), | |
| 1452 | normalise_value_for_var(evaluate_expression,EvalExpand,Value,NValue), | |
| 1453 | get_unknown_error_result(ErrRes), | |
| 1454 | exit_error_scope(ScopeID,ErrOcc,evaluate_expression), | |
| 1455 | % FIXME Is ErrOcc ever true here? | |
| 1456 | % For WD errors, b_compute_expression_nowf fails, so this code is never reached. | |
| 1457 | % Enumeration warnings are thrown as exceptions and so also bypass this code. | |
| 1458 | (ErrOcc=true | |
| 1459 | -> Term = error(ErrRes) | |
| 1460 | ; Term = value(NValue) | |
| 1461 | ). | |
| 1462 | evaluate_expression(_,_,_,error(ErrRes)) :- | |
| 1463 | get_unknown_error_result(ErrRes), | |
| 1464 | exit_error_scope(_ScopeID,_,evaluate_expression). | |
| 1465 | ||
| 1466 | % which result should be displayed in case of failure/errors: | |
| 1467 | get_unknown_error_result(ErrRes) :- | |
| 1468 | (abort_error_occured_in_error_scope -> ErrRes = 'NOT-WELL-DEFINED' ; ErrRes = 'UNKNOWN'). | |
| 1469 | ||
| 1470 | % a simplified/modified version of eval_strings:eval_predicate_aux | |
| 1471 | eval_predicate(State, ExTyped,Result,LocalState) :- | |
| 1472 | enter_new_error_scope(ScopeID,eval_predicate), clear_all_errors_in_error_scope(ScopeID), | |
| 1473 | (catch_clpfd_overflow_call2(prob2_interface:eval_predicate2(State, ExTyped,LocalState,Res), | |
| 1474 | fail) | |
| 1475 | -> true | |
| 1476 | ; event_occurred_in_error_scope(enumeration_warning(_,_,_,_,_Critical)) | |
| 1477 | -> Res=enum_warning | |
| 1478 | ; eval_predicate2_fail_result(ExTyped,Res) % either value(pred_true) or value(pred_false) | |
| 1479 | ), | |
| 1480 | get_unknown_error_result(ErrRes), | |
| 1481 | exit_error_scope(ScopeID,ErrOcc,eval_predicate), | |
| 1482 | (ErrOcc=true | |
| 1483 | -> Result = error(ErrRes) | |
| 1484 | ; Result = Res | |
| 1485 | ). | |
| 1486 | ||
| 1487 | :- use_module(probsrc(bsyntaxtree), [safe_create_texpr/4]). | |
| 1488 | :- use_module(eval_strings, []). | |
| 1489 | eval_predicate2(State, ExTyped,LocalState,value(pred_true)) :- | |
| 1490 | eval_strings:is_existential_quantifier(ExTyped,Parameters,Typed), % TO DO: move to module | |
| 1491 | !, | |
| 1492 | test_bool_exists(State, Parameters,Typed,LocalState). | |
| 1493 | eval_predicate2(State, ExTyped,LocalState,value(pred_false)) :- | |
| 1494 | is_universal_quantifier(ExTyped,Parameters,TypedLHS,TypedRHS), | |
| 1495 | !, | |
| 1496 | safe_create_texpr(negation(TypedRHS),pred,[try_smt],NegRHS), | |
| 1497 | conjunct_predicates([TypedLHS,NegRHS],Conjunction), % replace Kodkod? | |
| 1498 | test_bool_exists(State, Parameters,Conjunction,LocalState). | |
| 1499 | eval_predicate2(State, Typed,LocalState,value(pred_true)) :- LocalState=[], | |
| 1500 | b_test_boolean_expression_cs(Typed,LocalState,State,'ProB2-Java',0). | |
| 1501 | ||
| 1502 | % what should the result be if the above eval_predicate2 fails (without enumeration warning): | |
| 1503 | eval_predicate2_fail_result(ExTyped,Res) :- | |
| 1504 | is_universal_quantifier(ExTyped,_,_,_),!, Res=value(pred_true). | |
| 1505 | eval_predicate2_fail_result(_,value(pred_false)). | |
| 1506 | ||
| 1507 | ||
| 1508 | test_bool_exists(EState, Parameters,Typed,LocalState) :- | |
| 1509 | kernel_waitflags:init_wait_flags(WF,[test_bool_exists]), | |
| 1510 | b_interpreter:set_up_typed_localstate(Parameters,_FreshOutputVars,TypedVals,[],LocalState,positive), | |
| 1511 | b_enumerate:b_tighter_enumerate_values_in_ctxt(TypedVals,Typed,WF), | |
| 1512 | b_interpreter:b_test_boolean_expression(Typed,LocalState,EState,WF), | |
| 1513 | kernel_waitflags:ground_wait_flags(WF). | |
| 1514 | ||
| 1515 | is_universal_quantifier(b(forall(Parameters,LHS,RHS),pred,_),Parameters,LHS,RHS). | |
| 1516 | ||
| 1517 | :- dynamic prob2_formula/3. | |
| 1518 | ||
| 1519 | :- use_module(bmachine, [determine_type_of_formula/2]). | |
| 1520 | register_prob2_formula1(_, FormulaUUID, _) :- prob2_formula(FormulaUUID,_,_),!. | |
| 1521 | register_prob2_formula1(M, FormulaUUID, Formula) :- | |
| 1522 | default_eval_opts(EOpts), | |
| 1523 | formula_typecheck_for_eval(Formula,EOpts,M,Typed), | |
| 1524 | determine_type_of_formula(Typed,Requirements), | |
| 1525 | assertz(prob2_formula(FormulaUUID, Typed, Requirements)). | |
| 1526 | ||
| 1527 | %! register_prob2_formulas(+FormulaUUIDs, +Formulas) | |
| 1528 | register_prob2_formulas(FormulaUUIDs,Formulas) :- | |
| 1529 | % _Machine is shared across all calls so that full_b_machine only needs to be computed once. | |
| 1530 | maplist(register_prob2_formula1(_Machine),FormulaUUIDs,Formulas). | |
| 1531 | ||
| 1532 | ||
| 1533 | % TO DO: determine upon registering whether a formula reads nothing, just constants, or also variables | |
| 1534 | ||
| 1535 | % unregister a single or a list of formula ids: | |
| 1536 | unregister_prob2_formula(FormulaUUID) :- retractall(prob2_formula(FormulaUUID,_,_)). | |
| 1537 | unregister_prob2_formulas(Fs) :- maplist(unregister_prob2_formula,Fs). | |
| 1538 | ||
| 1539 | ||
| 1540 | % check whether we can evaluate the formula in the state: | |
| 1541 | requirements_met(requires_nothing,_). | |
| 1542 | requirements_met(requires_constants,constants_only_state). | |
| 1543 | requirements_met(requires_constants,full_initialised_state). | |
| 1544 | requirements_met(requires_variables,full_initialised_state). | |
| 1545 | requirements_met(formula(Typed),State) :- | |
| 1546 | (State=full_initialised_state -> true | |
| 1547 | ; determine_type_of_formula(Typed,Requirements), requirements_met(Requirements,State)). | |
| 1548 | ||
| 1549 | ||
| 1550 | ||
| 1551 | % API for showing Tk Animation Images in Java FX (or other): | |
| 1552 | :- use_module(extrasrc(graphical_state_viewer_images),[get_animation_images/1, | |
| 1553 | get_animation_image_grid/6, get_react_to_item_right_click_options/4, react_to_item_right_click/6]). | |
| 1554 | get_animation_image_list(ImageList) :- get_animation_images(ImageList). | |
| 1555 | % Format: [image_file(0,'images/empty_box_white.gif'),...,image_file(6,'images/F.gif')] | |
| 1556 | ||
| 1557 | get_animation_image_matrix_for_state(ID,Matrix,MinRow,MaxRow,MinCol,MaxCol) :- | |
| 1558 | (get_animation_image_grid(ID,M,M1,M2,M3,M4) | |
| 1559 | -> Matrix=M, MinRow=M1, MaxRow=M2, MinCol=M3, MaxCol=M4 | |
| 1560 | ; Matrix=[], MinRow = -1, MaxRow = 0, MinCol = -1, MaxCol = 0). | |
| 1561 | % Format: [entry(1,1,image(0)),... entry(2,3,text(some_atom)),...], entry(Row,Col,ImgOrText) | |
| 1562 | ||
| 1563 | % returns a list of atoms (strings) for the various options that are available in the state ID | |
| 1564 | % for Row/Col (Y/X) | |
| 1565 | get_react_to_item_right_click_options_for_state(ID,Row,Col,Options) :- | |
| 1566 | get_react_to_item_right_click_options(ID,Col,Row,Options). | |
| 1567 | ||
| 1568 | % should be called for one option provided by get_react_to_item_right_click_options_for_state | |
| 1569 | react_to_item_right_click_option_for_state(ID,Row,Col,Option,TransitionID,NewID) :- | |
| 1570 | react_to_item_right_click(ID,Col,Row,Option,TransitionID,NewID). | |
| 1571 | ||
| 1572 | % | ?- prob2_interface:get_react_to_item_right_click_options_for_state(3,1,1,L). | |
| 1573 | % L = ['Set(1,1,1)','Set(1,1,2)','Set(1,1,3)','Solve'|...] ? | |
| 1574 | % | ?- prob2_interface:react_to_item_right_click_option_for_state(3,1,1,'Set(1,1,1)',NewID). | |
| 1575 | % Performed: Set(int(1),int(1),int(1)) | |
| 1576 | % NewID = ..., TransitionID=... | |
| 1577 | ||
| 1578 | /** | |
| 1579 | get_states_for_predicate(+Raw,-States,-Errors) | |
| 1580 | ||
| 1581 | Takes a predicate and finds a list of all state ids for which the | |
| 1582 | predicate holds. The states that are not intitialized (i.e. root) are | |
| 1583 | included in the list. The list that is returned is therefore the union | |
| 1584 | of the uninitialised states and the states for which the predicate holds. | |
| 1585 | ||
| 1586 | #### called by: | |
| 1587 | * ProB 2.0: GetStatesFromPredicate | |
| 1588 | */ | |
| 1589 | get_states_for_predicate(Raw,States,Errors) :- | |
| 1590 | (predicate_typecheck_for_eval(Raw,Typed) -> | |
| 1591 | findall(StateId,get_state_for_predicate(StateId,Typed),States), | |
| 1592 | Errors = [] | |
| 1593 | ; | |
| 1594 | States = [], | |
| 1595 | get_all_errors_with_span_info_and_reset(Errors) | |
| 1596 | ). | |
| 1597 | ||
| 1598 | get_state_for_predicate(StateId,Typed) :- | |
| 1599 | state_space:visited_expression(StateId,StatePacked), | |
| 1600 | ( is_initialised_state(StateId) -> | |
| 1601 | expand_const_and_vars_to_full_store(StatePacked,State), | |
| 1602 | b_test_boolean_expression_cs(Typed,[],State,'ProB2-Java',0) | |
| 1603 | ; | |
| 1604 | true | |
| 1605 | ). | |
| 1606 | ||
| 1607 | /** | |
| 1608 | This cycles through all of the solutions and extracts the string | |
| 1609 | representation of the solutions. | |
| 1610 | */ | |
| 1611 | prettyprint_solutions(_PPOpts,[],[]). | |
| 1612 | prettyprint_solutions(PPOpts,[bind(Name,Res)|T],[PP|R]) :- | |
| 1613 | pretty_print_bvalue(PPOpts,Res,PPRes), | |
| 1614 | PP = solution(Name,PPRes), | |
| 1615 | prettyprint_solutions(PPOpts,T,R). | |
| 1616 | ||
| 1617 | /** | |
| 1618 | filter_states_for_predicate(+Raw,+States,-Filtered) | |
| 1619 | ||
| 1620 | Takes a list of state ids and a predicate and finds all of the states | |
| 1621 | for which the predicate is true | |
| 1622 | ||
| 1623 | #### called by: | |
| 1624 | * ProB 2.0: FilterStatesForPredicateCommand | |
| 1625 | */ | |
| 1626 | filter_states_for_predicate(Raw,States,Filtered) :- | |
| 1627 | (predicate_typecheck_for_eval(Raw,Typed) -> | |
| 1628 | filter_states_for_typed_predicate(Typed,States,Filtered) | |
| 1629 | ; | |
| 1630 | get_all_errors_with_span_info_and_reset(Errors), | |
| 1631 | Filtered = errors(Errors) | |
| 1632 | ). | |
| 1633 | ||
| 1634 | filter_states_for_typed_predicate(_,[],[]). | |
| 1635 | filter_states_for_typed_predicate(Typed,[Id|States],Filtered) :- | |
| 1636 | get_bstate_with_deferred_sets(Id,false,State,Kind,_), | |
| 1637 | ( Kind = full_initialised_state -> %is_initialised_state(Id) -> | |
| 1638 | (b_test_boolean_expression_cs(Typed,[],State,'ProB2-Java',0) -> | |
| 1639 | Filtered = [Id|Rest] ; | |
| 1640 | Filtered = Rest | |
| 1641 | ) | |
| 1642 | ; Filtered = [Id|Rest] | |
| 1643 | ), | |
| 1644 | filter_states_for_typed_predicate(Typed,States,Rest). | |
| 1645 | ||
| 1646 | /* ------------------------- */ | |
| 1647 | /* Formula Expansion */ | |
| 1648 | /* ------------------------- */ | |
| 1649 | ||
| 1650 | /** | |
| 1651 | get_top_level_formulas(-TopIds) | |
| 1652 | ||
| 1653 | Gets all top-level formula IDs from bvisual2. | |
| 1654 | ||
| 1655 | #### called by: | |
| 1656 | * ProB 2.0: GetTopLevelFormulasCommand | |
| 1657 | */ | |
| 1658 | get_top_level_formulas(TopIds) :- | |
| 1659 | suppress_rodin_positions(C), | |
| 1660 | bv_get_top_level(TopIds), | |
| 1661 | reset_suppress_rodin_positions(C). | |
| 1662 | ||
| 1663 | /** | |
| 1664 | insert_formula_for_expansion(+AST,-Id) | |
| 1665 | ||
| 1666 | Inserts a formula into bvisual2 module | |
| 1667 | The formula is inserted as a child of level "user" in bvisual2 | |
| 1668 | ||
| 1669 | #### called by: | |
| 1670 | * ProB 2.0: InsertFormulaForVisualizationCommand | |
| 1671 | */ | |
| 1672 | insert_formula_for_expansion(Typed,Id) :- Typed = b(_,_,_),!, | |
| 1673 | suppress_rodin_positions(C), | |
| 1674 | bv_insert_formula(Typed,user,Id), | |
| 1675 | reset_suppress_rodin_positions(C). | |
| 1676 | ||
| 1677 | insert_formula_for_expansion(AST,Id) :- | |
| 1678 | suppress_rodin_positions(C), | |
| 1679 | b_type_expression(AST,[variables],_,Typed,Errors), | |
| 1680 | ( Errors == [] -> | |
| 1681 | bv_insert_formula(Typed,user,Id), | |
| 1682 | reset_suppress_rodin_positions(C) | |
| 1683 | ; | |
| 1684 | add_all_perrors(Errors), reset_suppress_rodin_positions(C), | |
| 1685 | fail). | |
| 1686 | ||
| 1687 | /** | |
| 1688 | prob2_evaluate_bvisual2_formulas(+Ids,+StateId,-Values) | |
| 1689 | ||
| 1690 | Uses the bvisual2 module to evaluate the given formulas. | |
| 1691 | Unlike expand_formula_nonrecursive/6, this predicate only evaluates the formulas, | |
| 1692 | but doesn't return their label, description, or subformulas. | |
| 1693 | ||
| 1694 | #### called by: | |
| 1695 | * ProB 2.0: EvaluateBVisual2FormulasCommand | |
| 1696 | */ | |
| 1697 | prob2_evaluate_bvisual2_formulas(Ids,StateId,Values) :- | |
| 1698 | prob2_evaluate_bvisual2_formulas(Ids,StateId,[],Values). | |
| 1699 | ||
| 1700 | /** | |
| 1701 | prob2_evaluate_bvisual2_formulas(+Ids,+StateId,+Options,-Values) | |
| 1702 | ||
| 1703 | New version of the above predicate which also supports options. | |
| 1704 | Currently supported options: | |
| 1705 | - unlimited: does not truncate terms | |
| 1706 | */ | |
| 1707 | prob2_evaluate_bvisual2_formulas(Ids,StateId,Options,Values) :- | |
| 1708 | (member(unlimited,Options) -> | |
| 1709 | bv_get_values_unlimited(Ids,StateId,Values) | |
| 1710 | ; bv_get_values(Ids,StateId,Values)). | |
| 1711 | ||
| 1712 | /** | |
| 1713 | prob2_expand_bvisual2_formula(+FormulaId,+Options,-ExpandedFormula) | |
| 1714 | ||
| 1715 | Uses the bvisual2 module to expand a specified formula, | |
| 1716 | optionally also expanding child formulas recursively and/or evaluating all expanded formulas. | |
| 1717 | FormulaId must be a bvisual2 formula ID, | |
| 1718 | as returned for example by get_top_level_formulas/1, insert_formula_for_expansion/2, or prob2_expand_bvisual2_formula/3. | |
| 1719 | ||
| 1720 | #### called by: | |
| 1721 | * ProB 2.0: ExpandBVisual2FormulaCommand | |
| 1722 | */ | |
| 1723 | prob2_expand_bvisual2_formula(FormulaId,Options,ExpandedFormula) :- | |
| 1724 | % Check that no unknown or duplicate options were passed. | |
| 1725 | (selectchk(evaluate(_), Options, Options1) -> true ; Options1 = Options), | |
| 1726 | (selectchk(recursive, Options1, Options2) -> true ; Options2 = Options1), | |
| 1727 | Options2 == [], | |
| 1728 | ||
| 1729 | suppress_rodin_positions(C), | |
| 1730 | expand_bvisual2_formula_internal(Options,FormulaId,ExpandedFormula), | |
| 1731 | reset_suppress_rodin_positions(C). | |
| 1732 | ||
| 1733 | expand_bvisual2_formula_internal(Options,FormulaId,formula(Entries)) :- | |
| 1734 | findall(Attribute, bvisual2_formula_attribute(FormulaId,Options,Attribute), Entries). | |
| 1735 | ||
| 1736 | bvisual2_formula_attribute(FormulaId,_,id(FormulaId)). | |
| 1737 | bvisual2_formula_attribute(FormulaId,_,description(Description)) :- | |
| 1738 | bv_formula_description(FormulaId,Description). | |
| 1739 | bvisual2_formula_attribute(FormulaId,_,functor_symbol(FunctorSymbol)) :- | |
| 1740 | bv_get_formula_functor_symbol(FormulaId,FunctorSymbol). | |
| 1741 | bvisual2_formula_attribute(FormulaId,_,rodin_labels(Labels)) :- | |
| 1742 | bv_formula_labels(FormulaId,Labels). | |
| 1743 | bvisual2_formula_attribute(FormulaId,_,proof_info(DischargedInfo)) :- | |
| 1744 | bv_formula_discharged_info(FormulaId,DischargedInfo). | |
| 1745 | bvisual2_formula_attribute(FormulaId,Options,value(EvaluatedValue)) :- | |
| 1746 | memberchk(evaluate(StateId), Options), | |
| 1747 | % TODO Refactor to combine multiple bv_get_values calls? | |
| 1748 | bv_get_values([FormulaId], StateId, [EvaluatedValue]). | |
| 1749 | bvisual2_formula_attribute(FormulaId,_,type(Type)) :- | |
| 1750 | (bv_is_typed_predicate(FormulaId) -> | |
| 1751 | Type = predicate; | |
| 1752 | (bv_is_typed_formula(FormulaId) -> Type = expression; Type = other)). | |
| 1753 | bvisual2_formula_attribute(FormulaId,Options,Attribute) :- | |
| 1754 | bv_expand_formula(FormulaId,Label,ChildrenIds), | |
| 1755 | (Attribute = label(Label) ; bvisual2_formula_children_attribute(ChildrenIds,Options,Attribute)). | |
| 1756 | ||
| 1757 | ||
| 1758 | bvisual2_formula_children_attribute(ChildrenIds,Options,children(ExpandedChildren)) :- | |
| 1759 | memberchk(recursive, Options), | |
| 1760 | !, | |
| 1761 | maplist(expand_bvisual2_formula_internal(Options), ChildrenIds, ExpandedChildren). | |
| 1762 | bvisual2_formula_children_attribute(ChildrenIds,_,children_ids(ChildrenIds)). | |
| 1763 | ||
| 1764 | ||
| 1765 | /* ------------------------- */ | |
| 1766 | /* Model Checking */ | |
| 1767 | /* ------------------------- */ | |
| 1768 | ||
| 1769 | /** | |
| 1770 | do_modelchecking(+MaxNumberOfStatesToCheck,+Time,+Options,-Result,-Stats) | |
| 1771 | ||
| 1772 | #### do_modelchecking(+MaxNumberOfStatesToCheck, +Time,+Options,-Result,stats(-NrNodes,-NrTrans,-NrProcessed)) | |
| 1773 | * +MaxNumberOfStatesToCheck : maximum number of states to be checked | |
| 1774 | * +Time : Timeout specified by the user in ms | |
| 1775 | * +Options : List of options specified by the user. Used for predicate do_modelchecking(Time,Options,Result) | |
| 1776 | * -NrNodes : total number of nodes in state space. Calculated with get_state_space_stats | |
| 1777 | * -NrTrans : total number of nodes in state space. Calculated with get_state_space_stats | |
| 1778 | * -NrProcessed : total number of calculated nodes in state space. Calculated with get_state_space_stats | |
| 1779 | When Time Milliseconds have elapsed the modelchecker should stop after its next step | |
| 1780 | ||
| 1781 | #### called by: | |
| 1782 | * ProB Plugin: ModelCheckingCommand | |
| 1783 | * ProB 2.0: ModelCheckingStepCommand | |
| 1784 | */ | |
| 1785 | do_modelchecking(MaxNumberOfStatesToCheck, Time, Options, Result, stats(NrNodes,NrTrans,NrProcessed)) :- | |
| 1786 | statistics(walltime, [CurTime,_]), /* get current time in ms */ | |
| 1787 | LimitTime is CurTime+Time, | |
| 1788 | option_set(find_deadlocks, Options, Deadlock), | |
| 1789 | option_set(find_invariant_violations, Options, Invariant), | |
| 1790 | option_set(find_assertion_violations, Options, Assertions), | |
| 1791 | (option_set(ignore_state_errors, Options, 1) -> FindStateErrors=0 ; FindStateErrors=1), | |
| 1792 | option_set(inspect_existing_nodes, Options, InspectExistingNodes), | |
| 1793 | option_set(stop_at_full_coverage, Options, StopAtFullCoverage), | |
| 1794 | (option_set(breadth_first_search, Options, 1) -> set_depth_breadth_first_mode(breadth_first) ; | |
| 1795 | option_set(depth_first_search, Options, 1) -> set_depth_breadth_first_mode(depth_first) ; | |
| 1796 | set_depth_breadth_first_mode(mixed)), | |
| 1797 | option_set(find_goal, Options, Goal), | |
| 1798 | get_preference(pge,PartialGuardEvaluation), | |
| 1799 | get_preference(por,WithPOR), | |
| 1800 | tcltk_interface:do_model_check(MaxNumberOfStatesToCheck, _, LimitTime, Res, Deadlock, Invariant, Goal,Assertions, | |
| 1801 | FindStateErrors,StopAtFullCoverage, WithPOR, PartialGuardEvaluation, InspectExistingNodes), | |
| 1802 | build_modelcheck_return(Res, Result), | |
| 1803 | get_state_space_stats(NrNodes, NrTrans, NrProcessed). | |
| 1804 | ||
| 1805 | ||
| 1806 | /** | |
| 1807 | set_goal_for_model_checking(+Goal) | |
| 1808 | ||
| 1809 | Sets the goal for model checking. The Option search_for_goal needs to be set when starting | |
| 1810 | model checking in order for this to have an effect on the model checking. | |
| 1811 | ||
| 1812 | #### called by: | |
| 1813 | * ProB 2.0: SetBGoalCommand | |
| 1814 | */ | |
| 1815 | set_goal_for_model_checking(Goal) :- | |
| 1816 | predicate_typecheck_for_eval(Goal,TypedGoal), | |
| 1817 | b_set_parsed_typed_machine_goal(TypedGoal). | |
| 1818 | ||
| 1819 | /** | |
| 1820 | reset_goal_for_model_checking | |
| 1821 | ||
| 1822 | Reset the goal for model checking. Will remove a saved custom goal and load the goal from DEFINITIONS if it exists. | |
| 1823 | ||
| 1824 | #### called by: | |
| 1825 | * ProB 2.0: ResetBGoalCommand | |
| 1826 | */ | |
| 1827 | :- use_module(probsrc(bmachine), [b_unset_machine_goal/0, b_reset_machine_goal_from_DEFINITIONS/0]). | |
| 1828 | reset_goal_for_model_checking :- | |
| 1829 | b_unset_machine_goal, | |
| 1830 | (b_or_z_mode -> (b_reset_machine_goal_from_DEFINITIONS ; true) ; true), | |
| 1831 | !. | |
| 1832 | ||
| 1833 | /** | |
| 1834 | option_set(+Element, +List, -Result) | |
| 1835 | ||
| 1836 | Takes an atom and unifies Result with 1 if the atom is in the List. | |
| 1837 | Otherwise, Result is unified with 0. | |
| 1838 | */ | |
| 1839 | option_set(Element, List, Result) :- | |
| 1840 | ( member(Element,List) | |
| 1841 | -> Result = 1 | |
| 1842 | ; Result = 0). | |
| 1843 | ||
| 1844 | %! build_modelcheck_return(+MCRes, -JavaResult) | |
| 1845 | build_modelcheck_return(MCRes, JavaResult) :- | |
| 1846 | build_modelcheck_return2(MCRes, JavaResult) -> true | |
| 1847 | ; nl, print('### Unknown Model Check Error Result:'), print(MCRes), nl, /* TODO: Why do we print something here? Can we get rid of this print? (Q? from Joy)*/ | |
| 1848 | current_state_id(State), JavaResult=general_error(State, MCRes). | |
| 1849 | ||
| 1850 | build_modelcheck_return2(no, not_yet_finished(100000)). | |
| 1851 | build_modelcheck_return2([timeout,N], not_yet_finished(N1)) :- N1 is 100000 - N. | |
| 1852 | build_modelcheck_return2(deadlock, deadlock(State)):- current_state_id(State). | |
| 1853 | build_modelcheck_return2(invariant_violation, invariant_violation(State)):- current_state_id(State). | |
| 1854 | build_modelcheck_return2(xtl_error, xtl_error(State)):- current_state_id(State). | |
| 1855 | build_modelcheck_return2(assertion_violation, assertion_violation(State)):- current_state_id(State). | |
| 1856 | build_modelcheck_return2(state_error(_), state_error(State)):- current_state_id(State). | |
| 1857 | build_modelcheck_return2(goal_found, goal_found(State)) :- current_state_id(State). | |
| 1858 | build_modelcheck_return2(well_definedness_error, well_definedness_error(State)) :- current_state_id(State). | |
| 1859 | build_modelcheck_return2(general_error_occurred, general_error(State)):- current_state_id(State). | |
| 1860 | build_modelcheck_return2(full_coverage, full_coverage). | |
| 1861 | build_modelcheck_return2(all, Res) :- max_reached_or_timeout_for_node(_),!, Res=ok_not_all_nodes_considered. | |
| 1862 | build_modelcheck_return2(all, ok). | |
| 1863 | ||
| 1864 | :- use_module(symbolic_model_checker(bmc),[bmc_symbolic_model_check/1]). | |
| 1865 | :- use_module(symbolic_model_checker(kinduction), [kinduction_symbolic_model_check/1, tinduction_symbolic_model_check/1]). | |
| 1866 | :- use_module(symbolic_model_checker(ic3), [ic3_symbolic_model_check/1]). | |
| 1867 | symbolic_model_check(bmc,Result) :- | |
| 1868 | bmc_symbolic_model_check(Result). | |
| 1869 | symbolic_model_check(kinduction,Result) :- | |
| 1870 | kinduction_symbolic_model_check(Result). | |
| 1871 | symbolic_model_check(tinduction,Result) :- | |
| 1872 | tinduction_symbolic_model_check(Result). | |
| 1873 | symbolic_model_check(ic3,Result) :- | |
| 1874 | ic3_symbolic_model_check(Result). | |
| 1875 | ||
| 1876 | /** | |
| 1877 | compute_efficient_statespace_stats(-NrNodes, -NrTrans, -NrProcessed) | |
| 1878 | ||
| 1879 | Computes the coverage statistics of the current state space at any given time. | |
| 1880 | The information of interest includes the total number of nodes and transitions, as well as | |
| 1881 | a list of statistics about the nodes and operations and a list of the operations that have been uncovered sofar. | |
| 1882 | ||
| 1883 | #### called by: | |
| 1884 | * ProB Plugin: ComputeCoverageCommand | |
| 1885 | * ProB 2.0: ComputeCoverageCommand | |
| 1886 | */ | |
| 1887 | :- use_module(extrasrc(coverage_statistics), | |
| 1888 | [compute_the_coverage/5, operation_hit/2,query_node_hit/2, uncovered_operation/1]). | |
| 1889 | ||
| 1890 | compute_efficient_statespace_stats(NrNodes, NrTrans, NrProcessed) :- | |
| 1891 | get_state_space_stats(NrNodes, NrTrans, NrProcessed). | |
| 1892 | ||
| 1893 | %! compute_coverage(-TotalNodeNr,-TotalTransSum,-NodeStat,-OpStat,-Uncovered) | |
| 1894 | compute_coverage(TotalNodeNr,TotalTransSum,NodeStat,OpStat,Uncovered) :- | |
| 1895 | compute_the_coverage(_,TotalNodeNr,TotalTransSum,false,false), | |
| 1896 | findall(S2,(operation_hit(OpS,Nr),string_concatenate(':',Nr,S1),string_concatenate(OpS,S1,S2)),OpStat), | |
| 1897 | findall(S2,(query_node_hit(Prop,Nr),string_concatenate(':',Nr,S1),string_concatenate(Prop,S1,S2)),NodeStat), | |
| 1898 | findall(OpName, uncovered_operation(OpName),Uncovered). | |
| 1899 | ||
| 1900 | ||
| 1901 | get_modelchecking_coverage(TotalNodeNr,TotalTransSum,NodeStat,OpStat,Uncovered) :- | |
| 1902 | compute_the_coverage(_,TotalNodeNr,TotalTransSum,false,false), | |
| 1903 | findall(entry(OpS,Nr),operation_hit(OpS,Nr),OpStat), | |
| 1904 | findall(entry(Prop,Nr),query_node_hit(Prop,Nr),NodeStat), | |
| 1905 | findall(OpName, uncovered_operation(OpName),Uncovered). | |
| 1906 | ||
| 1907 | /** | |
| 1908 | get_statistics(+Option,-Value) | |
| 1909 | ||
| 1910 | Takes an option for the statistics and returns the corresponding value. | |
| 1911 | ||
| 1912 | #### called by: | |
| 1913 | * ProB 2.0: GetStatisticsCommand | |
| 1914 | */ | |
| 1915 | ||
| 1916 | get_statistics(global_runtime,V) :- statistics(runtime,[V,_]). | |
| 1917 | get_statistics(global_walltime,V) :- statistics(walltime,[V,_]). | |
| 1918 | get_statistics(delta_runtime,V) :- statistics(runtime,[_,V]). | |
| 1919 | get_statistics(delta_walltime,V) :- statistics(walltime,[_,V]). | |
| 1920 | get_statistics(memory_used,V) :- statistics(memory_used,V). | |
| 1921 | get_statistics(memory_free,V) :- statistics(memory_free,V). | |
| 1922 | get_statistics(global_stack_used,V) :- statistics(global_stack_used,V). | |
| 1923 | get_statistics(local_stack_used,V) :- statistics(local_stack_used,V). | |
| 1924 | %get_statistics(global_stack_free,V) :- statistics(global_stack_free,V). | |
| 1925 | %get_statistics(local_stack_free,V) :- statistics(local_stack_free,V). | |
| 1926 | get_statistics(trail_used,V) :- statistics(trail_used,V). | |
| 1927 | get_statistics(choice_used,V) :- statistics(choice_used,V). | |
| 1928 | get_statistics(atoms_used,V) :- statistics(atoms_used,V). | |
| 1929 | get_statistics(atoms_nbused,V) :- statistics(atoms_nbused,V). | |
| 1930 | get_statistics(gc_count,V) :- statistics(gc_count,V). | |
| 1931 | get_statistics(gc_time,V) :- statistics(gc_time,V). | |
| 1932 | ||
| 1933 | /** | |
| 1934 | prob2_deadlock_freedom_check(+Predicate,-Result) | |
| 1935 | ||
| 1936 | Performs deadlock freedom checking with constraint Predicate and calulates the Result. | |
| 1937 | ||
| 1938 | #### called by: | |
| 1939 | * ProB 2.0: ConstraintBasedDeadlockCheckCommand | |
| 1940 | */ | |
| 1941 | prob2_deadlock_freedom_check(Predicate,Result) :- | |
| 1942 | b_type_expression(Predicate,[variables],pred,TPredicate,Errors), | |
| 1943 | ( Errors == [] -> | |
| 1944 | prob2_deadlock_freedom_check1(TPredicate,Result) | |
| 1945 | ; | |
| 1946 | Result = errors(Errors)). | |
| 1947 | prob2_deadlock_freedom_check1(Predicate,Result) :- | |
| 1948 | % always do a deadlock check with SMT mode enabled | |
| 1949 | call_with_smt_mode_enabled(prob2_deadlock_freedom_check2(Predicate,Result)). | |
| 1950 | :- use_module(clpfd_interface,[catch_clpfd_overflow_call1/1]). | |
| 1951 | :- use_module(b_state_model_check,[cbc_deadlock_freedom_check/3]). | |
| 1952 | prob2_deadlock_freedom_check2(Predicate,Result) :- | |
| 1953 | user_interruptable_call_det(clpfd_interface:catch_clpfd_overflow_call1( | |
| 1954 | b_state_model_check:cbc_deadlock_freedom_check(State,Predicate,0)), | |
| 1955 | InterruptResult),!, | |
| 1956 | ( InterruptResult = interrupted -> | |
| 1957 | Result = interrupted | |
| 1958 | ; State = time_out -> | |
| 1959 | Result = interrupted | |
| 1960 | ; | |
| 1961 | Result = deadlock(Transition,StateId), | |
| 1962 | add_artificial_transition(root,deadlock_check,State,StateId,Transition)). | |
| 1963 | prob2_deadlock_freedom_check2(_Predicate,no_deadlock_found). | |
| 1964 | ||
| 1965 | ||
| 1966 | ||
| 1967 | ||
| 1968 | ||
| 1969 | ||
| 1970 | /** | |
| 1971 | prob2_invariant_check(+Ops,-Result) | |
| 1972 | ||
| 1973 | Performs invariant cbc checking for either for all operations or a list of operations. | |
| 1974 | ||
| 1975 | #### called by: | |
| 1976 | * ProB 2.0: ConstraintBasedInvariantCheckCommand | |
| 1977 | */ | |
| 1978 | prob2_invariant_check(all,Result) :- | |
| 1979 | findall(OpName,b_is_op_or_init(OpName),Ops), | |
| 1980 | % TO DO: also treat $initailise_machine; but state_model_check_invariant does not support it yet | |
| 1981 | prob2_invariant_check2(Ops,Result). | |
| 1982 | prob2_invariant_check(ops(Ops),Result) :- | |
| 1983 | prob2_invariant_check2(Ops,Result). | |
| 1984 | prob2_invariant_check2(Ops,Result) :- | |
| 1985 | call_with_smt_mode_enabled(prob2_invariant_check3(Ops,Result,[])). | |
| 1986 | prob2_invariant_check3([]) --> !. | |
| 1987 | prob2_invariant_check3([Op|Rest]) --> | |
| 1988 | prob2_invariant_check_for_single_op(Op), | |
| 1989 | prob2_invariant_check3(Rest). | |
| 1990 | prob2_invariant_check_for_single_op(OpName,In,Out) :- | |
| 1991 | ( clpfd_interface:catch_clpfd_overflow_call1( | |
| 1992 | b_state_model_check:state_model_check_invariant(OpName,State1,Operation,State2)) -> | |
| 1993 | In = [counterexample(OpName,Trans1,Trans2)|Out], | |
| 1994 | atom_concat( invariant_check_ , OpName, RootTrans), | |
| 1995 | add_artificial_transition(root, RootTrans,State1,StateId1,Trans1), | |
| 1996 | add_artificial_transition(StateId1,Operation,State2,_StateId2,Trans2) | |
| 1997 | ; | |
| 1998 | In = Out). | |
| 1999 | ||
| 2000 | b_is_op_or_init(OpName) :- b_is_operation_name(OpName). | |
| 2001 | b_is_op_or_init(OpName) :- b_is_initialisation_name(OpName). | |
| 2002 | ||
| 2003 | :- use_module(b_state_model_check,[cbc_find_redundant_invariants/2]). | |
| 2004 | prob2_redundant_invariants(Redundant, Timeout) :- | |
| 2005 | cbc_find_redundant_invariants(Redundant, Timeout). | |
| 2006 | ||
| 2007 | /** | |
| 2008 | add_artificial_transition(+SrcId,+Operation,+DstState,+DstId,-TransitionTuple) | |
| 2009 | ||
| 2010 | creates a helper transition that is artificially added to the state space (e.g. during deadlock checking) | |
| 2011 | This transition is added to the state space. | |
| 2012 | A triple TransitionTuple in the form op(TransId,OpName,SrcId,DstId) for this transition is generated. | |
| 2013 | */ | |
| 2014 | add_artificial_transition(SrcId,Operation,DstState,DstId,TransitionTuple) :- | |
| 2015 | tcltk_interface:tcltk_add_new_transition_transid(SrcId,Operation,DstId,DstState,[],TransId), | |
| 2016 | extract_op_name(Operation,OpName), | |
| 2017 | TransitionTuple = op(TransId,OpName,SrcId,DstId). | |
| 2018 | ||
| 2019 | /** | |
| 2020 | computes the enabling relation information for the provided operations of interest | |
| 2021 | get_enable_matrix(-PairsOfOperations,+EnableResult) | |
| 2022 | PairsOfOperations: list of pair(Op1,Op2) of operations pairs for which the enable relation is to be computed | |
| 2023 | EnableResult: list of terms enable_edges(Op1,Op2,enable_edges(E,KE,D,KD)) of same length | |
| 2024 | */ | |
| 2025 | get_enable_matrix(PairsOfOperations,EnableResult) :- | |
| 2026 | maplist(compute_enable_matrix_entry(100),PairsOfOperations,EnableResult). | |
| 2027 | ||
| 2028 | :- use_module(cbcsrc(enabling_analysis),[compute_cbc_enable_rel/4]). | |
| 2029 | compute_enable_matrix_entry(ExtraTimeout,pair(OpName1,OpName2), | |
| 2030 | enable_rel(OpName1,OpName2, | |
| 2031 | enable_edges(Enable,KeepEnabled,Disable,KeepDisabled))) :- | |
| 2032 | compute_cbc_enable_rel(OpName1,OpName2,ExtraTimeout,[Enable,KeepEnabled,Disable,KeepDisabled]). | |
| 2033 | ||
| 2034 | /** | |
| 2035 | prob2_do_ltl_modelcheck(+Formula,+Options,-Result) | |
| 2036 | ||
| 2037 | Performs an LTL model checking step. | |
| 2038 | ||
| 2039 | Supported options: | |
| 2040 | * max_new_states(Max) - maximum number of new states that will be explored, or -1 (the default) for no limit | |
| 2041 | * mode(Mode) - init (the default) to check starting from every initialized state, or specific_node(StateID) to check starting from one specific state | |
| 2042 | ||
| 2043 | #### called by: | |
| 2044 | * ProB 2.0: LtlCheckingCommand | |
| 2045 | */ | |
| 2046 | prob2_do_ltl_modelcheck(Formula, Options, Result) :- | |
| 2047 | (selectchk(max_new_states(Max), Options, Options1) -> true ; Max = -1, Options1 = Options), | |
| 2048 | (selectchk(mode(Mode), Options1, Options2) -> true ; Mode = init, Options2 = Options1), | |
| 2049 | Options2 == [], | |
| 2050 | ||
| 2051 | typecheck_temporal_formula(Formula,TypeCheckedFormula,Status), | |
| 2052 | (Status=ok -> | |
| 2053 | ltl_model_check_with_ce(TypeCheckedFormula,Max,Mode,Result1), | |
| 2054 | prob2_ltl_adapt_operations(Result1,Result) | |
| 2055 | ; | |
| 2056 | get_all_errors_with_span_info_and_reset(Errors), | |
| 2057 | Result = type_error(Errors) | |
| 2058 | ). | |
| 2059 | ||
| 2060 | % Old command without option list - can be removed after release of ProB Java API 4.14.0. | |
| 2061 | prob2_do_ltl_modelcheck(Formula,Max,Result,Errors) :- | |
| 2062 | prob2_do_ltl_modelcheck(Formula, [max_new_states(Max)], Res), | |
| 2063 | (Res = type_error(Errors) -> | |
| 2064 | Result = typeerror | |
| 2065 | ; | |
| 2066 | Result = Res, | |
| 2067 | Errors = [] | |
| 2068 | ). | |
| 2069 | ||
| 2070 | prob2_ltl_adapt_operations(counterexample(CE1,LoopEntry,PathToCE1), Res) :- !, | |
| 2071 | Res = counterexample(CE,LoopEntry,PathToCE), | |
| 2072 | create_simple_op_terms(PathToCE1,root,PathToCE), | |
| 2073 | prob2_ltl_adapt_ce(CE1,CE). | |
| 2074 | prob2_ltl_adapt_operations(Result,Result). | |
| 2075 | ||
| 2076 | prob2_ltl_adapt_ce([],[]). | |
| 2077 | prob2_ltl_adapt_ce([atom(StateId,_,OpTuple)|Irest],[Transition|Orest]) :- | |
| 2078 | prob2_ltl_adapt_ce2(OpTuple,StateId,Transition), | |
| 2079 | prob2_ltl_adapt_ce(Irest,Orest). | |
| 2080 | prob2_ltl_adapt_ce2(none,_StateId,none). | |
| 2081 | prob2_ltl_adapt_ce2((TransId,Action,DestId),StateId,op(TransId,Name,StateId,DestId)) :- | |
| 2082 | extract_op_name(Action,Name). | |
| 2083 | ||
| 2084 | ||
| 2085 | /** | |
| 2086 | prob2_do_ctl_modelcheck(+Formula, +Options, -Result, -CE) | |
| 2087 | ||
| 2088 | Performs an CTL model checking step. | |
| 2089 | ||
| 2090 | Supported options: | |
| 2091 | * max_new_states(Max) - maximum number of new states that will be explored, or -1 (the default) for no limit | |
| 2092 | * mode(Mode) - init (the default) to check starting from every initialized state, or specific_node(StateID) to check starting from one specific state | |
| 2093 | ||
| 2094 | #### called by: | |
| 2095 | * ProB 2.0: CtlCheckingCommand | |
| 2096 | */ | |
| 2097 | prob2_do_ctl_modelcheck(Formula, Options, Result, CE) :- | |
| 2098 | (selectchk(max_new_states(Max), Options, Options1) -> true ; Max = -1, Options1 = Options), | |
| 2099 | (selectchk(mode(Mode), Options1, Options2) -> true ; Mode = init, Options2 = Options1), | |
| 2100 | Options2 == [], | |
| 2101 | ||
| 2102 | typecheck_temporal_formula(Formula, TypeCheckedFormula, Status), | |
| 2103 | (Status = ok -> | |
| 2104 | ctl_model_check_with_ast(main, TypeCheckedFormula, Max, Mode, Result, CE) | |
| 2105 | ; | |
| 2106 | get_all_errors_with_span_info_and_reset(Errors), | |
| 2107 | Result = type_error(Errors) | |
| 2108 | ). | |
| 2109 | ||
| 2110 | % Old command without option list - can be removed after release of ProB Java API 4.14.0. | |
| 2111 | prob2_do_ctl_modelcheck(Formula, MaxNodes, Mode, Res, CE, Errors) :- | |
| 2112 | prob2_do_ctl_modelcheck(Formula, [max_new_states(MaxNodes), mode(Mode)], Res, CE), | |
| 2113 | (Res = type_error(Errors) -> | |
| 2114 | true %Result = typeerror | |
| 2115 | ; | |
| 2116 | %Result = Res, | |
| 2117 | Errors = [] | |
| 2118 | ). | |
| 2119 | ||
| 2120 | ||
| 2121 | /* ------------------------- */ | |
| 2122 | /* Find Traces */ | |
| 2123 | /* ------------------------- */ | |
| 2124 | ||
| 2125 | /** | |
| 2126 | find_trace_to_node(+StateId,-Trace) | |
| 2127 | ||
| 2128 | Finds a trace from the root state to the specified state in the current state space. | |
| 2129 | ||
| 2130 | #### Parameters: | |
| 2131 | * StateId | |
| 2132 | * Trace - List of op tuples op(OpId,SrcId,DestId) corresponding to the trace calculated by ProB or atom no_trace_found if the call was unsuccessful | |
| 2133 | ||
| 2134 | #### called by: | |
| 2135 | * ProB 2.0: GetShortestTraceCommand | |
| 2136 | */ | |
| 2137 | find_trace_to_node(StateId, Trace) :- | |
| 2138 | find_trace_from_node_to_node(root, StateId, Trace). | |
| 2139 | ||
| 2140 | /** | |
| 2141 | find_trace_from_node_to_node(+FromId,+ToId,-Trace) | |
| 2142 | ||
| 2143 | Finds a trace from one state to a goal state in the current state space. | |
| 2144 | ||
| 2145 | #### Parameters: | |
| 2146 | * FromId - Id of source node | |
| 2147 | * ToId - Id of destination node | |
| 2148 | * Trace - List of op tuples op(OpId,SrcId,DestId) corresponding to the trace calculated by ProB or atom no_trace_found if the call was unsuccessful | |
| 2149 | ||
| 2150 | #### called by: | |
| 2151 | * ProB 2.0: GetShortestTraceCommand | |
| 2152 | */ | |
| 2153 | find_trace_from_node_to_node(FromId, ToId, Trace) :- | |
| 2154 | (tcltk_interface:find_shortest_trace_to_node(FromId, ToId, OpIDs, _TraceIDs) -> | |
| 2155 | trace_to_op_terms(OpIDs,FromId,Trace); | |
| 2156 | Trace = no_trace_found | |
| 2157 | ). | |
| 2158 | ||
| 2159 | /** | |
| 2160 | trace_to_op_terms(+ListOpIds,+CurID,-ListOpTerms) | |
| 2161 | ||
| 2162 | Translates a list of transition ids to a list of terms op(TransId,OpName,SrcId,DestId). | |
| 2163 | The list must represent a trace, | |
| 2164 | i. e. the first transition must lead to the source state of the second one, | |
| 2165 | the second transition to the source state of the third, etc. | |
| 2166 | */ | |
| 2167 | trace_to_op_terms([],_,[]). | |
| 2168 | trace_to_op_terms([OpID|T], SrcID, [op(OpID,Name,SrcID,Dest)|OpT]) :- | |
| 2169 | transition(SrcID,Action,OpID,Dest), | |
| 2170 | extract_op_name(Action,Name), | |
| 2171 | trace_to_op_terms(T,Dest,OpT). | |
| 2172 | ||
| 2173 | /** | |
| 2174 | Takes a given predicate and finds a state in the state space that satisfies the predicate. | |
| 2175 | A helper transition is then added to go to the goal state. | |
| 2176 | ||
| 2177 | #### called by: | |
| 2178 | * ProB 2.0: FindValidStateCommand | |
| 2179 | */ | |
| 2180 | :- use_module(b_state_model_check,[b_set_up_valid_state_with_pred/4]). | |
| 2181 | find_state_for_predicate(Predicate,UseInvariant,Result) :- | |
| 2182 | (predicate_typecheck_for_eval(Predicate,TPredicate) -> | |
| 2183 | find_state_for_predicate1(TPredicate,UseInvariant,Result) | |
| 2184 | ; | |
| 2185 | get_all_errors_with_span_info_and_reset(Errors), | |
| 2186 | Result = errors(Errors) | |
| 2187 | ). | |
| 2188 | find_state_for_predicate1(Predicate,UseInvariant,Result) :- | |
| 2189 | user_interruptable_call_det(clpfd_interface:catch_clpfd_overflow_call1( | |
| 2190 | b_state_model_check:b_set_up_valid_state_with_pred(State,Predicate,UseInvariant,none)), % TODO: pass UseConstantsFromStateID | |
| 2191 | InterruptResult),!, | |
| 2192 | ( InterruptResult = interrupted -> | |
| 2193 | Result = interrupted | |
| 2194 | ; State = time_out -> | |
| 2195 | Result = interrupted | |
| 2196 | ; | |
| 2197 | Result = state_found(Transition,StateId), | |
| 2198 | add_artificial_transition(root,find_valid_state,State,StateId,Transition)). | |
| 2199 | find_state_for_predicate1(_Predicate,_,no_valid_state_found). | |
| 2200 | ||
| 2201 | /** | |
| 2202 | cbc_disprove(+Goal,+AllHypotheses,+SelectedHypotheses,+TimeoutFactor,-OutResult) | |
| 2203 | ||
| 2204 | #### called by: | |
| 2205 | * ProB Plugin (de.prob.eventb.disprover.core): DisproverCommand | |
| 2206 | */ | |
| 2207 | cbc_disprove(Goal,AllHypotheses,SelectedHypotheses,TimeoutFactor,OutResult) :- | |
| 2208 | disprove(Goal,AllHypotheses,SelectedHypotheses,TimeoutFactor,OutResult), | |
| 2209 | % remove the warning regarding double check, in rodin it is shown in the proof tree anyway | |
| 2210 | (get_error(warning(disprover_inconsistent_hypotheses),_) ; true). | |
| 2211 | ||
| 2212 | /** | |
| 2213 | cbc_disprove(+Goal,+AllHypotheses,+SelectedHypotheses,+TimeoutFactor,-OutResult) | |
| 2214 | ||
| 2215 | the same with explicit Options: | |
| 2216 | */ | |
| 2217 | cbc_disprove(Goal,AllHypotheses,SelectedHypotheses,TimeoutFactor,Options,OutResult) :- | |
| 2218 | % we do not have to add: [use_smt_mode/true,use_clpfd_solver/true,use_chr_solver/true], | |
| 2219 | % for Rodin these prefs are set in DisproverCommand.java | |
| 2220 | disprove_with_opts(Goal,AllHypotheses,SelectedHypotheses,TimeoutFactor,Options,OutResult), | |
| 2221 | % remove the warning regarding double check, in rodin it is shown in the proof tree anyway | |
| 2222 | (get_error(warning(disprover_inconsistent_hypotheses),_) ; true). | |
| 2223 | ||
| 2224 | :- assert_must_succeed((cbc_solve_with_opts('PROB',[truncate(10)], | |
| 2225 | equal(none,identifier(none,x),integer(none,10)),Identifiers,Result), | |
| 2226 | Identifiers == [x], | |
| 2227 | check_eqeq(Result,solution([binding(x,int(10),'10')])))). | |
| 2228 | ||
| 2229 | /** | |
| 2230 | cbc_solve_with_opts(+Solver,+Options,+Predicate,-Identifiers,-Result) | |
| 2231 | */ | |
| 2232 | cbc_solve_with_opts(Solver,Options,Predicate,Identifiers,Result) :- | |
| 2233 | maplist(prob2_interface:check_cbc_solve_opts,Options), | |
| 2234 | cbc_solve_type(Solver,Options,Predicate,TPredicate), | |
| 2235 | find_identifier_uses(TPredicate,[],Identifiers), | |
| 2236 | (select(timeout_factor(TimeoutFactor),Options,Opts2) -> true ; TimeoutFactor=1,Opts2=Options), | |
| 2237 | ? | cbc_solve_typed(Solver,TPredicate,_,TimeoutFactor,Opts2,Result). |
| 2238 | ||
| 2239 | cbc_timed_solve_with_opts(Solver,Options,Predicate,Identifiers,Result,Milliseconds) :- | |
| 2240 | maplist(prob2_interface:check_cbc_solve_opts,Options), | |
| 2241 | cbc_solve_type(Solver,Options,Predicate,TPredicate), | |
| 2242 | find_identifier_uses(TPredicate,[],Identifiers), | |
| 2243 | (select(timeout_factor(TimeoutFactor),Options,Opts2) -> true ; TimeoutFactor=1,Opts2=Options), | |
| 2244 | cbc_solve_timed(Solver,TPredicate,_,TimeoutFactor,Opts2,Result,Milliseconds). | |
| 2245 | ||
| 2246 | ||
| 2247 | check_cbc_solve_opts(full_machine_state) :- !. | |
| 2248 | check_cbc_solve_opts(solve_in_visited_state(ID)) :- !,atomic(ID). | |
| 2249 | check_cbc_solve_opts(timeout_factor(Nr)) :- !,number(Nr). | |
| 2250 | check_cbc_solve_opts(truncate(Nr)) :- !,number(Nr). % truncate pretty printing | |
| 2251 | check_cbc_solve_opts(truncate) :- !. % truncate pretty printing | |
| 2252 | check_cbc_solve_opts(force_evaluation) :- !. % force evaluation of symbolic results | |
| 2253 | check_cbc_solve_opts(provide_stored_let_values) :- !. | |
| 2254 | check_cbc_solve_opts(all_external_libraries) :- !. | |
| 2255 | check_cbc_solve_opts(IO) :- add_internal_error('Illegal cbc_solve_with_opts option:',IO). | |
| 2256 | ||
| 2257 | ||
| 2258 | :- use_module(cdclt_solver('cdclt_solver'), [cdclt_solve_predicate/3,cdclt_solve_predicate_in_state/4]). | |
| 2259 | :- use_module(probsrc(specfile),[get_state_for_b_formula/3]). | |
| 2260 | :- use_module(solver_interface, [solver_pp_bvalue/4]). | |
| 2261 | ||
| 2262 | timed_solve_predicate(Predicate,State,TimeoutFactor,Options,Result,Time) :- | |
| 2263 | statistics(walltime, [Start, _]), | |
| 2264 | solve_predicate(Predicate,State,TimeoutFactor,Options,Result), | |
| 2265 | statistics(walltime, [Stop,_]), | |
| 2266 | Time is Stop - Start. | |
| 2267 | ||
| 2268 | cbc_solve_timed('PROB',Predicate,State,TimeoutFactor,Options,Result,Time) :- | |
| 2269 | timed_solve_predicate(Predicate,State,TimeoutFactor,['SMT','CLPFD'|Options],Result,Time). | |
| 2270 | cbc_solve_timed('KODKOD',Predicate,State,TimeoutFactor,Options,Result,Time) :- | |
| 2271 | timed_solve_predicate(Predicate,State,TimeoutFactor,['KODKOD','SMT','CLPFD'|Options],Result,Time). | |
| 2272 | cbc_solve_timed('SMT_SUPPORTED_INTERPRETER',Predicate,State,TimeoutFactor,Options,Result,Time) :- | |
| 2273 | timed_solve_predicate(Predicate,State,TimeoutFactor, | |
| 2274 | ['SMT_SUPPORTED_INTERPRETER','SMT','CLPFD'|Options],Result,Time). | |
| 2275 | cbc_solve_timed(SOLVER,Predicate,_StateID,_,Options,Result,Time) :- | |
| 2276 | %TODO: why do we ignore _StateID and TimeoutFactor here? | |
| 2277 | statistics(walltime, [Start, _]), | |
| 2278 | (member(solve_in_visited_state(ID),Options) | |
| 2279 | -> solve_in_state_aux(SOLVER,ID,Predicate,Result) | |
| 2280 | ; solve_free_aux(SOLVER,Predicate,Result) | |
| 2281 | ), | |
| 2282 | statistics(walltime, [Stop,_]), | |
| 2283 | Time is Stop - Start. | |
| 2284 | ||
| 2285 | :- use_module(extension('satsolver/b2sat'), [solve_predicate_with_satsolver_free/4, | |
| 2286 | solve_predicate_with_satsolver_in_state/4]). | |
| 2287 | solve_in_state_aux('CDCLT',ID,Predicate,Result) :- !, | |
| 2288 | get_state_for_b_formula(ID, Predicate, Store), | |
| 2289 | cdclt_solve_predicate_in_state(Predicate, Store, _SolvedPredWdGuaranteed, CdcltResult), | |
| 2290 | translate_cbc_cdclt_result(CdcltResult, Result). | |
| 2291 | solve_in_state_aux('SAT',ID,Predicate,Result) :- !, | |
| 2292 | solve_in_state_sat_aux(ID,Predicate,Result,[]). | |
| 2293 | solve_in_state_aux('SATZ3',ID,Predicate,Result) :- !, | |
| 2294 | solve_in_state_sat_aux(ID,Predicate,Result,[use_satsolver(z3)]). | |
| 2295 | solve_in_state_aux(SOLVER,ID,Predicate,Result) :- | |
| 2296 | recognised_smt_solver(SOLVER,InternalName),!, | |
| 2297 | smt_solve_predicate_in_state(ID,InternalName,Predicate,_State,Result). | |
| 2298 | ||
| 2299 | solve_in_state_sat_aux(ID,Predicate,Result,Opts) :- !, | |
| 2300 | (ID=root -> solve_predicate_with_satsolver_free(Predicate,_,SatResult,Opts) | |
| 2301 | ; get_state_for_b_formula(ID, Predicate, Store), | |
| 2302 | solve_predicate_with_satsolver_in_state(Predicate,Store,SatResult,Opts) | |
| 2303 | ), | |
| 2304 | translate_cbc_cdclt_result(SatResult,Result), | |
| 2305 | print(sat_result(Result)),nl. | |
| 2306 | ||
| 2307 | solve_free_aux('CDCLT',Predicate,Result) :- !, | |
| 2308 | cdclt_solve_predicate(Predicate, _SolvedPredWdGuaranteed, CdcltResult), | |
| 2309 | translate_cbc_cdclt_result(CdcltResult, Result). | |
| 2310 | solve_free_aux('SAT',Predicate,Result) :- | |
| 2311 | solve_predicate_with_satsolver_free(Predicate,_,SatResult,[]), | |
| 2312 | translate_cbc_cdclt_result(SatResult,Result). | |
| 2313 | solve_free_aux('SATZ3',Predicate,Result) :- | |
| 2314 | solve_predicate_with_satsolver_free(Predicate,_,SatResult,[use_satsolver(z3)]), | |
| 2315 | translate_cbc_cdclt_result(SatResult,Result). | |
| 2316 | solve_free_aux(SOLVER,Predicate,Result) :- | |
| 2317 | recognised_smt_solver(SOLVER,InternalName),!, | |
| 2318 | smt_solve_predicate(InternalName,Predicate,_State,Result). | |
| 2319 | ||
| 2320 | cbc_solve_typed(Solver,Predicate,State,TimeoutFactor,Options,Result) :- | |
| 2321 | ? | cbc_solve_timed(Solver,Predicate,State,TimeoutFactor,Options,Result,_). |
| 2322 | ||
| 2323 | % As CDCL(T) does not pretty print its results, we need this translation, | |
| 2324 | % as CbcSolveCommand expects the pretty print. | |
| 2325 | % In case no solution was found, the original CDCL(T) result can be forwarded. | |
| 2326 | translate_cbc_cdclt_result(solution(NonPPBindings), solution(Bindings)) :- | |
| 2327 | !, | |
| 2328 | findall(binding(Id,EValue,PPValue), | |
| 2329 | (member(bind(Id,Value),NonPPBindings), | |
| 2330 | (solver_pp_bvalue(Value,[],EValue,PPValue) -> true | |
| 2331 | ; EValue=Value, PPValue='**pretty-print failed**')), | |
| 2332 | Bindings). | |
| 2333 | translate_cbc_cdclt_result(Result, Result). | |
| 2334 | ||
| 2335 | ||
| 2336 | ||
| 2337 | recognised_smt_solver('Z3',z3). | |
| 2338 | recognised_smt_solver('Z3CNS',z3cns). | |
| 2339 | recognised_smt_solver('Z3AXM',z3axm). | |
| 2340 | recognised_smt_solver('CVC4',cvc4). | |
| 2341 | ||
| 2342 | :- use_module(preferences,[temporary_set_preference/3,reset_temporary_preference/2]). | |
| 2343 | cbc_solve_type('KODKOD',Options,Pred,TPred) :- !, | |
| 2344 | temporary_set_preference(use_solver_on_load,kodkod,C), | |
| 2345 | call_cleanup(cbc_solve_type2(Options,Pred,TPred), | |
| 2346 | reset_temporary_preference(use_solver_on_load,C)). | |
| 2347 | cbc_solve_type(_,Options,Pred,TPred) :- cbc_solve_type2(Options,Pred,TPred). | |
| 2348 | cbc_solve_type2(Options,Pred,TPred) :- | |
| 2349 | !, get_eval_scope_with_opts(Options,Scope), | |
| 2350 | b_type_open_predicate(no_quantifier,Pred,Scope,TPred,Errors), | |
| 2351 | (Errors=[] -> true ; add_error_and_fail(cbc_solve_type, 'Type-Errors: ', Errors)). | |
| 2352 | ||
| 2353 | ||
| 2354 | :- use_module(code2vec(code2vec),[leaf_paths/2]). | |
| 2355 | ast_leaf_walks(B, Walks) :- | |
| 2356 | cbc_solve_type2([], B, TypedB), | |
| 2357 | leaf_paths(TypedB, Walks). | |
| 2358 | ||
| 2359 | /** | |
| 2360 | Takes a predicates and generates a pretty printed string | |
| 2361 | */ | |
| 2362 | :- assert_must_succeed((pretty_print_predicate(equal(none,identifier(none,x),integer(none,1)),[],Result), | |
| 2363 | check_eqeq(Result,'x = 1'))). | |
| 2364 | :- assert_must_succeed((pretty_print_predicate(not_equal(none,identifier(none,x),integer(none,1)),[latex],Result), | |
| 2365 | check_eqeq(Result,'\\mathit{x} \\neq 1'))). | |
| 2366 | :- assert_must_succeed((pretty_print_predicate(not_equal(pos(2,-1,1,1,1,7),integer(pos(3,-1,1,1,1,2),1), | |
| 2367 | integer(pos(4,-1,1,6,1,7),2)),[latex,nopt],PPString), | |
| 2368 | check_eqeq(PPString,'1 \\neq 2' ))). | |
| 2369 | ||
| 2370 | pretty_print_predicate(Pred,Options,PPString) :- | |
| 2371 | ? | select(nopt,Options,Opts2), |
| 2372 | !, | |
| 2373 | temporary_set_preference(optimize_ast,false,CHNG1), | |
| 2374 | call_cleanup(pretty_print_predicate(Pred,Opts2,PPString), | |
| 2375 | reset_temporary_preference(optimize_ast,CHNG1)). | |
| 2376 | pretty_print_predicate(Pred,Options,PPString) :- | |
| 2377 | get_eval_scope_with_opts(Options,Scope), | |
| 2378 | b_type_open_predicate(no_quantifier,Pred,Scope,TPred,Errors), | |
| 2379 | (Errors=[] -> true ; add_error_and_fail(pretty_print_predicate, 'Type-Errors: ', Errors)), | |
| 2380 | options_to_translation_mode(Options, Mode), | |
| 2381 | with_translation_mode(Mode, translate_bexpression(TPred,PPString)). | |
| 2382 | ||
| 2383 | options_to_translation_mode(Options, Mode) :- memberchk(latex, Options), !, Mode = latex. | |
| 2384 | options_to_translation_mode(Options, Mode) :- memberchk(unicode, Options), !, Mode = unicode. | |
| 2385 | options_to_translation_mode(_Options, ascii). | |
| 2386 | ||
| 2387 | % Constraint-Based Test-case generation | |
| 2388 | % TO DO: return values | |
| 2389 | :- use_module(cbcsrc(sap),[cbc_gen_test_cases/5]). | |
| 2390 | cbc_generate_test_cases(TargetPred,MaxDepth,OutputFile) :- | |
| 2391 | % I am not sure whether we should call b_parse_machine_predicate(TargetPred,...) or not | |
| 2392 | Events = all, | |
| 2393 | cbc_gen_test_cases(Events,TargetPred,MaxDepth,OutputFile,_Uncovered). | |
| 2394 | ||
| 2395 | ||
| 2396 | ||
| 2397 | :- use_module(cbcsrc(cbc_path_solver),[create_testcase_path/5]). | |
| 2398 | /** | |
| 2399 | prob2_find_test_path(+Events,+EndPredicate,+TimeoutMs,-ResultOpTerms) | |
| 2400 | ||
| 2401 | example call | ?- prob2_interface:prob2_find_test_path([enter1],truth(unknown),200,R). | |
| 2402 | ||
| 2403 | Result is either errors(Errors), timeout, interrupt, infeasible_path, or list of Operation IDs | |
| 2404 | */ | |
| 2405 | prob2_find_test_path(Events,EndPredicate,TimeoutMs,ResultOpTerms) :- | |
| 2406 | (predicate_typecheck_for_eval(EndPredicate,TPredicate) -> | |
| 2407 | prob2_find_test_path_aux(Events,TPredicate,TimeoutMs,ResultOpTerms) | |
| 2408 | ; | |
| 2409 | get_all_errors_with_span_info_and_reset(Errors), | |
| 2410 | ResultOpTerms = errors(Errors) | |
| 2411 | ). | |
| 2412 | ||
| 2413 | prob2_find_test_path_aux(Events,TPredicate,TimeoutMs,ResOperationIds) :- | |
| 2414 | ( create_testcase_path(init,Events,TPredicate,TimeoutMs,Trace) | |
| 2415 | -> (is_list(Trace) -> maplist(extract_opid,Trace,ResOperationIds) | |
| 2416 | % Trace can be "timeout" or "interrupt", too | |
| 2417 | ; ResOperationIds=Trace) | |
| 2418 | ; ResOperationIds = infeasible_path). | |
| 2419 | ||
| 2420 | extract_opid((TransId,OpTerm,StateId,DestId),op(TransId,Name,StateId,DestId)) :- extract_op_name(OpTerm,Name). | |
| 2421 | ||
| 2422 | /* ------------------------- */ | |
| 2423 | /* Check CSP Assertion */ | |
| 2424 | /* ------------------------- */ | |
| 2425 | ||
| 2426 | /** | |
| 2427 | check_csp_assertions(+Assertions,-Results,-ResultTraces) | |
| 2428 | ||
| 2429 | Takes a list of assertions and produce a list of results and result traces. | |
| 2430 | ||
| 2431 | TODO: We should modify the result traces so that they are useful for ProB 2.0. (or at least document what the result traces mean) | |
| 2432 | ||
| 2433 | #### called by: | |
| 2434 | * ProB 2.0: CSPAssertionsCommand | |
| 2435 | */ | |
| 2436 | check_csp_assertions(Assertions,Results,ResultTraces) :- | |
| 2437 | maplist(check_csp_assertion,Assertions,Results,ResultTraces). | |
| 2438 | ||
| 2439 | check_csp_assertion(AssClause,Res,ResTrace1) :- | |
| 2440 | read_from_codes(AssClause,Assertion), | |
| 2441 | tcltk_interface:checkAssertion(Assertion,_PP,_Negated,Res,ResTrace), | |
| 2442 | (ResTrace = no_counter_example -> ResTrace1 = []; ResTrace1=ResTrace). | |
| 2443 | ||
| 2444 | /* ------------------------- */ | |
| 2445 | /* Preferences Interface */ | |
| 2446 | /* ------------------------- */ | |
| 2447 | ||
| 2448 | /** | |
| 2449 | list_current_eclipse_preferences(-L) | |
| 2450 | ||
| 2451 | Returns a list of all the preferences with their current values | |
| 2452 | ||
| 2453 | #### called by: | |
| 2454 | * ProB 2.0: GetCurrentPreferencesCommand | |
| 2455 | */ | |
| 2456 | list_current_eclipse_preferences(L) :- | |
| 2457 | findall(preference(A,B),find_eclipse_preference(A,B),L). | |
| 2458 | ||
| 2459 | find_eclipse_preference(A,B) :- | |
| 2460 | list_all_eclipse_preferences(X), | |
| 2461 | member(preference(A,_,_,_,_),X), | |
| 2462 | get_eclipse_preference(A,B). | |
| 2463 | ||
| 2464 | /** | |
| 2465 | Returns the current value of a specified preference. | |
| 2466 | ||
| 2467 | #### called by: | |
| 2468 | * ProB 2.0: GetPreferenceCommand | |
| 2469 | */ | |
| 2470 | get_eclipse_preference(PrefS,PrefVal) :- | |
| 2471 | if(eclipse_preference(PrefS,PS), | |
| 2472 | get_preference(PS,PrefVal), | |
| 2473 | add_unknown_preference_error_and_fail(get_eclipse_preference,PrefS)). | |
| 2474 | ||
| 2475 | /** | |
| 2476 | list_eclipse_preferences(-L) | |
| 2477 | ||
| 2478 | Returns a list of all normal eclipse preferences as well as their information | |
| 2479 | (i.e. type, description, category, and default value) | |
| 2480 | ||
| 2481 | #### called by: | |
| 2482 | * ProB Plugin: GetPreferencesCommand | |
| 2483 | * ProB 2.0: GetDefaultPreferencesCommand | |
| 2484 | */ | |
| 2485 | list_eclipse_preferences(L) :- | |
| 2486 | findall(preference(A,B,C,D,E), | |
| 2487 | (get_eclipse_preference_infos(A,B,C,D,E), | |
| 2488 | \+ advanced_eclipse_preference(A,_)), L). | |
| 2489 | ||
| 2490 | /** | |
| 2491 | list_all_eclipse_preferences(-L) | |
| 2492 | ||
| 2493 | also includes advanced eclipse preferences | |
| 2494 | */ | |
| 2495 | list_all_eclipse_preferences(L) :- | |
| 2496 | findall(preference(A,B,C,D,E),get_eclipse_preference_infos(A,B,C,D,E),L). | |
| 2497 | ||
| 2498 | get_eclipse_preference_infos(PrefString,Type,Description,Category,DefaultValue) :- | |
| 2499 | eclipse_preference(PrefString,PS), | |
| 2500 | %\+ advanced_eclipse_preference(PrefString,PS), % we now want to show all preferences in ProB 2 | |
| 2501 | preference_val_type(PS,Type), | |
| 2502 | preference_description(PS,Description), | |
| 2503 | preference_category(PS,Category), | |
| 2504 | preference_default_value(PS,DefaultValue). | |
| 2505 | ||
| 2506 | /** | |
| 2507 | set_eclipse_preference(+PrefS,+PrefVal) | |
| 2508 | ||
| 2509 | Sets a preference | |
| 2510 | ||
| 2511 | #### called by: | |
| 2512 | * ProB Plugin: SetPreferenceCommand | |
| 2513 | * ProB 2.0: SetPreferenceCommand | |
| 2514 | */ | |
| 2515 | :- use_module(tools_strings, [convert_cli_arg/2]). | |
| 2516 | set_eclipse_preference(PrefS,PrefVal) :- | |
| 2517 | convert_cli_arg(PrefVal,Value), | |
| 2518 | convert_pref_value(Value,CValue), | |
| 2519 | ? | (eclipse_preference(PrefS,P) |
| 2520 | -> safe_set_pref(P,CValue,Value) | |
| 2521 | ; deprecated_eclipse_preference(PrefS,_,NewP,Mapping), | |
| 2522 | member(CValue/NewVal,Mapping) | |
| 2523 | -> add_message(set_eclipse_preference,'Deprecated preference: ',PrefS), | |
| 2524 | safe_set_pref(NewP,NewVal,Value) | |
| 2525 | ; obsolete_eclipse_preference(PrefS) | |
| 2526 | -> add_warning(set_eclipse_preference,'Obsolete preference: ',PrefS) % just warn and continue | |
| 2527 | ; add_unknown_preference_error_and_fail(set_eclipse_preference,PrefS) | |
| 2528 | ). | |
| 2529 | ||
| 2530 | safe_set_pref(P,CValue,Value) :- | |
| 2531 | (set_preference(P,CValue) | |
| 2532 | -> true | |
| 2533 | ; ajoin(['Could not set preference ',P,' to: '],Msg), | |
| 2534 | add_error(set_eclipse_preference,Msg,Value) | |
| 2535 | ). | |
| 2536 | ||
| 2537 | convert_pref_value('TRUE',V) :- !, V=true. | |
| 2538 | convert_pref_value('FALSE',V) :- !, V=false. | |
| 2539 | convert_pref_value(X,X). | |
| 2540 | ||
| 2541 | :- use_module(tools_matching,[get_possible_preferences_matches_msg/2]). | |
| 2542 | add_unknown_preference_error_and_fail(Source,PrefS) :- | |
| 2543 | obsolete_eclipse_preference(PrefS),!, | |
| 2544 | add_error_and_fail(Source,'Obsolete preference: ',PrefS). | |
| 2545 | add_unknown_preference_error_and_fail(Source,PrefS) :- | |
| 2546 | get_possible_preferences_matches_msg(PrefS,FuzzyMsg),!, | |
| 2547 | ajoin(['Unknown preference: ',PrefS,'. Did you mean: '],Msg), | |
| 2548 | add_error_and_fail(Source,Msg,FuzzyMsg). | |
| 2549 | add_unknown_preference_error_and_fail(Source,PrefS) :- | |
| 2550 | add_error_and_fail(Source,'Unknown preference: ',PrefS). | |
| 2551 | ||
| 2552 | /* ------------------------- */ | |
| 2553 | /* Apply Graph reduction */ | |
| 2554 | /* ------------------------- */ | |
| 2555 | ||
| 2556 | /** | |
| 2557 | get_signature_merge_state_space(+IgnoredEvents,-Space) | |
| 2558 | ||
| 2559 | Takes a list of ignored events, and applies the signature merge algorithm | |
| 2560 | from module `state_space_reduction` to the current state space. | |
| 2561 | ||
| 2562 | #### called by: | |
| 2563 | * ProB 2.0: ApplySignatureMergeCommand | |
| 2564 | */ | |
| 2565 | get_signature_merge_state_space(IgnoredEvents,Space) :- | |
| 2566 | reset_ignored_events, | |
| 2567 | set_ignored_events(IgnoredEvents), | |
| 2568 | compute_signature_merge, | |
| 2569 | findall(node(NodeId,Count,Color,Labels),extract_node_info(NodeId,Count,Color,simple_list,Labels),Nodes), | |
| 2570 | findall(trans(TransId,Src,Dest,Label,Style,Color),extract_trans_info(true,TransId,Src,Dest,Label,Style,Color),Trans), | |
| 2571 | Space = [Nodes,Trans]. | |
| 2572 | ||
| 2573 | /** | |
| 2574 | get_transition_diagram(+ParsedExpr,-Space) | |
| 2575 | ||
| 2576 | Takes a list of ignored events, and calculates a transition diagram | |
| 2577 | using module `state_space_reduction` for the current state space. | |
| 2578 | ||
| 2579 | #### called by: | |
| 2580 | * ProB 2.0: CalculateTransitionDiagramCommand | |
| 2581 | */ | |
| 2582 | get_transition_diagram(ParsedExpr,Space) :- | |
| 2583 | expression_typecheck_for_eval(ParsedExpr,TypedExpr), | |
| 2584 | compute_transition_diagram(TypedExpr), | |
| 2585 | findall(node(NodeId,Count,Color,Labels),extract_node_info(NodeId,Count,Color,gen_label,Labels),Nodes), | |
| 2586 | findall(trans(TransId,Src,Dest,Label,Style,Color),extract_trans_info(false,TransId,Src,Dest,Label,Style,Color),Trans), | |
| 2587 | Space = [Nodes,Trans]. | |
| 2588 | ||
| 2589 | write_dotty_transition_diagram(Expression,Filename) :- | |
| 2590 | write_dotty_for_expr(transition_diagram,Expression,Filename). | |
| 2591 | ||
| 2592 | write_dotty_signature_merge(IgnoredEvents,Filename) :- | |
| 2593 | write_signature_merge_to_dotfile(IgnoredEvents,Filename). | |
| 2594 | ||
| 2595 | write_dotty_state_space(Filename) :- | |
| 2596 | write_dotty(state_space,Filename). | |
| 2597 | ||
| 2598 | :- use_module(extrasrc(meta_interface),[is_dot_command/1, call_dot_command/3]). | |
| 2599 | % find out which commands only require a filename: | |
| 2600 | is_dotty_command(Command) :- is_dot_command(Command). | |
| 2601 | % call commands which generate a dot file (without requiring further arguments, such as an expression) | |
| 2602 | write_dotty(Command,Filename) :- OptionalArgs=[], | |
| 2603 | call_dot_command(Command,Filename,OptionalArgs). | |
| 2604 | ||
| 2605 | ||
| 2606 | :- use_module(extrasrc(meta_interface),[is_dot_command_for_expr/1, call_dot_command_for_expr/4]). | |
| 2607 | % find out which commands only require an expression and a filename: | |
| 2608 | is_dotty_command_for_expr(Command) :- is_dot_command_for_expr(Command). | |
| 2609 | % call commands which generate a dot file from an expression: | |
| 2610 | write_dotty_for_expr(Command,Expr,Filename) :- OptionalArgs=[], | |
| 2611 | call_dot_command_for_expr(Command,Expr,Filename,OptionalArgs). | |
| 2612 | ||
| 2613 | ||
| 2614 | :- use_module(extrasrc(meta_interface),[is_plantuml_command/1, call_plantuml_command/3]). | |
| 2615 | :- use_module(extrasrc(meta_interface),[is_plantuml_command_for_expr/1, call_plantuml_command_for_expr/4]). | |
| 2616 | :- use_module(extrasrc(meta_interface),[command_unavailable/2]). | |
| 2617 | ||
| 2618 | % -------------------------------------------------------- | |
| 2619 | % New preferred API for calling DOT / TABLE commands in ProB2 JFX: | |
| 2620 | % get_dot_commands_in_state/2 and call_dot_command_in_state/4 | |
| 2621 | % get_planuml_commands_in_state/2 and call_plantuml_command_in_state/4 | |
| 2622 | % get_table_commands_in_state/2 and call_table_command_in_state/4 | |
| 2623 | ||
| 2624 | get_commands_in_state(Category,StateID,List) :- | |
| 2625 | tcltk_interface:tcltk_try_goto_node_with_id(StateID), | |
| 2626 | findall(command(Command,Name,Description,NumberOfFormulaArgs,RelevantEclipsePrefs,AdditionalInfo,AvailMsg), | |
| 2627 | (is_a_command(Category,Command,Name,Description,NumberOfFormulaArgs,RelevantPrefs,AdditionalInfo), | |
| 2628 | maplist(convert_pref,RelevantPrefs,RelevantEclipsePrefs), | |
| 2629 | (command_unavailable(Command,AvailMsg) -> true ; AvailMsg = available)), | |
| 2630 | List). | |
| 2631 | get_commands_with_trace(Category,TransIDs,List) :- | |
| 2632 | try_set_trace_by_transition_ids(TransIDs), | |
| 2633 | findall(command(Command,Name,Description,NumberOfFormulaArgs,RelevantEclipsePrefs,AdditionalInfo,AvailMsg), | |
| 2634 | (is_a_command(Category,Command,Name,Description,NumberOfFormulaArgs,RelevantPrefs,AdditionalInfo), | |
| 2635 | maplist(convert_pref,RelevantPrefs,RelevantEclipsePrefs), | |
| 2636 | (command_unavailable(Command,AvailMsg) -> true ; AvailMsg = available)), | |
| 2637 | List). | |
| 2638 | ||
| 2639 | % example call: prob2_interface:get_dot_commands_in_state(1,List). | |
| 2640 | get_dot_commands_in_state(StateID,List) :- get_commands_in_state(dot,StateID,List). | |
| 2641 | get_dot_commands_with_trace(TransIDs,List) :- get_commands_with_trace(dot,TransIDs,List). | |
| 2642 | % example call: prob2_interface:get_plantuml_commands_in_state(1,List). | |
| 2643 | get_plantuml_commands_in_state(StateID,List) :- get_commands_in_state(plantuml,StateID,List). | |
| 2644 | get_plantuml_commands_with_trace(TransIDs,List) :- get_commands_with_trace(plantuml,TransIDs,List). | |
| 2645 | % example call: prob2_interface:get_table_commands_in_state(1,List). | |
| 2646 | get_table_commands_in_state(StateID,List) :- get_commands_in_state(table,StateID,List). | |
| 2647 | get_table_commands_with_trace(TransIDs,List) :- get_commands_with_trace(table,TransIDs,List). | |
| 2648 | ||
| 2649 | convert_pref(Pref,Res) :- eclipse_preference(ECLIPSEPREF,Pref),!,Res=ECLIPSEPREF. | |
| 2650 | convert_pref(P,P) :- preference_default_value(P,_),!. | |
| 2651 | convert_pref(P,P) :- print(unknown_preference(P)),nl. | |
| 2652 | ||
| 2653 | :- use_module(extrasrc(meta_interface),[is_dot_command/6, is_plantuml_command/6, is_table_command/6]). | |
| 2654 | is_a_command(dot,Command,Name,Description,NumberOfFormulaArgs,RelevantPreferences,AdditionalInfo) :- | |
| 2655 | is_dot_command(Command,Name,Description,NumberOfFormulaArgs,RelevantPreferences,AdditionalInfo). | |
| 2656 | is_a_command(plantuml,Command,Name,Description,NumberOfFormulaArgs,RelevantPreferences,AdditionalInfo) :- | |
| 2657 | is_plantuml_command(Command,Name,Description,NumberOfFormulaArgs,RelevantPreferences,AdditionalInfo). | |
| 2658 | is_a_command(table,Command,Name,Description,NumberOfFormulaArgs,RelevantPreferences,AdditionalInfo) :- | |
| 2659 | is_table_command(Command,Name,Description,NumberOfFormulaArgs,RelevantPreferences,AdditionalInfo). | |
| 2660 | ||
| 2661 | ||
| 2662 | call_dot_command_in_state(StateID,Command,Formulas,DotFile) :- | |
| 2663 | tcltk_interface:tcltk_try_goto_node_with_id(StateID), | |
| 2664 | call_dot_command_for_dotfile(Command,Formulas,DotFile). | |
| 2665 | call_dot_command_with_trace(TransIDs,Command,Formulas,DotFile) :- | |
| 2666 | try_set_trace_by_transition_ids(TransIDs), | |
| 2667 | call_dot_command_for_dotfile(Command,Formulas,DotFile). | |
| 2668 | ||
| 2669 | % call a dot command for generating a DotFile; used by call_dot_command_in_state | |
| 2670 | call_dot_command_for_dotfile(Command,[],DotFile) :- | |
| 2671 | is_dot_command(Command), !, OptionalArgs=[], | |
| 2672 | call_dot_command(Command,DotFile,OptionalArgs). | |
| 2673 | call_dot_command_for_dotfile(Command,[Expr],DotFile) :- | |
| 2674 | is_dot_command_for_expr(Command), !, OptionalArgs=[], | |
| 2675 | call_dot_command_for_expr(Command,Expr,DotFile,OptionalArgs). | |
| 2676 | call_dot_command_for_dotfile(Command,Formulas,DotFile) :- | |
| 2677 | add_internal_error('Illegal dot call: ',call_dot_command_for_dotfile(Command,Formulas,DotFile)), | |
| 2678 | fail. | |
| 2679 | ||
| 2680 | ||
| 2681 | call_plantuml_command_in_state(StateID,Command,Formulas,UmlFile) :- | |
| 2682 | tcltk_interface:tcltk_try_goto_node_with_id(StateID), | |
| 2683 | call_plantuml_command_for_pumlfile(Command,Formulas,UmlFile). | |
| 2684 | call_plantuml_command_with_trace(TransIDs,Command,Formulas,UmlFile) :- | |
| 2685 | try_set_trace_by_transition_ids(TransIDs), | |
| 2686 | call_plantuml_command_for_pumlfile(Command,Formulas,UmlFile). | |
| 2687 | ||
| 2688 | % call a plantuml command for generating a UmlFile; used by call_plantuml_command_in_state | |
| 2689 | call_plantuml_command_for_pumlfile(Command,[],UmlFile) :- | |
| 2690 | is_plantuml_command(Command), !, OptionalArgs=[], | |
| 2691 | call_plantuml_command(Command,UmlFile,OptionalArgs). | |
| 2692 | call_plantuml_command_for_pumlfile(Command,[Expr],UmlFile) :- | |
| 2693 | is_plantuml_command_for_expr(Command), !, OptionalArgs=[], | |
| 2694 | call_plantuml_command_for_expr(Command,Expr,UmlFile,OptionalArgs). | |
| 2695 | call_plantuml_command_for_pumlfile(Command,Formulas,UmlFile) :- | |
| 2696 | add_internal_error('Illegal plantuml call: ',call_dot_command_for_pumlfile(Command,Formulas,UmlFile)), | |
| 2697 | fail. | |
| 2698 | ||
| 2699 | % example call: prob2_interface:call_table_command_in_state(1,expr_as_table,[integer(pos,1)],Table). | |
| 2700 | :- use_module(extrasrc(meta_interface),[call_command/5]). | |
| 2701 | call_table_command_in_state(StateID,Command,Formulas,TableResult) :- | |
| 2702 | tcltk_interface:tcltk_try_goto_node_with_id(StateID), | |
| 2703 | append(Formulas,[TableResult],ActualArgs), | |
| 2704 | OptionalArgs=[], | |
| 2705 | debug_println(9,call_command(table,Command,_,ActualArgs,OptionalArgs)), | |
| 2706 | call_command(table,Command,_,ActualArgs,OptionalArgs), debug_println(9,result(TableResult)), | |
| 2707 | !. | |
| 2708 | call_table_command_in_state(StateID,Command,Formulas,TableResult) :- | |
| 2709 | add_error(call_table_command_in_state,'Table command failed:',call_table_command_in_state(StateID,Command,Formulas,TableResult)), | |
| 2710 | TableResult = list([list(['ERROR OCCURED'])]). | |
| 2711 | ||
| 2712 | call_table_command_with_trace(TransIDs,Command,Formulas,TableResult) :- | |
| 2713 | try_set_trace_by_transition_ids(TransIDs), | |
| 2714 | append(Formulas,[TableResult],ActualArgs), | |
| 2715 | OptionalArgs=[], | |
| 2716 | debug_println(9,call_command(table,Command,_,ActualArgs,OptionalArgs)), | |
| 2717 | call_command(table,Command,_,ActualArgs,OptionalArgs), debug_println(9,result(TableResult)), | |
| 2718 | !. | |
| 2719 | call_table_command_with_trace(TransIDs,Command,Formulas,TableResult) :- | |
| 2720 | add_error(call_table_command_with_trace,'Table command failed:',call_table_command_with_trace(TransIDs,Command,Formulas,TableResult)), | |
| 2721 | TableResult = list([list(['ERROR OCCURED'])]). | |
| 2722 | ||
| 2723 | ||
| 2724 | /** | |
| 2725 | write_dot_for_state_viz(+StateId, +Filename) | |
| 2726 | ||
| 2727 | Writes a dot representation of the given state to the specified file. | |
| 2728 | ||
| 2729 | */ | |
| 2730 | write_dot_for_state_viz(StateId, Filename) :- | |
| 2731 | get_state(StateId, State), | |
| 2732 | print_cstate_graph(State, Filename). | |
| 2733 | ||
| 2734 | /** | |
| 2735 | extract_node_info(+NodeId,-Count,-Color,+LabelGenerator,-Labels) | |
| 2736 | ||
| 2737 | Generates information about the nodes found during state space reduction | |
| 2738 | ||
| 2739 | #### Generated Information: | |
| 2740 | * Count - number of concrete states combined in the abstract state | |
| 2741 | * Color - the color used to represent this state type in a visualization | |
| 2742 | * Labels - determine the labels that should appear on a node in a visualization | |
| 2743 | */ | |
| 2744 | extract_node_info(NodeId,Count,Color,LabelGenerator,Labels) :- | |
| 2745 | get_reduced_node(AbsState,Count,Witness,NodeId), | |
| 2746 | generate_node_color(NodeId,Witness,AbsState,Count,Color), | |
| 2747 | generate_node_labels(LabelGenerator,AbsState,Labels). | |
| 2748 | ||
| 2749 | /** | |
| 2750 | extract_trans_info(+ShowSelfLoops,+TransId,-Src,-Dest,-Label,-Style,-Color) | |
| 2751 | ||
| 2752 | Generates information about the transitions created during state space reduction | |
| 2753 | ||
| 2754 | #### Generated Information: | |
| 2755 | * Src - ID corresponding to the abstract state that is the source of the abstract transition with TransId | |
| 2756 | * Dest - ID corresponding to the abstract state that is the destination of the abstract transition with TransId | |
| 2757 | * Label - the label that should appear on a transition in a visualization | |
| 2758 | * Style - the style that should be applied to a transition of this type in a visualization (e.g. dashed) | |
| 2759 | * Color - the color used to represent a transition of this type in a visualization | |
| 2760 | */ | |
| 2761 | extract_trans_info(ShowSelfLoops,TransId,Src,Dest,Label,Style,Color) :- | |
| 2762 | reduced_trans(Src,AbsAction,Count,Dest,TransId), | |
| 2763 | generate_transition_label(AbsAction,Count,Label), | |
| 2764 | generate_transition_color_and_style(ShowSelfLoops,Src,AbsAction,Dest,Color,Style). | |
| 2765 | ||
| 2766 | ||
| 2767 | /* ------------------ */ | |
| 2768 | /* Get Errors */ | |
| 2769 | /* ------------------ */ | |
| 2770 | ||
| 2771 | /** | |
| 2772 | get_error_messages_with_span_info(-ListOfErrMsgTerms) | |
| 2773 | ||
| 2774 | each error is of the form: error(ErrMsg,ErrType,ErrLocations) | |
| 2775 | ErrMsg is an atom (aka string) | |
| 2776 | ErrType is warning, internal_error or error | |
| 2777 | ErrLocations is a list of terms error_span(Filename,StartLine,StartCol,EndLine,EndCol) | |
| 2778 | Note: Filename is '' when not known | |
| 2779 | ||
| 2780 | #### called by: | |
| 2781 | * ProB 2.0: GetErrorItemsCommand | |
| 2782 | */ | |
| 2783 | get_error_messages_with_span_info(ListOfErrMsgTerms) :- | |
| 2784 | ignore_user_interrupt_det(get_all_errors_with_span_info_and_reset(ListOfErrMsgTerms)). | |
| 2785 | % TODO: replace by this: | |
| 2786 | % error(ErrMsg,ErrType,ErrLocations,GlobalContext,CallStack) | |
| 2787 | get_error_messages_with_span_and_contxt(ListOfErrMsgTerms) :- | |
| 2788 | ignore_user_interrupt_det(get_all_errors_with_span_and_context_and_reset(ListOfErrMsgTerms)). | |
| 2789 | ||
| 2790 | ||
| 2791 | % #################### | |
| 2792 | ||
| 2793 | /** | |
| 2794 | generate_trace_until_condition_fulfilled(+CurState,+Condition,-Trace,-Result) | |
| 2795 | ||
| 2796 | Animates randomly number of steps until a certain (LTL?) condition is fulfilled. | |
| 2797 | ||
| 2798 | #### Called by: | |
| 2799 | * ProB 2.0: ExecuteUntilCommand | |
| 2800 | ||
| 2801 | #### Arguments | |
| 2802 | * CurState - the ID of the current state | |
| 2803 | * Condition - a condition that should be satisfied at some point (this come as parsed term from the ProB2) | |
| 2804 | ||
| 2805 | #### Generated Information: | |
| 2806 | * Trace - a list of triples representing a trace in the state space of the model being analysed | |
| 2807 | * Result - the result found: ltl_found, typeerror, max_nr_of_steps_reached, deadlock | |
| 2808 | */ | |
| 2809 | generate_trace_until_condition_fulfilled(CurState,Condition,Trace,Result) :- | |
| 2810 | typecheck_temporal_formula(Condition,TypeCheckedCondition,Status), | |
| 2811 | ( Status=ok -> find_trace1(CurState,TypeCheckedCondition,no_loop,100000,Trace, Result) %FIXME: turn maximal numver of steps into an argument? | |
| 2812 | ; reset_errors, % Reset errors. We don't want to throw a ProBError on the Java side because the result is capsuled in Result. | |
| 2813 | Result=typeerror, Trace=[]). | |
| 2814 | ||
| 2815 | find_trace1(StateId,Ltl,Type,MaxSteps,OpTripleResultTrace, Result) :- | |
| 2816 | (MaxSteps =< 0 | |
| 2817 | -> add_error(find_trace,'Number of maximum animation steps should be a positive integer. The number of steps which was given is ',MaxSteps) | |
| 2818 | ; true), | |
| 2819 | set_current_state(StateId), !, % can be backtracked | |
| 2820 | % negate -> counterexample is the trace we are looking for | |
| 2821 | preprocess_formula(Ltl,Ltl2), | |
| 2822 | find_trace_aux(StateId,not(Ltl2),Type,0,MaxSteps,ResultTrace,ResultTrace,Names,Result), | |
| 2823 | gen_op_triples(ResultTrace,Names,OpTripleResultTrace). | |
| 2824 | %(gen_op_triples(ResultTrace,OpTripleResultTrace) -> print(ok(OpTripleResultTrace,result(Result))),nl | |
| 2825 | % ; add_error_and_fail(prob2_interface,'trace not correctly generated',ResultTrace)). | |
| 2826 | ||
| 2827 | find_trace_aux(CurID,Condition,Type,_N,_Max,StateTransitionHistory,[],[],RESULT) :- | |
| 2828 | debug_println(9,checking_ltl_formula(CurID,StateTransitionHistory)), | |
| 2829 | evaluate_ltl_formula(Condition,StateTransitionHistory,Type,ltl:check_ap,ltl:callback_tp,EvResult), | |
| 2830 | EvResult = false, | |
| 2831 | !, | |
| 2832 | RESULT=ltl_found. | |
| 2833 | find_trace_aux(CurID,Condition,Type,N,Max,StateTransitionHistory,STTail,Names,RESULT) :- | |
| 2834 | tcltk_interface:tcltk_compute_options(CurID,ActionsAndIDs), | |
| 2835 | debug_println(9,opts(ActionsAndIDs)), | |
| 2836 | ( N=Max | |
| 2837 | -> debug_println(9,'Maximum number of animation steps reached.'), | |
| 2838 | Names = [], | |
| 2839 | RESULT = maximum_nr_of_steps_reached | |
| 2840 | ; pick_action(random,ActionsAndIDs,ActionId,Name,DstID) % pick first one; we could do random | |
| 2841 | -> debug_println(9,performing_action(ActionId,from_to(CurID,DstID),opts(ActionsAndIDs))), | |
| 2842 | STTail = [strans(CurID,ActionId)|STTail2], | |
| 2843 | Names = [Name|Names2], | |
| 2844 | N1 is N+1, | |
| 2845 | find_trace_aux(DstID,Condition,Type,N1,Max,StateTransitionHistory,STTail2,Names2,RESULT) | |
| 2846 | ; STTail=[], Names = [], RESULT = deadlock | |
| 2847 | ). | |
| 2848 | ||
| 2849 | gen_op_triples([],[],[]). | |
| 2850 | gen_op_triples([_X],[_Y],[]). | |
| 2851 | gen_op_triples([strans(CurID,ActionId),strans(DstID,ActId)|T],[Name|NameT],[op(ActionId,Name,CurID,DstID)|Rest]) :- | |
| 2852 | gen_op_triples([strans(DstID,ActId)|T],NameT,Rest). | |
| 2853 | ||
| 2854 | :- use_module(library(random)). | |
| 2855 | :- use_module(library(lists)). | |
| 2856 | pick_action(first,[(ActionId,Term,DstID)|_], ActionId, Name, DstID) :- extract_op_name(Term,Name). | |
| 2857 | pick_action(random,Options,ActionId, Name, DstID) :- | |
| 2858 | length(Options,Len), | |
| 2859 | L1 is Len+1, | |
| 2860 | random(1,L1,RanChoice), | |
| 2861 | debug_println(9,random(RanChoice,Len)), | |
| 2862 | nth1(RanChoice,Options,(ActionId,ActionAsTerm,DstID)), | |
| 2863 | extract_op_name(ActionAsTerm,Name). | |
| 2864 | ||
| 2865 | ||
| 2866 | % ------------------------------------- | |
| 2867 | ||
| 2868 | /** | |
| 2869 | execute_model(+CurStateID,+MaxNrSteps,-TransitionInfo,-ExecutedSteps,-Result) | |
| 2870 | ||
| 2871 | an execution engine with minimal overhead: states are not stored in visited_expression database, only first enabled operation is taken | |
| 2872 | */ | |
| 2873 | execute_model(CurStateID,MaxNrSteps,TransitionInfo,ExecutedSteps,Result) :- | |
| 2874 | temporary_set_preference(try_operation_reuse,false,ChangeOccured), | |
| 2875 | (ChangeOccured=true | |
| 2876 | -> add_message(execute_model,'Disabling OPERATION_REUSE preference for execution from state: ',CurStateID) ; true), | |
| 2877 | call_cleanup(execute_model(CurStateID,MaxNrSteps,[],TransitionInfo,ExecutedSteps,Result), | |
| 2878 | reset_temporary_preference(try_operation_reuse,ChangeOccured)). | |
| 2879 | ||
| 2880 | /** | |
| 2881 | execute_model(+CurStateID,+MaxNrSteps,+Options,-TransitionInfo,-ExecutedSteps,-Result) | |
| 2882 | ||
| 2883 | Options can contain continue_after_errors, timeout(MS) | |
| 2884 | Result is either maximum_nr_of_steps_reached, deadlock, error, internal_error, time_out | |
| 2885 | */ | |
| 2886 | execute_model(CurStateID,MaxNrSteps,Options,TransitionInfo,ExecutedSteps,Result) :- | |
| 2887 | visited_expression(CurStateID,CurState0), | |
| 2888 | prepare_state_for_specfile_trans(CurState0,CurStateID,CurState), | |
| 2889 | % TODO: we still need to ensure that the individual steps below do not repack constants | |
| 2890 | execute_model_steps(0,CurState,MaxNrSteps,Options,'$none',NewState,ExecutedSteps,LastAction,Result), | |
| 2891 | (ExecutedSteps>0 | |
| 2892 | -> (ExecutedSteps=1, LastAction=act(ActionName,ActTerm) | |
| 2893 | -> true % use real action name and term | |
| 2894 | ; ActionName='EXECUTE', ActTerm='$JUMP'('EXECUTE'(ExecutedSteps))), | |
| 2895 | tcltk_interface:tcltk_add_new_transition_transid(CurStateID,ActTerm,ToID,NewState,[],TransId), | |
| 2896 | debug_println(4,added_transition_for_execute(ExecutedSteps,ToID)), | |
| 2897 | tcltk_interface:tcltk_goto_state(ActTerm,ToID), | |
| 2898 | TransitionInfo = op(TransId,ActionName,CurStateID,ToID) | |
| 2899 | ; TransitionInfo = none). | |
| 2900 | ||
| 2901 | execute_model_steps(StepNr,CurState,MaxNrSteps,_Options,PrevAction,NewState,ExecutedSteps,LastAction,Result) :- | |
| 2902 | StepNr >= MaxNrSteps,!, | |
| 2903 | NewState=CurState, | |
| 2904 | ExecutedSteps=StepNr, | |
| 2905 | LastAction=PrevAction, | |
| 2906 | Result=maximum_nr_of_steps_reached. | |
| 2907 | execute_model_steps(StepNr,CurState,MaxNrSteps,Options,PrevAction,NewState,ExecutedSteps,LastAction,Result) :- | |
| 2908 | cli_trans_aux(StepNr,CurState,Options,ActionName,ActTerm,State2,ErrorRes), | |
| 2909 | !, | |
| 2910 | debug_println(20,execute(StepNr,ActionName)), | |
| 2911 | S1 is StepNr+1, | |
| 2912 | (nonvar(ErrorRes) | |
| 2913 | -> Result=ErrorRes, ExecutedSteps=StepNr, NewState=CurState, LastAction=PrevAction | |
| 2914 | ; PrevAction2=act(ActionName,ActTerm), | |
| 2915 | execute_model_steps(S1,State2,MaxNrSteps,Options,PrevAction2,NewState,ExecutedSteps,LastAction,Result)). | |
| 2916 | execute_model_steps(Steps,CurState,_,_Options,PrevAction,CurState,Steps,PrevAction,deadlock). | |
| 2917 | ||
| 2918 | :- use_module(specfile,[specfile_possible_trans_name_for_successors/2,prepare_state_for_specfile_trans/3, | |
| 2919 | specfile_trans_or_partial_trans/7]). | |
| 2920 | :- use_module(error_manager,[throw_enumeration_warnings_in_current_scope/0, add_internal_error/2, error_occurred_in_error_scope/0]). | |
| 2921 | :- use_module(tools_meta,[safe_time_out/3]). | |
| 2922 | ||
| 2923 | % TO DO: use same optimisation as in -execute in prob_cli.pl (get_possible_next_operation_for_execute) | |
| 2924 | cli_trans_aux(StepNr,CurState,Options,ActionName,Act,NewState,ErrorRes) :- | |
| 2925 | specfile_possible_trans_name_for_successors(CurState,ActionName), | |
| 2926 | catch_enumeration_warning_exceptions( | |
| 2927 | (throw_enumeration_warnings_in_current_scope, | |
| 2928 | (member(timeout(MS),Options) -> | |
| 2929 | safe_time_out(specfile_trans_or_partial_trans(CurState,ActionName,Act,NewState,_TransInfo1,Residue,_),MS,TR) | |
| 2930 | ; specfile_trans_or_partial_trans(CurState,ActionName,Act,NewState,_TransInfo2,Residue,_) % no time-out ! | |
| 2931 | ), | |
| 2932 | (TR==time_out | |
| 2933 | -> add_error(execute,'Timeout occured during execute after step: ',StepNr),ErrorRes=time_out | |
| 2934 | ; error_occurred_in_error_scope -> | |
| 2935 | (member(continue_after_errors,Options) -> true | |
| 2936 | ; add_error(execute,'Error occured during execute after step: ',StepNr),ErrorRes=error) | |
| 2937 | ; true) | |
| 2938 | ), | |
| 2939 | (add_error(virtual_time_out_execute,'Virtual TIME-OUT occured during execute after step: ',StepNr), | |
| 2940 | ActionName = '*** VIRTUAL_TIME_OUT ***', Act=ActionName, | |
| 2941 | ErrorRes=time_out) | |
| 2942 | ), | |
| 2943 | (Residue=[] -> true | |
| 2944 | ; add_internal_error('Residue during execute after step: ',StepNr:Residue), | |
| 2945 | (nonvar(ErrorRes) -> true ; ErrorRes=internal_error)). | |
| 2946 | ||
| 2947 | % ------------------------------------- | |
| 2948 | ||
| 2949 | % computes a unsat core | |
| 2950 | :- use_module(tools,[start_ms_timer/1, stop_ms_walltimer_with_msg/2]). | |
| 2951 | get_unsat_core_with_fixed_conjuncts(Pred,FixedPreds,CoreOut) :- | |
| 2952 | typecheck_pred_for_unsat_core(Pred,TypedPred), | |
| 2953 | maplist(typecheck_pred_for_unsat_core,FixedPreds,TypedFixedPreds), | |
| 2954 | conjunct_predicates(TypedFixedPreds,Conj), | |
| 2955 | format('Computing an unsat core~n',[]), start_ms_timer(Timer), | |
| 2956 | unsat_chr_core_with_fixed_conjuncts_auto_time_limit(TypedPred,Conj,2000,Core), | |
| 2957 | stop_ms_walltimer_with_msg(Timer,'Computed unsat core'), | |
| 2958 | translate_bexpression(Core,CoreOut). | |
| 2959 | ||
| 2960 | % computes the unsat core of minimal size: | |
| 2961 | get_minimum_unsat_core_with_fixed_conjuncts(Pred,FixedPreds,CoreOut) :- | |
| 2962 | typecheck_pred_for_unsat_core(Pred,TypedPred), | |
| 2963 | maplist(typecheck_pred_for_unsat_core,FixedPreds,TypedFixedPreds), | |
| 2964 | conjunct_predicates(TypedFixedPreds,Conj), | |
| 2965 | format('Computing the minimal unsat core~n',[]), | |
| 2966 | minimum_unsat_core_with_fixed_conjuncts(TypedPred,Conj,Core), | |
| 2967 | translate_bexpression(Core,CoreOut). | |
| 2968 | ||
| 2969 | typecheck_pred_for_unsat_core(PIn,POut) :- | |
| 2970 | predicate_typecheck_for_eval(PIn,TExpr), | |
| 2971 | (get_texpr_expr(TExpr,exists(_,POut)) -> true | |
| 2972 | ; format(user_error,'Predicate for unsat core is not existentially quantified~n',[]), | |
| 2973 | POut = TExpr). | |
| 2974 | ||
| 2975 | /** | |
| 2976 | Access information about the current version of the ProB core. | |
| 2977 | ||
| 2978 | #### called by: | |
| 2979 | * ProB 2.0: GetInternalRepresentationPrettyPrintCommand | |
| 2980 | */ | |
| 2981 | :- use_module(specfile,[get_internal_representation/1]). | |
| 2982 | get_pretty_print(PP) :- | |
| 2983 | get_internal_representation(PPC), | |
| 2984 | atom_codes(PP,PPC). | |
| 2985 | ||
| 2986 | get_pretty_print_unicode(PP) :- | |
| 2987 | with_translation_mode(unicode,get_pretty_print(PP)). | |
| 2988 | ||
| 2989 | :- use_module(specfile, [get_internal_representation/4]). | |
| 2990 | :- use_module(translate, [set_print_type_infos/1]). | |
| 2991 | :- use_module(bmachine, [b_get_eventb_machine_as_classicalb_codes/3]). | |
| 2992 | /** | |
| 2993 | Pretty-print the machine's internal representation in B syntax. | |
| 2994 | ||
| 2995 | #### called by: | |
| 2996 | * ProB 2.0: GetInternalRepresentationCommand | |
| 2997 | prob2_interface:get_machine_internal_representation([translation_mode(atelierb)],PP). | |
| 2998 | */ | |
| 2999 | get_machine_internal_representation(Options, PP) :- | |
| 3000 | (selectchk(translation_mode(TransMode), Options, Options1) -> true ; TransMode = ascii, Options1 = Options), | |
| 3001 | (selectchk(type_infos(TypeInfos), Options1, Options2) -> true ; TypeInfos = none, Options2 = Options1), | |
| 3002 | Options2 == [], | |
| 3003 | ((TransMode=atelierb ; TransMode=atelierb_pp) -> AdditionalInfo=false, UnsetMinorMode = true | |
| 3004 | ; AdditionalInfo=true, UnsetMinorMode = false), | |
| 3005 | (animation_minor_mode(eventb), TransMode=atelierb | |
| 3006 | -> with_translation_mode(TransMode, b_get_eventb_machine_as_classicalb_codes(_,AdditionalInfo,PPC)) | |
| 3007 | % above will set type infos to true ! | |
| 3008 | ; with_translation_mode(TransMode, get_internal_representation(PPC, AdditionalInfo, UnsetMinorMode, TypeInfos)) | |
| 3009 | ), | |
| 3010 | atom_codes(PP, PPC). | |
| 3011 | ||
| 3012 | ||
| 3013 | ||
| 3014 | % Gets a names of the given operations | |
| 3015 | unpack_operation(ListOfOperation, NamesOfOperations) :- | |
| 3016 | unpack_operation_aux(ListOfOperation, NamesOfOperations). | |
| 3017 | unpack_operation_aux([b(operation(Name, _, _, _))|T], [Name|T1]):- | |
| 3018 | unpack_operation_aux(T, T1). | |
| 3019 | unpack_operation_aux([], []). | |
| 3020 | ||
| 3021 | :- use_module(bmachine, [b_get_machine_operation/4, b_get_machine_operation_for_animation/4, | |
| 3022 | b_get_initialisation_from_machine/2]). | |
| 3023 | get_operations_and_names([b(initialisation(Body))|AllOperations], ['$initialise_machine'|AllNames]) :- | |
| 3024 | findall(b(operation(Name, OutputParameters, InputParameter, Body)), | |
| 3025 | %b_get_machine_operation(Name, OutputParameters, InputParameter, Body), | |
| 3026 | b_get_machine_op_for_anim_with_otype(Name, OutputParameters, InputParameter, Body, _), | |
| 3027 | AllOperations), | |
| 3028 | unpack_operation(AllOperations, AllNames), | |
| 3029 | b_get_initialisation_from_machine(Body, _). | |
| 3030 | ||
| 3031 | ||
| 3032 | :- use_module(symbolic_model_checker(predicate_handling),[prime_predicate/2]). | |
| 3033 | get_primed_predicate(Pred,PrimedPredOut) :- | |
| 3034 | predicate_typecheck_for_eval(Pred,POutT), | |
| 3035 | prime_predicate(POutT,PrimedPred), | |
| 3036 | translate_bexpression(PrimedPred,PrimedPredOut). | |
| 3037 | ||
| 3038 | % Version of get_primed_predicate/2 which does not introduce an existential quantifier. | |
| 3039 | get_nonquantifying_primed_predicate(Pred,PrimedPredOut) :- | |
| 3040 | temporary_set_preference(optimize_ast,false,CHNG1), | |
| 3041 | call_cleanup(get_nonquantifying_primed_predicate_2(Pred,PrimedPredOut), | |
| 3042 | reset_temporary_preference(optimize_ast,CHNG1)). | |
| 3043 | ||
| 3044 | get_nonquantifying_primed_predicate_2(Pred, PrimedPredOut) :- | |
| 3045 | get_eval_scope(Scope), | |
| 3046 | (\+ bmachine:b_machine_is_loaded -> | |
| 3047 | bmachine:b_set_empty_machine % Ensure a machine is loaded someway or another. | |
| 3048 | ; true | |
| 3049 | ), | |
| 3050 | b_type_open_predicate(no_quantifier, Pred, Scope, Typed, Errors), | |
| 3051 | (Errors=[] -> true ; add_error_and_fail(get_primed_predicate, 'Type-Errors: ', Errors)), | |
| 3052 | prime_predicate(Typed, PrimedPred), | |
| 3053 | translate_bexpression(PrimedPred,PrimedPredOut). | |
| 3054 | ||
| 3055 | ||
| 3056 | :- use_module(extrasrc(weakest_preconditions),[weakest_precondition/3]). | |
| 3057 | :- use_module(preferences, [call_with_preference/3]). | |
| 3058 | get_weakest_precondition(OpName,Pred,WPOut) :- | |
| 3059 | % TODO: call with preference can be removed once ProB 2 reads ASTs instead of reparsing | |
| 3060 | call_with_preference(get_weakest_precondition_aux(OpName,Pred,WPOut),translate_ids_to_parseable_format,true). | |
| 3061 | get_weakest_precondition_aux(OpName,Pred,WPOut) :- | |
| 3062 | b_get_machine_operation(OpName,_Results,_Parameters,OpBody), | |
| 3063 | predicate_typecheck_for_eval(Pred,POutT), | |
| 3064 | weakest_precondition(OpBody,POutT,WP), | |
| 3065 | translate_bexpression(WP,WPOut). | |
| 3066 | ||
| 3067 | :- use_module(extrasrc(before_after_predicates),[before_after_predicate_for_operation/2]). | |
| 3068 | before_after_predicate(OpName,PredicateOut) :- | |
| 3069 | call_with_preference(before_after_predicate_aux(OpName,PredicateOut),translate_ids_to_parseable_format,true). | |
| 3070 | before_after_predicate_aux(OpName,PredicateOut) :- | |
| 3071 | before_after_predicate_for_operation(OpName,Predicate), | |
| 3072 | translate_bexpression(Predicate,PredicateOut). | |
| 3073 | ||
| 3074 | /** Synthesis Commands: | |
| 3075 | * | |
| 3076 | #### b_synthesis:start_synthesis_from_ui/13 called by: | |
| 3077 | * ProB 2.0: BSynthesisCommand | |
| 3078 | */ | |
| 3079 | start_synthesis_from_ui_(SynthesisMode,AdaptMachineCode,SolverTimeOut,Library,DoNotUseConstants,Solver,ConsiderIfVarNames,Operation,SynthesisType,Positive,Negative,NewMachineAtom,Distinguishing) :- | |
| 3080 | start_synthesis_from_ui(SynthesisMode,AdaptMachineCode,SolverTimeOut,Library,DoNotUseConstants,Solver,ConsiderIfVarNames,Operation,SynthesisType,Positive,Negative,NewMachineAtom,Distinguishing). | |
| 3081 | ||
| 3082 | /* | |
| 3083 | #### b_synthesis:start_synthesis_single_operation_from_ui/11 called by: | |
| 3084 | * BSynthesis: StartSynthesisCommand | |
| 3085 | */ | |
| 3086 | start_synthesis_single_operation_from_ui_(SolverTimeOut,Operations,Library,DoNotUseConstants,Solver,Operation,action,Positive,Negative,CacheOperationTuple,Distinguishing) :- | |
| 3087 | start_synthesis_single_operation_from_ui(SolverTimeOut,Operations,Library,DoNotUseConstants,Solver,Operation,action,Positive,Negative,CacheOperationTuple,Distinguishing). | |
| 3088 | ||
| 3089 | /* | |
| 3090 | #### b_synthesis:reset_synthesis_context/0 called by: | |
| 3091 | * ProB 2.0: ResetBSynthesisCommand | |
| 3092 | */ | |
| 3093 | reset_synthesis_context_ :- reset_synthesis_context. | |
| 3094 | ||
| 3095 | /* | |
| 3096 | #### synthesis_util:get_invariant_violating_vars_from_examples/3 called by: | |
| 3097 | * BSynthesis: GetViolatingVarsFromExamples | |
| 3098 | */ | |
| 3099 | get_invariant_violating_vars_from_examples_(Positive,Negative,ViolatingVarNames) :- | |
| 3100 | get_invariant_violating_vars_from_examples(Positive,Negative,ViolatingVarNames). | |
| 3101 | ||
| 3102 | /* | |
| 3103 | #### synthesis_util:get_valid_and_invalid_equality_predicates_for_operation/6 called by: | |
| 3104 | * BSynthesis: VisualizeOperationCommand | |
| 3105 | */ | |
| 3106 | get_valid_and_invalid_equality_predicates_for_operation_(OperationName,ValidAmount,InvalidAmount,ValidPrettyEqualityTuples,InvalidPrettyEqualities,IgnoredIDs) :- | |
| 3107 | get_valid_and_invalid_equality_predicates_for_operation(OperationName,ValidAmount,InvalidAmount,ValidPrettyEqualityTuples,InvalidPrettyEqualities,IgnoredIDs). | |
| 3108 | ||
| 3109 | /* | |
| 3110 | #### synthesis_util:get_valid_and_invalid_equality_predicates_for_invariants/4 called by: | |
| 3111 | * BSynthesis: VisualizeInvariantsCommand | |
| 3112 | */ | |
| 3113 | get_valid_and_invalid_equality_predicates_for_invariants_(ValidAmount,InvalidAmount,ValidPrettyEqualities,InvalidPrettyEqualities) :- | |
| 3114 | get_valid_and_invalid_equality_predicates_for_invariants(ValidAmount,InvalidAmount,ValidPrettyEqualities,InvalidPrettyEqualities). | |
| 3115 | ||
| 3116 | /* | |
| 3117 | #### synthesis_util:adapt_machine_code_for_operations/2 called by: | |
| 3118 | * BSynthesis: AdaptMachineCodeForOperationsCommand | |
| 3119 | */ | |
| 3120 | adapt_machine_code_for_operations_(Operations,NewMachineAtom) :- | |
| 3121 | adapt_machine_code_for_operations(Operations,NewMachineAtom). | |
| 3122 | ||
| 3123 | /* | |
| 3124 | #### predicate_data_generator:generate_synthesis_data_from_predicate_untyped_/5 called by: | |
| 3125 | * BSynthesisDataGenerator: SynthesisDataFromPredicateCommand | |
| 3126 | */ | |
| 3127 | generate_synthesis_data_from_predicate_untyped_(MachinePath, AugmentRecords, SolverTimeoutMs, UntypedPredAst, AugmentedSetOfData) :- | |
| 3128 | generate_synthesis_data_from_predicate_untyped(MachinePath, AugmentRecords, SolverTimeoutMs, UntypedPredAst, AugmentedSetOfData). | |
| 3129 | ||
| 3130 | /* | |
| 3131 | #### operation_data_generator:generate_operation_data_from_machine_path_/4 called by: | |
| 3132 | * BSynthesisDataGenerator: SynthesisDataFromOperationCommand | |
| 3133 | */ | |
| 3134 | generate_operation_data_from_machine_path_(MachinePath, AugmentRecords, SolverTimeoutMs, OperationData) :- | |
| 3135 | generate_operation_data_from_machine_path(MachinePath, AugmentRecords, SolverTimeoutMs, OperationData). | |
| 3136 | ||
| 3137 | /* | |
| 3138 | #### operation_data_generator:generate_data_from_machine_operation_/6 called by: | |
| 3139 | * BSynthesisDataGenerator: SynthesisDataFromOperationCommand | |
| 3140 | */ | |
| 3141 | generate_data_from_machine_operation_(OperationName, Augmentations, SolverTimeoutMs, AbsoluteFilePath, MachineName, OperationData) :- | |
| 3142 | generate_data_from_machine_operation(OperationName, Augmentations, SolverTimeoutMs, AbsoluteFilePath, MachineName, OperationData). | |
| 3143 | ||
| 3144 | /* | |
| 3145 | #### called by: | |
| 3146 | * ProB 2.0: GetMachineOperationNamesCommand | |
| 3147 | */ | |
| 3148 | :- use_module(probcspsrc(haskell_csp),[channel/2]). | |
| 3149 | ||
| 3150 | csp_channel_or_start('start_cspm_MAIN'). | |
| 3151 | csp_channel_or_start('start_cspm'). % TO DO: do we also need to support print channel ? | |
| 3152 | csp_channel_or_start(Name) :- channel(Name,_). | |
| 3153 | ||
| 3154 | get_machine_operation_names(MachineOperationNames) :- b_or_z_mode,!, | |
| 3155 | findall(MachineOperationName,b_is_operation_name(MachineOperationName),MachineOperationNames). | |
| 3156 | get_machine_operation_names(ChannelNames) :- csp_mode,!, | |
| 3157 | findall(Name, csp_channel_or_start(Name),ChannelNames). | |
| 3158 | get_machine_operation_names([]). | |
| 3159 | ||
| 3160 | :- use_module(probsrc(bsyntaxtree), [get_texpr_id/2]). | |
| 3161 | :- use_module(probsrc(bmachine),[b_get_operation_non_det_modifies/2, b_get_operation_normalized_read_write_info/3]). | |
| 3162 | % get list of operation info terms of the form | |
| 3163 | % operation_info(Name,ResultNames,ParameterNames,TopLevel,OType) | |
| 3164 | % where ResultNames and ParameterNames are list of atomic names | |
| 3165 | % TopeLevel is true if the operation is a top-level operation for animation/model checking | |
| 3166 | % OType is classic, csp or eventb_operation %was eventb_operation(ChangeSet,ParaValues,Operation) | |
| 3167 | get_machine_operation_infos(MachineOperationInfos) :- b_or_z_mode,!, | |
| 3168 | % TODO: ensure that we do not need to consider preference(show_eventb_any_arguments,EVENTB) | |
| 3169 | % TODO: examine what happens for CSP||B | |
| 3170 | findall(operation_info(Name,ResultNames,ParameterNames,TopLevel,OTypeF,Read,Modified,NonDetModifies), | |
| 3171 | (b_get_machine_op_for_anim_with_otype(Name, Results, AnimParameters,_, OType), | |
| 3172 | maplist(get_texpr_id,Results,ResultNames), | |
| 3173 | maplist(get_texpr_id,AnimParameters,ParameterNames), | |
| 3174 | functor(OType,OTypeF,_), | |
| 3175 | % TO DO: obtain machine file or machine name | |
| 3176 | (b_top_level_operation(Name) -> TopLevel = true ; TopLevel=false), | |
| 3177 | (b_get_operation_normalized_read_write_info(Name,OpRead,Modified) | |
| 3178 | -> exclude(op_id,OpRead,Read) | |
| 3179 | % exclude query operations called in expressions (allow_operation_calls_in_expr); | |
| 3180 | %ProB2 Java cannot deal with it and raises exception for non-atomic identifiers | |
| 3181 | ; Read=unknown,Modified=unknown | |
| 3182 | ), | |
| 3183 | (b_get_operation_non_det_modifies(Name,NonDetModifies) -> true ; NonDetModifies=unknown) | |
| 3184 | ), | |
| 3185 | MachineOperationInfos). | |
| 3186 | get_machine_operation_infos(ChannelInfos) :- csp_mode,!, | |
| 3187 | findall(operation_info(Name,[],[],true,csp,[],[],[]), csp_channel_or_start(Name),ChannelInfos). | |
| 3188 | get_machine_operation_infos([]). | |
| 3189 | ||
| 3190 | % get the operation for animation (possibly lifting ANY identifiers to paramaters) and returning OType | |
| 3191 | b_get_machine_op_for_anim_with_otype(Name, Results, AnimParameters, AnimBody, OType) :- | |
| 3192 | b_get_machine_operation(Name, _Results, _RealParameters,_RealBody,OType,_OpPos), | |
| 3193 | b_get_machine_operation_for_animation(Name, Results, AnimParameters, AnimBody). | |
| 3194 | ||
| 3195 | :- use_module(library(lists)). | |
| 3196 | %%Same as untyped | |
| 3197 | get_machine_operation_infos_typed(MachineOperationInfos) :- b_or_z_mode,!, | |
| 3198 | % TODO: ensure that we do not need to consider preference(show_eventb_any_arguments,EVENTB) | |
| 3199 | % TODO: examine what happens for CSP||B | |
| 3200 | findall(operation_info(Name,ResultNames,ParameterNames,TopLevel,OTypeF,Read,Modified,NonDetModifies, TypeMap), | |
| 3201 | (b_get_machine_op_for_anim_with_otype(Name, Results, AnimParameters,_, OType), | |
| 3202 | ||
| 3203 | maplist(get_texpr_id,Results,ResultNames), | |
| 3204 | maplist(get_texpr_type, Results,ResultTypes), | |
| 3205 | keys_and_values(ResultMap, ResultNames, ResultTypes), | |
| 3206 | maplist(get_texpr_id,AnimParameters,ParameterNames), | |
| 3207 | maplist(get_texpr_type, AnimParameters,ParameterTypes), | |
| 3208 | keys_and_values(ParameterMap, ParameterNames, ParameterTypes), | |
| 3209 | ||
| 3210 | functor(OType,OTypeF,_), | |
| 3211 | % TO DO: obtain machine file or machine name | |
| 3212 | (b_top_level_operation(Name) -> TopLevel = true ; TopLevel=false), | |
| 3213 | (b_get_operation_normalized_read_write_info(Name,OpRead,Modified) | |
| 3214 | -> exclude(op_id,OpRead,Read), | |
| 3215 | get_constants_type(OpRead, ConstReadType), | |
| 3216 | get_variable_type(OpRead, VarReadType), % TO DO: ids appear multiple times in TypeMap if read and written | |
| 3217 | get_variable_type(Modified, ModifiedType), | |
| 3218 | append([ConstReadType, VarReadType, ModifiedType], VarMap) | |
| 3219 | % exclude query operations called in expressions (allow_operation_calls_in_expr); | |
| 3220 | %ProB2 Java cannot deal with it and raises exception for non-atomic identifiers | |
| 3221 | ; Read=unknown,Modified=unknown, | |
| 3222 | VarMap = [] | |
| 3223 | ), | |
| 3224 | (b_get_operation_non_det_modifies(Name,NonDetModifies) | |
| 3225 | -> maplist(b_is_variable, NonDetModifies, NonDetModifiesType), | |
| 3226 | keys_and_values(NonDetModifiedMap, NonDetModifies, NonDetModifiesType) | |
| 3227 | ; NonDetModifies=unknown, | |
| 3228 | NonDetModifiedMap = [] | |
| 3229 | ), | |
| 3230 | append([ResultMap, ParameterMap, VarMap, NonDetModifiedMap], TypeMap) | |
| 3231 | ), | |
| 3232 | MachineOperationInfos). | |
| 3233 | get_machine_operation_infos_typed(ChannelInfos) :- csp_mode,!, | |
| 3234 | findall(operation_info(Name,[],[],true,csp,[],[],[],[]), csp_channel_or_start(Name),ChannelInfos). | |
| 3235 | get_machine_operation_infos_typed([]). | |
| 3236 | ||
| 3237 | %% note exclude return the elements where the predicate is not succesful | |
| 3238 | get_constants_type(ConstList, Map) :- | |
| 3239 | exclude(b_is_variable, ConstList, Filtered), | |
| 3240 | maplist(b_is_constant, Filtered, Types), | |
| 3241 | keys_and_values(Map, Filtered, Types). | |
| 3242 | ||
| 3243 | get_variable_type(VarList, Map) :- | |
| 3244 | exclude(b_is_constant, VarList, Filtered), | |
| 3245 | maplist(b_is_variable, Filtered, Types), | |
| 3246 | keys_and_values(Map, Filtered, Types). | |
| 3247 | ||
| 3248 | op_id(op(_)). | |
| 3249 | ||
| 3250 | ||
| 3251 | :- use_module(bmachine,[b_filenumber/4, get_machine_identifiers/2, get_machine_identifiers_with_pp_type/2]). | |
| 3252 | ||
| 3253 | get_all_spec_identifiers(SortedAllIDs) :- | |
| 3254 | get_spec_identifiers2(AllIDs), | |
| 3255 | sort(AllIDs,SortedAllIDs). | |
| 3256 | ||
| 3257 | :- use_module(probcspsrc(haskell_csp),[get_cspm_identifier/2]). | |
| 3258 | get_spec_identifiers2(AllIDs) :- b_or_z_mode, !, | |
| 3259 | findall(ID,get_machine_identifiers_with_pp_type(_,ID),LIds), append(LIds,AllIDs). | |
| 3260 | get_spec_identifiers2(AllIDs) :- csp_mode,!, | |
| 3261 | findall([ID,''],get_cspm_identifier(_,ID),AllIDs). | |
| 3262 | get_spec_identifiers2([]). | |
| 3263 | ||
| 3264 | % get a list of all machine files: TO DO: extend for CSP, Alloy, TLA... | |
| 3265 | get_machine_files(Files) :- | |
| 3266 | findall(b_file(Name,Extension,Filename),b_filenumber(Name,Extension,_,Filename), Files). | |
| 3267 | % TODO: add .cfg file for TLA+ if it exists | |
| 3268 | ||
| 3269 | % a predicate to obtain possible identifier completions for current machine: | |
| 3270 | :- use_module(tools_matching,[fuzzy_match_codes_lower_case/2, codes_to_lower_case/2, get_current_expr_keywords/1, | |
| 3271 | get_current_keywords/1, get_all_svg_attributes/1, | |
| 3272 | is_svg_color_name/1, get_all_dot_attributes/1]). | |
| 3273 | get_possible_completions(ID,_Options,Completions) :- | |
| 3274 | special_id_match_pattern(ID,Category,IDSuffix),!, % treat things like svg$stro -> complete to stroke without $svg | |
| 3275 | get_possible_completions(IDSuffix,[keywords(Category),lower_case],Completions). | |
| 3276 | get_possible_completions(ID,Options,Completions) :- | |
| 3277 | get_match_ids(Options,SortedAllIDs), | |
| 3278 | atom_codes(ID,IDCodes0), | |
| 3279 | (member(lower_case,Options) -> codes_to_lower_case(IDCodes0,IDCodes), Opt=lower_case | |
| 3280 | ; Opt=case_sensitive, IDCodes = IDCodes0), | |
| 3281 | findall([Target,Type,Kind],(member([Target,Type,Kind],SortedAllIDs),atom_codes(Target,TargetCodes), | |
| 3282 | match(Opt,IDCodes,TargetCodes)),Completions0), | |
| 3283 | (member(latex_to_unicode,Options), | |
| 3284 | atom_concat('\\',Latex,ID), | |
| 3285 | latex_to_unicode(Latex,Unicode) | |
| 3286 | -> ord_union([[Unicode,Latex,unicode]],Completions0,Completions1) | |
| 3287 | ; Completions1=Completions0 | |
| 3288 | ), | |
| 3289 | (member(ascii_to_unicode,Options), | |
| 3290 | ascii_to_unicode(ID,Unicode2) | |
| 3291 | -> ord_union([[Unicode2,ID,unicode]],Completions1,Completions2) | |
| 3292 | ; Completions2=Completions1 | |
| 3293 | ), | |
| 3294 | maplist(completion_add_backquotes_if_required,Completions2,Completions). % only in classical_b_mode? | |
| 3295 | ||
| 3296 | special_id_match_pattern(ID,Category,IDSuffix) :- atom_codes(ID,Codes), | |
| 3297 | category_pattern(Pattern,Category), | |
| 3298 | append(Pattern,SuffixCodes,Codes), | |
| 3299 | atom_codes(IDSuffix,SuffixCodes). | |
| 3300 | ||
| 3301 | category_pattern("$",special_categories_only). | |
| 3302 | category_pattern("col$",svg_colors_only). | |
| 3303 | category_pattern("dot$",dot_only). | |
| 3304 | category_pattern("svg$",svg_only). | |
| 3305 | category_pattern("tex$",latex_only). | |
| 3306 | % TODO: maybe find better patter svg:: and support other categories like dot, ext, ... | |
| 3307 | ||
| 3308 | get_all_special_categories(L) :- findall(ID, (category_pattern(Cs,_),atom_codes(ID,Cs)),L). | |
| 3309 | ||
| 3310 | % this is not very efficient; | |
| 3311 | % general check for all completions is not sufficient and leads to incorrect backquotes, e.g., for pragmas: `@desc` or latex: `\alpha` | |
| 3312 | % backquote check only for svg attributes and identifiers | |
| 3313 | completion_add_backquotes_if_required([Completion,Type,Kind],BQCompletion) :- | |
| 3314 | (Kind = svg; Kind = spec_id), | |
| 3315 | translate:id_requires_escaping(Completion) -> | |
| 3316 | tools:ajoin(['`',Completion,'`'],BQC), BQCompletion = completion(BQC, Type) | |
| 3317 | ; BQCompletion = completion(Completion,Type). | |
| 3318 | ||
| 3319 | ||
| 3320 | :- use_module(tools_lists,[common_prefix_atom/2]). | |
| 3321 | % Kind is either expr, latex or all | |
| 3322 | get_possible_completion(ID,Kind,Completion) :- | |
| 3323 | get_possible_completions(ID,[keywords(Kind)],Completions0), | |
| 3324 | maplist(ignore_type,Completions0,Completions), | |
| 3325 | (select(ID,Completions,C2), C2 \= [] | |
| 3326 | -> true % find a longer prefix in case ID is valid, so that we can find longer and longer completions in the UI | |
| 3327 | ; C2=Completions), | |
| 3328 | common_prefix_atom(C2,Completion). | |
| 3329 | % if Completion=ID we could return the first completion or cycle through them | |
| 3330 | ||
| 3331 | ignore_type(completion(Id,_),Id). | |
| 3332 | ||
| 3333 | match(case_sensitive,Pattern,TargetCodes) :- !, prefix(TargetCodes,Pattern). | |
| 3334 | match(lower_case,Pattern,TargetCodes) :- codes_to_lower_case(TargetCodes,TC2), prefix(TC2,Pattern). | |
| 3335 | ||
| 3336 | get_possible_fuzzy_matches(ID,FuzzyMatches) :- | |
| 3337 | get_match_ids([keywords(expr)],SortedAllIDs), | |
| 3338 | atom_codes(ID,IDCodes), | |
| 3339 | findall(Target,(member([Target,_,_],SortedAllIDs),atom_codes(Target,TargetCodes), | |
| 3340 | fuzzy_match_codes_lower_case(IDCodes,TargetCodes)),FuzzyMatches). | |
| 3341 | ||
| 3342 | :- use_module(library(ordsets),[ord_union/3]). | |
| 3343 | :- use_module(translate,[get_latex_keywords/1, get_latex_keywords_with_backslash/1, ascii_to_unicode/2, latex_to_unicode/2]). | |
| 3344 | get_match_ids(Options,Ids) :- | |
| 3345 | get_match_ids2(Options,Keywords,Kind), | |
| 3346 | maplist(add_id_type_kind(Kind),Keywords,Ids). | |
| 3347 | ||
| 3348 | % provides list [Id, Type, Kind]; Kind: latex, svg, dot, expr, all, spec_id, unicode | |
| 3349 | get_match_ids2(Options,Ids,special) :- member(keywords(special_categories_only),Options),!, | |
| 3350 | get_all_special_categories(Ids). % svg only | |
| 3351 | get_match_ids2(Options,Ids,latex) :- member(keywords(latex_only),Options),!, | |
| 3352 | get_latex_keywords(Ids). % latex only, without leading backslash | |
| 3353 | get_match_ids2(Options,Ids,svg) :- member(keywords(svg_only),Options),!, | |
| 3354 | get_all_svg_attributes(Ids). % svg only | |
| 3355 | get_match_ids2(Options,Ids,dot) :- member(keywords(dot_only),Options),!, | |
| 3356 | get_all_dot_attributes(Ids). | |
| 3357 | get_match_ids2(Options,Ids,svg) :- member(keywords(svg_colors_only),Options),!, | |
| 3358 | findall(Id,is_svg_color_name(Id),Ids). | |
| 3359 | get_match_ids2(Options,Ids,Kind) :- select(keywords(Kind),Options,Options2),!, | |
| 3360 | get_match_ids(Options2,SortedAllIDs), % already adds kinds! | |
| 3361 | (Kind=latex -> get_latex_keywords_with_backslash(Keywords) | |
| 3362 | ; Kind=expr -> get_current_expr_keywords(Keywords) | |
| 3363 | ; Kind=all -> get_current_keywords(Keywords) | |
| 3364 | ; Kind=svg -> get_all_svg_attributes(Keywords) | |
| 3365 | ; add_internal_error('Unknown ids kind:',get_match_ids2(Options,Ids,Kind)), Keywords=[], Kind=unknown | |
| 3366 | ), | |
| 3367 | ord_union(SortedAllIDs,Keywords,Ids). | |
| 3368 | get_match_ids2(_,SortedAllIDs,spec_id) :- get_all_spec_identifiers(SortedAllIDs). | |
| 3369 | ||
| 3370 | add_id_type_kind(Kind,Id,IdType) :- | |
| 3371 | (Kind=latex -> KindInfo = 'LaTeX' | |
| 3372 | ; Kind=svg -> KindInfo = 'SVG attribute' | |
| 3373 | ; Kind=dot -> KindInfo = 'dot attribute' | |
| 3374 | ; KindInfo = ''), | |
| 3375 | (Id = [Id0,Type] -> IdType = [Id0,Type,Kind] | |
| 3376 | ; Id \= [_,_,_] -> IdType = [Id,KindInfo,Kind] | |
| 3377 | ; IdType = Id). | |
| 3378 | ||
| 3379 | % ----------------------- | |
| 3380 | ||
| 3381 | :- use_module(bmachine_static_checks, [extended_static_check_machine/0]). | |
| 3382 | :- use_module(visbsrc(visb_visualiser),[extended_static_check_default_visb_file/0]). | |
| 3383 | /** | |
| 3384 | prob2_extended_static_check(-Problems) | |
| 3385 | */ | |
| 3386 | prob2_extended_static_check(Problems) :- | |
| 3387 | extended_static_check_machine, | |
| 3388 | extended_static_check_default_visb_file, % maybe we should make this optional | |
| 3389 | get_all_errors_with_span_info_and_reset(Problems). | |
| 3390 | ||
| 3391 | :- use_module(wdsrc(well_def_analyser), [analyse_wd_for_machine/3]). | |
| 3392 | /** | |
| 3393 | prob2_check_well_definedness(-NrDischarged,-NrTotal) | |
| 3394 | */ | |
| 3395 | prob2_check_well_definedness(NrDischarged,NrTotal) :- | |
| 3396 | analyse_wd_for_machine(NrDischarged,NrTotal,_). | |
| 3397 | ||
| 3398 | ||
| 3399 | :- use_module(extension('banditfuzz/welldef'), [ensure_wd/2]). | |
| 3400 | :- use_module(probsrc(b_ast_cleanup), [clean_up_pred/3]). | |
| 3401 | prob2_ensure_wd(Pred, Res) :- | |
| 3402 | get_eval_scope(Scope), | |
| 3403 | b_type_open_predicate(no_quantifier,Pred,Scope,TPred,Errors), | |
| 3404 | (Errors=[] -> true ; add_error_and_fail(prob2_ensure_wd, 'Type-Errors: ', Errors)), | |
| 3405 | clean_up_pred(TPred, [], PreCleaned), | |
| 3406 | ensure_wd(PreCleaned, WdPred), | |
| 3407 | clean_up_pred(WdPred, [], CleanWd), | |
| 3408 | translate_bexpression(CleanWd,Res). | |
| 3409 | ||
| 3410 | ||
| 3411 | ||
| 3412 | ||
| 3413 | % ----------- | |
| 3414 | :- use_module(visbsrc(visb_visualiser),[load_visb_file/1,get_visb_attributes_for_state/2, | |
| 3415 | get_default_visb_file/2, | |
| 3416 | get_visb_click_events/1, get_visb_hovers/1, get_visb_items/1, | |
| 3417 | get_visb_svg_objects/1, get_visb_default_svg_file_contents/1, | |
| 3418 | perform_visb_click_event/4, | |
| 3419 | visb_file_is_loaded/1, | |
| 3420 | visb_file_is_loaded/3, | |
| 3421 | generate_visb_html_for_history/2, | |
| 3422 | generate_visb_html_for_history_with_vars/1, | |
| 3423 | generate_visb_html_for_current_state/2, | |
| 3424 | generate_visb_html/3, | |
| 3425 | generate_visb_html_codes_for_states/3]). | |
| 3426 | ||
| 3427 | % load a VisB JSon file: this needs to be re-loaded everytime a new model is loaded or re-loaded | |
| 3428 | prob2_load_visb_file(JSonFile) :- | |
| 3429 | load_visb_file(JSonFile). | |
| 3430 | ||
| 3431 | % Check whether a non-empty VisB visualization is currently loaded, and if so, return its path. | |
| 3432 | % This predicate doesn't fail, even when no VisB visualization is loaded or it is empty. | |
| 3433 | prob2_get_loaded_visb_file(Res) :- AllowEmpty=false, | |
| 3434 | (visb_file_is_loaded(JsonFile,_Svg,AllowEmpty) -> Res = json_file(JsonFile) ; Res = none). | |
| 3435 | ||
| 3436 | % return current loaded JSON and SVG file; fail if no VisB file loaded | |
| 3437 | % The ProB Java API only calls this in mode (+JsonFile,-SvgFile). | |
| 3438 | prob2_visb_file_loaded(JsonFile,SvgFile) :- AllowEmpty=true, | |
| 3439 | visb_file_is_loaded(JsonFile,SvgFile,AllowEmpty). | |
| 3440 | ||
| 3441 | % for a given state Id (number) this returns a list with the following entries: | |
| 3442 | % set_attr(SVGId,Attr,Value) -> the attribute Attr of the SVG object with the id SVGId should be set to Value | |
| 3443 | prob2_visb_attributes_for_state(StateID,List) :- %start_ms_timer(T1), | |
| 3444 | set_current_state(StateID), % ensure external functions like ENABLED are evaluated in correct state | |
| 3445 | get_visb_attributes_for_state(StateID,List). | |
| 3446 | %, stop_ms_walltimer_with_msg(T1,visb_state(StateID)). | |
| 3447 | ||
| 3448 | % this returns two lists with the following entries: | |
| 3449 | % execute_event(SVGId,Event,Predicates): when clicking on SVG object with id SVGId one should execute | |
| 3450 | % the B event Event with the given list of predicates | |
| 3451 | % hover(OriginID,OtherID,Attr,EnterVal,ExitVal): when hovering over the SVG Object with id OriginID | |
| 3452 | % the hover should set the attribute Attr of the object OtherID to the value EnterVal, | |
| 3453 | % and reset it to ExitVal upon leaving | |
| 3454 | % Currently hovers do not take the current state into account; this may change in future | |
| 3455 | prob2_visb_click_events_and_hovers(Events,Hovers) :- | |
| 3456 | get_visb_click_events(Events), | |
| 3457 | get_visb_hovers(Hovers). | |
| 3458 | ||
| 3459 | % try and perform a click; if successful returning a list of transition ids to be performed | |
| 3460 | % if the visb_event is disabled it returns an empty list | |
| 3461 | % if no visb_event is associated with SvgID it fails | |
| 3462 | % MetaInfoList can contain infos about shiftKey, pageX, pageY infos of the click | |
| 3463 | prob2_visb_perform_click(SvgID,MetaInfoList,StateId,Transitions) :- | |
| 3464 | (perform_visb_click_event(SvgID,MetaInfoList,StateId,TransIDS) | |
| 3465 | -> trace_to_op_terms(TransIDS,StateId,Transitions) | |
| 3466 | ; add_message(prob2_interface,'VisB ID has no event: ',SvgID), | |
| 3467 | Transitions=[] | |
| 3468 | ). | |
| 3469 | ||
| 3470 | % this returns a list with the following entries: visb_item(SvgID,Attr,FormulaText,Desc,PositionTerm) | |
| 3471 | prob2_visb_items(Items) :- | |
| 3472 | get_visb_items(Items). | |
| 3473 | ||
| 3474 | prob2_read_visb_path_from_definitions(Path) :- | |
| 3475 | get_default_visb_file(Path,_) -> true; Path = none. | |
| 3476 | ||
| 3477 | prob2_visb_svg_objects(Objects) :- get_visb_svg_objects(Objects). | |
| 3478 | ||
| 3479 | prob2_visb_default_svg_file_contents(Atom) :- | |
| 3480 | get_visb_default_svg_file_contents(Codes), | |
| 3481 | atom_codes(Atom,Codes). | |
| 3482 | ||
| 3483 | prob2_export_visb_html_for_history(TransIDS, File) :- | |
| 3484 | try_set_trace_by_transition_ids(TransIDS), | |
| 3485 | generate_visb_html_for_history_with_vars(File). | |
| 3486 | prob2_export_visb_html_for_history(TransIDS,Options,File) :- | |
| 3487 | try_set_trace_by_transition_ids(TransIDS), | |
| 3488 | generate_visb_html_for_history(File,Options). | |
| 3489 | ||
| 3490 | prob2_export_visb_for_current_state(File) :- | |
| 3491 | generate_visb_html_for_current_state(File,[]). | |
| 3492 | prob2_export_visb_html_for_states(StateIds,File,Options) :- | |
| 3493 | generate_visb_html(StateIds,File,Options). | |
| 3494 | prob2_get_visb_html_for_states(StateIds,Options,HTMLAtom) :- | |
| 3495 | generate_visb_html_codes_for_states(StateIds,[id_namespace_prefix(auto)|Options],CodesList), | |
| 3496 | atom_codes(HTMLAtom,CodesList). | |
| 3497 | ||
| 3498 | :- use_module(probsrc(b_intelligent_trace_replay),[replay_json_trace_file/5]). | |
| 3499 | % replay a JSON trace file, Status can be perfect, imperfect(Grade), partial | |
| 3500 | % TransitionIDList can be used to replay the trace from root | |
| 3501 | % MatchInfoList is a list of replay_step(MatchInfo,ErrorList) term for all matches | |
| 3502 | % MatchInfo can be perfect, params_and_results, parameters_only... | |
| 3503 | prob2_replay_json_trace_file(File,ReplayStatus,Trace,MatchInfoList) :- | |
| 3504 | replay_json_trace_file(File,_,ReplayStatus,TransIds,MatchInfoList), | |
| 3505 | trace_to_op_terms(TransIds, root, Trace). | |
| 3506 | ||
| 3507 | ||
| 3508 | % used in prob_java for TLC4B option -constantssetup | |
| 3509 | get_constants_predicate(Predicate) :- | |
| 3510 | get_preference(maxNrOfEnablingsPerOperation,MaxO), | |
| 3511 | tcltk_interface:tcltk_get_constants_predicate(Predicate,MaxO). | |
| 3512 | ||
| 3513 | % get dest state id from a state trace file, e.g. <<name>>.tla.trace generated by TLC4B | |
| 3514 | replay_state_trace_from_file(File,ID,DestID) :- | |
| 3515 | (state_space:current_state_id(ID) -> true | |
| 3516 | ; state_space:state_space_reset, | |
| 3517 | (ID = root -> true | |
| 3518 | ; tcltk_interface:find_shortest_trace_to_node(root,ID,_OpIDs,TraceIDs), | |
| 3519 | try_set_trace_by_transition_ids(TraceIDs))), % allow replay of multiple TLC counter example traces in ProB2-UI; maybe there is a better solution? | |
| 3520 | b_trace_checking:tcltk_check_state_sequence_from_file_state_id(File,ID,DestID). |