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