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