1		% (c) 2009-2024 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(eclipse_interface,
6		[
7		clear_loaded_machines/0,
8		clear_loaded_machines_wo_errors/0,
9		set_application_type/1, % tell ProB wether it is being controlled via ProB1/Rodin or ProB2
10
11		load_b_file/1, load_b_file/2,
12		load_prob_file/1, load_prob_file/2,
13		load_eventb_file/1,
14		load_tla_file/1,
15
16		find_shortest_trace_to_current_state/1,
17		find_shortest_trace_to_current_state2/2,
18
19		do_modelchecking/4, % for ProB1 for Rodin
20		do_ltl_modelcheck/6,
21
22		getAllOperations/1, % deprecated, remove in 2.0
23		get_machine_objects/5,
24
25		getErrorMessages/2,
26		get_state_errors/2,
27
28		getCurrentStateID/1,
29		getOperationParameterNames/2, % deprecated, remove in 2.0
30
31		% getCurrentStateValues/2, no longer exists ??!
32		getStateValues/2,
33
34		test_boolean_expression_in_node/2, test_boolean_expression_in_node/3,
35
36		setCurrentState/1,
37		computeOperationsForState/2, % Used in ProB 1.0
38
39		evaluate_expression/2,
40
41		%in contrast to evaluate_expression, it supports predicates and does typing
42		evaluate_raw_expression/3,
43		evaluate_raw_expressions/3,
44
45		sap_find_test_path/4,
46		execute_custom_operations/6,
47
48		evaluation_get_top_level/1,
49		evaluation_expand_formula/3,
50		evaluation_get_values/3,
51		evaluation_insert_formula/3,
52
53		deadlock_freedom_check/1,
54		deadlock_freedom_check/2,
55		invariant_check/2,
56
57		refinement_check/2,
58
59		cbc_static_assertion_violation_checking/1,
60		cbc_dynamic_assertion_violation_checking/1,
61		get_vacuous_invariants/1, get_vacuous_guards/1,
62
63		quick_describe_unsat_properties/1,
64		find_state_satisfying_predicate/2
65		]).
66
67		:- use_module(module_information).
68		:- module_info(group,cli).
69		:- module_info(description,'This module provides the Prolog interface to Java and other languages (usually called via socket server).').
70
71		:- use_module(library(system),[environ/2]).
72		:- use_module(library(lists)).
73
74		:- use_module(error_manager).
75		:- use_module(self_check).
76		:- use_module(bsyntaxtree).
77		:- use_module(version).
78		:- use_module(eventhandling,[announce_event/1]).
79		:- use_module(tools, [safe_atom_codes/2]).
80
81		:- use_module(model_checker).
82
83		:- use_module(b_global_sets,[enum_global_type_limited/2]).
84		:- use_module(translate).
85		:- use_module(store).
86
87		:- use_module(extrasrc(bvisual2),[bv_get_top_level/1, bv_expand_formula/3, bv_get_values/3, bv_insert_formula/3]).
88
89		:- use_module(library(codesio)).
90
91		:- use_module(state_space,[visited_expression/2, visited_expression_id/1]).
92		:- use_module(tcltk_interface).
93
94
95		:- use_module(b_state_model_check,[cbc_deadlock_freedom_check/3]).
96
97		:- use_module(extension('user_signal/user_signal'), [user_interruptable_call_det/2]).
98
99		%:- use_module(extension('counter/counter'), [get_counter/2]).
100		:- use_module(prob2_interface, [get_state/2]).
101
102
103		:- use_module(preferences,[set_prob_application_type/1]).
104		set_application_type(T) :- % Note: can also be set as probcli option
105		set_prob_application_type(T). % T can be tcltk, probcli, prob2, rodin,...
106
107		/* ------------------------- */
108		/* Machine Loading Interface */
109		/* ------------------------- */
110
111		:- use_module(specfile,[b_or_z_mode/0,set_animation_mode/1,set_animation_minor_mode/1,animation_mode/1,
112		set_currently_opened_b_file/1,
113		set_currently_opening_file/1,
114		set_failed_to_open_file/1, animation_minor_mode/1]).
115		:- use_module(bmachine_construction,[check_machine/4, get_constructed_machine_name/2]).
116		:- use_module(probltlsrc(ltl),[ltl_model_check_with_ce/4,ltl_formula_structure/3]).
117		:- use_module(probltlsrc(ltl_tools),[typecheck_temporal_formula/3]).
118		:- use_module(tcltk_interface, [find_shortest_trace_to_node/4]).
119
120		:- use_module(state_space).
121		:- use_module(bmachine).
122
123
124		%:- use_module(preferences,[reset_all_temporary_preferences/0]).
125		clear_loaded_machines :-
126		clear_loaded_machines_wo_errors,
127		reset_errors,
128		% now done via event-handling: reset_all_temporary_preferences,
129		garbage_collect_atoms,!. % reclaim atoms if possible
130		clear_loaded_machines :- add_error(clear_loaded_machines,'clear_loaded_machines Failed').
131
132		% new profiler
133		%:- use_module('../extensions/profiler/profiler.pl').
134
135		% old profiler
136		%:- use_module(runtime_profiler,[reset_runtime_profiler/0]).
137
138		:- use_module(eventhandling, [announce_event/1]).
139		clear_loaded_machines_wo_errors :-
140		announce_event(reset_specification),
141		announce_event(clear_specification).
142		% Now done via event_handling: reduce_graph_reset reset_runtime_profiler, reset_refinement_checker state_space_initialise, b_machine_hierarchy:reset_hierarchy, b_interpreter:reset_b_interpreter, reset_model_checker haskell_csp:clear_cspm_spec, b_machine_reset,
143		% reset_dynamics, % new profiler
144		% reset_eval_strings.
145
146
147		:- use_module(debug,[debug_println/2]).
148		:- use_module(parsercall,[call_tla2b_parser/1, tla2prob_filename/2]).
149		load_tla_file(Filename) :-
150		call_tla2b_parser(Filename),
151		tla2prob_filename(Filename,GeneratedProbFile),
152		debug_println(10,loading_generated_prob_file(GeneratedProbFile)),
153		load_prob_file(GeneratedProbFile),
154		%load_b_file(GeneratedBFile),
155		debug_println(10,set_animation_minor_mode(tla)),
156		set_animation_minor_mode(tla). % TO DO: set before loading as parameter to load_prob_file ?
157		load_b_file(Filename) :- load_b_file(Filename,[]).
158		load_b_file(Filename,Options) :-
159		clear_loaded_machines_wo_errors,
160		set_animation_mode(b),
161		set_currently_opening_file(Filename),
162		(bmachine:b_load_machine_from_file(Filename,Options) % we can pass release_java_parser flag here
163		-> set_currently_opened_b_file(Filename)
164		; set_failed_to_open_file(Filename),fail).
165
166		load_prob_file(Filename) :- load_prob_file(Filename,[]).
167		load_prob_file(Filename,Options) :- % one option is use_fastread
168		clear_loaded_machines_wo_errors,
169		set_animation_mode(b),
170		set_currently_opening_file(Filename),
171		(bmachine:b_load_machine_probfile(Filename,Options)
172		-> set_currently_opened_b_file(Filename)
173		; set_failed_to_open_file(Filename),fail).
174
175		load_eventb_file(Filename) :-
176		clear_loaded_machines_wo_errors,
177		set_animation_mode(b), set_animation_minor_mode(eventb),
178		set_currently_opening_file(Filename),
179		(b_load_eventb_project(Filename)
180		-> set_currently_opened_b_file(Filename)
181		; set_failed_to_open_file(Filename),fail
182		).
183
184
185		get_event_infos(TransId,Infos) :-
186		findall(Info, transition_info(TransId,Info), Infos1),
187		filter_transition_infos(Infos1,Infos).
188
189		filter_transition_infos([],[]).
190		filter_transition_infos([I|Irest],[O|Orest]) :-
191		filter_transition_info(I,O),
192		filter_transition_infos(Irest,Orest).
193
194		filter_transition_info(event(StackI),event(StackO)) :- !,
195		filter_event_stack(StackI,StackO).
196		filter_transition_info(I,I).
197
198		filter_event_stack([],[]).
199		filter_event_stack([event(Name,Params)|Irest],[event(Name,Strings)|Orest]) :-
200		translate_bvalue_l(Params,Strings),
201		filter_event_stack(Irest,Orest).
202
203		translate_bvalue_l([],[]).
204		translate_bvalue_l([V|Vrest],[S|Srest]) :-
205		translate_bvalue(V,S),
206		translate_bvalue_l(Vrest,Srest).
207
208
209		:- use_module(prob2_interface,[do_modelchecking/5]).
210		% still used by ProB1 for Rodin:
211		%! do_modelchecking(+Time,+Options,-Result,-Stats)
212		do_modelchecking(Time, Options, Result, StatsRes) :-
213		MaxNumberOfStatesToCheck=100000,
214		do_modelchecking(MaxNumberOfStatesToCheck, Time, Options, Result, StatsRes).
215
216		% Mode is starthere, init, checkhere
217		% example call:
218		% XX=identifier(none,xx), Nr=integer(none,4), eclipse_interface:do_ltl_modelcheck(globally(ap(bpred(less(unknown,XX,Nr)))),500,init,Atomics,Structure,Result)
219		do_ltl_modelcheck(Formula,Max,Mode,Atomics,Structure,Result) :-
220		typecheck_temporal_formula(Formula,TypeCheckedFormula,Status),
221		( Status=ok ->
222		ltl_formula_structure(TypeCheckedFormula,Atomics,Structure),
223		ltl_model_check_with_ce(TypeCheckedFormula,Max,Mode,Result1),
224		ltl_adapt_operations(Result1,Result)
225		;
226		Atomics=[], Structure=[],
227		Result=typeerror([])).
228
229		ltl_adapt_operations(counterexample(CE1,LoopEntry,PathToCE1), counterexample(CE,LoopEntry,PathToCE)) :- !,
230		filter_ops_and_ids(PathToCE1,root,PathToCE),
231		ltl_adapt_ce(CE1,CE).
232		ltl_adapt_operations(Result,Result).
233
234		ltl_adapt_ce([],[]).
235		ltl_adapt_ce([atom(State,Evals,OpTuple)|Irest],[atom(State,Evals,Transition)|Orest]) :-
236		ltl_adapt_ce2(OpTuple,State,Transition),
237		ltl_adapt_ce(Irest,Orest).
238
239		ltl_adapt_ce2(none,_State,none).
240		ltl_adapt_ce2((TransId,Action,DstId),State,Transition) :-
241		create_operation_term(TransId,Action,State,DstId,Transition).
242
243
244		find_shortest_trace_to_current_state(TraceStrings) :-
245		find_shortest_trace_to_current_state2(TraceStrings, _).
246
247		find_shortest_trace_to_current_state2(TraceStrings, StateIDs) :-
248		current_state_id(ID),
249		find_shortest_trace_to_node(root,ID,TraceIds,StateIDs),
250		extract_term_trace_from_transition_ids(TraceIds,Trace),
251		translate_events(Trace,TraceStrings).
252
253
254		/* ------------------ */
255		/* getErrorMessages/1 */
256		/* ------------------ */
257		/* Returns a list of strings containing all error messages (of the error_manager).
258		Clears all the errors. Returns the empty list if no errors occurred since
259		the last call to getErrorMessages.
260		*/
261
262		getErrorMessages(WarningsOnly,ListOfErrMsgs) :-
263		(real_error_occurred -> WarningsOnly = false ; WarningsOnly = true),
264		(get_all_errors_and_reset(ListOfErrMsgs) -> true ; ListOfErrMsgs=[]).
265
266
267		/**
268		get_state_errors(+StateId,-Errors)
269
270		Takes a id for a given state in the state space and produces a list of all
271		state based errors.
272
273		#### called by:
274		* ProB Plugin: GetStateBasedErrorsCommand
275		*/
276		get_state_errors(StateId,Errors) :-
277		findall(E, (state_error(StateId,_,E),E \== invariant_violated), Errs),
278		convert_errors(Errs,Errors).
279		:- use_module(error_manager,[extract_span_description/2]).
280		convert_errors([],[]).
281		convert_errors([Error|InRest],[error(Event,Short,Long)|OutRest]) :-
282		( Error = eventerror(Event,EError,Trace) ->
283		translate_event_error(EError,Short),
284		explain_event_trace(Trace,LongStr,_Span),
285		safe_atom_codes(Long,LongStr)
286		;
287		(get_event_from_state_error(Error,Event) -> true
288		; Event = '*unknown*' % we don't know which event is responsible
289		),
290		translate_state_error(Error,Short),
291		explain_state_error(Error,_Span,LongStr),
292		safe_atom_codes(Long,LongStr)
293		),
294		convert_errors(InRest,OutRest).
295
296		get_event_from_state_error(abort_error(TYPE,_Msg,_ErrTerm,ErrorContext),Event) :-
297		(get_error_event_from_context(ErrorContext,Event) -> true ; functor(TYPE,Event,_)).
298		get_error_event_from_context(span_context(_,Context),Event) :-
299		get_error_event_from_context(Context,Event).
300		get_error_event_from_context(operation(Event,_State),Event).
301
302		/* ---------------------------- */
303		/* Syntax Information Interface */
304		/* ---------------------------- */
305
306		getAllOperations(L) :-
307		(b_or_z_mode
308		-> findall(OperationName, b_top_level_operation(OperationName), L)
309		; L=[]). % FIXME: provide list for CSP-M
310
311
312		get_machine_objects(Sections,SetElements,Constants,Variables,Operations) :-
313		b_get_animated_sections(Sections),
314		findall(TId,
315		( enum_global_type_limited(fd(Nr,Set),_),
316		translate_bvalue(fd(Nr,Set),String),
317		create_texpr(identifier(String),global(Set),[],TId)),
318		SetElements),
319		b_get_machine_constants(Constants),
320		b_get_machine_variables(Variables),
321		b_get_promoted_machine_operations(Operations1),
322		maplist(remove_op,Operations1,Operations).
323		remove_op(TId,NTId) :-
324		remove_bt(TId,identifier(Id),identifier(NId),NTId),
325		remove_op2(Id,NId).
326		remove_op2(op(Op),Op) :- !.
327		remove_op2(Op,Op).
328
329		/* ------------------- */
330		/* Animation Interface */
331		/* ------------------- */
332
333		/* get the ID of the current state */
334		getCurrentStateID(CurID) :-
335		current_state_id(CurID).
336
337		setCurrentState(ID) :- current_state_id(ID),!. % no need to jump
338		setCurrentState(ID) :- /* jumps to the given node; can be backtracked */
339		visited_expression_id(ID),
340		tcltk_interface:tcltk_goto_state(jump,ID).
341
342		:- use_module(specfile,[state_corresponds_to_initialised_b_machine/2]).
343
344		test_boolean_expression_in_node(ResID,BoolExpr) :-
345		test_boolean_expression_in_node(ResID,BoolExpr,'ProB1-Java in state').
346		test_boolean_expression_in_node(ResID,BoolExpr,Kind) :-
347	?	visited_expression(ResID,CurState),
348		(b_or_z_mode
349		-> state_corresponds_to_initialised_b_machine(CurState,CurBState)
350		; CurState = CurBState),
351		set_context_state(ResID,test_boolean_expression_in_node), % also sets it for external functions
352		call_cleanup(b_interpreter:b_test_boolean_expression_cs(BoolExpr,[],CurBState,Kind,ResID),
353		clear_context_state).
354
355		/* USED IN PROB 1.0*/
356		computeOperationsForState(StateID, OpsAndIDs) :- /* compute the enabled operations
357		(without the backtrack options) for a state ID which is not necessarily the current one */
358		visited_expression_id(StateID),
359		tcltk_interface:tcltk_compute_options(StateID,OpsSTAndIDs),
360		%print('OpsSTAndIDs: '),print(OpsSTAndIDs),nl,
361		(filter_ops_and_ids(OpsSTAndIDs,StateID,OpsAndIDs) -> true
362		; print(filter_ops_and_ids_failed(OpsSTAndIDs)),nl,fail).
363
364		/*
365		op(140,io,23,23,[[in(r14_1m)],'SetRoute',multi_span(460,35,460,71,16934,36,src_span(460,31,460,32,16930,1))],['{<< in(r14_1m) >>}','<< SetRoute >>','<< multi_span(460,35,460,71,16934,36,src_span(460,31,460,32,16930,1)) >>'],[],')
366		*/
367
368
369		getOperationParameterNames(Operation,Paras) :-
370		b_get_machine_operation_parameter_names(Operation,Paras).
371
372		filter_ops_and_ids([],_,[]).
373		filter_ops_and_ids([OpTuple|T],StateID,[FOp|FT]) :-
374		((OpTuple = (Id,OpTerm,Dst), create_operation_term(Id,OpTerm,StateID,Dst,FOp))
375		-> true
376		; print(filter_op_failed(OpTuple,StateID)),nl, FOp = ('?')),
377		filter_ops_and_ids(T,StateID,FT).
378
379		filter_op(TransId,OpTerm,Src,Dst,JavaOpTerm) :-
380		(animation_mode(cspm) ->
381		filter_op_csp(TransId,OpTerm,Src,Dst,JavaOpTerm)
382		;
383		filter_op1(TransId,OpTerm,Src,Dst,JavaOpTerm)).
384
385		filter_op1(TransId,OpTerm,Src,Dst,
386		op(TransId,Op,Src,Dst,Arguments,ArgumentsPretty,Infos,State)) :-
387		extract_args_and_return_values(OpTerm,Op,Arguments),
388		get_state(Dst,BState), translate:translate_bstate(BState,State),
389		prettyprint(Arguments,ArgumentsPretty),
390		get_event_infos(TransId,Infos).
391
392		filter_op_csp(TransId,OpTerm,Src,Dst,op(TransId,Op,Src,Dst,Arguments,ArgumentsPretty,Infos,CSPState)) :-
393		extract_csp_args_and_return_values(OpTerm,Op,Arguments),
394		translate:translate_event(OpTerm,PPEvent),
395		tools: split_atom(PPEvent,['.','!'],[_Op|ArgumentsPretty]),
396		get_state(Dst,CSPState),
397		get_event_infos(TransId,Infos).
398
399		extract_csp_args_and_return_values(io(Args,ChName,_SPAN),ChName,Args).
400		extract_csp_args_and_return_values(start_cspm(Name),Name,[]).
401		extract_csp_args_and_return_values(start_cspm_MAIN,'start_cspm_MAIN',[]).
402		extract_csp_args_and_return_values(tick(_),tick,[]).
403		extract_csp_args_and_return_values(tau(_),tau,[]).
404		extract_csp_args_and_return_values(_OP,'?',[]).
405
406		prettyprint([],[]).
407		prettyprint([H|T],[P|R]) :- translate_bvalue(H,P), prettyprint(T,R).
408
409		:- dynamic result_warning_emitted/0.
410
411		extract_args_and_return_values(Term,OpName,Arguments) :-
412		( Term='-->'(OpTerm,Results) ->
413		( result_warning_emitted -> true
414		;
415		print('Warning: results of operations are currently treated like arguments'),nl,
416		assertz(result_warning_emitted)),
417		append(Results,Args,Arguments)
418		; Term=OpTerm,Args=Arguments
419		),
420		OpTerm =.. [OpName|Args].
421
422
423
424		% returns all variables and their values of the given state as a list
425		% - constants and variables that are defined for the machine but
426		% not present in the given state get the value '?'
427		% - for each variable a term of the form
428		% binding(Id,Value,PPValue,Tag)
429		% is in the result list, where
430		% Id is the variable's name,
431		% Value is its value a Prolog term
432		% PPValue is its pretty-printed value
433		% NOTE: Tag no longer generated: TO DO REVIEW:
434		% Tag is one of (cst,var,unknown), depending on whether the
435		% variable is a constant, a variable or not defined in the
436		% machine description but present in the state
437		getStateValues(CurID,VariableState) :- /* get variable values */
438		get_state(CurID,CurBState),
439		findall( binding(Id,nope,PPValue),
440		(member(bind(Id,Value),CurBState),
441		(translate_bvalue(Value,PPValue) -> true ; PPValue='**pretty-print failed**')),
442		VariableState).
443
444		/* ------------------------------- */
445
446		/* evaluates an expression in Prolog format and computes the result in the current state */
447		evaluate_expression(Expression,Result) :-
448		current_expression(_CurID,CurState),
449		b_interpreter:b_compute_expression_nowf(Expression,[],CurState,Result,'ProB1-Java',0).
450
451
452
453		%%
454		% Code for invariant debug
455		%
456
457		:- use_module(probsrc(eval_interface),[get_value_string_of_formula/5]).
458
459		evaluate_raw_expression(StateID, Raw, Val):-
460		bmachine:b_type_expression(Raw, [variables], _, TExpr, Errors),
461		( var(TExpr) ->
462		print(error_while_typing_raw_expression(Errors)),nl,
463		flush_output,
464		!,
465		fail
466		;
467		get_state(StateID, State),
468		get_value_string_of_formula(State, [], TExpr, 400, Val) % get_value_of_expression or predicate without wd errors
469		).
470
471		% called in ProB1 for Rodin: de.prob.core/src/de/prob/core/command/EvaluateRawExpressionsCommand.java
472		evaluate_raw_expressions(StateID, Raws, Vals):-
473		maplist(evaluate_raw_expression(StateID), Raws, Vals).
474
475
476
477		/* ------------------------- */
478		/* Execute Operation */
479		/* ------------------------- */
480
481		% MaxNrOfSolutions is the maximum number of solutions ProB returns. Also we should consider existing solutions if the Predicate holds.
482		%:- use_module(succeed_max,[succeed_max_call/2]).
483
484		:- use_module(bmachine,[assert_temp_typed_predicate/1,reset_temp_predicate/0]).
485		:- use_module(b_global_sets,[inline_prob_deferred_set_elements_into_bexpr/2]).
486		/* PROB 1.0 */
487		execute_custom_operations(CurID, OpName, ParsedPredicate, MaxNrOfSolutions, TOperations, Errors) :-
488		setCurrentState(CurID),
489
490		( (OpName = '$initialise_machine';OpName = '$setup_constants' ) -> Scope = [prob_ids(visible),variables];
491		b_top_level_operation(OpName),
492		b_get_machine_operation(OpName,_,Parameters,_),
493		Scope = [identifier(Parameters),prob_ids(visible),variables] % prob scope allows one to use identifiers for deferred set elements
494		),
495		(MaxNrOfSolutions<1
496		-> add_message(eclipse_interface,'execute_custom_operations MaxNrOfSolutions < 1: ',MaxNrOfSolutions)
497		; true),
498		bmachine:b_type_expression(ParsedPredicate, Scope, _, TypedPred, Errors),
499		inline_prob_deferred_set_elements_into_bexpr(TypedPred,CP),
500		assert_temp_typed_predicate(CP),
501		set_context_state(CurID,execute_custom_operations),
502		findall(TO, execute_custom_operation(CurID,OpName,TO,MaxNrOfSolutions), TOperations),
503		reset_temp_predicate,
504		clear_context_state.
505
506		% TO DO: check if we need to recompute the operation effect: if the ParsedPredicate is TRUE
507		% (TRUE = equal(none,integer(none,1),integer(none,1)) ) & MaxNrOfSolutions <=
508		% what has already been used previously, we can simply reuse transition from the state space
509
510		execute_custom_operation(CurID,OpName,Operation_op,Max) :-
511		visited_expression(CurID,InState),
512		specfile:compute_operation_effect_max(InState,OpName,Operation,NewState,_TransPathInfo,Max),
513		% logger:writeln_log(sol(OpName,NewState)), %%
514		tcltk_interface:add_trans_id(CurID,Operation,NewState,NewID,TransId),
515		% logger:writeln_log(ids(OpName,Operation,NewID,TransId)), %%
516		create_operation_term(TransId,Operation,CurID,NewID, Operation_op).
517
518
519
520		% create a term op(...) with infos for Java interface about an operation-transition
521		create_operation_term(TransId,Op,CurID,NewID, JavaOpTerm) :-
522		(filter_op(TransId,Op,CurID,NewID, JavaOpTerm) -> true
523		; add_error(eclipse_interface,'filter_op failed: ', filter_op(TransId,Op,CurID,NewID, JavaOpTerm)),fail).
524
525		/* ------------------------- */
526		/* SAP Testcase Generation */
527		/* ------------------------- */
528		:- use_module(cbcsrc(cbc_path_solver),[create_testcase_path/5]).
529
530		sap_find_test_path(Events,EndPredicate,Timeout,Operations) :-
531		type_predicate(EndPredicate,TypedPredicate),
532		(create_testcase_path(init,Events,TypedPredicate,Timeout,Trace) -> true ; Trace = []),
533		% Trace can be "timeout" or "interrupt", too
534		(is_list(Trace) -> op_tuples_to_full_operations(Trace,Operations) ; Operations=Trace).
535
536		op_tuples_to_full_operations([],[]).
537		op_tuples_to_full_operations([(Id,OpTerm,Src,Dst)|Trest],[Op|Orest]) :-
538		create_operation_term(Id,OpTerm,Src,Dst,Op),
539		op_tuples_to_full_operations(Trest,Orest).
540
541		type_predicate(Predicate,TypedPredicate) :-
542		b_type_expression(Predicate,[variables],pred,TypedPredicate,Errors),
543		add_all_perrors(Errors,[],sap_target_predicate_type_error),
544		no_real_perror_occurred(Errors).
545
546		/* ------------------------- */
547		/* Formula evaluation */
548		/* ------------------------- */
549		evaluation_get_top_level(Tops) :-
550		% Currently, we do not want to see the rodin information positons
551		% in the expression viewer
552		suppress_rodin_positions(CHNG),
553		bv_get_top_level(TopIds),
554		findall( top(Id,Label,Children),
555		( member(Id,TopIds), bv_expand_formula(Id,Label,Children) ),
556		Tops),
557		reset_suppress_rodin_positions(CHNG).
558		evaluation_expand_formula(Id,Label,Children) :-
559		% Currently, we do not want to see the rodin information positons
560		% in the expression viewer
561		suppress_rodin_positions(CHNG),
562		bv_expand_formula(Id,Label,Children),
563		reset_suppress_rodin_positions(CHNG).
564		evaluation_get_values(Ids,StateId,Values) :-
565		bv_get_values(Ids,StateId,Values).
566		evaluation_insert_formula(AST,ParentId,Id) :-
567		b_type_expression(AST,[variables],_,Typed,Errors),
568		% this also calls ast_cleanup; we could temporarily set OPTIMIZE_AST to false
569		( Errors == [] ->
570		bv_insert_formula(Typed,ParentId,Id)
571		;
572		add_error_and_fail(eclipse_interface,'Could not type-check AST','')).
573
574		/* ------------------------------- */
575		/* Find state satisfying predicate */
576		/* ------------------------------- */
577		:- use_module(b_state_model_check,[b_set_up_valid_state_with_pred/2]).
578		find_state_satisfying_predicate(Predicate,Result) :-
579		b_type_expression(Predicate,[variables],pred,TPredicate,Errors),
580		( Errors == [] ->
581		find_state_satisfying_predicate1(TPredicate,Result)
582		;
583		Result = errors(Errors)).
584		:- use_module(clpfd_interface,[catch_clpfd_overflow_call1/1]).
585		find_state_satisfying_predicate1(Predicate,Result) :-
586		user_interruptable_call_det(clpfd_interface:catch_clpfd_overflow_call1(
587		b_state_model_check:b_set_up_valid_state_with_pred(State,Predicate)),
588		InterruptResult),!,
589		( InterruptResult = interrupted ->
590		Result = interrupted
591		; State = time_out ->
592		Result = interrupted
593		;
594		Result = state_found(Transition,StateId),
595		create_helper_transition(root,find_valid_state,State,StateId,Transition)).
596		find_state_satisfying_predicate1(_Predicate,no_valid_state_found).
597
598
599		/* ------------------------- */
600		/* Check for deadlocks */
601		/* ------------------------- */
602
603		:- use_module(solver_interface, [call_with_smt_mode_enabled/1]).
604
605		deadlock_freedom_check(Result) :-
606		create_texpr(truth,pred,[],Predicate),
607		deadlock_freedom_check1(Predicate,Result).
608		deadlock_freedom_check(Predicate,Result) :-
609		b_type_expression(Predicate,[variables],pred,TPredicate,Errors),
610		( Errors == [] ->
611		deadlock_freedom_check1(TPredicate,Result)
612		;
613		Result = errors(Errors)).
614		deadlock_freedom_check1(Predicate,Result) :-
615		% always do a deadlock check with SMT mode enabled
616		call_with_smt_mode_enabled(deadlock_freedom_check2(Predicate,Result)).
617		deadlock_freedom_check2(Predicate,Result) :-
618		user_interruptable_call_det(clpfd_interface:catch_clpfd_overflow_call1(
619		b_state_model_check:cbc_deadlock_freedom_check(State,Predicate,0)),
620		InterruptResult),!,
621		( InterruptResult = interrupted ->
622		Result = interrupted
623		; State = time_out ->
624		Result = interrupted
625		;
626		Result = deadlock(Transition,StateId),
627		create_helper_transition(root,deadlock_check,State,StateId,Transition)).
628		deadlock_freedom_check2(_Predicate,no_deadlock_found).
629
630		create_helper_transition(SrcId,Op,DstState,DstId,Transition) :-
631		tcltk_interface:tcltk_add_new_transition_transid(SrcId,Op,DstId,DstState,[],TransId),
632		transition(SrcId,Action,TransId,DstId),!,
633		create_operation_term(TransId,Action,SrcId,DstId,Transition).
634
635
636		/* ------------------------------- */
637		/* Find values */
638		/* ------------------------------- */
639		%find_values(Commands,Predicate,MaxNumberSolutions,Solutions) :-
640		% setup_userdef_state_space(Commands,root,State,Ids,ConstantsId).
641
642		%setup_userdef_state_space2(copy_state(Id),CState,State,Ids,ConstantsId) :-
643		% visited_expression(Id,S),
644		% ( S=concrete_constants(Constants) ->
645		% (CState=root -> ConstantsId = S ; ConstantsId = CState),
646
647
648		/* ------------------------------- */
649		/* Check for invariant violations */
650		/* ------------------------------- */
651
652		invariant_check(all,Result) :-
653		findall(OpName,b_is_operation_name(OpName),Ops),
654		invariant_check2(Ops,Result).
655		invariant_check(ops(Ops),Result) :-
656		invariant_check2(Ops,Result).
657		invariant_check2(Ops,Result) :-
658		call_with_smt_mode_enabled(user_interruptable_call_det(invariant_check3(Ops,Res,[]), Status)),
659		(Status = interrupted -> Result = interrupted ; Result = Res).
660		invariant_check3([]) --> !.
661		invariant_check3([Op|Rest]) -->
662		invariant_check_for_single_op(Op),
663		invariant_check3(Rest).
664		:- use_module(clpfd_interface,[catch_clpfd_overflow_call1/1]).
665		invariant_check_for_single_op(OpName,In,Out) :-
666		( clpfd_interface:catch_clpfd_overflow_call1(
667		b_state_model_check:state_model_check_invariant(OpName,State1,Operation,State2)) ->
668		In = [counterexample(OpName,Trans1,Trans2)|Out],
669		atom_concat( invariant_check_ , OpName, RootTrans),
670		create_helper_transition(root, RootTrans,State1,StateId1,Trans1),
671		create_helper_transition(StateId1,Operation,State2,_StateId2,Trans2)
672		;
673		In = Out).
674
675		/* ------------------------------- */
676		/* CBC Refinement Checking */
677		/* ------------------------------- */
678		:- use_module(symbolic_model_checker(cbc_refinement_checks), [cbc_refinement_check/2]).
679		refinement_check(ResultsString,Result) :-
680		call_with_smt_mode_enabled(cbc_refinement_check(ResultsString,Result)).
681
682		/* ----------------------------- */
683		/* CBC Static Assertion Checking */
684		/* ----------------------------- */
685		:- use_module(b_state_model_check, [cbc_static_assertions_check/1, cbc_dynamic_assertions_check/1]).
686		cbc_static_assertion_violation_checking(Result) :-
687		user_interruptable_call_det(catch_clpfd_overflow_call1(cbc_static_assertions_check(State)),InterruptResult), !,
688		( InterruptResult = interrupted ->
689		Result = interrupted
690		; State = time_out ->
691		Result = interrupted
692		; State = no_counterexample_found ->
693		Result = no_counterexample_found
694		; functor(State,no_counterexample_exists,_) -> % arity is 3
695		Result = no_counterexample_exists
696		;
697		State = counterexample_found(RealState),
698		Result = counterexample_found(Transition,StateId),
699		transition_name(static,TransName),
700		create_helper_transition(root,TransName,RealState,StateId,Transition)).
701		cbc_dynamic_assertion_violation_checking(Result) :-
702		user_interruptable_call_det(catch_clpfd_overflow_call1(cbc_dynamic_assertions_check(State)),InterruptResult), !,
703		( InterruptResult = interrupted ->
704		Result = interrupted
705		; State = time_out ->
706		Result = interrupted
707		; State = no_counterexample_found ->
708		Result = no_counterexample_found
709		; functor(State,no_counterexample_exists,_) -> % arity is 0
710		Result = no_counterexample_exists
711		;
712		State = counterexample_found(RealState),
713		Result = counterexample_found(Transition,StateId),
714		transition_name(dynamic,TransName),
715		create_helper_transition(root,TransName,RealState,StateId,Transition)).
716
717		transition_name(dynamic,Name) :- animation_minor_mode(eventb),!,
718		Name = 'context_theorems_check'.
719		transition_name(dynamic,dynamic_asserion_check).
720		transition_name(static,Name) :- animation_minor_mode(eventb),!,
721		Name = 'invariant_theorems_check'.
722		transition_name(static,static_asserion_check).
723
724		/* ------------------------- */
725		/* Generate Visualizations */
726		/* ------------------------- */
727
728		get_vacuous_invariants(L) :-
729		findall(I,vacuous_invariant(I),L).
730
731		vacuous_invariant(Inv) :-
732		b_get_invariant_from_machine(Invariant),
733	?	b_interpreter:member_conjunct(Inv,Invariant,_),
734		get_texpr_expr(Inv,IE),get_disj_lhs(IE,LHS),
735		print('Checking vor vacuity: '), translate:print_bexpr(Inv),nl,
736	?	(test_boolean_expression_in_node(ResID,LHS,'vacuous invariant')
737		-> print(rhs_triggered_in_state(ResID)),nl,nl, % Implication/disjunction trigger in at least one state
738		fail
739		; print(' *** VACUOUS *** '),nl,nl
740		).
741
742		get_disj_lhs(implication(LHS,_),LHS).
743		get_disj_lhs(disjunction(LHS,_),NLHS) :- create_negation(LHS,NLHS).
744
745		get_vacuous_guards(L) :-
746		findall(G,vacuous_guard(_,G),L).
747
748		:- use_module(probsrc(tools_strings),[ajoin/2]).
749		vacuous_guard(OpName,Result) :-
750		get_guard_with_one_negated(OpName,Guard,Neg),
751		translate:translate_bexpression_with_limit(Guard,GuardTS),
752		format('Checking vor vacuity: ~w : ~w~n',[OpName,GuardTS]),
753		%translate:print_bexpr(Neg),nl,
754		(test_boolean_expression_in_node(ResID,Neg,'vacuous guard')
755		-> print(guard_individually_false_in(ResID)),nl,nl,
756		fail
757		; print(' *** VACUOUS *** '),nl,nl,
758		ajoin([OpName,' : ',GuardTS],Result)
759		).
760
761
762		:- use_module(b_operation_guards,[get_operation_enabling_condition/7]).
763		%:- use_module(b_ast_cleanup, [clean_up/3]).
764		:- use_module(b_interpreter_components,[construct_optimized_exists/3]).
765
766		% get a guard, by translating all parameters into existential quantifiers
767		get_guard_with_one_negated(OpName,SingleGuard,FullModifiedGuard) :-
768		get_operation_enabling_condition(OpName,Parameters,EnablingCondition,_BecomesSuchVars,_Precise,false,true),
769		% TO DO: partition; avoid lifting becomes_such_that conditions
770		% (in EventB the feasibility PO will ensure that Guard => BecomeSuchThat is ok)
771		negate_one_guard(EnablingCondition,SingleGuard,ModifiedEnablingCondition),
772		construct_optimized_exists(Parameters,ModifiedEnablingCondition,FullModifiedGuard).
773
774		:- use_module(probsrc(bsyntaxtree),[conjunction_to_list/2]).
775		negate_one_guard(Conjunct,SingleGuard,ModifiedConjunct) :-
776		conjunction_to_list(Conjunct,L),
777		append(Rest1,[SingleGuard|Rest2],L),
778		create_negation(SingleGuard,NegSingleGuard),
779		append(Rest1,[NegSingleGuard|Rest2],NewGuard), % TO DO: better treatment for well-definedness !?
780		conjunct_predicates(NewGuard,ModifiedConjunct).
781
782		:- use_module(b_interpreter, [tcltk_quick_describe_unsat_properties/2, tcltk_unsatisfiable_components_exist/0]).
783		quick_describe_unsat_properties(Res) :-
784		tcltk_unsatisfiable_components_exist
785		-> tcltk_quick_describe_unsat_properties(list(TRes),_Status), % sometimes this can be 'The properties were satisfiable' if tcltk_unsatisfiable_components_exist faulty
786		Res = unsat_properties(TRes) % TO DO: use Status to say unsat or unknown_properties
787		; Res = no_unsat_properties_found.
788		% TODO: integrate WD prover and Z3 bup core here