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