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/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(pge,PartialGuardEvaluation),
1884 get_preference(por,WithPOR),
1885 tcltk_interface:do_model_check(MaxNumberOfStatesToCheck, _, LimitTime, Res, Deadlock, Invariant, Goal,Assertions,
1886 FindStateErrors,StopAtFullCoverage, WithPOR, PartialGuardEvaluation, InspectExistingNodes),
1887 build_modelcheck_return(Res, Result),
1888 get_state_space_stats(NrNodes, NrTrans, NrProcessed).
1889
1890
1891 /**
1892 set_goal_for_model_checking(+Goal)
1893
1894 Sets the goal for model checking. The Option search_for_goal needs to be set when starting
1895 model checking in order for this to have an effect on the model checking.
1896
1897 #### called by:
1898 * ProB 2.0: SetBGoalCommand
1899 */
1900 set_goal_for_model_checking(Goal) :-
1901 predicate_typecheck_for_eval(Goal,TypedGoal),
1902 b_set_parsed_typed_machine_goal(TypedGoal).
1903
1904 /**
1905 reset_goal_for_model_checking
1906
1907 Reset the goal for model checking. Will remove a saved custom goal and load the goal from DEFINITIONS if it exists.
1908
1909 #### called by:
1910 * ProB 2.0: ResetBGoalCommand
1911 */
1912 :- use_module(probsrc(bmachine), [b_unset_machine_goal/0, b_reset_machine_goal_from_DEFINITIONS/0]).
1913 reset_goal_for_model_checking :-
1914 b_unset_machine_goal,
1915 (b_or_z_mode -> (b_reset_machine_goal_from_DEFINITIONS ; true) ; true),
1916 !.
1917
1918 /**
1919 option_set(+Element, +List, -Result)
1920
1921 Takes an atom and unifies Result with 1 if the atom is in the List.
1922 Otherwise, Result is unified with 0.
1923 */
1924 option_set(Element, List, Result) :-
1925 ( member(Element,List)
1926 -> Result = 1
1927 ; Result = 0).
1928
1929 %! build_modelcheck_return(+MCRes, -JavaResult)
1930 build_modelcheck_return(MCRes, JavaResult) :-
1931 build_modelcheck_return2(MCRes, JavaResult) -> true
1932 ; 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)*/
1933 current_state_id(State), JavaResult=general_error(State, MCRes).
1934
1935 build_modelcheck_return2(no, not_yet_finished(100000)).
1936 build_modelcheck_return2([timeout,N], not_yet_finished(N1)) :- N1 is 100000 - N.
1937 build_modelcheck_return2(deadlock, deadlock(State)):- current_state_id(State).
1938 build_modelcheck_return2(invariant_violation, invariant_violation(State)):- current_state_id(State).
1939 build_modelcheck_return2(xtl_error, xtl_error(State)):- current_state_id(State).
1940 build_modelcheck_return2(assertion_violation, assertion_violation(State)):- current_state_id(State).
1941 build_modelcheck_return2(state_error(_), state_error(State)):- current_state_id(State).
1942 build_modelcheck_return2(goal_found, goal_found(State)) :- current_state_id(State).
1943 build_modelcheck_return2(well_definedness_error, well_definedness_error(State)) :- current_state_id(State).
1944 build_modelcheck_return2(general_error_occurred, general_error(State)):- current_state_id(State).
1945 build_modelcheck_return2(full_coverage, full_coverage).
1946 build_modelcheck_return2(all, Res) :- max_reached_or_timeout_for_node(_),!, Res=ok_not_all_nodes_considered.
1947 build_modelcheck_return2(all, ok).
1948
1949 :- use_module(symbolic_model_checker(bmc),[bmc_symbolic_model_check/1]).
1950 :- use_module(symbolic_model_checker(kinduction), [kinduction_symbolic_model_check/1, tinduction_symbolic_model_check/1]).
1951 :- use_module(symbolic_model_checker(ic3), [ic3_symbolic_model_check/1]).
1952 symbolic_model_check(bmc,Result) :-
1953 bmc_symbolic_model_check(Result).
1954 symbolic_model_check(kinduction,Result) :-
1955 kinduction_symbolic_model_check(Result).
1956 symbolic_model_check(tinduction,Result) :-
1957 tinduction_symbolic_model_check(Result).
1958 symbolic_model_check(ic3,Result) :-
1959 ic3_symbolic_model_check(Result).
1960
1961 /**
1962 compute_efficient_statespace_stats(-NrNodes, -NrTrans, -NrProcessed)
1963
1964 Computes the coverage statistics of the current state space at any given time.
1965 The information of interest includes the total number of nodes and transitions, as well as
1966 a list of statistics about the nodes and operations and a list of the operations that have been uncovered sofar.
1967
1968 #### called by:
1969 * ProB Plugin: ComputeCoverageCommand
1970 * ProB 2.0: ComputeCoverageCommand
1971 */
1972 :- use_module(extrasrc(coverage_statistics),
1973 [compute_the_coverage/5, operation_hit/2,query_node_hit/2, uncovered_operation/1]).
1974
1975 compute_efficient_statespace_stats(NrNodes, NrTrans, NrProcessed) :-
1976 get_state_space_stats(NrNodes, NrTrans, NrProcessed).
1977
1978 %! compute_coverage(-TotalNodeNr,-TotalTransSum,-NodeStat,-OpStat,-Uncovered)
1979 compute_coverage(TotalNodeNr,TotalTransSum,NodeStat,OpStat,Uncovered) :-
1980 compute_the_coverage(_,TotalNodeNr,TotalTransSum,false,false),
1981 findall(S2,(operation_hit(OpS,Nr),string_concatenate(':',Nr,S1),string_concatenate(OpS,S1,S2)),OpStat),
1982 findall(S2,(query_node_hit(Prop,Nr),string_concatenate(':',Nr,S1),string_concatenate(Prop,S1,S2)),NodeStat),
1983 findall(OpName, uncovered_operation(OpName),Uncovered).
1984
1985
1986 get_modelchecking_coverage(TotalNodeNr,TotalTransSum,NodeStat,OpStat,Uncovered) :-
1987 compute_the_coverage(_,TotalNodeNr,TotalTransSum,false,false),
1988 findall(entry(OpS,Nr),operation_hit(OpS,Nr),OpStat),
1989 findall(entry(Prop,Nr),query_node_hit(Prop,Nr),NodeStat),
1990 findall(OpName, uncovered_operation(OpName),Uncovered).
1991
1992 /**
1993 get_statistics(+Option,-Value)
1994
1995 Takes an option for the statistics and returns the corresponding value.
1996
1997 #### called by:
1998 * ProB 2.0: GetStatisticsCommand
1999 */
2000
2001 get_statistics(global_runtime,V) :- statistics(runtime,[V,_]).
2002 get_statistics(global_walltime,V) :- statistics(walltime,[V,_]).
2003 get_statistics(delta_runtime,V) :- statistics(runtime,[_,V]).
2004 get_statistics(delta_walltime,V) :- statistics(walltime,[_,V]).
2005 get_statistics(memory_used,V) :- statistics(memory_used,V).
2006 get_statistics(memory_free,V) :- statistics(memory_free,V).
2007 get_statistics(global_stack_used,V) :- statistics(global_stack_used,V).
2008 get_statistics(local_stack_used,V) :- statistics(local_stack_used,V).
2009 %get_statistics(global_stack_free,V) :- statistics(global_stack_free,V).
2010 %get_statistics(local_stack_free,V) :- statistics(local_stack_free,V).
2011 get_statistics(trail_used,V) :- statistics(trail_used,V).
2012 get_statistics(choice_used,V) :- statistics(choice_used,V).
2013 get_statistics(atoms_used,V) :- statistics(atoms_used,V).
2014 get_statistics(atoms_nbused,V) :- statistics(atoms_nbused,V).
2015 get_statistics(gc_count,V) :- statistics(gc_count,V).
2016 get_statistics(gc_time,V) :- statistics(gc_time,V).
2017
2018 /**
2019 prob2_deadlock_freedom_check(+Predicate,-Result)
2020
2021 Performs deadlock freedom checking with constraint Predicate and calulates the Result.
2022
2023 #### called by:
2024 * ProB 2.0: ConstraintBasedDeadlockCheckCommand
2025 */
2026 prob2_deadlock_freedom_check(Predicate,Result) :-
2027 b_type_expression(Predicate,[variables],pred,TPredicate,Errors),
2028 ( Errors == [] ->
2029 prob2_deadlock_freedom_check1(TPredicate,Result)
2030 ;
2031 Result = errors(Errors)).
2032 prob2_deadlock_freedom_check1(Predicate,Result) :-
2033 % always do a deadlock check with SMT mode enabled
2034 call_with_smt_mode_enabled(prob2_deadlock_freedom_check2(Predicate,Result)).
2035 :- use_module(clpfd_interface,[catch_clpfd_overflow_call1/1]).
2036 :- use_module(b_state_model_check,[cbc_deadlock_freedom_check/3]).
2037 prob2_deadlock_freedom_check2(Predicate,Result) :-
2038 user_interruptable_call_det(clpfd_interface:catch_clpfd_overflow_call1(
2039 b_state_model_check:cbc_deadlock_freedom_check(State,Predicate,0)),
2040 InterruptResult),!,
2041 ( InterruptResult = interrupted ->
2042 Result = interrupted
2043 ; State = time_out ->
2044 Result = interrupted
2045 ;
2046 Result = deadlock(Transition,StateId),
2047 add_artificial_transition(root,deadlock_check,State,StateId,Transition)).
2048 prob2_deadlock_freedom_check2(_Predicate,no_deadlock_found).
2049
2050
2051
2052
2053
2054
2055 /**
2056 prob2_invariant_check(+Ops,-Result)
2057
2058 Performs invariant cbc checking for either for all operations or a list of operations.
2059
2060 #### called by:
2061 * ProB 2.0: ConstraintBasedInvariantCheckCommand
2062 */
2063 prob2_invariant_check(all,Result) :-
2064 findall(OpName,b_is_op_or_init(OpName),Ops),
2065 % TO DO: also treat $initailise_machine; but state_model_check_invariant does not support it yet
2066 prob2_invariant_check2(Ops,Result).
2067 prob2_invariant_check(ops(Ops),Result) :-
2068 prob2_invariant_check2(Ops,Result).
2069 prob2_invariant_check2(Ops,Result) :-
2070 call_with_smt_mode_enabled(prob2_invariant_check3(Ops,Result,[])).
2071 prob2_invariant_check3([]) --> !.
2072 prob2_invariant_check3([Op|Rest]) -->
2073 prob2_invariant_check_for_single_op(Op),
2074 prob2_invariant_check3(Rest).
2075 prob2_invariant_check_for_single_op(OpName,In,Out) :-
2076 ( clpfd_interface:catch_clpfd_overflow_call1(
2077 b_state_model_check:state_model_check_invariant(OpName,State1,Operation,State2)) ->
2078 In = [counterexample(OpName,Trans1,Trans2)|Out],
2079 atom_concat( invariant_check_ , OpName, RootTrans),
2080 add_artificial_transition(root, RootTrans,State1,StateId1,Trans1),
2081 add_artificial_transition(StateId1,Operation,State2,_StateId2,Trans2)
2082 ;
2083 In = Out).
2084
2085 b_is_op_or_init(OpName) :- b_is_operation_name(OpName).
2086 b_is_op_or_init(OpName) :- b_is_initialisation_name(OpName).
2087
2088 :- use_module(b_state_model_check,[cbc_find_redundant_invariants/2]).
2089 prob2_redundant_invariants(Redundant, Timeout) :-
2090 cbc_find_redundant_invariants(Redundant, Timeout).
2091
2092 /**
2093 add_artificial_transition(+SrcId,+Operation,+DstState,+DstId,-TransitionTuple)
2094
2095 creates a helper transition that is artificially added to the state space (e.g. during deadlock checking)
2096 This transition is added to the state space.
2097 A triple TransitionTuple in the form op(TransId,OpName,SrcId,DstId) for this transition is generated.
2098 */
2099 add_artificial_transition(SrcId,Operation,DstState,DstId,TransitionTuple) :-
2100 tcltk_interface:tcltk_add_new_transition_transid(SrcId,Operation,DstId,DstState,[],TransId),
2101 extract_op_name(Operation,OpName),
2102 TransitionTuple = op(TransId,OpName,SrcId,DstId).
2103
2104 /**
2105 computes the enabling relation information for the provided operations of interest
2106 get_enable_matrix(-PairsOfOperations,+EnableResult)
2107 PairsOfOperations: list of pair(Op1,Op2) of operations pairs for which the enable relation is to be computed
2108 EnableResult: list of terms enable_edges(Op1,Op2,enable_edges(E,KE,D,KD)) of same length
2109 */
2110 get_enable_matrix(PairsOfOperations,EnableResult) :-
2111 maplist(compute_enable_matrix_entry(100),PairsOfOperations,EnableResult).
2112
2113 :- use_module(cbcsrc(enabling_analysis),[compute_cbc_enable_rel/4]).
2114 compute_enable_matrix_entry(ExtraTimeout,pair(OpName1,OpName2),
2115 enable_rel(OpName1,OpName2,
2116 enable_edges(Enable,KeepEnabled,Disable,KeepDisabled))) :-
2117 compute_cbc_enable_rel(OpName1,OpName2,ExtraTimeout,[Enable,KeepEnabled,Disable,KeepDisabled]).
2118
2119 /**
2120 prob2_do_ltl_modelcheck(+Formula,+Options,-Result)
2121
2122 Performs an LTL model checking step.
2123
2124 Supported options:
2125 * max_new_states(Max) - maximum number of new states that will be explored, or -1 (the default) for no limit
2126 * mode(Mode) - init (the default) to check starting from every initialized state, or specific_node(StateID) to check starting from one specific state
2127
2128 #### called by:
2129 * ProB 2.0: LtlCheckingCommand
2130 */
2131 prob2_do_ltl_modelcheck(Formula, Options, Result) :-
2132 (selectchk(max_new_states(Max), Options, Options1) -> true ; Max = -1, Options1 = Options),
2133 (selectchk(mode(Mode), Options1, Options2) -> true ; Mode = init, Options2 = Options1),
2134 Options2 == [],
2135
2136 typecheck_temporal_formula(Formula,TypeCheckedFormula,Status),
2137 (Status=ok ->
2138 ltl_model_check_with_ce(TypeCheckedFormula,Max,Mode,Result1),
2139 prob2_ltl_adapt_operations(Result1,Result)
2140 ;
2141 get_all_errors_with_span_info_and_reset(Errors),
2142 Result = type_error(Errors)
2143 ).
2144
2145 % Old command without option list - can be removed after release of ProB Java API 4.14.0.
2146 prob2_do_ltl_modelcheck(Formula,Max,Result,Errors) :-
2147 prob2_do_ltl_modelcheck(Formula, [max_new_states(Max)], Res),
2148 (Res = type_error(Errors) ->
2149 Result = typeerror
2150 ;
2151 Result = Res,
2152 Errors = []
2153 ).
2154
2155 prob2_ltl_adapt_operations(counterexample(CE1,LoopEntry,PathToCE1), Res) :- !,
2156 Res = counterexample(CE,LoopEntry,PathToCE),
2157 create_simple_op_terms(PathToCE1,root,PathToCE),
2158 prob2_ltl_adapt_ce(CE1,CE).
2159 prob2_ltl_adapt_operations(Result,Result).
2160
2161 prob2_ltl_adapt_ce([],[]).
2162 prob2_ltl_adapt_ce([atom(StateId,_,OpTuple)|Irest],[Transition|Orest]) :-
2163 prob2_ltl_adapt_ce2(OpTuple,StateId,Transition),
2164 prob2_ltl_adapt_ce(Irest,Orest).
2165 prob2_ltl_adapt_ce2(none,_StateId,none).
2166 prob2_ltl_adapt_ce2((TransId,Action,DestId),StateId,op(TransId,Name,StateId,DestId)) :-
2167 extract_op_name(Action,Name).
2168
2169
2170 /**
2171 prob2_do_ctl_modelcheck(+Formula, +Options, -Result, -CE)
2172
2173 Performs an CTL model checking step.
2174
2175 Supported options:
2176 * max_new_states(Max) - maximum number of new states that will be explored, or -1 (the default) for no limit
2177 * mode(Mode) - init (the default) to check starting from every initialized state, or specific_node(StateID) to check starting from one specific state
2178
2179 #### called by:
2180 * ProB 2.0: CtlCheckingCommand
2181 */
2182 prob2_do_ctl_modelcheck(Formula, Options, Result, CE) :-
2183 (selectchk(max_new_states(Max), Options, Options1) -> true ; Max = -1, Options1 = Options),
2184 (selectchk(mode(Mode), Options1, Options2) -> true ; Mode = init, Options2 = Options1),
2185 Options2 == [],
2186
2187 typecheck_temporal_formula(Formula, TypeCheckedFormula, Status),
2188 (Status = ok ->
2189 ctl_model_check_with_ast(main, TypeCheckedFormula, Max, Mode, Result, CE)
2190 ;
2191 get_all_errors_with_span_info_and_reset(Errors),
2192 Result = type_error(Errors),
2193 CE = [] % no counter example
2194 ).
2195
2196 % Old command without option list - can be removed after release of ProB Java API 4.14.0.
2197 prob2_do_ctl_modelcheck(Formula, MaxNodes, Mode, Res, CE, Errors) :-
2198 prob2_do_ctl_modelcheck(Formula, [max_new_states(MaxNodes), mode(Mode)], Res, CE),
2199 (Res = type_error(Errors) ->
2200 true %Result = typeerror
2201 ;
2202 %Result = Res,
2203 Errors = []
2204 ).
2205
2206
2207 /* ------------------------- */
2208 /* Find Traces */
2209 /* ------------------------- */
2210
2211 /**
2212 find_trace_to_node(+StateId,-Trace)
2213
2214 Finds a trace from the root state to the specified state in the current state space.
2215
2216 #### Parameters:
2217 * StateId
2218 * 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
2219
2220 #### called by:
2221 * ProB 2.0: GetShortestTraceCommand
2222 */
2223 find_trace_to_node(StateId, Trace) :-
2224 find_trace_from_node_to_node(root, StateId, Trace).
2225
2226 /**
2227 find_trace_from_node_to_node(+FromId,+ToId,-Trace)
2228
2229 Finds a trace from one state to a goal state in the current state space.
2230
2231 #### Parameters:
2232 * FromId - Id of source node
2233 * ToId - Id of destination node
2234 * 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
2235
2236 #### called by:
2237 * ProB 2.0: GetShortestTraceCommand
2238 */
2239 find_trace_from_node_to_node(FromId, ToId, Trace) :-
2240 (tcltk_interface:find_shortest_trace_to_node(FromId, ToId, OpIDs, _TraceIDs) ->
2241 trace_to_op_terms(OpIDs,FromId,Trace);
2242 Trace = no_trace_found
2243 ).
2244
2245 /**
2246 trace_to_op_terms(+ListOpIds,+CurID,-ListOpTerms)
2247
2248 Translates a list of transition ids to a list of terms op(TransId,OpName,SrcId,DestId).
2249 The list must represent a trace,
2250 i. e. the first transition must lead to the source state of the second one,
2251 the second transition to the source state of the third, etc.
2252 */
2253 trace_to_op_terms([],_,[]).
2254 trace_to_op_terms([OpID|T], SrcID, [op(OpID,Name,SrcID,Dest)|OpT]) :-
2255 transition(SrcID,Action,OpID,Dest),
2256 !,
2257 extract_op_name(Action,Name),
2258 trace_to_op_terms(T,Dest,OpT).
2259 trace_to_op_terms([skip|T], SrcID, [op(skip,skip,SrcID,SrcID)|OpT]) :-
2260 trace_to_op_terms(T,SrcID,OpT).
2261
2262 /**
2263 Takes a given predicate and finds a state in the state space that satisfies the predicate.
2264 A helper transition is then added to go to the goal state.
2265
2266 #### called by:
2267 * ProB 2.0: FindValidStateCommand
2268 */
2269 :- use_module(b_state_model_check,[b_set_up_valid_state_with_pred/4]).
2270 find_state_for_predicate(Predicate,UseInvariant,Result) :-
2271 (predicate_typecheck_for_eval(Predicate,TPredicate) ->
2272 find_state_for_predicate1(TPredicate,UseInvariant,Result)
2273 ;
2274 get_all_errors_with_span_info_and_reset(Errors),
2275 Result = errors(Errors)
2276 ).
2277 find_state_for_predicate1(Predicate,UseInvariant,Result) :-
2278 user_interruptable_call_det(clpfd_interface:catch_clpfd_overflow_call1(
2279 b_state_model_check:b_set_up_valid_state_with_pred(State,Predicate,UseInvariant,none)), % TODO: pass UseConstantsFromStateID
2280 InterruptResult),!,
2281 ( InterruptResult = interrupted ->
2282 Result = interrupted
2283 ; State = time_out ->
2284 Result = interrupted
2285 ;
2286 Result = state_found(Transition,StateId),
2287 % the following is incomplete if State contains constants;
2288 % see tcltk_add_cbc_state which adds an intermediate constants state if necessary
2289 % TODO: we also need to change the state_found/2 result to return a list of transitions
2290 add_artificial_transition(root,find_valid_state,State,StateId,Transition)).
2291 find_state_for_predicate1(_Predicate,_,no_valid_state_found).
2292
2293 /**
2294 cbc_disprove(+Goal,+AllHypotheses,+SelectedHypotheses,+TimeoutFactor,-OutResult)
2295
2296 #### called by:
2297 * ProB Plugin (de.prob.eventb.disprover.core): DisproverCommand
2298 */
2299 cbc_disprove(Goal,AllHypotheses,SelectedHypotheses,TimeoutFactor,OutResult) :-
2300 disprove(Goal,AllHypotheses,SelectedHypotheses,TimeoutFactor,OutResult),
2301 % remove the warning regarding double check, in rodin it is shown in the proof tree anyway
2302 (get_error(warning(disprover_inconsistent_hypotheses),_) ; true).
2303
2304 /**
2305 cbc_disprove(+Goal,+AllHypotheses,+SelectedHypotheses,+TimeoutFactor,-OutResult)
2306
2307 the same with explicit Options:
2308 */
2309 cbc_disprove(Goal,AllHypotheses,SelectedHypotheses,TimeoutFactor,Options,OutResult) :-
2310 % we do not have to add: [use_smt_mode/true,use_clpfd_solver/true,use_chr_solver/true],
2311 % for Rodin these prefs are set in DisproverCommand.java
2312 disprove_with_opts(Goal,AllHypotheses,SelectedHypotheses,TimeoutFactor,Options,OutResult),
2313 % remove the warning regarding double check, in rodin it is shown in the proof tree anyway
2314 (get_error(warning(disprover_inconsistent_hypotheses),_) ; true).
2315
2316 :- assert_must_succeed((cbc_solve_with_opts('PROB',[truncate(10)],
2317 equal(none,identifier(none,x),integer(none,10)),Identifiers,Result),
2318 Identifiers == [x],
2319 check_eqeq(Result,solution([binding(x,int(10),'10')])))).
2320
2321 /**
2322 cbc_solve_with_opts(+Solver,+Options,+Predicate,-Identifiers,-Result)
2323 */
2324 cbc_solve_with_opts(Solver,Options,Predicate,Identifiers,Result) :-
2325 maplist(prob2_interface:check_cbc_solve_opts,Options),
2326 cbc_solve_type(Solver,Options,Predicate,TPredicate),
2327 find_identifier_uses(TPredicate,[],Identifiers),
2328 (select(timeout_factor(TimeoutFactor),Options,Opts2) -> true ; TimeoutFactor=1,Opts2=Options),
2329 ? cbc_solve_typed(Solver,TPredicate,_,TimeoutFactor,Opts2,Result).
2330
2331 cbc_timed_solve_with_opts(Solver,Options,Predicate,Identifiers,Result,Milliseconds) :-
2332 maplist(prob2_interface:check_cbc_solve_opts,Options),
2333 cbc_solve_type(Solver,Options,Predicate,TPredicate),
2334 find_identifier_uses(TPredicate,[],Identifiers),
2335 (select(timeout_factor(TimeoutFactor),Options,Opts2) -> true ; TimeoutFactor=1,Opts2=Options),
2336 cbc_solve_timed(Solver,TPredicate,_,TimeoutFactor,Opts2,Result,Milliseconds).
2337
2338
2339 check_cbc_solve_opts(full_machine_state) :- !.
2340 check_cbc_solve_opts(solve_in_visited_state(ID)) :- !,atomic(ID).
2341 check_cbc_solve_opts(timeout_factor(Nr)) :- !,number(Nr).
2342 check_cbc_solve_opts(truncate(Nr)) :- !,number(Nr). % truncate pretty printing
2343 check_cbc_solve_opts(truncate) :- !. % truncate pretty printing
2344 check_cbc_solve_opts(force_evaluation) :- !. % force evaluation of symbolic results
2345 check_cbc_solve_opts(provide_stored_let_values) :- !.
2346 check_cbc_solve_opts(all_external_libraries) :- !.
2347 check_cbc_solve_opts(IO) :- add_internal_error('Illegal cbc_solve_with_opts option:',IO).
2348
2349
2350 :- use_module(cdclt_solver('cdclt_solver'), [cdclt_solve_predicate/3,cdclt_solve_predicate_in_state/4]).
2351 :- use_module(probsrc(specfile),[get_state_for_b_formula/3]).
2352 :- use_module(solver_interface, [solver_pp_bvalue/4]).
2353
2354 timed_solve_predicate(Predicate,State,TimeoutFactor,Options,Result,Time) :-
2355 statistics(walltime, [Start, _]),
2356 solve_predicate(Predicate,State,TimeoutFactor,Options,Result),
2357 statistics(walltime, [Stop,_]),
2358 Time is Stop - Start.
2359
2360 cbc_solve_timed('PROB',Predicate,State,TimeoutFactor,Options,Result,Time) :-
2361 timed_solve_predicate(Predicate,State,TimeoutFactor,['SMT','CLPFD'|Options],Result,Time).
2362 cbc_solve_timed('KODKOD',Predicate,State,TimeoutFactor,Options,Result,Time) :-
2363 timed_solve_predicate(Predicate,State,TimeoutFactor,['KODKOD','SMT','CLPFD'|Options],Result,Time).
2364 cbc_solve_timed('SMT_SUPPORTED_INTERPRETER',Predicate,State,TimeoutFactor,Options,Result,Time) :-
2365 timed_solve_predicate(Predicate,State,TimeoutFactor,
2366 ['SMT_SUPPORTED_INTERPRETER','SMT','CLPFD'|Options],Result,Time).
2367 cbc_solve_timed(SOLVER,Predicate,_StateID,_,Options,Result,Time) :-
2368 %TODO: why do we ignore _StateID and TimeoutFactor here?
2369 statistics(walltime, [Start, _]),
2370 (member(solve_in_visited_state(ID),Options)
2371 -> solve_in_state_aux(SOLVER,ID,Predicate,Result)
2372 ; solve_free_aux(SOLVER,Predicate,Result)
2373 ),
2374 statistics(walltime, [Stop,_]),
2375 Time is Stop - Start.
2376
2377 :- use_module(extension('satsolver/b2sat'), [solve_predicate_with_satsolver_free/4,
2378 solve_predicate_with_satsolver_in_state/4]).
2379 solve_in_state_aux('CDCLT',ID,Predicate,Result) :- !,
2380 get_state_for_b_formula(ID, Predicate, Store),
2381 cdclt_solve_predicate_in_state(Predicate, Store, _SolvedPredWdGuaranteed, CdcltResult),
2382 translate_cbc_cdclt_result(CdcltResult, Result).
2383 solve_in_state_aux('SAT',ID,Predicate,Result) :- !,
2384 solve_in_state_sat_aux(ID,Predicate,Result,[]).
2385 solve_in_state_aux('SATZ3',ID,Predicate,Result) :- !,
2386 solve_in_state_sat_aux(ID,Predicate,Result,[use_satsolver(z3)]).
2387 solve_in_state_aux(SOLVER,ID,Predicate,Result) :-
2388 recognised_smt_solver(SOLVER,InternalName),!,
2389 smt_solve_predicate_in_state(ID,InternalName,Predicate,_State,Result).
2390
2391 solve_in_state_sat_aux(ID,Predicate,Result,Opts) :- !,
2392 (ID=root -> solve_predicate_with_satsolver_free(Predicate,_,SatResult,Opts)
2393 ; get_state_for_b_formula(ID, Predicate, Store),
2394 solve_predicate_with_satsolver_in_state(Predicate,Store,SatResult,Opts)
2395 ),
2396 translate_cbc_cdclt_result(SatResult,Result),
2397 print(sat_result(Result)),nl.
2398
2399 solve_free_aux('CDCLT',Predicate,Result) :- !,
2400 cdclt_solve_predicate(Predicate, _SolvedPredWdGuaranteed, CdcltResult),
2401 translate_cbc_cdclt_result(CdcltResult, Result).
2402 solve_free_aux('SAT',Predicate,Result) :-
2403 solve_predicate_with_satsolver_free(Predicate,_,SatResult,[]),
2404 translate_cbc_cdclt_result(SatResult,Result).
2405 solve_free_aux('SATZ3',Predicate,Result) :-
2406 solve_predicate_with_satsolver_free(Predicate,_,SatResult,[use_satsolver(z3)]),
2407 translate_cbc_cdclt_result(SatResult,Result).
2408 solve_free_aux(SOLVER,Predicate,Result) :-
2409 recognised_smt_solver(SOLVER,InternalName),!,
2410 smt_solve_predicate(InternalName,Predicate,_State,Result).
2411
2412 cbc_solve_typed(Solver,Predicate,State,TimeoutFactor,Options,Result) :-
2413 ? cbc_solve_timed(Solver,Predicate,State,TimeoutFactor,Options,Result,_).
2414
2415 % As CDCL(T) does not pretty print its results, we need this translation,
2416 % as CbcSolveCommand expects the pretty print.
2417 % In case no solution was found, the original CDCL(T) result can be forwarded.
2418 translate_cbc_cdclt_result(solution(NonPPBindings), solution(Bindings)) :-
2419 !,
2420 findall(binding(Id,EValue,PPValue),
2421 (member(bind(Id,Value),NonPPBindings),
2422 (solver_pp_bvalue(Value,[],EValue,PPValue) -> true
2423 ; EValue=Value, PPValue='**pretty-print failed**')),
2424 Bindings).
2425 translate_cbc_cdclt_result(Result, Result).
2426
2427
2428
2429 recognised_smt_solver('Z3',z3).
2430 recognised_smt_solver('Z3CNS',z3cns).
2431 recognised_smt_solver('Z3AXM',z3axm).
2432 recognised_smt_solver('CVC4',cvc4).
2433
2434 :- use_module(preferences,[temporary_set_preference/3,reset_temporary_preference/2]).
2435 cbc_solve_type('KODKOD',Options,Pred,TPred) :- !,
2436 temporary_set_preference(use_solver_on_load,kodkod,C),
2437 call_cleanup(cbc_solve_type2(Options,Pred,TPred),
2438 reset_temporary_preference(use_solver_on_load,C)).
2439 cbc_solve_type(_,Options,Pred,TPred) :- cbc_solve_type2(Options,Pred,TPred).
2440 cbc_solve_type2(Options,Pred,TPred) :-
2441 !, get_eval_scope_with_opts(Options,Scope),
2442 b_type_open_predicate(no_quantifier,Pred,Scope,TPred,Errors),
2443 (Errors=[] -> true ; add_error_and_fail(cbc_solve_type, 'Type-Errors: ', Errors)).
2444
2445
2446 :- use_module(code2vec(code2vec),[leaf_paths/2]).
2447 ast_leaf_walks(B, Walks) :-
2448 cbc_solve_type2([], B, TypedB),
2449 leaf_paths(TypedB, Walks).
2450
2451 /**
2452 Takes a predicates and generates a pretty printed string
2453 */
2454 :- assert_must_succeed((pretty_print_predicate(equal(none,identifier(none,x),integer(none,1)),[],Result),
2455 check_eqeq(Result,'x = 1'))).
2456 :- assert_must_succeed((pretty_print_predicate(not_equal(none,identifier(none,x),integer(none,1)),[latex],Result),
2457 check_eqeq(Result,'\\mathit{x} \\neq 1'))).
2458 :- assert_must_succeed((pretty_print_predicate(not_equal(pos(2,-1,1,1,1,7),integer(pos(3,-1,1,1,1,2),1),
2459 integer(pos(4,-1,1,6,1,7),2)),[latex,nopt],PPString),
2460 check_eqeq(PPString,'1 \\neq 2' ))).
2461
2462 pretty_print_predicate(Pred,Options,PPString) :-
2463 ? select(nopt,Options,Opts2),
2464 !,
2465 temporary_set_preference(optimize_ast,false,CHNG1),
2466 call_cleanup(pretty_print_predicate(Pred,Opts2,PPString),
2467 reset_temporary_preference(optimize_ast,CHNG1)).
2468 pretty_print_predicate(Pred,Options,PPString) :-
2469 get_eval_scope_with_opts(Options,Scope),
2470 b_type_open_predicate(no_quantifier,Pred,Scope,TPred,Errors),
2471 (Errors=[] -> true ; add_error_and_fail(pretty_print_predicate, 'Type-Errors: ', Errors)),
2472 options_to_translation_mode(Options, Mode),
2473 with_translation_mode(Mode, translate_bexpression(TPred,PPString)).
2474
2475 options_to_translation_mode(Options, Mode) :- memberchk(latex, Options), !, Mode = latex.
2476 options_to_translation_mode(Options, Mode) :- memberchk(unicode, Options), !, Mode = unicode.
2477 options_to_translation_mode(_Options, ascii).
2478
2479 % Constraint-Based Test-case generation
2480 % TO DO: return values
2481 :- use_module(cbcsrc(sap),[cbc_gen_test_cases/5]).
2482 cbc_generate_test_cases(TargetPred,MaxDepth,OutputFile) :-
2483 % I am not sure whether we should call b_parse_machine_predicate(TargetPred,...) or not
2484 Events = all,
2485 cbc_gen_test_cases(Events,TargetPred,MaxDepth,OutputFile,_Uncovered).
2486
2487
2488
2489 :- use_module(cbcsrc(cbc_path_solver),[create_testcase_path/5]).
2490 /**
2491 prob2_find_test_path(+Events,+EndPredicate,+TimeoutMs,-ResultOpTerms)
2492
2493 example call | ?- prob2_interface:prob2_find_test_path([enter1],truth(unknown),200,R).
2494
2495 Result is either errors(Errors), timeout, interrupt, infeasible_path, or list of Operation IDs
2496 */
2497 prob2_find_test_path(Events,EndPredicate,TimeoutMs,ResultOpTerms) :-
2498 (predicate_typecheck_for_eval(EndPredicate,TPredicate) ->
2499 prob2_find_test_path_aux(Events,TPredicate,TimeoutMs,ResultOpTerms)
2500 ;
2501 get_all_errors_with_span_info_and_reset(Errors),
2502 ResultOpTerms = errors(Errors)
2503 ).
2504
2505 prob2_find_test_path_aux(Events,TPredicate,TimeoutMs,ResOperationIds) :-
2506 ( create_testcase_path(init,Events,TPredicate,TimeoutMs,Trace)
2507 -> (is_list(Trace) -> maplist(extract_opid,Trace,ResOperationIds)
2508 % Trace can be "timeout" or "interrupt", too
2509 ; ResOperationIds=Trace)
2510 ; ResOperationIds = infeasible_path).
2511
2512 extract_opid((TransId,OpTerm,StateId,DestId),op(TransId,Name,StateId,DestId)) :- extract_op_name(OpTerm,Name).
2513
2514 /* ------------------------- */
2515 /* Check CSP Assertion */
2516 /* ------------------------- */
2517
2518 /**
2519 check_csp_assertions(+Assertions,-Results,-ResultTraces)
2520
2521 Takes a list of assertions and produce a list of results and result traces.
2522
2523 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)
2524
2525 #### called by:
2526 * ProB 2.0: CSPAssertionsCommand
2527 */
2528 check_csp_assertions(Assertions,Results,ResultTraces) :-
2529 maplist(check_csp_assertion,Assertions,Results,ResultTraces).
2530
2531 check_csp_assertion(AssClause,Res,ResTrace1) :-
2532 read_from_codes(AssClause,Assertion),
2533 tcltk_interface:checkAssertion(Assertion,_PP,_Negated,Res,ResTrace),
2534 (ResTrace = no_counter_example -> ResTrace1 = []; ResTrace1=ResTrace).
2535
2536 /* ------------------------- */
2537 /* Preferences Interface */
2538 /* ------------------------- */
2539
2540 /**
2541 list_current_eclipse_preferences(-L)
2542
2543 Returns a list of all the preferences with their current values
2544
2545 #### called by:
2546 * ProB 2.0: GetCurrentPreferencesCommand
2547 */
2548 list_current_eclipse_preferences(L) :-
2549 findall(preference(A,B),find_eclipse_preference(A,B),L).
2550
2551 find_eclipse_preference(A,B) :-
2552 list_all_eclipse_preferences(X),
2553 member(preference(A,_,_,_,_),X),
2554 get_eclipse_preference(A,B).
2555
2556 /**
2557 Returns the current value of a specified preference.
2558
2559 #### called by:
2560 * ProB 2.0: GetPreferenceCommand
2561 */
2562 get_eclipse_preference(PrefS,PrefVal) :-
2563 if(eclipse_preference(PrefS,PS),
2564 get_preference(PS,PrefVal),
2565 add_unknown_preference_error_and_fail(get_eclipse_preference,PrefS)).
2566
2567 /**
2568 list_eclipse_preferences(-L)
2569
2570 Returns a list of all normal eclipse preferences as well as their information
2571 (i.e. type, description, category, and default value)
2572
2573 #### called by:
2574 * ProB Plugin: GetPreferencesCommand
2575 * ProB 2.0: GetDefaultPreferencesCommand
2576 */
2577 list_eclipse_preferences(L) :-
2578 findall(preference(A,B,C,D,E),
2579 (get_eclipse_preference_infos(A,B,C,D,E),
2580 \+ advanced_eclipse_preference(A,_)), L).
2581
2582 /**
2583 list_all_eclipse_preferences(-L)
2584
2585 also includes advanced eclipse preferences
2586 */
2587 list_all_eclipse_preferences(L) :-
2588 findall(preference(A,B,C,D,E),get_eclipse_preference_infos(A,B,C,D,E),L).
2589
2590 get_eclipse_preference_infos(PrefString,Type,Description,Category,DefaultValue) :-
2591 eclipse_preference(PrefString,PS),
2592 %\+ advanced_eclipse_preference(PrefString,PS), % we now want to show all preferences in ProB 2
2593 preference_val_type(PS,Type),
2594 preference_description(PS,Description),
2595 preference_category(PS,Category),
2596 preference_default_value(PS,DefaultValue).
2597
2598 /**
2599 set_eclipse_preference(+PrefS,+PrefVal)
2600
2601 Sets a preference
2602
2603 #### called by:
2604 * ProB Plugin: SetPreferenceCommand
2605 * ProB 2.0: SetPreferenceCommand
2606 */
2607 :- use_module(tools_strings, [convert_cli_arg/2]).
2608 set_eclipse_preference(PrefS,PrefVal) :-
2609 convert_cli_arg(PrefVal,Value),
2610 convert_pref_value(Value,CValue),
2611 ? (eclipse_preference(PrefS,P)
2612 -> safe_set_pref(P,CValue,Value)
2613 ; deprecated_eclipse_preference(PrefS,_,NewP,Mapping),
2614 ? member(CValue/NewVal,Mapping)
2615 -> add_message(set_eclipse_preference,'Deprecated preference: ',PrefS),
2616 safe_set_pref(NewP,NewVal,Value)
2617 ; obsolete_eclipse_preference(PrefS)
2618 -> add_warning(set_eclipse_preference,'Obsolete preference: ',PrefS) % just warn and continue
2619 ; add_unknown_preference_error_and_fail(set_eclipse_preference,PrefS)
2620 ).
2621
2622 safe_set_pref(P,CValue,Value) :-
2623 (set_preference(P,CValue)
2624 -> true
2625 ; ajoin(['Could not set preference ',P,' to: '],Msg),
2626 add_error(set_eclipse_preference,Msg,Value)
2627 ).
2628
2629 convert_pref_value('TRUE',V) :- !, V=true.
2630 convert_pref_value('FALSE',V) :- !, V=false.
2631 convert_pref_value(X,X).
2632
2633 :- use_module(tools_matching,[get_possible_preferences_matches_msg/2]).
2634 add_unknown_preference_error_and_fail(Source,PrefS) :-
2635 obsolete_eclipse_preference(PrefS),!,
2636 add_error_and_fail(Source,'Obsolete preference: ',PrefS).
2637 add_unknown_preference_error_and_fail(Source,PrefS) :-
2638 get_possible_preferences_matches_msg(PrefS,FuzzyMsg),!,
2639 ajoin(['Unknown preference: ',PrefS,'. Did you mean: '],Msg),
2640 add_error_and_fail(Source,Msg,FuzzyMsg).
2641 add_unknown_preference_error_and_fail(Source,PrefS) :-
2642 add_error_and_fail(Source,'Unknown preference: ',PrefS).
2643
2644 /* ------------------------- */
2645 /* Apply Graph reduction */
2646 /* ------------------------- */
2647
2648 /**
2649 get_signature_merge_state_space(+IgnoredEvents,-Space)
2650
2651 Takes a list of ignored events, and applies the signature merge algorithm
2652 from module `state_space_reduction` to the current state space.
2653
2654 #### called by:
2655 * ProB 2.0: ApplySignatureMergeCommand
2656 */
2657 get_signature_merge_state_space(IgnoredEvents,Space) :-
2658 reset_ignored_events,
2659 set_ignored_events(IgnoredEvents),
2660 compute_signature_merge,
2661 findall(node(NodeId,Count,Color,Labels),extract_node_info(NodeId,Count,Color,simple_list,Labels),Nodes),
2662 findall(trans(TransId,Src,Dest,Label,Style,Color),extract_trans_info(true,TransId,Src,Dest,Label,Style,Color),Trans),
2663 Space = [Nodes,Trans].
2664
2665 /**
2666 get_transition_diagram(+ParsedExpr,-Space)
2667
2668 Takes a list of ignored events, and calculates a transition diagram
2669 using module `state_space_reduction` for the current state space.
2670
2671 #### called by:
2672 * ProB 2.0: CalculateTransitionDiagramCommand
2673 */
2674 get_transition_diagram(ParsedExpr,Space) :-
2675 expression_typecheck_for_eval(ParsedExpr,TypedExpr),
2676 compute_transition_diagram(TypedExpr),
2677 findall(node(NodeId,Count,Color,Labels),extract_node_info(NodeId,Count,Color,gen_label,Labels),Nodes),
2678 findall(trans(TransId,Src,Dest,Label,Style,Color),extract_trans_info(false,TransId,Src,Dest,Label,Style,Color),Trans),
2679 Space = [Nodes,Trans].
2680
2681 write_dotty_transition_diagram(Expression,Filename) :-
2682 write_dotty_for_expr(transition_diagram,Expression,Filename).
2683
2684 write_dotty_signature_merge(IgnoredEvents,Filename) :-
2685 write_signature_merge_to_dotfile(IgnoredEvents,Filename).
2686
2687 write_dotty_state_space(Filename) :-
2688 write_dotty(state_space,Filename).
2689
2690 :- use_module(extrasrc(meta_interface),[is_dot_command/1, call_dot_command/3]).
2691 % find out which commands only require a filename:
2692 is_dotty_command(Command) :- is_dot_command(Command).
2693 % call commands which generate a dot file (without requiring further arguments, such as an expression)
2694 write_dotty(Command,Filename) :- OptionalArgs=[],
2695 call_dot_command(Command,Filename,OptionalArgs).
2696
2697
2698 :- use_module(extrasrc(meta_interface),[is_dot_command_for_expr/1, call_dot_command_for_expr/4]).
2699 % find out which commands only require an expression and a filename:
2700 is_dotty_command_for_expr(Command) :- is_dot_command_for_expr(Command).
2701 % call commands which generate a dot file from an expression:
2702 write_dotty_for_expr(Command,Expr,Filename) :- OptionalArgs=[],
2703 call_dot_command_for_expr(Command,Expr,Filename,OptionalArgs).
2704
2705
2706 :- use_module(extrasrc(meta_interface),[is_plantuml_command/1, call_plantuml_command/3]).
2707 :- use_module(extrasrc(meta_interface),[is_plantuml_command_for_expr/1, call_plantuml_command_for_expr/4]).
2708 :- use_module(extrasrc(meta_interface),[command_unavailable/2]).
2709
2710 % --------------------------------------------------------
2711 % New preferred API for calling DOT / TABLE commands in ProB2 JFX:
2712 % get_dot_commands_in_state/2 and call_dot_command_in_state/4
2713 % get_planuml_commands_in_state/2 and call_plantuml_command_in_state/4
2714 % get_table_commands_in_state/2 and call_table_command_in_state/4
2715
2716 get_commands_in_state(Category,StateID,List) :-
2717 tcltk_interface:tcltk_try_goto_node_with_id(StateID),
2718 findall(command(Command,Name,Description,NumberOfFormulaArgs,RelevantEclipsePrefs,AdditionalInfo,AvailMsg),
2719 (is_a_command(Category,Command,Name,Description,NumberOfFormulaArgs,RelevantPrefs,AdditionalInfo),
2720 maplist(convert_pref,RelevantPrefs,RelevantEclipsePrefs),
2721 (command_unavailable(Command,AvailMsg) -> true ; AvailMsg = available)),
2722 List).
2723 get_commands_with_trace(Category,TransIDs,List) :-
2724 try_set_trace_by_transition_ids(TransIDs),
2725 findall(command(Command,Name,Description,NumberOfFormulaArgs,RelevantEclipsePrefs,AdditionalInfo,AvailMsg),
2726 (is_a_command(Category,Command,Name,Description,NumberOfFormulaArgs,RelevantPrefs,AdditionalInfo),
2727 maplist(convert_pref,RelevantPrefs,RelevantEclipsePrefs),
2728 (command_unavailable(Command,AvailMsg) -> true ; AvailMsg = available)),
2729 List).
2730
2731 % example call: prob2_interface:get_dot_commands_in_state(1,List).
2732 get_dot_commands_in_state(StateID,List) :- get_commands_in_state(dot,StateID,List).
2733 get_dot_commands_with_trace(TransIDs,List) :- get_commands_with_trace(dot,TransIDs,List).
2734 % example call: prob2_interface:get_plantuml_commands_in_state(1,List).
2735 get_plantuml_commands_in_state(StateID,List) :- get_commands_in_state(plantuml,StateID,List).
2736 get_plantuml_commands_with_trace(TransIDs,List) :- get_commands_with_trace(plantuml,TransIDs,List).
2737 % example call: prob2_interface:get_table_commands_in_state(1,List).
2738 get_table_commands_in_state(StateID,List) :- get_commands_in_state(table,StateID,List).
2739 get_table_commands_with_trace(TransIDs,List) :- get_commands_with_trace(table,TransIDs,List).
2740
2741 convert_pref(Pref,Res) :- eclipse_preference(ECLIPSEPREF,Pref),!,Res=ECLIPSEPREF.
2742 convert_pref(P,P) :- preference_default_value(P,_),!.
2743 convert_pref(P,P) :- print(unknown_preference(P)),nl.
2744
2745 :- use_module(extrasrc(meta_interface),[is_dot_command/6, is_plantuml_command/6, is_table_command/6]).
2746 is_a_command(dot,Command,Name,Description,NumberOfFormulaArgs,RelevantPreferences,AdditionalInfo) :-
2747 is_dot_command(Command,Name,Description,NumberOfFormulaArgs,RelevantPreferences,AdditionalInfo).
2748 is_a_command(plantuml,Command,Name,Description,NumberOfFormulaArgs,RelevantPreferences,AdditionalInfo) :-
2749 is_plantuml_command(Command,Name,Description,NumberOfFormulaArgs,RelevantPreferences,AdditionalInfo).
2750 is_a_command(table,Command,Name,Description,NumberOfFormulaArgs,RelevantPreferences,AdditionalInfo) :-
2751 is_table_command(Command,Name,Description,NumberOfFormulaArgs,RelevantPreferences,AdditionalInfo).
2752
2753
2754 call_dot_command_in_state(StateID,Command,Formulas,DotFile) :-
2755 tcltk_interface:tcltk_try_goto_node_with_id(StateID),
2756 call_dot_command_for_dotfile(Command,Formulas,DotFile).
2757 call_dot_command_with_trace(TransIDs,Command,Formulas,DotFile) :-
2758 try_set_trace_by_transition_ids(TransIDs),
2759 call_dot_command_for_dotfile(Command,Formulas,DotFile).
2760
2761 % call a dot command for generating a DotFile; used by call_dot_command_in_state
2762 call_dot_command_for_dotfile(Command,[],DotFile) :-
2763 is_dot_command(Command), !, OptionalArgs=[],
2764 call_dot_command(Command,DotFile,OptionalArgs).
2765 call_dot_command_for_dotfile(Command,[Expr],DotFile) :-
2766 is_dot_command_for_expr(Command), !, OptionalArgs=[],
2767 call_dot_command_for_expr(Command,Expr,DotFile,OptionalArgs).
2768 call_dot_command_for_dotfile(Command,Formulas,DotFile) :-
2769 add_internal_error('Illegal dot call: ',call_dot_command_for_dotfile(Command,Formulas,DotFile)),
2770 fail.
2771
2772
2773 call_plantuml_command_in_state(StateID,Command,Formulas,UmlFile) :-
2774 tcltk_interface:tcltk_try_goto_node_with_id(StateID),
2775 call_plantuml_command_for_pumlfile(Command,Formulas,UmlFile).
2776 call_plantuml_command_with_trace(TransIDs,Command,Formulas,UmlFile) :-
2777 try_set_trace_by_transition_ids(TransIDs),
2778 call_plantuml_command_for_pumlfile(Command,Formulas,UmlFile).
2779
2780 % call a plantuml command for generating a UmlFile; used by call_plantuml_command_in_state
2781 call_plantuml_command_for_pumlfile(Command,[],UmlFile) :-
2782 is_plantuml_command(Command), !, OptionalArgs=[],
2783 call_plantuml_command(Command,UmlFile,OptionalArgs).
2784 call_plantuml_command_for_pumlfile(Command,[Expr],UmlFile) :-
2785 is_plantuml_command_for_expr(Command), !, OptionalArgs=[],
2786 call_plantuml_command_for_expr(Command,Expr,UmlFile,OptionalArgs).
2787 call_plantuml_command_for_pumlfile(Command,Formulas,UmlFile) :-
2788 add_internal_error('Illegal plantuml call: ',call_dot_command_for_pumlfile(Command,Formulas,UmlFile)),
2789 fail.
2790
2791 % example call: prob2_interface:call_table_command_in_state(1,expr_as_table,[integer(pos,1)],Table).
2792 :- use_module(extrasrc(meta_interface),[call_command/5]).
2793 call_table_command_in_state(StateID,Command,Formulas,TableResult) :-
2794 tcltk_interface:tcltk_try_goto_node_with_id(StateID),
2795 append(Formulas,[TableResult],ActualArgs),
2796 OptionalArgs=[],
2797 debug_println(9,call_command(table,Command,_,ActualArgs,OptionalArgs)),
2798 call_command(table,Command,_,ActualArgs,OptionalArgs), debug_println(9,result(TableResult)),
2799 !.
2800 call_table_command_in_state(StateID,Command,Formulas,TableResult) :-
2801 add_error(call_table_command_in_state,'Table command failed:',call_table_command_in_state(StateID,Command,Formulas,TableResult)),
2802 TableResult = list([list(['ERROR OCCURED'])]).
2803
2804 call_table_command_with_trace(TransIDs,Command,Formulas,TableResult) :-
2805 try_set_trace_by_transition_ids(TransIDs),
2806 append(Formulas,[TableResult],ActualArgs),
2807 OptionalArgs=[],
2808 debug_println(9,call_command(table,Command,_,ActualArgs,OptionalArgs)),
2809 call_command(table,Command,_,ActualArgs,OptionalArgs), debug_println(9,result(TableResult)),
2810 !.
2811 call_table_command_with_trace(TransIDs,Command,Formulas,TableResult) :-
2812 add_error(call_table_command_with_trace,'Table command failed:',call_table_command_with_trace(TransIDs,Command,Formulas,TableResult)),
2813 TableResult = list([list(['ERROR OCCURED'])]).
2814
2815
2816 /**
2817 write_dot_for_state_viz(+StateId, +Filename)
2818
2819 Writes a dot representation of the given state to the specified file.
2820
2821 */
2822 write_dot_for_state_viz(StateId, Filename) :-
2823 get_state(StateId, State),
2824 print_cstate_graph(State, Filename).
2825
2826 /**
2827 extract_node_info(+NodeId,-Count,-Color,+LabelGenerator,-Labels)
2828
2829 Generates information about the nodes found during state space reduction
2830
2831 #### Generated Information:
2832 * Count - number of concrete states combined in the abstract state
2833 * Color - the color used to represent this state type in a visualization
2834 * Labels - determine the labels that should appear on a node in a visualization
2835 */
2836 extract_node_info(NodeId,Count,Color,LabelGenerator,Labels) :-
2837 get_reduced_node(AbsState,Count,Witness,NodeId),
2838 generate_node_color(NodeId,Witness,AbsState,Count,Color),
2839 generate_node_labels(LabelGenerator,AbsState,Labels).
2840
2841 /**
2842 extract_trans_info(+ShowSelfLoops,+TransId,-Src,-Dest,-Label,-Style,-Color)
2843
2844 Generates information about the transitions created during state space reduction
2845
2846 #### Generated Information:
2847 * Src - ID corresponding to the abstract state that is the source of the abstract transition with TransId
2848 * Dest - ID corresponding to the abstract state that is the destination of the abstract transition with TransId
2849 * Label - the label that should appear on a transition in a visualization
2850 * Style - the style that should be applied to a transition of this type in a visualization (e.g. dashed)
2851 * Color - the color used to represent a transition of this type in a visualization
2852 */
2853 extract_trans_info(ShowSelfLoops,TransId,Src,Dest,Label,Style,Color) :-
2854 reduced_trans(Src,AbsAction,Count,Dest,TransId),
2855 generate_transition_label(AbsAction,Count,Label),
2856 generate_transition_color_and_style(ShowSelfLoops,Src,AbsAction,Dest,Color,Style).
2857
2858
2859 /* ------------------ */
2860 /* Get Errors */
2861 /* ------------------ */
2862
2863 /**
2864 get_error_messages_with_span_info(-ListOfErrMsgTerms)
2865
2866 each error is of the form: error(ErrMsg,ErrType,ErrLocations)
2867 ErrMsg is an atom (aka string)
2868 ErrType is warning, internal_error or error
2869 ErrLocations is a list of terms error_span(Filename,StartLine,StartCol,EndLine,EndCol)
2870 Note: Filename is '' when not known
2871
2872 #### called by:
2873 * ProB 2.0: GetErrorItemsCommand
2874 */
2875 get_error_messages_with_span_info(ListOfErrMsgTerms) :-
2876 ignore_user_interrupt_det(get_all_errors_with_span_info_and_reset(ListOfErrMsgTerms)).
2877 % TODO: replace by this:
2878 % error(ErrMsg,ErrType,ErrLocations,GlobalContext,CallStack)
2879 %get_error_messages_with_span_and_contxt(ListOfErrMsgTerms) :-
2880 % ignore_user_interrupt_det(get_all_errors_with_span_and_context_and_reset(ListOfErrMsgTerms)).
2881
2882
2883 % ####################
2884
2885 /**
2886 generate_trace_until_condition_fulfilled(+CurState,+Condition,-Trace,-Result)
2887
2888 Animates randomly number of steps until a certain (LTL?) condition is fulfilled.
2889
2890 #### Called by:
2891 * ProB 2.0: ExecuteUntilCommand
2892
2893 #### Arguments
2894 * CurState - the ID of the current state
2895 * Condition - a condition that should be satisfied at some point (this come as parsed term from the ProB2)
2896
2897 #### Generated Information:
2898 * Trace - a list of triples representing a trace in the state space of the model being analysed
2899 * Result - the result found: ltl_found, typeerror, max_nr_of_steps_reached, deadlock
2900 */
2901 generate_trace_until_condition_fulfilled(CurState,Condition,Trace,Result) :-
2902 typecheck_temporal_formula(Condition,TypeCheckedCondition,Status),
2903 ( Status=ok -> find_trace1(CurState,TypeCheckedCondition,no_loop,100000,Trace, Result) %FIXME: turn maximal numver of steps into an argument?
2904 ; reset_errors, % Reset errors. We don't want to throw a ProBError on the Java side because the result is capsuled in Result.
2905 Result=typeerror, Trace=[]).
2906
2907 find_trace1(StateId,Ltl,Type,MaxSteps,OpTripleResultTrace, Result) :-
2908 (MaxSteps =< 0
2909 -> add_error(find_trace,'Number of maximum animation steps should be a positive integer. The number of steps which was given is ',MaxSteps)
2910 ; true),
2911 set_current_state(StateId), !, % can be backtracked
2912 % negate -> counterexample is the trace we are looking for
2913 preprocess_formula(Ltl,Ltl2),
2914 find_trace_aux(StateId,not(Ltl2),Type,0,MaxSteps,ResultTrace,ResultTrace,Names,Result),
2915 gen_op_triples(ResultTrace,Names,OpTripleResultTrace).
2916 %(gen_op_triples(ResultTrace,OpTripleResultTrace) -> print(ok(OpTripleResultTrace,result(Result))),nl
2917 % ; add_error_and_fail(prob2_interface,'trace not correctly generated',ResultTrace)).
2918
2919 find_trace_aux(CurID,Condition,Type,_N,_Max,StateTransitionHistory,[],[],RESULT) :-
2920 debug_println(9,checking_ltl_formula(CurID,StateTransitionHistory)),
2921 evaluate_ltl_formula(Condition,StateTransitionHistory,Type,ltl:check_ap,ltl:callback_tp,EvResult),
2922 EvResult = false,
2923 !,
2924 RESULT=ltl_found.
2925 find_trace_aux(CurID,Condition,Type,N,Max,StateTransitionHistory,STTail,Names,RESULT) :-
2926 tcltk_interface:tcltk_compute_options(CurID,ActionsAndIDs),
2927 debug_println(9,opts(ActionsAndIDs)),
2928 ( N=Max
2929 -> debug_println(9,'Maximum number of animation steps reached.'),
2930 Names = [],
2931 RESULT = maximum_nr_of_steps_reached
2932 ; pick_action(random,ActionsAndIDs,ActionId,Name,DstID) % pick first one; we could do random
2933 -> debug_println(9,performing_action(ActionId,from_to(CurID,DstID),opts(ActionsAndIDs))),
2934 STTail = [strans(CurID,ActionId)|STTail2],
2935 Names = [Name|Names2],
2936 N1 is N+1,
2937 find_trace_aux(DstID,Condition,Type,N1,Max,StateTransitionHistory,STTail2,Names2,RESULT)
2938 ; STTail=[], Names = [], RESULT = deadlock
2939 ).
2940
2941 gen_op_triples([],[],[]).
2942 gen_op_triples([_X],[_Y],[]).
2943 gen_op_triples([strans(CurID,ActionId),strans(DstID,ActId)|T],[Name|NameT],[op(ActionId,Name,CurID,DstID)|Rest]) :-
2944 gen_op_triples([strans(DstID,ActId)|T],NameT,Rest).
2945
2946 :- use_module(library(random)).
2947 :- use_module(library(lists)).
2948 pick_action(first,[(ActionId,Term,DstID)|_], ActionId, Name, DstID) :- extract_op_name(Term,Name).
2949 pick_action(random,Options,ActionId, Name, DstID) :-
2950 length(Options,Len),
2951 L1 is Len+1,
2952 random(1,L1,RanChoice),
2953 debug_println(9,random(RanChoice,Len)),
2954 nth1(RanChoice,Options,(ActionId,ActionAsTerm,DstID)),
2955 extract_op_name(ActionAsTerm,Name).
2956
2957
2958 % -------------------------------------
2959
2960 /**
2961 execute_model(+CurStateID,+MaxNrSteps,-TransitionInfo,-ExecutedSteps,-Result)
2962
2963 an execution engine with minimal overhead: states are not stored in visited_expression database, only first enabled operation is taken
2964 */
2965 execute_model(CurStateID,MaxNrSteps,TransitionInfo,ExecutedSteps,Result) :-
2966 temporary_set_preference(try_operation_reuse,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(try_operation_reuse,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', ActTerm='$JUMP'('EXECUTE'(ExecutedSteps))),
2987 (memberchk(return_trace,Options)
2988 -> TransitionInfo = Transitions
2989 ; add_artificial_transition(CurStateID,ActTerm,NewState,ToID,Transition),
2990 debug_println(4,added_transition_for_execute(ExecutedSteps,ToID)),
2991 TransitionInfo = [Transition])
2992 ; TransitionInfo = none).
2993
2994 execute_model_steps(StepNr,CurState,_CurStateID,MaxNrSteps,_Options,PrevAction,PrevTrans,NewState,ExecutedSteps,LastAction,Transitions,Result) :-
2995 StepNr >= MaxNrSteps,!,
2996 NewState=CurState,
2997 ExecutedSteps=StepNr,
2998 LastAction=PrevAction,
2999 Transitions=PrevTrans,
3000 Result=maximum_nr_of_steps_reached.
3001 execute_model_steps(StepNr,CurState,CurStateID,MaxNrSteps,Options,PrevAction,PrevTrans,NewState,ExecutedSteps,LastAction,Transitions,Result) :-
3002 cli_trans_aux(StepNr,CurState,Options,ActionName,ActTerm,State2,ErrorRes),
3003 !,
3004 debug_println(20,execute(StepNr,ActionName)),
3005 S1 is StepNr+1,
3006 (nonvar(ErrorRes)
3007 -> Result=ErrorRes, ExecutedSteps=StepNr, NewState=CurState, LastAction=PrevAction
3008 ; PrevAction2=act(ActionName,ActTerm),
3009 (memberchk(return_trace,Options)
3010 -> (transition(CurStateID,ActTerm,TransID,ToID)
3011 -> Transition = op(TransID,ActionName,CurStateID,ToID)
3012 ; add_artificial_transition(CurStateID,ActTerm,State2,ToID,Transition),
3013 debug_println(4,added_transition_for_execute(ExecutedSteps,ToID))
3014 ),
3015 append(PrevTrans,[Transition],PrevTrans2)
3016 ; PrevTrans2 = []),
3017 execute_model_steps(S1,State2,ToID,MaxNrSteps,Options,PrevAction2,PrevTrans2,NewState,ExecutedSteps,LastAction,Transitions,Result)).
3018 execute_model_steps(Steps,CurState,_CurStateID,_,_Options,PrevAction,Transitions,CurState,Steps,PrevAction,Transitions,deadlock).
3019
3020 :- use_module(specfile,[specfile_possible_trans_name_for_successors/2,prepare_state_for_specfile_trans/3,
3021 specfile_trans_or_partial_trans/7]).
3022 :- use_module(error_manager,[throw_enumeration_warnings_in_current_scope/0, add_internal_error/2, error_occurred_in_error_scope/0]).
3023 :- use_module(tools_meta,[safe_time_out/3]).
3024
3025 % TO DO: use same optimisation as in -execute in prob_cli.pl (get_possible_next_operation_for_execute)
3026 cli_trans_aux(StepNr,CurState,Options,ActionName,Act,NewState,ErrorRes) :-
3027 specfile_possible_trans_name_for_successors(CurState,ActionName),
3028 catch_enumeration_warning_exceptions(
3029 (throw_enumeration_warnings_in_current_scope,
3030 (member(timeout(MS),Options) ->
3031 safe_time_out(specfile_trans_or_partial_trans(CurState,ActionName,Act,NewState,_TransInfo1,Residue,_),MS,TR)
3032 ; specfile_trans_or_partial_trans(CurState,ActionName,Act,NewState,_TransInfo2,Residue,_) % no time-out !
3033 ),
3034 (TR==time_out
3035 -> add_error(execute,'Timeout occured during execute after step: ',StepNr),ErrorRes=time_out
3036 ; error_occurred_in_error_scope ->
3037 (member(continue_after_errors,Options) -> true
3038 ; add_error(execute,'Error occured during execute after step: ',StepNr),ErrorRes=error)
3039 ; true)
3040 ),
3041 (add_error(virtual_time_out_execute,'Virtual TIME-OUT occured during execute after step: ',StepNr),
3042 ActionName = '*** VIRTUAL_TIME_OUT ***', Act=ActionName,
3043 ErrorRes=time_out)
3044 ),
3045 (Residue=[] -> true
3046 ; add_internal_error('Residue during execute after step: ',StepNr:Residue),
3047 (nonvar(ErrorRes) -> true ; ErrorRes=internal_error)).
3048
3049 % -------------------------------------
3050
3051 % computes a unsat core
3052 :- use_module(tools,[start_ms_timer/1, stop_ms_walltimer_with_msg/2]).
3053 get_unsat_core_with_fixed_conjuncts(Pred,FixedPreds,CoreOut) :-
3054 typecheck_pred_for_unsat_core(Pred,TypedPred),
3055 maplist(typecheck_pred_for_unsat_core,FixedPreds,TypedFixedPreds),
3056 conjunct_predicates(TypedFixedPreds,Conj),
3057 format('Computing an unsat core~n',[]), start_ms_timer(Timer),
3058 unsat_chr_core_with_fixed_conjuncts_auto_time_limit(TypedPred,Conj,2000,Core),
3059 stop_ms_walltimer_with_msg(Timer,'Computed unsat core'),
3060 translate_bexpression(Core,CoreOut).
3061
3062 % computes the unsat core of minimal size:
3063 get_minimum_unsat_core_with_fixed_conjuncts(Pred,FixedPreds,CoreOut) :-
3064 typecheck_pred_for_unsat_core(Pred,TypedPred),
3065 maplist(typecheck_pred_for_unsat_core,FixedPreds,TypedFixedPreds),
3066 conjunct_predicates(TypedFixedPreds,Conj),
3067 format('Computing the minimal unsat core~n',[]),
3068 minimum_unsat_core_with_fixed_conjuncts(TypedPred,Conj,Core),
3069 translate_bexpression(Core,CoreOut).
3070
3071 typecheck_pred_for_unsat_core(PIn,POut) :-
3072 predicate_typecheck_for_eval(PIn,TExpr),
3073 (get_texpr_expr(TExpr,exists(_,POut)) -> true
3074 ; format(user_error,'Predicate for unsat core is not existentially quantified~n',[]),
3075 POut = TExpr).
3076
3077 /**
3078 Access information about the current version of the ProB core.
3079
3080 #### called by:
3081 * ProB 2.0: GetInternalRepresentationPrettyPrintCommand
3082 */
3083 :- use_module(specfile,[get_internal_representation/1]).
3084 get_pretty_print(PP) :-
3085 get_internal_representation(PPC),
3086 atom_codes(PP,PPC).
3087
3088 get_pretty_print_unicode(PP) :-
3089 with_translation_mode(unicode,get_pretty_print(PP)).
3090
3091 :- use_module(specfile, [get_internal_representation/4]).
3092 :- use_module(translate, [set_print_type_infos/1]).
3093 :- use_module(bmachine, [b_get_eventb_machine_as_classicalb_codes/3]).
3094 /**
3095 Pretty-print the machine's internal representation in B syntax.
3096
3097 #### called by:
3098 * ProB 2.0: GetInternalRepresentationCommand
3099 prob2_interface:get_machine_internal_representation([translation_mode(atelierb)],PP).
3100 */
3101 get_machine_internal_representation(Options, PP) :-
3102 (selectchk(translation_mode(TransMode), Options, Options1) -> true ; TransMode = ascii, Options1 = Options),
3103 (selectchk(type_infos(TypeInfos), Options1, Options2) -> true ; TypeInfos = none, Options2 = Options1),
3104 Options2 == [],
3105 ((TransMode=atelierb ; TransMode=atelierb_pp) -> AdditionalInfo=false, UnsetMinorMode = true
3106 ; AdditionalInfo=true, UnsetMinorMode = false),
3107 (animation_minor_mode(eventb), TransMode=atelierb
3108 -> with_translation_mode(TransMode, b_get_eventb_machine_as_classicalb_codes(_,AdditionalInfo,PPC))
3109 % above will set type infos to true !
3110 ; with_translation_mode(TransMode, get_internal_representation(PPC, AdditionalInfo, UnsetMinorMode, TypeInfos))
3111 ),
3112 atom_codes(PP, PPC).
3113
3114
3115
3116 % Gets a names of the given operations
3117 unpack_operation(ListOfOperation, NamesOfOperations) :-
3118 unpack_operation_aux(ListOfOperation, NamesOfOperations).
3119 unpack_operation_aux([b(operation(Name, _, _, _))|T], [Name|T1]):-
3120 unpack_operation_aux(T, T1).
3121 unpack_operation_aux([], []).
3122
3123 :- use_module(bmachine, [b_get_machine_operation/4, b_get_machine_operation_for_animation/4,
3124 b_safe_get_initialisation_from_machine/2]).
3125 get_operations_and_names(Ops, Names) :-
3126 findall(b(operation(Name, OutputParameters, InputParameter, Body)),
3127 %b_get_machine_operation(Name, OutputParameters, InputParameter, Body),
3128 b_get_machine_op_for_anim_with_otype(Name, OutputParameters, InputParameter, Body, _),
3129 AllOperations),
3130 unpack_operation(AllOperations, AllNames),
3131 (b_safe_get_initialisation_from_machine(Body, _)
3132 -> Ops = [b(initialisation(Body))|AllOperations], Names = ['$initialise_machine'|AllNames]
3133 ; Ops = AllOperations, Names = AllNames
3134 ).
3135
3136
3137 :- use_module(symbolic_model_checker(predicate_handling),[prime_predicate/2]).
3138 get_primed_predicate(Pred,PrimedPredOut) :-
3139 predicate_typecheck_for_eval(Pred,POutT),
3140 prime_predicate(POutT,PrimedPred),
3141 translate_bexpression(PrimedPred,PrimedPredOut).
3142
3143 % Version of get_primed_predicate/2 which does not introduce an existential quantifier.
3144 get_nonquantifying_primed_predicate(Pred,PrimedPredOut) :-
3145 temporary_set_preference(optimize_ast,false,CHNG1),
3146 call_cleanup(get_nonquantifying_primed_predicate_2(Pred,PrimedPredOut),
3147 reset_temporary_preference(optimize_ast,CHNG1)).
3148
3149 get_nonquantifying_primed_predicate_2(Pred, PrimedPredOut) :-
3150 get_eval_scope(Scope),
3151 (\+ bmachine:b_machine_is_loaded ->
3152 bmachine:b_set_empty_machine % Ensure a machine is loaded someway or another.
3153 ; true
3154 ),
3155 b_type_open_predicate(no_quantifier, Pred, Scope, Typed, Errors),
3156 (Errors=[] -> true ; add_error_and_fail(get_primed_predicate, 'Type-Errors: ', Errors)),
3157 prime_predicate(Typed, PrimedPred),
3158 translate_bexpression(PrimedPred,PrimedPredOut).
3159
3160
3161 :- use_module(extrasrc(weakest_preconditions),[weakest_precondition/3]).
3162 :- use_module(preferences, [call_with_preference/3]).
3163 get_weakest_precondition(OpName,Pred,WPOut) :-
3164 % TODO: call with preference can be removed once ProB 2 reads ASTs instead of reparsing
3165 call_with_preference(get_weakest_precondition_aux(OpName,Pred,WPOut),translate_ids_to_parseable_format,true).
3166 get_weakest_precondition_aux(OpName,Pred,WPOut) :-
3167 b_get_machine_operation(OpName,_Results,_Parameters,OpBody),
3168 predicate_typecheck_for_eval(Pred,POutT),
3169 weakest_precondition(OpBody,POutT,WP),
3170 translate_bexpression(WP,WPOut).
3171
3172 :- use_module(extrasrc(before_after_predicates),[before_after_predicate_for_operation/2]).
3173 before_after_predicate(OpName,PredicateOut) :-
3174 call_with_preference(before_after_predicate_aux(OpName,PredicateOut),translate_ids_to_parseable_format,true).
3175 before_after_predicate_aux(OpName,PredicateOut) :-
3176 before_after_predicate_for_operation(OpName,Predicate),
3177 translate_bexpression(Predicate,PredicateOut).
3178
3179 /** Synthesis Commands:
3180 *
3181 #### b_synthesis:start_synthesis_from_ui/13 called by:
3182 * ProB 2.0: BSynthesisCommand
3183 */
3184 start_synthesis_from_ui_(SynthesisMode,AdaptMachineCode,SolverTimeOut,Library,DoNotUseConstants,Solver,ConsiderIfVarNames,Operation,SynthesisType,Positive,Negative,NewMachineAtom,Distinguishing) :-
3185 start_synthesis_from_ui(SynthesisMode,AdaptMachineCode,SolverTimeOut,Library,DoNotUseConstants,Solver,ConsiderIfVarNames,Operation,SynthesisType,Positive,Negative,NewMachineAtom,Distinguishing).
3186
3187 /*
3188 #### b_synthesis:start_synthesis_single_operation_from_ui/11 called by:
3189 * BSynthesis: StartSynthesisCommand
3190 */
3191 start_synthesis_single_operation_from_ui_(SolverTimeOut,Operations,Library,DoNotUseConstants,Solver,Operation,action,Positive,Negative,CacheOperationTuple,Distinguishing) :-
3192 start_synthesis_single_operation_from_ui(SolverTimeOut,Operations,Library,DoNotUseConstants,Solver,Operation,action,Positive,Negative,CacheOperationTuple,Distinguishing).
3193
3194 /*
3195 #### b_synthesis:reset_synthesis_context/0 called by:
3196 * ProB 2.0: ResetBSynthesisCommand
3197 */
3198 reset_synthesis_context_ :- reset_synthesis_context.
3199
3200 /*
3201 #### synthesis_util:get_invariant_violating_vars_from_examples/3 called by:
3202 * BSynthesis: GetViolatingVarsFromExamples
3203 */
3204 get_invariant_violating_vars_from_examples_(Positive,Negative,ViolatingVarNames) :-
3205 get_invariant_violating_vars_from_examples(Positive,Negative,ViolatingVarNames).
3206
3207 /*
3208 #### synthesis_util:get_valid_and_invalid_equality_predicates_for_operation/6 called by:
3209 * BSynthesis: VisualizeOperationCommand
3210 */
3211 get_valid_and_invalid_equality_predicates_for_operation_(OperationName,ValidAmount,InvalidAmount,ValidPrettyEqualityTuples,InvalidPrettyEqualities,IgnoredIDs) :-
3212 get_valid_and_invalid_equality_predicates_for_operation(OperationName,ValidAmount,InvalidAmount,ValidPrettyEqualityTuples,InvalidPrettyEqualities,IgnoredIDs).
3213
3214 /*
3215 #### synthesis_util:get_valid_and_invalid_equality_predicates_for_invariants/4 called by:
3216 * BSynthesis: VisualizeInvariantsCommand
3217 */
3218 get_valid_and_invalid_equality_predicates_for_invariants_(ValidAmount,InvalidAmount,ValidPrettyEqualities,InvalidPrettyEqualities) :-
3219 get_valid_and_invalid_equality_predicates_for_invariants(ValidAmount,InvalidAmount,ValidPrettyEqualities,InvalidPrettyEqualities).
3220
3221 /*
3222 #### synthesis_util:adapt_machine_code_for_operations/2 called by:
3223 * BSynthesis: AdaptMachineCodeForOperationsCommand
3224 */
3225 adapt_machine_code_for_operations_(Operations,NewMachineAtom) :-
3226 adapt_machine_code_for_operations(Operations,NewMachineAtom).
3227
3228 /*
3229 #### predicate_data_generator:generate_synthesis_data_from_predicate_untyped_/5 called by:
3230 * BSynthesisDataGenerator: SynthesisDataFromPredicateCommand
3231 */
3232 generate_synthesis_data_from_predicate_untyped_(MachinePath, AugmentRecords, SolverTimeoutMs, UntypedPredAst, AugmentedSetOfData) :-
3233 generate_synthesis_data_from_predicate_untyped(MachinePath, AugmentRecords, SolverTimeoutMs, UntypedPredAst, AugmentedSetOfData).
3234
3235 /*
3236 #### operation_data_generator:generate_operation_data_from_machine_path_/4 called by:
3237 * BSynthesisDataGenerator: SynthesisDataFromOperationCommand
3238 */
3239 generate_operation_data_from_machine_path_(MachinePath, AugmentRecords, SolverTimeoutMs, OperationData) :-
3240 generate_operation_data_from_machine_path(MachinePath, AugmentRecords, SolverTimeoutMs, OperationData).
3241
3242 /*
3243 #### operation_data_generator:generate_data_from_machine_operation_/6 called by:
3244 * BSynthesisDataGenerator: SynthesisDataFromOperationCommand
3245 */
3246 generate_data_from_machine_operation_(OperationName, Augmentations, SolverTimeoutMs, AbsoluteFilePath, MachineName, OperationData) :-
3247 generate_data_from_machine_operation(OperationName, Augmentations, SolverTimeoutMs, AbsoluteFilePath, MachineName, OperationData).
3248
3249 /*
3250 #### called by:
3251 * ProB 2.0: GetMachineOperationNamesCommand
3252 */
3253 :- use_module(probcspsrc(haskell_csp),[channel/2]).
3254
3255 csp_channel_or_start('start_cspm_MAIN').
3256 csp_channel_or_start('start_cspm'). % TO DO: do we also need to support print channel ?
3257 csp_channel_or_start(Name) :- channel(Name,_).
3258
3259 get_machine_operation_names(MachineOperationNames) :- b_or_z_mode,!,
3260 findall(MachineOperationName,b_is_operation_name(MachineOperationName),MachineOperationNames).
3261 get_machine_operation_names(ChannelNames) :- csp_mode,!,
3262 findall(Name, csp_channel_or_start(Name),ChannelNames).
3263 get_machine_operation_names([]).
3264
3265 :- use_module(probsrc(bsyntaxtree), [get_texpr_id/2]).
3266 :- use_module(probsrc(bmachine),[b_get_operation_non_det_modifies/2, b_get_operation_normalized_read_write_info/3]).
3267 % get list of operation info terms of the form
3268 % operation_info(Name,ResultNames,ParameterNames,TopLevel,OType)
3269 % where ResultNames and ParameterNames are list of atomic names
3270 % TopeLevel is true if the operation is a top-level operation for animation/model checking
3271 % OType is classic, csp or eventb_operation %was eventb_operation(ChangeSet,ParaValues,Operation)
3272 get_machine_operation_infos(MachineOperationInfos) :- b_or_z_mode,!,
3273 % TODO: ensure that we do not need to consider preference(show_eventb_any_arguments,EVENTB)
3274 % TODO: examine what happens for CSP||B
3275 findall(operation_info(Name,ResultNames,ParameterNames,TopLevel,OTypeF,Read,Modified,NonDetModifies),
3276 (b_get_machine_op_for_anim_with_otype(Name, Results, AnimParameters,_, OType),
3277 maplist(get_texpr_id,Results,ResultNames),
3278 maplist(get_texpr_id,AnimParameters,ParameterNames),
3279 functor(OType,OTypeF,_),
3280 % TO DO: obtain machine file or machine name
3281 (b_top_level_operation(Name) -> TopLevel = true ; TopLevel=false),
3282 (b_get_operation_normalized_read_write_info(Name,OpRead,Modified)
3283 -> exclude(op_id,OpRead,Read)
3284 % exclude query operations called in expressions (allow_operation_calls_in_expr);
3285 %ProB2 Java cannot deal with it and raises exception for non-atomic identifiers
3286 ; Read=unknown,Modified=unknown
3287 ),
3288 (b_get_operation_non_det_modifies(Name,NonDetModifies) -> true ; NonDetModifies=unknown)
3289 ),
3290 MachineOperationInfos).
3291 get_machine_operation_infos(ChannelInfos) :- csp_mode,!,
3292 findall(operation_info(Name,[],[],true,csp,[],[],[]), csp_channel_or_start(Name),ChannelInfos).
3293 get_machine_operation_infos(Infos) :- xtl_mode,!,
3294 findall(operation_info(Name,[],ParaNames,true,xtl,[],[],[]),
3295 xtl_interface:xtl_transition_parameters(Name,ParaNames),
3296 Infos).
3297 get_machine_operation_infos([]).
3298
3299 % get the operation for animation (possibly lifting ANY identifiers to paramaters) and returning OType
3300 b_get_machine_op_for_anim_with_otype(Name, Results, AnimParameters, AnimBody, OType) :-
3301 b_get_machine_operation(Name, _Results, _RealParameters,_RealBody,OType,_OpPos),
3302 b_get_machine_operation_for_animation(Name, Results, AnimParameters, AnimBody).
3303
3304 :- use_module(library(lists)).
3305 %%Same as untyped
3306 get_machine_operation_infos_typed(MachineOperationInfos) :- b_or_z_mode,!,
3307 % TODO: ensure that we do not need to consider preference(show_eventb_any_arguments,EVENTB)
3308 % TODO: examine what happens for CSP||B
3309 findall(operation_info(Name,ResultNames,ParameterNames,TopLevel,OTypeF,Read,Modified,NonDetModifies, TypeMap),
3310 (b_get_machine_op_for_anim_with_otype(Name, Results, AnimParameters,_, OType),
3311
3312 maplist(get_texpr_id,Results,ResultNames),
3313 maplist(get_texpr_type, Results,ResultTypes),
3314 keys_and_values(ResultMap, ResultNames, ResultTypes),
3315 maplist(get_texpr_id,AnimParameters,ParameterNames),
3316 maplist(get_texpr_type, AnimParameters,ParameterTypes),
3317 keys_and_values(ParameterMap, ParameterNames, ParameterTypes),
3318
3319 functor(OType,OTypeF,_),
3320 % TO DO: obtain machine file or machine name
3321 (b_top_level_operation(Name) -> TopLevel = true ; TopLevel=false),
3322 (b_get_operation_normalized_read_write_info(Name,OpRead,Modified)
3323 -> exclude(op_id,OpRead,Read),
3324 get_constants_type(OpRead, ConstReadType),
3325 get_variable_type(OpRead, VarReadType), % TO DO: ids appear multiple times in TypeMap if read and written
3326 get_variable_type(Modified, ModifiedType),
3327 append([ConstReadType, VarReadType, ModifiedType], VarMap)
3328 % exclude query operations called in expressions (allow_operation_calls_in_expr);
3329 %ProB2 Java cannot deal with it and raises exception for non-atomic identifiers
3330 ; Read=unknown,Modified=unknown,
3331 VarMap = []
3332 ),
3333 (b_get_operation_non_det_modifies(Name,NonDetModifies)
3334 -> maplist(b_is_variable, NonDetModifies, NonDetModifiesType),
3335 keys_and_values(NonDetModifiedMap, NonDetModifies, NonDetModifiesType)
3336 ; NonDetModifies=unknown,
3337 NonDetModifiedMap = []
3338 ),
3339 append([ResultMap, ParameterMap, VarMap, NonDetModifiedMap], TypeMap)
3340 ),
3341 MachineOperationInfos).
3342 get_machine_operation_infos_typed(ChannelInfos) :- csp_mode,!,
3343 findall(operation_info(Name,[],[],true,csp,[],[],[],[]), csp_channel_or_start(Name),ChannelInfos).
3344 get_machine_operation_infos_typed([]).
3345
3346 %% note exclude return the elements where the predicate is not succesful
3347 get_constants_type(ConstList, Map) :-
3348 exclude(b_is_variable, ConstList, Filtered),
3349 maplist(b_is_constant, Filtered, Types),
3350 keys_and_values(Map, Filtered, Types).
3351
3352 get_variable_type(VarList, Map) :-
3353 exclude(b_is_constant, VarList, Filtered),
3354 maplist(b_is_variable, Filtered, Types),
3355 keys_and_values(Map, Filtered, Types).
3356
3357 op_id(op(_)).
3358
3359
3360 :- use_module(bmachine,[b_filenumber/4, get_machine_identifiers/2, get_machine_identifiers_with_pp_type/2]).
3361
3362 get_all_spec_identifiers(SortedAllIDs) :-
3363 get_spec_identifiers2(AllIDs),
3364 sort(AllIDs,SortedAllIDs).
3365
3366 :- use_module(probcspsrc(haskell_csp),[get_cspm_identifier/2]).
3367 get_spec_identifiers2(AllIDs) :- b_or_z_mode, !,
3368 findall(ID,get_machine_identifiers_with_pp_type(_,ID),LIds), append(LIds,AllIDs).
3369 get_spec_identifiers2(AllIDs) :- csp_mode,!,
3370 findall([ID,''],get_cspm_identifier(_,ID),AllIDs).
3371 get_spec_identifiers2([]).
3372
3373 % get a list of all machine files: TO DO: extend for CSP, Alloy, TLA...
3374 get_machine_files(Files) :-
3375 findall(b_file(Name,Extension,Filename),b_filenumber(Name,Extension,_,Filename), Files).
3376 % TODO: add .cfg file for TLA+ if it exists
3377
3378 % a predicate to obtain possible identifier completions for current machine:
3379 :- use_module(tools_matching,[fuzzy_match_codes_lower_case/2, codes_to_lower_case/2, get_current_expr_keywords/1,
3380 get_current_keywords/1, get_all_svg_attributes/1,
3381 is_svg_color_name/1, get_all_dot_attributes/1]).
3382 get_possible_completions(ID,_Options,Completions) :-
3383 special_id_match_pattern(ID,Category,IDSuffix),!, % treat things like svg$stro -> complete to stroke without $svg
3384 get_possible_completions(IDSuffix,[keywords(Category),lower_case],Completions).
3385 get_possible_completions(ID,Options,Completions) :-
3386 get_match_ids(Options,SortedAllIDs),
3387 atom_codes(ID,IDCodes0),
3388 (member(lower_case,Options) -> codes_to_lower_case(IDCodes0,IDCodes), Opt=lower_case
3389 ; Opt=case_sensitive, IDCodes = IDCodes0),
3390 findall([Target,Type,Kind],(member([Target,Type,Kind],SortedAllIDs),atom_codes(Target,TargetCodes),
3391 match(Opt,IDCodes,TargetCodes)),Completions0),
3392 (member(latex_to_unicode,Options),
3393 atom_concat('\\',Latex,ID),
3394 latex_to_unicode(Latex,Unicode)
3395 -> ord_union([[Unicode,Latex,unicode]],Completions0,Completions1)
3396 ; Completions1=Completions0
3397 ),
3398 (member(ascii_to_unicode,Options),
3399 ascii_to_unicode(ID,Unicode2)
3400 -> ord_union([[Unicode2,ID,unicode]],Completions1,Completions2)
3401 ; Completions2=Completions1
3402 ),
3403 maplist(completion_add_backquotes_if_required,Completions2,Completions). % only in classical_b_mode?
3404
3405 special_id_match_pattern(ID,Category,IDSuffix) :- atom_codes(ID,Codes),
3406 category_pattern(Pattern,Category),
3407 append(Pattern,SuffixCodes,Codes),
3408 atom_codes(IDSuffix,SuffixCodes).
3409
3410 category_pattern("$",special_categories_only).
3411 category_pattern("col$",svg_colors_only).
3412 category_pattern("dot$",dot_only).
3413 category_pattern("svg$",svg_only).
3414 category_pattern("tex$",latex_only).
3415 category_pattern("str$",strings_only).
3416 % TODO: maybe find better pattern svg:: and support other categories like dot, ext, ...
3417
3418 get_all_special_categories(L) :- findall(ID, (category_pattern(Cs,_),atom_codes(ID,Cs)),L).
3419
3420 % this is not very efficient;
3421 % general check for all completions is not sufficient and leads to incorrect backquotes, e.g., for pragmas: `@desc` or latex: `\alpha`
3422 % backquote check only for svg attributes and identifiers
3423 completion_add_backquotes_if_required([Completion,Type,Kind],BQCompletion) :-
3424 (Kind = svg; Kind = spec_id),
3425 translate:id_requires_escaping(Completion) ->
3426 tools:ajoin(['`',Completion,'`'],BQC), BQCompletion = completion(BQC, Type)
3427 ; BQCompletion = completion(Completion,Type).
3428
3429
3430 :- use_module(tools_lists,[common_prefix_atom/2]).
3431 % Kind is either expr, latex or all
3432 get_possible_completion(ID,Kind,Completion) :-
3433 get_possible_completions(ID,[keywords(Kind)],Completions0),
3434 maplist(ignore_type,Completions0,Completions),
3435 (select(ID,Completions,C2), C2 \= []
3436 -> true % find a longer prefix in case ID is valid, so that we can find longer and longer completions in the UI
3437 ; C2=Completions),
3438 common_prefix_atom(C2,Completion).
3439 % if Completion=ID we could return the first completion or cycle through them
3440
3441 ignore_type(completion(Id,_),Id).
3442
3443 match(case_sensitive,Pattern,TargetCodes) :- !, prefix(TargetCodes,Pattern).
3444 match(lower_case,Pattern,TargetCodes) :- codes_to_lower_case(TargetCodes,TC2), prefix(TC2,Pattern).
3445
3446 get_possible_fuzzy_matches(ID,FuzzyMatches) :-
3447 get_match_ids([keywords(expr)],SortedAllIDs),
3448 atom_codes(ID,IDCodes),
3449 findall(Target,(member([Target,_,_],SortedAllIDs),atom_codes(Target,TargetCodes),
3450 fuzzy_match_codes_lower_case(IDCodes,TargetCodes)),FuzzyMatches).
3451
3452 :- use_module(library(ordsets),[ord_union/3]).
3453 :- use_module(translate,[get_latex_keywords/1, get_latex_keywords_with_backslash/1, ascii_to_unicode/2, latex_to_unicode/2]).
3454 get_match_ids(Options,Ids) :-
3455 get_match_ids2(Options,Keywords,Kind),
3456 maplist(add_id_type_kind(Kind),Keywords,Ids).
3457
3458 :- use_module(btypechecker,[machine_string/1]).
3459 % provides list [Id, Type, Kind]; Kind: latex, svg, dot, expr, all, spec_id, unicode
3460 get_match_ids2(Options,Ids,special) :- member(keywords(special_categories_only),Options),!,
3461 get_all_special_categories(Ids). % svg only
3462 get_match_ids2(Options,Ids,latex) :- member(keywords(latex_only),Options),!,
3463 get_latex_keywords(Ids). % latex only, without leading backslash
3464 get_match_ids2(Options,Ids,svg) :- member(keywords(svg_only),Options),!,
3465 get_all_svg_attributes(Ids). % svg only
3466 get_match_ids2(Options,Ids,dot) :- member(keywords(dot_only),Options),!,
3467 get_all_dot_attributes(Ids).
3468 get_match_ids2(Options,Ids,svg) :- member(keywords(svg_colors_only),Options),!,
3469 findall(Id,is_svg_color_name(Id),Ids).
3470 get_match_ids2(Options,Ids,strings) :- member(keywords(strings_only),Options),!,
3471 get_all_strings(Ids).
3472 get_match_ids2(Options,Ids,Kind) :- select(keywords(Kind),Options,Options2),!,
3473 get_match_ids(Options2,SortedAllIDs), % already adds kinds!
3474 (Kind=latex -> get_latex_keywords_with_backslash(Keywords)
3475 ; Kind=expr -> get_current_expr_keywords(Keywords)
3476 ; Kind=all -> get_current_keywords(Keywords)
3477 ; Kind=svg -> get_all_svg_attributes(Keywords)
3478 ; Kind=string -> get_all_strings(Keywords)
3479 ; add_internal_error('Unknown ids kind:',get_match_ids2(Options,Ids,Kind)), Keywords=[], Kind=unknown
3480 ),
3481 ord_union(SortedAllIDs,Keywords,Ids).
3482 get_match_ids2(_,SortedAllIDs,spec_id) :- get_all_spec_identifiers(SortedAllIDs).
3483 get_all_strings(SIDs) :- findall(Id,machine_string(Id),Ids), sort(Ids,SIDs).
3484
3485 add_id_type_kind(Kind,Id,IdType) :-
3486 (Kind=latex -> KindInfo = 'LaTeX'
3487 ; Kind=svg -> KindInfo = 'SVG attribute'
3488 ; Kind=string -> KindInfo = 'STRING'
3489 ; Kind=dot -> KindInfo = 'dot attribute'
3490 ; KindInfo = ''),
3491 (Id = [Id0,Type] -> IdType = [Id0,Type,Kind]
3492 ; Id \= [_,_,_] -> IdType = [Id,KindInfo,Kind]
3493 ; IdType = Id).
3494
3495 % -----------------------
3496
3497 :- use_module(bmachine_static_checks, [extended_static_check_machine/0]).
3498 :- use_module(visbsrc(visb_visualiser),[extended_static_check_default_visb_file/0]).
3499 /**
3500 prob2_extended_static_check(-Problems)
3501 */
3502 prob2_extended_static_check(Problems) :-
3503 extended_static_check_machine,
3504 extended_static_check_default_visb_file, % maybe we should make this optional
3505 get_all_errors_with_span_info_and_reset(Problems).
3506
3507 :- use_module(wdsrc(well_def_analyser), [analyse_wd_for_machine/3]).
3508 /**
3509 prob2_check_well_definedness(-NrDischarged,-NrTotal)
3510 */
3511 prob2_check_well_definedness(NrDischarged,NrTotal) :-
3512 analyse_wd_for_machine(NrDischarged,NrTotal,_).
3513
3514
3515 :- use_module(extension('banditfuzz/welldef'), [ensure_wd/2]).
3516 :- use_module(probsrc(b_ast_cleanup), [clean_up_pred/3]).
3517 prob2_ensure_wd(Pred, Res) :-
3518 get_eval_scope(Scope),
3519 b_type_open_predicate(no_quantifier,Pred,Scope,TPred,Errors),
3520 (Errors=[] -> true ; add_error_and_fail(prob2_ensure_wd, 'Type-Errors: ', Errors)),
3521 clean_up_pred(TPred, [], PreCleaned),
3522 ensure_wd(PreCleaned, WdPred),
3523 clean_up_pred(WdPred, [], CleanWd),
3524 translate_bexpression(CleanWd,Res).
3525
3526
3527
3528
3529 % -----------
3530 :- use_module(visbsrc(visb_visualiser),[load_visb_file/1,
3531 load_visb_definitions_from_list_of_facts/2,
3532 get_visb_attributes_for_state/2,
3533 get_default_visb_file/2,
3534 get_visb_click_events/1, get_visb_hovers/1, get_visb_items/1,
3535 get_visb_svg_objects/1, get_visb_default_svg_file_contents/1,
3536 perform_visb_click_event/4,
3537 visb_file_is_loaded/1,
3538 visb_file_is_loaded/3,
3539 generate_visb_html_for_history/2,
3540 generate_visb_html_for_history_with_vars/1,
3541 generate_visb_html_for_current_state/2,
3542 generate_visb_html/3,
3543 generate_visb_html_codes_for_states/3]).
3544
3545 % load a VisB JSon file: this needs to be re-loaded everytime a new model is loaded or re-loaded
3546 prob2_load_visb_file(JSonFile) :-
3547 load_visb_file(JSonFile).
3548
3549 prob2_load_visb_definitions_from_list_of_facts(DefFilePath, ListOfFacts) :-
3550 load_visb_definitions_from_list_of_facts(DefFilePath, ListOfFacts).
3551
3552 % Check whether a non-empty VisB visualization is currently loaded, and if so, return its path.
3553 % This predicate doesn't fail, even when no VisB visualization is loaded or it is empty.
3554 prob2_get_loaded_visb_file(Res) :- AllowEmpty=false,
3555 (visb_file_is_loaded(JsonFile,_Svg,AllowEmpty) -> Res = json_file(JsonFile) ; Res = none).
3556
3557 % return current loaded JSON and SVG file; fail if no VisB file loaded
3558 prob2_visb_file_loaded(JsonFile,SvgFile) :- AllowEmpty=true,
3559 visb_file_is_loaded(JsonFile,SvgFile,AllowEmpty).
3560
3561 % for a given state Id (number) this returns a list with the following entries:
3562 % set_attr(SVGId,Attr,Value) -> the attribute Attr of the SVG object with the id SVGId should be set to Value
3563 prob2_visb_attributes_for_state(StateID,List) :- %start_ms_timer(T1),
3564 set_current_state(StateID), % ensure external functions like ENABLED are evaluated in correct state
3565 get_visb_attributes_for_state(StateID,List).
3566 %, stop_ms_walltimer_with_msg(T1,visb_state(StateID)).
3567
3568 % this returns two lists with the following entries:
3569 % execute_event(SVGId,Event,Predicates): when clicking on SVG object with id SVGId one should execute
3570 % the B event Event with the given list of predicates
3571 % hover(OriginID,OtherID,Attr,EnterVal,ExitVal): when hovering over the SVG Object with id OriginID
3572 % the hover should set the attribute Attr of the object OtherID to the value EnterVal,
3573 % and reset it to ExitVal upon leaving
3574 % Currently hovers do not take the current state into account; this may change in future
3575 prob2_visb_click_events_and_hovers(Events,Hovers) :-
3576 get_visb_click_events(Events),
3577 get_visb_hovers(Hovers).
3578
3579 % try and perform a click; if successful returning a list of transition ids to be performed
3580 % if the visb_event is disabled it returns an empty list
3581 % if no visb_event is associated with SvgID it fails
3582 % MetaInfoList can contain infos about shiftKey, pageX, pageY infos of the click
3583 prob2_visb_perform_click(SvgID,MetaInfoList,StateId,Transitions) :-
3584 (perform_visb_click_event(SvgID,MetaInfoList,StateId,TransIDS)
3585 -> trace_to_op_terms(TransIDS,StateId,Transitions)
3586 ; add_message(prob2_interface,'VisB ID has no event: ',SvgID),
3587 Transitions=[]
3588 ).
3589
3590 % this returns a list with the following entries: visb_item(SvgID,Attr,FormulaText,Desc,PositionTerm)
3591 prob2_visb_items(Items) :-
3592 get_visb_items(Items).
3593
3594 prob2_read_visb_path_from_definitions(Path) :-
3595 get_default_visb_file(Path,_) -> true; Path = none.
3596
3597 prob2_visb_svg_objects(Objects) :- get_visb_svg_objects(Objects).
3598
3599 prob2_visb_default_svg_file_contents(Atom) :-
3600 get_visb_default_svg_file_contents(Codes),
3601 atom_codes(Atom,Codes).
3602
3603 prob2_export_visb_html_for_history(TransIDS, File) :-
3604 try_set_trace_by_transition_ids(TransIDS),
3605 generate_visb_html_for_history_with_vars(File).
3606 prob2_export_visb_html_for_history(TransIDS,Options,File) :-
3607 try_set_trace_by_transition_ids(TransIDS),
3608 generate_visb_html_for_history(File,Options).
3609
3610 prob2_export_visb_for_current_state(File) :-
3611 generate_visb_html_for_current_state(File,[]).
3612 prob2_export_visb_html_for_states(StateIds,File,Options) :-
3613 generate_visb_html(StateIds,File,Options).
3614 prob2_get_visb_html_for_states(StateIds,Options,HTMLAtom) :-
3615 generate_visb_html_codes_for_states(StateIds,[id_namespace_prefix(auto)|Options],CodesList),
3616 atom_codes(HTMLAtom,CodesList).
3617
3618 :- use_module(probsrc(b_intelligent_trace_replay),[replay_json_trace_file/5]).
3619 % replay a JSON trace file, Status can be perfect, imperfect(Grade), partial
3620 % TransitionIDList can be used to replay the trace from root
3621 % MatchInfoList is a list of replay_step(MatchInfo,ErrorList) term for all matches
3622 % MatchInfo can be perfect, params_and_results, parameters_only...
3623 prob2_replay_json_trace_file(File,ReplayStatus,Trace,MatchInfoList) :-
3624 replay_json_trace_file(File,_,ReplayStatus,TransIds,MatchInfoList),
3625 trace_to_op_terms(TransIds, root, Trace).
3626
3627 :- use_module(probsrc(b_intelligent_trace_replay),
3628 [load_json_trace_file_for_ireplay/1,
3629 get_stored_json_replay_steps/1,
3630 replay_of_current_step_is_possible_with_trans/5,
3631 ireplay_fast_forward_with_trans/6]).
3632 % interactive trace replay:
3633 prob2_interactive_replay_json_trace_file(File,List) :-
3634 load_json_trace_file_for_ireplay(File),
3635 get_stored_json_replay_steps(List).
3636
3637 prob2_interactive_replay_status(CurStepNr,StateID,OpTerm,MatchInfo,Errors) :-
3638 replay_of_current_step_is_possible_with_trans(CurStepNr,StateID,OpTerm,MatchInfo,list(Errors)), !.
3639 prob2_interactive_replay_status(_,_,none,failed,[]).
3640
3641 prob2_interactive_replay_fast_forward(CurStepNr,StateID,NrSteps,Transitions,MatchInfos,Errors) :-
3642 ireplay_fast_forward_with_trans(CurStepNr,StateID,NrSteps,Transitions,MatchInfos,Errors).
3643
3644
3645 % used in prob_java for TLC4B option -constantssetup
3646 get_constants_predicate(Predicate,PredicateComplete) :-
3647 tcltk_interface:tcltk_get_constants_predicate(root,Predicate,PredicateComplete).
3648 get_constants_predicate(Predicate) :-
3649 get_constants_predicate(Predicate,_).
3650
3651 % get dest state id from a state trace file, e.g. <<name>>.tla.trace generated by TLC4B
3652 replay_state_trace_from_file(File,ID,DestID) :-
3653 (state_space:current_state_id(ID) -> true
3654 ; state_space:state_space_reset,
3655 (ID = root -> true
3656 ; tcltk_interface:find_shortest_trace_to_node(root,ID,_OpIDs,TraceIDs),
3657 try_set_trace_by_transition_ids(TraceIDs))), % allow replay of multiple TLC counter example traces in ProB2-UI; maybe there is a better solution?
3658 b_trace_checking:tcltk_check_state_sequence_from_file_state_id(File,ID,DestID).
3659
3660 prob2_save_html_history(File,TransitionIds) :- % for export of animation function visualisations
3661 try_set_trace_by_transition_ids(TransitionIds), % workaround: history not updated in XTL mode?!
3662 graphical_state_viewer_images:html_print_history(File). % default depth 3, maybe add as an option
3663
3664 :- use_module(rulesdslsrc(rule_validation), [generate_report/3]).
3665 prob2_export_rule_report(StateID,File,Options) :- generate_report(StateID,File,Options). % options: checktime(.)
3666
3667 :- use_module(tcltk_interface, [tcltk_run_ltsmin/5]).
3668 % do_ltsmin_modelchecking(+Backend, +Options, -Result)
3669 % LTSmin modelchecking
3670 %
3671 % Backend = sequential or symbolic
3672 % Options may contain:
3673 % nodead: Disable Deadlock Checking
3674 % noinv: Disable Invariant Checking
3675 % por: Enable Partial Order Reduction
3676 %
3677 % Result may be one of:
3678 % no_counter_example_found
3679 % counter_example_found(ErrorStateId)
3680 do_ltsmin_modelchecking(Backend, Options, Result) :-
3681 (member(nodead, Options) -> NoDead=true ; NoDead=false),
3682 (member(noinv, Options) -> NoInv=true ; NoInv=false),
3683 (member(por, Options) -> UsePOR=true ; UsePOR=false),
3684 tcltk_run_ltsmin(Backend, NoDead, NoInv, UsePOR, Res),
3685 handle_ltsmin_result(Res, Result).
3686
3687 handle_ltsmin_result(counter_example_found, Result) :-
3688 !,
3689 % current state is error state, because the ltsmin runner replayed
3690 current_state_id(ErrorStateId),
3691 Result = counter_example_found(ErrorStateId).
3692 handle_ltsmin_result(Res, Result) :- !, Result = Res.