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