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