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