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(specfile, [
6		specfile_possible_trans_name/2, specfile_possible_trans_name_for_successors/2,
7		specfile_trans/6,
8		prepare_state_for_specfile_trans/3, prepare_state_for_specfile_trans/4,
9		extract_infos_from_prepared_state/2,
10
11		property/2, elementary_prop/2,
12
13		partial_trans/4, specfile_trans_or_partial_trans/7,
14
15		animation_mode/1, set_animation_mode/1, add_animation_minor_mode/1,
16		animation_minor_mode/1, set_animation_minor_mode/1, remove_animation_minor_mode/0,
17		unset_animation_minor_modes/1, reset_animation_minor_modes/1,
18		b_mode/0, z_mode/0, b_or_z_mode/0, b_or_z_mode/1,
19		eventb_mode/0,
20		classical_b_mode/0,
21		csp_mode/0, csp_mode/1,
22		csp_with_bz_mode/0, z_or_tla_minor_mode/0,
23		process_algebra_mode/0,
24		xtl_mode/0,
25		sequent_prover_mode/0,
26		b_syntax_available_for_source/0,
27
28		type_check_csp_and_b/0,
29
30		currently_opened_file/1, % only true for successfully opened files
31		currently_opened_file_status/2, % second parameter: success or failure
32		currently_opened_specification_name/1,
33		%reset_currently_opened_file/0,
34		set_currently_opened_file/1, set_currently_opened_b_file/1,
35		set_failed_to_open_file/1,
36		set_minor_animation_mode_from_file/1,
37		set_currently_opening_file/1,
38		set_currently_opened_package/1,
39		spec_file_has_been_successfully_loaded/0,
40		b_absolute_file_name_relative_to_opened_file/2,
41
42		state_corresponds_to_initialised_b_machine/1, state_corresponds_to_initialised_b_machine/2,
43		state_corresponds_to_fully_setup_b_machine/1, state_corresponds_to_fully_setup_b_machine/2,
44		state_corresponds_to_set_up_constants/1,
45		state_corresponds_to_set_up_constants/2, state_corresponds_to_set_up_constants_only/2,
46		extract_variables_from_state/2, extract_variables_from_state_as_primed/2,
47		current_b_expression/1,
48		get_current_state_for_b_formula/2, get_state_for_b_formula/3,
49
50		get_operation_name/2, get_operation_internal_name/2,
51		translate_operation_name/2,
52		get_operation_arguments/2, get_operation_return_values_and_arguments/3,
53		get_operation_description/2, get_operation_description_for_transition/4,
54		get_operation_description_for_transition_id/3,
55		build_up_b_real_operation/2,
56		expand_const_and_vars/3, expand_const_and_vars_to_full_store/2,
57		expand_to_constants_and_variables/3,
58
59		get_specific_time_out_for_operation/2,
60		get_specific_max_operations_for_operation/2,
61		max_operations_zero_for_operation/1,
62		max_operations_zero_for_setup_constants/0, max_operations_zero_for_initialisation/0,
63		compute_operation_effect_max/6, % has replaced compute_operation_effect/5
64		create_setup_constants_operation/3,
65		get_internal_representation/1, get_internal_representation/4,
66		get_possible_event/1, get_feasible_event/1,
67		get_possible_language_specific_top_level_event/3,
68		get_specification_description/2,
69		get_local_state_for_operation_transition/3,
70		get_local_states_for_operation_transition/4, create_local_store_for_operation/4
71		]).
72
73		:- use_module(tools).
74
75		:- use_module(module_information).
76		:- module_info(group,animator).
77		:- module_info(description,'This module computes transitions and properties depending on the current animator mode.').
78
79		:- use_module(library(lists)).
80		%:- use_module(library(avl)).
81		%:- use_module(library(clpfd)).
82
83		:- use_module(debug).
84		:- use_module(b_interpreter).
85		:- use_module(preferences).
86		:- use_module(self_check).
87		:- use_module(error_manager).
88		:- use_module(translate).
89		:- use_module(succeed_max,[succeed_max_call_id/3]).
90
91		:- use_module(store,[empty_state/1]).
92		:- use_module(bmachine).
93		:- use_module(bsyntaxtree).
94		:- use_module(xtl_interface).
95
96
97		%% :- use_module(delay).
98
99		:- use_module(value_persistance, [load_constants/2]).
100
101		:- set_prolog_flag(double_quotes, codes).
102
103		/* --------------------------------- */
104
105
106
107
108		/* --------------------------------- */
109		/* ANIMATION & TEMPORAL VERIFICATION */
110		/* --------------------------------- */
111
112
113		:- dynamic animation_mode/1, animation_minor_mode/1.
114		% not marking as volatile; otherwise we startup with no animation_mode set
115		% not all parts of ProB can deal with this at the moment
116		%:- volatile animation_mode/1, animation_minor_mode/1.
117
118		animation_mode(b).
119		% possible values: b, csp, xtl, z, csp_and_b, promela
120		% animation_minor_mode: possible values alloy, event_b, tla, z (classical B if no animation_minor_mode fact)
121
122		b_mode :- animation_mode(X), (X=b ; X=csp_and_b).
123		z_mode :- animation_mode(X), (X=b ; X=csp_and_b), animation_minor_mode(z).
124	?	classical_b_mode :- b_mode, (animation_minor_mode(Mode) -> classical_minor_mode(Mode) ; true).
125		classical_minor_mode(rules_dsl).
126
127		eventb_mode :-
128		animation_mode(X), (X=b ; X=csp_and_b),
129		animation_minor_mode(eventb).
130		csp_with_bz_mode :- animation_mode(csp_and_b).
131		z_or_tla_minor_mode :- animation_minor_mode(X), (X=tla ; X=z).
132
133		csp_mode :- animation_mode(X), csp_mode(X).
134		csp_mode(cspm).
135		csp_mode(csp_and_b).
136
137		xtl_mode :- animation_mode(xtl).
138		sequent_prover_mode :- animation_mode(xtl), animation_minor_mode(sequent_prover).
139
140		b_or_z_mode :-
141		(animation_mode(X) -> (X=b -> true ; X=csp_and_b)). % basically the same as b_mode
142		b_or_z_mode(b). b_or_z_mode(csp_and_b).
143
144		% is B syntax (ASCII/Unicode available for source files)
145		b_syntax_available_for_source :-
146		b_or_z_mode,
147		(animation_minor_mode(X) -> X=event_b ; true).
148
149		process_algebra_mode :- %Note: also covers xtl (Promela, CCS interpreters; see test 756); used for translating events (tau, tick, io(...))
150		animation_mode(X), X \= b,
151		\+ ((X=xtl, xtl_get_definition_string('PROCESS_ALGEBRA_MODE',false))).
152
153		set_animation_mode(X) :-
154		retractall(animation_mode(_)),
155		remove_animation_minor_mode,
156		assertz(animation_mode(X)).
157
158		set_animation_minor_mode(X) :-
159		remove_animation_minor_mode,
160		assertz(animation_minor_mode(X)).
161		remove_animation_minor_mode :-
162		retractall(animation_minor_mode(_)).
163
164		% use to temporarily unset animation minor mode:
165		:- use_module(library(lists),[maplist/2]).
166		unset_animation_minor_modes(L) :- findall(X,retract(animation_minor_mode(X)),L).
167		reset_animation_minor_modes(L) :- maplist(add_animation_minor_mode,L).
168
169		add_animation_minor_mode(X) :-
170		(animation_minor_mode(X) -> true ; assertz(animation_minor_mode(X))).
171
172
173		:- dynamic currently_opened_file_status/2.
174		:- volatile currently_opened_file_status/2.
175		%currently_opened_file(none).
176
177		:- use_module(bmachine,[b_machine_name/1]).
178		currently_opened_specification_name(Name) :-
179		(b_or_z_mode -> b_machine_name(Name)
180		; currently_opened_file(File),
181		get_modulename_filename(File,Name)
182		).
183
184		reset_currently_opened_file :- retractall(currently_opened_file_status(_,_)).
185		reset_specfile :- reset_currently_opened_file,
186		retractall(animation_minor_mode(_)).
187		:- use_module(eventhandling,[register_event_listener/3]).
188		:- register_event_listener(clear_specification,reset_specfile,
189		'Reset Specfile Currently Opened File.').
190
191		% call if a spec was not loaded from file but from package (e.g., via socket / prob2)
192		set_currently_opened_package(Type) :-
193		set_currently_opened_file(package(Type)).
194
195		% indicates we are in the process of opening a file
196		set_currently_opening_file(File) :-
197		reset_currently_opened_file,
198		assertz(currently_opened_file_status(File,opening)),
199		set_minor_animation_mode_from_file(File).
200
201		:- use_module(tools,[get_filename_extension/2]).
202		set_minor_animation_mode_from_file(File) :-
203		get_filename_extension(File,Extension),
204		file_extension_mode(Extension,Major,ExpectedMinor),!,
205		animation_mode(CurMajor),
206		(CurMajor=Major
207		-> (animation_minor_mode(CurMinor)
208		-> (CurMinor=ExpectedMinor -> true
209		; member(CurMinor,ExpectedMinor) -> true % is amongst the valid options
210		; add_warning(specfile,'Minor animation mode incompatible with file: ',CurMinor:File)
211		)
212		; ExpectedMinor=none -> true
213	?	; member(none,ExpectedMinor) -> true
214		; set_animation_minor_mode(ExpectedMinor)
215		)
216		; add_warning(specfile,'Major animation mode incompatible with file: ',CurMajor:File)
217		).
218		set_minor_animation_mode_from_file(File) :- add_warning(specfile,'Unknown file extension: ',File).
219
220		:- use_module(probsrc(tools_platform), [host_platform/1]).
221		file_extension_mode(mch,b,none). % classical b, could also be csp_and_b
222		file_extension_mode(ref,b,none).
223		file_extension_mode(imp,b,none).
224		file_extension_mode(def,b,none).
225		file_extension_mode(sys,b,none).
226		file_extension_mode(rmch,b,rules_dsl).
227		file_extension_mode(prob,b,[none,tla]). % Here we cannot infer the mode; TODO: in future store this info in the .prob file
228		file_extension_mode(tla,b,tla).
229		file_extension_mode(fuzz,b,z).
230		file_extension_mode(tex,b,z).
231		file_extension_mode(eventb,b,eventb).
232		file_extension_mode(pl,xtl,none). % can be proof obligation files (sequent_prover minor mode)
233		file_extension_mode(probpo,xtl,sequent_prover). % proof obligation files (sequent_prover minor mode)
234		file_extension_mode('P',xtl,none).
235		file_extension_mode('p',xtl,none) :- host_platform(windows),
236		add_message(specfile,'Lower-case file extension .p treated as .P for XTL mode').
237		file_extension_mode(als,b,alloy).
238		file_extension_mode(csp,cspm,none).
239		file_extension_mode(cspm,cspm,none).
240
241		% store currently openend specification file and set B minor animation mode
242		set_currently_opened_b_file(File) :-
243		set_currently_opened_file(File),
244		set_minor_animation_mode_from_file(File).
245
246		set_currently_opened_file(File) :-
247		reset_currently_opened_file,
248		assertz(currently_opened_file_status(File,success)).
249
250		set_failed_to_open_file(File) :-
251		reset_currently_opened_file,
252		assertz(currently_opened_file_status(File,failure)).
253
254		currently_opened_file(File) :- currently_opened_file_status(File,success).
255
256
257		:- use_module(tools,[safe_absolute_file_name/3, get_parent_directory/2]).
258		% open a file relateive to the main B file
259		b_absolute_file_name_relative_to_opened_file(File,AbsFileName) :-
260		currently_opened_file_status(MainFileName,_Status), % _Status=failure happens when error during loading
261		get_parent_directory(MainFileName,Directory),
262		safe_absolute_file_name(File,AbsFileName,[relative_to(Directory)]).
263
264		spec_file_has_been_successfully_loaded :- currently_opened_file(_).
265
266		:- use_module(bmachine,[b_machine_has_variables/0]).
267		% true if state corresponds to an initialised B machine
268		state_corresponds_to_initialised_b_machine(const_and_vars(_,_)) :- !,
269		b_or_z_mode.
270		state_corresponds_to_initialised_b_machine(expanded_const_and_vars(_,_,_,_)) :- !,
271		b_or_z_mode.
272		state_corresponds_to_initialised_b_machine(expanded_vars(_,_)) :- !,
273		b_or_z_mode.
274		state_corresponds_to_initialised_b_machine([]).
275		state_corresponds_to_initialised_b_machine([_|_]).
276		state_corresponds_to_initialised_b_machine(csp_and_b(_,BState)) :-
277		csp_with_bz_mode,
278		state_corresponds_to_initialised_b_machine(BState).
279
280
281		% check if state corresponds to an initialised B machine, and if so return expanded State
282		state_corresponds_to_initialised_b_machine(const_and_vars(ConstID,Vars),State) :- !,
283		b_or_z_mode, expand_const_and_vars(ConstID,Vars,State).
284		state_corresponds_to_initialised_b_machine(expanded_const_and_vars(_ConstID,_Vars,FullStore,_),State) :- !,
285		% generated by prepare_state_for_specfile_trans
286		State=FullStore.
287		state_corresponds_to_initialised_b_machine(expanded_vars(FullStore,_),State) :- !,
288		% generated by prepare_state_for_specfile_trans
289		State=FullStore.
290		state_corresponds_to_initialised_b_machine([],[]).
291		state_corresponds_to_initialised_b_machine([H|T],[H|T]).
292		state_corresponds_to_initialised_b_machine(csp_and_b(_,BState),State) :-
293		csp_with_bz_mode,
294		state_corresponds_to_initialised_b_machine(BState,State).
295
296		% check if all variables, constants setup; also allows concrete_constants if no variables exist
297		state_corresponds_to_fully_setup_b_machine(concrete_constants(_)) :- !, b_or_z_mode,
298		\+ b_machine_has_variables.
299		state_corresponds_to_fully_setup_b_machine(X) :- state_corresponds_to_initialised_b_machine(X).
300
301		state_corresponds_to_fully_setup_b_machine(concrete_constants(Constants),State) :- !, b_or_z_mode,
302		\+ b_machine_has_variables, State=Constants.
303		state_corresponds_to_fully_setup_b_machine(X,State) :- state_corresponds_to_initialised_b_machine(X,State).
304
305		% check if we only have constants, no variable values yet
306		state_corresponds_to_set_up_constants_only(root,State) :- !, animation_mode(b),
307		\+ b_machine_has_constants_or_properties, State=[]. % relevant for test 960
308		state_corresponds_to_set_up_constants_only(concrete_constants(Constants),State) :- !,
309		b_or_z_mode, State=Constants.
310		state_corresponds_to_set_up_constants_only(csp_and_b(_,BState),State) :- !,
311		csp_with_bz_mode,
312		state_corresponds_to_set_up_constants_only(BState,State).
313
314		state_corresponds_to_set_up_constants(const_and_vars(_,_)) :- !. % avoid expansion
315		state_corresponds_to_set_up_constants(X) :- state_corresponds_to_set_up_constants(X,_).
316
317		state_corresponds_to_set_up_constants(const_and_vars(ConstID,Vars),State) :- !,
318		b_or_z_mode, expand_const_and_vars(ConstID,Vars,State).
319		state_corresponds_to_set_up_constants(expanded_const_and_vars(_ConstID,_Vars,FullStore,_),State) :- !,
320		% generated by prepare_state_for_specfile_trans
321		State=FullStore.
322		state_corresponds_to_set_up_constants(expanded_vars(FullStore,_),State) :- !,
323		% generated by prepare_state_for_specfile_trans
324		State=FullStore.
325		state_corresponds_to_set_up_constants(concrete_constants(Constants),State) :- !,
326		b_or_z_mode, State=Constants.
327		state_corresponds_to_set_up_constants(csp_and_b(_,BState),State) :- !,
328		csp_with_bz_mode,
329		state_corresponds_to_set_up_constants(BState,State).
330		state_corresponds_to_set_up_constants([],State) :- !, State=[],
331		animation_mode(b).
332		state_corresponds_to_set_up_constants(State,RState) :-
333		animation_mode(b),
334		(State = root -> \+ b_machine_has_constants_or_properties,RState=[] ; RState=State).
335
336		:- use_module(state_space,[current_expression/2]).
337		current_b_expression(CurBState) :-
338		current_expression(_CurID,CurState),
339		state_corresponds_to_set_up_constants(CurState,CurBState).
340
341
342
343		:- use_module(state_space, [current_state_id/1]).
344		:- use_module(bmachine, [determine_type_of_formula/2]).
345		% get a state sufficient to evaluate a given formula (expression or predicate)
346		% it will give an error is the machine is not sufficiently initialised
347		get_current_state_for_b_formula(TypedExpr,BState) :-
348		current_state_id(CurID),
349		get_state_for_b_formula(CurID,TypedExpr,BState).
350		get_state_for_b_formula(StateID,TypedExpr,BState) :-
351		(formula_class(TypedExpr) -> Type=TypedExpr % user already provided formula class
352		; determine_type_of_formula(TypedExpr,Type)), % TODO: extract used ids and only expand those that are required
353		get_state(Type,StateID,TypedExpr,BState).
354
355		formula_class(requires_nothing).
356		formula_class(requires_constants).
357		formula_class(requires_variables).
358
359		:- use_module(probsrc(state_space),[get_constants_state_for_id/3]).
360		get_state(requires_nothing,_ID,_TE,[]).
361		get_state(requires_constants,StateID,TypedExpr,BState) :-
362		(get_constants_state_for_id(StateID,[allow_variable_list],BState) -> true
363		; ajoin(['Please setup constants first, cannot evaluate (in state ',StateID,') :'],Msg),
364		add_error(get_state,Msg,TypedExpr,TypedExpr),fail).
365		get_state(requires_variables,StateID,TypedExpr,BState) :-
366		my_visited_expression(StateID,State),
367		(state_corresponds_to_initialised_b_machine(State,BState) -> true ;
368		ajoin(['Please initialise machine first, cannot evaluate (in state ',StateID,') :'],Msg),
369		add_error(get_state,Msg,TypedExpr,TypedExpr),fail).
370		% TO DO: we could try and get only those identifiers that are really used
371
372		:- use_module(state_space,[visited_expression/2]).
373		my_visited_expression(root,S) :- !,
374		S=root. % ensure we succeed even if no state space set (e.g. when no machine provided to probcli)
375		my_visited_expression(StateID,State) :- visited_expression(StateID,State).
376
377		/* TRANSITIONS */
378
379		:- use_module(tools_meta,[call_residue/2]).
380		% ---------------------------------------------------
381
382
383		% Tries to find successor state for Op in State DB. Fails, if no solution is possible
384		% Input: State DB, Operation Op
385		% Output: DB2 the sucessor state
386		% Residue: Unfinished co-routines (should not happen!)
387		%specfile_trans(DB,Op,DB2,[]) :- !, specfile:i_transition(DB,Op,DB2).
388		specfile_trans(DB,OpName,Op,DB2,TransInfo,Residue) :-
389		% i_transition(DB,OpName,Op,DB2,TransInfo), Residue = []. % is faster, but no residue checking
390		animation_mode(MODE),
391	?	call_residue(i_transition(MODE,DB,OpName,Op,DB2,TransInfo),Residue).
392
393		i_transition(b,State,OpName,Op,NewState,TransInfo) :- !,
394	?	b_trans(State,OpName,Op,NewState,TransInfo).
395		i_transition(xtl,State,OpName,Op,NewState,TransInfo) :- !,
396	?	xtl_transition(State,Op,NewState,TransInfo), functor(Op,OpName,_).
397		i_transition(cspm,State,_OpName,Op,NewState,[]) :- !,
398		% Note: the OpName is ignored: we cannot make use of it
399	?	cspm_transition(State,Op,NewState).
400		%i_transition(promela,State,_OpName,Op,NewState,[]) :- !,
401		% promela_transition(State,Op,NewState).
402		% ; MODE=smv -> smv_transition(State,Op,NewState),TransInfo=[]
403		i_transition(csp_and_b,State,OpName,Op,NewState,TransInfo) :- !,
404		% Note: the OpName is either the name of a B operation or '$CSP' (or a variable)
405	?	csp_and_b_transition(State,OpName,Op,NewState,TransInfo).
406
407
408		% if you call specfile_trans multiple times for the same state, it is
409		% more efficient to call this predicate first once
410		prepare_state_for_specfile_trans(const_and_vars(ConstID,Vars),CurID,R) :- !, %print(expanding_const(ConstID)),nl,
411		R = expanded_const_and_vars(ConstID,Vars,FullStore,Infos),
412		expand_const_and_vars(ConstID,Vars,FullStore), %, print(full(FullStore)),nl.
413		prepare_infos(FullStore,CurID,Infos).
414		prepare_state_for_specfile_trans(FullStore,CurID,R) :- FullStore=[_|_],
415		prepare_infos(FullStore,CurID,Infos), Infos \=[],
416		!,
417		R = expanded_vars(FullStore,Infos).
418		prepare_state_for_specfile_trans(csp_and_b(CSP,BStore),CurID,csp_and_b(CSP,Res)) :- !,
419		prepare_state_for_specfile_trans(BStore,CurID,Res).
420		prepare_state_for_specfile_trans(X,_,X).
421
422		% a version with a memo argument to store expanded constants
423		prepare_state_for_specfile_trans(const_and_vars(ConstID,Vars),CurID,MEMO,R) :- !, %print(expanding_const(ConstID)),nl,
424		R = expanded_const_and_vars(ConstID,Vars,FullStore,Infos),
425		(nonvar(MEMO),MEMO = [ConstID/ConstantsStore]
426		% constants have already been previously extracted; e.g., in model_checker loop
427		-> %tools_printing:print_term_summary(memo(ConstID,ConstantsStore)),nl,
428		append(Vars,ConstantsStore,FullStore) % simply reuse expanded constants in MEMO
429		% used to be constants first, but has to be compatible with b_initialise_machine2 and expand_const_and_vars/3
430		; % expand_const_and_vars/3 inlined (so as to obtain ConstantsStore
431		visited_expression(ConstID,concrete_constants(ConstantsStore)), %% This can take a while if the Constants are big !
432		% print(no_memo(ConstID,MEMO)),tools_printing:print_term_summary(ConstantsStore),nl,
433		append(Vars,ConstantsStore,FullStore),
434		(var(MEMO)
435		-> MEMO=[ConstID/ConstantsStore] % store expanded constants to avoid unpacking again
436		; true)
437		), %, print(full(FullStore)),nl.
438		prepare_infos(FullStore,CurID,Infos).
439		prepare_state_for_specfile_trans(FullStore,CurID,_,R) :- FullStore=[_|_],
440		prepare_infos(FullStore,CurID,Infos), Infos \=[], !,
441		R = expanded_vars(FullStore,Infos).
442		prepare_state_for_specfile_trans(csp_and_b(CSP,BStore),CurID,MEMO,csp_and_b(CSP,Res)) :- !,
443		prepare_state_for_specfile_trans(BStore,CurID,MEMO,Res).
444		prepare_state_for_specfile_trans(X,_,_,X). % TODO: prepare infos as well if we have no constants
445
446		:- use_module(state_packing,[pack_state/2, get_packed_b_state_with_uncompressed_lists/2]).
447		% store some operation independent infos which are useful
448		prepare_infos(FullStore,CurID,Infos) :- CurID \= root,
449		(get_preference(operation_reuse_setting,false)
450		-> Infos = []
451		% TO DO: check if we should enable this: get_preference(use_state_packing,true)
452		% TODO: we could check if there are operations which do not write all variables
453		; Infos=[packed_state/PackedList, state_id/CurID],
454		(CurID \= unknown, state_space:packed_visited_expression(CurID,PS),
455		get_packed_b_state_with_uncompressed_lists(PS,PackedList) % replace '$cst_vars' and compressed lists
456		-> true %,write('+')
457		; format('prepare_infos for state ~w: need to pack_values~n',[CurID]), % should ideally not happen
458		pack_state(FullStore,PS), % precompute state packing; will be re-used multiple times
459		get_packed_b_state_with_uncompressed_lists(PS,PackedList)
460		)
461		).
462
463		% extract pre-computed infos
464		extract_infos_from_prepared_state(expanded_const_and_vars(_,_,_,Infos),Res) :- !, Res=Infos.
465		extract_infos_from_prepared_state(expanded_vars(_,Infos),Res) :- !, Res=Infos.
466		extract_infos_from_prepared_state(_,[]).
467
468		remove_infos_from_prepared_state(expanded_const_and_vars(C,V,_,_),Res) :- !, Res=const_and_vars(C,V).
469		remove_infos_from_prepared_state(expanded_vars(V,_),R) :- !, R=V.
470		remove_infos_from_prepared_state(S,S).
471
472		% extract initialised variables from a state
473		extract_variables_from_state(const_and_vars(_,V),R) :- !,R=V.
474		extract_variables_from_state(expanded_const_and_vars(_,V,_,_),R) :- !,R=V.
475		extract_variables_from_state(expanded_vars(V,_),R) :- !,R=V.
476		extract_variables_from_state([],[]).
477		extract_variables_from_state([H|T],[H|T]).
478
479		:- use_module(probsrc(btypechecker),[prime_atom0/2]). % add $0 at end of variable
480		prime_binding(bind(ID,V),bind(PID,V)) :- prime_atom0(ID,PID).
481
482		extract_variables_from_state_as_primed(SrcState,PrimedVarBindings) :-
483		extract_variables_from_state(SrcState,VarVals),
484		maplist(prime_binding,VarVals,PrimedVarBindings).
485
486
487		/* can be attempted if trans fails to attempt to use partially computed transitions */
488		partial_trans(DB,Op,DB2,Residue) :-
489		call_residue(partial_i_transition(DB,Op,DB2),Residue).
490
491		partial_i_transition(root,'$partial_setup_constants',concrete_constants(ConstantsStore)) :-
492		animation_mode(b),
493		set_error_context(operation('$partial_setup_constants',root)),
494		b_interpreter:b_partial_set_up_concrete_constants(ConstantsStore).
495
496		% a predicate which automatically calls partial_trans :
497		specfile_trans_or_partial_trans(DB,OpName,Op,DB2,TransInfo,Residue,Partial) :-
498	?	if(specfile_trans(DB,OpName,Op,DB2,TransInfo,Residue),Partial=false,
499		(OpName='$setup_constants', % OpName is often an input argument here
500		TransInfo=[], Partial = true,
501		partial_trans(DB,Op,DB2,Residue))).
502
503		/* build up skeletons of possible operations; to be used before time_out call is made */
504		% currently only used in zmq worker.pl
505		specfile_possible_trans_name(State,OpName) :- animation_mode(MODE),
506		(MODE=b -> b_possible_trans_name(State,OpName)
507		; MODE = csp_and_b -> csp_b_possible_trans_name(State,OpName)
508		; setup_transition_skeleton(MODE,OpName) /* TO DO: add more possible skeletons */
509		).
510
511		% only set up skeletons if it is worth it for computing all successors
512		% e.g., currently it is not worth it to setup skeletons for either CSP or CSP||B (due to renaming,... we cannot predict which parts of a CSP process can be excluded)
513		specfile_possible_trans_name_for_successors(State,OpName) :- animation_mode(MODE),
514		(MODE=b
515	?	-> b_possible_trans_name(State,OpName)
516		; setup_transition_skeleton(MODE,OpName)
517		).
518
519		setup_transition_skeleton(_,_). /* TO DO: add more possible skeletons ? */
520
521		:- use_module(library(random)).
522		b_possible_trans_name(root,OpName) :- !,
523		(b_machine_has_constants_or_properties
524		-> OpName = '$setup_constants'
525		; OpName = '$initialise_machine').
526		b_possible_trans_name(concrete_constants(_),OpName) :- !, OpName = '$initialise_machine'.
527		b_possible_trans_name(_State,OpName) :-
528		(preferences:preference(randomise_operation_order,true),random(1,3,1)
529		-> b_machine_operation_names_in_reverse_order(OpName) ; true),
530		%b_get_machine_operation(OpName,_Res,_Params,_,_,_).
531	?	b_top_level_feasible_operation(OpName). % TO DO: we could link also with cbc feasibility analysis if carried out
532		% we could check: b_operation_cannot_modify_state(OpName) given a preference, in particular for SAFETY_MODEL_CHECK when operation already covered
533
534		csp_b_possible_trans_name(csp_and_b_root,OpName) :- !,
535		(b_machine_has_constants_or_properties
536		-> OpName = 'tau($setup_constants)'
537		; OpName = 'tau($initialise_machine)').
538		csp_b_possible_trans_name(concrete_constants(_),OpName) :- !,
539		OpName = 'tau($initialise_machine)'.
540		csp_b_possible_trans_name(State,OpName) :-
541		b_possible_trans_name(State,OpName).
542		% TO DO: add non-synchronised channels
543
544		% --------------
545
546		:- use_module(probcspsrc(haskell_csp),[channel_type_list/2, symbol/4]).
547		:- use_module(debug).
548		% check whether a currently open CSP is type compatible with a loaded B machine
549		type_check_csp_and_b :- animation_mode(csp_and_b), debug_println(9,type_check_csp_and_b),
550	?	b_get_machine_operation(ChannelOpName,Res,Params,_,_,_), append(Params,Res,ParamsRes),
551		channel_type_list(ChannelOpName,CSPTypeList),
552		% TO DO: also check B variable names which match channel name
553		debug_println(9,checking_synchronised_channel(ChannelOpName,ParamsRes,CSPTypeList)),
554		l_check_compatibility(ParamsRes,CSPTypeList,ChannelOpName),
555		fail.
556		type_check_csp_and_b.
557
558		%convert_csp_type_to_list(type(T),R) :- convert_csp_type_to_list2(T,R).
559		%convert_csp_type_to_list2(dotUnitType,[]).
560		%convert_csp_type_to_list2(dotTupleType(T),T).
561
562		l_check_compatibility([],[],_) :- !.
563		l_check_compatibility([B|BT],[CSP|CSPT],ChannelOpName) :- !, check_compatibility(B,CSP,ChannelOpName),
564		l_check_compatibility(BT,CSPT,ChannelOpName).
565		l_check_compatibility([],CSP,ChannelOpName) :- !,
566		add_error(type_check_csp_and_b,'CSP Channel has too many parameters: ', ChannelOpName:CSP).
567		l_check_compatibility(B,[],ChannelOpName) :- !,
568		print('* CSP Channel has too few parameters: '), print(ChannelOpName),nl,
569		print('* B Arguments will be ignored: '), l_print_bexpr_or_subst(B),nl.
570		%add_error(type_check_csp_and_b,'CSP Channel has too few parameters: ', ChannelOpName:B).
571
572		check_compatibility(b(identifier(ID),TYPE,INFO),CSP_TYPE,ChannelOpName) :- !,
573		(type_ok(TYPE,CSP_TYPE) -> true ;
574		% TO DO: pretty print B and CSP Types
575		add_error(type_check_csp_and_b,'Incompatible types between B and CSP: ',ChannelOpName:ID:(TYPE:CSP_TYPE),b(identifier(ID),TYPE,INFO))
576		).
577		check_compatibility(B,CSP,ChannelOpName) :- !,
578		add_internal_error('Illegal types: ',check_compatibility(B,CSP,ChannelOpName)).
579
580		% TO DO: needs to be refined much more;
581		type_ok(Type,CSPType) :-
582		(type_ok2(Type,CSPType) -> true
583		; add_error(type_check_csp_and_b,'Cannot be converted (B:CSP): ',Type:CSPType),fail).
584		type_ok2(boolean,X) :- !, is_csp_boolean_type(X).
585		type_ok2(integer,X) :- !, is_csp_integer_type(X).
586		type_ok2(string,CSP) :- !,is_csp_global_set_type(CSP,string).
587		type_ok2(set(T),CSP) :- !, is_csp_set_type(CSP,T).
588		% TO DO: what if we have set(couple(integer,T)) instead of seq(T) ?
589		% rye
590		% check set(couple(integer,T)) (seq type) in B
591		type_ok2(seq(T),CSP) :- !, is_csp_seq_type(CSP,T).
592		type_ok2(couple(A,B),CSP) :- !, is_csp_couple_type(CSP,A,B).
593		type_ok2(global(GS),CSP) :- !,is_csp_global_set_type(CSP,GS).
594		type_ok2(X,Y) :- print(unknown(X,Y)),nl.
595
596		is_csp_couple_type(setValue([na_tuple([A|Rest])|_]),TA,TB) :- type_ok(TA,setValue([A])),
597		check_rest_couple_els(Rest,TB).
598		is_csp_couple_type(typeTuple([A|Rest]),TA,TB) :- type_ok(TA,A), check_rest_couple(Rest,TB).
599
600		check_rest_couple_els([B],TB) :- !, type_ok(TB,setValue([B])).
601		check_rest_couple_els([B1|BRest],couple(TB1,TBRest)) :- type_ok(TB1,setValue([B1])),
602		check_rest_couple_els(BRest,TBRest).
603		check_rest_couple([B],TB) :- !, type_ok(TB,B).
604		check_rest_couple([B1|BRest],couple(TB1,TBRest)) :- type_ok(TB1,B1),
605		check_rest_couple(BRest,TBRest).
606
607		% rye
608		% check if it is couple(integer, T) type and return T in 2nd arguments
609		couple_int(couple(integer, T), T). % possible sequence
610
611		% rye: it's not correct to check only Head
612		% % for example, for CSP type, {{}, {(1,2),(2,3)}}. Its head is emptyset, but the second one is set of tuple
613		is_csp_set_type('Set'([H|_]),Type) :- type_ok(Type,H). % just check Head
614		% check the 2nd element in set in case the 1st is emptyset
615		is_csp_set_type(setValue([_|T]),Type) :-
616		T = [H1 | _], !,
617		% if it is set(couple(integer, T)), it can be a sequence type
618		(couple_int(Type, TH1) -> is_csp_seq_type(setValue(T), TH1)
619		; type_ok(Type,H1)
620		). % check the 2nd
621		% if it is only one element in set, just check the head
622		is_csp_set_type(setValue([H|T]),Type) :-
623		(couple_int(Type, TH1) -> is_csp_seq_type(setValue([H|T]), TH1)
624		; type_ok(Type,H)
625		). % just check Head
626
627		is_csp_seq_type('Seq'(H),Type) :- type_ok(Type,H).
628		is_csp_seq_type(setValue([H|_]),Type) :- H=list(L), is_csp_list(L,Type).
629		is_csp_list([],_).
630		is_csp_list([H|_],Type) :- type_ok(Type,setValue([H])).
631
632		is_csp_boolean_type(boolType).
633		is_csp_boolean_type(setValue([H|_])) :- is_csp_boolean_value(H).
634		is_csp_boolean_value(true).
635		is_csp_boolean_value(false).
636
637		is_csp_integer_type(intType).
638		is_csp_integer_type(setFromTo(_,_)).
639		is_csp_integer_type(setFrom(_)).
640		is_csp_integer_type(setValue([int(_)|_])).
641
642		is_csp_global_set_type(dataType(_),_GS). % TO DO CHECK MEMBERS
643		is_csp_global_set_type(setValue([]),_GS). % TO DO CHECK MEMBERS
644		is_csp_global_set_type(setValue([_|_]),_GS). % TO DO CHECK MEMBERS
645
646		% --------------
647
648
649		:- use_module(bmachine,[b_get_machine_operation/4]).
650		:- use_module(bsets_clp,[tuple_of/3]).
651		% compute transitions for a CSP || B specification
652		% Note: the OpName is either the name of a B machine operation (even if hidden) or '$CSP' (useful for ltsmin)
653		csp_and_b_transition(root,OpName,Op,NewState,TransInfo) :- !,
654		Op = start_cspm_MAIN, OpName=Op, NewState = csp_and_b_root,TransInfo = [].
655		csp_and_b_transition(csp_and_b_root,OpName,Trans,NewState,TransInfo) :- !,
656		Trans = tau(Op), OpName = '$CSP',
657	?	b_trans(root,_,Op,InitialBState,TransInfo),
658		(InitialBState = concrete_constants(_)
659		-> NewState = InitialBState
660		; csp_initialisation_for_b(InitialCSPState),
661		NewState = csp_and_b(InitialCSPState,InitialBState)
662		).
663		csp_and_b_transition(concrete_constants(C),OpName,Trans,NewState,TransInfo) :- !,
664		Trans = tau(Op), OpName = '$CSP',
665		b_trans(concrete_constants(C),_,Op,InitialBState,TransInfo),
666		csp_initialisation_for_b(InitialCSPState),
667		NewState = csp_and_b(InitialCSPState,InitialBState).
668		csp_and_b_transition(csp_and_b(CSPState,BState),OpName,EventVisibleToUser,csp_and_b(NewCSP,NewB),TransInfo) :-
669		!,
670	?	csp_transition_for_b(CSPState,ChOpName,ChArgs,CSPAction,NewCSP),
671		% TO DO: split up csp_transition_for_b: into two parts; second part converts datatypes and only called if linking op exists
672		%% print(csp_trans(ChOpName,ChArgs)),nl, %%
673		length(ChArgs,Len), length(OpArgs,Len),
674	?	b_transition_for_csp(ChOpName,CSPAction,ChArgs,OpArgs,BState,OpName,Operation,NewB,TransInfo),
675	?	hide_csp_event(CSPAction,Operation,EventVisibleToUser).
676		csp_and_b_transition(State,'$CSP',Op,NewState,[]) :-
677		% we have a pure CSP state: use CSP-M transition
678	?	cspm_transition(State,Op,NewState).
679
680		:- use_module(bmachine,[b_is_variable/1,b_is_constant/1]).
681		% compute the B counterpart for a CSP transition:
682		b_transition_for_csp(ChOpName,_CSPAction,ChArgs,OpArgs,BState,OpName,Operation,NewB,TransInfo) :-
683	?	build_up_b_operation_for_csp(ChOpName,OpArgs,Operation),
684		!,
685		OpName = ChOpName,
686		%% print_message(trying_b_trans(Operation,ChArgs,OpArgs)), %%
687		(get_preference(operation_reuse_setting,false)
688		-> generate_b_operationargs_from_csp(ChArgs,OpArgs),
689	?	b_trans(BState,OpName,Operation,NewB,TransInfo)
690		;
691		% compute B transition without parameters so that we can cache
692	?	b_trans(BState,OpName,Operation,NewB,TransInfo),
693		% and unify afterwards
694		generate_b_operationargs_from_csp(ChArgs,OpArgs)
695		).
696		%%, print_message(csp_btrans(Operation)), %%.
697		b_transition_for_csp(ChOpName,_CSPAction,ChArgs,OpArgs,BState,OpName,Operation,NewB,TransInfo) :-
698		OpName = ChOpName,
699		(b_is_variable(ChOpName) ; b_is_constant(ChOpName)),
700		%% print(probing(ChOpName)),nl,
701		expand_const_and_vars_to_full_store(BState,FBState),
702		try_lookup_value_in_store_and_global_sets(ChOpName,FBState,IdValue),
703		!,
704		remove_infos_from_prepared_state(BState,NewB),
705		TransInfo=[],
706		/* interpret as probing operation: get value of var,cst,SET */
707		generate_b_operationargs_from_csp(ChArgs,OpArgs),
708		(OpArgs=[SingleVal]
709		-> SingleVal = IdValue, Operation='-->'(ChOpName,[IdValue])
710		; OpArgs=[Val1,Val2],
711	?	tuple_of(Val1,Val2,IdValue), /* from bsets_clp, use exact_element_of ??? */
712		OpCall =.. [ChOpName,Val1],
713		Operation='-->'(OpCall,[Val2])
714		).
715		b_transition_for_csp(_ChOpName,CSPAction,_ChArgs,_OpArgs,BState,OpName,Operation,NewB,TransInfo) :-
716		OpName = '$CSP', % all CSP events grouped together
717		remove_infos_from_prepared_state(BState,NewB),
718		TransInfo=[],
719		/* no B operation of the name; could be tau or tick or extra comm channel */
720		%Op1 =.. [ChOpName|OpArgs],
721		Operation = CSPAction. % removed csp(.) wrapper [for LTL model checker]
722
723		hide_csp_event(CSPAction,_,EventVisibleToUser) :-
724		symbol('HIDE_CSPB',_,Span,_),!, % if there is a HIDE_CSPB definition then we do MAIN [{| HIDE_CSPB |}] B_MACHINE \ {| HIDE_CSPB |}
725		haskell_csp:evaluate_argument(val_of('HIDE_CSPB',Span),EvCList),
726		% print(hide(EvCList,CSPAction)),nl,
727		haskell_csp:expand_channel_pattern_expression(EvCList,ECList,no_loc_info_available),
728	?	haskell_csp:cspm_hide_action(CSPAction,omega,ECList, Span, EventVisibleToUser,_).
729		hide_csp_event(_CSPAction,Operation,EventVisibleToUser) :-
730		% get_preference(csp_event_visible_to_user,true) -> EventVisibleToUser = CSPAction
731		EventVisibleToUser = Operation.
732
733		build_up_b_operation_for_csp(OpName,OpArgs,Operation) :- %print(csp(OpName,OpArgs,Operation)),nl,
734		nonvar(OpName),
735		b_get_machine_operation(OpName,Res,Params,_), %print(get_machine_op(OpName,Res,Params)),nl,
736	?	specfile:generate_args(OpArgs,Params,Res, BArgs,BResults,OpName), %print(gen_args(BArgs,BResults)),nl,
737		% TO DO: either also extract types from Params, Res or better write a static checker that tests that the B operation and CSP channel types are compatible
738		safe_univ(Op1,[OpName|BArgs]), %print(op1(Op1)),nl,
739		(BResults = [] -> Operation = Op1 ; Operation = '-->'(Op1,BResults)).
740
741		:- use_module(bmachine,[b_get_machine_operation_for_animation/6]).
742		build_up_b_real_operation(OpName,Operation) :-
743		b_get_machine_operation_for_animation(OpName,Res,Params,_,_,true), %true==TopLevel
744		length(Params,Len), length(OpArgs,Len),
745		length(Res,RLen), length(BResults,RLen),
746		safe_univ(Op1,[OpName|OpArgs]),
747		(BResults = [] -> Operation = Op1 ; Operation = '-->'(Op1,BResults)).
748
749		generate_args([],[],Res,[],BRes,_) :- length(Res,L), length(BRes,L).
750		generate_args([],[_Param|T],Res,[_|TA],BRes,OpName) :-
751	?	generate_args([],T,Res,TA,BRes,OpName).
752		generate_args([CSPArg|TC],[Param|T],Res,[CSPArg|TA],BRes,OpName) :- check_type_for_id(CSPArg,Param,OpName),
753	?	generate_args(TC,T,Res,TA,BRes,OpName).
754		generate_args([CSPArg|TC],[],[ReturnParam|TRes],[],[CSPArg|TBRes],OpName) :-
755		check_type_for_id(CSPArg,ReturnParam,OpName),
756	?	generate_args(TC,[],TRes,[],TBRes,OpName).
757		generate_args([H|T],[],[],[],[],OpName) :-
758		add_error(specfile,'CSP provides extra arguments: ',OpName:[H|T]).
759
760		check_type_for_id(Val,TID,OpName) :- get_texpr_type(TID,Type),
761		check_type(Type,Val,OpName:TID).
762
763		:- block check_type(?,-,?).
764		check_type(boolean,pred_true,_) :- !.
765		check_type(boolean,pred_false,_) :- !.
766		check_type(integer,int(_),_) :- !.
767		check_type(string,string(_),_) :- !.
768		check_type(global(GS),fd(_,GS),_) :- !.
769		check_type(couple(A,B),(VA,VB),OID) :- !, check_type(A,VA,OID), check_type(B,VB,OID).
770		check_type(set(_T),[],_) :- !.
771		check_type(set(_T),closure(_,_,_),_) :- !. % TO DO: check type signature of closure
772		check_type(set(T),[H|_],OID) :- !, check_type(T,H,OID).
773		check_type(set(T),avl_set((node(Y,_,_,_L,_R))),OID) :- !, check_type(T,Y,OID).
774		check_type(seq(T),V,OID) :- !, check_type(set(couple(integer,T)),V,OID).
775		% TO DO: record, freetype ; but do not appear in translation from CSP to B yet
776		check_type(Type,Value,OpName:TID) :-
777		def_get_texpr_id(TID,ID),
778		add_error(check_type_for_id,'Illegal CSP value for argument: ',OpName:ID:type(Type):value(Value)),
779		fail.
780
781		get_operation_internal_name(Op,Name) :- var(Op),!,
782		add_error(get_operation_internal_name,'Variable Transition: ',Op), Name=Op.
783		get_operation_internal_name('$initialise_machine',N) :- !, N='$initialise_machine'.
784		get_operation_internal_name('$setup_constants',N) :- !, N='$setup_constants'.
785		get_operation_internal_name('$partial_setup_constants',N) :- !, N='$partial_setup_constants'.
786		get_operation_internal_name(Op,Name) :- get_operation_name(Op,Name).
787
788		is_setup_constants_internal_name('$setup_constants').
789		is_setup_constants_internal_name('$partial_setup_constants').
790
791		% tool to get the basic operation/channel/event name of a transition:
792		get_operation_name(Op,Name) :- var(Op),!, add_error(get_operation_name,'Variable Transition: ',Op), Name=Op.
793		get_operation_name('-->'(F,_),N) :- !, functor(F,N,_).
794		%get_operation_name(io([Action|_],proc(_Nr,_PROC),_SPAN),F) :-
795		% animation_mode(promela),!,functor(Action,F,_).
796		get_operation_name(io(_V,Ch,_SPAN),N) :- csp_mode,!, functor(Ch,N,_).
797		get_operation_name(FullOperation,Name) :- functor(FullOperation,Functor,_),
798		translate_operation_name(Functor,Name).
799
800		get_operation_arguments(Op,Args) :- var(Op),!, add_error(get_operation_arguments,'Variable Transition: ',Op), Args=[].
801		get_operation_arguments('-->'(F,_ReturnValues),Args) :- !, F =.. [_|Args].
802		%get_operation_arguments(io([_Action|V],proc(_Nr,_PROC),_SPAN),Args) :-
803		% animation_mode(promela),!,Args=V.
804		get_operation_arguments(io(V,_Ch,_SPAN),Args) :- csp_mode,!, Args = V.
805		get_operation_arguments(FullOperation,Args) :- FullOperation =.. [_|Args].
806
807		get_operation_return_values_and_arguments('-->'(F,ReturnValues),ReturnValues,Args) :- !,
808		F =.. [_|Args].
809		get_operation_return_values_and_arguments(Op,[],Args) :- get_operation_arguments(Op,Args).
810
811		translate_operation_name(Var,T) :- var(Var),!,T='_?Operation?_'.
812		translate_operation_name('$initialise_machine',T) :- !,T='INITIALISATION'.
813		translate_operation_name('$setup_constants',T) :- !,T='SETUP_CONSTANTS'.
814		translate_operation_name('$partial_setup_constants',T) :- !,T='PARTIAL_SETUP_CONSTANTS'.
815		%translate_operation_name(InternalName,Res) :- !, Res=InternalName.
816		translate_operation_name(X,X).
817
818		:- use_module(bmachine,[b_get_operation_description/2]).
819		% get a textual description of a transition, based on description pragma
820		get_operation_description(OpTerm,Desc) :- b_or_z_mode,
821		get_operation_name(OpTerm,OpName),
822		b_get_operation_description(OpName,Desc).
823		% in future we could possible use operation parameter values to adapt description
824
825		:- use_module(state_space,[transition/4,transition_info/2]).
826		get_operation_description_for_transition_id(StateId,TransitionId,Desc) :-
827		transition(StateId,OpTerm,TransitionId,NextId), !,
828		(xtl_mode % TODO: allow other modes?
829		-> transition_info(TransitionId,description(Desc))
830		; get_operation_description_for_transition(StateId,OpTerm,NextId,Desc)
831		).
832		get_operation_description_for_transition_id(StateId,TransitionId,_) :-
833		format('No transition from state ~w with id ~w!~n', [StateId,TransitionId]),
834		fail.
835
836		:- use_module(probsrc(b_interpreter),[b_compute_explicit_epression_no_wf/6]).
837		:- use_module(probsrc(bmachine),[get_operation_description_template_expr/2]).
838		% get a description for operation from a given state; to do: we could provide destination state
839		get_operation_description_for_transition(StateId,OpTerm,NextId,Desc) :- xtl_mode, !,
840		transition(StateId,OpTerm,TransitionId,NextId),
841		transition_info(TransitionId,description(Desc)).
842		get_operation_description_for_transition(StateId,OpTerm,NextId,Desc) :- b_or_z_mode,
843		get_operation_internal_name(OpTerm,OpName),
844		get_operation_description_template_expr(OpName,TemplateStringExpr),
845		visited_expression(NextId,State),
846		state_for_op(OpName,State,BState1),
847		visited_expression(StateId,BeforeState),
848		( no_before_state(OpName) -> BState=BState1
849		; state_for_op(OpName,BeforeState,BState0)
850		-> extract_variables_from_state_as_primed(BState0,PrimedBefore),
851		append(PrimedBefore,BState1,BState)
852		; add_warning(specfile,'Could not get initialised before state for: ',StateId),
853		BState = BState1
854		),
855		% TODO: use NextId and add StateId as $0 vars
856		% maplist(create_primed_binding,InVariablesState,PrimedVars),
857		% append(PrimedVars,Out,PredState),
858		!,
859		get_local_state_for_operation_transition(OpName,OpTerm,LocalState),
860		%write(local_state(OpName,OpTerm,LocalState)),nl,
861		% TODO: process errors better
862		if(b_compute_explicit_epression_no_wf(TemplateStringExpr,LocalState,BState,string(SD),
863		operation_description(OpName),0),
864		Desc=SD,
865		(get_operation_description(OpTerm,D), ajoin(['Error evaluating template: ',D],Desc))
866		).
867		get_operation_description_for_transition(_StateId,OpTerm,_NextStateId,Desc) :-
868		get_operation_description(OpTerm,Desc).
869
870		state_for_op('$setup_constants',State,BState) :- !,
871		state_corresponds_to_set_up_constants(State,BState).
872		state_for_op(_,State,BState) :-
873		state_corresponds_to_initialised_b_machine(State,BState).
874
875		no_before_state('$setup_constants').
876		no_before_state('$initialise_machine').
877
878		get_local_state_for_operation_transition(OpName,OperationTerm,LocalState) :-
879		get_local_states_for_operation_transition(OpName,OperationTerm,ParaStore,ResultStore),
880		append(ResultStore,ParaStore,LocalState).
881
882		% get local states for parameter values and result values extracted from a B operation transition term
883		get_local_states_for_operation_transition(OpName,OperationTerm,ParaStore,ResultStore) :- b_or_z_mode,!,
884		get_operation_return_values_and_arguments(OperationTerm,ReturnValues,ParaValues),
885	?	(b_get_machine_operation_for_animation(OpName,Results,Parameters,_Body,_OType,_TopLevel,OpPos)
886		-> true
887		; is_setup_constants_internal_name(OpName) -> Results=[], Parameters=[], OpPos=unknown
888		; add_error(specfile,'Unrecognized operation: ',OpName),
889		Results=[], Parameters=[], OpPos=unknown
890		),
891		def_get_texpr_ids(Parameters,OpParameterNames), % also includes virtual parameters (show_eventb_any_arguments)
892		(ParaValues=[]
893		-> ParaStore=[]
894		; (OpParameterNames=[], ParaValues=[_|_]
895		-> (get_preference(show_eventb_any_arguments,true)
896		-> add_message(specfile,'Ignoring additional parameters for:',OpName,OpPos)
897		; add_warning(specfile,'Ignoring additional parameters for:',OpName,OpPos)
898		),
899		ParaStore = []
900		; create_local_store_for_operation(OpParameterNames,ParaValues,OpName,ParaStore)
901		)
902		),
903		(ReturnValues=[]
904		-> ResultStore = []
905		; %b_get_machine_operation_result_names(OpName,OpResults),
906		def_get_texpr_ids(Results,OpResults),
907		create_local_store_for_operation(OpResults,ReturnValues,OpName,ResultStore)
908		).
909		get_local_states_for_operation_transition(OpName,OperationTerm,ParaStore,ResultStore) :- xtl_mode,
910		xtl_transition_parameters(OpName,ParaNames), !, % user-defined parameters found, otherwise use default params below
911		get_operation_return_values_and_arguments(OperationTerm,_ReturnValues,ParaValues), % ReturnValues should always be []
912		ResultStore = [],
913		maplist(gen_id_bind,ParaNames,ParaValues,ParaStore).
914		get_local_states_for_operation_transition(_OpName,OperationTerm,ParaStore,ResultStore) :- % not B mode or no user-defined params available in XTL mode
915		ResultStore = [],
916		get_operation_return_values_and_arguments(OperationTerm,ReturnValues,ParaValues),
917		ReturnValues = [], % should always succeed
918		gen_para_bind(ParaValues,1,ParaStore). % create [bind(para1,Val1),...]
919
920		gen_id_bind(ID,Val,bind(ID,Val)).
921
922		gen_para_bind([],_,[]).
923		gen_para_bind([H|T],Nr,[bind(ParaNr,H)|BT]) :- ajoin([para,Nr],ParaNr),
924		N1 is Nr+1,
925		gen_para_bind(T,N1,BT).
926
927		% create a store from parameter names and values:
928		create_local_store_for_operation([],[],_,Store) :- !, Store=[].
929		create_local_store_for_operation([Name|NT],[Val|VT],OpName,[bind(Name,Val)|StoreT]) :- !,
930		create_local_store_for_operation(NT,VT,OpName,StoreT).
931		create_local_store_for_operation([Name|NT],[],OpName,Store) :- !,
932		ajoin(['Missing values for operation ',OpName,':'],Msg),
933		add_error(specfile,Msg,[Name|NT]),
934		Store = [].
935		create_local_store_for_operation(_,V,OpName,Store) :-
936		ajoin(['Too many values for operation ',OpName,':'],Msg),
937		add_error(specfile,Msg,V),
938		Store = [].
939
940		:- use_module(library(between),[between/3]).
941
942		b_trans(State,OpName,Operation,NewState,PathInfo) :-
943	?	compute_operation_effect_max(State,OpName,Operation,NewState,PathInfo,_Max).
944
945		:- use_module(store,[store_updates_and_normalise/3]).
946
947		compute_operation_effect_max([],OpName,Operation,NewState,PathInfo,Max) :-
948	?	compute_operation_updates_on_expanded_store([],OpName,Operation,Updates,PathInfo,Max),
949		store_updates_and_normalise(Updates,[],NewState).
950		compute_operation_effect_max([H|T],OpName,Operation,NewState,PathInfo,Max) :-
951	?	compute_operation_updates_on_expanded_store([H|T],OpName,Operation,Updates,PathInfo,Max),
952		store_updates_and_normalise(Updates,[H|T],NewState).
953		compute_operation_effect_max(const_and_vars(ConstID,Vars),OpName,Operation,ResultingStore,PathInfo,Max) :-
954		prepare_state_for_specfile_trans(const_and_vars(ConstID,Vars),unknown,R),
955		%print(expanded_const_and_vars(ConstID)),nl,
956		compute_operation_effect_max(R,OpName,Operation,ResultingStore,PathInfo,Max).
957		compute_operation_effect_max(expanded_const_and_vars(ID,Vars,FullStore,Infos),OpName,Operation,NewState,PathInfo,Max) :-
958	?	compute_operation_updates_on_expanded_store(expanded_const_and_vars(ID,Vars,FullStore,Infos),
959		OpName,Operation,Updates,PathInfo,Max),
960		NewState = const_and_vars(ID,NewVars),
961		store_updates_and_normalise(Updates,Vars,NewVars).
962		compute_operation_effect_max(expanded_vars(FullStore,Infos),OpName,Operation,NewState,PathInfo,Max) :-
963	?	compute_operation_updates_on_expanded_store(expanded_vars(FullStore,Infos),
964		OpName,Operation,Updates,PathInfo,Max),
965		store_updates_and_normalise(Updates,FullStore,NewState).
966
967		compute_operation_effect_max(concrete_constants(ConstantsStore),'$initialise_machine',OpInit,ResultingStore,PathInfo,Max) :-
968		get_max_enablings_for_init(Max,'$initialise_machine',MaxForCall),
969	?	succeed_max_call_id('$initialise_machine',
970		b_interpreter:b_initialise_machine(ConstantsStore,InitialVars,InitialStore,PathInfo),MaxForCall),
971		create_initialisation_operation(InitialVars,OpInit),
972		(\+ preferences:preference(symmetry_mode,flood), /* TO DO : improve permutation to allow using const_and_vars optimisation */
973	?	visited_expression(ConstID,concrete_constants(ConstantsStore))
974		-> ResultingStore = const_and_vars(ConstID,InitialVars) /* avoid storing constant values again */
975		; ResultingStore = InitialStore).
976		compute_operation_effect_max(root,'$setup_constants',OpSetup,concrete_constants(FilteredConstantsStore),[],Max) :-
977		b_machine_has_constants_or_properties,
978		get_max_enablings_for_init(Max,'$setup_constants',MaxForCall),
979	?	compute_constants(ConstantsStore,MaxForCall,Complete),
980		create_setup_constants_operation(ConstantsStore,Complete,OpSetup),
981		%%print_message('FOUND_CONSTANTS'(OpName)),
982		(get_preference(filter_unused_constants,true) % possibly disable if VisB or Custom Graph Definitions exist
983		-> exclude(unused_binding,ConstantsStore,FilteredConstantsStore)
984		; FilteredConstantsStore=ConstantsStore).
985		compute_operation_effect_max(root,'$initialise_machine',OpInit,InitialStore,PathInfo,Max) :-
986		\+ b_machine_has_constants_or_properties,
987		get_max_enablings_for_init(Max,'$initialise_machine',MaxForCall),
988		empty_state(EmptyState),
989	?	succeed_max_call_id('$initialise_machine',
990		b_interpreter:b_initialise_machine(EmptyState,InitialVars,InitialStore,PathInfo),MaxForCall),
991		create_initialisation_operation(InitialVars,OpInit).
992
993
994		unused_binding(bind(C,_)) :- bmachine:b_is_unused_constant(C).
995
996		compute_constants(ConstantsStore,_Max,C) :-
997		% check if values have been computed and stored into a file before -- if yes, use them
998		load_constants(Stores,MaxReached),!,
999		C = complete_properties, % TODO: check that only complete properties stored or that we store this info
1000	?	choose_loaded_solution(Stores,ConstantsStore,MaxReached).
1001		compute_constants(ConstantsStore,Max,Complete) :-
1002		% print('Searching for valid CONSTANTS'),nl,!,
1003	?	succeed_max_call_id('$setup_constants',b_interpreter:b_set_up_concrete_constants(ConstantsStore,Complete),Max).
1004
1005		choose_loaded_solution(Stores,ConstantsStore,_MaxReached) :-
1006	?	member(ConstantsStore,Stores).
1007		choose_loaded_solution(_Stores,_ConstantsStore,true) :-
1008		% provoke the setting of the "maximum reached flag"
1009		succeed_max_call_id('$setup_constants',member(_,_),1),fail.
1010
1011		expand_const_and_vars_to_full_store(root,R) :- !,R=[].
1012		expand_const_and_vars_to_full_store(concrete_constants(ConstantsStore),FullStore) :- !,
1013		ConstantsStore = FullStore.
1014		expand_const_and_vars_to_full_store(const_and_vars(ConstID,Vars),FullStore) :- !,
1015		expand_const_and_vars(ConstID,Vars,FullStore).
1016		expand_const_and_vars_to_full_store(expanded_const_and_vars(_ConstID,_Vars,ExpStore,_),FullStore) :- !,
1017		FullStore = ExpStore.
1018		expand_const_and_vars_to_full_store(expanded_vars(ExpStore,_),FullStore) :- !,
1019		FullStore = ExpStore.
1020		expand_const_and_vars_to_full_store(csp_and_b(_,BState),FullStore) :- !,
1021		expand_const_and_vars_to_full_store(BState,FullStore).
1022		expand_const_and_vars_to_full_store(R,R).
1023
1024		expand_const_and_vars(ConstID,Vars,FullStore) :-
1025		visited_expression(ConstID,concrete_constants(ConstantsStore)),
1026		%% This can take a while if the Constants are big !
1027		% print('exp: '),tools_printing:print_term_summary(ConstantsStore),nl,
1028		append(Vars,ConstantsStore,FullStore). % used to be Constants first, now consistent with b_initialise_machine2,
1029		% b_initialise_machine2 puts constants at end to make sharing of complete tail-list easier for successor states
1030
1031		expand_to_constants_and_variables(root,[],[]).
1032		expand_to_constants_and_variables(concrete_constants(ConstStore),ConstStore,[]).
1033		expand_to_constants_and_variables(const_and_vars(ConstID,VarStore),ConstStore,VarStore) :-
1034		visited_expression(ConstID,concrete_constants(ConstStore)).
1035		expand_to_constants_and_variables([],[],[]).
1036		expand_to_constants_and_variables([H|T],[],[H|T]).
1037		expand_to_constants_and_variables(csp_and_b(_,BState),ConstStore,VarStore) :-
1038		expand_to_constants_and_variables(BState,ConstStore,VarStore).
1039
1040		:- use_module(extrasrc(b_operation_cache),[compute_operation_on_expanded_store_cache/6]).
1041
1042		% compute operation effect on a store where all constants have been put into the environment
1043		compute_operation_updates_on_expanded_store(InState,OpName,Operation,NewState,PathInfo,Max) :-
1044		get_preference(operation_reuse_setting,V), V \= false,
1045		b_or_z_mode, % now works with CSP || B
1046		%\+ animation_minor_mode(eventb), % projection used to confuse Event-B interpreter, see test 2138
1047		!,
1048		get_max_enablings_per_operation(Max,OpName,maxNrOfEnablingsPerOperation,MaxForCall),
1049	?	compute_operation_on_expanded_store_cache(OpName,Operation,InState,NewState,PathInfo,MaxForCall).
1050		compute_operation_updates_on_expanded_store(Store,OpName,Operation,Updates,PathInfo,Max) :-
1051		extract_full_store(Store,FullStore),!,
1052	?	compute_operation_on_expanded_store2(FullStore,OpName,Operation,Updates,PathInfo,Max).
1053		compute_operation_updates_on_expanded_store(InState,OpName,Operation,Updates,PathInfo,Max) :-
1054	?	compute_operation_on_expanded_store2(InState,OpName,Operation,Updates,PathInfo,Max).
1055
1056		compute_operation_on_expanded_store2(InState,OpName,Operation,Updates,PathInfo,Max) :-
1057		get_max_enablings_per_operation(Max,OpName,maxNrOfEnablingsPerOperation,MaxForCall),
1058	?	succeed_max_call_id(OpName,
1059		b_interpreter:b_execute_top_level_operation_update(OpName,Operation,InState,Updates,PathInfo),
1060		MaxForCall).
1061
1062		extract_full_store(expanded_const_and_vars(_,_,FS,_),Res) :- !, Res=FS.
1063		extract_full_store(expanded_vars(FS,_),Res) :- !, Res=FS.
1064
1065		create_initialisation_operation(_InitialVars,'$initialise_machine').
1066
1067		create_setup_constants_operation(_ConstantVars,complete_properties,R) :- !, R='$setup_constants'.
1068		create_setup_constants_operation(_ConstantVars,_,'$partial_setup_constants').
1069
1070		:- use_module(bmachine,[b_get_machine_operation_max/2]). % MAX_OPERATIONS_... DEFINITIONS
1071		get_max_enablings_per_operation_aux(OpName,RMax,_,RandomisedRestart) :-
1072		% TODO: decompose prefixed operation names with . write(get_mach_op_max(OpName)),nl,
1073		b_get_machine_operation_max(OpName,Max),
1074		!,
1075		(Max<0 -> RMax is -Max, RandomisedRestart=true ; RMax=Max, RandomisedRestart=false).
1076		get_max_enablings_per_operation_aux(_OpName,Max,DefaultPref,false) :-
1077		preferences:preference(DefaultPref,Max).
1078
1079		max_operations_zero_for_operation(OpName) :-
1080		b_or_z_mode,
1081		b_top_level_operation(OpName),
1082		(b_get_machine_operation_max(OpName,0) -> true
1083		; get_preference(maxNrOfEnablingsPerOperation,0)).
1084
1085		max_operations_zero_for_setup_constants :-
1086		b_or_z_mode,
1087		(b_get_machine_operation_max('$setup_constants',0) -> true
1088		; get_preference(maxNrOfInitialisations,0)).
1089		max_operations_zero_for_initialisation :-
1090		b_or_z_mode,
1091		(b_get_machine_operation_max('$initialise_machine',0) -> true
1092		; get_preference(maxNrOfInitialisations,0)).
1093
1094		get_max_enablings_per_operation(Max,OpName,DefaultPref,MaxForCall) :-
1095		(var(Max) -> get_max_enablings_per_operation_aux(OpName,Max,DefaultPref,RandomisedRestart)
1096		; RandomisedRestart=false),
1097		(RandomisedRestart=true,
1098		get_preference(randomise_enumeration_order,true)
1099		-> % we succeed Max times with the value 1, thus forcing a randomised restart
1100		MaxForCall=1, between(1,Max,Retry), format('Randomised Restart ~w for ~w~n',[Retry,OpName])
1101		; % we succeed once with the value Max
1102		MaxForCall is Max).
1103
1104		get_max_enablings_for_init(Max,OpName,MaxForCall) :-
1105		translate_operation_name(OpName,IOp),
1106		get_max_enablings_per_operation(Max,IOp,maxNrOfInitialisations,MaxForCall).
1107
1108		get_specific_max_operations_for_operation(OpName,MaxOp) :-
1109		b_or_z_mode,
1110		b_get_machine_operation_max(OpName,MaxOp).
1111
1112		:- use_module(bmachine,[b_get_machine_operation_time_out/2]).
1113		get_specific_time_out_for_operation(OpName,TimeOut) :-
1114		b_or_z_mode,
1115		b_get_machine_operation_time_out(OpName,TimeOut).
1116
1117		/* PROPERTIES */
1118
1119		property(const_and_vars(ConstID,Vars),Property) :- b_or_z_mode,
1120		expand_const_and_vars(ConstID,Vars,FullStore),!,
1121	?	property(FullStore,Property).
1122		property(csp_and_b(CSPState,BState),Property) :- animation_mode(csp_and_b),!,
1123		%% print(checking_csp_and_b(CSPState)),nl,
1124		expand_const_and_vars_to_full_store(BState,FBState),
1125		(xtl_interface:cspm_property(CSPState,Property) ;
1126		b_property(FBState,Property)).
1127		property(State,Property) :- animation_mode(AM),
1128	?	(AM = b -> b_property(State,Property)
1129	?	; AM=xtl -> xtl_interface:xtl_property(State,Property)
1130		; AM=cspm -> xtl_interface:cspm_property(State,Property)
1131		; AM=csp_and_b -> b_property(State,Property) % State should be root
1132		).
1133
1134		%b_property(const_and_vars(ConstID,Vars),Prop) :- !,
1135		% expand_const_and_vars(ConstID,Vars,FullStore),
1136		% b_property(FullStore,Prop).
1137	?	b_property(root,Prop) :- !, b_preference_par(PARA,Op,VAL), Prop=.. [Op,PARA,VAL].
1138		b_property([H|T],non_ground(Var)) :- debug:debug_mode(on),
1139		member(bind(Var,Val),[H|T]),\+(ground(Val)).
1140	?	b_property([H|T],Prop) :- elementary_prop([H|T],Prop).
1141		b_property([],Prop) :- elementary_prop([],Prop).
1142		b_property(concrete_constants(DB),Prop) :- elementary_prop(DB,Prop).
1143
1144
1145
1146		:- use_module(preferences).
1147		:- use_module(b_global_sets,[b_global_set/1, b_fd_card/2,inferred_minimum_global_set_cardinality/2,
1148		inferred_maximum_global_set_cardinality/2, unfixed_deferred_set/1]).
1149
1150		% preference values shown as properties of the root node
1151		b_preference_par('MAXINT','=',MaxInt) :- get_preference(maxint,MaxInt).
1152		b_preference_par('MININT','=',MinInt) :- get_preference(minint,MinInt).
1153		b_preference_par(card(GlobalSet),Op,Card) :-
1154		b_global_set(GlobalSet),
1155		b_fd_card(GlobalSet,RCard),
1156		% provide feedback if unfixed_deferred_set
1157		(inferred_maximum_global_set_cardinality(GlobalSet,MaxCard),
1158		(inferred_minimum_global_set_cardinality(GlobalSet,MinCard) -> true ; MinCard=1),
1159		MinCard \= MaxCard,
1160		Op = ':', Card = '..'(MinCard,MaxCard)
1161
1162		;
1163
1164		inferred_minimum_global_set_cardinality(GlobalSet,MinCard),
1165		\+ (inferred_maximum_global_set_cardinality(GlobalSet,_)),
1166		Op='>=',Card=MinCard % show minimum cardinality info
1167
1168		;
1169
1170		Op= '=', (unfixed_deferred_set(GlobalSet)
1171		-> ajoin([RCard,' (assumed for deferred set)'],Card) ; Card=RCard)
1172		).
1173
1174		/* --------------------------------------------------------- */
1175
1176
1177		elementary_prop(DB,Prop) :-
1178	?	member(bind(Var,Val),DB), %print(var_prop(Var)),nl_time,
1179	?	elementary_prop3(Val,Var,Prop).
1180
1181		:- use_module(custom_explicit_sets,[is_avl_relation/1,is_avl_partial_function/1,get_first_avl_elements/4, avl_approximate_size/3]).
1182		elementary_prop3(Val,Var,Prop) :- var(Val),!, Prop = '='(Var,'_VAR_').
1183		elementary_prop3(avl_set(Avl),Var,Prop) :- !,
1184		(show_avl_set(Avl) % \+ custom_explicit_sets:is_avl_sequence(Avl))
1185	?	-> elementary_fun_prop(avl_set(Avl),Var,Prop)
1186		; elementary_var_prop(avl_set(Avl),Var,Prop)).
1187		elementary_prop3([H|T],Var,Prop) :- H=(_,_),
1188		get_preference(show_function_tuples_in_property,true),!,
1189		elementary_fun_prop([H|T],Var,Prop).
1190		elementary_prop3(Val,Var,Prop) :- elementary_var_prop(Val,Var,Prop).
1191
1192		show_avl_set(AVL) :- get_preference(show_function_tuples_in_property,true),
1193		is_avl_relation(AVL),
1194		avl_approximate_size(AVL,0,Size), Size < 257, % only the first 30 will be shown by get_relation_element anyway
1195		is_avl_partial_function(AVL).
1196
1197
1198		:- use_module(bmachine,[b_is_variable/2]).
1199		elementary_var_prop(Val,Var,Prop) :-
1200		% TODO: use translate:translate_bvalue_for_expression/3
1201		animation_minor_mode(tla),!,
1202		( identifier_has_tla_type(Var,TlaType) ->
1203		translate_bvalue_with_tlatype(Val,TlaType,Text)
1204		;
1205		translate_bvalue(Val,Text)),
1206		Prop = '='(Var,Text).
1207		elementary_var_prop(Val,Var,Prop) :-
1208	?	(var_cst_type(Var,Type)
1209		-> translate_bvalue_with_type_and_limit(Val,Type,320,Text)
1210		; translate_bvalue_with_type_and_limit(Val,any,320,Text)), % translate_properties_with_limit uses 320 Limit
1211		Prop = '='(Var,Text).
1212
1213		identifier_has_tla_type(Id,Type) :-
1214		get_texpr_id(TId,Id),
1215		(b_get_machine_constants(Ids)
1216		;b_get_machine_variables(Ids)),
1217		member(TId,Ids),!,
1218		get_texpr_info(TId,Infos),
1219		memberchk(tla_type(Type),Infos).
1220		% to do: use b_is_variable + translate_bvalue_with_type
1221		elementary_fun_prop(Val,Var,Prop) :-
1222		simple(Prop), % will only succeed if Prop is var or atom; translate_bexpression will raise error if Prop is compound
1223		nonvar(Val),
1224	?	(var_cst_type(Var,Type),dom_range_type(Type,Dom,Ran) -> true ; Type=any,Dom=any, Ran=any),
1225	?	get_relation_element(Val,X,Y), % Show value in form: Var(X) = Y
1226		create_texpr(identifier(Var),Type,[],Fun),
1227		create_value(X,Dom,Arg),
1228		create_texpr(function(Fun,Arg),Ran,[],Lhs),
1229		create_value(Y,Ran,Rhs),
1230		create_texpr(equal(Lhs,Rhs),pred,[],Expr),
1231		translate_bexpression_with_limit(Expr,80,Prop).
1232
1233		var_cst_type(Name,Type) :- (b_is_variable(Name,Type) ; b_is_constant(Name,Type)).
1234		dom_range_type(seq(R),integer,R).
1235		dom_range_type(set(couple(D,R)),D,R).
1236
1237		get_relation_element(avl_set(A),X,Y) :- custom_explicit_sets:is_avl_relation(A),
1238		!, %preferences:preference(expand_avl_upto,Limit),
1239		Limit=30, % reduced limit, as now we can inspect with evaluation view
1240		get_first_avl_elements(A,Limit,Els,CutOff),
1241		(member((X,Y),Els), X\=term(_)
1242		;
1243		CutOff=not_all, X='...', Y='...').
1244		get_relation_element(Value,X,Y) :-
1245		member((X,Y),Value). /* otherwise we have a record structure */
1246
1247		create_value('...',_,R) :- !, R = b(string('...'),string,[]).
1248		create_value(X,T,R) :-
1249		create_texpr(value(X),T,[],R).
1250
1251
1252		:- use_module(bmachine,[b_show_machine_representation/4]).
1253		:- use_module(probcspsrc(haskell_csp_analyzer),[get_internal_csp_representation/1]).
1254		:- use_module(seqproversrc(sequent_prover_exports),[pretty_print_pos/1]).
1255		get_internal_representation(X) :- get_internal_representation(X,true,false,none).
1256		get_internal_representation(X,AdditionalInfo,UnsetMinorMode,Typing) :- animation_mode(AM),
1257		get_internal_aux(AM,X,AdditionalInfo,UnsetMinorMode,Typing).
1258		get_internal_aux(b,X,AdditionalInfo,UnsetMinorMode,Typing) :- !,
1259		b_show_machine_representation(X,AdditionalInfo,UnsetMinorMode,Typing).
1260		% UnsetMinorMode=true means we try and generate classical B syntax
1261		get_internal_aux(cspm,X,_,_,_) :- !, get_internal_csp_representation(X).
1262		get_internal_aux(csp_and_b,Res,AdditionalInfo,UnsetMinorMode,Typing) :- !,
1263		append("CSP||B - B Part only",X,Res),
1264		b_show_machine_representation(X,AdditionalInfo,UnsetMinorMode,Typing).
1265		get_internal_aux(xtl,Res,_,_,_) :- animation_minor_mode(sequent_prover), !,
1266		pretty_print_pos(Res).
1267		get_internal_aux(_,X,_,_,_) :- X="Internal representation only available in B or CSP mode".
1268
1269
1270		:- use_module(probcspsrc(haskell_csp),[channel/2]).
1271		:- use_module(bmachine,[b_top_level_operation/1, b_top_level_feasible_operation/1]).
1272		get_possible_event(OpName) :- b_or_z_mode,
1273		%b_is_operation_name(OpName).
1274	?	b_top_level_operation(OpName).
1275		get_possible_event(Channel) :- csp_mode,
1276	?	channel(Channel,_).
1277		% what about csp_and_b mode ?
1278
1279		get_feasible_event(OpName) :- b_or_z_mode,
1280		%b_is_operation_name(OpName).
1281	?	b_top_level_feasible_operation(OpName).
1282		get_feasible_event(Channel) :- csp_mode,
1283	?	channel(Channel,_).
1284
1285
1286		get_possible_language_specific_top_level_event(OpName,ResultNames,ParameterNames) :-
1287		b_or_z_mode,!,
1288		get_possible_b_top_level_event(OpName,ResultNames,ParameterNames).
1289		get_possible_language_specific_top_level_event(TransName,[],ParameterNames) :- xtl_mode, !,
1290		xtl_transition_parameters(TransName,ParameterNames).
1291		get_possible_language_specific_top_level_event(Channel,unknown,unknown) :- csp_mode,
1292		channel(Channel,_).
1293
1294		get_possible_b_top_level_event('$setup_constants',[],Ids) :-
1295		b_machine_has_constants_or_properties,
1296		b_get_machine_constants(TIds), maplist(get_texpr_id,TIds,Ids).
1297		get_possible_b_top_level_event('$initialise_machine',[],Ids) :-
1298		b_get_machine_variables(TIds), maplist(get_texpr_id,TIds,Ids).
1299		get_possible_b_top_level_event(OpName,ResultNames,ParameterNames) :-
1300		b_top_level_operation(OpName),
1301		%b_get_machine_operation(OpName,Results,RealParameters,_RealBody,_OType,_OpPos),
1302		b_get_machine_operation_for_animation(OpName,Results,AllParameters,_RealBody,_OType,_TL),
1303		maplist(get_texpr_id,Results,ResultNames),
1304		maplist(get_texpr_id,AllParameters,ParameterNames).
1305
1306		% obtain a textual description of specification category names
1307		get_specification_description(Category,Name) :-
1308		animation_mode(Mode),
1309		(animation_minor_mode(Minor) -> true ; Minor = none), % there could be several minor modes !
1310	?	(get_specific_description(Mode,Minor,Category,N) -> Name=N
1311		; get_default_description(Category,N) -> Name = N
1312		; add_error(get_specification_description,'Unknown category: ',Category),
1313		Name=Category).
1314
1315		get_specific_description(cspm,_,C,N) :- get_csp_description(C,N).
1316		get_specific_description(b,eventb,C,N) :- get_eventb_description(C,N).
1317		get_specific_description(b,tla,C,N) :- get_tla_description(C,N).
1318		get_specific_description(b,alloy,C,N) :- get_alloy_description(C,N).
1319
1320		get_csp_description(operations,'CHANNELS').
1321		get_csp_description(operation,'CHANNEL').
1322		get_csp_description(assertions,'CSP_ASSERTIONS').
1323		get_csp_description(machine,'CSP_SPECIFICATION').
1324		get_csp_description(operations_lc,'events').
1325
1326		get_tla_description(properties,'ASSUME').
1327		get_tla_description(machine,'MODULE').
1328		get_tla_description(operation,'ACTION'). % no key word
1329		get_tla_description(operations,'ACTIONS'). % no key word
1330		get_tla_description(operations_lc,'actions').
1331
1332		get_eventb_description(properties,'AXIOMS').
1333		get_eventb_description(assertions,'THEOREMS').
1334		get_eventb_description(operations,'EVENTS').
1335		get_eventb_description(operation,'EVENT').
1336		get_eventb_description(operations_lc,'events').
1337		get_eventb_description(machine,'MODEL').
1338
1339		get_alloy_description(machine,'MODULE').
1340		get_alloy_description(sets,'SIGNATURES'). % abstract
1341		get_alloy_description(operations,'RUNS').
1342		get_alloy_description(operation,'RUN').
1343
1344		get_default_description(constraints,'CONSTRAINTS').
1345		get_default_description(properties,'PROPERTIES').
1346		get_default_description(assertions,'ASSERTIONS').
1347		get_default_description(invariant,'INVARIANT').
1348		get_default_description(invariants,'INVARIANTS').
1349		get_default_description(operations,'OPERATIONS').
1350		get_default_description(operation,'OPERATION').
1351		get_default_description(operations_lc,'operations').
1352		get_default_description(machine,'MACHINE').
1353		get_default_description(constants,'CONSTANTS').
1354		get_default_description(variables,'VARIABLES').
1355		get_default_description(initialisation,'INITIALISATION').
1356		get_default_description(sets,'SETS').
1357		get_default_description(goal,'GOAL').
1358		get_default_description(definition,'DEFINITION').
1359		get_default_description(definitions,'DEFINITIONS').
1360		get_default_description(variants,'VARIANTS').