1		% (c) 2009-2019 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
10		get_rand/4, % DEPRECATED, remove when switching to the new core
11		set_rand/4, % DEPRECATED, remove when switching to the new core
12
13		debug_console/2,
14
15		typecheck_b_project/3,
16
17		load_b_file/1, load_prob_file/1,
18		load_eventb_file/1,
19		load_tla_file/1,
20		load_xtl_file/1,
21
22		load_classical_b/1, % deprecated
23		load_classical_b/2, % deprecated
24
25		find_shortest_trace_to_current_state/1,
26		find_shortest_trace_to_current_state2/2,
27
28		do_ltl_modelcheck/6,
29
30		get_invariants/1,
31		get_name/1,
32
33		evaluate/3,
34
35		%es_reset/0, %evalstore: reset, remove all dynamic stores
36
37		load_cspm_spec_from_pl_file/1,
38
39		init_eclipse_preferences/0,
40
41		set_eclipse_card/2,
42
43		getAllOperations/1, % deprecated, remove in 2.0
44		getSetElements/1,
45		getInternalRep/1,
46		get_machine_objects/5,
47
48		get_all_transitions/1,
49
50		getErrorMessages/2,
51
52		ops_with_timeout/1, ops_with_virtual_timeout/1, ops_with_real_timeout/1, ops_user_interrupt_occured/0,
53
54		getCurrentStateID/1,
55		getVarCstValue/3, applyVarCstValue/4,
56		isRootState/1, isConstantsSetUpState/1,
57		getOperationParameterNames/2, % deprecated, remove in 2.0
58
59		get_operation_infos/1,
60
61
62		% getCurrentStateValues/2, no longer exists ??!
63		getStateValues/2,
64
65		test_boolean_expression_in_node/2,
66		computeOperations/1,
67		executeOperationNr/1, executeOperationNr_on_computed_node/1,
68
69		setCurrentState/1,
70		computeOperationsForState/2, % Used in ProB 1.0
71
72		evaluate_expression/2,
73
74		print_states_for_dot/1,
75
76		evaluate_expression_as_tree/4,
77		evaluate_properties_as_tree/1,
78		evaluate_invariant_as_tree/2,
79		evaluate_precondition_as_tree/3,
80		evaluate_raw_expression_as_tree/3,
81
82		%in contrast to evaluate_expression, it supports predicates and does typing
83		evaluate_raw_expression/3,
84		evaluate_raw_expressions/3,
85
86		sap_generate_local_testcases/5,
87		sap_find_test_path/4,
88		execute_custom_operations/6,
89
90		evaluation_get_top_level/1,
91		evaluation_expand_formula/3,
92		evaluation_get_values/3,
93		evaluation_insert_formula/3,
94
95		deadlock_freedom_check/1,
96		deadlock_freedom_check/2,
97		invariant_check/2,
98
99		save_as_classical_b/4,
100
101		analyse_predicate/6,
102		get_classicalb_machine_objects/2,
103
104		dot_hierarchy/1,
105
106		refinement_check/2,
107
108		load_sets_for_cbc/1,
109
110		cbc_static_assertion_violation_checking/1,
111		get_vacuous_invariants/1, get_vacuous_guards/1,
112
113		quick_describe_unsat_properties/1,
114		find_state_satisfying_predicate/2,
115
116		prob_construct_trace/6
117		]).
118
119		:- use_module(module_information).
120		:- module_info(group,cli).
121		:- module_info(description,'This module provides the Prolog interface to Java and other languages (usually called via socket server).').
122
123		:- use_module(library(system),[environ/2]).
124		:- use_module(library(lists)).
125
126		:- use_module(error_manager).
127		:- use_module(self_check).
128		:- use_module(bsyntaxtree).
129		:- use_module(version).
130		:- use_module(eventhandling,[announce_event/1]).
131
132		:- use_module(model_checker).
133
134		:- use_module(b_global_sets,[enum_global_type/2]).
135		:- use_module(translate).
136		:- use_module(store).
137
138		:- use_module(bvisual2).
139
140		:- use_module(library(codesio)).
141
142		:- use_module(state_space,[visited_expression/2, visited_expression_id/1]).
143		:- ensure_loaded(tcltk_interface).
144
145
146		:- use_module(b_state_model_check,[cbc_deadlock_freedom_check/3]).
147
148		:- use_module(extension('user_signal/user_signal'), [user_interruptable_call_det/2]).
149
150		%:- use_module(extension('counter/counter'), [get_counter/2]).
151		:- use_module(prob2_interface, [get_state/2]).
152
153		% analyse_predicate(+Type,-Desc,-Result,-Total,-False,-Unknown)
154
155		analyse_predicate(Type,Desc,Result,Total,False,Unknown) :-
156		user:tcltk_analyse_option(Type,Desc),
157		user:tcltk_analyse(ascii,Type,list(Result),Total,False,Unknown).
158
159
160		/* a list of the calls provided by this interface; useful for the whitelist of the socket server */
161
162
163		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
164		% WARNING: This is dangerous in a release. It allows to execute arbitrary code
165		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
166
167
168		check_key(Key) :-
169		environ('PROB_DEBUGGING_KEY',Key).
170
171		:- dynamic current_prob_module/1.
172		current_prob_module(user).
173
174		debug_console(Key,Commands) :-
175		check_key(Key), debug_console2(Commands).
176		debug_console2([]).
177		debug_console2([H|T]) :-
178		nonvar(H),
179		debug_command(H), debug_console2(T).
180
181		debug_command(set_module(X)) :-
182		!, current_module(X), retractall(current_prob_module(_)), assert(current_prob_module(X)).
183		debug_command(Command) :-
184		current_prob_module(M),
185		write(M:Command),nl,
186		call(M:Command).
187
188
189		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
190
191
192		/* ------------------------- */
193		/* Machine Loading Interface */
194		/* ------------------------- */
195
196		%:- use_module(pref_definitions,[b_get_preferences_from_machine/0]).
197		:- use_module(specfile,[b_or_z_mode/0,set_animation_mode/1,set_animation_minor_mode/1,animation_mode/1,
198		set_currently_opened_file/1]).
199		:- use_module(bmachine_construction,[check_machine/4, get_constructed_machine_name/2]).
200		:- use_module(probltlsrc(ltl),[ltl_model_check_with_ce/4,ltl_formula_structure/3]).
201		:- use_module(probltlsrc(ltl_tools),[typecheck_temporal_formula/3]).
202		%:- use_module(tcltk_interface, [find_shortest_trace_to_node/5]).
203
204		:- use_module(state_space).
205		:- use_module(bmachine).
206
207
208		% DEPRECATED, only here because the old Rodin plugin calls the predicates
209		get_rand(0,0,0,0).
210		set_rand(_,_,_,_).
211
212		%:- use_module(preferences,[reset_all_temporary_preferences/0]).
213		clear_loaded_machines :-
214		clear_loaded_machines_wo_errors,
215		reset_errors,
216		% now done via event-handling: reset_all_temporary_preferences,
217		garbage_collect_atoms,!. % reclaim atoms if possible
218		clear_loaded_machines :- add_error(clear_loaded_machines,'clear_loaded_machines Failed').
219
220		% new profiler
221		%:- use_module('../extensions/profiler/profiler.pl').
222
223		% old profiler
224		%:- use_module(runtime_profiler,[reset_runtime_profiler/0]).
225
226		:- use_module(eval_strings,[reset_eval_strings/0]).
227		:- use_module(eventhandling, [announce_event/1]).
228		clear_loaded_machines_wo_errors :-
229		announce_event(reset_specification),
230		announce_event(clear_specification),
231		% 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,
232		% reset_dynamics, % new profiler
233		reset_eval_strings.
234
235		% Errors is a list of error(ErrorDescription,Position)
236		% Position is the number of the Syntaxtree-Node
237		typecheck_b_project(Main,Machines,Errors) :-
238		check_machine(Main,Machines,_,Errors).
239
240		load_classical_b(Machines) :- % DEPRECATED
241		set_animation_mode(b),
242		load_classical_b(Machines,Errors),
243		add_errors(Errors).
244		load_classical_b(Machines,Errors) :-
245		[First|_] = Machines,
246		get_constructed_machine_name(First,Main),
247		b_set_machine(Main,Machines,Errors).
248		% Don't forget to call update_preferences_from_spec after this and before start_animation
249
250
251		add_errors([]).
252		add_errors([H|T]) :- error_manager:add_error('eclipse_interface','Error loading machine',H),add_errors(T).
253
254		:- use_module(debug,[debug_println/2]).
255		:- use_module(parsercall,[call_tla2b_parser/1, tla2prob_filename/2]).
256		load_tla_file(Filename) :-
257		call_tla2b_parser(Filename),
258		tla2prob_filename(Filename,GeneratedProbFile),
259		debug_println(10,loading_generated_prob_file(GeneratedProbFile)),
260		load_prob_file(GeneratedProbFile),
261		%load_b_file(GeneratedBFile),
262		debug_println(10,set_animation_minor_mode(tla)),
263		set_animation_minor_mode(tla).
264		load_b_file(Filename) :-
265		clear_loaded_machines_wo_errors,
266		set_animation_mode(b),
267		bmachine:b_load_machine_from_file(Filename),
268		set_currently_opened_file(Filename).
269		load_prob_file(Filename) :-
270		clear_loaded_machines_wo_errors,
271		set_animation_mode(b),
272		bmachine:b_load_machine_probfile(Filename),
273		set_currently_opened_file(Filename).
274
275		:- use_module(prob2_interface, [load_event_b_project/4]).
276		:- use_module(tools_files, [write_to_utf8_file/2]).
277
278		save_as_classical_b(File,Machines,Contexts,Errors) :-
279		/* first set the number of animated levels to 0*/
280		get_preference(number_animated_abstractions,OldNum),
281		call_cleanup( ( set_preference(number_animated_abstractions,0),
282		load_event_b_project(Machines,Contexts,[],Errors),!),
283		set_preference(number_animated_abstractions,OldNum)),
284		( Errors==[] ->
285		b_show_eventb_as_classicalb(Rep,true),
286		write_to_utf8_file(File,Rep)
287		; otherwise ->
288		/* Do nothing, but return the list of errors*/
289		true).
290
291
292		load_eventb_file(Filename) :-
293		clear_loaded_machines_wo_errors,
294		set_animation_mode(b), set_animation_minor_mode(eventb),
295		b_load_eventb_project(Filename),
296		set_currently_opened_file(Filename).
297
298		:- use_module(xtl_interface,[open_xtl_file/1]).
299		load_xtl_file(Filename) :-
300		clear_loaded_machines_wo_errors,
301		set_animation_mode(xtl),
302		xtl_interface:open_xtl_file(Filename),
303		set_currently_opened_file(Filename).
304
305		get_all_transitions(Transitions) :-
306		findall(trans(TransId,Src,Event,PP,Dst,Infos),
307		( transition(Src,Event,TransId,Dst),
308		translate_event(Event,PP),
309		get_event_infos(TransId,Infos)),
310		Transitions).
311
312		get_event_infos(TransId,Infos) :-
313		findall(Info, transition_info(TransId,Info), Infos1),
314		filter_transition_infos(Infos1,Infos).
315
316		filter_transition_infos([],[]).
317		filter_transition_infos([I|Irest],[O|Orest]) :-
318		filter_transition_info(I,O),
319		filter_transition_infos(Irest,Orest).
320
321		filter_transition_info(event(StackI),event(StackO)) :- !,
322		filter_event_stack(StackI,StackO).
323		filter_transition_info(I,I).
324
325		filter_event_stack([],[]).
326		filter_event_stack([event(Name,Params)|Irest],[event(Name,Strings)|Orest]) :-
327		translate_bvalue_l(Params,Strings),
328		filter_event_stack(Irest,Orest).
329
330		translate_bvalue_l([],[]).
331		translate_bvalue_l([V|Vrest],[S|Srest]) :-
332		translate_bvalue(V,S),
333		translate_bvalue_l(Vrest,Srest).
334
335		:- use_module(visualize_graph,[tcltk_print_states_for_dot/1]).
336		print_states_for_dot(X) :- visualize_graph:tcltk_print_states_for_dot(X).
337
338
339
340		do_ltl_modelcheck(Formula,Max,Mode,Atomics,Structure,Result) :-
341		typecheck_temporal_formula(Formula,TypeCheckedFormula,Status),
342		( Status=ok ->
343		ltl_formula_structure(TypeCheckedFormula,Atomics,Structure),
344		ltl_model_check_with_ce(TypeCheckedFormula,Max,Mode,Result1),
345		ltl_adapt_operations(Result1,Result)
346		; otherwise ->
347		Atomics=[], Structure=[],
348		Result=typeerror([])).
349
350		ltl_adapt_operations(counterexample(CE1,LoopEntry,PathToCE1), counterexample(CE,LoopEntry,PathToCE)) :- !,
351		filter_ops_and_ids(PathToCE1,root,PathToCE),
352		ltl_adapt_ce(CE1,CE).
353		ltl_adapt_operations(Result,Result).
354
355		ltl_adapt_ce([],[]).
356		ltl_adapt_ce([atom(State,Evals,OpTuple)|Irest],[atom(State,Evals,Transition)|Orest]) :-
357		ltl_adapt_ce2(OpTuple,State,Transition),
358		ltl_adapt_ce(Irest,Orest).
359		ltl_adapt_ce2(none,_State,none).
360		ltl_adapt_ce2((TransId,Action,DstId),State,Transition) :-
361		create_operation_term(TransId,Action,State,DstId,Transition).
362
363
364		find_shortest_trace_to_current_state(TraceStrings) :-
365		find_shortest_trace_to_current_state2(TraceStrings, _).
366
367		find_shortest_trace_to_current_state2(TraceStrings, TraceIDs) :-
368		getCurrentStateID(ID),
369		user:find_shortest_trace_to_node(root,ID,Trace,TraceIDs),
370		translate_events(Trace,TraceStrings).
371
372
373		% TODO: Should we put these predicates in another module? They are not called by any Java Interface
374		:- use_module(state_space, [time_out_for_node/3]).
375		ops_with_timeout(OpNameList) :-
376		getCurrentStateID(StateId),
377		ops_with_timeout(StateId,OpNameList,_).
378		ops_with_virtual_timeout(OpNameList) :-
379		getCurrentStateID(StateId),
380		ops_with_timeout(StateId,OpNameList,virtual_time_out(_)).
381		ops_with_real_timeout(OpNameList) :-
382		getCurrentStateID(StateId),
383		ops_with_timeout(StateId,OpNameList,time_out).
384		% Note: possibilities are currently: time_out, user_interrupt_signal, virtual_time_out(_)
385		ops_user_interrupt_occured :-
386		getCurrentStateID(StateId),
387		time_out_for_node(StateId,_,user_interrupt_signal).
388		ops_with_timeout(StateId,OpNameList,Type) :-
389		findall(OpName, time_out_for_node(StateId,OpName,Type), OpNameList).
390
391		/* ------------------------- */
392		/* CSP Loading Interface */
393		/* ------------------------- */
394
395		:- use_module(probcspsrc(haskell_csp),[load_cspm_pl_file/1]).
396		load_cspm_spec_from_pl_file(CSPMFile) :-
397		clear_loaded_machines_wo_errors,
398		specfile:set_animation_mode(cspm),
399		load_cspm_pl_file(CSPMFile),
400		set_currently_opened_file(CSPMFile).
401
402		/* --------------------- */
403		/* Preferences Interface */
404		/* --------------------- */
405
406		:- use_module(preferences,
407		[init_preferences/0,set_preference/2,get_preference/2]).
408
409		:- use_module(state_space_exploration_modes,[reset_depth_breadth_first_mode/0]).
410		init_eclipse_preferences :- preferences:init_preferences, reset_depth_breadth_first_mode.
411
412		% set Cardinality of SET; a bit like scope_SET == Scope DEFINITION
413		:- use_module(b_global_sets,[set_user_defined_scope/2]).
414		:- use_module(tools_strings, [convert_cli_arg/2]).
415		set_eclipse_card(Set,Scope) :-
416		convert_cli_arg(Scope,Value),
417		set_user_defined_scope(Set,Value).
418
419
420		/* ------------------ */
421		/* getErrorMessages/1 */
422		/* ------------------ */
423		/* Returns a list of strings containing all error messages (of the error_manager).
424		Clears all the errors. Returns the empty list if no errors occurred since
425		the last call to getErrorMessages.
426
427		TODO: This is equivalent with the get_error_messages predicate in prob2_interface
428		We changed the name in the ProB 2.0 interface for coding convention.
429		*/
430
431		getErrorMessages(WarningsOnly,ListOfErrMsgs) :-
432		(real_error_occurred -> WarningsOnly = false ; WarningsOnly = true),
433		(get_all_errors_and_reset(ListOfErrMsgs) -> true ; ListOfErrMsgs=[]).
434
435
436
437		/* ---------------------------- */
438		/* Syntax Information Interface */
439		/* ---------------------------- */
440
441		getAllOperations(L) :-
442		(b_or_z_mode
443		-> findall(OperationName, b_top_level_operation(OperationName), L)
444		; L=[]). % FIXME: provide list for CSP-M
445
446
447		get_operation_infos(L) :-
448		findall(op(Name,Results,Parameters),b_get_machine_operation(Name,Results,Parameters,_,_,_),L).
449
450
451
452
453		getSetElements(L) :- /* get a list of all fd(N,S) elements of all sets and precompute their translation */
454		findall(fds(Nr,Set,String),
455		(enum_global_type(fd(Nr,Set),_), translate_bvalue(fd(Nr,Set),String)), L).
456
457
458		:- use_module(specfile,[get_internal_representation/1]).
459		getInternalRep(X) :- get_internal_representation(X).
460
461		get_classicalb_machine_objects(Constants, Variables) :-
462		b_get_machine_constants(C),translate_list(C,Constants),
463		b_get_machine_variables(V),translate_list(V,Variables).
464
465
466		translate_list([],[]).
467		translate_list([H|T],[HT|TT]) :- translate_bexpression(H,HT), translate_list(T,TT).
468
469
470
471		get_machine_objects(Sections,SetElements,Constants,Variables,Operations) :-
472		b_get_animated_sections(Sections),
473		findall(TId,
474		( enum_global_type(fd(Nr,Set),_),
475		translate_bvalue(fd(Nr,Set),String),
476		create_texpr(identifier(String),global(Set),[],TId)),
477		SetElements),
478		b_get_machine_constants(Constants),
479		b_get_machine_variables(Variables),
480		b_get_promoted_machine_operations(Operations1),
481		maplist(remove_op,Operations1,Operations).
482		remove_op(TId,NTId) :-
483		remove_bt(TId,identifier(Id),identifier(NId),NTId),
484		remove_op2(Id,NId).
485		remove_op2(op(Op),Op) :- !.
486		remove_op2(Op,Op).
487
488		/* ------------------- */
489		/* Animation Interface */
490		/* ------------------- */
491
492
493		get_invariants(List) :- %print(start),nl,
494		b_get_invariant_from_machine(B),
495		% print(got(B)),nl,
496		conjunction_to_list(B,L), %print(L),nl,
497		maplist(mk_inv,L,List).
498
499		mk_inv(C,inv(Text,Pos)) :- translate_bexpression(C,Text),get_texpr_pos(C,P), (P=pos(Pos,_,_,_,_,_) -> true;Pos = P),!.
500		mk_inv(C,_) :- add_internal_error(mk_inv,'Failed: ',C, unknown),fail.
501
502		get_name(Name) :- b_machine_name(Name).
503
504		/* get the ID of the current state */
505		getCurrentStateID(CurID) :-
506		current_state_id(CurID).
507		/* get the ID of the current state */
508
509
510
511		isRootState(ID) :- ID=root.
512
513		:- use_module(specfile,[state_corresponds_to_set_up_constants/1,
514		state_corresponds_to_initialised_b_machine/2]).
515
516		isConstantsSetUpState(ID) :-
517		% true if no constants exists or if all constants have been valued
518		visited_expression(ID,State),
519		specfile:state_corresponds_to_set_up_constants(State).
520
521
522
523
524		/* compute enabled operations, if required, and return a list of
525		strings of all possible operations and arguments */
526		computeOperations(Operations) :-
527		user:tcltk_get_options(list(Operations)).
528
529
530		executeOperationNr(Nr) :-
531		user:compute_all_transitions_if_necessary, /* make sure options are computed; TO DO: improve */
532		user:tcltk_perform_nr(Nr).
533		executeOperationNr_on_computed_node(Nr) :- % a version which does not recompute transitions if necessary
534		user:tcltk_perform_nr(Nr).
535
536
537		setCurrentState(ID) :- current_state_id(ID),!. % no need to jump
538		setCurrentState(ID) :- /* jumps to the given node; can be backtracked */
539		visited_expression_id(ID),
540		user:tcltk_goto_state(jump,ID).
541
542
543		test_boolean_expression_in_node(ResID,BoolExpr) :-
544		visited_expression(ResID,CurState),
545		specfile:state_corresponds_to_initialised_b_machine(CurState,CurBState),
546		b_interpreter:b_test_boolean_expression_wf(BoolExpr,[],CurBState).
547
548		/* USED IN PROB 1.0*/
549		computeOperationsForState(StateID, OpsAndIDs) :- /* compute the enabled operations
550		(without the backtrack options) for a state ID which is not necessarily the current one */
551		visited_expression_id(StateID),
552		user:tcltk_compute_options(StateID,OpsSTAndIDs),
553		print('OpsSTAndIDs: '),print(OpsSTAndIDs),nl,
554		(filter_ops_and_ids(OpsSTAndIDs,StateID,OpsAndIDs) -> true
555		; print(filter_ops_and_ids_failed(OpsSTAndIDs)),nl,fail).
556
557		/*
558		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)) >>'],[],')
559		*/
560
561
562		getOperationParameterNames(Operation,Paras) :-
563		b_get_machine_operation_parameter_names(Operation,Paras).
564
565		filter_ops_and_ids([],_,[]).
566		filter_ops_and_ids([OpTuple|T],StateID,[FOp|FT]) :-
567		((OpTuple = (Id,OpTerm,Dst), create_operation_term(Id,OpTerm,StateID,Dst,FOp))
568		-> true
569		; print(filter_op_failed(OpTuple,StateID)),nl, FOp = ('?')),
570		filter_ops_and_ids(T,StateID,FT).
571
572		filter_op(TransId,OpTerm,Src,Dst,JavaOpTerm) :-
573		(animation_mode(cspm) ->
574		filter_op_csp(TransId,OpTerm,Src,Dst,JavaOpTerm)
575		; otherwise ->
576		filter_op1(TransId,OpTerm,Src,Dst,JavaOpTerm)).
577
578		filter_op1(TransId,OpTerm,Src,Dst,
579		op(TransId,Op,Src,Dst,Arguments,ArgumentsPretty,Infos,State)) :-
580		extract_args_and_return_values(OpTerm,Op,Arguments),
581		get_state(Dst,BState), translate:translate_bstate(BState,State),
582		prettyprint(Arguments,ArgumentsPretty),
583		get_event_infos(TransId,Infos).
584
585		filter_op_csp(TransId,OpTerm,Src,Dst,op(TransId,Op,Src,Dst,Arguments,ArgumentsPretty,Infos,CSPState)) :-
586		extract_csp_args_and_return_values(OpTerm,Op,Arguments),
587		translate:translate_event(OpTerm,PPEvent),
588		tools: split_atom(PPEvent,['.','!'],[_Op|ArgumentsPretty]),
589		get_state(Dst,CSPState),
590		get_event_infos(TransId,Infos).
591
592		extract_csp_args_and_return_values(io(Args,ChName,_SPAN),ChName,Args).
593		extract_csp_args_and_return_values(start_cspm(Name),Name,[]).
594		extract_csp_args_and_return_values(start_cspm_MAIN,'start_cspm_MAIN',[]).
595		extract_csp_args_and_return_values(tick(_),tick,[]).
596		extract_csp_args_and_return_values(tau(_),tau,[]).
597		extract_csp_args_and_return_values(_OP,'?',[]).
598
599		prettyprint([],[]).
600		prettyprint([H|T],[P|R]) :- translate_bvalue(H,P), prettyprint(T,R).
601
602		:- dynamic result_warning_emitted/0.
603
604		extract_args_and_return_values(Term,OpName,Arguments) :-
605		( Term='-->'(OpTerm,Results) ->
606		( result_warning_emitted -> true
607		; otherwise ->
608		print('Warning: results of operations are currently treated like arguments'),nl,
609		assert(result_warning_emitted)),
610		append(Results,Args,Arguments)
611		; otherwise -> Term=OpTerm,Args=Arguments
612		),
613		OpTerm =.. [OpName|Args].
614
615
616
617		% returns all variables and their values of the given state as a list
618		% - constants and variables that are defined for the machine but
619		% not present in the given state get the value '?'
620		% - for each variable a term of the form
621		% binding(Id,Value,PPValue,Tag)
622		% is in the result list, where
623		% Id is the variable's name,
624		% Value is its value a Prolog term
625		% PPValue is its pretty-printed value
626		% NOTE: Tag no longer generated: TO DO REVIEW:
627		% Tag is one of (cst,var,unknown), depending on whether the
628		% variable is a constant, a variable or not defined in the
629		% machine description but present in the state
630		getStateValues(CurID,VariableState) :- /* get variable values */
631		get_state(CurID,CurBState),
632		findall( binding(Id,nope,PPValue),
633		(member(bind(Id,Value),CurBState),
634		( translate_bvalue(Value,PPValue) -> true
635		; otherwise -> PPValue='**pretty-print failed**')),
636		VariableState).
637
638		getVarCstValue(ID,VarOrCst,TVals) :-
639		/* a function to get the value of a particular Variable or Constant;
640		treats relations specially: a list of relation pairs is returned */
641		get_state(ID,CurBState),
642		member(bind(VarOrCst,Val),CurBState),
643		(Val = [ (_,_) | _] /* check if it is a relation */
644		-> findall(TFact,relation_fact(_F,VarOrCst,Val,TFact),TVals)
645		; (TVals = [TVal], Val = TVal)
646		).
647
648		relation_fact(_F,_VarOrCst,Val,TFact) :-
649		member((L,R), Val), Fact = (L,R),
650		Fact=TFact.
651
652		applyVarCstValue(ID,VarOrCstFunction,DomValue,RanResult) :-
653		/* a function to apply a particular Variable or Constant Function/Relation to a value;
654		treats relations specially: a list of relation pairs is returned */
655		get_state(ID,CurBState),
656		member(bind(VarOrCstFunction,Val),CurBState),
657		member((DomValue,R),Val),
658		R= RanResult.
659
660		/* ------------------------------- */
661
662		/* evaluates an expression in Prolog format and computes the result in the current state */
663		evaluate_expression(Expression,Result) :-
664		current_expression(_CurID,CurState),
665		b_interpreter:b_compute_expression_nowf(Expression,[],CurState,Result).
666
667
668
669		%%
670		% Code for invariant debug
671		%
672
673		:- use_module(bvisual).
674
675		% probably not used anymore ?!! -> was calling non-existing predicates
676		evaluate_properties_as_tree(Tree):-
677		b_get_properties_from_machine(TExpr),
678		evaluate_expression_as_tree(root, [], TExpr, Tree).
679
680		evaluate_invariant_as_tree(StateID, Tree):-
681		b_get_invariant_from_machine(TExpr),
682		evaluate_expression_as_tree(StateID, [], TExpr, Tree).
683
684		evaluate_precondition_as_tree(StateID, OpName, Tree):-
685		bvisual:get_operation_pre(OpName, TExpr, _),
686		evaluate_expression_as_tree(StateID, [], TExpr, Tree).
687
688
689		evaluate_raw_expression_as_tree(StateID, Raw, Tree):-
690		bmachine:b_type_expression(Raw, [variables], _, TExpr, Errors),
691		( var(TExpr) ->
692		print(error_while_typing_raw_expression(Errors)),nl,
693		flush_output,
694		!,
695		fail
696		;
697		evaluate_expression_as_tree(StateID, [], TExpr, Tree)
698		).
699
700
701		evaluate_expression_as_tree(StateID, LocalState, Expr, Tree) :-
702		get_state(StateID, State),
703		get_tree_from_expr2(State, LocalState, Expr, T),
704		get_tree_node_info(T, Children, NewLocalState, Metas),
705		translate_bexpression(Expr, Pretty),
706		create_tree_node(Tree, Children, NewLocalState, [pretty_long_desc(Pretty) | Metas]).
707
708		evaluate_raw_expression(StateID, Raw, Val):-
709		bmachine:b_type_expression(Raw, [variables], _, TExpr, Errors),
710		( var(TExpr) ->
711		print(error_while_typing_raw_expression(Errors)),nl,
712		flush_output,
713		!,
714		fail
715		;
716		get_state(StateID, State),
717		bvisual:x_get_value_of_expr(State, [], TExpr, Val)
718		).
719
720		evaluate_raw_expressions(StateID, Raws, Vals):-
721		maplist(evaluate_raw_expression(StateID), Raws, Vals).
722
723
724
725		/* ------------------------- */
726		/* Execute Operation */
727		/* ------------------------- */
728
729		% MaxNrOfSolutions is the maximum number of solutions ProB returns. Also we should consider existing solutions if the Predicate holds.
730		%:- use_module(succeed_max,[succeed_max_call/2]).
731
732		/* PROB 1.0 */
733		execute_custom_operations(CurID, OpName, ParsedPredicate, MaxNrOfSolutions, TOperations, Errors) :-
734		setCurrentState(CurID),
735
736		( (OpName = '$initialise_machine';OpName = '$setup_constants' ) -> Scope = [prob_ids(visible),variables];
737		otherwise -> b_top_level_operation(OpName),
738		b_get_machine_operation(OpName,_,Parameters,_),
739		Scope = [identifier(Parameters),prob_ids(visible),variables] % prob scope allows one to use identifiers for deferred set elements
740		),
741		(MaxNrOfSolutions<1
742		-> add_message(eclipse_interface,'execute_custom_operations MaxNrOfSolutions < 1: ',MaxNrOfSolutions)
743		; true),
744		bmachine:b_type_expression(ParsedPredicate, Scope, _, TypedPred, Errors),
745		retractall(bmachine:b_machine_temp_predicate(_)),
746		assert(bmachine:b_machine_temp_predicate(TypedPred)),
747		%prob_socketserver:writeln_log(parsed_pred(ParsedPredicate)), %%
748		%prob_socketserver:writeln_log(succeed_max_call(execute_custom_operation(CurID,OpName,TO),MaxNrOfSolutions)), %%
749		findall(TO, execute_custom_operation(CurID,OpName,TO,MaxNrOfSolutions), TOperations),
750		%length(TOperations,Len), prob_socketserver:writeln_log(findall_length(Len)),
751		retractall(bmachine:b_machine_temp_predicate(_)),
752		clear_context_state.
753
754		% TO DO: check if we need to recompute the operation effect: if the ParsedPredicate is TRUE
755		% (TRUE = equal(none,integer(none,1),integer(none,1)) ) & MaxNrOfSolutions <=
756		% what has already been used previously, we can simply reuse transition from the state space
757
758		execute_custom_operation(CurID,OpName,Operation_op,Max) :-
759		set_context_state(CurID),
760		visited_expression(CurID,InState),
761		specfile:compute_operation_effect_max(InState,OpName,Operation,NewState,_TransPathInfo,Max),
762		% logger:writeln_log(sol(OpName,NewState)), %%
763		user:add_trans_id(CurID,Operation,NewState,[],NewID,[],TransId),
764		% logger:writeln_log(ids(OpName,Operation,NewID,TransId)), %%
765		create_operation_term(TransId,Operation,CurID,NewID, Operation_op).
766
767
768
769		% create a term op(...) with infos for Java interface about an operation-transition
770		create_operation_term(TransId,Op,CurID,NewID, JavaOpTerm) :-
771		(filter_op(TransId,Op,CurID,NewID, JavaOpTerm) -> true
772		; add_error(eclipse_interface,'filter_op failed: ', filter_op(TransId,Op,CurID,NewID, JavaOpTerm)),fail).
773
774		/* ------------------------- */
775		/* SAP Testcase Generation */
776		/* ------------------------- */
777		:- use_module(sap).
778
779
780		sap_generate_local_testcases(GFile,LFile,MaxNodes,Sat,Unsat) :-
781		sap:tcl_create_local_testsuite(GFile,LFile,MaxNodes,Sat,Unsat).
782
783		sap_find_test_path(Events,EndPredicate,Timeout,Operations) :-
784		type_predicate(EndPredicate,TypedPredicate),
785		( create_testcase_path(init,Events,TypedPredicate,Timeout,Trace) -> true
786		; otherwise -> Trace = []),
787		% Trace can be "timeout" or "interrupt", too
788		( is_list(Trace) -> op_tuples_to_full_operations(Trace,Operations)
789		; otherwise -> Operations=Trace).
790
791		op_tuples_to_full_operations([],[]).
792		op_tuples_to_full_operations([(Id,OpTerm,Src,Dst)|Trest],[Op|Orest]) :-
793		create_operation_term(Id,OpTerm,Src,Dst,Op),
794		op_tuples_to_full_operations(Trest,Orest).
795
796		type_predicate(Predicate,TypedPredicate) :-
797		b_type_expression(Predicate,[variables],pred,TypedPredicate,Errors),
798		add_all_perrors(Errors,[],sap_target_predicate_type_error),
799		no_real_perror_occurred(Errors).
800
801		/* ------------------------- */
802		/* Formula evaluation */
803		/* ------------------------- */
804		evaluation_get_top_level(Tops) :-
805		% Currently, we do not want to see the rodin information positons
806		% in the expression viewer
807		suppress_rodin_positions,
808		bv_get_top_level(TopIds),
809		findall( top(Id,Label,Children),
810		( member(Id,TopIds), bv_expand_formula(Id,Label,Children) ),
811		Tops).
812		evaluation_expand_formula(Id,Label,Children) :-
813		% Currently, we do not want to see the rodin information positons
814		% in the expression viewer
815		suppress_rodin_positions,
816		bv_expand_formula(Id,Label,Children).
817		evaluation_get_values(Ids,StateId,Values) :-
818		bv_get_values(Ids,StateId,Values).
819		evaluation_insert_formula(AST,ParentId,Id) :-
820		b_type_expression(AST,[variables],_,Typed,Errors),
821		( Errors == [] ->
822		bv_insert_formula(Typed,ParentId,Id)
823		; otherwise ->
824		add_error_and_fail(eclipse_interface,'Could not type-check AST','')).
825
826		/* ------------------------------- */
827		/* Find state satisfying predicate */
828		/* ------------------------------- */
829		:- use_module(b_state_model_check,[b_set_up_valid_state_with_pred/2]).
830		find_state_satisfying_predicate(Predicate,Result) :-
831		b_type_expression(Predicate,[variables],pred,TPredicate,Errors),
832		( Errors == [] ->
833		find_state_satisfying_predicate1(TPredicate,Result)
834		; otherwise ->
835		Result = errors(Errors)).
836		find_state_satisfying_predicate1(Predicate,Result) :-
837		user_interruptable_call_det(user:catch_clpfd_overflow_call1(b_set_up_valid_state_with_pred(State,Predicate)),
838		InterruptResult),!,
839		( InterruptResult = interrupted ->
840		Result = interrupted
841		; State = time_out ->
842		Result = interrupted
843		; otherwise ->
844		Result = state_found(Transition,StateId),
845		create_helper_transition(root,find_valid_state,State,StateId,Transition)).
846		find_state_satisfying_predicate1(_Predicate,no_valid_state_found).
847
848
849		/* ------------------------- */
850		/* Check for deadlocks */
851		/* ------------------------- */
852
853		:- use_module(solver_interface, [call_with_smt_mode_enabled/1]).
854
855		deadlock_freedom_check(Result) :-
856		create_texpr(truth,pred,[],Predicate),
857		deadlock_freedom_check1(Predicate,Result).
858		deadlock_freedom_check(Predicate,Result) :-
859		b_type_expression(Predicate,[variables],pred,TPredicate,Errors),
860		( Errors == [] ->
861		deadlock_freedom_check1(TPredicate,Result)
862		; otherwise ->
863		Result = errors(Errors)).
864		deadlock_freedom_check1(Predicate,Result) :-
865		% always do a deadlock check with SMT mode enabled
866		call_with_smt_mode_enabled(deadlock_freedom_check2(Predicate,Result)).
867		deadlock_freedom_check2(Predicate,Result) :-
868		user_interruptable_call_det(user:catch_clpfd_overflow_call1(cbc_deadlock_freedom_check(State,Predicate,0)),
869		InterruptResult),!,
870		( InterruptResult = interrupted ->
871		Result = interrupted
872		; State = time_out ->
873		Result = interrupted
874		; otherwise ->
875		Result = deadlock(Transition,StateId),
876		create_helper_transition(root,deadlock_check,State,StateId,Transition)).
877		deadlock_freedom_check2(_Predicate,no_deadlock_found).
878
879		create_helper_transition(SrcId,Op,DstState,DstId,Transition) :-
880		user:tcltk_add_new_transition_transid(SrcId,Op,DstId,DstState,[],TransId),
881		transition(SrcId,Action,TransId,DstId),!,
882		create_operation_term(TransId,Action,SrcId,DstId,Transition).
883
884
885		/* ------------------------------- */
886		/* Find values */
887		/* ------------------------------- */
888		%find_values(Commands,Predicate,MaxNumberSolutions,Solutions) :-
889		% setup_userdef_state_space(Commands,root,State,Ids,ConstantsId).
890
891		%setup_userdef_state_space2(copy_state(Id),CState,State,Ids,ConstantsId) :-
892		% visited_expression(Id,S),
893		% ( S=concrete_constants(Constants) ->
894		% ( CState=root -> ConstantsId = S
895		% ; otherwise -> ConstantsId = CState),
896
897
898		/* ------------------------------- */
899		/* Check for invariant violations */
900		/* ------------------------------- */
901
902		invariant_check(all,Result) :-
903		findall(OpName,b_is_operation_name(OpName),Ops),
904		invariant_check2(Ops,Result).
905		invariant_check(ops(Ops),Result) :-
906		invariant_check2(Ops,Result).
907		invariant_check2(Ops,Result) :-
908		call_with_smt_mode_enabled(user_interruptable_call_det(invariant_check3(Ops,Res,[]), Status)),
909		( Status = interrupted -> Result = interrupted
910		; otherwise -> Result = Res).
911		invariant_check3([]) --> !.
912		invariant_check3([Op|Rest]) -->
913		invariant_check_for_single_op(Op),
914		invariant_check3(Rest).
915		:- use_module(clpfd_interface,[catch_clpfd_overflow_call1/1]).
916		invariant_check_for_single_op(OpName,In,Out) :-
917		( clpfd_interface:catch_clpfd_overflow_call1(b_state_model_check:state_model_check(OpName,State1,Operation,State2)) ->
918		In = [counterexample(OpName,Trans1,Trans2)|Out],
919		atom_concat( invariant_check_ , OpName, RootTrans),
920		create_helper_transition(root, RootTrans,State1,StateId1,Trans1),
921		create_helper_transition(StateId1,Operation,State2,_StateId2,Trans2)
922		; otherwise ->
923		In = Out).
924
925		/* ------------------------------- */
926		/* CBC Refinement Checking */
927		/* ------------------------------- */
928		:- use_module(cbc_refinement_checks, [cbc_refinement_check/2]).
929		refinement_check(ResultsString,Result) :-
930		call_with_smt_mode_enabled(cbc_refinement_check(ResultsString,Result)).
931
932		/* ------------------------------- */
933		/* CBC Sets */
934		/* ------------------------------- */
935
936		:- use_module(library(sets), [list_to_set/2]).
937		%:- use_module(prob2_interface, [initialise_specification/0]).
938		load_sets_for_cbc(Sets) :-
939		list_to_set(Sets,SetOfSets),
940		load_sets_for_cbc_aux(SetOfSets).
941		%initialise_specification. % now has to be called afterwards
942		load_sets_for_cbc_aux([]) :-
943		load_event_b_project([],[event_b_context(none,'CBCSets',[])],[exporter_version(3)],[]), !.
944		load_sets_for_cbc_aux(SetOfSets) :-
945		maplist(create_set_term,SetOfSets,SetTerms),
946		load_event_b_project([],[event_b_context(none,'CBCSets',[sets(none,SetTerms)])],[exporter_version(3)],[]).
947
948		create_set_term(Name,deferred_set(none,Name)).
949
950		/* ----------------------------- */
951		/* CBC Static Assertion Checking */
952		/* ----------------------------- */
953		:- use_module(b_state_model_check, [cbc_static_assertions_check/1]).
954		cbc_static_assertion_violation_checking(Result) :-
955		user_interruptable_call_det(catch_clpfd_overflow_call1(cbc_static_assertions_check(State)),InterruptResult), !,
956		( InterruptResult = interrupted ->
957		Result = interrupted
958		; State = time_out ->
959		Result = interrupted
960		; State = no_counterexample_found ->
961		Result = no_counterexample_found
962		; State = no_counterexample_exists(_,_,_) ->
963		Result = no_counterexample_exists
964		; otherwise ->
965		State = counterexample_found(RealState),
966		Result = counterexample_found(Transition,StateId),
967		create_helper_transition(root,deadlock_check,RealState,StateId,Transition)).
968
969		/* ------------------------- */
970		/* Generate Visualizations */
971		/* ------------------------- */
972
973		evaluate(In,Result,Warnings) :- user:tcltk_eval(In,Result,Warnings,_Solution). % seems no longer used
974
975
976		/* ------------------------- */
977		/* Dot Printing */
978		/* ------------------------- */
979
980		dot_hierarchy(Filename) :- b_machine_hierarchy:write_dot_hierarchy_to_file(Filename).
981
982		% not used:
983		%:- use_module(evalstores,[evalstore_reset/0]).
984		%es_reset :- evalstore_reset.
985
986		get_vacuous_invariants(L) :-
987		findall(I,vacuous_invariant(I),L).
988
989		vacuous_invariant(Inv) :-
990		b_get_invariant_from_machine(Invariant),
991		b_interpreter:member_conjunct(Inv,Invariant,_),
992		get_texpr_expr(Inv,implication(LHS,_RHS)),
993		print('Checking vor vacuity: '), translate:print_bexpr(Inv),nl,
994		(test_boolean_expression_in_node(ResID,LHS)
995		-> print(lhs_true_in_state(ResID)),nl,nl, % Implication can be triggered in at least one state
996		fail
997		; print(' *** VACUOUS *** '),nl,nl
998		).
999
1000		get_vacuous_guards(L) :-
1001		findall(G,vacuous_guard(_,G),L).
1002
1003		:- use_module(probsrc(tools_strings),[ajoin/2]).
1004		vacuous_guard(OpName,Result) :-
1005		get_guard_with_one_negated(OpName,Guard,Neg),
1006		translate:translate_bexpression_with_limit(Guard,GuardTS),
1007		format('Checking vor vacuity: ~w : ~w~n',[OpName,GuardTS]),
1008		%translate:print_bexpr(Neg),nl,
1009		(test_boolean_expression_in_node(ResID,Neg)
1010		-> print(guard_individually_false_in(ResID)),nl,nl,
1011		fail
1012		; print(' *** VACUOUS *** '),nl,nl,
1013		ajoin([OpName,' : ',GuardTS],Result)
1014		).
1015
1016
1017		:- use_module(predicate_debugger,[get_operation_enabling_condition/7]).
1018		%:- use_module(b_ast_cleanup, [clean_up/3]).
1019		:- use_module(b_interpreter_components,[construct_optimized_exists/3]).
1020
1021		% get a guard, by translating all parameters into existential quantifiers
1022		get_guard_with_one_negated(OpName,SingleGuard,FullModifiedGuard) :-
1023		get_operation_enabling_condition(OpName,Parameters,EnablingCondition,_BecomesSuchVars,_Precise,false,true),
1024		% TO DO: partition; avoid lifting becomes_such_that conditions
1025		% (in EventB the feasibility PO will ensure that Guard => BecomeSuchThat is ok)
1026		negate_one_guard(EnablingCondition,SingleGuard,ModifiedEnablingCondition),
1027		construct_optimized_exists(Parameters,ModifiedEnablingCondition,FullModifiedGuard).
1028
1029		:- use_module(probsrc(bsyntaxtree),[conjunction_to_list/2]).
1030		negate_one_guard(Conjunct,SingleGuard,ModifiedConjunct) :-
1031		conjunction_to_list(Conjunct,L),
1032		append(Rest1,[SingleGuard|Rest2],L),
1033		create_negation(SingleGuard,NegSingleGuard),
1034		append(Rest1,[NegSingleGuard|Rest2],NewGuard), % TO DO: better treatment for well-definedness !?
1035		conjunct_predicates(NewGuard,ModifiedConjunct).
1036
1037		:- use_module(b_interpreter, [tcltk_quick_describe_unsat_properties/2, tcltk_unsatisfiable_components_exist/0]).
1038		quick_describe_unsat_properties(Res) :-
1039		tcltk_unsatisfiable_components_exist
1040		-> tcltk_quick_describe_unsat_properties(list(TRes),_Status), % sometimes this can be 'The properties were satisfiable' if tcltk_unsatisfiable_components_exist faulty
1041		Res = unsat_properties(TRes) % TO DO: use Status to say unsat or unknown_properties
1042		; Res = no_unsat_properties_found.
1043
1044
1045		% This just bundles a few commands used by BMotionStudio.
1046		% Should avoid communication overhead.
1047		% Replaced by ProB 2.0 Api
1048		:- use_module(prob2_interface,[state_property/3,op_timeout_occurred/2,get_state_errors/2]).
1049		prob_construct_trace([],[],[],[],[],[]).
1050		prob_construct_trace([Name|Names],[Pred|Preds],[NrOfSol|NrOfSols],
1051		[state(NewStateId,StateValues,Initialised,InvKO,MaxOpsReached,Timeout,OpTimeout,StateErrors,UnsatProps,OperationsForState)|States],
1052		[FirstOp|Ops],Errors) :-
1053		getCurrentStateID(Id),
1054		execute_custom_operations(Id,Name,Pred,NrOfSol,Op,LocalErrors),
1055		Op = [FirstOp|_],
1056		FirstOp = op(_,_,_,NewStateId,_,_,_,_),
1057		% the following is essentially ExploreStateCommand
1058		computeOperationsForState(NewStateId,OperationsForState),
1059		getStateValues(NewStateId,StateValues),
1060		state_property(initialised,NewStateId,Initialised),
1061		state_property(invariantKO,NewStateId,InvKO),
1062		state_property(max_operations_reached,NewStateId,MaxOpsReached),
1063		state_property(timeout_occurred,NewStateId,Timeout),
1064		op_timeout_occurred(NewStateId,OpTimeout),
1065		get_state_errors(NewStateId,StateErrors),
1066		quick_describe_unsat_properties(UnsatProps),
1067		setCurrentState(NewStateId),
1068		prob_construct_trace(Names,Preds,NrOfSols,States,Ops,FurtherErrors),
1069		append(LocalErrors,FurtherErrors,Errors).