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 virtual_time_out_for_node/1, 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(virtual_timeout_occurred,StateId) :- virtual_time_out_for_node(StateId).
1281 state_property2(max_operations_reached,StateId) :- max_operations_reached(StateId).
1282 state_property2(valid_state,StateId) :- visited_expression_id(StateId).
1283 state_property2(constants_set_up,StateId) :- is_constants_set_up_state(StateId).
1284 state_property2(initialised,StateId) :-
1285 (specfile:csp_mode ->
1286 true % in CSP the content of the state is irrelevant for the semantic of the state space
1287 ; is_initialised_state(StateId)
1288 ).
1289
1290
1291 /**
1292 prob2_get_state_errors(+StateId,-Errors)
1293
1294 Takes a id for a given state in the state space and produces a list of all
1295 state based errors.
1296
1297 #### called by:
1298 * ProB 2.0: GetStateBasedErrorsCommand
1299 */
1300 prob2_get_state_errors(StateId,Errors) :-
1301 findall(E, (state_error(StateId,_,Error), convert_error(Error,E)), Errors).
1302
1303 :- use_module(error_manager,[extract_span_description/2]).
1304 convert_error(invariant_violated,_) :- !, fail.
1305 convert_error(eventerror(Event,EError,Trace),error([event(Event),description(Short),long_description(Long)])) :-
1306 !,
1307 translate_event_error(EError,Short),
1308 explain_event_trace(Trace,LongStr,_Span),
1309 safe_atom_codes(Long,LongStr).
1310 convert_error(Error,error([description(Short),long_description(Long)|Tail])) :-
1311 translate_state_error(Error,Short),
1312 explain_state_error(Error,Span,LongStr),
1313 safe_atom_codes(Long,LongStr),
1314 % TODO Also return Span as structured error locations, not just a text description
1315 (extract_span_description(Span,SDescr) ->
1316 Tail = [span_description(SDescr)]
1317 ;
1318 Tail = []
1319 ).
1320
1321 /* ------------------------- */
1322 /* Evaluate Formulas */
1323 /* ------------------------- */
1324
1325 % term in string (see String argument) should be terminated by full-stop!!!
1326 evaluate_csp_expression_string(PlClause,R) :-
1327 read_from_codes(PlClause,PlTerm),
1328 evaluate_csp_expression_aux(PlTerm,R).
1329
1330 :- use_module(probcspsrc(haskell_csp), [evaluate_parsed_csp_expression_with_timing/2]).
1331 evaluate_csp_expression_aux(PlTerm,R) :-
1332 evaluate_parsed_csp_expression_with_timing(PlTerm,Res),
1333 translate:translate_cspm_expression(Res, R).
1334 evaluate_csp_expression_aux(Other,_R) :-
1335 add_error_and_fail(prob2_interface, 'Unexpected CSP Expression: ', Other).
1336
1337 :- assert_must_succeed((X=identifier(none,x),
1338 prob2_evaluate_formulas(
1339 [bexpr(comprehension_set(none,[X],greater(none,mult_or_cart(none,X,X),integer(none,2))))],
1340 [state(root)],
1341 Res
1342 ),
1343 Res = [result(Str,[],_)],
1344 atom_codes(Str,Codes),
1345 (phrase("/*@symbolic*/ ",Codes,C2) -> true ; C2=Codes),
1346 (phrase("{x\x2223\x * x > 2}", C2) ; % string below but with Rodin bar symbol
1347 phrase("{x|x * x > 2}", C2)))).
1348
1349 /**
1350 prob2_evaluate_formulas(+Formulas, +Options, -Results)
1351
1352 Evaluate a list of formulas.
1353 This is more efficient than evaluating each formula individually,
1354 because some calculations (e. g. expanding the current state) don't have to be repeated for each formula.
1355
1356 Supported formula types:
1357 * bpred(Raw)
1358 * bexpr(Raw)
1359 * csp(TermCodes)
1360
1361 Supported options:
1362 * all options supported by parse_eval_opts/3
1363 * all options supported by parse_pp_opts/3
1364
1365 Possible results:
1366 * result(Value,Solutions,Errors): evaluation succeeded
1367 * Value: String rep of the value calculated by ProB
1368 * Solutions: List of solutions as a triple: bind(Name,PPSol)
1369 * Name: Free variable from formula
1370 * PPSol: String representation of the solution bound to the name
1371 * Errors: List of error/3 terms for non-fatal errors (warnings or messages) that occurred during evaluation
1372 * errors(Value,Errors): Typechecking or evaluation failed
1373 * Value: Short description of error type (e. g. 'NOT-WELL-DEFINED', 'UNKNOWN')
1374 * Errors: List of error/3 terms for all errors that occurred
1375 * enum_warning: An enumeration warning was thrown during evaluation
1376 */
1377 prob2_evaluate_formulas(Formulas, Options, Results) :-
1378 parse_eval_opts(EvalOpts, Options, Options1),
1379 set_default_eval_opts(EvalOpts),
1380 EvalOpts = eval_opts(StateId,ProvideLets,_,_),
1381 parse_pp_opts(PPOpts,Options1,[]),
1382 % useful for certain external functions in LibraryMeta.def, e.g., ENABLED, EVAL_OVER_HISTORY, CHANGED, ...:
1383 set_current_state_for_external_fun(StateId),
1384 call_cleanup(
1385 (get_bstate_with_deferred_sets_for_formulas(StateId,Formulas,ProvideLets,State,StateKind),
1386 % _Machine is shared across all calls so that full_b_machine only needs to be computed once.
1387 maplist(evaluate_formula_in_state(EvalOpts,PPOpts,StateKind,State,_Machine),Formulas,Results)
1388 ),
1389 clear_state_for_external_fun).
1390
1391 evaluate_formula_in_state(EvalOpts, PPOpts, StateKind, State, Machine, Formula, Result) :-
1392 evaluate_formula_in_state_aux(Formula, EvalOpts, PPOpts, StateKind, State, Machine, Result).
1393
1394 evaluate_formula_in_state_aux(csp(Raw), _EvalOpts, _PPOpts, _StateKind, _State, _Machine, R) :- !,
1395 ( evaluate_csp_expression_string(Raw,Res) ->
1396 R = result(Res,[],[]);
1397 R = errors('UNKNOWN',[error('Unexpected CSP Expression',internal_error,[])])).
1398 evaluate_formula_in_state_aux(registered(FormulaID), EvalOpts, PPOpts, StateKind, State, _Machine, R) :-
1399 !,
1400 (prob2_formula(FormulaID, Typed, Requirements) ->
1401 evaluate_typechecked_b_formula_in_state(StateKind, Requirements, State, Typed, EvalOpts, PPOpts, R)
1402 ;
1403 R = errors('ERROR', [error('No formula registered with this UUID',internal_error,[])])
1404 ).
1405 evaluate_formula_in_state_aux(Formula, EvalOpts, PPOpts, StateKind, State, Machine, R) :-
1406 %logger:writeln_log_time(typechecking_raw(PredOrExpr)),
1407 (formula_typecheck_for_eval(Formula,EvalOpts,Machine,Typed) ->
1408 %logger:writeln_log_time(evaluate_typechecked_b_formula_in_state(StateKind)),
1409 %print('EVAL:'),nl,translate:print_bexpr(Typed),nl,
1410 evaluate_typechecked_b_formula_in_state(StateKind,formula(Typed),State,Typed,EvalOpts,PPOpts,R)
1411 ;
1412 get_all_errors_with_span_info_and_reset(Errors),
1413 R = errors('ERROR',Errors)
1414 ).
1415
1416 :- use_module(eval_let_store, [extend_state_with_stored_lets/2]).
1417 % Kind is empty_state, constants_only_state, full_initialised_state
1418 get_bstate_with_deferred_sets_for_formulas(StateId,Formulas,ProvideLets,State,Kind) :-
1419 (Formulas=[_], % we have a single untyped formula
1420 StateId \= root, \+ is_concrete_constants_state_id(StateId) % otherwise get_state_for_b_formula will raise error
1421 -> Kind = not_yet_obtained, % obtain state later, after formula has been type checked and we know what it needs
1422 State = lazy_get_state(StateId,ProvideLets)
1423 ; get_bstate_with_deferred_sets(StateId,ProvideLets,State,Kind)
1424 ).
1425 get_bstate_with_deferred_sets(StateId,ProvideLets,State,Kind) :-
1426 get_state_with_kind(StateId, State1,Kind,_CstID),
1427 add_prob_deferred_set_elements_to_store(State1, State2, visible),
1428 (ProvideLets = true -> extend_state_with_stored_lets(State2, State) ; State = State2).
1429
1430 get_bstate_with_deferred_sets_for_b_formula(StateId,TypedFormula,ProvideLets,State) :-
1431 get_state_for_b_formula(StateId,TypedFormula,State1),
1432 add_prob_deferred_set_elements_to_store(State1, State2, visible),
1433 (ProvideLets = true -> extend_state_with_stored_lets(State2, State) ; State = State2).
1434
1435 /**
1436 prob2_get_formula_type(+Formula,-PPType,-Errors)
1437
1438 Type checks the given untyped formula to determine its type and any type errors.
1439
1440 #### Params:
1441 * Formula - bexpr(Raw) or bpred(Raw), where Raw is the Prolog representation of non-typechecked expression or predicate
1442 * PPType - pretty-printed type of formula
1443 * Errors - any errors that have occured during typechecking
1444
1445 #### called by:
1446 ProB 2.0: FormulaTypecheckCommand
1447 */
1448 prob2_get_formula_type(Formula,PPType,Errors) :-
1449 default_eval_opts(EvalOpts),
1450 formula_typecheck2_for_eval(Formula,EvalOpts,_,TypedFormula,PErrors),
1451 add_all_perrors(PErrors),
1452 get_texpr_type(TypedFormula,Type),
1453 translate:pretty_type(Type,PPType),
1454 get_all_errors_with_span_info_and_reset(Errors).
1455
1456 formula_typecheck_for_eval(Formula,EvalOpts,M,TypedFormula) :-
1457 formula_typecheck2_for_eval(Formula,EvalOpts,M,TypedFormula,PErrors),
1458 add_all_perrors(PErrors),
1459 no_real_perror_occurred(PErrors).
1460
1461 % this predicate returns the internal Prolog type:
1462 %! formula_typecheck2_for_eval(+PredOrExpr,+EvalOpts,?Machine,+RawFormula,-TypedFormula,-Type,-Errors)
1463 formula_typecheck2_for_eval(bpred(Raw),EvalOpts,M,Typed,PErrors) :-
1464 !, predicate_typecheck_for_eval(M,Raw,EvalOpts,Typed,PErrors).
1465 formula_typecheck2_for_eval(bexpr(Raw),EvalOpts,M,Typed,PErrors) :-
1466 !, expression_typecheck_for_eval(M,Raw,EvalOpts,Typed,PErrors).
1467 formula_typecheck2_for_eval(Else,_,_M,_Typed,_PErrors) :-
1468 add_error_and_fail(prob2_interface,'Unsupported formula term:', Else),fail.
1469
1470 predicate_typecheck_for_eval(Raw,Typed) :-
1471 predicate_typecheck_for_eval(_,Raw,Typed).
1472 predicate_typecheck_for_eval(M,Raw,Typed) :-
1473 set_default_eval_opts(EvalOpts),
1474 predicate_typecheck_for_eval(M,Raw,EvalOpts,Typed,PErrors),
1475 add_all_perrors(PErrors),
1476 no_real_perror_occurred(PErrors).
1477 predicate_typecheck_for_eval(M,Raw,EvalOpts,Typed,PErrors) :-
1478 get_eval_scope_with_opts(EvalOpts,Scope), % TODO: pass options
1479 bmachine:b_type_open_predicate_for_full_b_machine(M,open(exists),Raw,Scope,Typed,PErrors).
1480
1481 :- use_module(bmachine,[b_is_variable/2, b_is_constant/2, b_type_expression_for_full_b_machine/6]).
1482 expression_typecheck_for_eval(Raw,Typed) :-
1483 expression_typecheck_for_eval(_,Raw,Typed).
1484 expression_typecheck_for_eval(M,Raw,Typed) :-
1485 set_default_eval_opts(EvalOpts),
1486 expression_typecheck_for_eval(M,Raw,EvalOpts,Typed,PErrors),
1487 add_all_perrors(PErrors),
1488 no_real_perror_occurred(PErrors).
1489 expression_typecheck_for_eval(_,identifier(Pos,ID),_,Typed,PErrors) :-
1490 (b_is_variable(ID,Type) ; b_is_constant(ID,Type)),
1491 !, % hack to avoid type-checking simple identifiers which just need to be looked up in state
1492 PErrors=[], Typed = b(identifier(ID),Type,[nodeid(Pos)]).
1493 expression_typecheck_for_eval(M,Raw,EvalOpts,Typed,PErrors) :-
1494 get_eval_scope_with_opts(EvalOpts,Scope), % TODO: pass options
1495 b_type_expression_for_full_b_machine(M,Raw,Scope,_Type,Typed,PErrors).
1496
1497 :- use_module(eval_let_store,[get_stored_let_typing_scope/1, reset_let_values/0]).
1498
1499 % a more conservative version, only add external libraries if requested
1500 get_eval_scope_with_opts(eval_opts(_,ProvideLets,_,_),Scope) :- !,
1501 (ProvideLets=true -> get_eval_scope_with_opts([provide_stored_let_values],Scope)
1502 ; get_eval_scope_with_opts([],Scope)).
1503 get_eval_scope_with_opts(Options,Scope) :-
1504 (member(provide_stored_let_values,Options),
1505 reset_let_values, % purge all invalid values
1506 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
1507 -> Scope = [Scope1|Scope2]
1508 ; Scope=Scope2),
1509 (member(all_available_libraries,Options) -> get_eval_scope(all,Scope2) ; get_eval_scope(safe,Scope2)).
1510
1511 % get scope for typechecker:
1512 get_eval_scope(Scope) :- get_eval_scope(all,Scope).
1513 get_eval_scope(ExtKind,[prob_ids(visible),Scope,
1514 external_library(Libs)]) :-
1515 % external_library for VisB and Debugging; TODO: should we only make it available in some contexts
1516 % Note: the external_library entries must come after Scope
1517 get_main_eval_scope(Scope),
1518 get_libraries(ExtKind,Libs).
1519 get_main_eval_scope(assertions_scope_and_additional_defs) :-
1520 get_preference(allow_operation_calls_in_expr,true),!.
1521 get_main_eval_scope(variables_and_additional_defs).
1522
1523 get_libraries(all,all_available_libraries).
1524 get_libraries(_,safe_available_libraries).
1525
1526
1527 % TODO Can the evaluation code be integrated with eval_strings again, and/or merged with bvisual2?
1528
1529 :- use_module(tools_meta,[safe_time_out/3]).
1530 % NOTE: This predicate always resets the error manager.
1531 % Any errors, warnings, etc. that occurred will be returned inside Result,
1532 % including any errors that occurred *before* this predicate is called!
1533 evaluate_typechecked_b_formula_in_state(StateKind,Requirements,State,Typed,EvalOpts,PPOpts,Result) :-
1534 ( State=lazy_get_state(StateId,ProvideLets),
1535 get_bstate_with_deferred_sets_for_b_formula(StateId,Typed,ProvideLets,RealState)
1536 % TO DO: we could try and get only those identifiers that are really used
1537 -> evaluate_typechecked_b_formula_in_state(RealState,Typed,EvalOpts,PPOpts,Result)
1538 ; requirements_met(Requirements,StateKind) ->
1539 evaluate_typechecked_b_formula_in_state(State,Typed,EvalOpts,PPOpts,Result)
1540 ;
1541 get_all_errors_with_span_info_and_reset(Errors),
1542 % TODO: extend ProB2 to recognise new error message:
1543 % (Requirements=requires_constants -> EMsg = 'NOT-INITIALISED' ; EMsg = 'CONSTANTS-NOT-SETUP'),
1544 Result = errors('NOT-INITIALISED',Errors)
1545 ).
1546 evaluate_typechecked_b_formula_in_state(State,Typed,eval_opts(_StateId,_ProvideLets,EvalExpand,TO),PPOpts,Result) :-
1547 safe_time_out(
1548 catch_enumeration_warning_exceptions(
1549 evaluate_formula_eval(State,Typed,EvalExpand,Res,Solution),
1550 Res = enum_warning),
1551 TO,TimeOutRes),
1552 (TimeOutRes=time_out -> Res=error(time_out) ; true),
1553 (real_error_occurred -> RealError = real_error ; RealError = no_real_error),
1554 get_all_errors_with_span_info_and_reset(Errors),
1555 extract_result(Res,Typed,Solution,PPOpts,Errors,RealError,Result).
1556
1557 extract_result(enum_warning,_,_,_,_,_,R) :- !, R=enum_warning.
1558 extract_result(error(ErrDesc),_,_Sol,_PPOpts,Errors,_RealError,Result) :- !,
1559 Result = errors(ErrDesc, Errors).
1560 extract_result(value(Term),Typed,Solutions,PPOpts,Errors,RealError,Result) :- !,
1561 get_texpr_type(Typed, Type),
1562 pretty_print_bvalue_with_type(PPOpts,Term,Type,R),
1563 (RealError == no_real_error ->
1564 % TODO: get the type of each of the solutions and pass it to the pretty print
1565 prettyprint_solutions(PPOpts,Solutions,PPSol),
1566 Result = result(R,PPSol,Errors)
1567 ;
1568 Result = errors(R,Errors)
1569 ).
1570
1571 %:- use_module(eval_strings,[eval_predicate/5]). % TODO: export and refactor
1572 % TO DO: move this into another more general module:
1573 evaluate_formula_eval(State,Typed,_EvalExpand,Res,LocalState) :-
1574 get_texpr_type(Typed,pred),
1575 !,
1576 eval_predicate(State,Typed,Res,LocalState).
1577 evaluate_formula_eval(State,Typed,EvalExpand,Res,[]) :-
1578 evaluate_expression(State,Typed,EvalExpand,Res).
1579
1580 :- use_module(clpfd_interface,[catch_clpfd_overflow_call2/2]).
1581 :- use_module(error_manager,[enter_new_error_scope/2, exit_error_scope/3,clear_all_errors_in_error_scope/1,
1582 event_occurred_in_error_scope/1, abort_error_occured_in_error_scope/0]).
1583 :- use_module(store,[normalise_value_for_var/4]).
1584 % a simplified/modified version of eval_strings:eval_expression
1585 % evaluate an expression Typed in an expanded state EState giving string result Result and Prolog value NValue
1586 evaluate_expression(EState,Typed,EvalExpand,Term) :-
1587 enter_new_error_scope(ScopeID,evaluate_expression),
1588 clear_all_errors_in_error_scope(ScopeID),
1589 %replace_expression_by_kodkod_if_enabled(Typed,Typed2),
1590 catch_clpfd_overflow_call2(b_interpreter:b_compute_expression_nowf(Typed,[],EState,Value,'ProB2',0),fail), % We could return CLPFD overflow error result
1591 !,
1592 %logger:writeln_log_time(normalise_value_for_var(evaluate_expression)),
1593 normalise_value_for_var(evaluate_expression,EvalExpand,Value,NValue),
1594 get_unknown_error_result(ErrRes),
1595 exit_error_scope(ScopeID,ErrOcc,evaluate_expression),
1596 % FIXME Is ErrOcc ever true here?
1597 % For WD errors, b_compute_expression_nowf fails, so this code is never reached.
1598 % Enumeration warnings are thrown as exceptions and so also bypass this code.
1599 (ErrOcc=true
1600 -> Term = error(ErrRes)
1601 ; Term = value(NValue)
1602 ).
1603 evaluate_expression(_,_,_,error(ErrRes)) :-
1604 get_unknown_error_result(ErrRes),
1605 exit_error_scope(_ScopeID,_,evaluate_expression).
1606
1607 % which result should be displayed in case of failure/errors:
1608 get_unknown_error_result(ErrRes) :-
1609 (abort_error_occured_in_error_scope -> ErrRes = 'NOT-WELL-DEFINED' ; ErrRes = 'UNKNOWN').
1610
1611 % a simplified/modified version of eval_strings:eval_predicate_aux
1612 eval_predicate(State, ExTyped,Result,LocalState) :-
1613 enter_new_error_scope(ScopeID,eval_predicate), clear_all_errors_in_error_scope(ScopeID),
1614 (catch_clpfd_overflow_call2(prob2_interface:eval_predicate2(State, ExTyped,LocalState,Res),
1615 fail)
1616 -> true
1617 ; event_occurred_in_error_scope(enumeration_warning(_,_,_,_,_Critical))
1618 -> Res=enum_warning
1619 ; eval_predicate2_fail_result(ExTyped,Res) % either value(pred_true) or value(pred_false)
1620 ),
1621 get_unknown_error_result(ErrRes),
1622 exit_error_scope(ScopeID,ErrOcc,eval_predicate),
1623 (ErrOcc=true
1624 -> Result = error(ErrRes)
1625 ; Result = Res
1626 ).
1627
1628 :- use_module(probsrc(bsyntaxtree), [safe_create_texpr/4]).
1629 :- use_module(eval_strings, []).
1630 eval_predicate2(State, ExTyped,LocalState,value(pred_true)) :-
1631 eval_strings:is_existential_quantifier(ExTyped,Parameters,Typed), % TO DO: move to module
1632 !,
1633 test_bool_exists(State, Parameters,Typed,LocalState).
1634 eval_predicate2(State, ExTyped,LocalState,value(pred_false)) :-
1635 is_universal_quantifier(ExTyped,Parameters,TypedLHS,TypedRHS),
1636 !,
1637 safe_create_texpr(negation(TypedRHS),pred,[try_smt],NegRHS),
1638 conjunct_predicates([TypedLHS,NegRHS],Conjunction), % replace Kodkod?
1639 test_bool_exists(State, Parameters,Conjunction,LocalState).
1640 eval_predicate2(State, Typed,LocalState,value(pred_true)) :- LocalState=[],
1641 b_test_boolean_expression_cs(Typed,LocalState,State,'ProB2-Java',0).
1642
1643 % what should the result be if the above eval_predicate2 fails (without enumeration warning):
1644 eval_predicate2_fail_result(ExTyped,Res) :-
1645 is_universal_quantifier(ExTyped,_,_,_),!, Res=value(pred_true).
1646 eval_predicate2_fail_result(_,value(pred_false)).
1647
1648
1649 test_bool_exists(EState, Parameters,Typed,LocalState) :-
1650 kernel_waitflags:init_wait_flags(WF,[test_bool_exists]),
1651 b_interpreter:set_up_typed_localstate(Parameters,_FreshOutputVars,TypedVals,[],LocalState,positive),
1652 b_enumerate:b_tighter_enumerate_values_in_ctxt(TypedVals,Typed,WF),
1653 b_interpreter:b_test_boolean_expression(Typed,LocalState,EState,WF),
1654 kernel_waitflags:ground_wait_flags(WF).
1655
1656 is_universal_quantifier(b(forall(Parameters,LHS,RHS),pred,_),Parameters,LHS,RHS).
1657
1658 :- dynamic prob2_formula/3.
1659
1660 :- use_module(bmachine, [determine_type_of_formula/2]).
1661 register_prob2_formula1(_, FormulaUUID, _) :- prob2_formula(FormulaUUID,_,_),!.
1662 register_prob2_formula1(M, FormulaUUID, Formula) :-
1663 default_eval_opts(EOpts),
1664 formula_typecheck_for_eval(Formula,EOpts,M,Typed),
1665 determine_type_of_formula(Typed,Requirements),
1666 assertz(prob2_formula(FormulaUUID, Typed, Requirements)).
1667
1668 %! register_prob2_formulas(+FormulaUUIDs, +Formulas)
1669 register_prob2_formulas(FormulaUUIDs,Formulas) :-
1670 % _Machine is shared across all calls so that full_b_machine only needs to be computed once.
1671 maplist(register_prob2_formula1(_Machine),FormulaUUIDs,Formulas).
1672
1673
1674 % TO DO: determine upon registering whether a formula reads nothing, just constants, or also variables
1675
1676 % unregister a single or a list of formula ids:
1677 unregister_prob2_formula(FormulaUUID) :- retractall(prob2_formula(FormulaUUID,_,_)).
1678 unregister_prob2_formulas(Fs) :- maplist(unregister_prob2_formula,Fs).
1679
1680
1681 % check whether we can evaluate the formula in the state:
1682 requirements_met(requires_nothing,_).
1683 requirements_met(requires_constants,constants_only_state).
1684 requirements_met(requires_constants,full_initialised_state).
1685 requirements_met(requires_variables,full_initialised_state).
1686 requirements_met(formula(Typed),State) :-
1687 (State=full_initialised_state -> true
1688 ; determine_type_of_formula(Typed,Requirements), requirements_met(Requirements,State)).
1689
1690
1691
1692 % API for showing Tk Animation Images in Java FX (or other):
1693 :- use_module(extrasrc(graphical_state_viewer_images),[get_animation_images/1,
1694 get_animation_image_grid/6, get_react_to_item_right_click_options/4, react_to_item_right_click/6]).
1695 get_animation_image_list(ImageList) :- get_animation_images(ImageList).
1696 % Format: [image_file(0,'images/empty_box_white.gif'),...,image_file(6,'images/F.gif')]
1697
1698 get_animation_image_matrix_for_state(ID,Matrix,MinRow,MaxRow,MinCol,MaxCol) :-
1699 (get_animation_image_grid(ID,M,M1,M2,M3,M4)
1700 -> Matrix=M, MinRow=M1, MaxRow=M2, MinCol=M3, MaxCol=M4
1701 ; Matrix=[], MinRow = -1, MaxRow = 0, MinCol = -1, MaxCol = 0).
1702 % Format: [entry(1,1,image(0)),... entry(2,3,text(some_atom)),...], entry(Row,Col,ImgOrText)
1703
1704 % returns a list of terms option(transition_term, description) for the various options that are available in the state ID
1705 % for Row/Col (Y/X)
1706 get_react_to_item_right_click_options_for_state(ID,Row,Col,Options) :-
1707 get_react_to_item_right_click_options(ID,Col,Row,Options).
1708
1709 % should be called for one option provided by get_react_to_item_right_click_options_for_state
1710 react_to_item_right_click_option_for_state(ID,Row,Col,Option,TransitionID,NewID) :-
1711 react_to_item_right_click(ID,Col,Row,Option,TransitionID,NewID).
1712
1713 % | ?- prob2_interface:get_react_to_item_right_click_options_for_state(3,1,1,L).
1714 % L = ['Set(1,1,1)','Set(1,1,2)','Set(1,1,3)','Solve'|...] ?
1715 % | ?- prob2_interface:react_to_item_right_click_option_for_state(3,1,1,'Set(1,1,1)',NewID).
1716 % Performed: Set(int(1),int(1),int(1))
1717 % NewID = ..., TransitionID=...
1718
1719 /**
1720 get_states_for_predicate(+Raw,-States,-Errors)
1721
1722 Takes a predicate and finds a list of all state ids for which the
1723 predicate holds. The states that are not intitialized (i.e. root) are
1724 included in the list. The list that is returned is therefore the union
1725 of the uninitialised states and the states for which the predicate holds.
1726
1727 #### called by:
1728 * ProB 2.0: GetStatesFromPredicate
1729 */
1730 get_states_for_predicate(Raw,States,Errors) :-
1731 (predicate_typecheck_for_eval(Raw,Typed) ->
1732 findall(StateId,get_state_for_predicate(StateId,Typed),States),
1733 Errors = []
1734 ;
1735 States = [],
1736 get_all_errors_with_span_info_and_reset(Errors)
1737 ).
1738
1739 get_state_for_predicate(StateId,Typed) :-
1740 state_space:visited_expression(StateId,StatePacked),
1741 ( is_initialised_state(StateId) ->
1742 expand_const_and_vars_to_full_store(StatePacked,State),
1743 b_test_boolean_expression_cs(Typed,[],State,'ProB2-Java',0)
1744 ;
1745 true
1746 ).
1747
1748 /**
1749 This cycles through all of the solutions and extracts the string
1750 representation of the solutions.
1751 */
1752 prettyprint_solutions(_PPOpts,[],[]).
1753 prettyprint_solutions(PPOpts,[bind(Name,Res)|T],[PP|R]) :-
1754 pretty_print_bvalue(PPOpts,Res,PPRes),
1755 PP = solution(Name,PPRes),
1756 prettyprint_solutions(PPOpts,T,R).
1757
1758 /**
1759 filter_states_for_predicate(+Raw,+States,-Filtered)
1760
1761 Takes a list of state ids and a predicate and finds all of the states
1762 for which the predicate is true
1763
1764 #### called by:
1765 * ProB 2.0: FilterStatesForPredicateCommand
1766 */
1767 filter_states_for_predicate(Raw,States,Filtered) :-
1768 (predicate_typecheck_for_eval(Raw,Typed) ->
1769 filter_states_for_typed_predicate(Typed,States,Filtered)
1770 ;
1771 get_all_errors_with_span_info_and_reset(Errors),
1772 Filtered = errors(Errors)
1773 ).
1774
1775 filter_states_for_typed_predicate(_,[],[]).
1776 filter_states_for_typed_predicate(Typed,[Id|States],Filtered) :-
1777 get_bstate_with_deferred_sets(Id,false,State,Kind),
1778 ( Kind = full_initialised_state -> %is_initialised_state(Id) ->
1779 (b_test_boolean_expression_cs(Typed,[],State,'ProB2-Java',0) ->
1780 Filtered = [Id|Rest] ;
1781 Filtered = Rest
1782 )
1783 ; Filtered = [Id|Rest]
1784 ),
1785 filter_states_for_typed_predicate(Typed,States,Rest).
1786
1787 /* ------------------------- */
1788 /* Formula Expansion */
1789 /* ------------------------- */
1790
1791 /**
1792 get_top_level_formulas(-TopIds)
1793
1794 Gets all top-level formula IDs from bvisual2.
1795
1796 #### called by:
1797 * ProB 2.0: GetTopLevelFormulasCommand
1798 */
1799 get_top_level_formulas(TopIds) :-
1800 suppress_rodin_positions(C),
1801 bv_get_top_level(TopIds),
1802 reset_suppress_rodin_positions(C).
1803
1804 /**
1805 insert_formula_for_expansion(+AST,-Id)
1806
1807 Inserts a formula into bvisual2 module
1808 The formula is inserted as a child of level "user" in bvisual2
1809
1810 #### called by:
1811 * ProB 2.0: InsertFormulaForVisualizationCommand
1812 */
1813 insert_formula_for_expansion(Typed,Id) :- Typed = b(_,_,_),!,
1814 suppress_rodin_positions(C),
1815 bv_insert_formula(Typed,user,Id),
1816 reset_suppress_rodin_positions(C).
1817
1818 insert_formula_for_expansion(AST,Id) :-
1819 suppress_rodin_positions(C),
1820 b_type_expression(AST,[variables],_,Typed,Errors),
1821 ( Errors == [] ->
1822 bv_insert_formula(Typed,user,Id),
1823 reset_suppress_rodin_positions(C)
1824 ;
1825 add_all_perrors(Errors), reset_suppress_rodin_positions(C),
1826 fail).
1827
1828 /**
1829 prob2_evaluate_bvisual2_formulas(+Ids,+StateId,-Values)
1830
1831 Uses the bvisual2 module to evaluate the given formulas.
1832 Unlike expand_formula_nonrecursive/6, this predicate only evaluates the formulas,
1833 but doesn't return their label, description, or subformulas.
1834
1835 #### called by:
1836 * ProB 2.0: EvaluateBVisual2FormulasCommand
1837 */
1838 prob2_evaluate_bvisual2_formulas(Ids,StateId,Values) :-
1839 prob2_evaluate_bvisual2_formulas(Ids,StateId,[],Values).
1840
1841 /**
1842 prob2_evaluate_bvisual2_formulas(+Ids,+StateId,+Options,-Values)
1843
1844 New version of the above predicate which also supports options.
1845 Currently supported options:
1846 - unlimited: does not truncate terms
1847 */
1848 prob2_evaluate_bvisual2_formulas(Ids,StateId,Options,Values) :-
1849 (member(unlimited,Options) ->
1850 bv_get_values_unlimited(Ids,StateId,Values)
1851 ; bv_get_values(Ids,StateId,Values)).
1852
1853 /**
1854 prob2_expand_bvisual2_formula(+FormulaId,+Options,-ExpandedFormula)
1855
1856 Uses the bvisual2 module to expand a specified formula,
1857 optionally also expanding child formulas recursively and/or evaluating all expanded formulas.
1858 FormulaId must be a bvisual2 formula ID,
1859 as returned for example by get_top_level_formulas/1, insert_formula_for_expansion/2, or prob2_expand_bvisual2_formula/3.
1860
1861 #### called by:
1862 * ProB 2.0: ExpandBVisual2FormulaCommand
1863 */
1864 prob2_expand_bvisual2_formula(FormulaId,Options,ExpandedFormula) :-
1865 % Check that no unknown or duplicate options were passed.
1866 (selectchk(evaluate(_), Options, Options1) -> true ; Options1 = Options),
1867 (selectchk(recursive, Options1, Options2) -> true ; Options2 = Options1),
1868 Options2 == [],
1869
1870 suppress_rodin_positions(C),
1871 expand_bvisual2_formula_internal(Options,FormulaId,ExpandedFormula),
1872 reset_suppress_rodin_positions(C).
1873
1874 expand_bvisual2_formula_internal(Options,FormulaId,formula(Entries)) :-
1875 findall(Attribute, bvisual2_formula_attribute(FormulaId,Options,Attribute), Entries).
1876
1877 bvisual2_formula_attribute(FormulaId,_,id(FormulaId)).
1878 bvisual2_formula_attribute(FormulaId,_,description(Desc)) :-
1879 (bv_formula_description(FormulaId,Description) -> true ; Description=''),
1880 bv_formula_origin(FormulaId,Origin), % TODO: store this as a seperate attribute
1881 (Description='' -> Origin \= '', Desc = Origin
1882 ; Origin='' -> Desc = Description
1883 ; ajoin([Description,'\n',Origin],Desc)).
1884 bvisual2_formula_attribute(FormulaId,_,functor_symbol(FunctorSymbol)) :-
1885 bv_get_formula_functor_symbol(FormulaId,FunctorSymbol).
1886 bvisual2_formula_attribute(FormulaId,_,rodin_labels(Labels)) :-
1887 bv_formula_labels(FormulaId,Labels).
1888 bvisual2_formula_attribute(FormulaId,_,proof_info(DischargedInfo)) :-
1889 bv_formula_discharged_info(FormulaId,DischargedInfo).
1890 bvisual2_formula_attribute(FormulaId,Options,value(EvaluatedValue)) :-
1891 memberchk(evaluate(StateId), Options),
1892 % TODO Refactor to combine multiple bv_get_values calls?
1893 bv_get_values([FormulaId], StateId, [EvaluatedValue]).
1894 bvisual2_formula_attribute(FormulaId,_,type(Type)) :-
1895 (bv_is_typed_predicate(FormulaId) ->
1896 Type = predicate;
1897 (bv_is_typed_formula(FormulaId) -> Type = expression; Type = other)).
1898 bvisual2_formula_attribute(FormulaId,Options,Attribute) :-
1899 bv_expand_formula(FormulaId,Label,ChildrenIds),
1900 (Attribute = label(Label) ; bvisual2_formula_children_attribute(ChildrenIds,Options,Attribute)).
1901
1902
1903 bvisual2_formula_children_attribute(ChildrenIds,Options,children(ExpandedChildren)) :-
1904 memberchk(recursive, Options),
1905 !,
1906 maplist(expand_bvisual2_formula_internal(Options), ChildrenIds, ExpandedChildren).
1907 bvisual2_formula_children_attribute(ChildrenIds,_,children_ids(ChildrenIds)).
1908
1909
1910 /* ------------------------- */
1911 /* Model Checking */
1912 /* ------------------------- */
1913
1914 /**
1915 do_modelchecking(+MaxNumberOfStatesToCheck,+Time,+Options,-Result,-Stats)
1916
1917 #### do_modelchecking(+MaxNumberOfStatesToCheck, +Time,+Options,-Result,stats(-NrNodes,-NrTrans,-NrProcessed))
1918 * +MaxNumberOfStatesToCheck : maximum number of states to be checked
1919 * +Time : Timeout specified by the user in ms
1920 * +Options : List of options specified by the user. Used for predicate do_modelchecking(Time,Options,Result)
1921 * -NrNodes : total number of nodes in state space. Calculated with get_state_space_stats
1922 * -NrTrans : total number of nodes in state space. Calculated with get_state_space_stats
1923 * -NrProcessed : total number of calculated nodes in state space. Calculated with get_state_space_stats
1924 When Time Milliseconds have elapsed the modelchecker should stop after its next step
1925
1926 #### called by:
1927 * ProB Plugin: ModelCheckingCommand
1928 * ProB 2.0: ModelCheckingStepCommand
1929 */
1930 do_modelchecking(MaxNumberOfStatesToCheck, Time, Options, Result, stats(NrNodes,NrTrans,NrProcessed)) :-
1931 statistics(walltime, [CurTime,_]), /* get current time in ms */
1932 LimitTime is CurTime+Time,
1933 option_set(find_deadlocks, Options, Deadlock),
1934 option_set(find_invariant_violations, Options, Invariant),
1935 option_set(find_assertion_violations, Options, Assertions),
1936 (option_set(ignore_state_errors, Options, 1) -> FindStateErrors=0 ; FindStateErrors=1),
1937 option_set(inspect_existing_nodes, Options, InspectExistingNodes),
1938 option_set(stop_at_full_coverage, Options, StopAtFullCoverage),
1939 (option_set(breadth_first_search, Options, 1) -> set_depth_breadth_first_mode(breadth_first) ;
1940 option_set(depth_first_search, Options, 1) -> set_depth_breadth_first_mode(depth_first) ;
1941 set_depth_breadth_first_mode(mixed)),
1942 option_set(find_goal, Options, Goal),
1943 get_preference(por,WithPOR),
1944 tcltk_interface:do_model_check(MaxNumberOfStatesToCheck, _, LimitTime, Res, Deadlock, Invariant, Goal,Assertions,
1945 FindStateErrors,StopAtFullCoverage, WithPOR, InspectExistingNodes),
1946 build_modelcheck_return(Res, Result),
1947 get_state_space_stats(NrNodes, NrTrans, NrProcessed).
1948
1949
1950 /**
1951 set_goal_for_model_checking(+Goal)
1952
1953 Sets the goal for model checking. The Option search_for_goal needs to be set when starting
1954 model checking in order for this to have an effect on the model checking.
1955
1956 #### called by:
1957 * ProB 2.0: SetBGoalCommand
1958 */
1959 set_goal_for_model_checking(Goal) :-
1960 predicate_typecheck_for_eval(Goal,TypedGoal),
1961 b_set_parsed_typed_machine_goal(TypedGoal).
1962
1963 /**
1964 reset_goal_for_model_checking
1965
1966 Reset the goal for model checking. Will remove a saved custom goal and load the goal from DEFINITIONS if it exists.
1967
1968 #### called by:
1969 * ProB 2.0: ResetBGoalCommand
1970 */
1971 :- use_module(probsrc(bmachine), [b_unset_machine_goal/0, b_reset_machine_goal_from_DEFINITIONS/0]).
1972 reset_goal_for_model_checking :-
1973 b_unset_machine_goal,
1974 (b_or_z_mode -> (b_reset_machine_goal_from_DEFINITIONS ; true) ; true),
1975 !.
1976
1977 /**
1978 option_set(+Element, +List, -Result)
1979
1980 Takes an atom and unifies Result with 1 if the atom is in the List.
1981 Otherwise, Result is unified with 0.
1982 */
1983 option_set(Element, List, Result) :-
1984 ( member(Element,List)
1985 -> Result = 1
1986 ; Result = 0).
1987
1988 %! build_modelcheck_return(+MCRes, -JavaResult)
1989 build_modelcheck_return(MCRes, JavaResult) :-
1990 build_modelcheck_return2(MCRes, JavaResult) -> true
1991 ; 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)*/
1992 current_state_id(State), JavaResult=general_error(State, MCRes).
1993
1994 build_modelcheck_return2(no, not_yet_finished(100000)).
1995 build_modelcheck_return2([timeout,N], not_yet_finished(N1)) :- N1 is 100000 - N.
1996 build_modelcheck_return2(deadlock, deadlock(State)):- current_state_id(State).
1997 build_modelcheck_return2(invariant_violation, invariant_violation(State)):- current_state_id(State).
1998 build_modelcheck_return2(xtl_error, xtl_error(State)):- current_state_id(State).
1999 build_modelcheck_return2(assertion_violation, assertion_violation(State)):- current_state_id(State).
2000 build_modelcheck_return2(state_error(_), state_error(State)):- current_state_id(State).
2001 build_modelcheck_return2(goal_found, goal_found(State)) :- current_state_id(State).
2002 build_modelcheck_return2(well_definedness_error, well_definedness_error(State)) :- current_state_id(State).
2003 build_modelcheck_return2(general_error_occurred, general_error(State)):- current_state_id(State).
2004 build_modelcheck_return2(full_coverage, full_coverage).
2005 build_modelcheck_return2(all, Res) :- max_reached_or_timeout_for_node(_),!, Res=ok_not_all_nodes_considered.
2006 build_modelcheck_return2(all, ok).
2007
2008 :- use_module(symbolic_model_checker(bmc),[bmc_symbolic_model_check/1]).
2009 :- use_module(symbolic_model_checker(kinduction), [kinduction_symbolic_model_check/1, tinduction_symbolic_model_check/1]).
2010 :- use_module(symbolic_model_checker(ic3), [ic3_symbolic_model_check/1]).
2011 symbolic_model_check(bmc,Result) :-
2012 bmc_symbolic_model_check(Result).
2013 symbolic_model_check(kinduction,Result) :-
2014 kinduction_symbolic_model_check(Result).
2015 symbolic_model_check(tinduction,Result) :-
2016 tinduction_symbolic_model_check(Result).
2017 symbolic_model_check(ic3,Result) :-
2018 ic3_symbolic_model_check(Result).
2019
2020 /**
2021 compute_efficient_statespace_stats(-NrNodes, -NrTrans, -NrProcessed)
2022
2023 Computes the coverage statistics of the current state space at any given time.
2024 The information of interest includes the total number of nodes and transitions, as well as
2025 a list of statistics about the nodes and operations and a list of the operations that have been uncovered sofar.
2026
2027 #### called by:
2028 * ProB Plugin: ComputeCoverageCommand
2029 * ProB 2.0: ComputeCoverageCommand
2030 */
2031 :- use_module(extrasrc(coverage_statistics),
2032 [compute_the_coverage/5, operation_hit/2,query_node_hit/2, uncovered_operation/1]).
2033
2034 compute_efficient_statespace_stats(NrNodes, NrTrans, NrProcessed) :-
2035 get_state_space_stats(NrNodes, NrTrans, NrProcessed).
2036
2037 %! compute_coverage(-TotalNodeNr,-TotalTransSum,-NodeStat,-OpStat,-Uncovered)
2038 compute_coverage(TotalNodeNr,TotalTransSum,NodeStat,OpStat,Uncovered) :-
2039 compute_the_coverage(_,TotalNodeNr,TotalTransSum,false,false),
2040 findall(S2,(operation_hit(OpS,Nr),string_concatenate(':',Nr,S1),string_concatenate(OpS,S1,S2)),OpStat),
2041 findall(S2,(query_node_hit(Prop,Nr),string_concatenate(':',Nr,S1),string_concatenate(Prop,S1,S2)),NodeStat),
2042 findall(OpName, uncovered_operation(OpName),Uncovered).
2043
2044
2045 get_modelchecking_coverage(TotalNodeNr,TotalTransSum,NodeStat,OpStat,Uncovered) :-
2046 compute_the_coverage(_,TotalNodeNr,TotalTransSum,false,false),
2047 findall(entry(OpS,Nr),operation_hit(OpS,Nr),OpStat),
2048 findall(entry(Prop,Nr),query_node_hit(Prop,Nr),NodeStat),
2049 findall(OpName, uncovered_operation(OpName),Uncovered).
2050
2051 /**
2052 get_statistics(+Option,-Value)
2053
2054 Takes an option for the statistics and returns the corresponding value.
2055
2056 #### called by:
2057 * ProB 2.0: GetStatisticsCommand
2058 */
2059
2060 get_statistics(global_runtime,V) :- statistics(runtime,[V,_]).
2061 get_statistics(global_walltime,V) :- statistics(walltime,[V,_]).
2062 get_statistics(delta_runtime,V) :- statistics(runtime,[_,V]).
2063 get_statistics(delta_walltime,V) :- statistics(walltime,[_,V]).
2064 get_statistics(memory_used,V) :- statistics(memory_used,V).
2065 get_statistics(memory_free,V) :- statistics(memory_free,V).
2066 get_statistics(global_stack_used,V) :- statistics(global_stack_used,V).
2067 get_statistics(local_stack_used,V) :- statistics(local_stack_used,V).
2068 %get_statistics(global_stack_free,V) :- statistics(global_stack_free,V).
2069 %get_statistics(local_stack_free,V) :- statistics(local_stack_free,V).
2070 get_statistics(trail_used,V) :- statistics(trail_used,V).
2071 get_statistics(choice_used,V) :- statistics(choice_used,V).
2072 get_statistics(atoms_used,V) :- statistics(atoms_used,V).
2073 get_statistics(atoms_nbused,V) :- statistics(atoms_nbused,V).
2074 get_statistics(gc_count,V) :- statistics(gc_count,V).
2075 get_statistics(gc_time,V) :- statistics(gc_time,V).
2076
2077 /**
2078 prob2_deadlock_freedom_check(+Predicate,-Result)
2079
2080 Performs deadlock freedom checking with constraint Predicate and calulates the Result.
2081
2082 #### called by:
2083 * ProB 2.0: ConstraintBasedDeadlockCheckCommand
2084 */
2085 prob2_deadlock_freedom_check(Predicate,Result) :-
2086 b_type_expression(Predicate,[variables],pred,TPredicate,Errors),
2087 ( Errors == [] ->
2088 prob2_deadlock_freedom_check1(TPredicate,Result)
2089 ;
2090 Result = errors(Errors)).
2091 prob2_deadlock_freedom_check1(Predicate,Result) :-
2092 % always do a deadlock check with SMT mode enabled
2093 call_with_smt_mode_enabled(prob2_deadlock_freedom_check2(Predicate,Result)).
2094 :- use_module(clpfd_interface,[catch_clpfd_overflow_call1/1]).
2095 :- use_module(b_state_model_check,[cbc_deadlock_freedom_check/3]).
2096 prob2_deadlock_freedom_check2(Predicate,Result) :-
2097 user_interruptable_call_det(clpfd_interface:catch_clpfd_overflow_call1(
2098 b_state_model_check:cbc_deadlock_freedom_check(State,Predicate,0)),
2099 InterruptResult),!,
2100 ( InterruptResult = interrupted ->
2101 Result = interrupted
2102 ; State = time_out ->
2103 Result = interrupted
2104 ;
2105 Result = deadlock(Transition,StateId),
2106 add_artificial_transition(root,deadlock_check,State,StateId,Transition)).
2107 prob2_deadlock_freedom_check2(_Predicate,no_deadlock_found).
2108
2109
2110
2111
2112
2113
2114 /**
2115 prob2_invariant_check(+Ops,-Result)
2116
2117 Performs invariant cbc checking for either for all operations or a list of operations.
2118
2119 #### called by:
2120 * ProB 2.0: ConstraintBasedInvariantCheckCommand
2121 */
2122 prob2_invariant_check(all,Result) :-
2123 findall(OpName,b_is_op_or_init(OpName),Ops),
2124 % TO DO: also treat $initailise_machine; but state_model_check_invariant does not support it yet
2125 prob2_invariant_check2(Ops,Result).
2126 prob2_invariant_check(ops(Ops),Result) :-
2127 prob2_invariant_check2(Ops,Result).
2128 prob2_invariant_check2(Ops,Result) :-
2129 call_with_smt_mode_enabled(prob2_invariant_check3(Ops,Result,[])).
2130 prob2_invariant_check3([]) --> !.
2131 prob2_invariant_check3([Op|Rest]) -->
2132 prob2_invariant_check_for_single_op(Op),
2133 prob2_invariant_check3(Rest).
2134 prob2_invariant_check_for_single_op(OpName,In,Out) :-
2135 ( clpfd_interface:catch_clpfd_overflow_call1(
2136 b_state_model_check:state_model_check_invariant(OpName,State1,Operation,State2)) ->
2137 In = [counterexample(OpName,Trans1,Trans2)|Out],
2138 atom_concat( invariant_check_ , OpName, RootTrans),
2139 add_artificial_transition(root, RootTrans,State1,StateId1,Trans1),
2140 add_artificial_transition(StateId1,Operation,State2,_StateId2,Trans2)
2141 ;
2142 In = Out).
2143
2144 b_is_op_or_init(OpName) :- b_is_operation_name(OpName).
2145 b_is_op_or_init(OpName) :- b_is_initialisation_name(OpName).
2146
2147 :- use_module(b_state_model_check,[cbc_find_redundant_invariants/2]).
2148 prob2_redundant_invariants(Redundant, Timeout) :-
2149 cbc_find_redundant_invariants(Redundant, Timeout).
2150
2151 /**
2152 add_artificial_transition(+SrcId,+Operation,+DstState,+DstId,-TransitionTuple)
2153
2154 creates a helper transition that is artificially added to the state space (e.g. during CBC deadlock checking)
2155 This transition is added to the state space.
2156 A triple TransitionTuple in the form op(TransId,OpName,SrcId,DstId) for this transition is generated.
2157 */
2158 % TODO: return list of transitions and re-use concrete_constants if possible, see seperate_state_into_const_and_vars
2159 add_artificial_transition(SrcId,Operation,DstState,DstId,TransitionTuple) :-
2160 tcltk_interface:tcltk_add_new_transition_transid(SrcId,Operation,DstId,DstState,[],TransId),
2161 extract_op_name(Operation,OpName),
2162 TransitionTuple = op(TransId,OpName,SrcId,DstId).
2163
2164 /**
2165 computes the enabling relation information for the provided operations of interest
2166 get_enable_matrix(-PairsOfOperations,+EnableResult)
2167 PairsOfOperations: list of pair(Op1,Op2) of operations pairs for which the enable relation is to be computed
2168 EnableResult: list of terms enable_edges(Op1,Op2,enable_edges(E,KE,D,KD)) of same length
2169 */
2170 get_enable_matrix(PairsOfOperations,EnableResult) :-
2171 maplist(compute_enable_matrix_entry(100),PairsOfOperations,EnableResult).
2172
2173 :- use_module(cbcsrc(enabling_analysis),[compute_cbc_enable_rel/4]).
2174 compute_enable_matrix_entry(ExtraTimeout,pair(OpName1,OpName2),
2175 enable_rel(OpName1,OpName2,
2176 enable_edges(Enable,KeepEnabled,Disable,KeepDisabled))) :-
2177 compute_cbc_enable_rel(OpName1,OpName2,ExtraTimeout,[Enable,KeepEnabled,Disable,KeepDisabled]).
2178
2179 /**
2180 prob2_do_ltl_modelcheck(+Formula,+Options,-Result)
2181
2182 Performs an LTL model checking step.
2183
2184 Supported options:
2185 * max_new_states(Max) - maximum number of new states that will be explored, or -1 (the default) for no limit
2186 * mode(Mode) - init (the default) to check starting from every initialized state, or specific_node(StateID) to check starting from one specific state
2187
2188 #### called by:
2189 * ProB 2.0: LtlCheckingCommand
2190 */
2191 prob2_do_ltl_modelcheck(Formula, Options, Result) :-
2192 (selectchk(max_new_states(Max), Options, Options1) -> true ; Max = -1, Options1 = Options),
2193 (selectchk(mode(Mode), Options1, Options2) -> true ; Mode = init, Options2 = Options1),
2194 Options2 == [],
2195
2196 typecheck_temporal_formula(Formula,TypeCheckedFormula,Status),
2197 (Status=ok ->
2198 ltl_model_check_with_ce(TypeCheckedFormula,Max,Mode,Result1),
2199 prob2_ltl_adapt_operations(Result1,Result)
2200 ;
2201 get_all_errors_with_span_info_and_reset(Errors),
2202 Result = type_error(Errors)
2203 ).
2204
2205 % Old command without option list - can be removed after release of ProB Java API 4.14.0.
2206 prob2_do_ltl_modelcheck(Formula,Max,Result,Errors) :-
2207 prob2_do_ltl_modelcheck(Formula, [max_new_states(Max)], Res),
2208 (Res = type_error(Errors) ->
2209 Result = typeerror
2210 ;
2211 Result = Res,
2212 Errors = []
2213 ).
2214
2215 prob2_ltl_adapt_operations(counterexample(CE1,LoopEntry,PathToCE1), Res) :- !,
2216 Res = counterexample(CE,LoopEntry,PathToCE),
2217 create_simple_op_terms_for_path(PathToCE1,root,PathToCE),
2218 prob2_ltl_adapt_ce(CE1,CE).
2219 prob2_ltl_adapt_operations(Result,Result).
2220
2221 prob2_ltl_adapt_ce([],[]).
2222 prob2_ltl_adapt_ce([atom(StateId,_,OpTuple)|Irest],[Transition|Orest]) :-
2223 prob2_ltl_adapt_ce2(OpTuple,StateId,Transition),
2224 prob2_ltl_adapt_ce(Irest,Orest).
2225 prob2_ltl_adapt_ce2(none,_StateId,none).
2226 prob2_ltl_adapt_ce2((TransId,Action,DestId),StateId,op(TransId,Name,StateId,DestId)) :-
2227 extract_op_name(Action,Name).
2228
2229
2230 create_simple_op_terms_for_path([],_,[]).
2231 create_simple_op_terms_for_path([(Id,Op,DstId)|T],StateID,[op(Id,Name,StateID,DstId)|FT]) :-
2232 extract_op_name(Op,Name),
2233 create_simple_op_terms_for_path(T,DstId,FT). % difference to create_simple_op_terms: we move to DstId
2234
2235
2236 /**
2237 prob2_do_ctl_modelcheck(+Formula, +Options, -Result, -CE)
2238
2239 Performs an CTL model checking step.
2240
2241 Supported options:
2242 * max_new_states(Max) - maximum number of new states that will be explored, or -1 (the default) for no limit
2243 * mode(Mode) - init (the default) to check starting from every initialized state, or specific_node(StateID) to check starting from one specific state
2244
2245 #### called by:
2246 * ProB 2.0: CtlCheckingCommand
2247 */
2248 prob2_do_ctl_modelcheck(Formula, Options, Result, CE) :-
2249 (selectchk(max_new_states(Max), Options, Options1) -> true ; Max = -1, Options1 = Options),
2250 (selectchk(mode(Mode), Options1, Options2) -> true ; Mode = init, Options2 = Options1),
2251 Options2 == [],
2252
2253 typecheck_temporal_formula(Formula, TypeCheckedFormula, Status),
2254 (Status = ok ->
2255 ctl_model_check_with_ast(main, TypeCheckedFormula, Max, Mode, Result, CE)
2256 ;
2257 get_all_errors_with_span_info_and_reset(Errors),
2258 Result = type_error(Errors),
2259 CE = [] % no counter example
2260 ).
2261
2262 % Old command without option list - can be removed after release of ProB Java API 4.14.0.
2263 prob2_do_ctl_modelcheck(Formula, MaxNodes, Mode, Res, CE, Errors) :-
2264 prob2_do_ctl_modelcheck(Formula, [max_new_states(MaxNodes), mode(Mode)], Res, CE),
2265 (Res = type_error(Errors) ->
2266 true %Result = typeerror
2267 ;
2268 %Result = Res,
2269 Errors = []
2270 ).
2271
2272
2273 /* ------------------------- */
2274 /* Find Traces */
2275 /* ------------------------- */
2276
2277 /**
2278 find_trace_to_node(+StateId,-Trace)
2279
2280 Finds a trace from the root state to the specified state in the current state space.
2281
2282 #### Parameters:
2283 * StateId
2284 * 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
2285
2286 #### called by:
2287 * ProB 2.0: GetShortestTraceCommand
2288 */
2289 find_trace_to_node(StateId, Trace) :-
2290 find_trace_from_node_to_node(root, StateId, Trace).
2291
2292 /**
2293 find_trace_from_node_to_node(+FromId,+ToId,-Trace)
2294
2295 Finds a trace from one state to a goal state in the current state space.
2296
2297 #### Parameters:
2298 * FromId - Id of source node
2299 * ToId - Id of destination node
2300 * 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
2301
2302 #### called by:
2303 * ProB 2.0: GetShortestTraceCommand
2304 */
2305 find_trace_from_node_to_node(FromId, ToId, Trace) :-
2306 (tcltk_interface:find_shortest_trace_to_node(FromId, ToId, OpIDs, _TraceIDs) ->
2307 trace_to_op_terms(OpIDs,FromId,Trace);
2308 Trace = no_trace_found
2309 ).
2310
2311 /**
2312 trace_to_op_terms(+ListOpIds,+CurID,-ListOpTerms)
2313
2314 Translates a list of transition ids to a list of terms op(TransId,OpName,SrcId,DestId).
2315 The list must represent a trace,
2316 i. e. the first transition must lead to the source state of the second one,
2317 the second transition to the source state of the third, etc.
2318 */
2319 trace_to_op_terms([],_,[]).
2320 trace_to_op_terms([OpID|T], SrcID, [op(OpID,Name,SrcID,Dest)|OpT]) :-
2321 transition(SrcID,Action,OpID,Dest),
2322 !,
2323 extract_op_name(Action,Name),
2324 trace_to_op_terms(T,Dest,OpT).
2325 trace_to_op_terms([skip|T], SrcID, [op(skip,skip,SrcID,SrcID)|OpT]) :-
2326 trace_to_op_terms(T,SrcID,OpT).
2327
2328 /**
2329 Takes a given predicate and finds a state in the state space that satisfies the predicate.
2330 A helper transition is then added to go to the goal state.
2331
2332 #### called by:
2333 * ProB 2.0: FindValidStateCommand
2334 */
2335 :- use_module(b_state_model_check,[b_set_up_valid_state_with_pred/4]).
2336 find_state_for_predicate(Predicate,UseInvariant,Result) :-
2337 (predicate_typecheck_for_eval(Predicate,TPredicate) ->
2338 find_state_for_predicate1(TPredicate,UseInvariant,Result)
2339 ;
2340 get_all_errors_with_span_info_and_reset(Errors),
2341 Result = errors(Errors)
2342 ).
2343 find_state_for_predicate1(Predicate,UseInvariant,Result) :-
2344 user_interruptable_call_det(clpfd_interface:catch_clpfd_overflow_call1(
2345 b_state_model_check:b_set_up_valid_state_with_pred(State,Predicate,
2346 UseInvariant,none)), % TODO: pass UseConstantsFromStateID
2347 InterruptResult),!,
2348 ( InterruptResult = interrupted ->
2349 Result = interrupted
2350 ; State = time_out ->
2351 Result = interrupted
2352 ;
2353 Result = state_found(Transition,StateId),
2354 % the following is incomplete if State contains constants; TODO: seperate constants
2355 % see tcltk_add_cbc_state which adds an intermediate constants state if necessary
2356 % TODO: we also need to change the state_found/2 result to return a list of transitions
2357 add_artificial_transition(root,find_valid_state,State,StateId,Transition)).
2358 find_state_for_predicate1(_Predicate,_,no_valid_state_found).
2359
2360 /**
2361 cbc_disprove(+Goal,+AllHypotheses,+SelectedHypotheses,+TimeoutFactor,-OutResult)
2362
2363 #### called by:
2364 * ProB Plugin (de.prob.eventb.disprover.core): DisproverCommand
2365 */
2366 cbc_disprove(Goal,AllHypotheses,SelectedHypotheses,TimeoutFactor,OutResult) :-
2367 disprove(Goal,AllHypotheses,SelectedHypotheses,TimeoutFactor,OutResult),
2368 % remove the warning regarding double check, in rodin it is shown in the proof tree anyway
2369 (get_error(warning(disprover_inconsistent_hypotheses),_) ; true).
2370
2371 /**
2372 cbc_disprove(+Goal,+AllHypotheses,+SelectedHypotheses,+TimeoutFactor,-OutResult)
2373
2374 the same with explicit Options:
2375 */
2376 cbc_disprove(Goal,AllHypotheses,SelectedHypotheses,TimeoutFactor,Options,OutResult) :-
2377 % we do not have to add: [use_smt_mode/true,use_clpfd_solver/true,use_chr_solver/true],
2378 % for Rodin these prefs are set in DisproverCommand.java
2379 disprove_with_opts(Goal,AllHypotheses,SelectedHypotheses,TimeoutFactor,Options,OutResult),
2380 % remove the warning regarding double check, in rodin it is shown in the proof tree anyway
2381 (get_error(warning(disprover_inconsistent_hypotheses),_) ; true).
2382
2383 :- assert_must_succeed((cbc_solve_with_opts('PROB',[truncate(10)],
2384 equal(none,identifier(none,x),integer(none,10)),Identifiers,Result),
2385 Identifiers == [x],
2386 check_eqeq(Result,solution([binding(x,int(10),'10')])))).
2387
2388 /**
2389 cbc_solve_with_opts(+Solver,+Options,+Predicate,-Identifiers,-Result)
2390 */
2391 cbc_solve_with_opts(Solver,Options,Predicate,Identifiers,Result) :-
2392 maplist(prob2_interface:check_cbc_solve_opts,Options),
2393 cbc_solve_type(Solver,Options,Predicate,TPredicate),
2394 find_identifier_uses(TPredicate,[],Identifiers),
2395 (select(timeout_factor(TimeoutFactor),Options,Opts2) -> true ; TimeoutFactor=1,Opts2=Options),
2396 cbc_solve_typed(Solver,TPredicate,_,TimeoutFactor,Opts2,Result).
2397
2398 cbc_timed_solve_with_opts(Solver,Options,Predicate,Identifiers,Result,Milliseconds) :-
2399 maplist(prob2_interface:check_cbc_solve_opts,Options),
2400 cbc_solve_type(Solver,Options,Predicate,TPredicate),
2401 find_identifier_uses(TPredicate,[],Identifiers),
2402 (select(timeout_factor(TimeoutFactor),Options,Opts2) -> true ; TimeoutFactor=1,Opts2=Options),
2403 cbc_solve_timed(Solver,TPredicate,_,TimeoutFactor,Opts2,Result,Milliseconds).
2404
2405
2406 check_cbc_solve_opts(full_machine_state) :- !.
2407 check_cbc_solve_opts(solve_in_visited_state(ID)) :- !,atomic(ID).
2408 check_cbc_solve_opts(timeout_factor(Nr)) :- !,number(Nr).
2409 check_cbc_solve_opts(truncate(Nr)) :- !,number(Nr). % truncate pretty printing
2410 check_cbc_solve_opts(truncate) :- !. % truncate pretty printing
2411 check_cbc_solve_opts(force_evaluation) :- !. % force evaluation of symbolic results
2412 check_cbc_solve_opts(provide_stored_let_values) :- !.
2413 check_cbc_solve_opts(all_external_libraries) :- !.
2414 check_cbc_solve_opts(IO) :- add_internal_error('Illegal cbc_solve_with_opts option:',IO).
2415
2416
2417 :- use_module(cdclt_solver('cdclt_solver'), [cdclt_solve_predicate/3,cdclt_solve_predicate_in_state/4]).
2418 :- use_module(probsrc(specfile),[get_state_for_b_formula/3]).
2419 :- use_module(solver_interface, [solver_pp_bvalue/4]).
2420
2421 timed_solve_predicate(Predicate,State,TimeoutFactor,Options,Result,Time) :-
2422 statistics(walltime, [Start, _]),
2423 solve_predicate(Predicate,State,TimeoutFactor,Options,Result),
2424 statistics(walltime, [Stop,_]),
2425 Time is Stop - Start.
2426
2427 cbc_solve_timed('PROB',Predicate,State,TimeoutFactor,Options,Result,Time) :-
2428 timed_solve_predicate(Predicate,State,TimeoutFactor,['SMT','CLPFD'|Options],Result,Time).
2429 cbc_solve_timed('KODKOD',Predicate,State,TimeoutFactor,Options,Result,Time) :-
2430 timed_solve_predicate(Predicate,State,TimeoutFactor,['KODKOD','SMT','CLPFD'|Options],Result,Time).
2431 cbc_solve_timed('SMT_SUPPORTED_INTERPRETER',Predicate,State,TimeoutFactor,Options,Result,Time) :-
2432 timed_solve_predicate(Predicate,State,TimeoutFactor,
2433 ['SMT_SUPPORTED_INTERPRETER','SMT','CLPFD'|Options],Result,Time).
2434 cbc_solve_timed(SOLVER,Predicate,_StateID,_,Options,Result,Time) :-
2435 %TODO: why do we ignore _StateID and TimeoutFactor here?
2436 statistics(walltime, [Start, _]),
2437 (member(solve_in_visited_state(ID),Options)
2438 -> solve_in_state_aux(SOLVER,ID,Predicate,Result)
2439 ; solve_free_aux(SOLVER,Predicate,Result)
2440 ),
2441 statistics(walltime, [Stop,_]),
2442 Time is Stop - Start.
2443
2444 :- use_module(extension('satsolver/b2sat'), [solve_predicate_with_satsolver_free/4,
2445 solve_predicate_with_satsolver_in_state/4]).
2446 solve_in_state_aux('CDCLT',ID,Predicate,Result) :- !,
2447 get_state_for_b_formula(ID, Predicate, Store),
2448 cdclt_solve_predicate_in_state(Predicate, Store, _SolvedPredWdGuaranteed, CdcltResult),
2449 translate_cbc_cdclt_result(CdcltResult, Result).
2450 solve_in_state_aux('SAT',ID,Predicate,Result) :- !,
2451 solve_in_state_sat_aux(ID,Predicate,Result,[]).
2452 solve_in_state_aux('SATZ3',ID,Predicate,Result) :- !,
2453 solve_in_state_sat_aux(ID,Predicate,Result,[use_satsolver(z3)]).
2454 solve_in_state_aux(SOLVER,ID,Predicate,Result) :-
2455 recognised_smt_solver(SOLVER,InternalName),!,
2456 smt_solve_predicate_in_state(ID,InternalName,Predicate,_State,Result).
2457
2458 solve_in_state_sat_aux(ID,Predicate,Result,Opts) :- !,
2459 (ID=root -> solve_predicate_with_satsolver_free(Predicate,_,SatResult,Opts)
2460 ; get_state_for_b_formula(ID, Predicate, Store),
2461 solve_predicate_with_satsolver_in_state(Predicate,Store,SatResult,Opts)
2462 ),
2463 translate_cbc_cdclt_result(SatResult,Result).
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.