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