1		% (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		% tcltk_interface.pl
6		:- module(tcltk_interface,[
7		tcltk_goto_state/2,
8		tcltk_add_new_transition_transid/6,
9		tcltk_add_new_transition/5,
10		tcltk_get_options/1, tcltk_get_options_dest_info/1, tcltk_get_state/1, tcltk_get_state/2,
11		tcltk_get_options_or_candidates/1, tcltk_get_options_candidate_nr_name/2,
12		tcltk_get_options_nr_description/2,
13
14		tcltk_get_state_errors/1, tcltk_get_detailed_state_error/6,
15		tcltk_open_state_error_in_editor/1,
16		tcltk_get_line_col/5,
17		tcltk_current_state_invariant_violated/0,
18		tcltk_get_status/3,
19		tcltk_get_ops_with_virtual_timeout/1,
20		tcltk_get_ops_with_real_timeout/1,
21		tcltk_get_ops_user_interrupt_occurred/0,
22
23		tcltk_compute_options/2,
24		can_generate_dot_from_last_state_error/0,
25		tcltk_initialise/0, tcltk_reset/0,
26
27		tcltk_perform_nr/1, tcltk_random_perform/0, tcltk_random_perform/1,
28		tcltk_perform_nr_option/3,
29		tcltk_perform_action_term/2,
30		tcltk_is_sync_event/1,
31
32		tcltk_exists_an_open_node/0, tcltk_goto_an_open_node/0,
33		tcltk_goto_max_reached_node/0, tcltk_goto_timeout_node/0,
34		tcltk_state_exists_with_invariant_violated/0,
35		tcltk_goto_an_invariant_violation/0, tcltk_goto_node_with_id/1,
36		tcltk_current_node_has_no_real_transition/0, tcltk_current_node_has_real_transition/0,
37		tcltk_current_node_has_partial_transition/0,
38		tcltk_goto_a_non_deterministic_node/1, tcltk_goto_a_non_deterministic_output_node/1,
39		tcltk_goto_a_branching_node/0, tcltk_goto_a_non_resetable_node/0,
40		tcltk_state_space_only_has_root_node/0, tcltk_no_constants_or_no_inititalisation_found/0,
41		tcltk_goto_event_list_property_violation/3, tcltk_goto_state_enabling_operation/2,
42		tcltk_find_max_reached_node/0, tcltk_find_max_reached_node/1,
43		tcltk_search_among_existing_nodes/6,
44		find_invariant_violation_among_not_checked_nodes/1,
45
46		tcltk_model_check/12, do_model_check/13,
47		tcltk_set_dbf_mode/1, tcltk_dbf_modes/1,
48		tcltk_mark_current_node_to_be_recomputed_wo_timeout/0,
49		tcltk_mark_current_node_to_be_recomputed_with_random_enum/0,
50		tcltk_finish_current_node_to_be_recomputed_with_random_enum/0,
51		tcltk_hash_model_checking_imprecise/0,
52		tcltk_clear_state_space_and_refocus_to_current_state/0,
53
54		tcltk_constraint_based_check/1,
55		tcltk_constraint_based_check_op/2, tcltk_constraint_based_check_op/3,
56		tcltk_constraint_based_check/2, tcltk_constraint_based_check_with_timeout/2,
57		tcltk_cbc_find_trace/2, tcltk_cbc_find_trace/4,
58		tcltk_cbc_refinement_check/2,
59		tcltk_constraint_find_valid_state/0,
60		tcltk_constraint_find_maximal_valid_state/0,
61		tcltk_constraint_find_dynamic_assertion_violation/0,
62		tcltk_constraint_find_valid_state_with_pred/3,
63		tcltk_constraint_find_deadlock_state/1,
64		tcltk_constraint_find_deadlock_state_with_goal/2,
65		tcltk_constraint_find_deadlock_state_with_goal/3,
66		tcltk_constraint_find_static_assertion_violation/1,
67		tcltk_check_if_feasible_operation/4,
68		cbc_constraint_find_static_assertion_violation/2,
69
70		tcltk_can_backtrack/0, tcltk_can_backtrack/1,
71		tcltk_can_forward/0, tcltk_can_forward/1,
72		tcltk_prepare_for_reload/0,
73		tcltk_backtrack/0, tcltk_backtrack/1, tcltk_fast_forward/0, tcltk_forward/0,
74		tcltk_execute_trace_to_current_node/0, tcltk_find_shortest_trace_to_current_node/1,
75		tcltk_execute_longest_trace_from/1,
76		tcltk_get_history/1,
77		tcltk_perform_action_string/3,
78		tcltk_perform_action/2,
79		tcltk_perform_action/4,
80
81		tcltk_open_xtl_file/1,
82		tcltk_open_z_file/1, tcltk_open_z_tex_file/1,
83		tcltk_open_alloy_file/1, tcltk_open_alloy_prolog_ast_file/1,
84		tcltk_open_cspm_file/1,
85		tcltk_add_csp_file/1,
86		tcltk_load_packaged_eventb_file/1,
87
88		tcltk_verify_alloy_cmd/4,
89		tcltk_get_alloy_cmd_names/1,
90		tcltk_load_alloy_cmd_in_current_translation/1,
91
92		tcltk_machine_has_assertions/0,
93		tcltk_unique_top_level_operation/1, tcltk_top_level_operations/1,
94
95		compute_all_transitions_if_necessary/0,
96		compute_all_transitions_if_necessary/2,
97		compute_state_information_if_necessary/0, % compute transitions and invariant
98		compute_invariant_if_necessary/3,
99		check_invariantKO/2,
100		check_invariantKO/3,
101		catch_clpfd_overflow_call_for_state/4,
102		compute_ample_set/3,
103		compute_all_transitions/2,
104		add_transition/4,
105		add_trans_id/5,
106
107		tcltk_has_eventtrace/1, tcltk_show_eventtrace/2,
108		tcltk_execute_model/3,
109		tcltk_execute_trace_to_node/1,
110		find_shortest_trace_to_node/4,
111
112		tcltk_explore_csp_process/2, tcltk_visualize_csp_process/2,
113		get_csp_process_id/2, get_csp_process_stats/1,
114
115		tcltk_add_user_executed_operation/2, tcltk_add_user_executed_operation/3,
116		tcltk_add_user_executed_operation_typed/4, tcltk_add_user_executed_operation_typed/6,
117		tcltk_add_user_executed_statement/3,
118		tcltk_add_user_modify_variable_transition/2, tcltk_add_user_modify_variable_transition/4,
119
120		tcltk_analyse_option/2,
121		tcltk_analyse/6,
122		tcltk_show_typing_of_variables_and_constants/1,
123		tcltk_show_current_state/1,
124		tcltk_eval/4, interruptable_tcltk_eval/4,
125		tcltk_eval_as_table/2,
126		tcltk_find_value_as_table/3, find_value_in_cur_state/4,
127		tcltk_time_call/1, eval_elapsed_time/1,
128		tcltk_check_csp_assertions/2, tcltk_check_csp_assertion/4, tcltk_check_csp_assertion/5,
129		checkAssertion/5,
130		tcltk_get_vacuous_guards/1,
131		tcltk_get_vacuous_invariants/1, tcltk_get_vacuous_invariants_table/1,
132		tcltk_operations_covered_info/3, operation_name_covered/1,
133		tcltk_show_expression_as_dot/2,
134		generate_dot_from_formula/2,
135		generate_dot_from_invariant/1, generate_dot_from_properties/1, generate_dot_from_assertions/1,
136		generate_dot_from_deadlock_po/1, generate_dot_from_goal/1, generate_dot_from_last_span_predicate/1,
137		generate_dot_from_operation/2, generate_dot_from_operation_with_params/4,
138		write_dot_file_for_pred_expr/2,
139		write_dot_file_for_value_as_tree/2,
140		evaluate_expression_over_history_to_csv_file/2, tcltk_evaluate_expression_over_history/2,
141		translate_error_for_tclk/2,
142		tcltk_set_initial_machine/0, tcltk_clear_machine/0,
143		% set_tcltk_cspm_mode/0, unset_tcltk_cspm_mode/0,
144		tcltk_open_b_file/1, tcltk_open_b_file_for_minor_mode/2,
145		tcltk_run_ltsmin/5,
146		tcltk_save_history_as_trace_file/1,
147		tcltk_execute_until/1,
148
149		tcltk_bv_get_tops/1,
150		tcltk_bv_get_structure/3,
151		tcltk_bv_is_leaf/2,
152		tcltk_bv_get_values/3,
153		tcltk_bv_get_value/3,
154		tcltk_bv_show_formula_as_dot_tree/2,
155		tcltk_bv_show_formula_as_dot_graph/2,
156		tcltk_bv_show_value_as_dot_tree/2,
157		tcltk_bv_get_pp_formula_string/2,
158		tcltk_show_identifier_value_as_dot_tree/2, % a version of the above independent of bvisual
159		tcltk_bv_get_unlimited_value/3, tcltk_bv_get_unlimited_value_atom/2,
160
161		tcltk_get_constants_predicate/2,
162
163		get_cbc_data_base_id_checks/1, get_cbc_data_base_text_checks/1,
164
165		tcltk_write_uml_sequence_chart/1,
166
167		get_ltl_formulas_from_file/2,
168		tcltk_mcts_auto_play/0, tcltk_mcts_auto_play/1, mcts_auto_play_available/0,
169		tcltk_simplify_predicate/2 % not used
170
171		]).
172
173
174		:- meta_predicate call_pred_on_expanded_state(3,-,-,-).
175		:- meta_predicate map_over_history(3,-).
176		:- meta_predicate tcltk_time_call(0).
177		:- meta_predicate catch_clpfd_overflow_call_for_state(-,-,0,0).
178		:- meta_predicate add_csp_process_id1(-,-,1).
179
180		%prob_use_module(X) :- load_files(X,[if(changed),load_type(source),compilation_mode(compile)]).
181
182		/* load all necessary modules */
183		:- use_module(library(random)).
184		:- use_module(library(lists)).
185
186		:- use_module(library(ordsets)).
187		:- use_module(library(avl)).
188
189		:- use_module(module_information).
190		:- module_info(group,tcltk).
191		:- module_info(description,'Interface between the Tcl/Tk GUI, the CLI and the internal modules.').
192
193		:- use_module(typechecker).
194		:- use_module(self_check).
195		:- use_module(probsrc(preferences)).
196		:- use_module(probsrc(debug)).
197		:- use_module(error_manager).
198		:- use_module(kernel_waitflags).
199		:- use_module(probsrc(tools)).
200		:- use_module(probsrc(specfile)).
201		:- use_module(probsrc(state_space_exploration_modes)).
202		:- use_module(probsrc(translate)).
203		:- use_module(probsrc(b_state_model_check)).
204		:- use_module(probsrc(bmachine)).
205		:- use_module(probsrc(b_interpreter)).
206		:- use_module(probsrc(b_trace_checking)).
207		:- use_module(probsrc(bsyntaxtree)).
208		:- use_module(kernel_objects).
209		:- use_module(probsrc(state_space)).
210		:- use_module(extension('plspec/plspec/plspec_core'),[set_error_handler/1]).
211		:- use_module(extension('plspec/plspec/prettyprinter'),[pretty_print_error/1]).
212		prob_plspec_error_handler(ErrTerm) :- pretty_print_error(ErrTerm),
213		add_internal_error('Error detected by plspec',ErrTerm).
214		:- set_error_handler(tcltk_interface:prob_plspec_error_handler).
215		:- use_module(model_checker).
216		:- use_module(dotsrc(visualize_graph)).
217		:- use_module(dotsrc(state_space_reduction)).
218		:- use_module(dotsrc(state_custom_dot_graph)).
219		:- use_module(succeed_max).
220		%:- use_module(testcase_generator).
221		:- use_module(prozsrc(proz),[open_proz_file/2]).
222		:- use_module(dotsrc(reduce_graph_state_space)).
223		:- use_module(b_read_write_info).
224		%:- use_module(flow).
225		:- use_module(probltlsrc(ltl),[parse_and_preprocess_formula/3, parse_ltlfile/2,
226		pp_ltl_formula/2, ltl_model_check_with_ce1/5,
227		is_fairness_implication/1, tcltk_play_ltl_counterexample/2]).
228		:- use_module(probltlsrc(ctl),[ctl_model_check_with_ce/6, tcltk_play_ctl_counterexample/2]).
229		%:- use_module('promela/promela_ncprinter').
230		:- use_module(extrasrc(bvisual2),[bv_get_top_level/1, bv_expand_formula/3, bv_get_values/3, bv_get_btvalue/4,
231		bv_get_stored_formula_expr/2, bv_is_explanation_node/1, bv_get_value_unlimited/3]).
232		:- use_module(b_show_history).
233		:- use_module(probcspsrc(haskell_csp),[parse_single_csp_declaration/3]).
234		%:- use_module(probcspsrc(slicer_csp),[slice_from_program_point/14]).
235		:- use_module(value_persistance, [save_constants/1,add_new_transitions_to_cache/1]).
236		:- use_module(cbcsrc(cbc_path_solver),[create_testcase_path_nondet/4,verify_alloy_command/5]).
237		:- use_module(dotsrc(uml_generator),[write_uml_sequence_chart/1]).
238
239		/* main program
240		* ============
241		*/
242
243
244		/*
245		Start server for LTSmin
246		*/
247
248		:- use_module(extension('ltsmin/ltsmin'),[start_ltsmin/4]).
249
250
251		% Backend = symbolic or sequential
252		tcltk_run_ltsmin(Backend,NoDead,NoInv,UsePOR,Res) :-
253		% in case of POR we can also enable/disable use_cbc_analysis preference
254		(UsePOR == true -> MoreFlags = [por] ; MoreFlags=[]),
255		start_ltsmin(Backend, [NoDead, NoInv], MoreFlags,Result),
256		get_check_name(NoDead,NoInv,Kind),
257		process_ltsmin_result(Result,Kind,Res).
258
259		get_check_name(true,false,Kind) :- Kind = 'INVARIANT'.
260		get_check_name(false,true,Kind) :- Kind = 'DEADLOCK'.
261
262		:- use_module(tools_printing,[format_with_colour_nl/4]).
263		:- use_module(extension('ltsmin/ltsmin_trace'),[csv_to_trace/3]).
264		process_ltsmin_result(ltsmin_model_checking_ok,Kind,no_counter_example_found) :-
265		format_with_colour_nl(user_output,green,'LTSMin found no ~w Counter Example',Kind).
266		process_ltsmin_result(ltsmin_counter_example_found(CsvFile),Kind,counter_example_found) :-
267		format_with_colour_nl(user_output,[red,bold],'LTSMin found ~w Counter Example',Kind),
268		csv_to_trace(CsvFile,States,Transitions),
269		print('*** REPLAYING TRACE: '),nl,print(Transitions),nl,
270		%print(States),nl,
271		length(Transitions,TLen), length(States,SLen), print(len(TLen,SLen)),nl,
272		(replay_ltsmin_trace(States,Transitions) -> true
273		; add_error(process_ltsmin_result,'Could not replay trace:',Transitions)).
274
275		replay_ltsmin_trace([],[]).
276		replay_ltsmin_trace([State|TS],[TransName|TT]) :-
277		(find_successor_state(State,TransName)
278		-> replay_ltsmin_trace(TS,TT)
279		; add_error(replay_ltsmin_trace,'Could not execute:',TransName),fail).
280
281		:- use_module(state_space,[visited_expression/2]).
282		find_successor_state(EState,'$init_state') :- !,
283		compute_all_inits,
284		is_initial_state_id(NewID),
285		state_space:visited_expression(NewID,State),
286		%print(try_init(NewID,State)),nl, print(EState),nl,
287		expand_const_and_vars_to_full_store(State,EState1),
288		%print(EState1),nl,
289		EState1=EState,
290		tcltk_reset,
291		tcltk_execute_trace_to_node(NewID).
292		find_successor_state(EState,TransName) :-
293		tcltk_get_options(_),
294		current_options(Options), % print(Options),nl,
295		member( (_,_Action,ActionOpAsTerm,NewID), Options),
296		get_operation_name(ActionOpAsTerm,TransName),
297		visited_expression(NewID,State),
298		expand_const_and_vars_to_full_store(State,EState), % TO DO: only compare variables
299		tcltk_goto_state(ActionOpAsTerm,NewID).
300
301		% compute all INITIALISATIONS
302		compute_all_inits :- is_concrete_constants_state_id(ID), compute_all_transitions_if_necessary(ID),fail.
303		compute_all_inits.
304
305		/* -------------------------------------------------------------------- */
306
307		%tcltk_find_untyped_vars(Vs) :- find_untyped_vars(Vs), Vs \== [].
308
309		%tcltk_find_untyped_consts(Vs) :- find_untyped_consts(Vs), Vs \== [].
310
311
312		tcltk_find_max_reached_node :- tcltk_find_max_reached_node(_).
313		tcltk_find_max_reached_node(ID) :- max_reached_or_timeout_for_node(ID).
314
315
316		tcltk_current_node_has_no_real_transition :-
317		\+ tcltk_current_node_has_real_transition.
318		tcltk_current_node_has_real_transition :-
319		current_state_id(CurID),
320		transition(CurID,Trans,_),
321		(CurID \= root -> true
322		; Trans = '$partial_setup_constants'
323		-> properties_were_filtered(Nr), Nr>0 % we probably have the partial transition due to prob-ignore pragmas
324		% TODO: detect whether any of the other non-ignored conjuncts were false/unknown
325		; true),!.
326		tcltk_current_node_has_partial_transition :-
327		current_state_id(CurID),
328		transition(CurID,'$partial_setup_constants',_),!.
329
330		/* --------------------------------------------------------------------- */
331		tcltk_goto_state(ActionAsTerm,StateID) :-
332		(var(StateID) -> print_message(var_state(tcltk_goto_state(ActionAsTerm,StateID))) ;true),
333		(visited_expression_id(StateID)
334		-> true
335		; ajoin(['State ',StateID,' does not exist. Could be due to insufficient memory. Transition: '],Msg),
336		add_warning(tcltk_goto_state,Msg,ActionAsTerm),
337		fail
338		),
339		(current_state_id(CurID) -> true ; print(no_current_state_id),nl),
340		set_current_state_id(StateID),
341	?	(transition(CurID,ActionAsTerm,OpID,StateID)
342		-> /* ok: proper transition */
343		add_to_op_trace_ids(OpID),
344		add_id_to_history(CurID)
345		; (CurID=StateID
346		-> true
347		; debug_println(19,jumping(CurID,ActionAsTerm,StateID)),
348		add_to_op_trace_ids(jump(StateID)),
349		add_id_to_history(CurID)
350		)
351		).
352
353		add_id_to_history(CurID) :-
354		(retract(history(History))->true),
355		assertz(history([CurID|History])), retractall(forward_history(_)).
356
357
358
359		tcltk_add_new_transition(FromID,Action,ToID,ToTempl,TransInfo) :-
360		tcltk_add_new_transition_transid(FromID,Action,ToID,ToTempl,TransInfo,_TransId).
361
362		tcltk_add_new_transition_transid(FromID,Action,ToID,ToTempl,TransInfo,TransId) :-
363		add_new_transition_transid_with_infos(FromID,[],Action,ToID,ToTempl,TransInfo,TransId).
364
365		% variation with precomputed infos for the initial id (FromID)
366		add_new_transition_transid_with_infos(FromID,PrecomputedInfos,Action,ToID,ToTempl,TransInfo,TransId) :-
367		get_operation_internal_name(Action,OpName), % will use $initialise_machine; important for test 961 and PROOF_INFO
368		get_id_of_node_and_add_if_required_with_skip_check(ToTempl,ToID,Exists,FromID,OpName,PrecomputedInfos),
369		%% print_message(tcltk_add_new_transition(FromID,Action,ToID,Exists)), %%
370		( Exists=exists,
371		(preferences:preference(store_only_one_incoming_transition,true),
372		\+ operation_not_yet_covered(OpName) % otherwise store at least one transition to achieve coverage
373		%-> transition(FromID,_,_,_) % add transition to prevent deadlock being detected
374	?	; transition(FromID,Action,TransId,ToID)
375		)
376		-> true % // the transition already exists
377		; % we have a new transition:
378		(preferences:preference(forget_state_space,true)
379		-> (any_transition(FromID,_,_) -> true
380		; store_transition(FromID,'$NO_DEADLOCK',FromID,TransId)) /* just add dummy transition */
381		; store_transition(FromID,Action,ToID,TransId
382		),
383		(store_transition_infos(TransInfo,TransId) -> true
384		; add_internal_error('storing transition info failed', store_transition_infos(TransInfo,TransId)))
385		),
386		mark_operation_as_covered(OpName),
387		(FromID \= ToID, b_or_z_mode, not_all_transitions_added(ToID)
388		-> add_additional_destination_infos(FromID,OpName,ToID) % e.g., PROOF_INF
389		; true
390		)
391		).
392
393		% a version that checks for query/skip operations and then simply returns old id
394		get_id_of_node_and_add_if_required_with_skip_check(_ToTempl,ToID,Exists,FromID,OpName,_PrecomputedInfos) :-
395		animation_mode(b), % csp_and_b mode is *not* ok ; see test 1701 for example
396		b_operation_cannot_modify_state(OpName),
397		!,
398		Exists=exists,ToID=FromID.
399		get_id_of_node_and_add_if_required_with_skip_check(ToTempl,ToID,Exists,FromID,OpName,PrecomputedInfos) :-
400		get_id_of_node_and_add_if_required(ToTempl,ToID,Exists,FromID,OpName,PrecomputedInfos).
401
402
403
404		% will only be called for ToID different from FromID
405		add_additional_destination_infos(FromID,ActionName,ToID) :- %print(add_dest(FromID,ActionName,ToID)),nl,
406		( b_operation_preserves_invariant(ActionName,Full),
407		\+ invariant_still_to_be_checked(FromID),
408		\+ invariant_violated(FromID) % if Invariant does not hold in previous state, we have no idea about invariants in the new state (proof assumes invariant holds before)
409		->
410		(retract(specialized_inv(ToID,OldAVL)) -> true ; empty_avl(OldAVL)),
411		(Full=full_invariant
412		-> assertz(specialized_inv(ToID,invariant_preserved))
413		% unfortunately we cannot yet retract invariant_not_yet_checked
414		; OldAVL=invariant_preserved
415		-> assertz(specialized_inv(ToID,invariant_preserved))
416		; avl_store(ActionName,OldAVL,nothing,NewAVL),
417		%print(specialized_inv(ToID,NewAVL)),nl,
418		assertz(specialized_inv(ToID,NewAVL))
419		)
420		; true
421		).
422		/*
423		Store names of incoming transitions in an AVL tree
424		Used to calculate invariant in presence of proof information
425		*/
426		% we could store this information to allow us to quickly generate traces from root to any state
427		%add_additional_destination_infos(FromID,ActionName,ToID) :-
428		% (reached_via(ToID,_,_) -> true ; %TODO: probably we should also store transition id
429		% assertz(reached_via(ToID,ActionName,FromID))).
430		% TO DO: we could store pge disabling information here disabled_operations
431
432
433
434
435		:- use_module(state_space_exploration_modes,[set_depth_breadth_first_mode/1,dbf_modes/3]).
436
437
438		tcltk_set_dbf_mode(Nr) :- dbf_modes(Nr,Mode,_),!,
439		set_depth_breadth_first_mode(Mode).
440		tcltk_set_dbf_mode(Nr) :- add_error(tcltk_set_dbf_mode,'Unknown mode: ',Nr).
441
442		tcltk_dbf_modes(list(Names)) :- findall(N,dbf_modes(_,_,N),Names).
443
444
445		:- dynamic prev_randomise_enumeration_order/1.
446
447
448		tcltk_mark_current_node_to_be_recomputed_wo_timeout :-
449		current_state_id(CurID), print(recomputing(CurID)),nl,
450		tcltk_mark_node_for_recomputed(CurID),
451		(use_no_timeout(CurID) -> true ; assertz(use_no_timeout(CurID))).
452
453		% used for recomputing a state with random enumeration
454		tcltk_mark_current_node_to_be_recomputed_with_random_enum :-
455		current_state_id(CurID), print(recomputing(CurID)),nl,
456		tcltk_mark_node_for_recomputed(CurID),
457		% retractall(transition(CurID,_,_,_)), % we no longer delete the transitions; this can cause problems with the history
458		% (if CurID appears earlier in the history and we remove the transition) and lead to error messages
459		% also: for the user it may be good to add new transitions incrementally
460		temporary_set_preference(randomise_enumeration_order,true,PREV),
461		assertz(prev_randomise_enumeration_order(PREV)).
462
463		tcltk_finish_current_node_to_be_recomputed_with_random_enum :-
464		retract(prev_randomise_enumeration_order(PREV)),
465		reset_temporary_preference(randomise_enumeration_order,PREV).
466
467		tcltk_mark_node_for_recomputed(ID) :-
468		(not_all_transitions_added(ID) -> true
469		; add_id_at_front(ID)),
470		retractall(max_reached_for_node(ID)),
471		retractall(time_out_for_node(ID,_,_)),
472		% TODO: clear b_operation_cache:operation_cached_time_out for relevant nodes
473		(transition(ID,'$partial_setup_constants',ID2)
474		-> delete_node(ID2) ; true),
475		retractall(state_space:transition(ID,'$partial_setup_constants',_,_)).
476
477		transitions_computed_for_node(ID) :-
478		\+(not_all_transitions_added(ID)),
479		\+ is_not_interesting(ID).
480
481
482
483
484		tcltk_set_initial_machine :-
485		tcltk_clear_machine,
486		b_set_initial_machine,
487		set_animation_mode(b).
488
489		% new profiler
490		%:- use_module('../extensions/profiler/profiler.pl').
491		% old profiler
492		%:- use_module(runtime_profiler,[reset_runtime_profiler/0]).
493
494		% the following clears the entire state space and uses the current state as now starting initial state
495		tcltk_clear_state_space_and_refocus_to_current_state :-
496		Op = 'REFOCUS-ANIMATOR',
497		current_expression(_CurID,CurState),
498		(CurState = const_and_vars(ConstID,VarState) ->
499		visited_expression(ConstID,ConstState),
500		transition(root,SetupConstantAction,_,ConstID)
501		; ConstState=[]),
502		announce_event(reset_specification),
503		(ConstState=[]
504		-> add_trans_id(root,Op,CurState,NewID,_TransId)
505		; add_trans_id(root,SetupConstantAction,ConstState,NewConstID,_),
506		add_trans_id(NewConstID,Op,const_and_vars(NewConstID,VarState),NewID,_),
507		(retract_open_node(NewConstID) -> true ; true),
508		tcltk_goto_state(Op,NewConstID)
509		),
510		tcltk_goto_state(Op,NewID),
511		(retract_open_node(root) -> true ; true).
512
513		:- use_module(eventhandling, [announce_event/1]).
514		tcltk_clear_machine :-
515		announce_event(reset_specification),
516		announce_event(clear_specification),
517		reset_tcltk_interface,
518		set_animation_mode(b),
519		bmachine:b_set_empty_machine,
520		reset_errors,
521		% reset_dynamics, % new profiler
522		% Now done via event handling: b_interpreter:reset_b_interpreter,reset_model_checker,
523		garbage_collect_atoms. % reclaim atoms if possible
524
525		:- use_module(prob2_interface, [start_animation/0, update_preferences_from_spec/0]).
526		tcltk_initialise :-
527		update_preferences_from_spec,
528		start_animation,
529		tcltk_try_reload.
530
531		tcltk_reset :- reset_errors,
532		history(H), op_trace_ids(T),
533		current_state_id(CurID),
534		(forward_history(FH) -> true ; FH=[]),
535		state_space_reset,
536		gen_forward_history(T,[CurID|H],FH,FwdHist),
537		retractall(forward_history(_)),
538		assertz(forward_history(FwdHist)).
539
540		gen_forward_history([],H,R,R) :- (H=[root] -> true ; print(unexpected_remaining_hist(H)),nl).
541		gen_forward_history([A|TT],[ID|TH],Acc,Res) :-
542		gen_forward_history(TT,TH,[forward(ID,A)|Acc],Res).
543
544
545
546		/* ---- getting available options ----- */
547
548		tcltk_get_options_dest_info(L) :-
549		tcltk_get_options_dest_info(L,[]). %[no_query_operations]).
550		tcltk_get_options_dest_info(list(DestinationInfos),Options) :-
551		debug_println(9,start_tcltk_get_options_dest_info),
552		% get a list of all options which are skip events
553		current_state_id(CurID),
554		compute_all_transitions_if_necessary(CurID),
555		tcltk_get_candidates_dest_info(List1),
556		findall(Res, (transition(CurID,ActionAsTerm,ID), % check no_query_operations
557		(member(no_query_operations,Options) -> \+ query_op_transition(ActionAsTerm) ; true),
558		option_dest_info(ID,ActionAsTerm,CurID,Res)),
559		DestinationInfos,List1).
560
561		option_dest_info(DestID,ActionAsTerm,CurID,Res) :- DestID=CurID,!,
562		(query_op_transition(ActionAsTerm) -> Res=query ; Res=skip).
563		option_dest_info(DestID,_,_,Res) :- not_all_transitions_added(DestID),!, Res=open.
564		option_dest_info(DestID,_,_,Res) :- invariant_violated(DestID),!,Res=invariant_violated.
565		option_dest_info(DestID,_,_,Res) :- is_deadlocked(DestID),!,Res=deadlock.
566		option_dest_info(DestID,_,_,Res) :- node_satisfies_goal(DestID),!,Res=goal.
567		option_dest_info(_DestID,_,_,unknown).
568
569		query_op_transition(Term) :- b_or_z_mode,
570		get_operation_name(Term,OpName),
571		b_operation_cannot_modify_state(OpName).
572
573		tcltk_get_options(O) :-
574		tcltk_get_options(O,[]). %[no_query_operations]).
575		tcltk_get_options(list(Options),Parameters) :-
576		current_state_id(CurID), debug_println(9,start_tcltk_get_options(CurID)),
577		catch(tcltk_compute_options(CurID,TransSpecs), user_interrupt_signal, (
578		assert_time_out_for_node(CurID,'unspecified_operation_interrupted_by_user',user_interrupt_signal),
579		tcltk_get_computed_options(CurID,TransSpecs)
580		)),
581		extract_actions(TransSpecs,CurID,Parameters,ActionsAndIDs,Actions),
582		set_current_options(ActionsAndIDs),
583		%print(Actions),nl,
584		debug_println(9,finished_tcltk_get_options(CurID)),
585		Actions = Options.
586
587		:- dynamic current_candidate_options/1.
588
589		% a newer version of tcltk_options which returns list of potentially enabled events
590		% in case MAX_OPERATIONS is set to 0; these virtual events are appended at the end of the
591		% current transitions (which at the start are empty; but can be populated by executed by predicate)
592		tcltk_get_options_or_candidates(list(List)) :-
593		retractall(current_candidate_options(_)),
594		tcltk_get_options(list(List1)),
595		current_state_id(CurID),
596		(preference(maxNrOfEnablingsPerOperation,0),
597		CurID \= root,
598		\+ is_concrete_constants_state_id(CurID) % we could provide setup_constants or initialisation in other states
599		-> tcltk_get_candidate_operations(Candidates),
600		assert(current_candidate_options(Candidates)),
601		maplist(get_cand_name,Candidates,List2),
602		append(List1,List2,List)
603		; List=List1).
604		get_cand_name(candidate(OpName,TO),OpNameRes) :-
605		(TO==true -> ajoin([OpName,' (*timeout*)'],OpNameRes) ; OpNameRes=OpName).
606
607
608		% in case of MAX_OPERATIONS=0 just show the potentially enabled operations
609		tcltk_get_candidate_operations(Candidates) :-
610		current_state_id(CurID),
611		findall(candidate(OpName,TO), potentially_enabled_operation(CurID,OpName,TO),Candidates).
612
613		:- use_module(tools_timeout,[time_out_with_factor_call/4]).
614		potentially_enabled_operation(StateId,OpName,TimeOutOccurred) :- b_or_z_mode,
615		b_top_level_operation(OpName),
616		Simplify=true,
617		get_quantified_operation_enabling_condition(OpName, Guard, _, Simplify),
618		(time_out_with_factor_call(
619		eclipse_interface:test_boolean_expression_in_node(StateId,Guard,'operation Guard'),
620		0.1, [max_time_out(2000),
621		silent],
622		(format('TIME-OUT checking if ~w is enabled; assuming it could be.~n',[OpName]),TimeOutOccurred=true)
623		)
624		-> (var(TimeOutOccurred) -> TimeOutOccurred=false ; true)).
625
626		% get the name of a currently stored candidate option/operation
627		% the option list was empty and we inserted a list of candidate operations
628		tcltk_get_options_candidate_nr_name(Nr,OpName) :-
629		current_candidate_options(List),
630		current_options(List1), length(List1,Len),
631		N1 is Nr-Len, % the candidate of potentially enabled events are listed after the regular options
632		nth1(N1,List,candidate(OpName,_)).
633
634
635		tcltk_get_candidates_dest_info(L) :- current_candidate_options(Cands),!,
636		maplist(get_cand_dest,Cands,L).
637		tcltk_get_candidates_dest_info([]).
638		get_cand_dest(candidate(_,true),time_out).
639		get_cand_dest(_,candidate).
640
641		:- use_module(tools_timeout,[time_out_call/2]).
642		:- use_module(translate,[translate_event_with_src_and_target_id/4]).
643		extract_actions([],_,_,[],[]).
644		extract_actions([(_,Term,_)|T],CurID,Parameters,Srest,ET) :-
645		member(no_query_operations,Parameters),
646		query_op_transition(Term),
647		!,
648		extract_actions(T,CurID,Parameters,Srest,ET).
649		extract_actions([(ActionId,Term,Dst)|T],CurID,Parameters,[(ActionId,Str,Term,Dst)|Srest],[Str|ET]) :-
650		time_out_call(translate_event_with_src_and_target_id(Term,CurID,Dst,Str),
651		Str='**TIMEOUT**'),
652		extract_actions(T,CurID,Parameters,Srest,ET).
653
654		% compute transitions and invariant info
655		compute_state_information_if_necessary :-
656		current_state_id(CurID),
657		compute_state_information_if_necessary(CurID).
658		compute_state_information_if_necessary(CurID) :-
659		compute_all_transitions_if_necessary(CurID,true). % CheckInvariant=true
660
661		tcltk_compute_options(CurID,ActionsAndIDs) :-
662		compute_state_information_if_necessary(CurID),
663		%print(found_transitions(CurID)),nl,
664		tcltk_get_computed_options(CurID,ActionsAndIDs).
665
666		tcltk_get_computed_options(CurID,ActionsAndIDs) :-
667		findall((ActId,ActionAsTerm,DestID),
668		transition(CurID,ActionAsTerm,ActId,DestID),
669		% TO DO: sort or group, especially if we randomize transition/3
670		ActionsAndIDs).
671
672		tcltk_get_status(INVVIOLATED,MAXREACHED,TIMEOUT) :- debug_println(9,start_tcltk_get_status),
673		current_state_id(CurID),
674		(time_out_for_invariant(CurID) -> INVVIOLATED = 2
675		; invariant_violated(CurID) -> INVVIOLATED = 1
676		; not_invariant_checked(CurID) -> INVVIOLATED = 3
677		; not_interesting(CurID) -> INVVIOLATED = 3
678		; INVVIOLATED = 0
679		),
680		(max_reached_for_node(CurID) -> MAXREACHED = 1
681		; not_interesting(CurID) -> MAXREACHED = 2
682		; MAXREACHED = 0),
683		(time_out_for_node(CurID,_,time_out) -> TIMEOUT = 1
684		; time_out_for_node(CurID,_,user_interrupt_signal) -> TIMEOUT = 3 % CTRL-C
685		; time_out_for_node(CurID,_,virtual_time_out(kodkod_timeout)) -> TIMEOUT = 1 % KODKOD; regular time-out
686		; time_out_for_node(CurID,_,_) -> TIMEOUT = 2 % virtual_time_out
687		; TIMEOUT = 0),
688		debug_println(9,got_status(INVVIOLATED,MAXREACHED,TIMEOUT)).
689
690		tcltk_get_ops_with_virtual_timeout(OpNameList) :-
691		current_state_id(StateId),
692		ops_with_timeout(StateId,OpNameList,virtual_time_out(_)).
693		tcltk_get_ops_with_real_timeout(OpNameList) :-
694		current_state_id(StateId),
695		ops_with_timeout(StateId,OpNameList,time_out).
696		% Note: possibilities are currently: time_out, user_interrupt_signal, virtual_time_out(_)
697		tcltk_get_ops_user_interrupt_occurred :-
698		current_state_id(StateId),
699		time_out_for_node(StateId,_,user_interrupt_signal).
700		ops_with_timeout(StateId,OpNameList,Type) :-
701		findall(OpName, time_out_for_node(StateId,OpName,Type), OpNameList).
702
703
704		%%fd_copy_term(X,Y,true) :- copy_term(X,Y).
705
706
707
708		/* --------------------------------------------------------------------- */
709
710		tcltk_get_history(list(StringHistory)) :- debug_println(9,start_tcltk_get_trace),
711		get_action_trace(History),
712		convert_trace_to_list_of_strings(History,StringHistory).
713
714		convert_trace_to_list_of_strings([],[]).
715		convert_trace_to_list_of_strings([action(AS,_)|T],[AS|CT]) :- !,
716		%truncate_atom(AS,1000,TruncatedAS), % especially SETUP_CONSTANTS, INITIALISATION can be very large; leading to performance issues
717		% get_action_trace now truncates
718		convert_trace_to_list_of_strings(T,CT).
719		convert_trace_to_list_of_strings([H|T],[H|CT]) :- convert_trace_to_list_of_strings(T,CT).
720
721		tcltk_write_uml_sequence_chart(File) :-
722		write_uml_sequence_chart(File).
723
724		/* --------------------------------------------------------------------- */
725
726		:- dynamic cached_state_as_strings/2.
727
728		%tcltk_get_state(list(List)) :- !,List=[]. % comment in to disable State Properties View in ProB Tcl/Tk
729		tcltk_get_state(list(List)) :- debug_println(9,start_tcltk_get_state),
730		current_expression(CurID,CurState),
731		compute_state_information_if_necessary(CurID),
732		(time_out_for_invariant(CurID) -> List = [invariant_time_out|StateAsStrings]
733		; invariant_violated(CurID) -> List = [invariant_violated|StateAsStrings]
734		; invariant_not_yet_checked(CurID) -> List = [invariant_not_checked|StateAsStrings]
735		; CurID=root -> List = StateAsStrings
736		; CurState = concrete_constants(_) -> List = StateAsStrings
737		; specfile:b_or_z_mode -> List=[invariant_ok|StateAsStrings] % only in b_or_z_mode do we add not_invariant_checked facts and check invariant while model checking/animating
738		; List=StateAsStrings),
739		(cached_state_as_strings(CurID,StateAsStrings) % TO DO: separate constant / variable properties ?
740		-> true
741		; retractall(cached_state_as_strings(_,_)),
742		time_out_call(tcltk_get_state(StateAsStrings,CurState),
743		StateAsStrings = ['***TIMEOUT-PROPERTY***']),
744		assertz(cached_state_as_strings(CurID,StateAsStrings))
745		),
746		debug_println(9,finished_tcltk_get_state).
747
748		tcltk_get_state(StateAsStrings,State) :-
749		%print(get_state),nl,
750		findall(Prop,property(State,Prop),StateProps),
751		%print(translating(StateProps)),nl,
752		translate:translate_properties_with_limit(StateProps,StateAsStrings).
753		%print(translated(StateAsStrings)),nl.
754
755
756		tcltk_get_state_errors(list(ErrorsAsStrings)) :-
757		get_current_state_errors(_CurID,Errors),
758		translate_state_errors(Errors,ErrorsAsStrings).
759
760		get_current_state_errors(CurID,Errors) :-
761		current_state_id(CurID),
762		findall(Error,( state_error(CurID,_,Error), Error \== invariant_violated ), Errors).
763
764		:- dynamic last_detailed_error/3.
765
766		reset_tcltk_interface :- debug_println(19,reset_tcltk),
767		retractall(cbc_inv_error_found(_,_)), reset_nr_cbc_sols,
768		retractall(find_flag(_,_)),
769		retractall(resetable_node(_)),
770		retractall(non_det_constant(_)),
771		retractall(current_candidate_options(_)),
772		retractall(cached_state_as_strings(_,_)),
773		retractall(last_detailed_error(_,_,_)).
774
775		tcltk_get_detailed_state_error(Num,ErrorMsg,Srow,Scol,Erow,Ecol) :-
776		retractall(last_detailed_error(_,_,_)),
777		get_current_state_errors(CurID,Errors),
778		nth0(Num,Errors,Error),
779		!,
780		explain_state_error(Error,Span,ErrorMsg),
781		assertz(last_detailed_error(CurID,Span,ErrorMsg)), % save info, so that we can debug if Span contains a span_predicate
782		%(generate_dot_from_last_span_predicate('~/Desktop/err.dot') -> true ; true),
783		(extract_line_col_for_main_file(Span,Srow,Scol,Erow,Ecol)
784		-> true
785		; Srow= -1, Scol= -1, Erow= -2, Ecol= -2).
786
787
788		:- use_module(probsrc(tools_commands),[edit_file/2]).
789		:- use_module(specfile,[b_absolute_file_name_relative_to_opened_file/2]).
790		% show location of state error in external editor
791		tcltk_open_state_error_in_editor(Num) :-
792		get_current_state_errors(_,Errors),
793		nth0(Num,Errors,Error),
794		(get_state_error_span(Error,Span)
795		-> (extract_file_line_col(Span,FILE,LINE,_COL,_Erow,_Ecol)
796		-> b_absolute_file_name_relative_to_opened_file(FILE,AFILE),
797		edit_file(AFILE,LINE)
798		; add_error(tcltk_open_state_error_in_editor,'Could not extract file position: ',Span)
799		)
800		; add_error(tcltk_open_state_error_in_editor,'Could not extract source location for state error: ',Num)
801		).
802
803		can_generate_dot_from_last_state_error :-
804		last_detailed_error(_CurID,ErrSpan,_),!,
805		get_inner_span(ErrSpan,span_predicate(_,_,_)).
806		can_generate_dot_from_last_state_error :-
807		current_state_id(CurID), state_error(CurID,_,_). % not sure if it is really possible to extract span predicate though
808		generate_dot_from_last_span_predicate(FileName) :-
809		current_state_id(CurID),
810		(last_detailed_error(CurID,ErrSpan,_ErrorMsg) % also works with expressions
811		-> true
812		; tcltk_get_detailed_state_error(0,_,_,_,_,_), % try and generate error description
813		last_detailed_error(CurID,ErrSpan,_)
814		),
815		get_inner_span(ErrSpan,span_predicate(P,LS,State)),
816		(State=[], visited_expression(CurID,S),
817		state_corresponds_to_initialised_b_machine(S,FullState)
818		-> true % span predicates from event trace do not have the current state, add state
819		; FullState=State),
820		write_dot_file_for_pred_expr_and_state(P, LS, FullState,FileName).
821
822		get_inner_span(pos_context(Span1,_,_),SP) :- !,
823		get_inner_span(Span1,SP).
824		get_inner_span(SP,SP).
825
826		tcltk_current_state_invariant_violated :-
827		current_state_id(CurID),
828		invariant_violated(CurID).
829
830		tcltk_state_exists_with_invariant_violated :-
831		(invariant_violated(_) -> true).
832
833		/* --------------------------------------------------------------------- */
834
835		:- use_module(b_trace_checking, [tcltk_save_history_as_trace_file/2]).
836		tcltk_save_history_as_trace_file(File) :-
837		tcltk_save_history_as_trace_file(prolog,File).
838
839
840		/* --------------------------------------------------------------------- */
841
842		:- use_module(translate, [get_bexpression_column_template/4]).
843		evaluate_bexpr_over_state(Stream,Expr,ValueTemplate,Columns,ResultColStrings,BState,OpName) :-
844		format(Stream,'~w,',[OpName]),
845		b_compute_expression_with_prob_ids(Expr,BState,Value),
846		copy_term((ValueTemplate,Columns),(Value,ResultCols)),
847		my_print_csv_value(ResultCols,Stream),
848		maplist(translate:translate_bvalue,ResultCols,ResultColStrings),
849		nl(Stream).
850
851		% evaluate an expression over the history and save the result to a CSV file
852		evaluate_expression_over_history_to_csv_file(Expr,File) :-
853		parse_machine_expression(Expr,TypedExpr),
854		get_bexpression_column_template(TypedExpr,ValueTemplate,ColHeaders,Columns),
855		format('Writing CSV file: ~w~n',[File]),
856		open(File,write,Stream),
857		format(Stream,'OPERATION,',[]),
858		my_print_csv_atoms(ColHeaders,Stream),
859		call_cleanup(map_over_history(evaluate_bexpr_over_state(Stream,TypedExpr,ValueTemplate,Columns),_),
860		close(Stream)),
861		format('Finished writing CSV file: ~w~n',[File]).
862
863
864		tcltk_evaluate_expression_over_history(Expr,list([list(['OPERATION','State Id'|ColHeaders])|ColumnLists])) :-
865		parse_machine_expression(Expr,TypedExpr),
866		get_bexpression_column_template(TypedExpr,ValueTemplate,ColHeaders,Columns),
867		map_over_history(evaluate_bexpr_over_state(user_output,TypedExpr,ValueTemplate,Columns),
868		ColumnLists).
869
870		map_over_history(Pred,ResColumnLists) :-
871		history(H), current_state_id(CurID),
872		reverse([CurID|H],RH),
873		get_action_trace(T), reverse(T,RT),
874		maplist(call_pred_on_expanded_state(Pred),RH,[action(root,root)|RT],ColumnLists),
875		prune_list(ColumnLists,ResColumnLists).
876		% remove unknown elements at front for Tk
877		prune_list([unknown|T],Res) :- !, prune_list(T,Res).
878		prune_list(R,R).
879
880		call_pred_on_expanded_state(_Pred,root,_,ColList) :- !, ColList=unknown.
881		call_pred_on_expanded_state(Pred,StateId,action(_,ActionTerm),ResColList) :- print(StateId),nl,
882		specfile:get_operation_name(ActionTerm,OpName),
883		format('Processing state ~w (reached via ~w)~n',[StateId,OpName]),
884		visited_expression(StateId,State),
885		(state_corresponds_to_initialised_b_machine(State,BState)
886		-> call(Pred,ColList,BState,OpName), ResColList = list([OpName,StateId|ColList])
887		; ResColList = unknown ).
888
889		:- use_module(eval_let_store,[extend_state_with_probids_and_lets/2]).
890		b_compute_expression_with_prob_ids(Expr,BState,Value) :-
891		extend_state_with_probids_and_lets(BState,BState2),
892		b_interpreter:b_compute_expression_nowf(Expr,[],BState2,Value,'Tcl/Tk',0).
893
894
895		my_print_csv_atoms([A,B|T],Stream) :- !, format(Stream,'"~w",',[A]),
896		my_print_csv_atoms([B|T],Stream).
897		my_print_csv_atoms([A],Stream) :- format(Stream,'"~w"~n',[A]).
898
899		my_print_csv_value([A,B|T],Stream) :- !,
900		my_print_csv_value([A],Stream),
901		write(Stream,','),
902		my_print_csv_value([B|T],Stream).
903		my_print_csv_value([V],Stream) :-
904		(no_quotes_necessary(V) -> true ; write(Stream,'"')),
905		translate:print_bvalue_stream(Stream,V),
906		(no_quotes_necessary(V) -> true ; write(Stream,'"')).
907
908		no_quotes_necessary(int(_)).
909		no_quotes_necessary(pred_false).
910		no_quotes_necessary(pred_true).
911
912
913		/* --------------------------------------------------------------------- */
914
915		:- use_module(probltlsrc(ltl_tools),[temporal_parser/3]).
916		:- use_module(probltlsrc(ltl),[preprocess_formula/2]).
917
918		tcltk_execute_until(FormulaAsAtom) :-
919		(temporal_parser(FormulaAsAtom,ltl,Ltl) ->
920		true
921		;
922		add_error(ltl,'LTL Parser failed: ',FormulaAsAtom),fail),
923		( Ltl=syntax_error ->
924		add_error(ltl,'Syntax error while parsing: ',FormulaAsAtom),fail
925		;
926		preprocess_formula(Ltl,Ltl2)
927		),
928		current_state_id(CurID),
929		prob2_interface: find_trace1(CurID,Ltl2,no_loop,1000,Trace,_Result),
930		%TODO: check if result is deadlock. Will not fail.
931		update_history_from_trace(Trace).
932
933		update_history_from_trace([]). % TODO: Can we get an empty trace from find_trace predicate?
934		update_history_from_trace([op(OpID,_Name,CurID,NextID)]) :-
935		add_id_to_history(CurID),
936		add_to_op_trace_ids(OpID),
937		add_id_to_history(NextID),
938		set_current_state_id(NextID).
939		update_history_from_trace([op(OpID,_Name,CurID,NextID)|T]) :-
940		add_id_to_history(CurID),
941		add_to_op_trace_ids(OpID),
942		add_id_to_history(NextID),
943		update_history_from_trace(T).
944
945
946		tcltk_random_perform :- tcltk_random_perform2(_,fully_random).
947		tcltk_random_perform(Kind) :- tcltk_random_perform2(_,Kind).
948
949		% Kind can be fully_random, no_self_loops, explore_open
950		% TODO: other options like out_degree, ...
951		tcltk_random_perform2(ActionId,Kind) :-
952		current_options(Opts),
953		current_state_id(CurID),
954		(Kind=explore_open, exclude(is_already_explored,Opts,Options2), Options2 = [_|_] -> true % try and find unexplored successor
955		; is_heuristic(Kind),
956		maplist(compute_heuristic(Kind),Opts,HOpts),
957		sort(HOpts,SHOpts),
958		keep_min_heuristic(SHOpts,Opts1)
959		->
960		(exclude(is_already_explored,Opts1,Options2), Options2 = [_|_]
961		-> true % among the nodes with the lowest heuristic value choose open nodes first; to try find new values
962		; Options2=Opts1)
963		; Kind\=fully_random,
964		exclude(is_self_loop(CurID),Opts,Options2), Options2 = [_|_] -> true % try find different node
965		; Options2=Opts),
966		length(Options2,Len),
967		(Len>0
968		-> L1 is Len+1,
969		random(1,L1,RanChoice),
970		tcltk_perform_nr_option(RanChoice,Options2,ActionId)
971		; true
972		).
973
974		is_already_explored((_Id,_Action,_,NextId)) :- \+ not_all_transitions_added(NextId).
975		is_self_loop(CurId,(_Id,_Action,_,CurId)).
976
977		is_heuristic(heuristic).
978		is_heuristic(min_out_degree).
979		:- use_module(probsrc(state_space_exploration_modes),[compute_heuristic_function_for_state_id/2]).
980		:- use_module(probsrc(state_space),[out_degree/2, compute_transitions_if_necessary/1]).
981		compute_heuristic(Kind,(Id,Action,ActTerm,NextId),heurval(HeurVal,Id,Action,ActTerm,NextId)) :-
982		compute_h2(Kind,NextId,HeurVal).
983		compute_h2(heuristic,NextId,HeurVal) :-
984		compute_heuristic_function_for_state_id(NextId,HeurVal).
985		compute_h2(min_out_degree,NextId,HeurVal) :-
986		compute_transitions_if_necessary(NextId),
987		out_degree(NextId,HeurVal).
988		%compute_h2(out_degree,NextId,HeurVal) :-
989
990		% only keep the maximal value
991		keep_min_heuristic([heurval(HeurVal,Id,Action,ActTerm,NextId)|HT],
992		[(Id,Action,ActTerm,NextId)|T]) :- keep_min2(HT,HeurVal,T).
993		keep_min2([heurval(HeurVal,Id,Action,ActTerm,NextId)|HT],HeurVal,
994		[(Id,Action,ActTerm,NextId)|T]) :- !, keep_min2(HT,HeurVal,T).
995		keep_min2(_,_,[]).
996
997
998		tcltk_get_line_col(Nr,list(StartLine),list(StartCol),list(EndLine),list(EndCol)) :- /* just get the location in the source code */
999		current_options(Options),
1000		nth1(Nr,Options,(_Id,_Action,ActionAsTerm,_NewID)),
1001		%print(get_source_text(ActionAsTerm)),nl,
1002		time_out_call(get_source_text_positions(ActionAsTerm,StartLine,StartCol,EndLine,EndCol),
1003		add_error_and_fail(tcltk_get_line_col,'Timeout determining source code position: ',ActionAsTerm)),
1004		StartLine \= []. % otherwise fail
1005		% print(startlines(StartLine)),nl,print(startcols(StartCol)),nl,
1006		% print(endlines(EndLine)),nl, print(endcol(EndCol)),nl.
1007
1008		tcltk_is_sync_event(Nr) :-
1009		current_options(Options),
1010		nth1(Nr,Options,(_Id,_Action,ActionAsTerm,_NewID)),
1011		extract_span_from_event(ActionAsTerm,SPAN,_,_),
1012		extract_span_info(SPAN,Info),
1013		% print(extracted_span_info_for_sync(Info,SPAN)),nl,
1014		member(sharing,Info).
1015
1016		:- use_module(specfile,[get_operation_description_for_transition/3]).
1017		% get textual description of nth option in current options
1018		% is derived from description pragma attached to operations
1019		tcltk_get_options_nr_description(Nr,Desc) :-
1020		b_or_z_mode,
1021		current_state_id(CurID),
1022		current_options(Options),
1023		nth1(Nr,Options,(_ActionId,_Action,ActionAsTerm,_NewID)),
1024		get_operation_description_for_transition(CurID,ActionAsTerm,Desc).
1025
1026
1027		% counter-part to tcltk_get_options, to execute the option/operation number Nr in that list
1028		tcltk_perform_nr(Nr) :-
1029		current_options(Options),
1030		tcltk_perform_nr_option(Nr,Options,_).
1031
1032		tcltk_perform_nr_option(Nr,Options,ActionId) :-
1033		(nth1(Nr,Options,(ActionId,_Action,ActionAsTerm,NewID))
1034		-> (forward_history([forward(NewID,ActionId)|_FwdHist])
1035		-> tcltk_forward
1036		; tcltk_perform_action_term(ActionAsTerm,NewID),
1037		retractall(forward_history(_))
1038		)
1039		; tcltk_backtrack /* interpret as backtrack */
1040		).
1041
1042
1043		tcltk_can_backtrack :- history([_|_]).
1044		tcltk_can_backtrack(Len) :- history(His), length(His,Len),Len>0.
1045
1046		tcltk_backtrack :- \+ tcltk_can_backtrack,!,
1047		print_message('Cannot backtrack'),fail.
1048		tcltk_backtrack :-
1049		remove_from_op_trace_ids(LastTraceH),
1050		retract(history(History)),
1051		retract(current_state_id(CurID)),!,
1052		History= [LastID|EHist],
1053		assertz(history(EHist)),
1054		%visited_expression(LastID,LastExpr,LastBody),
1055		assertz(current_state_id(LastID)),
1056		(retract(forward_history(FwdHist)) -> true ; FwdHist=[]),
1057		assertz(forward_history([forward(CurID,LastTraceH)|FwdHist])).
1058
1059		% used for right-clicks in history
1060		tcltk_backtrack(N) :- N =< 0, !.
1061		tcltk_backtrack(N) :- tcltk_backtrack, N1 is N-1, tcltk_backtrack(N1).
1062
1063		:- dynamic saved_forward_history/2.
1064		:- volatile saved_forward_history/2.
1065
1066
1067		% save certain information to restore when reload is completed:
1068		tcltk_prepare_for_reload :-
1069		saved_forward_history([_|_],Mode), % tcltk_try_reload not executed; probably reloading failed
1070		animation_mode(Mode),
1071		current_state_id(root), %user has not performed another trace
1072		get_action_trace([]),!,
1073		format('Keeping saved forward history~n',[]). % so that user can fix error and re-load again
1074		tcltk_prepare_for_reload :-
1075		retractall(saved_forward_history(_,_)),
1076		get_action_term_trace(TrA),reverse(TrA,Tr),
1077		%print(prepare_reloading(Tr)),nl,
1078		maplist(gen_unknown_forward,Tr,SavedForwardHistory),
1079		animation_mode(Mode),
1080		% TO DO: add current forward history as well and restore when doing a reload with fastforward
1081		% forward_history(ForwHis), maplist(remove_forward_id,ForwHis,SavedPrevForwHis),
1082		assertz(saved_forward_history(SavedForwardHistory,Mode)).
1083
1084		%remove_forward_id(forward(_,Step),forward('$UNKNOWN',Step)).
1085		gen_unknown_forward(Step,forward('$UNKNOWN',Step)). % the forward ID is unknown
1086
1087		% try reloading certain information from previous load of same model
1088		tcltk_try_reload :-
1089		retract(saved_forward_history(SavedForwardHistory,Mode)),
1090		animation_mode(Mode), % we are in the same mode as when saved
1091		!,
1092		% TO DO: also retractall in other places
1093		%print(reloading(SavedForwardHistory)),nl,
1094		retractall(forward_history(_)),
1095		assertz(forward_history(SavedForwardHistory)).
1096		tcltk_try_reload.
1097
1098
1099		% go forward while possible
1100		tcltk_fast_forward :- tcltk_can_forward,!, tcltk_forward,
1101		current_state_id(CurID),
1102		compute_state_information_if_necessary(CurID),
1103		tcltk_fast_forward.
1104		tcltk_fast_forward.
1105
1106		tcltk_can_forward :- forward_history([_|_]).
1107		tcltk_can_forward(Len) :- forward_history(His), length(His,Len), Len>0.
1108
1109		tcltk_forward :- \+ tcltk_can_forward,!,
1110		print_message('Cannot go forward'),fail.
1111		tcltk_forward :-
1112		retract(forward_history([forward(FwdID,LastTraceH)|FwdHist])),
1113		% TO DO: check if FwdID is '$UNKNOWN' -> then try to find successor which can be reached via LastTraceH
1114		retract(history(EHist)),
1115		retract(current_state_id(CurID)),!,
1116		go_forward(FwdID,LastTraceH,FwdHist,CurID,EHist).
1117		go_forward('$UNKNOWN',ActionAsTerm,FwdHist,CurID,EHist) :-
1118		transition(CurID,ActionAsTerm,TransitionID,FwdID),!,
1119		%print(found(CurID,ActionAsTerm,TransitionID,FwdID)),nl,
1120		go_forward(FwdID,TransitionID,FwdHist,CurID,EHist).
1121		% TO DO: try and execute by predicat in case max_reached is true !
1122		go_forward('$UNKNOWN',ActionAsTerm,FwdHist,CurID,EHist) :-
1123		is_initialisation_op(ActionAsTerm),
1124		% maybe PROPERTIES/INITIALISATION has changed; try and replay with other values
1125		transition(CurID,ActionAsTerm2,TransitionID,FwdID),
1126		is_initialisation_op(ActionAsTerm2),
1127		!,
1128		%print(found(CurID,ActionAsTerm,TransitionID,FwdID)),nl,
1129		translate_event(ActionAsTerm,Action),
1130		format('Could not replay ~w.~nUsing other possible transition instead.~n',[Action]),
1131		go_forward(FwdID,TransitionID,FwdHist,CurID,EHist).
1132		go_forward('$UNKNOWN',ActionAsTerm,_FwdHist,CurID,EHist) :- !,
1133		assertz(forward_history([])),
1134		assertz(history(EHist)),
1135		assertz(current_state_id(CurID)),
1136		translate_event(ActionAsTerm,Action),
1137		add_error(tcltk_forward,'Cannot replay step after reload: ',Action).
1138		go_forward(FwdID,LastTraceH,FwdHist,CurID,EHist) :-
1139		assertz(forward_history(FwdHist)),
1140		assertz(history([CurID|EHist])),
1141		add_to_op_trace_ids(LastTraceH),
1142		assertz(current_state_id(FwdID)),
1143		re_execute_transition_if_necessary(CurID,LastTraceH,FwdID).
1144		%visited_expression(FwdID,FwdExpr,FwdBody).
1145
1146		is_initialisation_op(Op) :-
1147		(functor(Op,'$setup_constants',_) ;functor(Op,'$initialise_machine',_)).
1148
1149		% re-execute operation with side-effects if necessary and if preference set
1150		% TO DO: tie into tcltk_perform so that not only the forward button but also double click
1151		% in operations pane works
1152		re_execute_transition_if_necessary(FromID,TransitionID,ToID) :-
1153		b_or_z_mode,
1154		get_preference(re_execute_operations_with_side_effects,true),
1155		bmachine_construction:external_procedure_used(_), % TO DO: check if operation itself has side-effects
1156		!,
1157		(re_execute_transition(FromID,TransitionID,ToID)
1158		-> true
1159		; add_error(tcltk_forward,'Could not re-execute operation: ',TransitionID)).
1160		re_execute_transition_if_necessary(_,_,_).
1161
1162		re_execute_transition(FromID,TransitionID,ToID) :-
1163		transition(FromID,ActionTerm,TransitionID,ToID),
1164		%%print(trans(ActionTerm)),nl,
1165		specfile:get_operation_name(ActionTerm,OpName),
1166		debug_println(9,re_executing_operation(OpName,FromID,TransitionID,ToID)),
1167		visited_expression(FromID,InState),
1168		specfile:b_trans(InState,OpName,ActionTerm,_NewState,_TransInfo),
1169		debug_println(9,re_executed(OpName)).
1170
1171		% a version of tcltk_perform_action_term which can be given only the String (e.g., for trace checking)
1172		tcltk_perform_action_string(ActionString,ActionAsTerm,NewID) :-
1173		current_state_id(CurID),
1174	?	transition(CurID,ActionAsTerm,_,NewID),
1175		translate_event_with_src_and_target_id(ActionAsTerm,CurID,NewID,ActionString),
1176		tcltk_goto_state(ActionAsTerm,NewID).
1177		% translate_event_with_limit(ActionAsTerm,5000,ActionString). % should use same limit as below; otherwise trace checking will fail; ideally we should check ActionString is prefix
1178		%translate_event(ActionAsTerm,ActionString).
1179
1180		% perform the Action with term ActionAsTerm leading to new state NewID
1181		tcltk_perform_action_term(ActionAsTerm,NewID) :- %print(tcltk_perform_action_term(Action,ActionAsTerm,NewID)),nl,
1182		(var(ActionAsTerm)
1183		-> add_internal_error('Illegal call: ',tcltk_perform_action_term(ActionAsTerm,NewID)) ; true),
1184		tcltk_goto_state(ActionAsTerm,NewID).
1185
1186		/* allows one to execute an action in term form, from the current state: */
1187		%tcltk_perform_action(T,Cur) :- print_message(perf(T,Cur)),fail.
1188
1189		tcltk_perform_action(ActionAsTerm,NewID) :-
1190		current_state_id(CurID),
1191		tcltk_perform_action(CurID,ActionAsTerm,NewID).
1192		tcltk_perform_action(CurID,ActionAsTerm,NewID) :-
1193		tcltk_perform_action(CurID,ActionAsTerm,NewID,_).
1194		tcltk_perform_action(CurID,ActionAsTerm,TransitionID,NewStateID) :-
1195		transition(CurID,ActionAsTerm,TransitionID,NewStateID),
1196		tcltk_goto_state(ActionAsTerm,NewStateID).
1197
1198		tcltk_no_constants_or_no_inititalisation_found :-
1199		(current_expression(root,_) ; current_expression(_,concrete_constants(_))),
1200		current_options([]).
1201
1202		/* ------------ */
1203		/* tcltk_open/1 */
1204		/* ------------ */
1205
1206
1207		%prolog_check_load_errors :-
1208		% (tcltk_find_untyped_consts(ErrRes)
1209		% -> add_error(prolog_open,'These constants were not given a proper type:', ErrRes)
1210		% ; true),
1211		% (tcltk_find_untyped_vars(ErrRes)
1212		% -> add_error(prolog_open,'These variables were not given a proper type:', ErrRes)
1213		% ; true).
1214
1215		tcltk_open_b_file_for_minor_mode(File,Minor) :- tcltk_open_b_file(File),
1216		set_animation_minor_mode(Minor).
1217
1218		tcltk_open_b_file(File) :-
1219		tcltk_clear_machine,
1220		set_animation_mode(b),
1221		print_message(loading_b_file(File)),flush_output,
1222		set_currently_opening_file(File),
1223		% to do: b_load_machine_probfile
1224		(b_load_aux(File)
1225		-> print_message(loaded),
1226		set_currently_opened_b_file(File)
1227		; tcltk_set_failed_to_open_file(File),
1228		fail
1229		).
1230
1231		tcltk_set_failed_to_open_file(File) :-
1232		set_failed_to_open_file(File),
1233		copy_current_errors_to_state(root,loading_context(File)).
1234
1235		:- use_module(probsrc(bmachine), [b_load_machine_from_file/1,b_load_machine_probfile/1]).
1236		:- use_module(tools,[get_filename_extension/2]).
1237		b_load_aux(File) :- get_filename_extension(File,'prob'),!,
1238		b_load_machine_probfile(File).
1239		b_load_aux(File) :-
1240		b_load_machine_from_file(File).
1241
1242		:- use_module(xtl_interface,[open_xtl_file/1]).
1243		tcltk_open_xtl_file(File) :- % TODO: redundant wrt load_xtl_spec_from_prolog_file
1244		tcltk_clear_machine,
1245		set_animation_mode(xtl),
1246		set_currently_opening_file(File),
1247		(open_xtl_file(File)
1248		-> set_currently_opened_file(File)
1249		; tcltk_set_failed_to_open_file(File), fail).
1250
1251
1252		tcltk_open_cspm_file(File) :-
1253		tcltk_clear_machine,
1254		set_animation_mode(cspm),
1255		set_currently_opening_file(File),
1256		(xtl_interface:open_cspm_file(File)
1257		-> set_currently_opened_file(File)
1258		; tcltk_set_failed_to_open_file(File), fail).
1259
1260		:- use_module(xtl_interface).
1261		%tcltk_open_promela_file(File) :-
1262		% tcltk_clear_machine,
1263		% set_animation_mode(promela), set_currently_opening_file(File),
1264		% xtl_interface:open_promela_file(File), set_currently_opened_file(File).
1265
1266		% disabled because Java parser seems broken
1267		%tcltk_open_smv_file(File) :-
1268		% tcltk_clear_machine,
1269		% set_animation_mode(smv), set_currently_opening_file(File),
1270		% xtl_interface:open_smv_file(File), set_currently_opened_file(File).
1271
1272		:- use_module(specfile,[type_check_csp_and_b/0]).
1273		:- use_module(library(file_systems),[file_exists/1,delete_file/1]).
1274
1275		tcltk_add_csp_file(File) :-
1276		\+ file_exists(File),!,
1277		add_error(csp_guide,'CSP guide file does not exist:',File).
1278		tcltk_add_csp_file(File) :-
1279		unset_animation_minor_modes(L), % we could be in z or tla or eventb mode
1280		set_animation_mode(csp_and_b),
1281		reset_animation_minor_modes(L),
1282		xtl_interface:open_cspm_file(File),
1283		notify_change_of_animation_mode,
1284		type_check_csp_and_b.
1285
1286		notify_change_of_animation_mode :-
1287		announce_event(change_of_animation_mode).
1288		% clear_applicable_flag. % no done via event handling
1289
1290
1291		tcltk_open_z_file(File) :-
1292		tcltk_clear_machine,
1293		tcltk_open_z_file2(File).
1294		tcltk_open_z_file2(File) :-
1295		set_currently_opening_file(File),
1296		open_proz_file(File,BMachine),
1297		set_animation_mode(b), set_animation_minor_mode(z),
1298		b_set_typed_machine(BMachine,File),
1299		!,
1300		set_currently_opened_b_file(File).
1301		tcltk_open_z_file2(File) :- tcltk_set_failed_to_open_file(File),fail.
1302
1303		:- use_module(parsercall,[call_fuzz_parser/2]).
1304		tcltk_open_z_tex_file(TexFile) :-
1305		tcltk_clear_machine,
1306		call_fuzz_parser(TexFile,FuzzFile),
1307		tcltk_open_z_file2(FuzzFile).
1308
1309
1310		:- use_module(eclipse_interface,[load_eventb_file/1]).
1311		tcltk_load_packaged_eventb_file(File) :-
1312		tcltk_clear_machine,
1313		load_eventb_file(File).
1314
1315		:- use_module(parsercall,[call_alloy2pl_parser/2]).
1316		:- use_module(probsrc('alloy2b/alloy2b')).
1317		tcltk_open_alloy_file(AlloyFile) :-
1318		tcltk_clear_machine,
1319		start_ms_timer(T1),
1320		formatsilent('Parsing Alloy file: ~w~n',[AlloyFile]),
1321		set_currently_opening_file(AlloyFile),
1322		call_alloy2pl_parser(AlloyFile,PrologFile),
1323		(silent_mode(off) -> stop_ms_walltimer_with_msg(T1,'parsing and type checking: ') ; true),
1324		%printsilent(generated_prolog_ast(PrologFile)),nls,
1325		start_ms_timer(T2),
1326		( load_alloy_ast_prolog_file(PrologFile)
1327		-> true
1328		; delete_file(PrologFile), % delete parsed Prolog file if model couldn't be loaded
1329		fail % since it's potentially empty due to the failure
1330		),
1331		!,
1332		(silent_mode(off) -> stop_ms_walltimer_with_msg(T2,'loading and translation to B: ') ; true),
1333		set_currently_opened_b_file(AlloyFile).
1334		tcltk_open_alloy_file(AlloyFile) :- tcltk_set_failed_to_open_file(AlloyFile),fail.
1335
1336
1337		tcltk_open_alloy_prolog_ast_file(AlloyPrologFile) :-
1338		tcltk_clear_machine,
1339		start_ms_timer(T2),
1340		load_alloy_ast_prolog_file(AlloyPrologFile),
1341		!,
1342		(silent_mode(off) -> stop_ms_walltimer_with_msg(T2,'loading B translation of Alloy: ') ; true),
1343		set_currently_opened_b_file(AlloyPrologFile).
1344
1345		%% tcltk_load_alloy_cmd_in_current_translation(+CmdName).
1346		tcltk_load_alloy_cmd_in_current_translation(CmdName) :-
1347		alloy2b:load_command_in_current_translation(CmdName).
1348
1349		%% tcltk_get_alloy_cmd_names(-CmdNames).
1350		tcltk_get_alloy_cmd_names(CmdNames) :-
1351		alloy2b:get_command_names(CmdNames).
1352
1353		%% tcltk_verify_alloy_cmd(+CmdName, +SolverName, -CmdIsValid, -IsCheckCmd).
1354		tcltk_verify_alloy_cmd(CmdName, SolverName, CmdIsValid, IsCheckCmd) :-
1355		verify_alloy_command(CmdName, SolverName, CmdIsValid, IsCheckCmd, Res),
1356		( Res = solution(Bindings)
1357		-> bindings_to_state(Bindings, State),
1358		tcltk_add_cbc_state(State, CmdName)
1359		; true
1360		).
1361
1362		bindings_to_state([], []).
1363		bindings_to_state([Binding|T], [Bind|NT]) :-
1364		(Binding = binding(Id,Val,_); Binding = bind(Id,Val)),
1365		Bind = bind(Id,Val),
1366		bindings_to_state(T, NT).
1367
1368		/* --------------------------------------------------------------------- */
1369
1370		tcltk_exists_an_open_node :-
1371		not_all_transitions_added(_) ; not_interesting(_).
1372		tcltk_goto_an_open_node :-
1373		(not_all_transitions_added(ID) ; not_interesting(ID)),!,
1374		tcltk_goto_state(find_open_node,ID).
1375		tcltk_goto_max_reached_node :-
1376		(max_reached_for_node(ID) ; time_out_for_node(ID)),!,
1377		tcltk_execute_trace_to_node(ID).
1378		tcltk_goto_timeout_node :-
1379		time_out_for_node(ID),!,
1380		tcltk_execute_trace_to_node(ID).
1381		% tcltk_goto_state(find_max_reached_node,ID).
1382
1383		tcltk_goto_an_invariant_violation :-
1384		invariant_violated(ID),!,
1385		tcltk_goto_state(find_inv_violation,ID).
1386
1387
1388		tcltk_goto_node_with_id(ToID) :-
1389		current_state_id(ToID),!.
1390		tcltk_goto_node_with_id(ID) :-
1391		visited_expression_id(ID),
1392		tcltk_execute_trace_to_node(ID).
1393
1394
1395
1396		/* --------------------------------------------------------------------- */
1397
1398		% TO DO: clean up and move into model_checker module
1399
1400	?	tcltk_state_space_only_has_root_node :- transition(root,_,ID),
1401		\+ not_all_transitions_added(ID),!,fail.
1402		tcltk_state_space_only_has_root_node.
1403
1404		tcltk_search_among_existing_nodes(TclTkRes,FindDeadlocks,FindInvViolations,
1405		FindGoal,FindAssViolations,FindStateErrors) :-
1406		search_among_existing_nodes(Res,FindDeadlocks,FindInvViolations,
1407		FindGoal,FindAssViolations,FindStateErrors),
1408		translate_error_for_tclk(Res,TclTkRes).
1409
1410		% if tcltk_state_space_only_has_root_node is true: then we should call search_among_existing_nodes before doing open_search to ensure that we uncover state_errors in the root node
1411		% TODO: process mc_continue_after_error preference
1412		search_among_existing_nodes(invariant_violation,_FindDeadlocks,FindInvViolations,
1413		_FindGoal,_FindAssViolations,_FindStateErrors) :-
1414		(get_state_space_stats(_,_,PrN), PrN>100
1415		-> print_message('Search Among Processed Nodes'), print_message(number_of_nodes(PrN)) ; true),
1416		FindInvViolations=1,
1417		(invariant_violated(ResID) -> true
1418		; find_invariant_violation_among_not_checked_nodes(ResID)),
1419		tcltk_execute_trace_to_node(ResID).
1420		search_among_existing_nodes(DEADLOCK,FindDeadlocks,_,_,_,_) :-
1421		FindDeadlocks=1,
1422	?	visited_expression_id(ResID),
1423		transitions_computed_for_node(ResID),
1424		is_deadlocked(ResID),
1425		(time_out_for_node(ResID)
1426		-> DEADLOCK = possible_deadlock_timeout
1427		; get_preference(store_only_one_incoming_transition,true) -> DEADLOCK = possible_deadlock
1428		; DEADLOCK = deadlock),
1429		print_message(deadlock_among_existing_nodes(ResID)),
1430		tcltk_execute_trace_to_node(ResID).
1431		search_among_existing_nodes(goal_found,_,_,FindGoal,_,_) :-
1432		FindGoal=1,
1433		%visited_expression(ResID,_CurState),
1434		%\+(not_all_transitions_added(ResID)), % if commented out: will also look at open nodes
1435		node_satisfies_goal(ResID),
1436		tcltk_execute_trace_to_node(ResID).
1437		search_among_existing_nodes(assertion_violation,_,_,_,FindAssViolations,_) :-
1438		FindAssViolations=1,
1439		b_machine_has_assertions,
1440	?	visited_expression(ResID,CurState),
1441		transitions_computed_for_node(ResID),
1442		state_violates_assertions(ResID,CurState),
1443		tcltk_execute_trace_to_node(ResID).
1444		search_among_existing_nodes(ERR,_,_,_,_,FindStateErrors) :- FindStateErrors=1,
1445		state_space:state_error(ResID,_,Error), Error \== invariant_violated,
1446		(Error = abort_error(ERR,_,_,_) -> true ; ERR = state_error(Error)),
1447		tcltk_execute_trace_to_node(ResID).
1448		search_among_existing_nodes(all,_,_,_,_,_).
1449
1450
1451		compute_all_transitions_if_necessary :-
1452		current_state_id(CurID),
1453		compute_all_transitions_if_necessary(CurID,false).
1454		:- public compute_all_transitions_if_necessary/1.
1455		compute_all_transitions_if_necessary(CurID) :-
1456		compute_all_transitions_if_necessary(CurID,false).
1457
1458		compute_all_transitions_if_necessary(CurID,CheckInvariant) :-
1459		(retract_open_node(CurID) % will assert not_invariant_checked
1460		-> set_context_state(CurID),
1461		% first check invariant, relevant if we want to use specialized_inv proof information
1462		visited_expression(CurID,State),
1463		% TO DO: this does not expand concrete_constants: the expansion may be done twice below:
1464		% once for compute_invariant (corresponds_to_b...) and once for compute_all_transitions (prepare_state_for_specfile_trans)
1465		prepare_state_for_specfile_trans(State,CurID,PreparedState),
1466		(CheckInvariant==true
1467		-> compute_invariant_if_necessary_and_requested(CurID,PreparedState) ; true),
1468		compute_all_transitions(CurID,PreparedState),
1469		clear_context_state
1470		; true).
1471		%compute_all_transitions_if_necessary(CurID,CurState) :-
1472		% ((not_all_transitions_added(CurID);not_interesting(CurID))
1473		% -> compute_all_transitions(CurID,CurState) ; true).
1474
1475
1476		compute_invariant_if_necessary_and_requested(ID,State) :-
1477		enter_new_error_scope(ErrScID,compute_invariant_if_necessary_and_requested), % here we setup a new error scope; see comment for force_check_invariantKO below
1478		compute_invariant_if_necessary(ID,State),
1479		exit_error_scope(ErrScID,_ErrOcc,compute_invariant_if_necessary_and_requested). % should we do something with error occured result ?
1480
1481		compute_invariant_if_necessary(ID,State) :-
1482		animation_mode(MODE),compute_invariant_if_necessary(ID,State,MODE).
1483		compute_invariant_if_necessary(ID,State,MODE) :-
1484		( check_invariantKO(MODE,ID,State) -> true ; true).
1485
1486		check_invariantKO(ID,State) :-
1487		animation_mode(MODE),check_invariantKO(MODE,ID,State).
1488		check_invariantKO(b,ID,State) :-
1489		check_invariantKO2(ID,State).
1490		check_invariantKO(csp_and_b,ID,State) :-
1491		check_invariantKO2(ID,State).
1492
1493
1494		check_invariantKO2(ID,_) :- invariant_violated(ID),!.
1495		check_invariantKO2(ID,CurState) :-
1496		set_invariant_checked(ID), % only succeeds if we haven't checked invariant for ID yet
1497		% print(check_inv(ID)),nl,
1498		%state_corresponds_to_initialised_b_machine(CurState,CurBState),
1499		state_corresponds_to_initialised_b_machine(CurState),
1500		( preferences:preference(do_invariant_checking,false) -> assertz(not_invariant_checked(ID))
1501		; force_check_invariantKO(ID,CurState)).
1502
1503
1504		force_check_invariantKO(ID,CurBState) :-
1505		% Note: this checks the invariant without setting up a new error scope
1506		% (Reason: in the model checker it would be relatively expensive to set up an error scope for each state
1507		% the model checker stops anyway when the first error is found and then exits its error scope)
1508		catch_clpfd_overflow_call_for_state(ID, 'checking invariants',
1509		b_state_violates_invariant(ID,CurBState),true) ->
1510		%(b_state_violates_invariant(ID,CurBState) ->
1511		set_invariant_violated(ID).
1512		% TO DO ?: call state_satisfies_negation_of_invariant if double_evaluation_when_analysing is true ?
1513
1514		% try and find an invariant violation among those nodes that have not yet been checked
1515		find_invariant_violation_among_not_checked_nodes(ID) :-
1516		retract(not_invariant_checked(ID)), %print(checking_invariant(ID)),nl,
1517		visited_expression(ID,State),
1518		state_corresponds_to_initialised_b_machine(State),
1519		prepare_state_for_specfile_trans(State,ID,CurBState),
1520		force_check_invariantKO(ID,CurBState).
1521
1522		:- use_module(probporsrc(ample_sets),[compute_ample_set2/3]).
1523		% computing ample sets (model_checker.pl)
1524		compute_ample_set(CurID,CurState,POROptions) :-
1525		catch_clpfd_overflow_call_for_state(CurID,'computing ample sets for POR',
1526		compute_ample_set2(CurID,CurState,POROptions),clear_context_state).
1527
1528
1529		%compute_all_transitions(CurID,CurState) :- get_preference(use_clpfd_solver,false),!,
1530		% compute_all_transitions2(CurID,CurState). % in principle this overflow cannot/should not happen with CLPFD FALSE
1531		% but no performance benefit can be measured by removing the catch
1532		compute_all_transitions(CurID,CurState) :-
1533		catch_clpfd_overflow_call_for_state(CurID,'computing all enabled transitions',
1534		compute_all_transitions2(CurID,CurState),clear_context_state).
1535
1536
1537		%catch_clpfd_overflow_call_for_state(_CurID, Call,_ExtraCleanUpCode) :-
1538		% preferences:preference(use_clpfd_solver,false),!, % Overflow should not occur
1539		% call(Call).
1540		:- use_module(clpfd_interface,[catch_clpfd_overflow_call2/2]).
1541		catch_clpfd_overflow_call_for_state(CurID, Context, Call,ExtraCleanUpCode) :-
1542		catch_clpfd_overflow_call2(Call,
1543		( store_state_error(CurID,clpfd_overflow_error(Context),_),
1544		call(ExtraCleanUpCode)) ).
1545
1546
1547
1548
1549		:- use_module(probsrc(succeed_max),[reset_max_reached/0,max_reached/0, max_reached/1]).
1550		compute_all_transitions2(CurID,CurState) :- /* compute all outgoing transitions for a given node */
1551		% set_context_state(CurID), % error_context is set for each operation below anyway.
1552		reset_max_reached,
1553		prepare_state_for_specfile_trans(CurState,CurID,PreparedCurState), % will perform unpacking of constants just once, for example
1554		((time_out_preference_disabled % e.g., when using probcli -disable_time_out
1555		; use_no_timeout(CurID))
1556		-> add_transitions_fail_loop(CurID,PreparedCurState)
1557		; preferences:preference(time_out,CurTO),
1558		add_transitions__with_timeout_fail_loop(CurID,PreparedCurState,CurTO)
1559		),
1560		add_partial_transitions(CurID,PreparedCurState), % also copies unsat component infos
1561		(max_reached -> assert_max_reached_for_node(CurID),MaxReached=true ; MaxReached=false),
1562		% TO DO: use max_reached(OpID)
1563		(CurID==root -> save_constants(MaxReached) ; add_new_transitions_to_cache(CurID))
1564		. %,clear_context_state.
1565
1566		:- use_module(error_manager,[get_virtual_time_out_from_exception/2]). % used by time_out_with_enum_warning_for_findall
1567		% loop to compute successor states without a time_out
1568		add_transitions_fail_loop(CurID,CurState) :-
1569		catch(
1570		add_transitions_fail_loop2(CurID,CurState,TimeOutRes),
1571		Exc,
1572		get_virtual_time_out_from_exception(Exc,TimeOutRes)),
1573		(nonvar(TimeOutRes)
1574		-> assert_time_out_for_node(CurID,'unspecified_operation',TimeOutRes)
1575		; true).
1576
1577		add_transitions_fail_loop2(CurID,CurState,_) :-
1578		possible_trans_name_for_successors(CurState,ActionName),
1579		% we could check pge info here (e.g., store one Predecessor ID and look if ActionName can be enabled after)
1580		set_error_context(operation(ActionName,CurID)),
1581		add_transition(CurID,CurState,ActionName,_NewId), % TO DO: transmit animation_mode value?
1582		fail.
1583		add_transitions_fail_loop2(_,_,TimeOutRes) :-
1584		(enumeration_warning_occured_in_error_scope
1585		-> (virtual_time_out_occured_in_error_scope(TimeOutRes)
1586		-> true % i.e., critical enumeration warning occured
1587		; true),
1588		clear_enumeration_warnings
1589		; true % no warnings: sunshine case
1590		),
1591		clear_error_context.
1592
1593		possible_trans_name_for_successors(CurState,ActionName) :-
1594	?	specfile_possible_trans_name_for_successors(CurState,ActionName),
1595		(preference(store_only_one_incoming_transition,true), % SAFETY_MODEL_CHECK
1596		nonvar(ActionName),
1597		b_or_z_mode,
1598		b_operation_cannot_modify_state(ActionName) % we have a skip operation
1599		-> operation_not_yet_covered(ActionName)
1600		% if operation covered: all we could is create a self-loop, which would not be added to the state space anyway
1601		; true).
1602
1603
1604		:- use_module(library(timeout),[time_out/3]).
1605		my_timeout_test(1000000) :- write('.'), !, my_timeout_test(0).
1606		my_timeout_test(X) :- X1 is X+1, my_timeout_test(X1).
1607		:- public my_timeout_test/0.
1608		my_timeout_test :- time_out(my_timeout_test(0),500,TO), nl,
1609		print(time_out_result(TO)),nl, TO==time_out.
1610		:- assert_must_succeed(tcltk_interface:my_timeout_test).
1611
1612		add_transitions__with_timeout_fail_loop(CurID,CurState,CurTO) :-
1613		enter_new_error_scope(Level,add_transitions__with_timeout_fail_loop),
1614		call_cleanup(add_transitions__with_timeout_fail_loop2(Level,CurID,CurState,CurTO),
1615		exit_error_scope(Level,_,add_transitions__with_timeout_fail_loop)).
1616
1617		% old profiler
1618		:- use_module(runtime_profiler,[profile_failure_driven_loop/2]).
1619
1620		% the loop to compute all successors of state CurID with a time-out
1621		add_transitions__with_timeout_fail_loop2(Level,CurID,CurState,CurTO) :- % statistics(runtime,_),
1622		% TO DO: prepare computing the state: expanding const and vars, unpacking, ...
1623	?	possible_trans_name_for_successors(CurState,ActionName),
1624		profile_failure_driven_loop(ActionName,CurID),
1625		% Note: we enumerate possible transition names so that we can catch the time-out per name !
1626		% statistics(runtime,[T1,DeltaT]), print(delta_time(ActionName,DeltaT)),nl, %%
1627		% first enumerate possible Operations/... to obtain timeout per operation/...
1628		% TO DO: divide CurTO by number of transitions ???
1629		% We could also decide to have one time-out per state, only if that one is triggered move to
1630		% finer-grained timeouts
1631		% For probcli ../prob_examples/public_examples/B/Benchmarks/Cruise_finite1.mch --model-check, there are 35360 calls to timeout/3 (one per state the model checker reached and per transition group), with -disable-timeout none
1632		% In SICS 4.3.5 the runtime increased from 1.480 to 2.270 seconds = 0.022 ms per timeout call
1633		% In SICS 4.4.1 the runtime increased from 1.494 to 3.033 seconds. = 0.044 ms per timeout call.
1634		%% statistics(runtime,[T1,_]), print(try(ActionName,T1)),nl,%%
1635		set_error_context(operation(ActionName,CurID)),
1636	?	time_out_with_enum_warning_for_findall_in_current_error_scope(Level,
1637		add_transition(CurID,CurState,ActionName,_NewId),CurTO,TimeOutRes),
1638		%% statistics(runtime,[T2,_]), TDiff is T2-T1, print(added_transition(CurID,ActionName,TDiff,TimeOutRes)),nl, %%
1639		%% add_transition(CurID,CurState,ActionName,_NewId) ,
1640		((TimeOutRes==time_out ; nonvar(TimeOutRes),TimeOutRes=virtual_time_out(_), \+ max_reached(ActionName))
1641		% virtual time outs not relevant if we have already stopped earlier anyway; TO DO: does not seem to work for INITIALISATION
1642		-> (TimeOutRes=virtual_time_out(_) -> true
1643		; print_message('TIME OUT: '),print_message(CurID),
1644		print_message(CurTO),print_message(ActionName)
1645		),
1646		(var(ActionName)
1647		-> assert_time_out_for_node(CurID,'unspecified_operation',TimeOutRes)
1648		; assert_time_out_for_node(CurID,ActionName,TimeOutRes)) % TO DO: assert info per ActionSkeleton ?
1649		; true
1650		),fail.
1651		add_transitions__with_timeout_fail_loop2(_,_,_,_) :- clear_error_context.
1652		% statistics(runtime,[_,DeltaT]), print(delta_time(end,DeltaT)),nl.
1653
1654		% compute and add transition to next states
1655		add_transition(CurID,CurState,ActionName,NewId) :-
1656		/* ActionName maybe pre-instantiated */
1657		extract_infos_from_prepared_state(CurState,PrecomputedInfos),
1658	?	specfile_trans(CurState,ActionName,Act,NewExpression,TransInfo,Residue),
1659		%% print_bt_message(specfile_trans(CurState,ActionName,Act,NewExpression,TransInfo,Residue)), %%
1660		add_trans_id_with_infos(CurID,PrecomputedInfos,Act,NewExpression,Residue,NewId,TransInfo,_).
1661
1662
1663		% after being computed, add a new transition in the state space; adding the destination state if required
1664		add_trans_id_with_infos(CurID,PrecomputedInfos,Act,NewExpression,Residue,NewID,TransInfo,TransId) :-
1665		(Residue=[] -> true
1666		; add_error(add_trans_id,'Residue: ',CurID:Act:Residue),
1667		tools_printing:print_goal(Residue),nl
1668		),
1669		add_new_transition_transid_with_infos(CurID,PrecomputedInfos,Act,NewID,NewExpression,TransInfo,TransId).
1670
1671		add_trans_id(CurID,Act,NewExpression,NewID,TransId) :-
1672		add_trans_id_with_infos(CurID,[],Act,NewExpression,[],NewID,[],TransId).
1673
1674		add_partial_transitions(root,CurState) :-
1675		/* for the moment the only state where partial transitions are computed */
1676	?	\+ any_transition(root,_,_), /* adding normal transitions was not successful */
1677		partial_trans(CurState,Act,NewExpression,Residue),
1678		add_trans_id_with_infos(root,[],Act,NewExpression,Residue,_NewID,[],_),fail.
1679		add_partial_transitions(_CurID,_).
1680
1681		/* --------------------------------------------------------------------- */
1682
1683		/* A bit like AO* algorithm: expands open nodes (i.e., states whose transitions
1684		have not yet been computed */
1685
1686		:- use_module(model_checker).
1687
1688		tcltk_model_check(Nr,TclTkRes,FindDeadlocks,FindInvViolations,FindGoal,FindAssViolations,
1689		FindStateErrors,StopFullCoverage,PartialOrderReduction,PartialGuardsEvaluation,TIMELIMIT,TotalTime) :-
1690		statistics(walltime,[CurTime,_]), /* get current time in ms */
1691		LimitTime is CurTime+TIMELIMIT,
1692		%debug_println(10,start_tcltk_model_check(Nr,TIMELIMIT)),
1693		InspectExistingNodes = 0,
1694		(do_model_check(Nr,_A,LimitTime,Res,FindDeadlocks,FindInvViolations,FindGoal,
1695		FindAssViolations,FindStateErrors,StopFullCoverage,
1696		PartialOrderReduction,PartialGuardsEvaluation,InspectExistingNodes)
1697		-> translate_error_for_tclk(Res,TclTkRes)
1698		; add_internal_error('Call failed: ',do_model_check(Nr,_A,LimitTime,Res,FindDeadlocks,FindInvViolations,FindGoal,
1699		FindAssViolations,FindStateErrors,StopFullCoverage,
1700		PartialOrderReduction,PartialGuardsEvaluation,InspectExistingNodes)),
1701		TclTkRes=error),
1702		statistics(walltime,[CurTime2,_]),
1703		TotalTime is CurTime2-CurTime,
1704		debug_println(10,tcltk_model_check(Nr,TotalTime,Res)).
1705
1706		translate_error_for_tclk([timeout,Nr],Res) :- !, Res=[timeout,Nr].
1707		translate_error_for_tclk(state_error(S),String) :- !, translate_state_err_for_tcltk(S,String).
1708		translate_error_for_tclk(S,R) :- atomic(S),!,R=S.
1709		translate_error_for_tclk(S,R) :- nonvar(S), add_error(translate_error_for_tclk,'Unknown Model Check result: ',S), R=unknown.
1710
1711		translate_state_err_for_tcltk(abort_error(TYPE,_,_,_),ERR) :- !, ERR = TYPE.
1712		translate_state_err_for_tcltk(eventerror(Event,Error,_),ERR) :- !,
1713		functor(Error,F,_),
1714		ajoin(['event_error:',Event,':',F],ERR).
1715		translate_state_err_for_tcltk(Error,ERR) :-
1716		functor(Error, StateError, _), atom_concat('state_error:',StateError,ERR).
1717
1718
1719
1720		do_model_check(_Nr,NodesAnalysed,_LimitTime,Res,FindDeadlocks,FindInvViolations,FindGoal,
1721		FindAssViolations,FindStateErrors,_StopFullCoverage,
1722		_PartialOrderReduction,_PartialGuardsEvaluation,ForceInspectExistingNodes) :-
1723		(tcltk_state_space_only_has_root_node -> true % Then also look at the root node
1724		; ForceInspectExistingNodes == 1),
1725		search_among_existing_nodes(Res,FindDeadlocks,FindInvViolations,FindGoal,
1726		FindAssViolations,FindStateErrors),
1727		Res \=all, NodesAnalysed=0.
1728		do_model_check(LimitNr,NodesAnalysed,LimitTime,Res,FindDeadlocks,FindInvViolations,FindGoal,
1729		FindAssViolations,FindStateErrors,StopFullCoverage,PartialOrderReduction,PartialGuardsEvaluation,_) :-
1730		update_ass(FindAssViolations,FindAssViolations2),
1731		open_search(LimitNr,NodesAnalysed,LimitTime,Res,FindDeadlocks,FindInvViolations,FindGoal,
1732		FindAssViolations2,FindStateErrors,StopFullCoverage,PartialOrderReduction,PartialGuardsEvaluation).
1733
1734		update_ass(1,FindAssViol) :- \+ b_machine_has_assertions,!, % no need to check assertions
1735		FindAssViol=0.
1736		update_ass(X,X).
1737
1738		/* --------------------------------------------------- */
1739
1740		/* constraint-based checking of refinements */
1741		:- use_module(symbolic_model_checker(cbc_refinement_checks), [cbc_refinement_check/2]).
1742		tcltk_cbc_refinement_check(list(List),ErrorOccured) :-
1743		cbc_refinement_check(List,ErrorOccured).
1744
1745		/* constraint-based/model search for invariant violations */
1746
1747		:- dynamic cbc_inv_error_found/2.
1748
1749		tcltk_constraint_based_check(L) :- tcltk_constraint_based_check(L,_).
1750		tcltk_constraint_based_check(list(List),ErrorsOrTimeoutWereFound) :-
1751		retractall(cbc_inv_error_found(_,_)),
1752		findall(Res, (tcltk_constraint_based_check_with_timeout(OpName,ErrorDesc),
1753		(ErrorDesc=ok -> true ; assertz(cbc_inv_error_found(OpName,ErrorDesc))),
1754		string_concatenate(' == ',ErrorDesc,Res1),
1755		string_concatenate(OpName,Res1,Res)), List),
1756		%%print(list(List)),nl, %%
1757		(cbc_inv_error_found(_,_) ->
1758		(cbc_inv_error_found(_,X),X\=time_out
1759		-> ErrorsOrTimeoutWereFound=true ; ErrorsOrTimeoutWereFound=time_out
1760		)
1761		; ErrorsOrTimeoutWereFound = false).
1762
1763		% can also be called with uninstantiated OpName
1764		tcltk_constraint_based_check_with_timeout(OpName,ErrorDesc) :-
1765		preferences:get_computed_preference(debug_time_out,DebugTimeOut),
1766		valid_operation_or_init(OpName,IOpName),
1767		(time_out_with_enum_warning_one_solution(tcltk_constraint_based_check_op(IOpName,ErrorDesc),DebugTimeOut,TimeOutRes)
1768		-> (is_time_out_result(TimeOutRes)
1769		-> print_message('TIME OUT: '), print_message(OpName), print_message(DebugTimeOut),
1770		ErrorDesc = timeout
1771		; true
1772		)).
1773		valid_operation_or_init(OpName,R) :- OpName=='@INITIALISATION',!,R='$initialise_machine'.
1774		valid_operation_or_init(OpName,OpName) :- b_get_machine_operation(OpName,_,_,_).
1775		valid_operation_or_init('INITIALISATION','$initialise_machine'). % used e.g. in test 1821: -cbc INITIALISATION
1776
1777		tcltk_constraint_based_check_op(OpName,ErrorDesc) :-
1778		tcltk_constraint_based_check_op(OpName,invariant,ErrorDesc).
1779
1780		tcltk_constraint_based_check_op(TclOpName,InvOrAssertion,ErrorDesc) :-
1781		adapt_tcl_operation_name(TclOpName,OpName),
1782		tcltk_constraint_based_check_op2(OpName,InvOrAssertion,ErrorDesc).
1783
1784		% code below because names with $ cause problems in Tcl with eval
1785		adapt_tcl_operation_name(X,R) :- var(X),!,R=X.
1786		adapt_tcl_operation_name('@PROPERTIES','$setup_constants') :- !.
1787		adapt_tcl_operation_name('@INITIALISATION','$initialise_machine') :- !.
1788		adapt_tcl_operation_name(X,X).
1789
1790		% a version that allows either invariant or assertions check after an Operation OpName
1791		tcltk_constraint_based_check_op2(OpName,InvOrAssertion,ErrorDesc) :-
1792		call_cbc_command(state_model_check(OpName,InvOrAssertion,State,Operation,NewState)),!,
1793		%fd_copy_term(NewState,ResTempl,ResBody), print(ResTempl),print(ResBody),nl,
1794		%fd_copy_term(State,PriorTempl,PriorBody),
1795		tcltk_add_new_transition_transid(root,'$JUMP'(constraint_based_check),PriorID,State,[],TransId1),
1796		translate_event(Operation,Action),
1797		tcltk_add_new_transition_transid(PriorID,Operation,NewID,NewState,[],TransId2),
1798		set_current_state_id(NewID),
1799		reset_op_trace_ids,
1800		add_to_op_trace_ids(TransId1), add_to_op_trace_ids(TransId2),
1801		retractall(history(_)),
1802		retractall(forward_history(_)),
1803		assertz(history([PriorID,root])),
1804		ajoin([InvOrAssertion,'_violated_after(',Action,')'],ErrorDesc).
1805		tcltk_constraint_based_check_op2(_,_,'ok').
1806
1807
1808		% try to find constants, parameters that make a given trace feasible
1809		tcltk_cbc_find_trace(TraceToBeFound,Res) :-
1810		tcltk_cbc_find_trace(TraceToBeFound,'',first_solution,Res).
1811
1812		%:- public tcltk_cbc_find_invariant_violation/2.
1813		%tcltk_cbc_find_invariant_violation(TraceToBeFound,Res) :-
1814		% tcltk_cbc_find_trace(TraceToBeFound,'#not_invariant',first_solution,Res).
1815		% could also call tcltk_constraint_based_check_op('$initialise_machine',invariant,Res)
1816
1817		tcltk_cbc_find_trace(TraceToBeFound,TargetPredString,FindAll,Res) :-
1818		b_parse_optional_machine_predicate(TargetPredString,TargetPred),
1819		formatsilent('Looking for solution for trace ~w~n',[TraceToBeFound]),
1820		split_atom(TraceToBeFound,[',',';',' '],TraceAsList),
1821		(maplist(check_valid_operation,TraceAsList)
1822		-> start_ms_timer(Timer),
1823		tcltk_cbc_find_trace_aux(Timer,TraceAsList,TargetPred,FindAll,Res)
1824		; Res = error).
1825		tcltk_cbc_find_trace_aux(Timer,TraceAsList,TargetPred,FindAll,Res) :-
1826		preferences:get_computed_preference(debug_time_out,DebugTimeOut),
1827		reset_nr_cbc_sols,
1828		time_out_with_enum_warning_one_solution(
1829		cbc_path_solver:create_testcase_path_nondet(init,TraceAsList,TargetPred,Transitions),DebugTimeOut,TimeOutRes),
1830		stop_ms_timer(Timer),
1831		(is_time_out_result(TimeOutRes)
1832		-> !,
1833		print_message('*** TIME OUT: '), print_message(DebugTimeOut), Res = time_out
1834		; FindAll = findall -> inc_nr_cbc_sols,
1835		print('% *** FOUND PATH: '), maplist(print_trans,Transitions),nl,
1836		fail % backtrack to find further solutions
1837		; !,Res = ok,
1838		print('% *** FOUND PATH: '), maplist(print_trans,Transitions),nl,
1839		maplist(extract_trans_id,Transitions,TransIds),
1840		set_trace_by_transition_ids(TransIds)
1841		).
1842		tcltk_cbc_find_trace_aux(Timer,_TraceToBeFound,_TargetPred,findall,R) :- !, stop_ms_timer(Timer),
1843		R=nr_cbc_sols(Res),
1844		nr_cbc_sols(Res),
1845		print_message('*** ALL SOLUTIONS FOUND ').
1846		tcltk_cbc_find_trace_aux(Timer,_TraceToBeFound,_TargetPred,_FindAll,no_solution_found) :-
1847		stop_ms_timer(Timer),
1848		print_message('*** NO SOLUTION FOUND'),nl.
1849
1850		:- dynamic nr_cbc_sols/1.
1851		nr_cbc_sols(0).
1852		reset_nr_cbc_sols :- retractall(nr_cbc_sols(_)), assertz(nr_cbc_sols(0)).
1853		inc_nr_cbc_sols :-
1854		retract(nr_cbc_sols(N)), N1 is N+1, assertz(nr_cbc_sols(N1)).
1855		extract_trans_id( (TransId,_,_,_), TransId).
1856		print_trans( (_,Event,_,_)) :- translate_event(Event,S), print(S), print(' ').
1857
1858		:- use_module(probsrc(tools_matching), [get_possible_top_level_event_matches_msg/2]).
1859		check_valid_operation(Op) :-
1860		(get_possible_language_specific_top_level_event(Op,_,_) -> true
1861		; (get_possible_top_level_event_matches_msg(Op,FMsg)
1862		-> ajoin(['Unknown operation/event (did you mean ',FMsg,' ?):'],Msg)
1863		; Msg='Unknown operation/event:'
1864		),
1865		add_error(cbc_find_sequence,Msg,Op),
1866		fail
1867		).
1868
1869
1870
1871		% ------------
1872
1873		:- use_module(bsyntaxtree).
1874		tcltk_constraint_find_valid_state_with_pred(ParameterBindList,RestPreCond,UseConstantsFromStateID) :-
1875		parse_tclk_parameter_values_and_pred('$initialise_machine',ParameterBindList,RestPreCond,CustomPredicate),
1876		UseInvariant=true,
1877		call_cbc_command(
1878		b_state_model_check:b_set_up_valid_state_with_pred(State,CustomPredicate,
1879		UseInvariant,UseConstantsFromStateID)),
1880		tcltk_add_cbc_state(State,find_valid_state).
1881		tcltk_constraint_find_valid_state :-
1882		call_cbc_command(b_set_up_valid_state(State)),
1883		tcltk_add_cbc_state(State,find_valid_state).
1884
1885		:- use_module(extrasrc(optimizing_solver),[b_set_up_maximally_valid_state/2]).
1886		tcltk_constraint_find_maximal_valid_state :-
1887		current_state_id(ID),
1888		call_cbc_command(b_set_up_maximally_valid_state(ID,State)),
1889		tcltk_add_cbc_state(State,find_maximal_valid_state).
1890
1891
1892		tcltk_constraint_find_dynamic_assertion_violation :-
1893		call_cbc_command(b_find_dynamic_assertion_violation(State)),
1894		tcltk_add_cbc_state(State,cbc_dynamic_assertions_check).
1895
1896		:- use_module(clpfd_interface,[catch_clpfd_overflow_call1/1]).
1897		:- use_module(error_manager,[call_in_fresh_error_scope_for_one_solution/1]).
1898		% catch CLPFD overflows and catch other errors
1899		call_cbc_command(Command) :-
1900		call_in_fresh_error_scope_for_one_solution(
1901		(catch_clpfd_overflow_call1(Command) -> true
1902		; translate_events_in_current_scope_to_warnings(cbc,'Warning: '),fail
1903		% Maybe we should raise error when Command fails and enumeration warnings are there ?
1904		)).
1905
1906
1907		tcltk_constraint_find_deadlock_state(Res) :-
1908		check_we_are_in_b_mode(cbc_deadlock_freedom_check),
1909		create_texpr(truth,pred,[],True),
1910		call_cbc_command(cbc_deadlock_freedom_check(State,True,0)),
1911		(State == time_out -> Res = time_out
1912		; tcltk_add_cbc_state(State,cbc_deadlock), Res=deadlock).
1913
1914		% if Filter=1 we remove guards which are inconsitent with goal
1915		tcltk_constraint_find_deadlock_state_with_goal(Filter,Res) :-
1916		check_we_are_in_b_mode(cbc_deadlock_freedom_check),
1917		(b_get_machine_goal(Goal) -> true ; create_texpr(truth,pred,[],Goal)),
1918		call_cbc_command(cbc_deadlock_freedom_check(State,Goal,Filter)),
1919		(State == time_out -> Res = time_out
1920		; tcltk_add_cbc_state(State,cbc_deadlock), Res=deadlock).
1921
1922		check_we_are_in_b_mode(_) :- b_or_z_mode,!.
1923		check_we_are_in_b_mode(Cmd) :- add_error(check_we_are_in_b_mode,'This command can only be performed in B,Z or TLA+ mode: ',Cmd),fail.
1924
1925		tcltk_constraint_find_deadlock_state_with_goal(true,_Filter,Res) :-
1926		!,tcltk_constraint_find_deadlock_state(Res).
1927		tcltk_constraint_find_deadlock_state_with_goal(GoalPred,Filter,Res) :-
1928		bmachine:b_set_machine_goal(GoalPred),
1929		tcltk_constraint_find_deadlock_state_with_goal(Filter,Res).
1930
1931		:- use_module(cbcsrc(enabling_analysis),[check_if_feasible_operation/5]).
1932		tcltk_check_if_feasible_operation(OpName,UseInvariant,TimeOutFactor,Result) :- % UseInvariant currently always 1 from Tcl
1933		check_if_feasible_operation(OpName,UseInvariant,TimeOutFactor,Result,ResultState),
1934		tcltk_add_cbc_state(ResultState,feasibility_check(OpName)).
1935
1936		% add a state found by constraint-based verification
1937		tcltk_add_cbc_state('$UNKNOWN_STATE',_) :- !.
1938		tcltk_add_cbc_state(State,OpName) :-
1939		seperate_state_into_const_and_vars(State,Constants,Variables),
1940		!,
1941		% store the constants separately: important for memory consumption when continuing animation/model checking
1942		tcltk_add_new_transition_transid(root,'$setup_constants',CstID,concrete_constants(Constants),[],TransId1),
1943		FullState = const_and_vars(CstID,Variables),
1944		% TODO: if Variables are [] we could simply create an initialisation transition
1945		tcltk_add_new_transition_transid(CstID,'$JUMP'(OpName),NewID,FullState,[],TransId2),
1946		set_cbc_state(NewID,[TransId1,TransId2],[CstID,root]).
1947		tcltk_add_cbc_state(State,OpName) :-
1948		tcltk_add_new_transition_transid(root,'$JUMP'(OpName),NewID,State,[],TransId),
1949		set_cbc_state(NewID,[TransId],[root]).
1950
1951		set_cbc_state(NewID,TransIds,His) :-
1952		set_current_state_id(NewID),
1953		reset_op_trace_ids,
1954		maplist(add_to_op_trace_ids,TransIds),
1955		retractall(history(_)),
1956		retractall(forward_history(_)),
1957		assertz(history(His)). %, print(State),nl.
1958
1959		is_constant_binding(SortedCsts,bind(ID,_)) :-
1960		ord_member(ID,SortedCsts).
1961
1962		:- use_module(bsyntaxtree, [get_texpr_ids/2]).
1963		seperate_state_into_const_and_vars(State,Constants,Variables) :-
1964		b_get_machine_constants(TCs), get_texpr_ids(TCs,Cs),
1965		sort(Cs,SortedCsts),
1966		include(is_constant_binding(SortedCsts),State,Constants),
1967		Constants \= [],
1968		exclude(is_constant_binding(SortedCsts),State,Variables).
1969
1970
1971
1972		tcltk_constraint_find_static_assertion_violation(TclResult) :-
1973		cbc_constraint_find_static_assertion_violation(Result,[]),
1974		functor(Result,TclResult,_).
1975		cbc_constraint_find_static_assertion_violation(Result,Options) :-
1976		call_cbc_command(cbc_static_assertions_check(State,Options)),
1977		( State = counterexample_found(CE) ->
1978		Result = counterexample_found,
1979		tcltk_add_cbc_state(CE,static_assertion_check)
1980		;
1981		Result = State).
1982
1983		/* --------------------------------------------------- */
1984
1985
1986		:- use_module(error_manager,[extract_all_line_col/5]).
1987		:- use_module(probcspsrc(haskell_csp),[extract_span_from_event/4,extract_span_info/2]).
1988
1989		get_source_text_positions(Event,Line,Col,EndLine,EndCol) :-
1990		extract_span_from_action(Event,SPAN),
1991		extract_all_line_col(SPAN,Line,Col,EndLine,EndCol).
1992
1993		extract_span_from_action(Event,Span) :- csp_mode,
1994		extract_span_from_event(Event,Span,_,_).
1995		extract_span_from_action(Event,Pos) :- b_or_z_mode,
1996		get_operation_name(Event,ID),
1997		b_get_machine_operation(ID,_Res,_TParas,_Body,_OType,Pos).
1998
1999
2000		/* -------------------------------------------------------------------- */
2001
2002		get_current_option_eventtrace(OptionNum,Trace) :-
2003		% the option number starts with 0 (coming from a TK listbox)
2004		current_options(ActionsAndIDs),
2005		nth0(OptionNum,ActionsAndIDs,(Id,_,_,_)),
2006		transition_info(Id,eventtrace(Trace)),!.
2007
2008
2009		tcltk_has_eventtrace(OptionNum) :-
2010		get_current_option_eventtrace(OptionNum,_Trace).
2011
2012		tcltk_show_eventtrace(OptionNum,Desc) :-
2013		get_current_option_eventtrace(OptionNum,Trace),
2014		explain_event_trace(Trace,Desc,_Span).
2015
2016
2017
2018		/* --------------------------------------------------- */
2019
2020		:- use_module(prob2_interface,[execute_model/5]).
2021
2022		tcltk_execute_model(MaxNrSteps,ExecutedSteps,Result) :-
2023		current_state_id(CurID),
2024		execute_model(CurID,MaxNrSteps,_TransitionInfo,ExecutedSteps,Result).
2025
2026
2027		tcltk_find_shortest_trace_to_current_node(list(StringList)) :-
2028		find_trace_to_current_node(OpL),
2029		translate_events(OpL,StringList).
2030
2031
2032		tcltk_execute_trace_to_current_node :-
2033		current_state_id(CurID),
2034		tcltk_execute_trace_to_node(CurID).
2035
2036		tcltk_execute_trace_to_node(ToID) :- /* can be useful for TestCase Generation */
2037		set_target_id(ToID),
2038		tcltk_execute_trace_from_to_found_predicate(root,_,_).
2039
2040		% execcute longest loop-free trace (no repeated state)
2041		tcltk_execute_longest_trace_from(From) :-
2042		set_longest_trace_target,
2043		tcltk_execute_trace_from_to_found_predicate(From,_,_).
2044
2045		% OpL is list of operation ids, IDList is list of state ids
2046		tcltk_execute_trace_from_to_found_predicate(From,OpL,IDList) :-
2047		debug_println(19,finding_trace_from_to(From)), flush_output(user),
2048		find_shortest_path_from_to_found_predicate(From,OpL,IDList,ToID), !,
2049		(current_state_id(From) -> true ; state_space_reset),
2050		debug_println(9,executing_trace(From,OpL,ToID)), flush_output(user),
2051		execute_id_trace_from_current(ToID,OpL,IDList).
2052
2053
2054		find_trace_to_current_node(Trace) :-
2055		current_state_id(CurID),
2056		find_shortest_path_from_to(root,CurID,L,_),
2057		extract_term_trace_from_transition_ids(L,Trace).
2058
2059		:- use_module(state_space_dijkstra).
2060
2061		find_shortest_trace_to_node(FromID,ToID,OpIDListe,StateIDList) :-
2062		find_shortest_path_from_to(FromID,ToID,OpIDListe,StateIDList).
2063
2064
2065		/* --------------------------------------------------- */
2066
2067
2068
2069		tcltk_goto_a_non_deterministic_node(Msg) :- /* same transition leads to different resulting state */
2070		visited_expression_id(ID),
2071		external_functions:non_det_transition(ID,_OpName,TID1,TID2),
2072		tcltk_execute_trace_to_node(ID),
2073		transition(ID,Op1,TID1,ID1),
2074		transition(ID,_Op2,TID2,ID2),
2075		translate_event_with_src_and_target_id(Op1,ID,ID1,OpStr),
2076		ajoin(['Operation leads to at least two different states (ids ', ID1,', ',ID2,
2077		') for same arguments: ', OpStr], Msg).
2078
2079		tcltk_goto_a_non_deterministic_output_node(Msg) :- /* same transition leads to different outputs */
2080		visited_expression_id(ID),
2081		external_functions:non_det_output_transition(ID,_OpName,TID1,TID2),
2082		tcltk_execute_trace_to_node(ID),
2083		transition(ID,Op1,TID1,ID1),
2084		transition(ID,Op2,TID2,ID2),
2085		translate_event_with_src_and_target_id(Op1,ID,ID1,OpStr1),
2086		translate_event_with_src_and_target_id(Op2,ID,ID2,OpStr2),
2087		ajoin(['Operation has at least two different results for same arguments: ', OpStr1,
2088		'\n and ',OpStr2], Msg).
2089
2090		dif_ID(ID1,ID2) :- (number(ID1),number(ID2) -> ID2>ID1 ; ID1 \= ID2).
2091
2092		tcltk_goto_a_branching_node :- /* two different events/operations enabled */
2093		transition(ID,X,ID2), get_operation_name(X,NX),
2094		transition(ID,Y,ID3), dif_ID(ID2,ID3), get_operation_name(Y,NY), NX\=NY,
2095		print_message(found_branching_op(ID,NX,NY)),
2096		%tcltk_goto_state(find_branching_node,ID),
2097		tcltk_execute_trace_to_node(ID).
2098
2099		tcltk_goto_a_non_resetable_node :-
2100		find_resetable_nodes,
2101		visited_expression_id(ID),
2102		\+(resetable_node(ID)),
2103		\+(not_all_transitions_added(ID)), !,
2104		%tcltk_goto_state(find_non_resetable_node,ID).
2105		tcltk_execute_trace_to_node(ID).
2106
2107		operation_name_covered(OpName) :- operation_name_covered(OpName,_).
2108		operation_name_covered(OpName,Template) :- b_get_machine_operation(OpName,Results,Par,_),
2109		\+ operation_not_yet_covered(OpName),
2110		length(Par,Arity),
2111		functor(Op,OpName,Arity),
2112		(Results\=[] -> Template = '-->'(Op,_) ; Template = Op).
2113
2114		tcltk_goto_event_list_property_violation(Property,EventSelection,list(OperationList)) :-
2115		% first translate Tk EventSelection Number list into Events
2116		sap:get_selected_events(EventSelection,_AllEvents,OperationList),
2117		include(operation_name_covered,OperationList,_,EnabledOpList), % only keep operations that can be enabled anyway
2118		maplist(operation_name_covered,EnabledOpList,TemplateList), % replace by template
2119		print(find_property_violation_for_template(Property,TemplateList)),nl,
2120		visited_expression(ID,S), ID \= root, S\= concrete_constants(_),
2121		\+(not_all_transitions_added(ID)),
2122		\+( check_event_list_property(Property,ID,TemplateList) ),
2123		print(found_event_list_property_violation(Property,ID)),nl,
2124		tcltk_execute_trace_to_node(ID).
2125
2126		check_event_list_property(relative_deadlock_freedom,ID,TemplateList) :-
2127		relative_deadlock_freedom(ID,TemplateList).
2128		check_event_list_property(valid_controller,ID,TemplateList) :-
2129		is_valid_controller_state(ID,TemplateList).
2130		check_event_list_property(det_controller,ID,TemplateList) :-
2131		is_det_controller_state(ID,TemplateList).
2132
2133		relative_deadlock_freedom(ID,TemplateList) :- member(Template,TemplateList),
2134		transition(ID,Template,_).
2135		is_valid_controller_state(ID,TemplateList) :- % check that exactly one event from TemplateList is enabled
2136		append(_,[LiveEvent|RestTemplate],TemplateList),
2137		transition(ID,LiveEvent,_),!, % we found one enabled event
2138		\+ relative_deadlock_freedom(ID,RestTemplate). % all other events from list must be disabled
2139		is_det_controller_state(ID,TemplateList) :- % check that *at most* one event from TemplateList is enabled
2140		append(_,[LiveEvent|RestTemplate],TemplateList),
2141		transition(ID,LiveEvent,_),!, % we found one enabled event from list
2142		\+ relative_deadlock_freedom(ID,RestTemplate). % all other events from list must be disabled
2143		is_det_controller_state(_,_) :- true. % no event enabled is also ok
2144
2145
2146		tcltk_goto_state_enabling_operation(TclOpName,FromCurrent) :-
2147		adapt_tcl_operation_name(TclOpName,OpName),
2148		operation_name_covered(OpName,Template),
2149		set_found_predicate(ID, transition(ID,Template,_)),
2150		print(template(Template,FromCurrent)),nl,
2151		print_message('Computing trace to node'),
2152		(FromCurrent=1
2153		-> current_state_id(FromID) % inefficient: better to do one dijkstra from FromID !
2154		; FromID = root
2155		),
2156		tcltk_execute_trace_from_to_found_predicate(FromID,_,_).
2157		% tcltk_goto_state(find_enabled(OpName),ID).
2158
2159
2160		:- use_module(tools_lists,[count_occurences/2]).
2161		% quickly compute which operations have already been covered and which ones not
2162		tcltk_operations_covered_info(list([list(['Operation','Covered'])|OpCov]),list(Occurences),Precise) :-
2163		findall(list([OpName,Cov]),
2164		(specfile:get_possible_event(OpName),
2165		(operation_name_not_yet_covered(OpName)
2166		-> not_yet_covered_info(Precise,OpName,Cov)
2167		; Cov = 'yes')),OpCov),
2168		(maplist(get_cov,OpCov,Cov2),
2169		count_occurences(Cov2,Occ2),
2170		maplist(construct_list,Occ2,Occurences) -> true ; Occurences=[]).
2171
2172		get_cov(list([_,Cov|_]),Cov).
2173		construct_list(Kind-Nr,list([Kind,Nr])).
2174
2175		:- use_module(cbcsrc(enabling_analysis),[feasible_operation/2]).
2176		not_yet_covered_info(precise,OpName,Cov) :-
2177		feasible_operation(OpName,Res),!, Res=Cov.
2178		not_yet_covered_info(precise,_,R) :- !, R='unknown'.
2179		not_yet_covered_info(_,_,'uncovered').
2180
2181		:- dynamic resetable_node/1.
2182
2183		resetable_node(a).
2184
2185		:- public find_resetable_nodes/0.
2186		:- dynamic find_flag/2.
2187		find_resetable_nodes :-
2188		retractall(find_flag(_,_)),
2189		retractall(resetable_node(_)),
2190		any_transition(root,_,ID), /* add nodes reachable from root */
2191		assertz(find_flag(ID,0)),
2192		fail.
2193		find_resetable_nodes :-
2194		visited_expression(CID,concrete_constants(_C)),
2195		any_transition(CID,_,ID), /* add nodes reachable after a setup_constants */
2196		assertz(find_flag(ID,0)),
2197		fail.
2198		find_resetable_nodes :- find_resetable_nodes_loop,
2199		print_message('Not resetable:'),
2200		visited_expression_id(ID),
2201		\+(resetable_node(ID)),
2202		print_message(ID),
2203		fail.
2204		find_resetable_nodes :-
2205		print_message('Done').
2206
2207
2208		find_resetable_nodes_loop :-
2209		retract(find_flag(ID,N)), !, find_resetable_nodes_loop(ID,N).
2210		find_resetable_nodes_loop.
2211
2212		find_resetable_nodes_loop(ID,N) :- N1 is N+1,
2213		assertz(resetable_node(ID)),
2214		any_transition(NewID,_,ID),
2215		\+(resetable_node(NewID)),
2216		\+(find_flag(NewID,_)),
2217		assertz(find_flag(NewID,N1)),
2218		fail.
2219		find_resetable_nodes_loop(_,_) :- find_resetable_nodes_loop.
2220
2221
2222		:- use_module(specfile, [get_current_state_for_b_formula/2]).
2223
2224		tcltk_show_expression_as_dot(VorE,File) :-
2225		parse_machine_expression(VorE,TypedExpr),
2226		tcltk_show_typed_expression_as_dot_graph(TypedExpr,File).
2227		tcltk_show_expression_as_dot(_VorE,File) :-
2228		add_error(tcltk_show_expression_as_dot,'Computing Value Dot Representation Failed for: ',File),
2229		fail.
2230
2231		:- use_module(dotsrc(state_as_dot_graph),[print_cstate_graph/2]).
2232		:- use_module(dotsrc(state_custom_dot_graph),[tcltk_generate_state_custom_dot_graph_for_expr/2, is_valid_custom_dot_graph_record/1]).
2233
2234		tcltk_show_typed_expression_as_dot_graph(TypedExpr,File) :-
2235		is_valid_custom_dot_graph_record(TypedExpr),
2236		!, % use the more powerful custom_dot_graph mechanism
2237		tcltk_generate_state_custom_dot_graph_for_expr(TypedExpr,File).
2238		tcltk_show_typed_expression_as_dot_graph(TypedExpr,File) :-
2239		get_current_state_for_b_formula(TypedExpr,BState),
2240		extend_state_with_probids_and_lets(BState,BState1),
2241		decompose_expression_for_dot(TypedExpr,ExprList,[]), % decompose pairs so that user can provide multiple values/graphs
2242		compute_for_dot(ExprList,BState1,GraphState), % compute value for each sub-component
2243		format('Writing value to DOT file: ~w~n',[File]),
2244		print_cstate_graph(GraphState,File),
2245		format('Finished writing value to DOT file: ~w~n',[File]).
2246
2247
2248		:- use_module(bmachine, [b_parse_machine_expression_from_codes_with_prob_ids/2, type_with_errors/4]).
2249		parse_machine_expression(RawAST,TypedExpr) :- compound(RawAST),!, % allow to pass raw AST as well
2250		extend_typing_scope_for_stored_lets([prob_ids(visible),variables,external_library(safe_available_libraries)],Scope),
2251		type_with_errors(RawAST,Scope,Type,TypedExpr),
2252		% TODO: get_stored_let_typing_scope and add values to state returned by get_current_state_for_b_formula
2253		((Type=pred ; Type=subst)
2254		-> add_error(parse_machine_expression,'Expected expression formula but obtained: ',Type),fail
2255		; true ).
2256		parse_machine_expression(VorE,TypedExpr) :-
2257		atom_codes(VorE,VorECodes),
2258		b_parse_machine_expression_from_codes_with_prob_ids(VorECodes,TypedExpr).
2259
2260		compute_for_dot([],_,[]).
2261		compute_for_dot([String,TypedExpr|Tail],BState,[bind(Str,Value)|TS]) :-
2262		% allow user to specify labels for graphs ("lbl1", e1, "lbl2", e2, ...)
2263		get_texpr_expr(String,string(Str)),!,
2264		translate:translate_bexpression_with_limit(TypedExpr,100,EStr),
2265		format('Computing value for expression: ~w~n',[EStr]),
2266		b_compute_expression_with_prob_ids(TypedExpr,BState,Value),
2267		compute_for_dot(Tail,BState,TS).
2268		compute_for_dot([TypedExpr|Tail],BState,[bind(Str,Value)|TS]) :-
2269		translate:translate_bexpression_with_limit(TypedExpr,100,Str),
2270		format('Computing value for expression: ~w~n',[Str]),
2271		b_compute_expression_with_prob_ids(TypedExpr,BState,Value),
2272		compute_for_dot(Tail,BState,TS).
2273
2274		:- use_module(bsyntaxtree, [replace_ids_by_exprs/4]).
2275
2276		% decompose_expression_for_dot ensures that
2277		% ("label1",graph1,"lbl2",graph2) or rec(label:graph) is decomposed and we can associate labels with multiple graphs
2278		decompose_expression_for_dot(b(couple(A,B),_,_)) --> !,
2279		decompose_expression_for_dot(A), decompose_expression_for_dot(B).
2280		decompose_expression_for_dot(b(rec(Fields),_,_)) --> !,decompose_fields_for_dot(Fields).
2281		decompose_expression_for_dot(b(let_expression(Ids,Exprs,Body),couple(_,_),_)) --> !,
2282		% this can happen when OPTIMIZE_AST is set to FALSE and the Jupyter kernel adds LETs; lift string out of let
2283		% :dot expr_as_graph ("h",h,"hh",(h;h))
2284		{replace_ids_by_exprs(Body,Ids,Exprs,Body2)},
2285		decompose_expression_for_dot(Body2).
2286		decompose_expression_for_dot(X) --> [X].
2287
2288
2289		decompose_fields_for_dot([]) --> [].
2290		decompose_fields_for_dot([field(Name,Val)|T]) --> [b(string(Name),string,[]),Val], decompose_fields_for_dot(T).
2291
2292		/* ------------------------------------------------------------------ */
2293
2294		% aka Execute by Predicate
2295		tcltk_add_user_executed_operation(TclOpName,CustomPredicate) :-
2296		tcltk_add_user_executed_operation(TclOpName,[],CustomPredicate).
2297
2298		tcltk_add_user_executed_operation(TclOpName,ParameterBindList,RestPreCond) :-
2299		adapt_tcl_operation_name(TclOpName,OpName),
2300		parse_tclk_parameter_values_and_pred(OpName,ParameterBindList,RestPreCond,CustomPredicate),
2301		current_state_id(CurID),
2302		b_trans_one_solution_with_pred(OpName,CustomPredicate,CurID,_,_,_).
2303
2304		parse_tclk_parameter_values_and_pred(OpName,ParameterBindList,RestPreCond,CustomPredicate) :-
2305		GenParseErrors=true, ExtraScope=[],
2306		b_parse_machine_operation_pre_post_predicate(RestPreCond,ExtraScope,RestTypedPred,OpName,GenParseErrors),
2307		get_animation_operation_parameters(OpName,Parameters),
2308		% print(tcltk_add_user_executed_operation(OpName,ParameterBindList,Parameters)),nl,
2309		parse_parameter_values(ParameterBindList,Parameters,List),
2310		conjunct_predicates([RestTypedPred|List],CustomPredicate).
2311
2312		:- use_module(bmachine,[b_get_machine_operation_for_animation/7]).
2313		get_animation_operation_parameters('$setup_constants',Parameters) :-
2314		b_get_machine_operation_typed_parameters('$setup_constants',Parameters).
2315		get_animation_operation_parameters(OpName,FullParameters) :-
2316		TopLevel=true, % otherwise ANY parameters not added when show_eventb_any_arguments is true
2317		b_get_machine_operation_for_animation(OpName,_Results,Parameters,_Body,_OType,TopLevel,_OpPos),
2318		b_get_operation_non_det_modifies(OpName,NonDetVars), % also allow setting non-deterministically assigned vars
2319		b_get_machine_variables(Vars),
2320		include(non_det_modified(NonDetVars),Vars,ParaVars),
2321		append(ParaVars,Parameters,FullParameters).
2322
2323		non_det_modified(NonDetVars,TID) :- get_texpr_id(TID,ID), ord_member(ID,NonDetVars).
2324
2325		% parse a list of variable names and expressions and turn into equal predicates
2326		% Motivation: this can also deal with Z-style identifiers like in?, ... which cannot be parsed
2327		:- use_module(btypechecker, [unify_types_strict/2]).
2328		parse_parameter_values([],_,Res) :- !,Res=[].
2329		parse_parameter_values(['='(ParameterID,ExpressionStr)|T],Parameters,[Pred|PT]) :-
2330		atom_codes(ExpressionStr,Codes),
2331		format('Parsing for parameter ~w : ~w~n',[ParameterID,ExpressionStr]),
2332		!,
2333		b_parse_machine_expression_from_codes_with_prob_ids(Codes,TypedExpr),
2334		get_texpr_type(TypedExpr,Type),
2335		TID = b(identifier(ParameterID),Type,[]),
2336		(member(b(identifier(ParameterID),Type2,_),Parameters)
2337		-> (unify_types_strict(Type,Type2)
2338		-> Pred = b(equal(TID,TypedExpr),pred,[]),
2339		translate:print_bexpr(Pred),nl,
2340		parse_parameter_values(T,Parameters,PT)
2341		;
2342		pretty_type(Type,String1), pretty_type(Type2,String2),
2343		ajoin(['Value for parameter ',ParameterID,' has unexpected type ',String1,', expected: '],Msg),
2344		add_error(parse_parameter_values,Msg,String2),
2345		fail
2346		)
2347		; add_error(parse_parameter_values,'Unknown operation parameter: ',ParameterID),
2348		fail).
2349		parse_parameter_values(PB,P,_) :- add_internal_error('Illegal parameter binding: ',parse_parameter_values(PB,P,_)),fail.
2350
2351
2352		% just as above but with typed predicate
2353		tcltk_add_user_executed_operation_typed(OpName,Operation,TypedCustomPredicate,NewID) :-
2354		current_state_id(CurID),
2355		tcltk_add_user_executed_operation_typed(OpName,CurID,Operation,TypedCustomPredicate,_,NewID).
2356		tcltk_add_user_executed_operation_typed(OpName,CurID,Operation,TypedCustomPredicate,TransID,NewID) :-
2357		b_trans_one_solution_with_pred(OpName,TypedCustomPredicate,CurID,Operation,TransID,NewID).
2358
2359		% allows the user to arbitrarily change variable values
2360		% Attention: this can of course violate the invariant
2361		tcltk_add_user_modify_variable_transition(VarID,ValueStr) :-
2362		current_state_id(CurID),
2363		tcltk_add_user_modify_variable_transition(CurID,VarID,ValueStr,_).
2364		tcltk_add_user_modify_variable_transition(CurID,VarID,ValueStr,NewID) :-
2365		get_id_type(VarID,Kind,Type),!,
2366		format('Trying to update ~w ~w to new value: ~w~n',[Kind,VarID,ValueStr]),
2367		eval_string_in_cur_state(ValueStr,ValTyped,Value),
2368		get_texpr_type(ValTyped,ValType),
2369		check_types(Kind,VarID,Type,ValType),
2370		visited_expression(CurID,CurState),
2371		update_variable(CurState,VarID,Value,NewState),
2372		Residue=[], TransInfo=[],
2373		Operation = '$modify'(string(VarID),string(ValueStr)),
2374		add_trans_id_with_infos(CurID,[],Operation,NewState,Residue,NewID,TransInfo,_),
2375		tcltk_goto_state(Operation,NewID).
2376
2377		check_types(_,_,Type,ValType) :-
2378		unify_types_strict(Type,ValType),!.
2379		check_types(Kind,VarID,Type,ValType) :-
2380		pretty_type(ValType,VTS), pretty_type(Type,TS),
2381		ajoin(['Unexpected type of value (', VTS, ' instead of ',TS,') for ',Kind,' :'],Msg),
2382		add_error(check_types,Msg,VarID),
2383		fail.
2384
2385		:- use_module(bmachine,[b_is_variable/2, b_is_constant/2]).
2386		get_id_type(ID,variable,Type) :- b_is_variable(ID,Type).
2387		get_id_type(ID,constant,Type) :- b_is_constant(ID,Type).
2388		% update variable value or constant value in concrete_constants state
2389		update_variable([],VarID,_,[]) :- add_error(update_variable,'Identifier does not exist in state:',VarID),fail.
2390		update_variable([bind(VarID,_)|T],VarID,NewVal,Res) :- !, Res = [bind(VarID,NewVal)|T].
2391		update_variable([H|T],VarID,NewVal,[H|UT]) :- !, update_variable(T,VarID,NewVal,UT).
2392		update_variable(const_and_vars(ConstID,Old),VarID,NewVal,const_and_vars(ConstID,New)) :- !,
2393		update_variable(Old,VarID,NewVal,New).
2394		update_variable(concrete_constants(Old),VarID,NewVal,concrete_constants(New)) :- !,
2395		update_variable(Old,VarID,NewVal,New). % here we allow updating constants
2396
2397		% execute operation by predicate finding just one solution
2398		b_trans_one_solution_with_pred(OpName,TypedCustomPredicate,CurID,Operation,TransId,NewID) :-
2399		catch(
2400		(
2401		call_cleanup(b_trans_one_solution_with_pred2(OpName,TypedCustomPredicate,CurID,Operation,TransId,NewID),
2402		bmachine:reset_temp_predicate)
2403		),
2404		enumeration_warning(Cause,_,_,_,_),
2405		(
2406		add_warning(b_trans_one_solution_with_pred,
2407		'Enumeration warning prevented finding solution for operation: ',Cause),
2408		fail
2409		)
2410		).
2411
2412		% find one solution from current state using OpName and respecting temp_predicate
2413		b_trans_one_solution_with_pred2(OpName,TypedCustomPredicate,CurID,Operation,TransId,NewID) :-
2414		b_top_level_operation(OpName),
2415		!,
2416		visited_expression(CurID,InState),
2417		set_context_state(CurID,b_trans_one_solution_with_pred),
2418		debug_format(19,'Executing ~w in state ~w by predicate~n',[OpName,CurID]),
2419		call_cleanup(execute_operation_by_predicate_in_state(InState,OpName,TypedCustomPredicate,Operation,NewState),
2420		clear_context_state),
2421		!,
2422		debug_format(19,'Executed by predicate: ~w~n',[OpName]),
2423		%debug_format(19,'Executed ~w: ~w~nOut=~w~n',[OpName,Operation,NewState]),
2424		add_trans_id(CurID,Operation,NewState,NewID,TransId),
2425		tcltk_goto_state(Operation,NewID).
2426		b_trans_one_solution_with_pred2(OpName,TypedCustomPredicate,CurID,Operation,TransId,NewID) :-
2427		assert_temp_predicate_with_prob_def_set_elements(TypedCustomPredicate),
2428		visited_expression(CurID,InState),
2429		set_context_state(CurID,b_trans_one_solution_with_pred),
2430		temporary_set_preference(maxNrOfEnablingsPerOperation,1,Max),
2431		temporary_set_preference(maxNrOfInitialisations,1,MaxI),
2432		start_ms_timer(Timer),
2433		call_cleanup((specfile:b_trans(InState,OpName,Operation,NewState,TransInfo) -> true),
2434		(stop_ms_timer(Timer),
2435		reset_temporary_preference(maxNrOfEnablingsPerOperation,Max),
2436		reset_temporary_preference(maxNrOfInitialisations,MaxI),
2437		clear_context_state)
2438		),
2439		debug_println(9,found_solution(NewState)),nl,
2440		% now add a transition to the state space:
2441		Residue=[],
2442		add_trans_id_with_infos(CurID,[],Operation,NewState,Residue,NewID,TransInfo,TransId),
2443		tcltk_goto_state(Operation,NewID).
2444
2445		:- use_module(b_global_sets,[inline_prob_deferred_set_elements_into_bexpr/2]).
2446		assert_temp_predicate_with_prob_def_set_elements(CustomPredicate) :-
2447		inline_prob_deferred_set_elements_into_bexpr(CustomPredicate,CompiledPred),
2448		bmachine:assert_temp_typed_predicate(CompiledPred).
2449
2450
2451		% allow user to execute any statement
2452		% TO DO: catch operation_calls and route them differently
2453		% translate operation_call arguments into predicate and call tcltk_add_user_executed_operation_typed(OpName,Operation,TypedCustomPredicate,NewID)
2454		tcltk_add_user_executed_statement(Statement,Updates,NewID) :-
2455		current_expression(CurID,InState),
2456		state_corresponds_to_initialised_b_machine(InState,BState),
2457		set_context_state(CurID,tcltk_add_user_executed_statement),
2458		%start_ms_timer(Timer),
2459		call_cleanup((tcltk_interface:b_full_execute_top_level_statement_with_probids(Statement,BState,Updates,NewState)->true),
2460		clear_context_state),
2461		% TO DO: do we need to catch enumeration warnings ?
2462		%stop_ms_timer(Timer),
2463		Residue=[], TransInfo = [],
2464		debug_println(4,executed(Updates,NewState)),
2465		compute_all_transitions_if_necessary(CurID), % first ensure we have already computed outgoing transitions as usual, so that we can detect if a new state is added
2466		(get_id_of_node_and_add_if_required(NewState,NewID,Exists,CurID,'$unknown_operation',[]),
2467		Exists=exists,
2468		transition(CurID,Action,TransId,NewID)
2469		-> debug_println(4,transition_exists_already(Action,TransId))
2470		; translate:translate_substitution(Statement,OpLabel),
2471		add_trans_id_with_infos(CurID,[],'$USER'(OpLabel),NewState,Residue,NewID,TransInfo,_),
2472		format('Added new user-initiated transition to ~w via: ~w~n',[NewID,OpLabel])
2473		),
2474		tcltk_goto_state(OpLabel,NewID).
2475
2476		:- use_module(eval_let_store,[extend_state_with_probids_and_lets/2]).
2477		:- use_module(kernel_waitflags,[init_wait_flags_with_call_stack/2, ground_wait_flags/1]).
2478		%% allows one to execute any statement (not just operations).
2479		b_full_execute_top_level_statement_with_probids(Body,InState,Updates,NewState) :-
2480		extend_state_with_probids_and_lets(InState,InState1),
2481		init_wait_flags_with_call_stack(WF,[prob_command_context(user_executed_statement,unknown)]),
2482		b_execute_top_level_statement(Body,[],InState1,Updates,WF,_Path1,output_not_required),
2483		ground_wait_flags(WF),
2484		store:store_updates_and_normalise(Updates,InState,NewState).
2485
2486		% --------------------------------------------------------------------------------------
2487
2488
2489		:- use_module(bmachine).
2490		:- use_module(specfile).
2491		:- use_module(tools).
2492		:- use_module(library(lists)).
2493		:- use_module(store).
2494		:- use_module(self_check).
2495		:- use_module(b_global_sets).
2496		:- use_module(translate).
2497
2498
2499		/* --------------------------------------------------------- */
2500		/* --------------------------------------------------------- */
2501
2502
2503		/* ----------------------------------*/
2504		/* b_analyse_conjunction */
2505		/* ----------------------------------*/
2506
2507
2508		/* provide list of possible options for analysis */
2509		tcltk_analyse_option(invariant,'INVARIANT') :- b_or_z_mode.
2510		tcltk_analyse_option(properties,S) :- b_or_z_mode,
2511		get_specification_description(properties,S).
2512		tcltk_analyse_option(assertions,S) :- (b_or_z_mode ; csp_mode),
2513		get_specification_description(assertions,S).
2514		tcltk_analyse_option(deadlock,'DEADLOCKED') :- b_or_z_mode.
2515
2516
2517		:- use_module(predicate_evaluator).
2518		/* perform the various analysis */
2519		tcltk_analyse(Mode,Type,ListWithResults,Total,False,Unknown) :-
2520		(Mode == unicode
2521		-> set_unicode_mode,
2522		call_cleanup(tcltk_analyse2(Type,ListWithResults,Summary),unset_unicode_mode)
2523		; tcltk_analyse2(Type,ListWithResults,Summary)),
2524		(member(total/Total,Summary) -> true ; Total=0),
2525		(member(false/False,Summary) -> true ; False=0),
2526		(member(unknown/Unknown,Summary) -> true ; Unknown=0).
2527		tcltk_analyse2(invariant,L,Summary) :- !,tcltk_analyse_invariant(L,Summary).
2528		tcltk_analyse2(properties,L,Summary) :- !,tcltk_analyse_properties(L,Summary).
2529		tcltk_analyse2(assertions,L,Summary) :- !,tcltk_analyse_assertions(L,Summary).
2530		tcltk_analyse2(deadlock,L,Summary) :- !,tcltk_analyse_deadlock(L,Summary).
2531		tcltk_analyse2(X,L,Summary) :- add_error(tcltk_analyse, 'Unknown type of formula: ', X),
2532		L=[], Summary=[].
2533
2534
2535		/* --------------------------------- */
2536
2537		tcltk_show_current_state(TransBState) :-
2538		current_b_expression(B),
2539		translate_bstate(B,TransBState).
2540
2541
2542		tcltk_show_typing_of_variables_and_constants(list(List)) :-
2543		b_get_machine_variables(TypedVarList),
2544		convert_typed_varlist(TypedVarList,VarList,Types),
2545		generate_typing_list(VarList,Types,VList,VarCard),
2546		length(VarList,NrVars),
2547		format_to_codes(' VARIABLES [nr=~w,card=~w]',[NrVars,VarCard],Codes1),atom_codes(VARAtom,Codes1),
2548
2549		b_get_machine_all_constants(TypedCstList),
2550		convert_typed_varlist(TypedCstList,CVarList,CTypes),
2551		find_non_det_constants,
2552		generate_typing_list(CVarList,CTypes,CList,CCard),
2553		( CList = []
2554		-> List = [VARAtom|VList]
2555		; length(CVarList,NrCsts),
2556		format_to_codes(' CONSTANTS [nr=~w,card=~w]',[NrCsts,CCard],Codes2),atom_codes(CstAtom,Codes2),
2557		append([CstAtom|CList],[VARAtom|VList],List)
2558		),!.
2559		tcltk_show_typing_of_variables_and_constants(list(['TYPE ERROR in MACHINE'])).
2560
2561
2562		%%% Used to get the constant values for the currently loaded B machine in form of a B predicate.
2563		%%% In case that the constants in the model has not been set up then all possible constants'
2564		%%% evaluations will be provided in form of a predicate in Disjunctive Normal Form.
2565		%%% Predicate used for setting up constants when model checking with TLC. (TLA)
2566		tcltk_get_constants_predicate(P,N) :-
2567		current_state_id(CurID),
2568		(CurID==root
2569		-> get_constants_as_disjoint_predicate(N,P)
2570		; prob2_interface:get_state(CurID,EState),
2571		filter_constants_bindings(EState,X), % this will only get current constants values
2572		translate_bstate_to_pred(X,P)
2573		).
2574
2575		get_constants_as_disjoint_predicate(N,Res) :-
2576		findall(R,get_set_up_constants_solution(R),L),
2577		get_a_part_of_the_found_solutions(L,N,Part),
2578		add_or_between_constant_predicates(Part,Res).
2579
2580		get_a_part_of_the_found_solutions(L,N,Part) :-
2581		length(L,Length),
2582		(N>=Length
2583		-> Part=L
2584		; sublist(L,Part,_B,N,_A)).
2585
2586		translate_bstate_to_pred(State,P) :-
2587		temporary_set_preference(expand_avl_upto,-1,CHNG2),
2588		translate: translate_bstate(State,P),
2589		reset_temporary_preference(expand_avl_upto,CHNG2).
2590
2591		get_set_up_constants_solution(R) :-
2592		%\+ max_reached_or_timeout_for_node(root),!, % then lookup constants rather than computing them
2593		transition(root,_,Dst),
2594		visited_expression(Dst,concrete_constants(X)),
2595		translate_bstate_to_pred(X,R).
2596		%get_set_up_constants_solution(R) :-
2597		% b_interpreter: b_set_up_concrete_constants(X,_),
2598		% translate:translate_bstate(X,R).
2599
2600		add_or_between_constant_predicates([],'1=1').
2601		add_or_between_constant_predicates(L,Res) :-
2602		tools: ajoin_with_sep(L,' or ',Res).
2603
2604		filter_constants_bindings(EState,R) :-
2605		b_get_machine_all_constants(C),
2606		convert_typed_varlist(C,CVarList,_CTypes),
2607		filter_constants_bindings1(EState,CVarList,R).
2608
2609		filter_constants_bindings1([],_,[]).
2610		filter_constants_bindings1([bind(Ident,Val)|T],CVarList,Res) :-
2611		(member(Ident,CVarList) -> Res = [bind(Ident,Val)|Rest]; Res = Rest),
2612		filter_constants_bindings1(T,CVarList,Rest).
2613
2614		convert_typed_varlist([],[],[]).
2615		convert_typed_varlist([b(identifier(ID),Type,_)|T],[ID|IT],[Type|TT]) :-
2616		%print(ID), print(' : '), print(Type),nl,
2617		% db : set(couple(global(Name),global(Code))) a : set(integer) boolean
2618		convert_typed_varlist(T,IT,TT).
2619		%--------------------------------------
2620
2621
2622		:- use_module(symsrc(symmetry_marker),[type_allows_for_precise_marker/1]).
2623		:- use_module(bmachine,[b_is_unused_constant/1]).
2624		:- use_module(library(codesio),[format_to_codes/3]).
2625		generate_typing_list([],[],[],1).
2626		generate_typing_list([Var|VT],[BasicType|TT],[Translation|Rest],TotCard) :-
2627		pretty_type(BasicType,PrettyType),
2628		(kernel_objects:max_cardinality(BasicType,Card) -> true ; Card='??'),
2629		(b_get_constant_represented_inside_global_set(Var,BasicType)
2630		-> Imp='(treated as enumerated) '
2631		; (preference(symmetry_mode,hash),
2632		\+type_allows_for_precise_marker(BasicType))
2633		-> Imp = '(IMPRECISE for HASH) '
2634		; Imp = ''
2635		),
2636		(non_det_constant(Var)
2637		-> MulSol ='[multiple solutions in SETUP_CONSTANTS]'
2638		; MulSol=''),
2639		(b_is_unused_constant(Var) -> Unused=' (unused)' ; Unused=''),
2640		% translate:translate_bexpression(b(member(identifier(Var),BasicType),pred,[]),Translation),
2641		format_to_codes('~w:~w [card=~w]~w~w~w',[Var,PrettyType,Card,MulSol,Imp,Unused],Codes),
2642		atom_codes(Translation,Codes),
2643		generate_typing_list(VT,TT,Rest,RestCard),
2644		kernel_objects:safe_mul(RestCard,Card,TotCard).
2645
2646		:- use_module(symsrc(symmetry_marker),[hash_model_checking_imprecise/2]).
2647		:- use_module(translate,[pretty_type/2]).
2648
2649		tcltk_hash_model_checking_imprecise :-
2650		get_preference(symmetry_mode,hash),
2651		hash_model_checking_imprecise(ID,BasicType),!,
2652		print(' * Note: Hashing may be imprecise for: '),
2653		print(ID), print(' : '),translate:pretty_type(BasicType,S),print(S), print(' !'),nl.
2654
2655
2656		/* find constants which are assigned multiple values */
2657		:- dynamic non_det_constant/1.
2658		find_non_det_constants :-
2659		retractall(non_det_constant(_)),
2660		findall(Csts,visited_expression(_,concrete_constants(Csts),_),CL),
2661		(CL=[Valuation1|O],O=[_|_] -> find_non_det_constants1(Valuation1,O)
2662		; true /* 0 or 1 valuation only */
2663		).
2664
2665		find_non_det_constants1([],_).
2666		find_non_det_constants1([bind(C,Value)|T],Other) :- check_cst(Other, C, Value, PeeledOther),
2667		find_non_det_constants1(T,PeeledOther).
2668
2669		check_cst([],_,_,[]).
2670		check_cst([ [bind(C,OtherVal)|T1] | TT], C, Value, [ T1 | PTT]) :-
2671		(Value=OtherVal -> check_cst(TT,C,Value,PTT)
2672		; assertz(non_det_constant(C)), peel2(TT,PTT)).
2673		peel2([],[]).
2674		peel2([ [_|T1] | TT], [ T1 | PTT]) :- peel2(TT,PTT).
2675
2676
2677		/* --------------------------------- */
2678
2679
2680		/* --------------------------------- */
2681
2682		%%
2683		% Visualize Invariant...
2684		%
2685		% Siehe bvisual.pl
2686
2687		:- use_module(dotsrc(bvisual),[get_tree_from_expr/4, write_dot_graph_to_file/2]).
2688
2689
2690		generate_dot_from_invariant(FileName):-
2691		bmachine:b_get_invariant_from_machine(BExpr),
2692		write_dot_file_for_pred_expr(BExpr,FileName).
2693
2694
2695		:- use_module(b_operation_guards,[get_quantified_operation_enabling_condition/4]).
2696		generate_dot_from_operation(TclOpName,FileName) :-
2697		adapt_tcl_operation_name(TclOpName,OpName),
2698		Simplify=false,
2699		get_quantified_operation_enabling_condition(OpName, BExpr, _BecomesSuchVars, Simplify),
2700		write_dot_file_for_pred_expr(BExpr,FileName).
2701		%generate_tree_from_boolean_expression(BExpr, Tree,BecomesSuchVars),
2702		%write_dot_graph_to_file(Tree,FileName).
2703
2704		% a version with additional parameters and additional pre condition / guard predicate
2705		generate_dot_from_operation_with_params(TclOpName,ParameterBindList,RestPreCond, FileName) :-
2706		adapt_tcl_operation_name(TclOpName,OpName),
2707		Simplify=false,
2708		get_quantified_operation_enabling_condition(OpName, BExpr, BecomesSuchVars,Simplify),
2709		parse_tclk_parameter_values_and_pred(OpName,ParameterBindList,RestPreCond,CustomPredicate),
2710		insert_custom_predicate_into_guard(BExpr,CustomPredicate,FullPred),
2711		%translate:nested_print_bexpr(FullPred),nl,
2712		% TODO: probably allow all variables to be primed in CustomPredicate:
2713		b_ast_cleanup:annotate_becomes_such_vars(BecomesSuchVars,CustomPredicate,BSV2),
2714		write_dot_file_for_pred_expr(FullPred,FileName,BSV2).
2715
2716		insert_custom_predicate_into_guard(b(exists(Para,Body),pred,Info),Pred,Res) :- !,
2717		Res = b(exists(Para,BodyRes),pred,Info), % TODO: update wd infos
2718		insert_custom_predicate_into_guard(Body,Pred,BodyRes).
2719		insert_custom_predicate_into_guard(Guard,CustomPred,FullPred) :-
2720		conjunct_predicates([Guard,CustomPred],FullPred).
2721
2722		:- use_module(bmachine, [
2723		b_get_properties_from_machine/1,
2724		b_get_machine_constants/1,
2725		b_machine_has_constants_or_properties/0 ]).
2726		:- use_module(bsyntaxtree,[create_or_merge_exists/3]).
2727		get_properties(BExpr,CreateExists):-
2728		b_get_properties_from_machine(Condition),
2729		( (CreateExists=true,b_machine_has_constants_or_properties) ->
2730		b_get_machine_constants(IDs),
2731		create_or_merge_exists(IDs, Condition, BExpr)
2732		;
2733		BExpr = Condition
2734		).
2735
2736		generate_dot_from_properties(FileName) :-
2737		(current_state_corresponds_to_fully_setup_b_machine -> CreateExists=false; CreateExists=true),
2738		get_properties(BExpr,CreateExists),
2739		write_dot_file_for_pred_expr(BExpr,FileName).
2740
2741		:- use_module(bsyntaxtree,[conjunct_predicates/2]).
2742
2743		generate_dot_from_assertions(FileName) :-
2744		(current_state_corresponds_to_setup_constants_b_machine,
2745		bmachine:b_get_dynamic_assertions_from_machine(BExpr), BExpr \=[]
2746		-> true
2747		; bmachine:b_get_static_assertions_from_machine(BExpr)
2748		),
2749		conjunct_predicates(BExpr,BE),
2750		write_dot_file_for_pred_expr(BE,FileName).
2751
2752		generate_dot_from_goal(FileName) :-
2753		b_get_machine_goal(BExpr),!,
2754		write_dot_file_for_pred_expr(BExpr,FileName,all_primed_vars).
2755		generate_dot_from_goal(FileName) :-
2756		write_dot_file_for_pred_expr_and_state(b(string('No GOAL DEFINITION available'),string,[]),[],[],FileName).
2757
2758		generate_dot_from_deadlock_po(FileName) :-
2759		b_state_model_check:get_unsorted_all_guards_false_pred(BExpr),
2760		%print('% CHECKING: '),translate_bexpression(BExpr,PT), print(PT),nl,
2761		write_dot_file_for_pred_expr(BExpr,FileName). % we do not check it is a predicate anymore
2762
2763
2764		generate_dot_from_formula(Pred,FileName) :-
2765		debug_format(19,'Parsing formula ~w~n',[Pred]),
2766		parse_machine_formula(Pred,TypedExpr),
2767		debug_format(19,'Writing dot formula ~w~n',[Pred]),
2768		write_dot_file_for_pred_expr(TypedExpr,FileName,all_primed_vars).
2769
2770
2771		:- use_module(bmachine, [b_parse_machine_formula/3, type_with_errors/4, get_primed_machine_variables/1]).
2772		parse_machine_formula(RawAST,TypedPred) :- compound(RawAST),!, % allow to pass raw AST as well
2773		get_primed_machine_variables(PV),
2774		type_with_errors(RawAST,[prob_ids(visible),identifier(PV),variables],_Type,TypedPred).
2775		parse_machine_formula(PredStr,TypedExpr) :-
2776		get_primed_machine_variables(PV),
2777		b_parse_machine_formula(PredStr,[prob_ids(visible),identifier(PV),variables],TypedExpr).
2778
2779
2780		write_dot_file_for_pred_expr(BExpr,FileName) :-
2781		write_dot_file_for_pred_expr(BExpr,FileName,[]).
2782		write_dot_file_for_pred_expr(BExpr,FileName,BecomesSuchVars) :-
2783		generate_tree_in_cur_state(BExpr, Tree,BecomesSuchVars),
2784		printsilent('% Writing to: '), printsilent(FileName),nls,
2785		write_dot_graph_to_file(Tree,FileName).
2786		write_dot_file_for_pred_expr_and_state(BExpr, LocalState, State,FileName) :-
2787		get_tree_from_expr(Tree, BExpr, LocalState, State),
2788		printsilent('% Writing to: '), printsilent(FileName),nls,
2789		write_dot_graph_to_file(Tree,FileName).
2790
2791		:- use_module(probsrc(state_space),[get_current_predecessor_state_id/1]).
2792		:- use_module(probsrc(specfile),[extract_variables_from_state_as_primed/2]).
2793
2794		generate_tree_in_cur_state(BExpr,Tree,all_primed_vars) :-
2795		(get_current_predecessor_state_id(PredID),
2796		visited_expression(PredID,SrcState),
2797		extract_variables_from_state_as_primed(SrcState,PrimedVarBindings)
2798		-> true
2799		; PrimedVarBindings=[]
2800		),
2801		get_current_state_for_b_formula(BExpr,CurState0),
2802		extend_state_with_probids_and_lets(CurState0,CurState1),
2803		append(PrimedVarBindings,CurState1,CurState),
2804		get_tree_from_expr(Tree, BExpr, [], CurState).
2805		generate_tree_in_cur_state(BExpr,Tree,BecomesSuchVars) :-
2806		get_current_state_for_b_formula(BExpr,CurState0),
2807		extend_state_with_probids_and_lets(CurState0,CurState1),
2808		% print(cur(CurState1)),nl,
2809		insert_before_substitution_variables(BecomesSuchVars,[],CurState1,CurState1,CurState),
2810		!,
2811		get_tree_from_expr(Tree, BExpr, [], CurState).
2812
2813		% generate a dot tree representation for a value; mostly useful for symbolic values
2814		write_dot_file_for_value_as_tree(Value,FileName) :-
2815		transform_value_to_expr(Value,BExpr),
2816		temporary_set_preference(formula_tree_minimal_timeout,5,Prev1),
2817		temporary_set_preference(formula_tree_maximal_timeout,30,Prev2),
2818		call_cleanup(generate_tree_in_cur_state(BExpr, Tree,[]),
2819		(reset_temporary_preference(formula_tree_minimal_timeout,Prev1),
2820		reset_temporary_preference(formula_tree_maximal_timeout,Prev2))),
2821		printsilent('% Writing to: '), printsilent(FileName),nls,
2822		write_dot_graph_to_file(Tree,FileName).
2823
2824		:- use_module(probsrc(bsyntaxtree),[create_typed_id/3]).
2825		:- use_module(library(lists),[maplist/4]).
2826		transform_value_to_expr(closure(P,T,B),E) :-
2827		maplist(create_typed_id,P,T,Parameters),!,
2828		E=b(comprehension_set(Parameters,B),set(any),[]). % TO DO: we could create typing
2829		transform_value_to_expr(Val,b(value(Val),any,[])).
2830
2831		:- use_module(tools,[maplist5/5]).
2832		tcltk_bv_get_tops(Tops) :-
2833		bv_get_top_level(Tops).
2834		tcltk_bv_get_structure(Id,Label,list(Subs)) :-
2835		bv_expand_formula(Id,Label,Subs).
2836		tcltk_bv_is_leaf(Id,Label) :-
2837		bv_expand_formula(Id,Label,[]).
2838		tcltk_bv_get_values(Ids,list(RTexts),list(Tags)) :-
2839		current_state_id(StateId),
2840		bv_get_values(Ids,StateId,Values),
2841		maplist5(tcltk_interface:retrieve_tag_adapted_text_for_id,Ids,Values,Tags,RTexts).
2842		tcltk_bv_get_value(Id,RText,Tag) :-
2843		tcltk_bv_get_values([Id],list([RText]),list([Tag])).
2844		tcltk_bv_show_formula_as_dot_tree(Id,File) :-
2845		bv_get_stored_formula_expr(Id,TExpr),
2846		write_dot_file_for_pred_expr(TExpr,File).
2847		tcltk_bv_get_pp_formula_string(Id,PPFormula) :-
2848		bv_get_stored_formula_expr(Id,TExpr),
2849		translate:translate_bexpression(TExpr,PPFormula).
2850
2851		tcltk_bv_show_formula_as_dot_graph(Id,File) :-
2852		bv_get_stored_formula_expr(Id,TExpr),
2853		get_texpr_type(TExpr,Type),
2854		Type \= pred, Type \= subst,
2855		% tcltk_show_typed_expression_as_dot_graph decomposes expressions and shows value as graph: could be useful for pre-configured DEFINITIONS
2856		tcltk_show_typed_expression_as_dot_graph(TExpr,File).
2857
2858		tcltk_bv_show_value_as_dot_tree(Id,File) :- % useful for symbolic values
2859		current_state_id(StateId),
2860		bv_get_btvalue(Id,StateId,_E,Value),
2861		write_dot_file_for_value_as_tree(Value,File).
2862
2863		% a variation of tcltk_bv_show_value_as_dot_tree without dependence on bvisual2
2864		tcltk_show_identifier_value_as_dot_tree(RawId,File) :- % this also works if bvisual2 is not set up and entry active
2865		get_identifier(RawId,Id),
2866		current_expression(_ID,CurState),
2867		expand_const_and_vars_to_full_store(CurState,EState),
2868		(lookup_value_for_existing_id(Id,EState,Value)
2869		-> write_dot_file_for_value_as_tree(Value,File)
2870		; add_error(tcltk_show_identifier_value_as_dot_tree,'Cannot retrieve value for identifier:',Id)).
2871
2872		get_identifier(AtomicID,Res) :- atom(AtomicID), valid_id(AtomicID), !,Res=AtomicID.
2873		get_identifier(identifier(_,ID),Res) :- valid_id(ID),!, Res=ID. % raw ID from prob2_interface
2874		get_identifier(RawFormula,_) :-
2875		add_error(tcltk_show_identifier_value_as_dot_tree,'Please provide valid identifier of constant or variable:',RawFormula),
2876		fail.
2877		valid_id(ID) :- b_is_variable(ID).
2878		valid_id(ID) :- b_is_constant(ID).
2879
2880		retrieve_tag_adapted_text_for_id(Id,Value,Tag,RText) :-
2881		retrieve_tag_text_for_id(Id,Value,Tag,Text),
2882		(Text = '[]' -> RText = '[ ]' ; RText=Text). % for some reason the empty sequence translation [] gets transformed into '' by the tcltk library
2883
2884		retrieve_tag_text_for_id(Id,Value,FullTag,Text) :-
2885		retrieve_tag_text(Value,Tag,Text),
2886		(bv_is_explanation_node(Id) -> convert_explain_tag(Tag,FullTag) ; FullTag=Tag).
2887		retrieve_tag_text(i, inac, '').
2888		retrieve_tag_text(e(Text), error, Text).
2889		retrieve_tag_text(v(Text), value, Text).
2890		retrieve_tag_text(p(true), ptrue, true).
2891		retrieve_tag_text(p(false),pfalse, false).
2892		retrieve_tag_text(bv_info(Text), inac, Text).
2893
2894
2895		tcltk_bv_get_unlimited_value(Id,Text,Tag) :-
2896		current_state_id(StateId),
2897		bv_get_value_unlimited(Id,StateId,Value),
2898		retrieve_tag_text_for_id(Id,Value,Tag,Text1),
2899		atom_codes(Text1,Text). % TODO: In the end, the result was converted from codes to atom and back
2900
2901		% a version which returns just the value as an atom:
2902		tcltk_bv_get_unlimited_value_atom(Id,AtomText) :-
2903		current_state_id(StateId),
2904		bv_get_value_unlimited(Id,StateId,Value),
2905		retrieve_tag_text_for_id(Id,Value,_Tag,AtomText).
2906
2907		convert_explain_tag(ptrue,explaintrue).
2908		convert_explain_tag(pfalse,explainfalse).
2909		convert_explain_tag(X,X).
2910
2911		% -----------------------------------------
2912
2913		% STILL TO DO: refactor eval from here and probcli into separate module
2914
2915		:- dynamic eval_elapsed_time/1.
2916		tcltk_time_call(Call) :-
2917		cputime(T1),Call,cputime(T2),ElapsedTime is T2-T1,
2918		retractall(eval_elapsed_time(_)),assertz(eval_elapsed_time(ElapsedTime)).
2919
2920		:- use_module(eval_strings).
2921
2922
2923		tcltk_eval(String,StringResult,EnumWarning,Solution) :-
2924		get_computed_preference(debug_time_out,DTO),
2925		%print(debug_time_out(DTO)),nl,
2926		time_out_with_enum_warning_one_solution(eval_string(String,StringResult,EnumWarning,LocalState),DTO,TimeOutRes),
2927		(LocalState=[] -> Solution='' ; translate_bstate(LocalState,Solution)),
2928		(is_time_out_result(TimeOutRes) ->
2929		StringResult = '**** TIME-OUT ****', print(StringResult), print(' ('),print(DTO), print('ms)'),nl,
2930		EnumWarning = no
2931		; print_last_info).
2932
2933		:- public tcltk_eval_string_in_cur_state/2.
2934		tcltk_eval_string_in_cur_state(String,TclValue) :-
2935		eval_string_in_cur_state(String,_,Value),
2936		convert_value_to_tcl(Value,TclValue).
2937		convert_value_to_tcl(int(X),R) :- !, R=X.
2938		convert_value_to_tcl(pred_true,R) :- !, R=1.
2939		convert_value_to_tcl(pred_false,R) :- !, R=0.
2940		convert_value_to_tcl(string(X),R) :- !, R=X.
2941		% TO DO: add sets,...
2942		convert_value_to_tcl(R,R) :- print(cannot_convert_to_tcl(R,R)),nl.
2943
2944		eval_string_in_cur_state(String,Typed,Value) :-
2945		%format('Parsing : "~w"~n',[String]),
2946		bmachine:parse_expression_raw_or_atom_with_prob_ids(String,Typed),
2947		current_state_id(CurID), prob2_interface:get_state(CurID,EState),
2948		%print(evaluating_in_state(CurID)),nl,
2949		b_compute_expression_with_prob_ids(Typed,EState,Value).
2950
2951		% code to translate an expression into a list of lists that can be displayed as a table in Tk
2952		% TO DO: make more robust and add more fancy translations
2953		:- use_module(extrasrc(table_tools),[expand_and_translate_to_table_for_expr/5]).
2954		tcltk_eval_as_table(String,Res) :-
2955		eval_string_in_cur_state(String,Typed,Value),
2956		Res = list([list(Header)|Table]),
2957		expand_and_translate_to_table_for_expr(Typed,Value,Header,Table,['no-row-numbers']).
2958
2959		:- use_module(user_interrupts,[interruptable_call/1]).
2960		interruptable_tcltk_eval(String,StringResult,EnumWarning,Solution) :-
2961		if(interruptable_call(tcltk_eval(String,StringResult,EnumWarning,Solution)),true,
2962		(StringResult = 'Error or User-Interrupt', EnumWarning=unknown, Solution='')).
2963
2964		% -----------------------------------------
2965
2966		tcltk_find_value_as_table(String,Options,list([Header|Matches])) :-
2967		eval_string_in_cur_state(String,Typed,GoalValue),
2968		Header = list(['ID','Kind','MatchPath']),
2969		get_texpr_type(Typed,Type),
2970		findall(list([ID,Kind,MatchMsg]),
2971		(find_value_in_cur_state(GoalValue,Type,Options,match(Kind,ID,Path)),
2972		format_to_codes('~w',[Path],MatchMsgC),
2973		format('* match inside ~w ~w @ path: ~w~n',[Kind,ID,Path]),
2974		atom_codes(MatchMsg,MatchMsgC)),Matches).
2975
2976		% find a given value somewhere in a constant or variable value
2977
2978		find_value_in_cur_state(GoalValue,Type,Options,match(Kind,ID,Path)) :-
2979		translate:translate_bvalue(GoalValue,VS),
2980		get_current_state_for_b_formula(requires_variables,State), % produce full state
2981		member(bind(ID,Value),State),
2982		( bmachine:b_is_variable(ID,IDType), Kind=variable
2983		; bmachine:b_is_constant(ID,IDType), Kind=constant),
2984		debug_format(19,'Searching id ~w for ~w~n',[ID,VS]),
2985		% TODO check if Type occurs in type of ID
2986		find_value(Value,IDType,GoalValue,Type,Options,Path).
2987
2988
2989		:- use_module(probsrc(kernel_freetypes),[registered_freetype/2]).
2990		:- use_module(bsyntaxtree,[is_set_type/2]).
2991		:- use_module(kernel_strings,[to_b_string/2]).
2992		find_value(Val,Type,GoalVal,Type,Options,Path) :- !, % target and goal type match; to do: unify_types
2993		(kernel_objects:equal_object(Val,GoalVal) -> Path = '*'
2994		; fuzzy_find_value(Val,Type,GoalVal,Type,Options,Path)).
2995		find_value((A,B),couple(TA,TB),GoalVal,Type,Options,Path) :- !,
2996		( find_value(A,TA,GoalVal,Type,Options,PA),
2997		Path=','(PA,BS), translate:translate_bvalue(B,BS)
2998		; find_value(B,TB,GoalVal,Type,Options,PB),
2999		Path=','(AS,PB), translate:translate_bvalue(A,AS)).
3000		find_value(rec(Fields),record(FieldTypes),GoalVal,Type,Options,rec(Field,Path)) :- !,
3001		member(field(Field,Val),Fields),
3002		member(field(Field,TVal),FieldTypes),
3003		find_value(Val,TVal,GoalVal,Type,Options,Path).
3004		find_value(avl_set(AVL),AType,GoalVal,Type,Options,'{}'(Path)) :- !,
3005		is_set_type(AType,TA),
3006		custom_explicit_sets:avl_member_opt(Value,AVL), % TODO: provide a more proper interface predicate
3007		find_value(Value,TA,GoalVal,Type,Options,Path).
3008		find_value([H|T],set(TA),GoalVal,Type,Options,'{}'(Path)) :- !,
3009		member(Value,[H|T]),
3010		find_value(Value,TA,GoalVal,Type,Options,Path).
3011		find_value(freeval(ID,Case,Val),freetype(ID),GoalVal,Type,Options,freeval(Case,Path)) :- !,
3012		(registered_freetype(ID,Cases),
3013		member(case(Case,TVal),Cases) -> true
3014		; add_error(find_value,'Illegal freeval:',freeval(ID,Case,Val)),fail
3015		),
3016		find_value(Val,TVal,GoalVal,Type,Options,Path).
3017		find_value(Val,TypeVal,GoalVal,Type,Options,Path) :-
3018		fuzzy_find_value(Val,TypeVal,GoalVal,Type,Options,Path).
3019
3020		fuzzy_find_value(Val,_Type,string(GoalAtom),string,[Option],'**'(TargetAtom)) :-
3021		GoalAtom \= '',
3022		simple_value_to_match(Val),
3023		to_b_string(Val,string(TargetAtom)),
3024		find_match_string(Option,TargetAtom,GoalAtom).
3025
3026		simple_value_to_match(fd(_,_)).
3027		simple_value_to_match(string(_)).
3028		simple_value_to_match(int(_)).
3029		simple_value_to_match(term(_)).
3030		simple_value_to_match(freeval(_,_Case,Val)) :- ground(Val), Val=term(_).
3031
3032		:- use_module(tools_matching,[fuzzy_match_codes_lower_case/2]).
3033
3034		% check whether TargetAtom matches GoalAtom given match option
3035		find_match_string(exact,GoalAtom,GoalAtom).
3036		find_match_string(prefix,TargetAtom,GoalAtom) :-
3037		atom_concat(GoalAtom,_,TargetAtom). % use sub_atom ?
3038		find_match_string(suffix,TargetAtom,GoalAtom) :-
3039		atom_concat(_,GoalAtom,TargetAtom).
3040		find_match_string(infix,TargetAtom,GoalAtom) :-
3041		sub_atom(TargetAtom,_Before,Length,_After,GoalAtom), Length>0.
3042		find_match_string(fuzzy,TargetAtom,GoalAtom) :-
3043		atom_codes(TargetAtom,TC),
3044		atom_codes(GoalAtom,GC),
3045		fuzzy_match_codes_lower_case(TC,GC).
3046		% TODO: regex
3047
3048		% -----------------------------------------
3049		% B Simplifier
3050		:- use_module(probporsrc(b_simplifier),[tcltk_simplify_b_predicate/2]).
3051		tcltk_simplify_predicate(String,StringResult) :-
3052		tcltk_simplify_b_predicate(String,StringResult).
3053
3054
3055		% -----------------------------------------
3056		% CBC Check
3057
3058		get_cbc_data_base_id_checks(IDs) :-
3059		findall(ID,b_state_model_check: cbc_check(ID,_Text,_Call,_Res,_Ok),IDs).
3060		get_cbc_data_base_text_checks(Strings) :-
3061		findall(Text1,(b_state_model_check: cbc_check(_ID,Text,_Call,_Res,_Ok),tools: string_concatenate(Text,';',Text1)),Strings).
3062
3063
3064		% -----------------------------------------
3065
3066		% CSP Refinement Search
3067
3068		%:- dynamic tcltk_cspm_mode/0.
3069		%set_tcltk_cspm_mode :- assertz(tcltk_cspm_mode).
3070		%unset_tcltk_cspm_mode :- retractall(tcltk_cspm_mode).
3071
3072
3073		%get_new_csp_process_id(E,File,ID) :-
3074		% ( parse_single_csp_expression_file(E,File,Proc) ->
3075		% haskell_csp: check_compiled_term(Proc), add_csp_process_id1(Proc,ID,haskell_csp:animatable_process)
3076		% ; add_error(parse_single_csp_expression_file,'Invalid process expression: ',E),fail
3077		% ).
3078
3079		%parse_and_analyze_process_expression(ProcExp,File,Proc) :-
3080		% ( parse_single_csp_expression_file(ProcExp,File,Proc) -> true
3081		% ; add_error(parse_single_csp_expression_file,'Invalid process expression: ',ProcExp),fail
3082		% ).
3083
3084		get_csp_process_id(Process,ID) :- get_start_transition_term(Process,Trans),
3085		transition(root,Trans,ID).
3086
3087		:- use_module(probcspsrc(haskell_csp),[animatable_process_without_arguments/1,animatable_process_cli/1]).
3088		add_csp_process_id(Process,NewID) :-
3089		add_csp_process_id1(Process,NewID,animatable_process_cli).
3090
3091		add_csp_process_id1(Process,NewID,Pred) :-
3092		(call(Pred,Process)
3093		-> get_start_transition_term(Process,Trans),
3094		(transition(root,Trans,_,DestID) -> NewID=DestID % process already set up
3095		; xtl_interface:get_start_expr(Process,NewState),
3096		add_trans_id(root,Trans,NewState,NewID,_)
3097		)
3098		; add_error_fail(add_csp_process_id,'Not an animatable CSP Process: ',Process)).
3099
3100		get_start_transition_term('MAIN',R) :- !, R= start_cspm_MAIN.
3101		get_start_transition_term(agent_call(_Src,'MAIN',[]),R) :- !, R= start_cspm_MAIN.
3102		get_start_transition_term(P,start_cspm(P)).
3103
3104		add_csp_general_process_id(val_of(Process,_),ID) :- !,
3105		( animatable_process_without_arguments(Process) % in case the called processes is one without arguments, then we don't have to parse the expression
3106		-> add_csp_process_id(Process,ID)
3107		% code below not covered; loaded_main_file only defined for probcli entry point !
3108		%; animation_mode(cspm),
3109		% loaded_main_file(CSPFile),
3110		% parse_and_analyze_process_expression(Process,CSPFile,Proc),
3111		% (transition(root,start_cspm(Proc),_TransID,ID) -> true
3112		% ; otherwise -> add_trans_id(root,start_cspm(Proc),Proc,ID,_)
3113		% )
3114		).
3115		add_csp_general_process_id(GenProcExpr,ID) :-
3116		% stripping out the source-loc info
3117		haskell_csp_analyzer: clear_span(GenProcExpr,GenProcExpr1),
3118		get_start_transition_term(GenProcExpr1,Trans),
3119		(transition(root,Trans,_TransID,ID)
3120		-> true
3121		; add_trans_id(root,Trans,GenProcExpr1,ID,_)
3122		).
3123
3124		:- public tcltk_csp_in_situ_refinement/4.
3125		tcltk_csp_in_situ_refinement(ImplProcess,AbsProcess,ResTrace,Style) :-
3126		format('Checking ~w ~w ~w~n',[AbsProcess,Style,ImplProcess]),
3127		tcltk_csp_in_situ_refinement(ImplProcess,AbsProcess,ResTrace,Style,10000000).
3128		csp_ref_style('[T=',trace). % Trace Refinement
3129		csp_ref_style('T',trace). % Trace Refinement
3130		csp_ref_style('[SF=',singleton_failures). % Singleton Failures Refinement
3131		csp_ref_style('[F=',failures). % Failures Refinement
3132		csp_ref_style('[R=',refusals). % Refusals Refinement
3133		csp_ref_style('[RD=',refusals_div). % Refusals-Divergence Refinement
3134		csp_ref_style('F',failures). % Failures Refinement
3135		csp_ref_style('[FD=',X) :- csp_ref_style('FailureDivergence',X).
3136		csp_ref_style('FD',X) :- csp_ref_style('FailureDivergence',X).
3137		csp_ref_style('Trace',trace).
3138		csp_ref_style('Failure',failures).
3139		csp_ref_style('FailureDivergence',failure_divergences).
3140		csp_ref_style('RefusalTesting',refusals).
3141		csp_ref_style('RefusalTestingDiv',refusals_div).
3142		csp_ref_style('RevivalTesting',revival) :- add_error(unsupported_refinement_operator,'[V= refinement not yet supported.').
3143		csp_ref_style('RevivalTestingDiv',revival_div) :- add_error(unsupported_refinement_operator,'[VD= refinement not yet supported.').
3144
3145		translate_csp_ref_style(Style,RefStyle) :- (csp_ref_style(Style,RefStyle) -> true ;
3146		add_error_fail(csp,'Unknown refinement style: ',Style)).
3147
3148		:- use_module(extrasrc(refinement_checker),[in_situ_ref_search/5]).
3149
3150		% tcltk_csp_in_situ_refinement('P','Q',R,0,1000). tcltk_csp_in_situ_refinement('Q','P',R,1000).
3151		tcltk_csp_in_situ_refinement(ImplProcess,AbsProcess,ResTrace,Style,MaxNrOfNewNodes) :-
3152		add_csp_process_id(ImplProcess,ImplNodeID),
3153		add_csp_process_id(AbsProcess,SpecNodeID),
3154		translate_csp_ref_style(Style,RefStyle),
3155		in_situ_ref_search(ImplNodeID,SpecNodeID,ResTrace,RefStyle,MaxNrOfNewNodes).
3156
3157		:- use_module(probcspsrc(haskell_csp),[get_csp_assertions/1,translate_csp_assertion/2]).
3158
3159		tcltk_check_csp_assertions(List,Summary) :- get_csp_assertions(Assertions),
3160		treat_csp_ass(Assertions,List,0,0,0,Summary). % TO DO: display _List
3161
3162		treat_csp_ass([],[],T,F,U,[total/Tot, true/T, false/F, unknown/U]) :- Tot is T+F+U.
3163		treat_csp_ass([Assertion|T],['='(PP,Ok)|TPP],True,False,U,Summary) :- !,
3164		(checkAssertion(Assertion,PP,_,Ok,_)
3165		-> U1=U, (Ok=true -> T1 is True+1, F1=False ; T1=True, F1 is False+1)
3166		; U1 is U+1, T1=True, F1=False,Ok=unknown),
3167		treat_csp_ass(T,TPP,T1,F1,U1,Summary).
3168		treat_csp_ass([H|T],TP,T1,F1,U,Summary) :- add_error(treat_csp_ass,'Unknown CSP assertion: ',H),
3169		U1 is U+1, treat_csp_ass(T,TP,T1,F1,U1,Summary).
3170
3171		% assertModelCheckExt(False,val_of(P3,src_span(25,8,25,10,562,2)),DeadlockFree,F)
3172
3173		:- use_module(extrasrc(refinement_checker),[in_situ_model_check/5, reset_refinement_checker/0]).
3174
3175		run_assertion_check(assertModelCheckExt(Negated,Spec,Type,ModelStyle),Negated,ResTrace) :-
3176		haskell_csp_analyzer: compile_body(Spec,'assertModelCheck',[],[],CSpec),
3177		debug_println(9,assertModelCheckExt(Negated,CSpec,Type,ModelStyle)),
3178		add_csp_general_process_id(CSpec,SpecNodeID),
3179		translate_csp_ref_style(ModelStyle,RefStyle),
3180		in_situ_model_check(SpecNodeID,ResTrace,Type,RefStyle,10000000),
3181		formatsilent('Result trace for assertModelCheck: ~w~n',[ResTrace]).
3182		run_assertion_check(assertModelCheck(Negated,Spec,Style),Negated,ResTrace) :-
3183		run_assertion_check(assertModelCheckExt(Negated,Spec,Style,'FailureDivergence'),Negated,ResTrace).
3184		run_assertion_check(assertRef(Negated,Spec,Style,Impl,Span),Negated,ResTrace) :-
3185		haskell_csp_analyzer: compile_body(Spec,'assertRef',[],[],CSpec),
3186		haskell_csp_analyzer: compile_body(Impl,'assertRef',[],[],CImpl),
3187		debug_println(9,assertRef(Negated,CSpec,Style,CImpl,Span)),
3188		add_csp_general_process_id(CSpec,SpecNodeID),
3189		add_csp_general_process_id(CImpl,ImplNodeID),
3190		translate_csp_ref_style(Style,RefStyle),
3191		refinement_checker:in_situ_ref_search(ImplNodeID,SpecNodeID,ResTrace,RefStyle,10000000).
3192		run_assertion_check(assertLtl(Negated,Spec,FormulaAsAtom,_Span),Negated,ResTrace) :-
3193		add_csp_process_id_normalized(Spec,'assertLtl',CSpec,CSpecNodeID),
3194		%% print(add_csp_general_process_id(Spec,CSpec,SpecNodeID)),nl,
3195		tcltk_reset,
3196		ltl_model_check_with_ce1(CSpec,FormulaAsAtom,-1,specific_node(CSpecNodeID),Result),
3197		translate_ltl_result(Result,ResTrace),
3198		debug_println(9,ltl_result(Negated,CSpec,CSpecNodeID,FormulaAsAtom,Result)).
3199		run_assertion_check(assertCtl(Negated,Spec,FormulaAsAtom,_Span),Negated,ResTrace) :-
3200		add_csp_process_id_normalized(Spec,'assertCtl',CSpec,CSpecNodeID),
3201		tcltk_reset,
3202		ctl_model_check_with_ce(CSpec,FormulaAsAtom,-1,specific_node(CSpecNodeID),Result,Trace),
3203		debug_println(9,ctl_result(Negated,CSpec,CSpecNodeID,FormulaAsAtom,Result)),
3204		translate_ctl_result(Result,Trace,ResTrace).
3205
3206		checkAssertion(Assertion,PP,Negated,Ok,ResTrace) :-
3207		(silent_mode(on) -> true
3208		; print('CHECKING '),
3209		translate_csp_assertion(Assertion,PP),
3210		print(PP),nl
3211		),
3212		debug_println(9,checkAssertion(Assertion)),
3213		reset_refinement_checker,
3214		(run_assertion_check(Assertion,Negated,ResTrace)
3215		-> debug_println(9,result(ResTrace)),
3216		(ResTrace=no_counter_example
3217		-> (Negated = 'False' -> Ok=true
3218		; %add_error(check_assertRef,'Assertion FAILS (expected refinement not to hold): ',PP),
3219		Ok=false)
3220		; (ResTrace=[interrupted|_]
3221		-> Ok=interrupted
3222		; (Negated = 'False' -> %add_error(check_assertRef,'Assertion FAILS: ',PP),
3223		Ok=false ; Ok=true)
3224		)
3225		),
3226		(Ok=true -> printsilent('OK'),nls
3227		; Ok=interrupted -> print('*** Execution interrupted by user ***'),nl
3228		; print('*** FALSE ***'),nl
3229		)
3230		; add_error_fail(checkAssertion,'Internal Error, Assertion Checking Failed for: ',PP)
3231		).
3232
3233		add_csp_process_id_normalized(Spec,Functor,CSpec,CSpecNodeID) :-
3234		% stripping out the src_span info
3235		haskell_csp_analyzer: clear_span(Spec,SpecNoSpan),
3236		haskell_csp_analyzer: compile_body(SpecNoSpan,Functor,[],[],CSpec),
3237		add_csp_general_process_id(CSpec,CSpecNodeID).
3238
3239		translate_ltl_result(ok,Res) :- !,
3240		Res = no_counter_example.
3241		translate_ltl_result(no,Res) :- !,
3242		Res = no.
3243		translate_ltl_result(ce(Atom),Res) :-
3244		!, % we have a counter-example for the LTL formula
3245		Res=Atom.
3246		translate_ltl_result(interrupted,Res) :-
3247		!,
3248		Res=[interrupted].
3249		translate_ltl_result(Status,_Res) :-
3250		add_error_fail(ltl_assertions_result, 'Internal Error: unknown LTL assertion result ', Status).
3251
3252		translate_ctl_result(true,_Trace,ResTrace) :- !,
3253		ResTrace = no_counter_example.
3254		translate_ctl_result(false,ce(Atom),ResTrace) :- !,
3255		ResTrace = Atom.
3256		translate_ctl_result(interrupted,_TRace,ResTrace) :-
3257		!,
3258		ResTrace=[interrupted].
3259		translate_ctl_result(Status,_Trace,_ResTrace) :-
3260		add_error_fail(ctl_assertions_result, 'Internal Error: unknown CTL assertion result ', Status).
3261
3262
3263		tcltk_check_csp_assertion(Assertion,CSPFile,Negated,Result) :-
3264		tcltk_check_csp_assertion(Assertion,CSPFile,Negated,_PlTerm,Result).
3265
3266		tcltk_check_csp_assertion(Assertion,CSPFile,Negated,PlTerm,Result) :-
3267		parse_single_csp_declaration(Assertion,CSPFile,PlTerm),
3268		checkAssertion(PlTerm,_PP,Negated,_Ok,Result).
3269
3270		:- public tcltk_play_ltl_ctl_counterexample_trace/4.
3271		tcltk_play_ltl_ctl_counterexample_trace(Assertion,CSPFile,Type,FairnessChecked) :-
3272		announce_event(play_counterexample),
3273		( Type == ltl -> Functor = assertLtl
3274		; Type == ctl -> Functor = assertCtl
3275		; add_error_fail(ltl_ctl_counterexample, 'Internal Error: Model checker type unknown: ',Type)),
3276		% constructing the prolog declaration term
3277		PlDeclTerm =.. [Functor,_Negated,Spec,FormulaAsAtom,_Span],
3278		parse_single_csp_declaration(Assertion,CSPFile,PlDeclTerm),
3279		haskell_csp_analyzer: clear_span(Spec,SpecNoSpan),
3280		haskell_csp_analyzer: compile_body(SpecNoSpan,'assertLtl',[],[],CSpec),
3281		% parsing and preprocessing the LTL/CTL formula
3282		parse_and_preprocess_formula(FormulaAsAtom,Type,PF),
3283		(is_fairness_implication(PF) -> FairnessChecked='yes'; FairnessChecked='no'),
3284		% need to reset history and current state before loading the counter-example
3285		tcltk_reset,
3286		tcltk_play_counterexample(Type,CSpec,PF).
3287
3288		tcltk_play_counterexample(ltl,Spec,Formula) :- !,
3289		tcltk_play_ltl_counterexample(Spec,Formula).
3290		tcltk_play_counterexample(ctl,Spec,Formula) :- !,
3291		tcltk_play_ctl_counterexample(Spec,Formula).
3292		tcltk_play_counterexample(Type,Spec,Formula) :-
3293		add_error_fail(ltl_ctl_counterexample, 'Internal Error: Unknown domain type: ', (Type,Spec,Formula)).
3294
3295		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3296
3297
3298		%%%% Parse and get LTL formulas from LTL File %%%%
3299		get_ltl_formulas_from_file(Filename,Text) :-
3300		parse_ltlfile(Filename, Formulas), print(Formulas),nl,
3301		translate_ltl_formulas(Formulas,Text).
3302
3303		translate_ltl_formulas(Formulas,Text) :-
3304		maplist(translate_ltl_formula,Formulas,Strings),
3305		haskell_csp: concatenate_string_list(Strings,Text).
3306
3307		translate_ltl_formula(formula(_Name,Formula),Text) :- !,
3308		pp_ltl_formula(Formula,T),
3309		string_concatenate(T,'$',Text).
3310		translate_ltl_formula(F,'') :- add_error(get_ltl_formulas_from_file,'Illegal formula: ',F).
3311
3312
3313		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3314
3315
3316		tcltk_explore_csp_process(ProcString,SpecNodeID) :-
3317		haskell_csp: parse_single_csp_expression(ltl,ProcString,Res),
3318		haskell_csp_analyzer: clear_span(Res,ResNoSpan),
3319		haskell_csp_analyzer: compile_body(ResNoSpan,'assertLtl',[],[],CRes),
3320		add_csp_general_process_id(CRes,SpecNodeID),
3321		refinement_checker:dfs_check(SpecNodeID,_ResTrace,false,false).
3322
3323		tcltk_visualize_csp_process(SpecNodeID,F) :-
3324		visualize_graph: tcltk_print_csp_process_states_for_dot(F,SpecNodeID).
3325
3326		:- dynamic nr_csp_process_state/1.
3327		get_csp_process_stats(NrNodes) :-
3328		assertz(nr_csp_process_state(0)),
3329		count_nodes,
3330		nr_csp_process_state(NrNodes),
3331		retractall(nr_csp_process_state(_)).
3332
3333		count_nodes :-
3334		refinement_checker: dvisited(_NodeID),
3335		nr_csp_process_state(NrNodes),
3336		NewNrNodes is NrNodes +1,
3337		retractall(nr_csp_process_state(_)),
3338		assertz(nr_csp_process_state(NewNrNodes)),
3339		fail.
3340		count_nodes.
3341
3342		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3343
3344		tcltk_machine_has_assertions :-
3345		( b_get_static_assertions_from_machine([_|_]); b_get_dynamic_assertions_from_machine([_|_]) ), !.
3346
3347		tcltk_unique_top_level_operation(Name) :- b_top_level_operation(Name),
3348		\+ (b_top_level_operation(N2), N2 \= Name).
3349
3350		tcltk_top_level_operations(list(Res)) :-
3351		findall(Name,b_top_level_operation(Name),Names),
3352		length(Names,L),
3353		(L>5 -> sort(Names,Res) ; Res=Names).
3354
3355		tcltk_get_vacuous_guards(list(R)) :-
3356		eclipse_interface:get_vacuous_guards(L), % to do: add source column
3357		(L=[] -> R = ['No vacuous guards']
3358		; R=L).
3359
3360		tcltk_get_vacuous_invariants(list(L)) :-
3361		eclipse_interface:get_vacuous_invariants(LP),
3362		(LP=[] -> L = ['No vacuous invariants']
3363		; maplist(translate:translate_bexpression,LP,L)).
3364
3365		tcltk_get_vacuous_invariants_table(list([list(['LHS','Op','RHS','Source'])|L])) :-
3366		eclipse_interface:get_vacuous_invariants(LP),
3367		LP \= [], !,
3368		maplist(get_expr_and_source,LP,L).
3369		tcltk_get_vacuous_invariants_table(list(['No vacuous invariants'])).
3370
3371		:- use_module(translate,[translate_bexpression_with_limit/3]).
3372		:- use_module(error_manager,[get_tk_table_position_info/2]).
3373		get_expr_and_source(P,list([TS1,Op,TS2,Src])) :-
3374		decompose(P,LHS,Op,RHS),
3375		translate_bexpression_with_limit(LHS,150,TS1),
3376		translate_bexpression_with_limit(RHS,60,TS2),
3377		get_tk_table_position_info(P,Src).
3378
3379		decompose(b(implication(LHS,RHS),pred,_),LHS,'=>',RHS) :- !.
3380		decompose(b(disjunction(LHS,RHS),pred,_),LHS,'or',RHS) :- !.
3381		decompose(LHS,LHS,'?',b(truth,pred,[])).
3382
3383
3384		% -------------------
3385
3386
3387		:- use_module(extrasrc(mcts_game_play), [mcts_auto_play/4, mcts_auto_play_available/0]).
3388
3389		tcltk_mcts_auto_play :- tcltk_mcts_auto_play(_).
3390		tcltk_mcts_auto_play(TransID) :-
3391		mcts_auto_play_available,
3392		current_state_id(CurID),
3393		mcts_auto_play(CurID,ActionAsTerm,TransID,State2),
3394		(tcltk_perform_action(CurID,ActionAsTerm,TransID,State2)
3395		-> true
3396		; add_error(tcltk_mcts_auto_play,'Cannot perform chosen action:',ActionAsTerm),fail).