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		state_corresponds_to_initialised_b_machine(CurState,CurBState),
349		set_context_state(ResID,test_boolean_expression_in_node), % also sets it for external functions
350		call_cleanup(b_interpreter:b_test_boolean_expression_cs(BoolExpr,[],CurBState,Kind,ResID),
351		clear_context_state).
352
353		/* USED IN PROB 1.0*/
354		computeOperationsForState(StateID, OpsAndIDs) :- /* compute the enabled operations
355		(without the backtrack options) for a state ID which is not necessarily the current one */
356		visited_expression_id(StateID),
357		tcltk_interface:tcltk_compute_options(StateID,OpsSTAndIDs),
358		%print('OpsSTAndIDs: '),print(OpsSTAndIDs),nl,
359		(filter_ops_and_ids(OpsSTAndIDs,StateID,OpsAndIDs) -> true
360		; print(filter_ops_and_ids_failed(OpsSTAndIDs)),nl,fail).
361
362		/*
363		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)) >>'],[],')
364		*/
365
366
367		getOperationParameterNames(Operation,Paras) :-
368		b_get_machine_operation_parameter_names(Operation,Paras).
369
370		filter_ops_and_ids([],_,[]).
371		filter_ops_and_ids([OpTuple|T],StateID,[FOp|FT]) :-
372		((OpTuple = (Id,OpTerm,Dst), create_operation_term(Id,OpTerm,StateID,Dst,FOp))
373		-> true
374		; print(filter_op_failed(OpTuple,StateID)),nl, FOp = ('?')),
375		filter_ops_and_ids(T,StateID,FT).
376
377		filter_op(TransId,OpTerm,Src,Dst,JavaOpTerm) :-
378		(animation_mode(cspm) ->
379		filter_op_csp(TransId,OpTerm,Src,Dst,JavaOpTerm)
380		;
381		filter_op1(TransId,OpTerm,Src,Dst,JavaOpTerm)).
382
383		filter_op1(TransId,OpTerm,Src,Dst,
384		op(TransId,Op,Src,Dst,Arguments,ArgumentsPretty,Infos,State)) :-
385		extract_args_and_return_values(OpTerm,Op,Arguments),
386		get_state(Dst,BState), translate:translate_bstate(BState,State),
387		prettyprint(Arguments,ArgumentsPretty),
388		get_event_infos(TransId,Infos).
389
390		filter_op_csp(TransId,OpTerm,Src,Dst,op(TransId,Op,Src,Dst,Arguments,ArgumentsPretty,Infos,CSPState)) :-
391		extract_csp_args_and_return_values(OpTerm,Op,Arguments),
392		translate:translate_event(OpTerm,PPEvent),
393		tools: split_atom(PPEvent,['.','!'],[_Op|ArgumentsPretty]),
394		get_state(Dst,CSPState),
395		get_event_infos(TransId,Infos).
396
397		extract_csp_args_and_return_values(io(Args,ChName,_SPAN),ChName,Args).
398		extract_csp_args_and_return_values(start_cspm(Name),Name,[]).
399		extract_csp_args_and_return_values(start_cspm_MAIN,'start_cspm_MAIN',[]).
400		extract_csp_args_and_return_values(tick(_),tick,[]).
401		extract_csp_args_and_return_values(tau(_),tau,[]).
402		extract_csp_args_and_return_values(_OP,'?',[]).
403
404		prettyprint([],[]).
405		prettyprint([H|T],[P|R]) :- translate_bvalue(H,P), prettyprint(T,R).
406
407		:- dynamic result_warning_emitted/0.
408
409		extract_args_and_return_values(Term,OpName,Arguments) :-
410		( Term='-->'(OpTerm,Results) ->
411		( result_warning_emitted -> true
412		;
413		print('Warning: results of operations are currently treated like arguments'),nl,
414		assertz(result_warning_emitted)),
415		append(Results,Args,Arguments)
416		; Term=OpTerm,Args=Arguments
417		),
418		OpTerm =.. [OpName|Args].
419
420
421
422		% returns all variables and their values of the given state as a list
423		% - constants and variables that are defined for the machine but
424		% not present in the given state get the value '?'
425		% - for each variable a term of the form
426		% binding(Id,Value,PPValue,Tag)
427		% is in the result list, where
428		% Id is the variable's name,
429		% Value is its value a Prolog term
430		% PPValue is its pretty-printed value
431		% NOTE: Tag no longer generated: TO DO REVIEW:
432		% Tag is one of (cst,var,unknown), depending on whether the
433		% variable is a constant, a variable or not defined in the
434		% machine description but present in the state
435		getStateValues(CurID,VariableState) :- /* get variable values */
436		get_state(CurID,CurBState),
437		findall( binding(Id,nope,PPValue),
438		(member(bind(Id,Value),CurBState),
439		(translate_bvalue(Value,PPValue) -> true ; PPValue='**pretty-print failed**')),
440		VariableState).
441
442		/* ------------------------------- */
443
444		/* evaluates an expression in Prolog format and computes the result in the current state */
445		evaluate_expression(Expression,Result) :-
446		current_expression(_CurID,CurState),
447		b_interpreter:b_compute_expression_nowf(Expression,[],CurState,Result,'ProB1-Java',0).
448
449
450
451		%%
452		% Code for invariant debug
453		%
454
455		:- use_module(probsrc(eval_interface),[get_value_string_of_formula/5]).
456
457		evaluate_raw_expression(StateID, Raw, Val):-
458		bmachine:b_type_expression(Raw, [variables], _, TExpr, Errors),
459		( var(TExpr) ->
460		print(error_while_typing_raw_expression(Errors)),nl,
461		flush_output,
462		!,
463		fail
464		;
465		get_state(StateID, State),
466		get_value_string_of_formula(State, [], TExpr, 400, Val) % get_value_of_expression or predicate without wd errors
467		).
468
469		% called in ProB1 for Rodin: de.prob.core/src/de/prob/core/command/EvaluateRawExpressionsCommand.java
470		evaluate_raw_expressions(StateID, Raws, Vals):-
471		maplist(evaluate_raw_expression(StateID), Raws, Vals).
472
473
474
475		/* ------------------------- */
476		/* Execute Operation */
477		/* ------------------------- */
478
479		% MaxNrOfSolutions is the maximum number of solutions ProB returns. Also we should consider existing solutions if the Predicate holds.
480		%:- use_module(succeed_max,[succeed_max_call/2]).
481
482		:- use_module(bmachine,[assert_temp_typed_predicate/1,reset_temp_predicate/0]).
483		:- use_module(b_global_sets,[inline_prob_deferred_set_elements_into_bexpr/2]).
484		/* PROB 1.0 */
485		execute_custom_operations(CurID, OpName, ParsedPredicate, MaxNrOfSolutions, TOperations, Errors) :-
486		setCurrentState(CurID),
487
488		( (OpName = '$initialise_machine';OpName = '$setup_constants' ) -> Scope = [prob_ids(visible),variables];
489		b_top_level_operation(OpName),
490		b_get_machine_operation(OpName,_,Parameters,_),
491		Scope = [identifier(Parameters),prob_ids(visible),variables] % prob scope allows one to use identifiers for deferred set elements
492		),
493		(MaxNrOfSolutions<1
494		-> add_message(eclipse_interface,'execute_custom_operations MaxNrOfSolutions < 1: ',MaxNrOfSolutions)
495		; true),
496		bmachine:b_type_expression(ParsedPredicate, Scope, _, TypedPred, Errors),
497		inline_prob_deferred_set_elements_into_bexpr(TypedPred,CP),
498		assert_temp_typed_predicate(CP),
499		set_context_state(CurID,execute_custom_operations),
500		findall(TO, execute_custom_operation(CurID,OpName,TO,MaxNrOfSolutions), TOperations),
501		reset_temp_predicate,
502		clear_context_state.
503
504		% TO DO: check if we need to recompute the operation effect: if the ParsedPredicate is TRUE
505		% (TRUE = equal(none,integer(none,1),integer(none,1)) ) & MaxNrOfSolutions <=
506		% what has already been used previously, we can simply reuse transition from the state space
507
508		execute_custom_operation(CurID,OpName,Operation_op,Max) :-
509		visited_expression(CurID,InState),
510		specfile:compute_operation_effect_max(InState,OpName,Operation,NewState,_TransPathInfo,Max),
511		% logger:writeln_log(sol(OpName,NewState)), %%
512		tcltk_interface:add_trans_id(CurID,Operation,NewState,NewID,TransId),
513		% logger:writeln_log(ids(OpName,Operation,NewID,TransId)), %%
514		create_operation_term(TransId,Operation,CurID,NewID, Operation_op).
515
516
517
518		% create a term op(...) with infos for Java interface about an operation-transition
519		create_operation_term(TransId,Op,CurID,NewID, JavaOpTerm) :-
520		(filter_op(TransId,Op,CurID,NewID, JavaOpTerm) -> true
521		; add_error(eclipse_interface,'filter_op failed: ', filter_op(TransId,Op,CurID,NewID, JavaOpTerm)),fail).
522
523		/* ------------------------- */
524		/* SAP Testcase Generation */
525		/* ------------------------- */
526		:- use_module(cbcsrc(cbc_path_solver),[create_testcase_path/5]).
527
528		sap_find_test_path(Events,EndPredicate,Timeout,Operations) :-
529		type_predicate(EndPredicate,TypedPredicate),
530		(create_testcase_path(init,Events,TypedPredicate,Timeout,Trace) -> true ; Trace = []),
531		% Trace can be "timeout" or "interrupt", too
532		(is_list(Trace) -> op_tuples_to_full_operations(Trace,Operations) ; Operations=Trace).
533
534		op_tuples_to_full_operations([],[]).
535		op_tuples_to_full_operations([(Id,OpTerm,Src,Dst)|Trest],[Op|Orest]) :-
536		create_operation_term(Id,OpTerm,Src,Dst,Op),
537		op_tuples_to_full_operations(Trest,Orest).
538
539		type_predicate(Predicate,TypedPredicate) :-
540		b_type_expression(Predicate,[variables],pred,TypedPredicate,Errors),
541		add_all_perrors(Errors,[],sap_target_predicate_type_error),
542		no_real_perror_occurred(Errors).
543
544		/* ------------------------- */
545		/* Formula evaluation */
546		/* ------------------------- */
547		evaluation_get_top_level(Tops) :-
548		% Currently, we do not want to see the rodin information positons
549		% in the expression viewer
550		suppress_rodin_positions(CHNG),
551		bv_get_top_level(TopIds),
552		findall( top(Id,Label,Children),
553		( member(Id,TopIds), bv_expand_formula(Id,Label,Children) ),
554		Tops),
555		reset_suppress_rodin_positions(CHNG).
556		evaluation_expand_formula(Id,Label,Children) :-
557		% Currently, we do not want to see the rodin information positons
558		% in the expression viewer
559		suppress_rodin_positions(CHNG),
560		bv_expand_formula(Id,Label,Children),
561		reset_suppress_rodin_positions(CHNG).
562		evaluation_get_values(Ids,StateId,Values) :-
563		bv_get_values(Ids,StateId,Values).
564		evaluation_insert_formula(AST,ParentId,Id) :-
565		b_type_expression(AST,[variables],_,Typed,Errors),
566		% this also calls ast_cleanup; we could temporarily set OPTIMIZE_AST to false
567		( Errors == [] ->
568		bv_insert_formula(Typed,ParentId,Id)
569		;
570		add_error_and_fail(eclipse_interface,'Could not type-check AST','')).
571
572		/* ------------------------------- */
573		/* Find state satisfying predicate */
574		/* ------------------------------- */
575		:- use_module(b_state_model_check,[b_set_up_valid_state_with_pred/2]).
576		find_state_satisfying_predicate(Predicate,Result) :-
577		b_type_expression(Predicate,[variables],pred,TPredicate,Errors),
578		( Errors == [] ->
579		find_state_satisfying_predicate1(TPredicate,Result)
580		;
581		Result = errors(Errors)).
582		:- use_module(clpfd_interface,[catch_clpfd_overflow_call1/1]).
583		find_state_satisfying_predicate1(Predicate,Result) :-
584		user_interruptable_call_det(clpfd_interface:catch_clpfd_overflow_call1(
585		b_state_model_check:b_set_up_valid_state_with_pred(State,Predicate)),
586		InterruptResult),!,
587		( InterruptResult = interrupted ->
588		Result = interrupted
589		; State = time_out ->
590		Result = interrupted
591		;
592		Result = state_found(Transition,StateId),
593		create_helper_transition(root,find_valid_state,State,StateId,Transition)).
594		find_state_satisfying_predicate1(_Predicate,no_valid_state_found).
595
596
597		/* ------------------------- */
598		/* Check for deadlocks */
599		/* ------------------------- */
600
601		:- use_module(solver_interface, [call_with_smt_mode_enabled/1]).
602
603		deadlock_freedom_check(Result) :-
604		create_texpr(truth,pred,[],Predicate),
605		deadlock_freedom_check1(Predicate,Result).
606		deadlock_freedom_check(Predicate,Result) :-
607		b_type_expression(Predicate,[variables],pred,TPredicate,Errors),
608		( Errors == [] ->
609		deadlock_freedom_check1(TPredicate,Result)
610		;
611		Result = errors(Errors)).
612		deadlock_freedom_check1(Predicate,Result) :-
613		% always do a deadlock check with SMT mode enabled
614		call_with_smt_mode_enabled(deadlock_freedom_check2(Predicate,Result)).
615		deadlock_freedom_check2(Predicate,Result) :-
616		user_interruptable_call_det(clpfd_interface:catch_clpfd_overflow_call1(
617		b_state_model_check:cbc_deadlock_freedom_check(State,Predicate,0)),
618		InterruptResult),!,
619		( InterruptResult = interrupted ->
620		Result = interrupted
621		; State = time_out ->
622		Result = interrupted
623		;
624		Result = deadlock(Transition,StateId),
625		create_helper_transition(root,deadlock_check,State,StateId,Transition)).
626		deadlock_freedom_check2(_Predicate,no_deadlock_found).
627
628		create_helper_transition(SrcId,Op,DstState,DstId,Transition) :-
629		tcltk_interface:tcltk_add_new_transition_transid(SrcId,Op,DstId,DstState,[],TransId),
630		transition(SrcId,Action,TransId,DstId),!,
631		create_operation_term(TransId,Action,SrcId,DstId,Transition).
632
633
634		/* ------------------------------- */
635		/* Find values */
636		/* ------------------------------- */
637		%find_values(Commands,Predicate,MaxNumberSolutions,Solutions) :-
638		% setup_userdef_state_space(Commands,root,State,Ids,ConstantsId).
639
640		%setup_userdef_state_space2(copy_state(Id),CState,State,Ids,ConstantsId) :-
641		% visited_expression(Id,S),
642		% ( S=concrete_constants(Constants) ->
643		% (CState=root -> ConstantsId = S ; ConstantsId = CState),
644
645
646		/* ------------------------------- */
647		/* Check for invariant violations */
648		/* ------------------------------- */
649
650		invariant_check(all,Result) :-
651		findall(OpName,b_is_operation_name(OpName),Ops),
652		invariant_check2(Ops,Result).
653		invariant_check(ops(Ops),Result) :-
654		invariant_check2(Ops,Result).
655		invariant_check2(Ops,Result) :-
656		call_with_smt_mode_enabled(user_interruptable_call_det(invariant_check3(Ops,Res,[]), Status)),
657		(Status = interrupted -> Result = interrupted ; Result = Res).
658		invariant_check3([]) --> !.
659		invariant_check3([Op|Rest]) -->
660		invariant_check_for_single_op(Op),
661		invariant_check3(Rest).
662		:- use_module(clpfd_interface,[catch_clpfd_overflow_call1/1]).
663		invariant_check_for_single_op(OpName,In,Out) :-
664		( clpfd_interface:catch_clpfd_overflow_call1(
665		b_state_model_check:state_model_check_invariant(OpName,State1,Operation,State2)) ->
666		In = [counterexample(OpName,Trans1,Trans2)|Out],
667		atom_concat( invariant_check_ , OpName, RootTrans),
668		create_helper_transition(root, RootTrans,State1,StateId1,Trans1),
669		create_helper_transition(StateId1,Operation,State2,_StateId2,Trans2)
670		;
671		In = Out).
672
673		/* ------------------------------- */
674		/* CBC Refinement Checking */
675		/* ------------------------------- */
676		:- use_module(symbolic_model_checker(cbc_refinement_checks), [cbc_refinement_check/2]).
677		refinement_check(ResultsString,Result) :-
678		call_with_smt_mode_enabled(cbc_refinement_check(ResultsString,Result)).
679
680		/* ----------------------------- */
681		/* CBC Static Assertion Checking */
682		/* ----------------------------- */
683		:- use_module(b_state_model_check, [cbc_static_assertions_check/1, cbc_dynamic_assertions_check/1]).
684		cbc_static_assertion_violation_checking(Result) :-
685		user_interruptable_call_det(catch_clpfd_overflow_call1(cbc_static_assertions_check(State)),InterruptResult), !,
686		( InterruptResult = interrupted ->
687		Result = interrupted
688		; State = time_out ->
689		Result = interrupted
690		; State = no_counterexample_found ->
691		Result = no_counterexample_found
692		; functor(State,no_counterexample_exists,_) -> % arity is 3
693		Result = no_counterexample_exists
694		;
695		State = counterexample_found(RealState),
696		Result = counterexample_found(Transition,StateId),
697		transition_name(static,TransName),
698		create_helper_transition(root,TransName,RealState,StateId,Transition)).
699		cbc_dynamic_assertion_violation_checking(Result) :-
700		user_interruptable_call_det(catch_clpfd_overflow_call1(cbc_dynamic_assertions_check(State)),InterruptResult), !,
701		( InterruptResult = interrupted ->
702		Result = interrupted
703		; State = time_out ->
704		Result = interrupted
705		; State = no_counterexample_found ->
706		Result = no_counterexample_found
707		; functor(State,no_counterexample_exists,_) -> % arity is 0
708		Result = no_counterexample_exists
709		;
710		State = counterexample_found(RealState),
711		Result = counterexample_found(Transition,StateId),
712		transition_name(dynamic,TransName),
713		create_helper_transition(root,TransName,RealState,StateId,Transition)).
714
715		transition_name(dynamic,Name) :- animation_minor_mode(eventb),!,
716		Name = 'context_theorems_check'.
717		transition_name(dynamic,dynamic_asserion_check).
718		transition_name(static,Name) :- animation_minor_mode(eventb),!,
719		Name = 'invariant_theorems_check'.
720		transition_name(static,static_asserion_check).
721
722		/* ------------------------- */
723		/* Generate Visualizations */
724		/* ------------------------- */
725
726		get_vacuous_invariants(L) :-
727		findall(I,vacuous_invariant(I),L).
728
729		vacuous_invariant(Inv) :-
730		b_get_invariant_from_machine(Invariant),
731		b_interpreter:member_conjunct(Inv,Invariant,_),
732		get_texpr_expr(Inv,IE),get_disj_lhs(IE,LHS),
733		print('Checking vor vacuity: '), translate:print_bexpr(Inv),nl,
734		(test_boolean_expression_in_node(ResID,LHS,'vacuous invariant')
735		-> print(rhs_triggered_in_state(ResID)),nl,nl, % Implication/disjunction trigger in at least one state
736		fail
737		; print(' *** VACUOUS *** '),nl,nl
738		).
739
740		get_disj_lhs(implication(LHS,_),LHS).
741		get_disj_lhs(disjunction(LHS,_),NLHS) :- create_negation(LHS,NLHS).
742
743		get_vacuous_guards(L) :-
744		findall(G,vacuous_guard(_,G),L).
745
746		:- use_module(probsrc(tools_strings),[ajoin/2]).
747		vacuous_guard(OpName,Result) :-
748		get_guard_with_one_negated(OpName,Guard,Neg),
749		translate:translate_bexpression_with_limit(Guard,GuardTS),
750		format('Checking vor vacuity: ~w : ~w~n',[OpName,GuardTS]),
751		%translate:print_bexpr(Neg),nl,
752		(test_boolean_expression_in_node(ResID,Neg,'vacuous guard')
753		-> print(guard_individually_false_in(ResID)),nl,nl,
754		fail
755		; print(' *** VACUOUS *** '),nl,nl,
756		ajoin([OpName,' : ',GuardTS],Result)
757		).
758
759
760		:- use_module(b_operation_guards,[get_operation_enabling_condition/7]).
761		%:- use_module(b_ast_cleanup, [clean_up/3]).
762		:- use_module(b_interpreter_components,[construct_optimized_exists/3]).
763
764		% get a guard, by translating all parameters into existential quantifiers
765		get_guard_with_one_negated(OpName,SingleGuard,FullModifiedGuard) :-
766		get_operation_enabling_condition(OpName,Parameters,EnablingCondition,_BecomesSuchVars,_Precise,false,true),
767		% TO DO: partition; avoid lifting becomes_such_that conditions
768		% (in EventB the feasibility PO will ensure that Guard => BecomeSuchThat is ok)
769		negate_one_guard(EnablingCondition,SingleGuard,ModifiedEnablingCondition),
770		construct_optimized_exists(Parameters,ModifiedEnablingCondition,FullModifiedGuard).
771
772		:- use_module(probsrc(bsyntaxtree),[conjunction_to_list/2]).
773		negate_one_guard(Conjunct,SingleGuard,ModifiedConjunct) :-
774		conjunction_to_list(Conjunct,L),
775		append(Rest1,[SingleGuard|Rest2],L),
776		create_negation(SingleGuard,NegSingleGuard),
777		append(Rest1,[NegSingleGuard|Rest2],NewGuard), % TO DO: better treatment for well-definedness !?
778		conjunct_predicates(NewGuard,ModifiedConjunct).
779
780		:- use_module(b_interpreter, [tcltk_quick_describe_unsat_properties/2, tcltk_unsatisfiable_components_exist/0]).
781		quick_describe_unsat_properties(Res) :-
782		tcltk_unsatisfiable_components_exist
783		-> tcltk_quick_describe_unsat_properties(list(TRes),_Status), % sometimes this can be 'The properties were satisfiable' if tcltk_unsatisfiable_components_exist faulty
784		Res = unsat_properties(TRes) % TO DO: use Status to say unsat or unknown_properties
785		; Res = no_unsat_properties_found.
786		% TODO: integrate WD prover and Z3 bup core here