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