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