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