1		% Heinrich Heine Universitaet Duesseldorf
2		% (c) 2009-2019 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,
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_tex_file/1,
17		load_xtl_spec_from_prolog_file/1,
18		load_alloy_spec_from_file/1,
19		load_alloy_spec_from_term/2,
20
21		reset_animator/0, clear_animator/0, start_animation/0,
22
23		serialize/2,
24		deserialize/2,
25
26		get_state/2,
27		get_b_state/2,
28
29		compute_operations_for_state/2,
30		prob2_execute_custom_operations/6,
31
32		get_op_from_id/4,
33
34		is_initialised_state/1,
35		is_initialised_b_state/1,
36		state_property/3,
37		op_timeout_occurred/2,
38
39		get_state_errors/2,
40
41		evaluate_formula/3, evaluate_formulas/3,
42		evaluate_registered_formulas/3,
43		register_prob2_formula/2, register_prob2_formulas/2,
44		deactivate_prob2_formula/1, deactivate_prob2_formulas/1,
45		activate_prob2_formula/1, activate_prob2_formulas/1,
46		unregister_prob2_formula/1, unregister_prob2_formulas/1,
47		get_machine_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		evaluate_formula_typecheck/5,
53
54		get_states_for_predicate/3,
55
56		filter_states_for_predicate/3,
57
58		insert_formula_for_expansion/2,
59		expand_formula/3,
60
61		do_modelchecking/4,
62		set_goal_for_model_checking/1,
63		compute_efficient_statespace_stats/3,
64		compute_coverage/5,
65		get_modelchecking_coverage/5,
66		prob2_deadlock_freedom_check/2,
67		prob2_invariant_check/2,
68		prob2_redundant_invariants/2,
69
70
71
72		get_enable_matrix/2,
73
74		prob2_do_ltl_modelcheck/4,
75
76		activate_plugin/1, % not working anymore
77		get_plugin_output/2, % not working anymore
78
79		find_trace_to_node/2,
80		find_trace_from_node_to_node/3,
81		find_state_for_predicate/3,
82
83		cbc_disprove/5, cbc_disprove/6,
84		cbc_solve/4, cbc_solve/5, % deprecated
85		cbc_solve_with_opts/5,
86		pretty_print_predicate/3,
87		cbc_generate_test_cases/3,
88		prob2_find_test_path/4,
89
90
91
92		check_csp_assertions/3,
93
94		list_eclipse_preferences/1,
95		list_all_eclipse_preferences/1, % also includes advanced eclipse preferences
96		list_current_eclipse_preferences/1,
97		get_eclipse_preference/2,
98		set_eclipse_preference/2,
99
100		get_signature_merge_state_space/2,
101		get_transition_diagram/2,
102
103		write_dotty_transition_diagram/2,
104		write_dotty_signature_merge/2,
105		write_dot_for_state_viz/2,
106		write_dotty_state_space/1,
107		is_dotty_command/1, write_dotty/2,
108		is_dotty_command_for_expr/1, write_dotty_for_expr/3,
109		get_dot_commands_in_state/2, call_dot_command_and_dot_in_state/5, call_dot_command_in_state/4,
110		%is_dot_command/5, call_dot_command_and_dot/4, % deprecated
111		get_table_commands_in_state/2, call_table_command_in_state/4,
112
113		get_error_messages/2,
114		get_error_messages_with_span_info/2,
115
116		es_copy_from_statespace/2,
117		es_eval/4,
118		evaluate_expression_prolog/3,
119
120		generate_trace_until_condition_fulfilled/4,
121		execute_model/5, execute_model/6,
122		get_unsat_core_with_fixed_conjuncts/3,
123		get_minimum_unsat_core_with_fixed_conjuncts/3,
124
125		prob2_construct_trace/6,
126
127		symbolic_model_check/2,
128
129		% synthesis
130		start_synthesis_from_ui_/13,
131		start_synthesis_single_operation_from_ui_/11,
132		get_valid_and_invalid_equality_predicates_for_operation_/6,
133		get_valid_and_invalid_equality_predicates_for_invariants_/4,
134		get_invariant_violating_vars_from_examples_/3,
135		adapt_machine_code_for_operations_/2,
136		reset_synthesis_context_/0,
137		generate_synthesis_data_from_predicate_/5,
138
139		% These predicates should probably not be exported after the end of the migration
140
141
142		evalb_evaluate_formula/2,
143		evalb_evaluate_tautology/2,
144
145		get_pretty_print/1,
146
147		get_primed_predicate/2,
148		get_weakest_precondition/3,
149		before_after_predicate/2,
150
151		get_machine_operation_names/1, get_machine_operation_infos/1,
152		get_machine_identifiers/2,
153		get_machine_files/1,
154
155		get_possible_completions/3,
156		get_possible_fuzzy_matches/2
157		]).
158
159
160		:- use_module(module_information).
161		:- module_info(group,cli).
162		:- module_info(description,'This module provides the new ProB2 Prolog interface to Java and other languages (usually called via socket server).').
163
164		:- use_module(state_space, [time_out_for_node/1, time_out_for_node/3,
165		time_out_for_invariant/1, max_reached_for_node/1,
166		max_reached_or_timeout_for_node/1,
167		visited_expression/2, transition/4, visited_expression_id/1,
168		set_context_state/1, clear_context_state/0,
169		state_error/3, current_state_id/1,
170		get_state_space_stats/3 %, state_space_initialise/0
171		]).
172		% new profiler
173		%:- use_module('../extensions/profiler/profiler.pl').
174
175
176		:- use_module(symmetry_marker, [precompile_marker_typing_info/0]).
177		:- use_module(value_persistance, [initialise_operation_caching/0]).
178		:- use_module(eventhandling, [announce_event/1]).
179		%:- use_module(self_check, [turn_off_run_time_type_checks/0]).
180		:- use_module(version, [version/4, revision/1, lastchangeddate/1]).
181		:- use_module(pref_definitions, [b_get_preferences_from_machine/0, b_get_preferences_from_machine/1]).
182		:- use_module(bsyntaxtree, [conjunct_predicates/2, get_texpr_ids/2,
183		get_texpr_expr/2,
184		find_identifier_uses/3]).
185		:- use_module(evalstores, [evalstore_bindings/2, evalstore_create_store_by_state/2, evalstore_eval_formula/4]).
186		%:- use_module(model_checker, [is_deadlocked/1]).
187		:- use_module(state_space_exploration_modes,[set_depth_breadth_first_mode/1]).
188		:- use_module(bmachine, [b_type_expression/5, b_get_machine_operation/4, b_get_machine_operation/6,
189		b_type_open_predicate/5, b_top_level_operation/1,
190		b_load_machine_from_list_of_facts/2,
191		b_set_eventb_project_flat/3, load_additional_information/1,
192		b_machine_precompile/0, other_spec_precompile/0,
193		b_set_parsed_typed_machine_goal/1]).
194		:- use_module(probltlsrc(ltl), [ltl_model_check_with_ce/4,preprocess_formula/2]).
195		:- use_module(probltlsrc(ltl_tools), [typecheck_temporal_formula/3]).
196		:- use_module(probltlsrc(ltl_verification), [evaluate_ltl_formula/6]).
197		%:- use_module(b_interpreter, [b_compute_expression_nowf/4]).
198		:- use_module(b_global_sets, [add_prob_deferred_set_elements_to_store/3]).
199		:- use_module(extension('user_signal/user_signal'), [user_interruptable_call_det/2,
200		ignore_user_interrupt_det/1]).
201		:- use_module(library(lists), [maplist/3, maplist/4]).
202		:- use_module(library(codesio), [read_from_codes/2, write_term_to_codes/4]).
203		:- use_module(specfile, [expand_const_and_vars_to_full_store/2, animation_mode/1,
204		b_or_z_mode/0, set_currently_opened_file/1,
205		set_currently_opened_package/1,
206		set_animation_mode/1, set_animation_minor_mode/1]).
207		:- use_module(translate, [translate_bvalue/2, suppress_rodin_positions/0,
208		translate_event/2, translate_bstate/2, translate_state_error/2,
209		translate_bexpression/2, translate_bvalue_with_limit/3,
210		translate_event_error/2, explain_event_trace/2, explain_state_error/3]).
211		:- use_module(error_manager, [add_error_and_fail/3, get_all_errors_and_reset/1,
212		get_all_errors_with_span_info_and_reset/1,
213		add_error/3, add_error/2, add_error_and_fail/2,
214		add_message/2, %reset_errors/0,
215		add_warning/3,
216		add_all_perrors/1,
217		get_error/2,
218		catch_enumeration_warning_exceptions/2,
219		real_error_occurred/0]).
220		:- use_module(tools, [string_concatenate/3, split_atom/3,
221		safe_atom_codes/2,ajoin/2]).
222		%:- use_module(kernel_tools, [map_over_bvalue/3]). % not used ??
223		:- use_module(bvisual2, [bv_insert_formula/3, bv_expand_formula/3,
224		bv_get_values/3]).
225		:- use_module(preferences, [eclipse_preference/2, get_preference/2,
226		preference_description/2, preference_val_type/2,
227		preference_default_value/2, preference_category/2,
228		set_preference/2, advanced_eclipse_preference/2,
229		obsolete_eclipse_preference/1]).
230		:- use_module(disprover, [disprove/5, disprove_with_opts/6]).
231		:- use_module(solver_interface, [solve_predicate/5,
232		call_with_smt_mode_enabled/1]).
233		:- use_module(probcspsrc(haskell_csp), [parse_and_load_cspm_file/1]).
234		:- use_module(state_space_reduction, [reset_ignored_events/0, set_ignored_events/1,
235		compute_signature_merge/0, compute_transition_diagram/1,
236		get_reduced_node/4, reduced_trans/5,
237		generate_node_color/5, generate_node_labels/3,
238		generate_transition_label/3, generate_transition_color_and_style/6,
239		write_signature_merge_to_dotfile/2]).
240		:- use_module(graph_canon, [print_cstate_graph/2]).
241		:- use_module(debug, [debug_println/2]).
242		:- use_module(unsat_cores, [unsat_core_with_fixed_conjuncts/3,
243		minimum_unsat_core_with_fixed_conjuncts/3]).
244		:- use_module(smt_solvers_interface(smt_solvers_interface), [smt_solve_predicate_in_state/5, smt_solve_predicate/4]).
245
246		:- use_module(typechecker).
247		:- use_module(self_check).
248
249		:- use_module(probsrc('synthesis/deep_learning/predicate_data_generator'), [generate_synthesis_data_from_predicate/5]).
250		:- use_module(synthesis(b_synthesis),[start_synthesis_from_ui/13,
251		start_synthesis_single_operation_from_ui/11,
252		reset_synthesis_context/0]).
253		:- use_module(synthesis(synthesis_util),[get_valid_and_invalid_equality_predicates_for_operation/6,
254		get_valid_and_invalid_equality_predicates_for_invariants/4,
255		get_invariant_violating_vars_from_examples/3,
256		adapt_machine_code_for_operations/2]).
257		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
258
259		/**
260		Access information about the current version of the ProB core.
261
262		#### called by:
263		* ProB 2.0: GetVersionCommand
264		*/
265		get_version(Major,Minor,Service,Qualifier,GitRevision,LastChangedDate,PrologInfo) :-
266		version(Major,Minor,Service,Qualifier),
267		revision(GitRevision), lastchangeddate(LastChangedDate), prolog_flag(version,PrologInfo).
268
269
270		% get the total number of errors of ProB's Prolog code; cannot be accidentally reset
271		% useful for validation reports,...
272		:- use_module(error_manager,[get_total_number_of_errors/1]).
273		get_prob_total_number_of_errors(X) :- get_total_number_of_errors(X).
274
275		/* ------------------------- */
276		/* B Loading Interface */
277		/* ------------------------- */
278
279		/**
280		Loads a classical b model.
281
282		#### called by:
283		* ProB 2.0: LoadBProjectCommand
284		*/
285		:- mode load_classical_b_from_list_of_facts(+MainFilename,+ListOfFacts).
286		load_classical_b_from_list_of_facts(MainFilename,ListOfFacts) :-
287		clear_animator,
288		b_load_machine_from_list_of_facts(MainFilename,ListOfFacts),
289		set_currently_opened_file(MainFilename), % or should we use set_currently_opened_package
290		update_preferences_from_spec.
291
292		/**
293		update preferences from SET_PREF Definitions in B machines:
294		should be called after loading a model and before start_animation
295		*/
296		update_preferences_from_spec :- (b_or_z_mode -> b_get_preferences_from_machine ; true).
297		update_preferences_from_spec(List) :- (b_or_z_mode -> b_get_preferences_from_machine(List) ; List=[]).
298
299		/* ------------------------- */
300		/* Event-B Loading Interface */
301		/* ------------------------- */
302
303		/**
304		Loads an Event-B model.
305
306		#### called by:
307		* ProB Plugin: de.prob.eventb.translator.internal.EventBTranslator, DisproverLoadCommand
308		* ProB 2.0: de.prob.model.eventb.translate.EventBModelTranslator (LoadEventBProjectCommand)
309		*/
310		load_event_b_project(Machines,Contexts,Proofs,Errors) :-
311		clear_animator,
312		set_animation_mode(b), set_animation_minor_mode(eventb),
313		b_set_eventb_project_flat(Machines,Contexts,Proofs),
314		load_additional_information(Proofs),
315		Errors = [],
316		set_currently_opened_package(event_b_project).
317
318		/* ------------------------- */
319		/* CSP Loading Interface */
320		/* ------------------------- */
321
322		/**
323		Takes a path to a CSPM specification and loads the file using the CSPM parser.
324
325		#### called by:
326		* ProB 2.0: LoadCSPCommand
327		*/
328		:- mode load_cspm_spec_from_cspm_file(+CSPMFile).
329		load_cspm_spec_from_cspm_file(CSPMFile) :-
330		clear_animator,
331		set_animation_mode(cspm),
332		parse_and_load_cspm_file(CSPMFile),
333		set_currently_opened_file(CSPMFile).
334
335		/* ------------------------- */
336		/* Z Loading Interface */
337		/* ------------------------- */
338
339		load_z_spec_from_tex_file(TexFile) :-
340		clear_animator,
341		user:tcltk_open_z_tex_file(TexFile).
342
343		/* ------------------------- */
344		/* XTL Loading Interface */
345		/* ------------------------- */
346
347		load_xtl_spec_from_prolog_file(PrologFile) :-
348		clear_animator,
349		user:tcltk_open_xtl_file(PrologFile).
350
351		load_alloy_spec_from_file(PrologFile) :-
352		clear_animator,
353		user:tcltk_open_alloy_file(PrologFile).
354
355		:- use_module(probsrc('alloy2b/alloy2b'),[load_alloy_model/2]).
356		load_alloy_spec_from_term(PrologTerm,AlloyFile) :-
357		clear_animator,
358		load_alloy_model(PrologTerm,AlloyFile).
359		/* ------------------------- */
360		/* Animation */
361		/* ------------------------- */
362
363		reset_animator :- announce_event(reset_specification). % just reset; keeping same spec
364		clear_animator :- reset_animator,announce_event(clear_specification).
365
366		start_animation :- %reset_errors, % we no longer reset_errors here !
367		initialise_specification,!.
368		start_animation :- add_error(start_animation,'Start Animation Failed').
369		%NOW done by events: reset_flow, state_space_initialise, reduce_graph_reset, reset_runtime_profiler,
370		% reset_refinement_checker reset_model_checker,
371		% reset_dynamics, % new profiler
372
373		:- use_module(eventhandling,[register_event_listener/3]).
374		:- register_event_listener(clear_specification,reset_prob2_interface,
375		'Reset prob2_interface caches.').
376		reset_prob2_interface :- retractall(cached_registered_formula_result(_,_,_)).
377
378
379		initialise_specification :- /* call once before starting animation or model checking */
380		announce_event(start_initialising_specification),
381		( b_or_z_mode -> b_machine_precompile
382		; otherwise ->
383		preferences:get_preference(symmetry_mode,X),
384		( X=off -> true
385		; otherwise ->
386		add_message(initialise_specification,'Symmetry can only be used for B & Z specifications'),
387		preferences:set_preference(symmetry_mode,off) /* Turn symmetry off */
388		),
389		%tools:print_bt_message(other_spec_precompile),
390		other_spec_precompile
391		),
392		%TODO(DP,11.8.2008)
393		user:initialise_operation_not_yet_covered,
394		% now done via event_handline: reset_external_functions,
395		preferences:get_preference(symmetry_mode,SymMode),
396		precompile_marker_typing_info, % from symmetry_marker.pl
397		( SymMode=nauty ->
398		(graph_canon:initialise_nauty -> true ; preferences:set_preference(symmetry_mode,off))
399		; otherwise -> graph_canon:clear_nauty),
400		announce_event(specification_initialised),
401		( initialise_operation_caching -> true
402		; otherwise -> add_error_and_fail(b_load_machine,'Initialising operation caching failed')).
403
404		/* ------------------------- */
405		/* Handling States */
406		/* ------------------------- */
407
408		/**
409		Produces a prolog serialization of a given state id
410
411		#### called by:
412		* ProB Plugin: SerializeStateCommand
413		* ProB 2.0: SerializeStateCommand
414		*/
415		:- mode serialize(+Id,-SerializedState).
416		serialize(Id,SerializedState) :-
417		visited_expression(Id,State),
418		write_term_to_codes(State,Codes,".",[quoted(true)]),
419		atom_codes(SerializedState,Codes).
420
421		/**
422		Deserialize a state and add it if necessary
423
424		#### called by:
425		* ProB Plugin: DeserializeStateCommand
426		* ProB 2.0: DeserializeStateCommand
427		*/
428		:- mode deserialize(-NewId,+SerializedState).
429		deserialize(NewId,SerializedState) :-
430		atom_codes(SerializedState,Codes),
431		read_from_codes(Codes,State),
432		user:get_id_of_node_and_add_if_required(State,NewId,_Res,root).
433
434		get_state(ID,BState) :- get_state(ID,BState,_,_).
435		get_state(es(ID),Store,full_initialised_state,-1) :- % use a store from the evalstore module instead of
436		!,evalstore_bindings(ID,Store). % a state from the state space
437		get_state(ID,BState,Kind,ConstID) :-
438		if(visited_expression(ID,State),true,(ID=root,State=root)),
439		get_state2(State,BState,Kind),
440		get_constants_id(State,ID,ConstID).
441		get_state2(csp_and_b(CSPState,BState),[bind('CSP_CONTROLLER',CSPState)|ExpandedBState],Kind) :- !,
442		get_state2(BState,ExpandedBState,Kind).
443		get_state2(concrete_constants(BState),BState,constants_only_state) :- !.
444		get_state2(root,BState,empty_state) :- !, BState=[].
445		get_state2(State,Res,full_initialised_state) :- expand_const_and_vars_to_full_store(State,BState),
446		(BState=[_|_] -> Res=BState ; Res=[] /* we have [] or a CSP process or similar */).
447
448		get_constants_id(const_and_vars(ConstID,_),_,Res) :- !,Res=ConstID.
449		get_constants_id(concrete_constants(_),ConstID,Res) :- !,Res=ConstID.
450		get_constants_id(_,_,-1).
451
452		/**
453		Get the predicate representation of a BState
454
455		#### called by:
456		* ProB 2.0: GetBStateCommand
457		*/
458		get_b_state(StateId, BState) :-
459		get_state(StateId, S), translate_bstate(S, BState).
460
461		/**
462		Compute the enabled operations (without the backtrack options) for a given state id.
463		Transitions is a list of operation tuples with the form op(TransitionId,SrcId,DestId)
464
465		#### called by:
466		* ProB 2.0: GetEnabledOperationsCommand
467		*/
468		:- mode compute_operations_for_state(+StateID,-Transitions).
469		compute_operations_for_state(StateID, Transitions) :-
470		visited_expression_id(StateID),
471		user:tcltk_compute_options(StateID,OpsSTAndIDs),
472		(create_simple_op_terms(OpsSTAndIDs,StateID,Transitions) -> true
473		; add_error_and_fail(prob2_interface, 'Creating op terms failed', OpsSTAndIDs)).
474
475		create_simple_op_terms([],_,[]).
476		create_simple_op_terms([(Id,Op,Dst)|T],StateID,[op(Id,Name,StateID,Dst)|FT]) :-
477		extract_op_name(Op,Name),
478		create_simple_op_terms(T,StateID,FT).
479
480		set_current_state(ID) :- current_state_id(ID),!. % no need to jump
481		set_current_state(ID) :- /* jumps to the given node; can be backtracked */
482		visited_expression_id(ID),
483		user:tcltk_goto_state(jump,ID).
484
485		/**
486		Calculates an operation given a predicate from the user.
487
488		#### called by:
489		* ProB 2.0: GetOperationByPredicateCommand
490		*/
491		:- use_module(bmachine,[b_is_operation_name/1]).
492		:- mode prob2_execute_custom_operations(+CurID, +OpName, +ParsedPredicate, +MaxNrOfSolutions, -TOperations, -Errors).
493		prob2_execute_custom_operations(_CurID, _OpName, _Pred, MaxNrOfSolutions, TOps, Errs) :-
494		MaxNrOfSolutions < 1,
495		!,
496		TOps = [],Errs = ['max nr of solutions too small'].
497		prob2_execute_custom_operations(_CurID, OpName, _Pred, _Max, TOps, Errs) :-
498		\+ valid_op_name(OpName),
499		!,
500		TOps = [],
501		(b_is_operation_name(OpName) -> ajoin(['Not a Top-Level Operation ', OpName], Msg)
502		; ajoin(['Unknown Operation ', OpName], Msg)),
503		Errs = [Msg].
504		prob2_execute_custom_operations(CurID, OpName, ParsedPredicate, MaxNrOfSolutions, TOperations, ErrorsOut) :-
505		set_current_state(CurID),
506		prob2_execute_custom_operations_aux(CurID, OpName, ParsedPredicate, MaxNrOfSolutions, TOperations, ErrorsOut).
507
508		% special case for TRUE=TRUE predicate to avoid parser overhead
509		prob2_execute_custom_operations_aux(CurID, OpName, Pred, MaxNrOfSolutions, TOperations, ErrorsOut) :-
510		raw_truth(Pred),!,
511		findall(TO, prob2_execute_custom_operation(CurID,OpName,TO,MaxNrOfSolutions), TOperations),
512		clear_context_state,
513		(TOperations = []
514		-> gen_exec_error_message(CurID,OpName,truth,Msg),
515		ErrorsOut = [Msg]
516		; ErrorsOut = []).
517		prob2_execute_custom_operations_aux(CurID, OpName, ParsedPredicate, MaxNrOfSolutions, TOperations, ErrorsOut) :-
518		( is_special_op(OpName,_)
519		-> Scope = [prob_ids(visible),variables]
520		; otherwise -> b_top_level_operation(OpName),
521		b_get_machine_operation(OpName,_,Parameters,_),
522		Scope = [identifier(Parameters),prob_ids(visible),variables] % prob scope allows one to use identifiers for deferred set elements
523		),
524		b_type_expression(ParsedPredicate, Scope, _, TypedPred, Errors),
525		(Errors = [] ->
526		findall(TO, prob2_execute_custom_operation_with_predicate(CurID,OpName,TypedPred,TO,MaxNrOfSolutions),
527		TOperations),
528		retractall(bmachine:b_machine_temp_predicate(_)),
529		clear_context_state,
530		(TOperations = []
531		-> gen_exec_error_message(CurID,OpName,TypedPred,Msg),
532		ErrorsOut = [Msg]
533		; ErrorsOut = [])
534		; TOperations = [],
535		ErrorsOut = [typechecker_errors(Errors)]
536		).
537
538		gen_exec_error_message(root,OpName,_,Msg) :- \+ is_special_op(OpName,_),!,
539		ajoin(['Machine is not initialised, could not execute operation ', OpName], Msg).
540		gen_exec_error_message(concrete_constants(_),OpName,_,Msg) :- \+ is_special_op(OpName,_),!,
541		ajoin(['Machine is not initialised, could not execute operation ', OpName], Msg).
542		gen_exec_error_message(concrete_constants(_),'$setup_constants',_,Msg) :- !,
543		Msg = 'Constants are already set up, could not execute SETUP_CONSTANTS '.
544		gen_exec_error_message(CurID,OpName,_,Msg) :- CurID \= root, CurID \= concrete_constants(_),
545		is_special_op(OpName,OpS), !,
546		ajoin(['Machine is already initialised, cannot execute ', OpS], Msg).
547		gen_exec_error_message(_,OpName,truth,Msg) :- !,
548		(is_special_op(OpName,OpS) -> true ; OpS=OpName),
549		ajoin(['Could not execute operation ', OpS], Msg).
550		gen_exec_error_message(_,OpName,_,Msg) :- (is_special_op(OpName,OpS) -> true ; OpS=OpName),
551		ajoin(['Could not execute operation ', OpS, ' with additional predicate'], Msg).
552		is_special_op('$setup_constants','SETUP_CONSTANTS').
553		is_special_op('$initialise_machine','INITIALISATION').
554
555		% true if a raw expression definitely represents truth
556		raw_truth(equal(_,E1,E2)) :- raw_equals(E1,E2).
557		raw_equals(boolean_true(_),boolean_true(_)).
558		raw_equals(boolean_false(_),boolean_false(_)).
559		raw_equals(integer(_,I),integer(_,I)).
560
561		valid_op_name('$initialise_machine').
562		valid_op_name('$setup_constants').
563		valid_op_name(OpName) :- b_top_level_operation(OpName).
564		%valid_op_name(OpName) :- b_get_promoted_machine_operations(OpName).
565
566		/**
567
568		Calculates a trace given a list of operation names and a list of guards.
569		In case of errors, a partial trace is generated that jumps over the errornous operation / event.
570		In addition, a list of integers should be given as argument that make possible to execute some
571		operations in the oprations list multiple times or as long as they are disabled (in this case one should give -1).
572		E.g. by calling prob2_construct_trace(0,[e1,e2,e3],[TRUE,TRUE,TRUE],[2,1,-1],OpsOut,ErrOut) the predicate calculates
573		a trace starting at the state with the ID 0 where e1 is executed sequentially 2 times, after that e2 once,
574		and finally e3 until it becomes disabled.
575
576		#### called by:
577		* ProB 2.0: ConstructTraceCommand
578		*/
579
580		prob2_construct_trace(CurId,Names,Preds,Nrs,OpsOut,ErrOut) :-
581		construct_trace(CurId,Names,Preds,Nrs,[],OpsOut,[],ErrOut).
582
583		construct_trace(_CurId,[],[],[],OpsOut,OpsOut,ErrOut,ErrOut).
584		construct_trace(CurId,[Name|Names],[Pred|Preds],[NrName|NrNames],CurOpsOut,OpsOut,CurErrOut,ErrOut) :-
585		execute_nr_of_custom_operations(CurId,Name,Pred,NrName,NewId,ListOfOps,ListOfErrs),
586		append(CurOpsOut,ListOfOps,NewOpsOut),
587		append(CurErrOut,ListOfErrs,NewErrOut),
588		construct_trace(NewId,Names,Preds,NrNames,NewOpsOut,OpsOut,NewErrOut,ErrOut).
589
590		execute_nr_of_custom_operations(CurId,_Name,_Pred,0,CurId,[],[]).
591		execute_nr_of_custom_operations(CurId,Name,Pred,Nr,NewId,ListOfOps,ListOfErrs) :-
592		( Nr = -1 ->
593		execute_until_disabled(CurId,Name,Pred,NewId,ListOfOps,ListOfErrs)
594		; otherwise -> % Nr is greater than 0
595		prob2_execute_custom_operations(CurId,Name,Pred,1,ListContainingSingleOp,SingleErr),
596		( ListContainingSingleOp = [] ->
597		NextId=CurId
598		; ListContainingSingleOp = [op(_Trans,_Name,_From,To)],
599		NextId = To
600		),
601		append(ListContainingSingleOp,Ops,ListOfOps),
602		append(SingleErr,Errs,ListOfErrs),
603		NewNr is Nr - 1,
604		execute_nr_of_custom_operations(NextId,Name,Pred,NewNr,NewId,Ops,Errs)
605		).
606
607
608		execute_until_disabled(CurId,OpName,Pred,NewId,ListOfOps,ListOfErrs) :-
609		execute_until_disabled(CurId,OpName,Pred,NewId,[],ListOfOps,ListOfErrs).
610
611		execute_until_disabled(CurId,OpName,Pred,NewId,CurListOfOps,ListOfOps,ListOfErrs) :-
612		prob2_execute_custom_operations(CurId,OpName,Pred,1,ListContainingSingleOp,SingleErr),
613		( ListContainingSingleOp = [] -> % reached a state where OpName is not executed
614		NewId=CurId,
615		ListOfOps=CurListOfOps,
616		ajoin(['Could not execute Operation ', OpName, ' with additional predicate'], Msg),
617		(member(Msg,SingleErr) -> % Error message generated because OpName is disabled at some state
618		ListOfErrs = []
619		; otherwise -> % unexpected error occurred, need to be reported
620		ListOfErrs = SingleErr
621		)
622		; ListContainingSingleOp = [op(Trans,Name,From,To)],
623		( member(op(_T,_N,To,_To),CurListOfOps) -> % in case of a loop we terminate, otherwise we will go forever
624		ListOfOps = CurListOfOps,
625		NewId=From
626		; otherwise ->
627		NextId = To,
628		append(CurListOfOps,[op(Trans,Name,From,To)],NewCurListOfOps),
629		execute_until_disabled(NextId,OpName,Pred,NewId,NewCurListOfOps,ListOfOps,ListOfErrs)
630		)
631		).
632
633		% TO DO: check if we need to recompute the operation effect: if the ParsedPredicate is TRUE
634		% (TRUE = equal(none,integer(none,1),integer(none,1)) ) & MaxNrOfSolutions <=
635		% what has already been used previously, we can simply reuse transition from the state space
636
637		prob2_execute_custom_operation(CurID,OpName,Transition,Max) :-
638		statistics(walltime, [CurTime1,_]),
639		set_context_state(CurID),
640		visited_expression(CurID,InState),
641		specfile:compute_operation_effect_max(InState,OpName,Operation,NewState,_TransPathInfo,Max),
642		% logger:writeln_log(sol(OpName,NewState)), %%
643		user:add_trans_id(CurID,Operation,NewState,[],NewID,[],TransId),
644		% logger:writeln_log(ids(OpName,Operation,NewID,TransId)), %%
645		statistics(walltime, [CurTime2,_]),
646		log_executed_operation(CurID,Operation,NewID,CurTime1,CurTime2), % TODO? : log errors as comments
647		Transition = op(TransId,OpName,CurID,NewID).
648
649		:- use_module(succeed_max,[succeed_max_call_id/3]).
650		:- use_module(b_state_model_check,[execute_operation_by_predicate_in_state/5]).
651		prob2_execute_custom_operation_with_predicate(CurID,OpName,Predicate,Transition,Max) :-
652		b_top_level_operation(OpName),
653		!,
654		statistics(walltime, [CurTime1,_]),
655		set_context_state(CurID),
656		visited_expression(CurID,InState),
657		succeed_max_call_id(prob2_execute_custom_operation,
658		execute_operation_by_predicate_in_state(InState,OpName,Predicate,Operation,NewState),Max),
659		user:add_trans_id(CurID,Operation,NewState,[],NewID,[],TransId),
660		statistics(walltime, [CurTime2,_]),
661		log_executed_operation(CurID,Operation,NewID,CurTime1,CurTime2),
662		Transition = op(TransId,OpName,CurID,NewID).
663		prob2_execute_custom_operation_with_predicate(CurID,OpName,Predicate,Transition,MaxNrOfSolutions) :-
664		retractall(bmachine:b_machine_temp_predicate(_)), % temporary fix: old style execution for INIT, setup_constants
665		assert(bmachine:b_machine_temp_predicate(Predicate)),
666		prob2_execute_custom_operation(CurID,OpName,Transition,MaxNrOfSolutions).
667
668		:- dynamic last_trace_id/2. % if this fact is set, we assume we will log to a trace file
669
670		:- use_module(preferences,[get_prob_application_type/1]).
671		:- use_module(bmachine,[b_absolute_file_name_relative_to_main_machine/2]).
672		:- register_event_listener(start_initialising_specification,reset_last_trace_id,
673		'Reset for logging.').
674		reset_last_trace_id :- retractall(last_trace_id(_,_)),
675		(get_preference(prob2_trace_file,File),File \= '',
676		get_prob_application_type(Type), Type \= tcltk, % logging not working, would overwrite Trace file
677		b_absolute_file_name_relative_to_main_machine(File,AFile)
678		-> reset_trace_file(AFile,WritableFile),
679		assert(last_trace_id(root,WritableFile)) ; true).
680
681		% log for later replay
682		log_executed_operation(CurID,Operation,NewID,CurTime1,CurTime2) :-
683		retract(last_trace_id(LastID,File)), !,
684		(LastID=CurID -> true ; add_jump(LastID,CurID,File)),
685		Delta is CurTime2 - CurTime1,
686		detailed_print_to_trace_file(File,Operation,CurID,NewID,Delta),
687		% TO DO: print some timing info,... in comments
688		assert(last_trace_id(NewID,File)).
689		log_executed_operation(_,_,_,_,_).
690
691		:- use_module(state_space,[is_concrete_constants_state_id/1]).
692		add_jump(X,X,_) :- !.
693		add_jump(root,X,File) :- is_concrete_constants_state_id(X), % in case we missed a setup_constants
694		!, print_to_trace_file(File,'$setup_constants').
695		add_jump(X,Y,File) :- nl, nl, print(add_jump(X,Y,File)),nl,
696		(X=root ; is_concrete_constants_state_id(X)), % in case we missed an initialisation
697		!,
698		print_to_trace_file(File,'$initialise_machine').
699		add_jump(LastID,CurID,File) :- print_to_trace_file(File,'$jump'(LastID,CurID)).
700
701		:- use_module(tools_printing,[print_time_stamp/1]).
702		reset_trace_file(File,WritableFile) :-
703		(get_preference(prob2_trace_file_gen_unique_name,true)
704		-> open(File,write,Stream,[if_exists(generate_unique_name)]),
705		stream_property(Stream,file_name(WritableFile))
706		; open(File,write,Stream), WritableFile=File
707		),
708		write(Stream,'% Created: '), print_time_stamp(Stream), nl(Stream),
709		revision(GitRevision),
710		format(Stream,'% ProB GIT revision: ~w~n',[GitRevision]),
711		close(Stream).
712		print_to_trace_file(File,Term) :-
713		open(File,append,Stream),
714		portray_clause(Stream,Term),
715		close(Stream).
716		detailed_print_to_trace_file(File,Term,CurID,NewID,Delta) :-
717		open(File,append,Stream),
718		format(Stream,'~n% Executed ~w -> ~w in ~w ms at ',[CurID,NewID,Delta]), print_time_stamp(Stream), nl(Stream),
719		get_state_space_stats(NrNodes, NrTrans, NrProcessed), statistics(memory_used,V), VMb is V / 1048576,
720		format(Stream,'% State space: nodes = ~w, transitions = ~w, processed = ~w, MB used: ~3f~n',[NrNodes,NrTrans,NrProcessed,VMb]),
721		portray_clause(Stream,Term), % TO DO: also export in JSON format; drawback is we need to add closing brackets at the end, whereas in Prolog format we always have a valid trace file
722		close(Stream).
723
724
725		/**
726		Extracts information about the parameters and return values for the
727		specified transition.
728
729		#### called by:
730		* ProB 2.0: GetOpFromId
731		*/
732		:- mode get_op_from_id(+Id,+Truncate,-Params,-RetVals).
733		get_op_from_id(Id,Truncate,Params,RetVals) :-
734		transition(_Src,Op,Id,_Dest),
735		create_op_tuple(Op,Truncate,Params,RetVals).
736
737		/**
738		Creates an operation tuple from transition id, source id, an op term, and a destination id.
739		If creation is unsuccessful, an error is added and the predicate fails.
740		See comment for extract_op_tuple for a description of OpTuple
741		*/
742		:- mode create_op_tuple(+OpTerm, +Truncate, -Params, -RetVals).
743		create_op_tuple(OpTerm, Truncate, Params, RetVals) :-
744		(extract_op_tuple(OpTerm, Truncate, Params, RetVals) -> true;
745		add_error_and_fail(prob2_interface, 'Could not create OpTuple ', extract_op_tuple(OpTerm, Params, RetVals))).
746
747		/**
748		Extracts the parameters and return values of the operations
749		*/
750		:- mode extract_op_tuple(+OpTerm, +Truncate, -Params, -RetVals).
751		extract_op_tuple(OpTerm, Truncate, Params, RetVals) :-
752		(animation_mode(cspm) ->
753		extract_csp_op(OpTerm, Params, RetVals)
754		; extract_b_op(OpTerm, Truncate, Params, RetVals)
755		).
756
757		/**
758		Extracts information for a CSP operation.
759		*/
760		:- mode extract_csp_op(+OpTerm, -Params, -RetVals).
761		extract_csp_op(OpTerm, Params, []) :-
762		%OpTuple = op(TransId, Src, Dest, Name, params(Source, Pretty), return([],[]), TargetState), /* TODO: CSP operations do not have return types, is this correct??? */
763		%extract_csp_name_and_args(OpTerm, _Name, _Source),
764		translate_event(OpTerm, PPEvent),
765		split_atom(PPEvent,['.','!'],[_Op|Params]).
766
767		:- mode extract_csp_name_and_args(+OpTerm, -Name, -Args).
768		extract_csp_name_and_args(io(Args,ChName,_SPAN),ChName,Args).
769		extract_csp_name_and_args(start_cspm(Name), Name, []).
770		extract_csp_name_and_args(start_cspm_MAIN,'start_cspm_MAIN',[]).
771		extract_csp_name_and_args(tick(_),tick,[]).
772		extract_csp_name_and_args(tau(_),tau,[]).
773		extract_csp_name_and_args(_OP,'?',[]).
774
775		/**
776		Extracts information for a B operation.
777		*/
778		:- mode extract_b_op(+OpTerm, +Truncate, -Params, -RetVals).
779		extract_b_op(OpTerm, Truncate, Params, RetVals) :-
780		extract_b_op_infos(OpTerm, _Name, PSource, RSource),
781		maplist(pretty_print_bvalue(Truncate), PSource, Params),
782		maplist(pretty_print_bvalue(Truncate), RSource, RetVals).
783
784		:- mode extract_b_op_infos(+Term, -Name, -Arguments, -RetVals).
785		extract_b_op_infos(Term, Name, Arguments, RetVals) :-
786		(Term = '-->'(OpTerm,RetVals) -> true;
787		OpTerm = Term, RetVals = []),
788		OpTerm =.. [Name|Arguments].
789
790		extract_op_name(OpTerm,Name) :-
791		(animation_mode(cspm) ->
792		extract_csp_name_and_args(OpTerm, Name, _Args)
793		; extract_b_op_infos(OpTerm, Name, _Params, _RetVals)
794		).
795
796		pretty_print_bvalue_unicode(Truncate,Formula,Result) :-
797		set_unicode_mode,
798		call_cleanup(pretty_print_bvalue(Truncate,Formula,Result),unset_unicode_mode).
799		pretty_print_bvalue(truncate,Formula,Result) :-
800		translate_bvalue_with_limit(Formula,600,Result).
801		%translate_bvalue(Formula, Result).
802		pretty_print_bvalue(expand,Formula,Result) :-
803		translate_bvalue_with_limit(Formula,-1,Result).
804
805		/* ------------------------- */
806		/* Boolean Properties */
807		/* ------------------------- */
808
809		is_initialised_state(ID) :- b_mode,!,
810		is_initialised_b_state(ID).
811		is_initialised_state(ID) :-
812		visited_expression_id(ID), ID \= root.
813
814		is_initialised_b_state(ID) :-
815		visited_expression(ID,State), ID \= root,
816		(b_mode -> specfile:state_corresponds_to_initialised_b_machine(State) ; true).
817
818
819		invariantKO(StateID) :- is_initialised_state(StateID),
820		get_state(StateID,State),
821		user:check_invariantKO(StateID,State),
822		state_space:invariant_violated(StateID).
823
824		/**
825		Takes a state id and finds all of the operations for which a timeout occurred
826
827		#### called by:
828		* ProB Plugin: GetTimeoutedOperationsCommand
829		* ProB 2.0: GetOperationsWithTimeout
830		*/
831		op_timeout_occurred(StateID,OpNameList) :-
832		findall(OpName,time_out_for_node(StateID,OpName,_Type),OpNameList).
833
834		inv_timeout_occurred(StateID) :- time_out_for_invariant(StateID).
835		timeout_occurred(StateID) :- time_out_for_node(StateID).
836		max_operations_reached(StateID) :- max_reached_for_node(StateID).
837
838		/**
839		Finds the status for a given property
840		Properties can be: invariantKO, timeout_occurred, max_operations_reached, initialised
841		Statuses are expected to be boolean values: either true or false
842
843		#### called by:
844		* ProB Plugin: CheckBooleanPropertyCommand
845		* ProB 2.0: CheckBooleanPropertyCommand
846		*/
847		:- mode state_property(+Property,+StateId,-Status).
848		state_property(Property,StateId,Status) :-
849		( state_property2(Property,StateId) -> Status = true
850		; otherwise -> Status = false).
851		state_property2(invariantKO,StateId) :- invariantKO(StateId).
852		state_property2(timeout_occurred,StateId) :- inv_timeout_occurred(StateId) ; timeout_occurred(StateId).
853		state_property2(max_operations_reached,StateId) :- max_operations_reached(StateId).
854		state_property2(valid_state,StateId) :- visited_expression(StateId, _State).
855		state_property2(initialised,StateId) :-
856		(specfile:csp_mode ->
857		true % in CSP the content of the state is irrelevant for the semantic of the state space
858		; is_initialised_state(StateId)
859		).
860
861
862		/**
863		Takes a id for a given state in the state space and produces a list of all
864		state based errors.
865
866		#### called by:
867		* ProB Plugin: GetStateBasedErrorsCommand
868		* ProB 2.0: GetStateBasedErrorsCommand
869		*/
870		:- mode get_state_errors(+StateId,-Errors).
871		get_state_errors(StateId,Errors) :-
872		findall(E, (state_error(StateId,_,E),E \== invariant_violated), Errs),
873		convert_errors(Errs,Errors).
874		convert_errors([],[]).
875		convert_errors([Error|InRest],[error(Event,Short,Long)|OutRest]) :-
876		( Error = eventerror(Event,EError,Trace) ->
877		translate_event_error(EError,Short),
878		explain_event_trace(Trace,LongStr),
879		safe_atom_codes(Long,LongStr)
880		; otherwise ->
881		Event = '*unknown*',
882		translate_state_error(Error,Short),
883		explain_state_error(Error,_Span,LongStr),
884		safe_atom_codes(Long,LongStr)),
885		convert_errors(InRest,OutRest).
886
887		/* ------------------------- */
888		/* Evaluate Formulas */
889		/* ------------------------- */
890
891		% term in string (see String argument) should be terminated by full-stop!!!
892		evaluate_csp_expression_string(PlClause,R) :-
893		read_from_codes(PlClause,PlTerm),
894		evaluate_csp_expression_aux(PlTerm,R).
895
896		evaluate_csp_expression_aux(PlTerm,R) :-
897		haskell_csp:evaluate_expression(PlTerm,Res),
898		translate:translate_cspm_expression(Res, R).
899		evaluate_csp_expression_aux(Other,_R) :-
900		add_error_and_fail(prob2_interface, 'Unexpected CSP Expression: ', Other).
901
902		/**
903		Evaluate a formula given a state id and the raw prolog representation of the formula
904
905		#### Params:
906		* StateId - state for which the formula should be evaluated
907		* Element - Triple in the form eval(Formula,Type,Code)
908		* Formula - Prolog representation of non-typechecked formula
909		* Type - csp,'#PREDICATE',or '#EXPRESSION'
910		* Code - String representation of Formula
911		* Truncate - if the result should be truncated or expanded
912		* Result - Triple result(Value,Solutions,Code)
913		* Value - String rep of the value calculated by ProB or tuple: v(SRes,Term)
914		* SRes - String rep of the value calculated by ProB
915		* Term - Prolog representation of the value
916		* Solutions - List of solutions as a triple: bind(Name,Solution,PPSol)
917		* Name - String free variable from formula
918		* Solution - Prolog representation of the solution bound to the name
919		* PPSol - String representation of the solution bound to the name
920		* Code - String representation of evaluated formula
921
922		#### called by:
923		ProB 2.0: EvaluateFormulaCommand
924		*/
925
926		:- mode evaluate_formula(+StateId,+Element,-R).
927		evaluate_formula(StateId,Element,R) :-
928		get_state_with_deferred_sets(StateId,State,Kind,_),
929		evaluate_formula_in_state(Kind,State,StateId,Element,R).
930
931		% a list version of the above: advantage: state expanded only once
932		:- mode evaluate_formulas(+StateId,+Elements,-Results).
933		evaluate_formulas(StateId,Elements,Rs) :-
934		get_state_with_deferred_sets(StateId,State,Kind,_ConstID),
935		maplist(inline_machine(_Machine),Elements,Elements2),
936		maplist(evaluate_formula_in_state(Kind,State,StateId),Elements2,Rs).
937
938		% detect all expressions and insert machine term variable to avoid generating term multiple times
939		% TO DO: maybe also inline Typechecker's type environment
940		inline_machine(Machine,eval(Raw,Type,Code,Truncate),eval(Raw,for_machine(Machine,Type),Code,Truncate)) :-
941		Type \= csp, !.
942		inline_machine(_,E,E).
943
944		:- use_module(runtime_profiler,[profile_single_call/3]).
945		:- meta_predicate myprofile(-,-,0).
946		myprofile(_,_,Call) :- call(Call).
947		%myprofile(Source,StateId,Call) :- profile_single_call(Source,StateId,Call).
948		evaluate_formula_in_state(_Kind, _State,_StateId, eval(Raw,csp,Code,_Truncate), R) :- !,
949		( evaluate_csp_expression_string(Raw,Res) ->
950		R = result(Res,[]);
951		R = [Code,"Unexpected CSP Expression"]).
952		evaluate_formula_in_state(StateKind,State,StateId, eval_typed(Typed,Truncate), R) :- !,
953		get_texpr_type(Typed, Type),
954		myprofile(prob2_evaluate_typed_formula,StateId,
955		prob2_interface:evaluate_typechecked_b_formula_in_state(StateKind,formula(Typed),State,Typed,Type,Truncate,R)).
956		evaluate_formula_in_state(StateKind, State,StateId, eval(Raw,PredOrExpr,Code,Truncate), R) :-
957		%logger:writeln_log_time(typechecking_raw(PredOrExpr)),
958		myprofile(Raw,StateId,
959		prob2_interface:evaluate_formula_typecheck2(PredOrExpr,Raw,Typed,Type,Errors)),
960		%logger:writeln_log_time(evaluate_typechecked_b_formula_in_state(StateKind)),
961		( Errors=[] ->
962		%print('EVAL:'),nl,translate:print_bexpr(Typed),nl,
963		myprofile(prob2_evaluate_formula,StateId,
964		prob2_interface:evaluate_typechecked_b_formula_in_state(StateKind,formula(Typed),State,Typed,Type,Truncate,R))
965		; R = [Code|Errors]).
966
967		get_state_with_deferred_sets(StateId,State,Kind,ConstID) :-
968		get_state(StateId, State1,Kind,ConstID), % TO DO: we could try and get only those identifiers that are really used
969		add_prob_deferred_set_elements_to_store(State1, State, visible).
970
971		/**
972		Type checks a given formula.
973
974		#### Params:
975		* PredOrExpr - '#PREDICATE' or '#EXPRESSION'
976		* RawFormula - Prolog representation of non-typechecked formula
977		* TypedFormula - Prolog representation of typechecked formula
978		* Type - type of formula
979		* Errors - any errors that have occured during typechecking
980
981		#### called by:
982		ProB 2.0: EvaluateFormulaCommand
983		*/
984		% can be expensive for big machines, as typechecking calls full_b_machine (20-30 ms for ZC scheduler)
985
986		:- mode evaluate_formula_typecheck(+PredOrExpr,+RawFormula,-TypedFormula,-Type,-Errors).
987		evaluate_formula_typecheck(PredOrExpr,RawFormula,TypedFormula,PPType,Errors) :-
988		evaluate_formula_typecheck2(PredOrExpr,RawFormula,TypedFormula,Type,Errors),
989		translate:pretty_type(Type,PPType).
990		evaluate_formula_typecheck(PredOrExpr,RawFormula,TypedFormula,Errors) :-
991		evaluate_formula_typecheck2(PredOrExpr,RawFormula,TypedFormula,_Type,Errors).
992
993		:- use_module(bmachine,[b_is_variable/2, b_is_constant/2, b_type_expression_for_full_b_machine/6]).
994		% this predicate returns the internal Prolog type:
995		:- mode evaluate_formula_typecheck2(+PredOrExpr,+RawFormula,-TypedFormula,-Type,-Errors).
996		evaluate_formula_typecheck2('#PREDICATE',Raw,Typed,Type,Errors) :-
997		!, get_eval_scope(Scope),
998		b_type_open_predicate(open(exists),Raw,Scope,Typed,PErrors),
999		convert_perrors(PErrors, Errors),
1000		Type=pred.
1001		evaluate_formula_typecheck2(for_machine(M,'#PREDICATE'),Raw,Typed,Type,Errors) :-
1002		!,get_eval_scope(Scope),
1003		bmachine:b_type_open_predicate_for_full_b_machine(M,open(exists),Raw,Scope,Typed,PErrors),
1004		convert_perrors(PErrors, Errors),
1005		Type=pred.
1006		evaluate_formula_typecheck2('#EXPRESSION',identifier(Pos,ID),Typed,Type,Errors) :-
1007		(b_is_variable(ID,Type) ; b_is_constant(ID,Type)),
1008		!, % hack to avoid type-checking simple identifiers which just need to be looked up in state
1009		Errors=[], Typed = b(identifier(ID),Type,[nodeid(Pos)]).
1010		evaluate_formula_typecheck2('#EXPRESSION',Raw,Typed,Type,Errors) :-
1011		!,get_eval_scope(Scope),
1012		b_type_expression(Raw,Scope,Type,Typed,PErrors),
1013		convert_perrors(PErrors, Errors).
1014		evaluate_formula_typecheck2(for_machine(_M,'#EXPRESSION'),identifier(Pos,ID),Typed,Type,Errors) :-
1015		(b_is_variable(ID,Type) ; b_is_constant(ID,Type)),
1016		!, % hack to avoid type-checking simple identifiers which just need to be looked up in state
1017		Errors=[], Typed = b(identifier(ID),Type,[nodeid(Pos)]).
1018		evaluate_formula_typecheck2(for_machine(M,'#EXPRESSION'),Raw,Typed,Type,Errors) :-
1019		!,get_eval_scope(Scope),
1020		b_type_expression_for_full_b_machine(M,Raw,Scope,Type,Typed,PErrors),
1021		convert_perrors(PErrors, Errors).
1022		evaluate_formula_typecheck2(Else,_Raw,_Typed,_Type,_Errors) :-
1023		add_error_and_fail(prob2_interface,'expected #PREDICATE or #EXPRESSION instead of:', Else),fail.
1024
1025		% get scope for typechecker:
1026		get_eval_scope([prob_ids(visible),Scope]) :- get_main_eval_scope(Scope).
1027		get_main_eval_scope(assertions_scope) :- get_preference(allow_operation_calls_in_expr,true),!.
1028		get_main_eval_scope(variables).
1029
1030		% FIXME This is a bit hacky, it would be better to implement this properly in error_manager.
1031		convert_perrors(PErrors, Errors) :-
1032		add_all_perrors(PErrors),
1033		get_all_errors_with_span_info_and_reset(Errors).
1034
1035		:- use_module(tools_meta,[safe_time_out/3]).
1036		%evaluate_typechecked_b_formula(StateId,Typed,Type,Truncate,Result) :-
1037		% get_state_with_deferred_sets(StateId,State),
1038		% evaluate_typechecked_b_formula_in_state(State,Typed,Type,Truncate,Result).
1039
1040		evaluate_typechecked_b_formula_in_state(StateKind,Requirements,State,Typed,Type,Truncate,Result) :-
1041		(requirements_met(Requirements,StateKind) ->
1042		evaluate_typechecked_b_formula_in_state(State,Typed,Type,Truncate,Result)
1043		; Result = errors('IDENTIFIER(S) NOT YET INITIALISED; INITIALISE MACHINE FIRST',[])
1044		).
1045		evaluate_typechecked_b_formula_in_state(State,Typed,Type,Truncate,Result) :-
1046		% should we use get_computed_preference(debug_time_out,DTO) instead of 1000 ?
1047		% there seem to be two uses in ProB2: for state view, where we want a short time out, and LISB or maybe REPL where we want a longer time out or no time out
1048		(Truncate=truncate -> TO = 1000, FORCE=limit(10000) ; TO = 30000, FORCE=force),
1049		safe_time_out(evaluate_formula_eval(Type,State,Typed,FORCE,Res,Solution,EnumWarning),TO,TimeOutRes),
1050		(TimeOutRes=time_out -> Res=time_out, EnumWarning=false ; true),
1051		get_error_messages(_WarningsOnly,Errors),
1052		extract_result(EnumWarning,Errors,Res,Solution,Truncate,Result).
1053
1054		extract_result(true,_,_,_,_,enum_warning).
1055		extract_result(_EnumW,[],v(_SRes,Term),[],Truncate,Result) :- % v/2 for value
1056		pretty_print_bvalue_unicode(Truncate,Term,R),
1057		Result = result(R,[]).
1058		extract_result(_EnumW,[],SRes,Solutions,Truncate,Result) :-
1059		prettyprint_solutions(Truncate,Solutions,PPSol),
1060		Result = result(SRes,PPSol).
1061		extract_result(_EnumW,Errors,v(SRes,_),_Sol,_Truncate,Result) :-
1062		Result = errors(SRes, Errors).
1063		extract_result(_EnumW,Errors,SRes,_Sol,_Truncate,Result) :-
1064		Result = errors(SRes, Errors).
1065
1066		%:- use_module(eval_strings,[eval_predicate/5]). % TODO: export and refactor
1067		% TO DO: move this into another more general module:
1068		evaluate_formula_eval(pred,State,Typed,_,Res,LocalState,EnumWarning) :-
1069		!,catch_enumeration_warning_exceptions(
1070		(eval_predicate(State,Typed,Res,EnumWarning,LocalState)->true),
1071		(Res = time_out,EnumWarning = true)).
1072		evaluate_formula_eval(_Type,State,Typed,FORCE,Res,[],EnumWarning) :-
1073		catch_enumeration_warning_exceptions(
1074		(evaluate_expression(State,Typed,FORCE,SRes,Term)->EnumWarning=false),
1075		(SRes = time_out, EnumWarning = true)),
1076		Res = v(SRes,Term).
1077
1078		:- use_module(clpfd_interface,[catch_clpfd_overflow_call2/2]).
1079		:- use_module(error_manager,[enter_new_error_scope/2, exit_error_scope/3,clear_all_errors_in_error_scope/1,
1080		event_occurred_in_error_scope/1]).
1081		:- use_module(store,[normalise_value_for_var/4]).
1082		% a simplified version of eval_strings:eval_expression
1083		% evaluate an expression Typed in an expanded state EState giving string result Result and Prolog value NValue
1084		% FORCE = force or e.g. limit(10000)
1085		evaluate_expression(EState,Typed,FORCE,Result,NValue) :-
1086		enter_new_error_scope(ScopeID,evaluate_expression),
1087		clear_all_errors_in_error_scope(ScopeID),
1088		%replace_expression_by_kodkod_if_enabled(Typed,Typed2),
1089		catch_clpfd_overflow_call2(b_interpreter:b_compute_expression_nowf(Typed,[],EState,Value),fail), % We could return CLPFD overflow error result
1090		!,
1091		%logger:writeln_log_time(normalise_value_for_var(evaluate_expression)),
1092		normalise_value_for_var(evaluate_expression,FORCE,Value,NValue),
1093		exit_error_scope(ScopeID,ErrOcc,evaluate_expression),
1094		(ErrOcc=true % TO DO: check which kind of error occured
1095		-> Result = 'NOT-WELL-DEFINED'
1096		; translate:translate_bvalue_for_expression(NValue,Typed,Result)
1097		).
1098		evaluate_expression(_,_,_,'NOT-WELL-DEFINED',error) :-
1099		exit_error_scope(_ScopeID,_,evaluate_expression).
1100
1101		% a simplified version of eval_strings:eval_predicate_aux
1102
1103		eval_predicate(State, ExTyped,Result,EnumWarning,LocalState) :-
1104		enter_new_error_scope(ScopeID,eval_predicate), clear_all_errors_in_error_scope(ScopeID),
1105		(catch_clpfd_overflow_call2(prob2_interface:eval_predicate2(State, ExTyped,LocalState),
1106		fail)
1107		-> Res='TRUE', EnumWarning=false
1108		; event_occurred_in_error_scope(enumeration_warning(_,_,_,_,_Critical))
1109		-> Res= 'NOT-WELL-DEFINED', EnumWarning=true
1110		; Res='FALSE', EnumWarning=false
1111		),
1112		exit_error_scope(ScopeID,ErrOcc,eval_predicate),
1113		(ErrOcc=true % TO DO: check which kind of error occured
1114		-> Result = 'NOT-WELL-DEFINED'
1115		; Result = Res
1116		).
1117
1118		eval_predicate2(State, ExTyped,LocalState) :-
1119		eval_strings:is_existential_quantifier(ExTyped,Parameters,Typed), % TO DO: move to module
1120		!,
1121		test_bool_exists(State, Parameters,Typed,LocalState).
1122		eval_predicate2(State, Typed,LocalState) :- LocalState=[],
1123		b_interpreter:b_test_boolean_expression_wf(Typed,LocalState,State).
1124
1125		test_bool_exists(EState, Parameters,Typed,LocalState) :-
1126		kernel_waitflags:init_wait_flags(WF),
1127		b_interpreter:set_up_typed_localstate(Parameters,_FreshOutputVars,TypedVals,[],LocalState,positive),
1128		b_enumerate:b_tighter_enumerate_values(TypedVals,WF),
1129		b_interpreter:b_test_boolean_expression(Typed,LocalState,EState,WF),
1130		kernel_waitflags:ground_wait_flags(WF).
1131
1132		:- dynamic prob2_formula/4.
1133		:- dynamic inactive_prob2_formula/1.
1134
1135		/**
1136		Type checks a specified formula and asserts so that it can be found later
1137		and evaluated later.
1138
1139		#### called by:
1140		* ProB 2.0: RegisterFormulaCommand
1141		*/
1142
1143		:- mode register_prob2_formula(+FormulaUUID, +Formula).
1144		register_prob2_formula(FormulaUUID, _) :- prob2_formula(FormulaUUID,_,_,_),!.
1145		register_prob2_formula(FormulaUUID, eval(Raw,PredOrExpr,Truncate)) :-
1146		evaluate_formula_typecheck(PredOrExpr,Raw,Typed,Errors),
1147		( Errors=[] ->
1148		register_prob2_formula2(FormulaUUID, Typed, Truncate)
1149		; otherwise ->
1150		add_error_and_fail(register_prob2_formula, 'Type-Errors: ', Errors)
1151		).
1152		register_prob2_formula(FormulaUUID, eval_typed(Typed,Truncate)) :-
1153		register_prob2_formula2(FormulaUUID,Typed,Truncate).
1154
1155		:- use_module(bmachine, [determine_type_of_formula/2]).
1156		register_prob2_formula2(FUUID, Typed, Truncate) :-
1157		determine_type_of_formula(Typed,Requirements),
1158		assert(prob2_formula(FUUID, Typed, Truncate,Requirements)).
1159
1160		:- mode register_prob2_formulas(+FormulaUUIDs, +Formulas).
1161		register_prob2_formulas(FormulaUUIDs,Formulas) :-
1162		maplist(inline_machine(_Machine),FormulaUUIDs,FormulaUUIDs2),
1163		maplist(register_prob2_formula,FormulaUUIDs2,Formulas).
1164
1165
1166		% TO DO: determine upon registering whether a formula reads nothing, just constants, or also variables
1167
1168		% unregister a single or a list of formula ids:
1169		unregister_prob2_formula(FormulaUUID) :- retractall(prob2_formula(FormulaUUID,_,_,_)).
1170		unregister_prob2_formulas(Fs) :- maplist(unregister_prob2_formula,Fs).
1171
1172		% mark certain formulas as inactive; will not be computed by evaluate_registered_formula
1173		% useful when certain information currently not needed (e.g., in state view the formula is not visible/shown)
1174		deactivate_prob2_formulas(Fs) :- maplist(deactivate_prob2_formula,Fs).
1175		deactivate_prob2_formula(FormulaUUID) :- prob2_formula(FormulaUUID,_,_,_),!,
1176		(inactive_prob2_formula(FormulaUUID) -> print(formula_already_inactive(FormulaUUID)),nl
1177		; assert(inactive_prob2_formula(FormulaUUID))).
1178		deactivate_prob2_formula(FormulaUUID) :-
1179		add_internal_error('Cannot deactivate unknown formula: ',deactivate_prob2_formula(FormulaUUID)).
1180
1181		% mark certain formulas as active again; will not be computed by evaluate_registered_formula
1182		activate_prob2_formulas(Fs) :- maplist(activate_prob2_formula,Fs).
1183		activate_prob2_formula(FormulaUUID) :- prob2_formula(FormulaUUID,_,_,_),!,
1184		(retract(inactive_prob2_formula(FormulaUUID)) -> true ; print(formula_already_active(FormulaUUID)),nl).
1185		activate_prob2_formula(FormulaUUID) :- add_internal_error('Cannot activate unknown formula: ',activate_prob2_formula(FormulaUUID)).
1186
1187		/**
1188		Takes a state id and a list of formula ids (that were registered already)
1189		via register_prob2_formula predicate. Then it evaluates all of the formulas
1190		for the given state id.
1191
1192		#### called by:
1193		* ProB 2.0: EvaluateRegisteredFormulasCommand
1194		*/
1195		:- mode evaluate_registered_formulas(+StateId, +FormIds, -Results).
1196		evaluate_registered_formulas(StateId,FormIds,Results) :-
1197		get_state_with_deferred_sets(StateId,State,Kind,ConstID),
1198		maplist(evaluate_registered_formula(State,Kind,ConstID), FormIds, Results).
1199
1200		:- use_module(probsrc(bsyntaxtree),[get_texpr_type/2]).
1201		evaluate_registered_formula(_,_,_,FormulaUUID,Result) :- inactive_prob2_formula(FormulaUUID),!,
1202		Result = errors('IDENTIFIER(S) NOT YET INITIALISED; INITIALISE MACHINE FIRST',[]). % TO DO: maybe other return value
1203		%evaluate_registered_formula(State,StateKind,FormulaUUID,Result) :-
1204		% prob2_formula(FormulaUUID,Typed,Truncate,Requirements),!,
1205		% tools:ajoin([Requirements,':',StateKind],R), Result = result(R,[]).
1206		evaluate_registered_formula(State,StateKind,ConstID,FormulaUUID,Result) :-
1207		prob2_formula(FormulaUUID,Typed,Truncate,Requirements),!,
1208		get_texpr_type(Typed,Type),
1209		(cached_registered_formula_result(FormulaUUID,ConstID,R) -> Result = R
1210		; requirements_met(Requirements,StateKind) ->
1211		evaluate_typechecked_b_formula_in_state(State,Typed,Type,Truncate,Result),
1212		store_result_in_cache(Requirements,ConstID,FormulaUUID,Type,Result)
1213		; StateKind=requires_constants ->
1214		Result = errors('IDENTIFIER(S) NOT YET INITIALISED; INITIALISE MACHINE FIRST',[]) %Result = errors('CONSTANTS NOT INITIALISED',[])
1215		; Result = errors('IDENTIFIER(S) NOT YET INITIALISED; INITIALISE MACHINE FIRST',[])).
1216		evaluate_registered_formula(_State,_StateKind,_ConstID,FormulaUUID,Result) :-
1217		add_error(prob2_interface,'Unknown formula id:',FormulaUUID),
1218		Result = errors('IDENTIFIER(S) NOT YET INITIALISED; INITIALISE MACHINE FIRST',[]).
1219
1220		% check whether we can evaluate the formula in the state:
1221		requirements_met(requires_nothing,_).
1222		requirements_met(requires_constants,constants_only_state).
1223		requirements_met(requires_constants,full_initialised_state).
1224		requirements_met(requires_variables,full_initialised_state).
1225		requirements_met(formula(Typed),State) :-
1226		(State=full_initialised_state -> true
1227		; determine_type_of_formula(Typed,Requirements), requirements_met(Requirements,State)).
1228
1229		:- dynamic cached_registered_formula_result/3.
1230		store_result_in_cache(requires_nothing,ConstID,FormulaUUID,Type,Result) :- cache_this_type(Type), !,
1231		assert(cached_registered_formula_result(FormulaUUID,ConstID,Result)).
1232		store_result_in_cache(requires_constants,ConstID,FormulaUUID,Type,Result) :- cache_this_type(Type), ConstID>=0,!,
1233		assert(cached_registered_formula_result(FormulaUUID,ConstID,Result)).
1234		store_result_in_cache(_,_,_,_,_).
1235
1236		cache_this_type(pred). % currently we only cache predicates, anyway: it makes no sense to cache identifiers (their values are stored in the state anyway)
1237
1238		% return a list of nodes for the hierarchical state viewer:
1239		% NODES ::= category(NAME, list(INFO), list(NODES)) | formula(AST,PP)
1240		% INFO ::= expanded | propagated
1241		% (expanded means: by default this category is expanded, propagated means: if it is not expanded, still show summary info)
1242
1243		get_machine_formulas(Structure) :-
1244		findall(category(Desc,Infos,Subs),category(_,Desc,Infos,Subs),Structure).
1245
1246		:- type prob2_nodes +--> (category(atomic,list(atomic),list(prob2_nodes)) ; formula(b(ground,ground,list(ground)),atomic)).
1247		:- assert_must_succeed( (get_machine_formulas(S), type_check(S,list(prob2_nodes)) )).
1248
1249		:- use_module(specfile,[b_mode/0, csp_mode/0, get_specification_description/2]).
1250		:- use_module(probcspsrc(haskell_csp),[channel_type_list/2]).
1251		:- use_module(translate,[translate_cspm_expression/2]).
1252		category(Category,Desc,Infos,ProcessedSubNodes) :- b_mode,
1253		b_category(Category,Infos,Subs),
1254		Subs \= [],
1255		get_specification_description(Category,Desc),
1256		maplist(process_formula,Subs,ProcessedSubNodes).
1257		category(operations,Desc,Infos,Subs) :- Infos = [], % not expanded
1258		b_mode,
1259		get_specification_description(operations,Desc),
1260		findall(category(OpName,[propagated],Guards), get_guards(OpName,Guards), Subs), Subs \= [].
1261		category(variants,Desc,Infos,Subs) :- Infos = [], % not expanded
1262		b_mode,
1263		get_specification_description(variants,Desc),
1264		findall(category(OpNameV,[propagated],[PF]),
1265		(b_get_operation_variant(OpName,ConvOrAnt,Variant),
1266		(ConvOrAnt=convergent -> string_concatenate(OpName,' (<)',OpNameV)
1267		; string_concatenate(OpName,' (<=)',OpNameV)),
1268		process_formula(Variant,PF)), Subs), Subs \= [].
1269		category(definitions,Desc,[],Subs) :- b_mode,
1270		get_specification_description(definitions,Desc),
1271		findall(Def,b_definition(Def),Subs), Subs \= [].
1272		category(channels,'CHANNELS',[],Channels) :- csp_mode,
1273		findall( formula(b(string(ChannelDescr),string,[]),Channel),
1274		(channel_type_list(Channel,TypeList), % something like [dataType('SubSubMsg'),intType,boolType]
1275		translate_cspm_expression(dotTuple(TypeList),TypeString),
1276		ajoin([Channel,' : ', TypeString],ChannelDescr)
1277		), Channels).
1278
1279
1280		%get_csp_datatype(bind(DT,string(TypeString))) :-
1281		% haskell_csp:dataTypeDef(DT,TypeList), % something like [dataType('SubSubMsg'),intType,boolType]
1282		% translate_cspm_expression(dataTypeDef(TypeList),TypeString).
1283		%get_csp_subtype(bind(DT,string(TypeString))) :-
1284		% haskell_csp:subTypeDef(DT,TypeList), % something like [dataType('SubSubMsg'),intType,boolType]
1285		% translate_cspm_expression(dataTypeDef(TypeList),TypeString).
1286
1287
1288		:- use_module(translate,[translate_bexpression_to_unicode/2]).
1289		process_formula(AST,formula(AST,PPString)) :- translate_bexpression_to_unicode(AST,PPString). % TO DO: we could also return location info
1290
1291		:- use_module(probsrc(bsyntaxtree),[conjunction_to_list/2]).
1292		:- use_module(bmachine,[b_get_properties_from_machine/1,get_all_assertions_from_machine/1,
1293		b_get_invariant_from_machine/1, b_get_machine_goal/1,
1294		b_get_machine_heuristic_function/1, b_get_machine_searchscope/1,
1295		b_get_machine_variables/1, b_get_machine_constants/1,
1296		b_get_machine_set/2, b_machine_has_variables/0,
1297		b_get_operation_variant/3]).
1298		b_category(sets,Exp,Subs) :- findall(ST,b_get_machine_or_int_set(ST),Subs),
1299		(b_machine_has_variables -> Exp = [] ; Exp=[expanded]).
1300		b_category(constants,Exp,Subs) :- b_get_machine_constants(Subs),
1301		(b_machine_has_variables -> Exp = [] ; Exp=[expanded]).
1302		b_category(variables,[expanded],Subs) :- b_get_machine_variables(Subs).
1303		b_category(properties,[],Subs) :-
1304		b_get_properties_from_machine(Props),
1305		conjunction_to_list(Props,Subs).
1306		b_category(assertions,[],Subs) :- get_all_assertions_from_machine(Subs).
1307		b_category(invariants,[],Subs) :-
1308		b_get_invariant_from_machine(Inv),
1309		conjunction_to_list(Inv,Subs).
1310		% TO DO: add guard theorems,...
1311
1312		:- use_module(specfile,[animation_minor_mode/1]).
1313		b_get_machine_or_int_set(STyped) :- b_get_machine_set(_,STyped).
1314		%b_get_machine_or_int_set(b(integer_set('INT'),set(integer),[])) :-
1315		% \+ animation_minor_mode(_). % INT only exists in pure B mode
1316		b_get_machine_or_int_set(b(interval(L,U),set(integer),[])) :- % INT is usually not expanded by interpreter: better provide interval directly
1317		\+ animation_minor_mode(_), % INT only exists in pure B mode
1318		% get_preference(maxint,MAXINT), get_preference(minint,MININT),
1319		L = b(min_int,integer,[]),
1320		U = b(max_int,integer,[]).
1321
1322		:- use_module(pref_definitions,[b_get_set_pref_definition/3]).
1323		:- use_module(bmachine,[b_get_machine_animation_function/2]).
1324		b_definition(category('GOAL',[propagated],ProcessedSubNodes)) :-
1325		b_get_machine_goal(G),
1326		conjunction_to_list(G,Subs),
1327		maplist(process_formula,Subs,ProcessedSubNodes).
1328		b_definition(category('SCOPE',[propagated],[PF])) :-
1329		b_get_machine_searchscope(F), process_formula(F,PF).
1330		b_definition(category('HEURISTIC_FUNCTION',[propagated],[PF])) :-
1331		b_get_machine_heuristic_function(F), process_formula(F,PF).
1332		b_definition(category('ANIMATION_FUNCTIONS',[],PFS)) :-
1333		findall(PF,(b_get_machine_animation_function(AF,_Nr), process_formula(AF,PF)),PFS),
1334		PFS \= [].
1335		b_definition(category('ANIMATION_IMAGES',[],PFS)) :-
1336		get_animation_images(L), L \= [],
1337		findall(formula(b(string(File),string,[]),Nr),(member(image_file(Nr,File),L)),PFS),
1338		PFS \= [].
1339		b_definition(category(DefName,[propagated],[PF])) :-
1340		b_get_set_pref_definition(DefName,_String,F), process_formula(F,PF).
1341		% TO DO: add ANIMATION Images,... ?
1342
1343		:- use_module(predicate_debugger,[get_unsimplified_operation_guard/2]).
1344		get_guards(OpName,ProcessedSubNodes) :-
1345		get_unsimplified_operation_guard(OpName,Guard),
1346		\+ is_initialisation_op(OpName),
1347		conjunction_to_list(Guard,Subs),
1348		maplist(process_formula,Subs,ProcessedSubNodes).
1349
1350		is_initialisation_op('$setup_constants').
1351		is_initialisation_op('$initialise_machine').
1352
1353
1354		% API for showing Tk Animation Images in Java FX (or other):
1355		:- use_module(state_viewer_images,[get_animation_images/1,
1356		get_animation_image_grid/6, get_react_to_item_right_click_options/4, react_to_item_right_click/6]).
1357		get_animation_image_list(ImageList) :- get_animation_images(ImageList).
1358		% Format: [image_file(0,'images/empty_box_white.gif'),...,image_file(6,'images/F.gif')]
1359
1360		get_animation_image_matrix_for_state(ID,Matrix,MinRow,MaxRow,MinCol,MaxCol) :-
1361		(get_animation_image_grid(ID,M,M1,M2,M3,M4)
1362		-> Matrix=M, MinRow=M1, MaxRow=M2, MinCol=M3, MaxCol=M4
1363		; Matrix=[], MinRow = -1, MaxRow = 0, MinCol = -1, MaxCol = 0).
1364		% Format: [entry(1,1,image(0)),... entry(2,3,text(some_atom)),...], entry(Row,Col,ImgOrText)
1365
1366		% returns a list of atoms (strings) for the various options that are available in the state ID
1367		% for Row/Col (Y/X)
1368		get_react_to_item_right_click_options_for_state(ID,Row,Col,Options) :-
1369		get_react_to_item_right_click_options(ID,Col,Row,Options).
1370
1371		% should be called for one option provided by get_react_to_item_right_click_options_for_state
1372		react_to_item_right_click_option_for_state(ID,Row,Col,Option,TransitionID,NewID) :-
1373		react_to_item_right_click(ID,Col,Row,Option,TransitionID,NewID).
1374
1375		% | ?- prob2_interface:get_react_to_item_right_click_options_for_state(3,1,1,L).
1376		% L = ['Set(1,1,1)','Set(1,1,2)','Set(1,1,3)','Solve'|...] ?
1377		% | ?- prob2_interface:react_to_item_right_click_option_for_state(3,1,1,'Set(1,1,1)',NewID).
1378		% Performed: Set(int(1),int(1),int(1))
1379		% NewID = ..., TransitionID=...
1380
1381		/**
1382		Takes a predicate and finds a list of all state ids for which the
1383		predicate holds. The states that are not intitialized (i.e. root) are
1384		included in the list. The list that is returned is therefore the union
1385		of the uninitialised states and the states for which the predicate holds.
1386
1387		#### called by:
1388		* ProB 2.0: GetStatesFromPredicate
1389		*/
1390		:- mode get_states_for_predicate(+Raw,-States,-Errors).
1391		get_states_for_predicate(Raw,States,Errors) :-
1392		evaluate_formula_typecheck('#PREDICATE',Raw,Typed,Errors),
1393		findall(StateId,get_state_for_predicate(StateId,Typed),States).
1394
1395		get_state_for_predicate(StateId,Typed) :-
1396		state_space:visited_expression(StateId,StatePacked),
1397		( is_initialised_state(StateId) ->
1398		expand_const_and_vars_to_full_store(StatePacked,State),
1399		eval_predicate(State,Typed,'TRUE',_,_)
1400		;
1401		true
1402		).
1403
1404		/**
1405		This cycles through all of the solutions and extracts the string
1406		representation of the solutions.
1407		*/
1408		prettyprint_solutions(_Truncate,[],[]).
1409		prettyprint_solutions(Truncate,[bind(Name,Res)|T],[PP|R]) :-
1410		pretty_print_bvalue(Truncate,Res,PPRes), % pretty_print_bvalue_unicode ?
1411		PP = solution(Name,PPRes),
1412		prettyprint_solutions(Truncate,T,R).
1413
1414		/**
1415		Allows Strings to be parsed and evaluated. Used for EvalB
1416
1417		#### called by:
1418		* ProB 2.0: RemoteEvaluateCommand
1419		*/
1420		:- use_module(eval_strings).
1421		evalb_evaluate_formula(Codes, result(R,Solutions,Quantor,Vars,Warn)):-
1422		eval_strings:eval_codes(Codes,exists,R,Warn,LocalState,TypeInfo),
1423		extract_typeinfo(TypeInfo,Quantor,Vars),
1424		prettyprint_solutions(truncate,LocalState,Solutions).
1425
1426		evalb_evaluate_tautology(Codes, result(R,Solutions,Quantor,Vars,Warn)):-
1427		eval_strings:eval_codes(Codes,forall,R,Warn,LocalState,TypeInfo),
1428		extract_typeinfo(TypeInfo,Quantor,Vars),
1429		prettyprint_solutions(truncate,LocalState,Solutions).
1430
1431		extract_typeinfo(expression(_),expression,[]).
1432		extract_typeinfo(predicate(forall(BL)),forall,L) :- translate_list(BL,L).
1433		extract_typeinfo(predicate(exists(BL)),exists,L) :- translate_list(BL,L).
1434		extract_typeinfo(predicate(no_outer_quantifier),predicate,[]).
1435
1436		translate_list([],[]).
1437		translate_list([H|T],[HT|TT]) :- translate_bexpression(H,HT), translate_list(T,TT).
1438
1439		/**
1440		Takes a list of state ids and a predicate and finds all of the states
1441		for which the predicate is true
1442
1443		#### called by:
1444		* ProB 2.0: FilterStatesForPredicateCommand
1445		*/
1446		:- mode filter_states_for_predicate(+Raw,+States,-Filtered).
1447		filter_states_for_predicate(Raw,States,Filtered) :-
1448		evaluate_formula_typecheck('#PREDICATE',Raw,Typed,Errors),
1449		(Errors=[] ->
1450		filter_states_for_typed_predicate(Typed,States,Filtered)
1451		;
1452		Filtered = errors(Errors)
1453		).
1454
1455		filter_states_for_typed_predicate(_,[],[]).
1456		filter_states_for_typed_predicate(Typed,[Id|States],Filtered) :-
1457		get_state_with_deferred_sets(Id,State,Kind,_),
1458		( Kind = full_initialised_state -> %is_initialised_state(Id) ->
1459		(eval_predicate(State,Typed,'TRUE',_,_) ->
1460		Filtered = [Id|Rest] ;
1461		Filtered = Rest
1462		)
1463		; Filtered = [Id|Rest]
1464		),
1465		filter_states_for_typed_predicate(Typed,States,Rest).
1466
1467		/* ------------------------- */
1468		/* Formula Expansion */
1469		/* ------------------------- */
1470
1471		/**
1472		Inserts a formula into bvisual2 module
1473		The formula is inserted as a child of level "user" in bvisual2
1474
1475		#### called by:
1476		* ProB 2.0: InsertFormulaForVisualizationCommand
1477		*/
1478		:- mode insert_formula_for_expansion(+AST,-Id).
1479		insert_formula_for_expansion(Typed,Id) :- Typed = b(_,_,_),!,
1480		suppress_rodin_positions,
1481		bv_insert_formula(Typed,user,Id).
1482
1483		insert_formula_for_expansion(AST,Id) :-
1484		suppress_rodin_positions,
1485		b_type_expression(AST,[variables],_,Typed,Errors),
1486		( Errors == [] ->
1487		bv_insert_formula(Typed,user,Id)
1488		; otherwise ->
1489		add_error_and_fail(eclipse_interface,'Could not type-check AST','')).
1490
1491		/**
1492		Uses the bvisual2 module to recursively expand and evaluate a specified formula.
1493		This formula must first be inserted into the bvisual2 module using the predicate
1494		insert_formula_for_expansion. The formula is then identified by the Id specified
1495		at the time of insertion.
1496
1497		#### called by:
1498		* ProB 2.0: ExpandFormulaCommand
1499		*/
1500		:- mode expand_formula(+Id,+StateId,-Tree).
1501		expand_formula(Id,StateId,Tree) :-
1502		bv_expand_formula(Id,Label,Children),
1503		bv_get_values([Id],StateId,[Value]),
1504		bv_get_values(Children,StateId,ChildrenValues),
1505		find_all_subformulas(StateId,Children,ChildrenValues,AsTrees),
1506		Tree = formula(Label,Value,Id,AsTrees).
1507
1508		find_all_subformulas(_,[],_,[]).
1509		find_all_subformulas(StateId,[Id|RestI],[Value1|RestV],[formula(Label,Value1,Id,Trees)|RestT]) :-
1510		bv_expand_formula(Id,Label,Children),
1511		bv_get_values(Children,StateId,CValues),
1512		find_all_subformulas(StateId,Children,CValues,Trees),
1513		find_all_subformulas(StateId,RestI,RestV,RestT).
1514
1515
1516		/* ------------------------- */
1517		/* Model Checking */
1518		/* ------------------------- */
1519
1520		/**
1521		#### do_modelchecking(+Time,+Options,-Result,stats(-NrNodes,-NrTrans,-NrProcessed))
1522		* +Time : Timeout specified by the user in ms
1523		* +Options : List of options specified by the user. Used for predicate do_modelchecking(Time,Options,Result)
1524		* -NrNodes : total number of nodes in state space. Calculated with get_state_space_stats
1525		* -NrTrans : total number of nodes in state space. Calculated with get_state_space_stats
1526		* -NrProcessed : total number of calculated nodes in state space. Calculated with get_state_space_stats
1527		When Time Milliseconds have elapsed the modelchecker should stop after its next step
1528
1529		#### called by:
1530		* ProB Plugin: ModelCheckingCommand
1531		* ProB 2.0: ModelCheckingStepCommand
1532		*/
1533		:- mode do_modelchecking(+Time,+Options,-Result,-Stats).
1534		do_modelchecking(Time, Options, Result, stats(NrNodes,NrTrans,NrProcessed)) :-
1535		statistics(walltime, [CurTime,_]), /* get current time in ms */
1536		LimitTime is CurTime+Time,
1537		option_set(find_deadlocks, Options, Deadlock),
1538		option_set(find_invariant_violations, Options, Invariant),
1539		option_set(find_assertion_violations, Options, Assertions),
1540		option_set(inspect_existing_nodes, Options, InspectExistingNodes),
1541		option_set(stop_at_full_coverage, Options, StopAtFullCoverage),
1542		(option_set(breadth_first_search, Options, 1) -> set_depth_breadth_first_mode(breadth_first) ;
1543		option_set(depth_first_search, Options, 1) -> set_depth_breadth_first_mode(depth_first) ;
1544		set_depth_breadth_first_mode(mixed)),
1545		option_set(find_goal, Options, Goal),
1546		(option_set(partial_guard_evaluation, Options, 1)
1547		-> preferences:get_preference(pge,PartialGuardEvaluation)
1548		; PartialGuardEvaluation = off),
1549		(option_set(partial_order_reduction, Options, 1)
1550		-> preferences:get_preference(por,WithPOR)
1551		; WithPOR = off),
1552		% no partial guards evaluation
1553		MaxNumberOfStatesToCheck=100000,
1554		user:do_model_check(MaxNumberOfStatesToCheck, _, LimitTime, Res, Deadlock, Invariant, Goal,Assertions,
1555		StopAtFullCoverage, WithPOR, PartialGuardEvaluation, InspectExistingNodes),
1556		build_modelcheck_return(Res, Result),
1557		get_state_space_stats(NrNodes, NrTrans, NrProcessed).
1558
1559		/**
1560		Sets the goal for model checking. The Option search_for_goal needs to be set when starting
1561		model checking in order for this to have an effect on the model checking.
1562
1563		#### called by:
1564		* ProB 2.0: SetBGoalCommand
1565		*/
1566		:- mode set_goal_for_model_checking(+Goal).
1567		set_goal_for_model_checking(Goal) :-
1568		evaluate_formula_typecheck('#PREDICATE',Goal,TypedGoal,Errors),
1569		(Errors = [] ->
1570		b_set_parsed_typed_machine_goal(TypedGoal);
1571		add_error_and_fail(set_goal_for_model_checking,typeerror,Errors)
1572		).
1573
1574		/**
1575		Takes an atom and unifies Result with 1 if the atom is in the List.
1576		Otherwise, Result is unified with 0.
1577		*/
1578		:- mode option_set(+Element, +List, -Result).
1579		option_set(Element, List, Result) :-
1580		( member(Element,List)
1581		-> Result = 1
1582		; Result = 0).
1583
1584		:- mode build_modelcheck_return(+MCRes, -JavaResult).
1585		build_modelcheck_return(MCRes, JavaResult) :-
1586		build_modelcheck_return2(MCRes, JavaResult) -> true
1587		; 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)*/
1588		current_state_id(State), JavaResult=general_error(State, MCRes).
1589
1590		build_modelcheck_return2(no, not_yet_finished(100000)).
1591		build_modelcheck_return2([timeout,N], not_yet_finished(N1)) :- N1 is 100000 - N.
1592		build_modelcheck_return2(deadlock, deadlock(State)):- current_state_id(State).
1593		build_modelcheck_return2(invariant_violation, invariant_violation(State)):- current_state_id(State).
1594		build_modelcheck_return2(assertion_violation, assertion_violation(State)):- current_state_id(State).
1595		build_modelcheck_return2(state_error, state_error(State)):- current_state_id(State).
1596		build_modelcheck_return2(state_error(_), state_error(State)):- current_state_id(State).
1597		build_modelcheck_return2(goal_found, goal_found(State)) :- current_state_id(State).
1598		build_modelcheck_return2(well_definedness_error, well_definedness_error(State)) :- current_state_id(State).
1599		build_modelcheck_return2(general_error_occurred, general_error(State)):- current_state_id(State).
1600		build_modelcheck_return2(full_coverage, full_coverage).
1601		build_modelcheck_return2(all, Res) :- max_reached_or_timeout_for_node(_),!, Res=ok_not_all_nodes_considered.
1602		build_modelcheck_return2(all, ok).
1603
1604		:- use_module(symbolic_model_checker(bmc),[bmc_symbolic_model_check/1]).
1605		:- use_module(symbolic_model_checker(kinduction), [kinduction_symbolic_model_check/1, tinduction_symbolic_model_check/1]).
1606		:- use_module(symbolic_model_checker(ic3), [ic3_symbolic_model_check/1]).
1607		symbolic_model_check(bmc,Result) :-
1608		bmc_symbolic_model_check(Result).
1609		symbolic_model_check(kinduction,Result) :-
1610		kinduction_symbolic_model_check(Result).
1611		symbolic_model_check(tinduction,Result) :-
1612		tinduction_symbolic_model_check(Result).
1613		symbolic_model_check(ic3,Result) :-
1614		ic3_symbolic_model_check(Result).
1615
1616		/**
1617		Computes the coverage statistics of the current state space at any given time.
1618		The information of interest includes the total number of nodes and transitions, as well as
1619		a list of statistics about the nodes and operations and a list of the operations that have been uncovered sofar.
1620
1621		#### called by:
1622		* ProB Plugin: ComputeCoverageCommand
1623		* ProB 2.0: ComputeCoverageCommand
1624		*/
1625		:- use_module(coverage_statistics, [compute_the_coverage/5, operation_hit/2,query_node_hit/2, uncovered_operation/1]).
1626
1627		:- mode compute_efficient_statespace_stats(-NrNodes, -NrTrans, -NrProcessed).
1628		compute_efficient_statespace_stats(NrNodes, NrTrans, NrProcessed) :-
1629		get_state_space_stats(NrNodes, NrTrans, NrProcessed).
1630
1631		:- mode compute_coverage(-TotalNodeNr,-TotalTransSum,-NodeStat,-OpStat,-Uncovered).
1632		compute_coverage(TotalNodeNr,TotalTransSum,NodeStat,OpStat,Uncovered) :-
1633		compute_the_coverage(_,TotalNodeNr,TotalTransSum,false,false),
1634		findall(S2,(operation_hit(OpS,Nr),string_concatenate(':',Nr,S1),string_concatenate(OpS,S1,S2)),OpStat),
1635		findall(S2,(query_node_hit(Prop,Nr),string_concatenate(':',Nr,S1),string_concatenate(Prop,S1,S2)),NodeStat),
1636		findall(OpName, uncovered_operation(OpName),Uncovered).
1637
1638
1639		get_modelchecking_coverage(TotalNodeNr,TotalTransSum,NodeStat,OpStat,Uncovered) :-
1640		compute_the_coverage(_,TotalNodeNr,TotalTransSum,false,false),
1641		findall(entry(OpS,Nr),operation_hit(OpS,Nr),OpStat),
1642		findall(entry(Prop,Nr),query_node_hit(Prop,Nr),NodeStat),
1643		findall(OpName, uncovered_operation(OpName),Uncovered).
1644
1645
1646		/**
1647		Performs deadlock freedom checking with constraint Predicate and calulates the Result.
1648
1649		#### called by:
1650		* ProB 2.0: ConstraintBasedDeadlockCheckCommand
1651		*/
1652		:- mode prob2_deadlock_freedom_check(+Predicate,-Result).
1653		prob2_deadlock_freedom_check(Predicate,Result) :-
1654		b_type_expression(Predicate,[variables],pred,TPredicate,Errors),
1655		( Errors == [] ->
1656		prob2_deadlock_freedom_check1(TPredicate,Result)
1657		; otherwise ->
1658		Result = errors(Errors)).
1659		prob2_deadlock_freedom_check1(Predicate,Result) :-
1660		% always do a deadlock check with SMT mode enabled
1661		call_with_smt_mode_enabled(prob2_deadlock_freedom_check2(Predicate,Result)).
1662		prob2_deadlock_freedom_check2(Predicate,Result) :-
1663		user_interruptable_call_det(user:catch_clpfd_overflow_call1(cbc_deadlock_freedom_check(State,Predicate,0)),
1664		InterruptResult),!,
1665		( InterruptResult = interrupted ->
1666		Result = interrupted
1667		; State = time_out ->
1668		Result = interrupted
1669		; otherwise ->
1670		Result = deadlock(Transition,StateId),
1671		add_artificial_transition(root,deadlock_check,State,StateId,Transition)).
1672		prob2_deadlock_freedom_check2(_Predicate,no_deadlock_found).
1673
1674
1675
1676
1677
1678
1679		/**
1680		Performs invariant checking for either for all operations or a list of operations.
1681
1682		#### called by:
1683		* ProB 2.0: ConstraintBasedInvariantCheckCommand
1684		*/
1685		:- mode prob2_invariant_check(+Ops,-Result).
1686		prob2_invariant_check(all,Result) :-
1687		findall(OpName,b_is_operation_name(OpName),Ops),
1688		prob2_invariant_check2(Ops,Result).
1689		prob2_invariant_check(ops(Ops),Result) :-
1690		prob2_invariant_check2(Ops,Result).
1691		prob2_invariant_check2(Ops,Result) :-
1692		call_with_smt_mode_enabled(prob2_invariant_check3(Ops,Result,[])).
1693		prob2_invariant_check3([]) --> !.
1694		prob2_invariant_check3([Op|Rest]) -->
1695		prob2_invariant_check_for_single_op(Op),
1696		prob2_invariant_check3(Rest).
1697		prob2_invariant_check_for_single_op(OpName,In,Out) :-
1698		( clpfd_interface:catch_clpfd_overflow_call1(b_state_model_check:state_model_check(OpName,State1,Operation,State2)) ->
1699		In = [counterexample(OpName,Trans1,Trans2)|Out],
1700		atom_concat( invariant_check_ , OpName, RootTrans),
1701		add_artificial_transition(root, RootTrans,State1,StateId1,Trans1),
1702		add_artificial_transition(StateId1,Operation,State2,_StateId2,Trans2)
1703		; otherwise ->
1704		In = Out).
1705
1706
1707		prob2_redundant_invariants(Redundant, Timeout) :-
1708		b_state_model_check:cbc_find_redundant_invariants(Redundant, Timeout).
1709
1710		/**
1711		creates a helper transition that is artificially added to the state space (e.g. during deadlock checking)
1712		This transition is added to the state space.
1713		A triple TransitionTuple in the form op(TransId,OpName,SrcId,DstId) for this transition is generated.
1714		*/
1715		:- mode add_artificial_transition(+SrcId,+Operation,+DstState,+DstId,-TransitionTuple).
1716		add_artificial_transition(SrcId,Operation,DstState,DstId,TransitionTuple) :-
1717		user:tcltk_add_new_transition_transid(SrcId,Operation,DstId,DstState,[],TransId),
1718		extract_op_name(Operation,OpName),
1719		TransitionTuple = op(TransId,OpName,SrcId,DstId).
1720
1721		/**
1722		computes the enabling relation information for the provided operations of interest
1723		get_enable_matrix(-PairsOfOperations,+EnableResult)
1724		PairsOfOperations: list of pair(Op1,Op2) of operations pairs for which the enable relation is to be computed
1725		EnableResult: list of terms enable_edges(Op1,Op2,enable_edges(E,KE,D,KD)) of same length
1726		*/
1727		get_enable_matrix(PairsOfOperations,EnableResult) :-
1728		maplist(compute_enable_matrix_entry(100),PairsOfOperations,EnableResult).
1729
1730		:- use_module(probsrc(enabling_analysis),[compute_cbc_enable_rel/4]).
1731		compute_enable_matrix_entry(ExtraTimeout,pair(OpName1,OpName2),
1732		enable_rel(OpName1,OpName2,
1733		enable_edges(Enable,KeepEnabled,Disable,KeepDisabled))) :-
1734		compute_cbc_enable_rel(OpName1,OpName2,ExtraTimeout,[Enable,KeepEnabled,Disable,KeepDisabled]).
1735
1736		/**
1737		Performs an LTL model checking step.
1738
1739		#### called by:
1740		* ProB 2.0: LtlCheckingCommand
1741		*/
1742		:- mode prob2_do_ltl_modelcheck(+Formula,+Max,-Result,-Errors).
1743		prob2_do_ltl_modelcheck(Formula,Max,Result,Errors) :-
1744		typecheck_temporal_formula(Formula,TypeCheckedFormula,Status),
1745		( Status=ok ->
1746		ltl_model_check_with_ce(TypeCheckedFormula,Max,init,Result1),
1747		prob2_ltl_adapt_operations(Result1,Result),
1748		get_error_messages(_WarningsOnly,Errors)
1749		; otherwise ->
1750		Result=typeerror,
1751		get_error_messages(_WarningsOnly,Errors)).
1752
1753		prob2_ltl_adapt_operations(counterexample(CE1,LoopEntry,PathToCE1), Res) :- !,
1754		Res = counterexample(CE,LoopEntry,PathToCE),
1755		create_simple_op_terms(PathToCE1,root,PathToCE),
1756		prob2_ltl_adapt_ce(CE1,CE).
1757		prob2_ltl_adapt_operations(Result,Result).
1758
1759		prob2_ltl_adapt_ce([],[]).
1760		prob2_ltl_adapt_ce([atom(StateId,_,OpTuple)|Irest],[Transition|Orest]) :-
1761		prob2_ltl_adapt_ce2(OpTuple,StateId,Transition),
1762		prob2_ltl_adapt_ce(Irest,Orest).
1763		prob2_ltl_adapt_ce2(none,_StateId,none).
1764		prob2_ltl_adapt_ce2((TransId,Action,DestId),StateId,op(TransId,Name,StateId,DestId)) :-
1765		extract_op_name(Action,Name).
1766
1767		/* ------------------------- */
1768		/* Plugin Handling */
1769		/* ------------------------- */
1770
1771		/**
1772		Activates a plugin with the given ID
1773
1774		#### called by:
1775		* ProB Plugin: ActivateUnitPluginCommand
1776		* ProB 2.0: ActivateUnitPluginCommand
1777		*/
1778		:- mode activate_plugin(+ID).
1779		activate_plugin(ID) :- add_internal_error('Plugins no longer supported',activate_plugin(ID)).
1780
1781		/**
1782		Gets the output for a given plugin
1783
1784		#### called by:
1785		* ProB Plugin: GetPluginResultCommand
1786		* ProB 2.0: GetPluginResultCommand
1787		*/
1788		:- mode get_plugin_output(+OutputID,-Output).
1789		get_plugin_output(OutputID,Output) :-
1790		add_internal_error('Plugins no longer supported',get_plugin_output(OutputID,Output)).
1791
1792
1793		/* ------------------------- */
1794		/* Find Traces */
1795		/* ------------------------- */
1796
1797		/**
1798		Finds a trace from the root state to the specified state in the current state space.
1799
1800		#### Parameters:
1801		* StateId
1802		* 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
1803
1804		#### called by:
1805		* ProB 2.0: GetShortestTraceCommand
1806		*/
1807		:- mode find_trace_to_node(+StateId,-Trace).
1808		find_trace_to_node(StateId, Trace) :-
1809		find_trace_from_node_to_node(root, StateId, Trace).
1810
1811		/**
1812		Finds a trace from one state to a goal state in the current state space.
1813
1814		#### Parameters:
1815		* FromId - Id of source node
1816		* ToId - Id of destination node
1817		* 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
1818
1819		#### called by:
1820		* ProB 2.0: GetShortestTraceCommand
1821		*/
1822		:- mode find_trace_from_node_to_node(+FromId,+ToId,-Trace).
1823		find_trace_from_node_to_node(FromId, ToId, Trace) :-
1824		(user:find_shortest_trace_to_node(FromId, ToId, OpIDs, _TraceIDs) ->
1825		trace_to_op_triple(OpIDs,FromId,Trace);
1826		Trace = no_trace_found
1827		).
1828
1829		/**
1830		Translates a list of transition ids to a list of op tuples op(TransId,OpName,SrcId,DestId)
1831		*/
1832		:- mode trace_to_op_triple(+ListOpIds,+CurID,-ListTuples).
1833		trace_to_op_triple([],_,[]).
1834		trace_to_op_triple([OpID|T], SrcID, [op(OpID,Name,SrcID,Dest)|OpT]) :-
1835		transition(SrcID,Action,OpID,Dest),
1836		extract_op_name(Action,Name),
1837		trace_to_op_triple(T,Dest,OpT).
1838
1839		/**
1840		Takes a given predicate and finds a state in the state space that satisfies the predicate.
1841		A helper transition is then added to go to the goal state.
1842
1843		#### called by:
1844		* ProB 2.0: FindValidStateCommand
1845		*/
1846		find_state_for_predicate(Predicate,UseInvariant,Result) :-
1847		evaluate_formula_typecheck('#PREDICATE',Predicate,TPredicate,Errors),
1848		( Errors == [] ->
1849		find_state_for_predicate1(TPredicate,UseInvariant,Result)
1850		; otherwise ->
1851		Result = errors(Errors)).
1852		find_state_for_predicate1(Predicate,UseInvariant,Result) :-
1853		user_interruptable_call_det(user:catch_clpfd_overflow_call1(
1854		b_set_up_valid_state_with_pred(State,Predicate,UseInvariant,none)), % TODO: pass UseConstantsFromStateID
1855		InterruptResult),!,
1856		( InterruptResult = interrupted ->
1857		Result = interrupted
1858		; State = time_out ->
1859		Result = interrupted
1860		; otherwise ->
1861		Result = state_found(Transition,StateId),
1862		add_artificial_transition(root,find_valid_state,State,StateId,Transition)).
1863		find_state_for_predicate1(_Predicate,_,no_valid_state_found).
1864
1865		/**
1866		#### called by:
1867		* ProB Plugin (de.prob.eventb.disprover.core): DisproverCommand
1868		*/
1869		:- mode cbc_disprove(+Goal,+AllHypotheses,+SelectedHypotheses,+TimeoutFactor,-OutResult).
1870		cbc_disprove(Goal,AllHypotheses,SelectedHypotheses,TimeoutFactor,OutResult) :-
1871		disprove(Goal,AllHypotheses,SelectedHypotheses,TimeoutFactor,OutResult),
1872		% remove the warning regarding double check, in rodin it is shown in the proof tree anyway
1873		(get_error(warning(disprover_inconsistent_hypotheses),_) ; true).
1874
1875		:- mode cbc_disprove(+Goal,+AllHypotheses,+SelectedHypotheses,+TimeoutFactor,-OutResult).
1876		cbc_disprove(Goal,AllHypotheses,SelectedHypotheses,TimeoutFactor,Options,OutResult) :-
1877		disprove_with_opts(Goal,AllHypotheses,SelectedHypotheses,TimeoutFactor,Options,OutResult),
1878		% remove the warning regarding double check, in rodin it is shown in the proof tree anyway
1879		(get_error(warning(disprover_inconsistent_hypotheses),_) ; true).
1880
1881		/**
1882		Takes a predicates and produces a result from the selected solver
1883		#### called by:
1884		* ProB 2.0: CbcSolveCommand
1885		*/
1886		:- mode cbc_solve(+Solver,+Predicate,-Identifiers,-Result).
1887		cbc_solve(Solver,Predicate,Identifiers,Result) :-
1888		cbc_solve(Solver,Predicate,_State,Identifiers,Result).
1889		cbc_solve(Solver,Predicate,State,Identifiers,Result) :-
1890		cbc_solve(Solver,Predicate,State,1,Identifiers,Result).
1891		cbc_solve(Solver,Predicate,State,TimeoutFactor,Identifiers,Result) :-
1892		cbc_solve_type(Solver,Predicate,TPredicate),
1893		find_identifier_uses(TPredicate,[],Identifiers),
1894		(atomic(State) -> Options = [solve_in_visited_state(State)] ; LState=State),
1895		cbc_solve_typed(Solver,TPredicate,LState,TimeoutFactor,Options,Result).
1896
1897		:- assert_must_succeed((cbc_solve_with_opts('PROB',[truncate(10)],
1898		equal(none,identifier(none,x),integer(none,10)),Identifiers,Result),
1899		Identifiers == [x],
1900		Result == solution([binding(x,int(10),'10')]))).
1901
1902		% This should be the new entry point for CbcSolveCommand, cbc_solve is no longer used
1903		:- mode cbc_solve_with_opts(+Solver,+Options,+Predicate,-Identifiers,-Result).
1904		cbc_solve_with_opts(Solver,Options,Predicate,Identifiers,Result) :-
1905		maplist(prob2_interface:check_cbc_solve_opts,Options),
1906		cbc_solve_type(Solver,Predicate,TPredicate),
1907		find_identifier_uses(TPredicate,[],Identifiers),
1908		(select(timeout_factor(TimeoutFactor),Options,Opts2) -> true ; TimeoutFactor=1,Opts2=Options),
1909		cbc_solve_typed(Solver,TPredicate,_,TimeoutFactor,Opts2,Result).
1910
1911		check_cbc_solve_opts(full_machine_state) :- !.
1912		check_cbc_solve_opts(solve_in_visited_state(ID)) :- !,atomic(ID).
1913		check_cbc_solve_opts(timeout_factor(Nr)) :- !,number(Nr).
1914		check_cbc_solve_opts(truncate(Nr)) :- !,number(Nr). % truncate pretty printing
1915		check_cbc_solve_opts(truncate) :- !. % truncate pretty printing
1916		check_cbc_solve_opts(force_evaluation) :- !. % force evaluation of symbolic results
1917		check_cbc_solve_opts(IO) :- add_internal_error('Illegal cbc_solve option:',IO).
1918
1919		cbc_solve_typed('PROB',Predicate,State,TimeoutFactor,Options,Result) :-
1920		solve_predicate(Predicate,State,TimeoutFactor,['SMT','CLPFD'|Options],Result).
1921		cbc_solve_typed('KODKOD',Predicate,State,TimeoutFactor,Options,Result) :-
1922		solve_predicate(Predicate,State,TimeoutFactor,['KODKOD','SMT','CLPFD'|Options],Result).
1923		cbc_solve_typed('SMT_SUPPORTED_INTERPRETER',Predicate,State,TimeoutFactor,Options,Result) :-
1924		solve_predicate(Predicate,State,TimeoutFactor,['SMT_SUPPORTED_INTERPRETER','SMT','CLPFD'|Options],Result).
1925		cbc_solve_typed(SOLVER,Predicate,_StateID,_,Options,Result) :- recognised_smt_solver(SOLVER,InternalName),
1926		(member(solve_in_visited_state(ID),Options) ->
1927		smt_solve_predicate_in_state(ID,InternalName,Predicate,_State,Result)
1928		; smt_solve_predicate(InternalName,Predicate,_State,Result)).
1929
1930		recognised_smt_solver('Z3',z3).
1931		recognised_smt_solver('CVC4',cvc4).
1932
1933		:- use_module(preferences,[temporary_set_preference/3,reset_temporary_preference/2]).
1934		cbc_solve_type('KODKOD',Pred,TPred) :- !,
1935		temporary_set_preference(try_kodkod_on_load,true,C),
1936		call_cleanup(cbc_solve_type2(Pred,TPred),
1937		reset_temporary_preference(try_kodkod_on_load,C)).
1938		cbc_solve_type(_,Pred,TPred) :- cbc_solve_type2(Pred,TPred).
1939		cbc_solve_type2(Pred,TPred) :-
1940		!, get_eval_scope(Scope),
1941		b_type_open_predicate(no_quantifier,Pred,Scope,TPred,Errors),
1942		(Errors=[] -> true ; add_error_and_fail(register_prob2_formula, 'Type-Errors: ', Errors)).
1943
1944		/**
1945		Takes a predicates and generates a pretty printed string
1946		*/
1947		:- assert_must_succeed((pretty_print_predicate(equal(none,identifier(none,x),integer(none,1)),[],Result),
1948		Result == 'x = 1')).
1949		:- assert_must_succeed((pretty_print_predicate(not_equal(none,identifier(none,x),integer(none,1)),[latex],Result),
1950		Result == '\\mathit{x} \\neq 1')).
1951		:- assert_must_succeed((pretty_print_predicate(not_equal(pos(2,-1,1,1,1,7),integer(pos(3,-1,1,1,1,2),1),
1952		integer(pos(4,-1,1,6,1,7),2)),[latex,nopt],PPString),
1953		PPString == '1 \\neq 2' )).
1954
1955		pretty_print_predicate(Pred,Options,PPString) :-
1956		select(nopt,Options,Opts2),
1957		!,
1958		temporary_set_preference(optimize_ast,false,CHNG1),
1959		pretty_print_predicate(Pred,Opts2,PPString),
1960		reset_temporary_preference(optimize_ast,CHNG1).
1961		pretty_print_predicate(Pred,Options,PPString) :-
1962		get_eval_scope(Scope),
1963		b_type_open_predicate(no_quantifier,Pred,Scope,TPred,Errors),
1964		(Errors=[] -> true ; add_error_and_fail(pretty_print_predicate, 'Type-Errors: ', Errors)),
1965		translate_pred(TPred,Options,PPString).
1966
1967		:- use_module(translate,[set_unicode_mode/0, unset_unicode_mode/0, unicode_mode/0,
1968		set_latex_mode/0, unset_latex_mode/0, latex_mode/0]).
1969		translate_pred(TPred,Options,PPString) :-
1970		select(unicode,Options,Opts2), \+ unicode_mode,
1971		!,
1972		set_unicode_mode,translate_pred(TPred,Opts2,PPString),unset_unicode_mode.
1973		translate_pred(TPred,Options,PPString) :-
1974		select(latex,Options,Opts2), \+ latex_mode,
1975		!,
1976		set_latex_mode,translate_pred(TPred,Opts2,PPString),unset_latex_mode.
1977		translate_pred(TPred,_,PPString) :-
1978		translate_bexpression(TPred,PPString).
1979
1980		% Constraint-Based Test-case generation
1981		% TO DO: return values
1982		:- use_module(sap,[cbc_gen_test_cases/5]).
1983		cbc_generate_test_cases(TargetPred,MaxDepth,OutputFile) :-
1984		% I am not sure whether we should call b_parse_machine_predicate(TargetPred,...) or not
1985		Events = all,
1986		cbc_gen_test_cases(Events,TargetPred,MaxDepth,OutputFile,_Uncovered).
1987
1988
1989
1990		:- use_module(sap,[create_testcase_path/5]).
1991		% example call | ?- prob2_interface:prob2_find_test_path([enter1],truth(unknown),200,R).
1992		:- mode prob2_find_test_path(+Events,+EndPredicate,+TimeoutMs,-ResultOpTerms).
1993		% Result is either errors(Errors), timeout, interrupt, infeasible_path, or list of Operation IDs
1994		prob2_find_test_path(Events,EndPredicate,TimeoutMs,ResultOpTerms) :-
1995		evaluate_formula_typecheck('#PREDICATE',EndPredicate,TPredicate,Errors),
1996		( Errors == [] ->
1997		prob2_find_test_path_aux(Events,TPredicate,TimeoutMs,ResultOpTerms)
1998		; ResultOpTerms = errors(Errors)).
1999
2000		prob2_find_test_path_aux(Events,TPredicate,TimeoutMs,ResOperationIds) :-
2001		( create_testcase_path(init,Events,TPredicate,TimeoutMs,Trace)
2002		-> (is_list(Trace) -> maplist(extract_opid,Trace,ResOperationIds)
2003		% Trace can be "timeout" or "interrupt", too
2004		; ResOperationIds=Trace)
2005		; ResOperationIds = infeasible_path).
2006
2007		extract_opid((TransId,OpTerm,StateId,DestId),op(TransId,Name,StateId,DestId)) :- extract_op_name(OpTerm,Name).
2008
2009		/* ------------------------- */
2010		/* Check CSP Assertion */
2011		/* ------------------------- */
2012
2013		/**
2014		Takes a list of assertions and produce a list of results and result traces.
2015
2016		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)
2017
2018		#### called by:
2019		* ProB 2.0: CSPAssertionsCommand
2020		*/
2021		:- mode check_csp_assertions(+Assertions,-Results,-ResultTraces).
2022		check_csp_assertions(Assertions,Results,ResultTraces) :-
2023		maplist(check_csp_assertion,Assertions,Results,ResultTraces).
2024
2025		check_csp_assertion(AssClause,Res,ResTrace1) :-
2026		read_from_codes(AssClause,Assertion),
2027		user:checkAssertion(Assertion,_PP,_Negated,Res,ResTrace),
2028		(ResTrace = no_counter_example -> ResTrace1 = []; ResTrace1=ResTrace).
2029
2030		/* ------------------------- */
2031		/* Preferences Interface */
2032		/* ------------------------- */
2033
2034		/**
2035		Returns a list of all the preferences with their current values
2036
2037		#### called by:
2038		* ProB 2.0: GetCurrentPreferencesCommand
2039		*/
2040		:- mode list_current_eclipse_preferences(-L).
2041		list_current_eclipse_preferences(L) :-
2042		findall(preference(A,B),find_eclipse_preference(A,B),L).
2043
2044		find_eclipse_preference(A,B) :-
2045		list_all_eclipse_preferences(X),
2046		member(preference(A,_,_,_,_),X),
2047		get_eclipse_preference(A,B).
2048
2049		/**
2050		Returns the current value of a specified preference.
2051
2052		#### called by:
2053		* ProB 2.0: GetPreferenceCommand
2054		*/
2055		get_eclipse_preference(PrefS,PrefVal) :-
2056		if(eclipse_preference(PrefS,PS),
2057		get_preference(PS,PrefVal),
2058		add_error_and_fail(get_eclipse_preference,'Unknown preference:',PrefS)).
2059
2060		/**
2061		Returns a list of all normal eclipse preferences as well as their information
2062		(i.e. type, description, category, and default value)
2063
2064		#### called by:
2065		* ProB Plugin: GetPreferencesCommand
2066		* ProB 2.0: GetDefaultPreferencesCommand
2067		*/
2068		:- mode list_eclipse_preferences(-L).
2069		list_eclipse_preferences(L) :-
2070		findall(preference(A,B,C,D,E),
2071		(get_eclipse_preference_infos(A,B,C,D,E),
2072		\+ advanced_eclipse_preference(A,_)), L).
2073		:- mode list_all_eclipse_preferences(-L). % also includes advanced eclipse preferences
2074		list_all_eclipse_preferences(L) :-
2075		findall(preference(A,B,C,D,E),get_eclipse_preference_infos(A,B,C,D,E),L).
2076
2077		get_eclipse_preference_infos(PrefString,Type,Description,Category,DefaultValue) :-
2078		eclipse_preference(PrefString,PS),
2079		%\+ advanced_eclipse_preference(PrefString,PS), % we now want to show all preferences in ProB 2
2080		preference_val_type(PS,Type),
2081		preference_description(PS,Description),
2082		preference_category(PS,Category),
2083		preference_default_value(PS,DefaultValue).
2084
2085		/**
2086		Sets a preference
2087
2088		#### called by:
2089		* ProB Plugin: SetPreferenceCommand
2090		* ProB 2.0: SetPreferenceCommand
2091		*/
2092		:- use_module(tools_strings, [convert_cli_arg/2]).
2093		:- mode set_eclipse_preference(+PrefS,+PrefVal).
2094		set_eclipse_preference(PrefS,PrefVal) :-
2095		convert_cli_arg(PrefVal,Value),
2096		convert_pref_value(Value,CValue),
2097	?	(eclipse_preference(PrefS,P)
2098		-> (set_preference(P,CValue)
2099		-> true
2100		; add_error(eclipse_preference,'Could not set preference: ',Value))
2101		; obsolete_eclipse_preference(PrefS)
2102		-> add_warning(eclipse_preference,'Obsolete preference: ',PrefS)
2103		; add_error_and_fail(eclipse_preference,'Unknown preference: ',PrefS)
2104		).
2105
2106		convert_pref_value('TRUE',V) :- !, V=true.
2107		convert_pref_value('FALSE',V) :- !, V=false.
2108		convert_pref_value(X,X).
2109
2110		/* ------------------------- */
2111		/* Apply Graph reduction */
2112		/* ------------------------- */
2113
2114		/**
2115		Takes a list of ignored events, and applies the signature merge algorithm
2116		from module `state_space_reduction` to the current state space.
2117
2118		#### called by:
2119		* ProB 2.0: ApplySignatureMergeCommand
2120		*/
2121		:- mode get_signature_merge_state_space(+IgnoredEvents,-Space).
2122		get_signature_merge_state_space(IgnoredEvents,Space) :-
2123		reset_ignored_events,
2124		set_ignored_events(IgnoredEvents),
2125		compute_signature_merge,
2126		findall(node(NodeId,Count,Color,Labels),extract_node_info(NodeId,Count,Color,simple_list,Labels),Nodes),
2127		findall(trans(TransId,Src,Dest,Label,Style,Color),extract_trans_info(true,TransId,Src,Dest,Label,Style,Color),Trans),
2128		Space = [Nodes,Trans].
2129
2130		/**
2131		Takes a list of ignored events, and calculates a transition diagram
2132		using module `state_space_reduction` for the current state space.
2133
2134		#### called by:
2135		* ProB 2.0: CalculateTransitionDiagramCommand
2136		*/
2137		:- mode get_transition_diagram(+ParsedExpr,-Space).
2138		get_transition_diagram(ParsedExpr,Space) :-
2139		evaluate_formula_typecheck('#EXPRESSION',ParsedExpr,TypedExpr,Errors),
2140		(Errors = [] -> true; add_error_and_fail(get_transition_diagram,typeerror,Errors)),
2141		compute_transition_diagram(TypedExpr),
2142		findall(node(NodeId,Count,Color,Labels),extract_node_info(NodeId,Count,Color,gen_label,Labels),Nodes),
2143		findall(trans(TransId,Src,Dest,Label,Style,Color),extract_trans_info(false,TransId,Src,Dest,Label,Style,Color),Trans),
2144		Space = [Nodes,Trans].
2145
2146		write_dotty_transition_diagram(Expression,Filename) :-
2147		write_dotty_for_expr(transition_diagram,Expression,Filename).
2148
2149		write_dotty_signature_merge(IgnoredEvents,Filename) :-
2150		write_signature_merge_to_dotfile(IgnoredEvents,Filename).
2151
2152		write_dotty_state_space(Filename) :-
2153		write_dotty(state_space,Filename).
2154
2155		:- use_module(meta_interface,[is_dot_command/1, call_dot_command/3]).
2156		% find out which commands only require a filename:
2157		is_dotty_command(Command) :- is_dot_command(Command).
2158		% call commands which generate a dot file (without requiring further arguments, such as an expression)
2159		write_dotty(Command,Filename) :- OptionalArgs=[],
2160		call_dot_command(Command,Filename,OptionalArgs).
2161
2162
2163		:- use_module(meta_interface,[is_dot_command_for_expr/1, call_dot_command_for_expr/4]).
2164		% find out which commands only require an expression and a filename:
2165		is_dotty_command_for_expr(Command) :- is_dot_command_for_expr(Command).
2166		% call commands which generate a dot file from an expression:
2167		write_dotty_for_expr(Command,Expr,Filename) :- OptionalArgs=[],
2168		call_dot_command_for_expr(Command,Expr,Filename,OptionalArgs).
2169
2170
2171		:- use_module(meta_interface,[command_additional_info/2, command_unavailable/2]).
2172
2173		% --------------------------------------------------------
2174		% New preferred API for calling DOT / TABLE commands in ProB2 JFX:
2175		% get_dot_commands_in_state/2 and call_dot_command_and_dot_in_state/5
2176		% get_table_commands_in_state/2 and call_table_command_in_state/4
2177
2178
2179		% example call: prob2_interface:get_dot_commands_in_state(1,List).
2180		get_dot_commands_in_state(StateID,List) :- get_commands_in_state(dot,StateID,List).
2181		get_commands_in_state(Category,StateID,List) :-
2182		user:tcltk_goto_node_with_id(StateID),
2183		findall(command(Command,Name,Description,NumberOfFormulaArgs,RelevantEclipsePrefs,AdditionalInfo,AvailMsg),
2184		(is_a_command(Category,Command,Name,Description,NumberOfFormulaArgs,RelevantPrefs,AdditionalInfo),
2185		maplist(convert_pref,RelevantPrefs,RelevantEclipsePrefs),
2186		(command_unavailable(Command,AvailMsg) -> true ; AvailMsg = available)),
2187		List).
2188		% example call: prob2_interface:get_table_commands_in_state(1,List).
2189		get_table_commands_in_state(StateID,List) :- get_commands_in_state(table,StateID,List).
2190
2191		convert_pref(Pref,Res) :- eclipse_preference(ECLIPSEPREF,Pref),!,Res=ECLIPSEPREF.
2192		convert_pref(P,P) :- print(cannot_convert_pref(P)),nl.
2193
2194		:- use_module(meta_interface,[is_dot_command/6, is_table_command/6]).
2195		is_a_command(dot,Command,Name,Description,NumberOfFormulaArgs,RelevantPreferences,AdditionalInfo) :-
2196		is_dot_command(Command,Name,Description,NumberOfFormulaArgs,RelevantPreferences,AdditionalInfo).
2197		is_a_command(table,Command,Name,Description,NumberOfFormulaArgs,RelevantPreferences,AdditionalInfo) :-
2198		is_table_command(Command,Name,Description,NumberOfFormulaArgs,RelevantPreferences,AdditionalInfo).
2199
2200
2201		% example call: prob2_interface:call_dot_command_and_dot_in_state(1,invariant,[],svg,'~/Desktop/out.svg').
2202		call_dot_command_and_dot_in_state(StateID,Command,Formulas,OutputType,OutputFile) :-
2203		user:tcltk_goto_node_with_id(StateID),
2204		call_dot_command_and_dot(Command,Formulas,OutputType,OutputFile).
2205
2206		call_dot_command_in_state(StateID,Command,Formulas,DotFile) :-
2207		user:tcltk_goto_node_with_id(StateID),
2208		call_dot_command_for_dotfile(Command,Formulas,DotFile).
2209
2210		% call a dot command for generating a DotFile; used by call_dot_command_and_dot
2211		call_dot_command_for_dotfile(Command,[],DotFile) :-
2212		is_dot_command(Command), !, OptionalArgs=[],
2213		call_dot_command(Command,DotFile,OptionalArgs).
2214		call_dot_command_for_dotfile(Command,[Expr],DotFile) :-
2215		is_dot_command_for_expr(Command), !, OptionalArgs=[],
2216		call_dot_command_for_expr(Command,Expr,DotFile,OptionalArgs).
2217		call_dot_command_for_dotfile(Command,Formulas,DotFile) :-
2218		add_internal_error('Illegal dot call: ',call_dot_command_for_dotfile(Command,Formulas,DotFile)),
2219		fail.
2220
2221		% call a dot command and generate dot, canon, png, svg, pdf output file
2222		% example call: prob2_interface:call_dot_command_and_dot(state_space,[],dot,'~/Desktop/out.dot').
2223		% prob2_interface:call_dot_command_and_dot(state_space,[],svg,'~/Desktop/out.svg')
2224		:- use_module(tools_commands,[gen_dot_output_env/6]).
2225		:- use_module(system_call,[get_temporary_filename/2]).
2226		%call_dot_command_and_dot(Command,Formulas,dot,DotFile) :- !, call_dot_command_for_dotfile(Command,Formulas,DotFile).
2227		call_dot_command_and_dot(Command,Formulas,OutputType,OutputFile) :-
2228		get_temporary_filename('prob2_dot_output.dot',DotFile),
2229		call_dot_command_for_dotfile(Command,Formulas,DotFile), % generate Dotfile
2230		(command_additional_info(Command,preferred_dot_type(Cmd)) ; Cmd=default),
2231		gen_dot_output_env(DotFile,Cmd,OutputType,OutputFile,[detached(false)],no_process_wait). % layout and convert Dotfile to target output
2232
2233
2234		% example call: prob2_interface:call_table_command_in_state(1,expr_as_table,[integer(pos,1)],Table).
2235		:- use_module(meta_interface,[call_command/5]).
2236		call_table_command_in_state(StateID,Command,Formulas,TableResult) :-
2237		(user:tcltk_goto_node_with_id(StateID) -> true
2238		; add_error(call_table_command_in_state,'Could not reach state: ',StateID)
2239		),
2240		(Formulas=[_|_],is_table_command(Command,_,_,0,_,_)
2241		-> ActualArgs = [TableResult] % correct bug in ProB2 Java code
2242		; append(Formulas,[TableResult],ActualArgs)
2243		), OptionalArgs=[],
2244		debug_println(9,call_command(table,Command,_,ActualArgs,OptionalArgs)),
2245		call_command(table,Command,_,ActualArgs,OptionalArgs), debug_println(9,result(TableResult)),
2246		!.
2247		call_table_command_in_state(StateID,Command,Formulas,TableResult) :-
2248		add_error(call_table_command_in_state,'Table command failed:',call_table_command_in_state(StateID,Command,Formulas,TableResult)),
2249		TableResult = list([list(['ERROR OCCURED'])]).
2250
2251
2252		/**
2253		Writes a dot representation of the given state to the specified file.
2254
2255		*/
2256		:- mode write_dot_for_state_viz(+StateId, +Filename).
2257		write_dot_for_state_viz(StateId, Filename) :-
2258		get_state(StateId, State),
2259		print_cstate_graph(State, Filename).
2260
2261		/**
2262		Generates information about the nodes found during state space reduction
2263
2264		#### Generated Information:
2265		* Count - number of concrete states combined in the abstract state
2266		* Color - the color used to represent this state type in a visualization
2267		* Labels - determine the labels that should appear on a node in a visualization
2268		*/
2269		:- mode extract_node_info(+NodeId,-Count,-Color,+LabelGenerator,-Labels).
2270		extract_node_info(NodeId,Count,Color,LabelGenerator,Labels) :-
2271		get_reduced_node(AbsState,Count,Witness,NodeId),
2272		generate_node_color(NodeId,Witness,AbsState,Count,Color),
2273		generate_node_labels(LabelGenerator,AbsState,Labels).
2274
2275		/**
2276		Generates information about the transitions created during state space reduction
2277
2278		#### Generated Information:
2279		* Src - ID corresponding to the abstract state that is the source of the abstract transition with TransId
2280		* Dest - ID corresponding to the abstract state that is the destination of the abstract transition with TransId
2281		* Label - the label that should appear on a transition in a visualization
2282		* Style - the style that should be applied to a transition of this type in a visualization (e.g. dashed)
2283		* Color - the color used to represent a transition of this type in a visualization
2284		*/
2285		:- mode extract_trans_info(+ShowSelfLoops,+TransId,-Src,-Dest,-Label,-Style,-Color).
2286		extract_trans_info(ShowSelfLoops,TransId,Src,Dest,Label,Style,Color) :-
2287		reduced_trans(Src,AbsAction,Count,Dest,TransId),
2288		generate_transition_label(AbsAction,Count,Label),
2289		generate_transition_color_and_style(ShowSelfLoops,Src,AbsAction,Dest,Color,Style).
2290
2291
2292		/* ------------------ */
2293		/* Get Errors */
2294		/* ------------------ */
2295
2296		/**
2297		Returns a list of strings containing all error messages (of the error_manager).
2298		Clears all the errors. Returns the empty list if no errors occurred since
2299		the last call to get_error_messages.
2300
2301		#### called by:
2302		* ProB 2.0: GetErrorsCommand
2303		*/
2304		:- mode get_error_messages(-WarningsOnly,-ListOfErrMsgs).
2305		get_error_messages(WarningsOnly,ListOfErrMsgs) :-
2306		(real_error_occurred -> WarningsOnly = false ; WarningsOnly = true),
2307		ignore_user_interrupt_det((get_all_errors_and_reset(ListOfErrMsgs) -> true ; ListOfErrMsgs=[])).
2308
2309		% each error is of the form: error(ErrMsg,ErrType,ErrLocations)
2310		% ErrMsg is an atom (aka string)
2311		% ErrType is warning, internal_error or error
2312		% ErrLocations is a list of terms error_span(Filename,StartLine,StartCol,EndLine,EndCol)
2313		% Note: Filename is '' when not known
2314		:- mode get_error_messages_with_span_info(-WarningsOnly,-ListOfErrMsgTerms).
2315		get_error_messages_with_span_info(WarningsOnly,ListOfErrMsgTerms) :-
2316		(real_error_occurred -> WarningsOnly = false ; WarningsOnly = true),
2317		ignore_user_interrupt_det(get_all_errors_with_span_info_and_reset(ListOfErrMsgTerms)).
2318
2319
2320
2321		/* ------------------------- */
2322		/* Evalstore */
2323		/* ------------------------- */
2324
2325		/**
2326		TODO: Please document what this does.
2327
2328		#### called by:
2329		* ProB 2.0: EvalstoreCreateByStateCommand
2330		*/
2331		es_copy_from_statespace(StateId,EvalstoreId) :-
2332		evalstore_create_store_by_state(StateId,EvalstoreId).
2333
2334		/**
2335		TODO: Please document what this does.
2336
2337		#### called by:
2338		* ProB 2.0: EvalstoreEvalCommand
2339		*/
2340		:- mode es_eval(+EvalstoreId,+UntypedFormula,+Timeout,-Result).
2341		es_eval(EvalstoreId,UntypedFormula,Timeout,Result) :-
2342		evalstore_eval_formula(EvalstoreId,UntypedFormula,Timeout,Result1), !,
2343		(Result1 = ok(V,TypedIds,StoreId) ->
2344		Result = ok(V,PP,Ids,StoreId),
2345		get_texpr_ids(TypedIds,Ids),
2346		es_eval_translate(V,PP)
2347		; otherwise -> Result = Result1).
2348		es_eval_translate(pred(V),V).
2349		es_eval_translate(value(V),PP) :-
2350		translate_bvalue(V,PP).
2351
2352		% ####################
2353
2354		/**
2355
2356		Animates randomly number of steps until a certain (LTL?) condition is fulfilled.
2357
2358		#### Called by:
2359		* ProB 2.0: ExecuteUntilCommand
2360
2361		#### Arguments
2362		* CurState - the ID of the current state
2363		* Condition - a condition that should be satisfied at some point (this come as parsed term from the ProB2)
2364
2365		#### Generated Information:
2366		* Trace - a list of triples representing a trace in the state space of the model being analysed
2367		* Result - the result found: ltl_found, typeerror, max_nr_of_steps_reached, deadlock
2368		*/
2369		:- mode generate_trace_until_condition_fulfilled(+CurState,+Condition,-Trace,-Result).
2370		generate_trace_until_condition_fulfilled(CurState,Condition,Trace,Result) :-
2371		typecheck_temporal_formula(Condition,TypeCheckedCondition,Status),
2372		( Status=ok -> find_trace1(CurState,TypeCheckedCondition,no_loop,100000,Trace, Result) %FIXME: turn maximal numver of steps into an argument?
2373		; otherwise -> get_error_messages(_WOnly,_Errors), % Reset errors. We don't want to throw a ProBError on the Java side because the result is capsuled in Result.
2374		Result=typeerror, Trace=[]).
2375
2376		find_trace1(StateId,Ltl,Type,MaxSteps,OpTripleResultTrace, Result) :-
2377		(MaxSteps =< 0
2378		-> add_error(find_trace,'Number of maximum animation steps should be a positive integer. The number of steps which was given is ',MaxSteps)
2379		; true),
2380		set_current_state(StateId), !, % can be backtracked
2381		% negate -> counterexample is the trace we are looking for
2382		preprocess_formula(Ltl,Ltl2),
2383		find_trace_aux(StateId,not(Ltl2),Type,0,MaxSteps,ResultTrace,ResultTrace,Names,Result),
2384		gen_op_triples(ResultTrace,Names,OpTripleResultTrace).
2385		%(gen_op_triples(ResultTrace,OpTripleResultTrace) -> print(ok(OpTripleResultTrace,result(Result))),nl
2386		% ; add_error_and_fail(prob2_interface,'trace not correctly generated',ResultTrace)).
2387
2388		find_trace_aux(CurID,Condition,Type,_N,_Max,StateTransitionHistory,[],[],RESULT) :-
2389		debug_println(9,checking_ltl_formula(CurID,StateTransitionHistory)),
2390		evaluate_ltl_formula(Condition,StateTransitionHistory,Type,ltl:check_ap,ltl:callback_tp,EvResult),
2391		EvResult = false,
2392		!,
2393		RESULT=ltl_found.
2394		find_trace_aux(CurID,Condition,Type,N,Max,StateTransitionHistory,STTail,Names,RESULT) :-
2395		user:tcltk_compute_options(CurID,ActionsAndIDs),
2396		debug_println(9,opts(ActionsAndIDs)),
2397		( N=Max
2398		-> debug_println(9,'Maximum number of animation steps reached.'),
2399		Names = [],
2400		RESULT = maximum_nr_of_steps_reached
2401		; pick_action(random,ActionsAndIDs,ActionId,Name,DstID) % pick first one; we could do random
2402		-> debug_println(9,performing_action(ActionId,from_to(CurID,DstID),opts(ActionsAndIDs))),
2403		STTail = [strans(CurID,ActionId)|STTail2],
2404		Names = [Name|Names2],
2405		N1 is N+1,
2406		find_trace_aux(DstID,Condition,Type,N1,Max,StateTransitionHistory,STTail2,Names2,RESULT)
2407		; otherwise
2408		-> STTail=[], Names = [], RESULT = deadlock
2409		).
2410
2411		gen_op_triples([],[],[]).
2412		gen_op_triples([_X],[_Y],[]).
2413		gen_op_triples([strans(CurID,ActionId),strans(DstID,ActId)|T],[Name|NameT],[op(ActionId,Name,CurID,DstID)|Rest]) :-
2414		gen_op_triples([strans(DstID,ActId)|T],NameT,Rest).
2415
2416		:- use_module(library(random)).
2417		:- use_module(library(lists)).
2418		pick_action(first,[(ActionId,Term,DstID)|_], ActionId, Name, DstID) :- extract_op_name(Term,Name).
2419		pick_action(random,Options,ActionId, Name, DstID) :-
2420		length(Options,Len),
2421		L1 is Len+1,
2422		random(1,L1,RanChoice),
2423		debug_println(9,random(RanChoice,Len)),
2424		nth1(RanChoice,Options,(ActionId,ActionAsTerm,DstID)),
2425		extract_op_name(ActionAsTerm,Name).
2426
2427
2428		% -------------------------------------
2429
2430		% an execution engine with minimal overhead: states are not stored in visited_expression database, only first enabled operation is taken
2431		:- mode execute_model(+CurStateID,+MaxNrSteps,-TransitionInfo,-ExecutedSteps,-Result).
2432		execute_model(CurStateID,MaxNrSteps,TransitionInfo,ExecutedSteps,Result) :-
2433		execute_model(CurStateID,MaxNrSteps,[],TransitionInfo,ExecutedSteps,Result).
2434
2435		:- mode execute_model(+CurStateID,+MaxNrSteps,+Options,-TransitionInfo,-ExecutedSteps,-Result).
2436		% Options can contain continue_after_errors, timeout(MS)
2437		% Result is either maximum_nr_of_steps_reached, deadlock, error, internal_error, time_out
2438		execute_model(CurStateID,MaxNrSteps,Options,TransitionInfo,ExecutedSteps,Result) :-
2439		visited_expression(CurStateID,CurState),
2440		% we could do something like prepare_state_for_specfile_trans(CurState,CurState2) + ensure that the individual steps do not repack constants
2441		execute_model_steps(0,CurState,MaxNrSteps,Options,NewState,ExecutedSteps,Result),
2442		(ExecutedSteps>0
2443		-> user:tcltk_add_new_transition_transid(CurStateID,'$JUMP'('EXECUTE'(ExecutedSteps)),ToID,NewState,[],TransId),
2444		debug_println(4,added_transition_for_execute(ExecutedSteps,ToID)),
2445		user:tcltk_goto_state('$JUMP'('EXECUTE'(ExecutedSteps)),ToID),
2446		TransitionInfo = op(TransId,'EXECUTE',CurStateID,ToID)
2447		; TransitionInfo = none).
2448
2449		execute_model_steps(StepNr,CurState,MaxNrSteps,_Options,NewState,ExecutedSteps,Result) :-
2450		StepNr >= MaxNrSteps,!,
2451		NewState=CurState,
2452		ExecutedSteps=StepNr, Result=maximum_nr_of_steps_reached.
2453		execute_model_steps(StepNr,CurState,MaxNrSteps,Options,NewState,ExecutedSteps,Result) :-
2454		cli_trans_aux(StepNr,CurState,Options,ActionName,_Act,State2,ErrorRes),
2455		!,
2456		debug_println(20,execute(StepNr,ActionName)),
2457		%print(step(StepNr,Act,State2)),nl,
2458		S1 is StepNr+1,
2459		(nonvar(ErrorRes) -> Result=ErrorRes, ExecutedSteps=StepNr, NewState=CurState
2460		; execute_model_steps(S1,State2,MaxNrSteps,Options,NewState,ExecutedSteps,Result)).
2461		execute_model_steps(Steps,CurState,_,_Options,CurState,Steps,deadlock).
2462
2463		:- use_module(specfile,[specfile_trans_or_partial_trans/6]).
2464		:- use_module(error_manager,[throw_enumeration_warnings_in_current_scope/0, add_internal_error/2, error_occurred_in_error_scope/0]).
2465		:- use_module(tools_meta,[safe_time_out/3]).
2466
2467		cli_trans_aux(StepNr,CurState,Options,ActionName,Act,NewState,ErrorRes) :-
2468		catch_enumeration_warning_exceptions(
2469		(throw_enumeration_warnings_in_current_scope,
2470		(member(timeout(MS),Options) ->
2471		safe_time_out(specfile_trans_or_partial_trans(CurState,ActionName,Act,NewState,_TransInfo,Residue),MS,TR)
2472		; specfile_trans_or_partial_trans(CurState,ActionName,Act,NewState,_TransInfo,Residue) % no time-out !
2473		),
2474		(TR==time_out
2475		-> add_error(execute,'Timeout occured during execute after step: ',StepNr),ErrorRes=time_out
2476		; error_occurred_in_error_scope ->
2477		(member(continue_after_errors,Options) -> true
2478		; add_error(execute,'Error occured during execute after step: ',StepNr),ErrorRes=error)
2479		; true)
2480		),
2481		(add_error(virtual_time_out_execute,'Virtual TIME-OUT occured during execute after step: ',StepNr),
2482		ActionName = '*** VIRTUAL_TIME_OUT ***', Act=ActionName,
2483		ErrorRes=time_out)
2484		),
2485		(Residue=[] -> true
2486		; add_internal_error('Residue during execute after step: ',StepNr:Residue),
2487		(nonvar(ErrorRes) -> true ; ErrorRes=internal_error)).
2488
2489		% -------------------------------------
2490
2491		get_unsat_core_with_fixed_conjuncts(Pred,FixedPreds,CoreOut) :-
2492		typecheck_pred_for_unsat_core(Pred,TypedPred),
2493		maplist(typecheck_pred_for_unsat_core,FixedPreds,TypedFixedPreds),
2494		conjunct_predicates(TypedFixedPreds,Conj),
2495		unsat_core_with_fixed_conjuncts(TypedPred,Conj,Core),
2496		translate_bexpression(Core,CoreOut).
2497
2498		get_minimum_unsat_core_with_fixed_conjuncts(Pred,FixedPreds,CoreOut) :-
2499		typecheck_pred_for_unsat_core(Pred,TypedPred),
2500		maplist(typecheck_pred_for_unsat_core,FixedPreds,TypedFixedPreds),
2501		conjunct_predicates(TypedFixedPreds,Conj),
2502		minimum_unsat_core_with_fixed_conjuncts(TypedPred,Conj,Core),
2503		translate_bexpression(Core,CoreOut).
2504
2505		typecheck_pred_for_unsat_core(PIn,POut) :-
2506		evaluate_formula_typecheck('#PREDICATE',PIn,POutT,[]),
2507		get_texpr_expr(POutT,exists(_,POut)).
2508
2509		/**
2510		Access information about the current version of the ProB core.
2511
2512		#### called by:
2513		* ProB 2.0: GetInternalRepresentationPrettyPrintCommand
2514		*/
2515		:- use_module(specfile,[get_internal_representation/1]).
2516		get_pretty_print(PP) :-
2517		get_internal_representation(PPC),
2518		atom_codes(PP,PPC).
2519
2520		:- use_module(symbolic_model_checker(predicate_handling)).
2521		get_primed_predicate(Pred,PrimedPredOut) :-
2522		evaluate_formula_typecheck('#PREDICATE',Pred,POutT,[]),
2523		prime_predicate(POutT,PrimedPred),
2524		translate_bexpression(PrimedPred,PrimedPredOut).
2525
2526		:- use_module(weakest_preconditions).
2527		:- use_module(preferences, [call_with_preference/3]).
2528		get_weakest_precondition(OpName,Pred,WPOut) :- % TODO: call with preference can be removed once ProB 2 reads ASTs instead of reparsing
2529		call_with_preference(get_weakest_precondition_aux(OpName,Pred,WPOut),translate_ids_to_parseable_format,true).
2530		get_weakest_precondition_aux(OpName,Pred,WPOut) :-
2531		b_get_machine_operation(OpName,_Results,_Parameters,OpBody),
2532		evaluate_formula_typecheck('#PREDICATE',Pred,POutT,[]),
2533		weakest_precondition(OpBody,POutT,WP),
2534		translate_bexpression(WP,WPOut).
2535
2536		:- use_module(before_after_predicates,[before_after_predicate_for_operation/2]).
2537		before_after_predicate(OpName,PredicateOut) :-
2538		call_with_preference(before_after_predicate_aux(OpName,PredicateOut),translate_ids_to_parseable_format,true).
2539		before_after_predicate_aux(OpName,PredicateOut) :-
2540		before_after_predicate_for_operation(OpName,Predicate),
2541		translate_bexpression(Predicate,PredicateOut).
2542
2543		/** Synthesis Commands:
2544		*
2545		#### b_synthesis:start_synthesis_from_ui/13 called by:
2546		* ProB 2.0: BSynthesisCommand
2547		*/
2548		start_synthesis_from_ui_(SynthesisMode,AdaptMachineCode,SolverTimeOut,Library,DoNotUseConstants,Solver,ConsiderIfVarNames,Operation,SynthesisType,Positive,Negative,NewMachineAtom,Distinguishing) :-
2549		start_synthesis_from_ui(SynthesisMode,AdaptMachineCode,SolverTimeOut,Library,DoNotUseConstants,Solver,ConsiderIfVarNames,Operation,SynthesisType,Positive,Negative,NewMachineAtom,Distinguishing).
2550
2551		/*
2552		#### b_synthesis:start_synthesis_single_operation_from_ui/11 called by:
2553		* BSynthesis: StartSynthesisCommand
2554		*/
2555		start_synthesis_single_operation_from_ui_(SolverTimeOut,Operations,Library,DoNotUseConstants,Solver,Operation,action,Positive,Negative,CacheOperationTuple,Distinguishing) :-
2556		start_synthesis_single_operation_from_ui(SolverTimeOut,Operations,Library,DoNotUseConstants,Solver,Operation,action,Positive,Negative,CacheOperationTuple,Distinguishing).
2557
2558		/*
2559		#### b_synthesis:reset_synthesis_context/0 called by:
2560		* ProB 2.0: ResetBSynthesisCommand
2561		*/
2562		reset_synthesis_context_ :- reset_synthesis_context.
2563
2564		/*
2565		#### synthesis_util:get_invariant_violating_vars_from_examples/3 called by:
2566		* BSynthesis: GetViolatingVarsFromExamples
2567		*/
2568		get_invariant_violating_vars_from_examples_(Positive,Negative,ViolatingVarNames) :-
2569		get_invariant_violating_vars_from_examples(Positive,Negative,ViolatingVarNames).
2570
2571		/*
2572		#### synthesis_util:get_valid_and_invalid_equality_predicates_for_operation/6 called by:
2573		* BSynthesis: VisualizeOperationCommand
2574		*/
2575		get_valid_and_invalid_equality_predicates_for_operation_(OperationName,ValidAmount,InvalidAmount,ValidPrettyEqualityTuples,InvalidPrettyEqualities,IgnoredIDs) :-
2576		get_valid_and_invalid_equality_predicates_for_operation(OperationName,ValidAmount,InvalidAmount,ValidPrettyEqualityTuples,InvalidPrettyEqualities,IgnoredIDs).
2577
2578		/*
2579		#### synthesis_util:get_valid_and_invalid_equality_predicates_for_invariants/4 called by:
2580		* BSynthesis: VisualizeInvariantsCommand
2581		*/
2582		get_valid_and_invalid_equality_predicates_for_invariants_(ValidAmount,InvalidAmount,ValidPrettyEqualities,InvalidPrettyEqualities) :-
2583		get_valid_and_invalid_equality_predicates_for_invariants(ValidAmount,InvalidAmount,ValidPrettyEqualities,InvalidPrettyEqualities).
2584
2585		/*
2586		#### synthesis_util:adapt_machine_code_for_operations/2 called by:
2587		* BSynthesis: AdaptMachineCodeForOperationsCommand
2588		*/
2589		adapt_machine_code_for_operations_(Operations,NewMachineAtom) :-
2590		adapt_machine_code_for_operations(Operations,NewMachineAtom).
2591
2592		/*
2593		#### predicate_data_generator:generate_synthesis_data_from_predicate_/5 called by:
2594		* BSynthesisDataGenerator: SynthesisDataFromPredicateCommand
2595		*/
2596		generate_synthesis_data_from_predicate_(MachinePath, AugmentRecords, SolverTimeoutMs, RawPredicate, AugmentedSetOfData) :-
2597		generate_synthesis_data_from_predicate(MachinePath, AugmentRecords, SolverTimeoutMs, RawPredicate, AugmentedSetOfData).
2598
2599		/*
2600		#### called by:
2601		* ProB 2.0: GetMachineOperationNamesCommand
2602		*/
2603		:- use_module(probcspsrc(haskell_csp),[channel/2]).
2604
2605		csp_channel_or_start('start_cspm_MAIN').
2606		csp_channel_or_start('start_cspm'). % TO DO: do we also need to support print channel ?
2607		csp_channel_or_start(Name) :- channel(Name,_).
2608
2609		get_machine_operation_names(MachineOperationNames) :- b_mode,!,
2610		findall(MachineOperationName,b_is_operation_name(MachineOperationName),MachineOperationNames).
2611		get_machine_operation_names(ChannelNames) :- csp_mode,!,
2612		findall(Name, csp_channel_or_start(Name),ChannelNames).
2613		get_machine_operation_names([]).
2614
2615		:- use_module(probsrc(bsyntaxtree), [get_texpr_id/2]).
2616		:- use_module(probsrc(bmachine),[b_get_operation_non_det_modifies/2, b_get_operation_normalized_read_write_info/3]).
2617		% get list of operation info terms of the form
2618		% operation_info(Name,ResultNames,ParameterNames,TopLevel,OType)
2619		% where ResultNames and ParameterNames are list of atomic names
2620		% TopeLevel is true if the operation is a top-level operation for animation/model checking
2621		% OType is classic, csp or eventb_operation %was eventb_operation(ChangeSet,ParaValues,Operation)
2622		get_machine_operation_infos(MachineOperationInfos) :- b_mode,!,
2623		% TODO: ensure that we do not need to consider preference(show_eventb_any_arguments,EVENTB)
2624		% TODO: examine what happens for CSP||B
2625		findall(operation_info(Name,ResultNames,ParameterNames,TopLevel,OTypeF,Read,Modified,NonDetModifies),
2626		(b_get_machine_operation(Name,Results,RealParameters,_RealBody,OType,_OpPos),
2627		maplist(get_texpr_id,Results,ResultNames),
2628		maplist(get_texpr_id,RealParameters,ParameterNames),
2629		functor(OType,OTypeF,_),
2630		% TO DO: obtain machine file or machine name
2631		(b_top_level_operation(Name) -> TopLevel = true ; TopLevel=false),
2632		(b_get_operation_normalized_read_write_info(Name,OpRead,Modified)
2633		-> exclude(op_id,OpRead,Read)
2634		% exclude query operations called in expressions (allow_operation_calls_in_expr);
2635		%ProB2 Java cannot deal with it and raises exception for non-atomic identifiers
2636		; (Read,Modified)=(unknown,unknown)),
2637		(b_get_operation_non_det_modifies(Name,NonDetModifies) -> true ; NonDetModifies=unknown)
2638		),
2639		MachineOperationInfos).
2640		get_machine_operation_infos(ChannelInfos) :- csp_mode,!,
2641		findall(operation_info(Name,[],[],true,csp,[],[],[]), csp_channel_or_start(Name),ChannelInfos).
2642		get_machine_operation_infos([]).
2643
2644		op_id(op(_)).
2645
2646		:- use_module(b_global_sets,[b_global_set/1, is_b_global_constant/3]).
2647		:- use_module(bmachine,[b_get_machine_constants/1,b_get_machine_variables/1,b_get_definition/5,b_filenumber/4]).
2648
2649		:- mode get_machine_identifiers(+Category, -ListOfIdentifiers).
2650		get_machine_identifiers(machines,MN) :-
2651		findall(FID, (b_filenumber(FID,Type,_,_),Type \= def),MN).
2652		get_machine_identifiers(definition_files,DFN) :-
2653		findall(FID, b_filenumber(FID,def,_,_),DFN).
2654		get_machine_identifiers(definitions,DN) :-
2655		findall(DefID,b_get_definition(DefID,_,_,_,_),DN).
2656		get_machine_identifiers(sets,Sets) :-
2657		findall(GS,b_global_set(GS),Sets).
2658		get_machine_identifiers(set_constants,Csts) :-
2659		findall(Cst,is_b_global_constant(_GS,_,Cst),Csts).
2660		get_machine_identifiers(constants,CN) :-
2661		b_get_machine_constants(Constants),
2662		get_texpr_ids(Constants,CN).
2663		get_machine_identifiers(variables,VN) :-
2664		b_get_machine_variables(Variables),
2665		get_texpr_ids(Variables,VN).
2666		get_machine_identifiers(operations,Ops) :-
2667		findall(Op,b_top_level_operation(Op),Ops).
2668
2669		get_all_machine_identifiers(SortedAllIDs) :-
2670		findall(ID,get_machine_identifiers(_,ID),LIds), append(LIds,AllIDs),
2671		sort(AllIDs,SortedAllIDs).
2672
2673		% get a list of all machine files: TO DO: extend for CSP, ...
2674		get_machine_files(Files) :-
2675		findall(b_file(Name,Extension,Filename),b_filenumber(Name,Extension,_,Filename), Files).
2676
2677		% a predicate to obtain possible identifier completions for current machine:
2678		:- use_module(tools_matching,[fuzzy_match_codes_lower_case/2, codes_to_lower_case/2, get_current_keywords/1]).
2679		get_possible_completions(ID,Options,Completions) :-
2680		get_match_ids(Options,SortedAllIDs),
2681		atom_codes(ID,IDCodes0),
2682		(member(lower_case,Options) -> codes_to_lower_case(IDCodes0,IDCodes), Opt=lower_case
2683		; Opt=case_sensitive, IDCodes = IDCodes0),
2684		findall(Target,(member(Target,SortedAllIDs),atom_codes(Target,TargetCodes),
2685		match(Opt,IDCodes,TargetCodes)),Completions).
2686
2687		match(case_sensitive,Pattern,TargetCodes) :- !, prefix(TargetCodes,Pattern).
2688		match(lower_case,Pattern,TargetCodes) :- codes_to_lower_case(TargetCodes,TC2), prefix(TC2,Pattern).
2689
2690		get_possible_fuzzy_matches(ID,FuzzyMatches) :-
2691		get_match_ids([keywords],SortedAllIDs),
2692		atom_codes(ID,IDCodes),
2693		findall(Target,(member(Target,SortedAllIDs),atom_codes(Target,TargetCodes),
2694		fuzzy_match_codes_lower_case(IDCodes,TargetCodes)),FuzzyMatches).
2695
2696		:- use_module(library(ordsets),[ord_union/3]).
2697		get_match_ids(Options,Ids) :- member(keywords,Options),!,
2698		get_all_machine_identifiers(SortedAllIDs),
2699		get_current_keywords(Keywords),
2700		ord_union(SortedAllIDs,Keywords,Ids).
2701		get_match_ids(_,SortedAllIDs) :- get_all_machine_identifiers(SortedAllIDs).
2702		% -----------------------
2703
2704		% preliminary predicate for obtaining values as raw Prolog terms
2705		% sample call: prob2_interface:evaluate_expression_prolog(0,boolean_true(pos(13,1,6,5,6,7)),R).
2706		evaluate_expression_prolog(StateId,RawAST,NValuePrologTerm) :-
2707		evaluate_expression_prolog(StateId,RawAST,_,NValuePrologTerm).
2708		evaluate_expression_prolog(StateId,RawAST,TypedAST,NValuePrologTerm) :-
2709		get_eval_scope(Scope),
2710		b_type_expression(RawAST,Scope,_Type,TypedAST,Errors),
2711		Errors=[],
2712		get_state(StateId, State),
2713		evaluate_expression(State,TypedAST,force,_SRes,NValuePrologTerm).