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