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