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