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