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