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