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