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