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