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