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