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(specfile, [
6		specfile_possible_trans_name/2, specfile_possible_trans_name_for_successors/2,
7		specfile_trans/6,
8		prepare_state_for_specfile_trans/2, prepare_state_for_specfile_trans/3,
9
10		property/2, elementary_prop/2,
11
12		partial_trans/4, specfile_trans_or_partial_trans/6,
13
14		animation_mode/1, set_animation_mode/1, add_animation_minor_mode/1,
15		animation_minor_mode/1, set_animation_minor_mode/1, remove_animation_minor_mode/0,
16		unset_animation_minor_modes/1, reset_animation_minor_modes/1,
17		b_mode/0, z_mode/0, b_or_z_mode/0, b_or_z_mode/1, eventb_mode/0,
18		csp_mode/0, csp_mode/1,
19		csp_with_bz_mode/0, z_or_tla_minor_mode/0,
20		process_algebra_mode/0,
21
22		type_check_csp_and_b/0,
23
24		currently_opened_file/1, % only true for successfully opened files
25		currently_opened_file_status/2, % second parameter: success or failure
26		reset_currently_opened_file/0,set_currently_opened_file/1, set_failed_to_open_file/1,
27		set_currently_opened_package/1,
28		spec_file_has_been_successfully_loaded/0,
29
30		state_corresponds_to_initialised_b_machine/1, state_corresponds_to_initialised_b_machine/2,
31		state_corresponds_to_fully_setup_b_machine/1, state_corresponds_to_fully_setup_b_machine/2,
32		state_corresponds_to_set_up_constants/1, state_corresponds_to_set_up_constants/2, state_corresponds_to_set_up_constants_only/2,
33		current_b_expression/1,
34
35		get_operation_name/2, get_operation_internal_name/2,
36		translate_operation_name/2,
37		get_operation_arguments/2, get_operation_return_values_and_arguments/3,
38		build_up_b_real_operation/2,
39		expand_const_and_vars/3, expand_const_and_vars_to_full_store/2,
40		expand_to_constants_and_variables/3,
41
42		compute_operation_effect_max/6, % has replaced compute_operation_effect/5
43		create_setup_constants_operation/2,
44		get_internal_representation/1, get_internal_representation/2,
45		get_possible_event/1, get_possible_language_specific_top_level_event/3,
46		get_specification_description/2
47		]).
48
49		:- use_module(tools).
50
51		:- use_module(module_information).
52		:- module_info(group,animator).
53		:- module_info(description,'This module computes transitions and properties depending on the current animator mode.').
54
55		:- use_module(library(lists)).
56		%:- use_module(library(avl)).
57		%:- use_module(library(clpfd)).
58
59		:- use_module(debug).
60		:- use_module(b_interpreter).
61		:- use_module(preferences).
62		:- use_module(self_check).
63		:- use_module(error_manager).
64		:- use_module(translate).
65		:- use_module(succeed_max,[succeed_max_call_id/3]).
66
67		:- use_module(store,[empty_state/1]).
68		:- use_module(bmachine).
69		:- use_module(bsyntaxtree).
70
71
72		%% :- use_module(delay).
73
74		:- use_module(value_persistance, [load_constants/2]).
75
76		/* --------------------------------- */
77
78
79
80
81		/* --------------------------------- */
82		/* ANIMATION & TEMPORAL VERIFICATION */
83		/* --------------------------------- */
84
85
86		:- dynamic animation_mode/1, animation_minor_mode/1.
87		% not marking as volatile; otherwise we startup with no animation_mode set
88		% not all parts of ProB can deal with this at the moment
89		%:- volatile animation_mode/1, animation_minor_mode/1.
90
91		animation_mode(b).
92		/* possible values: b, csp, xtl, z, csp_and_b, promela */
93
94	?	b_mode :- animation_mode(X), (X=b ; X=csp_and_b).
95		z_mode :- animation_mode(X), (X=b ; X=csp_and_b), animation_minor_mode(z).
96		eventb_mode :- animation_mode(X), (X=b ; X=csp_and_b), animation_minor_mode(eventb).
97		csp_with_bz_mode :- animation_mode(csp_and_b).
98		z_or_tla_minor_mode :- animation_minor_mode(X), (X=tla ; X=z).
99
100		csp_mode :- animation_mode(X), csp_mode(X).
101		csp_mode(cspm).
102		csp_mode(csp_and_b).
103
104		b_or_z_mode :-
105		(animation_mode(X) -> (X=b -> true ; X=csp_and_b)). % basically the same as b_mode
106		b_or_z_mode(b). b_or_z_mode(csp_and_b).
107
108		process_algebra_mode :-
109		(animation_mode(X) -> \+ X=b, \+X=z).
110
111		set_animation_mode(X) :-
112		retractall(animation_mode(_)),
113		remove_animation_minor_mode,
114		assert(animation_mode(X)).
115
116		set_animation_minor_mode(X) :-
117		remove_animation_minor_mode,
118		assert(animation_minor_mode(X)).
119		remove_animation_minor_mode :-
120		retractall(animation_minor_mode(_)).
121
122		% use to temporarily unset animation minor mode:
123		:- use_module(library(lists),[maplist/2]).
124		unset_animation_minor_modes(L) :- findall(X,retract(animation_minor_mode(X)),L).
125		reset_animation_minor_modes(L) :- maplist(add_animation_minor_mode,L).
126
127		add_animation_minor_mode(X) :-
128		(animation_minor_mode(X) -> true ; assert(animation_minor_mode(X))).
129
130
131		:- dynamic currently_opened_file_status/2.
132		:- volatile currently_opened_file_status/2.
133		%currently_opened_file(none).
134
135		reset_currently_opened_file :- retractall(currently_opened_file_status(_,_)).
136		:- use_module(eventhandling,[register_event_listener/3]).
137		:- register_event_listener(clear_specification,reset_currently_opened_file,
138		'Reset Specfile Currently Opened File.').
139
140		% call if a spec was not loaded from file but from package (e.g., via socket / prob2)
141		set_currently_opened_package(Type) :-
142		set_currently_opened_file(package(Type)).
143
144		set_currently_opened_file(File) :-
145		reset_currently_opened_file,
146		assert(currently_opened_file_status(File,success)).
147
148		set_failed_to_open_file(File) :-
149		reset_currently_opened_file,
150		assert(currently_opened_file_status(File,failure)).
151
152		currently_opened_file(File) :- currently_opened_file_status(File,success).
153
154		spec_file_has_been_successfully_loaded :- currently_opened_file(_).
155
156		:- use_module(bmachine,[b_machine_has_variables/0]).
157		% true if state corresponds to an initialised B machine
158		state_corresponds_to_initialised_b_machine(const_and_vars(_,_)) :- !,
159		b_or_z_mode.
160		state_corresponds_to_initialised_b_machine([]).
161		state_corresponds_to_initialised_b_machine([_|_]).
162		state_corresponds_to_initialised_b_machine(csp_and_b(_,BState)) :-
163		csp_with_bz_mode,
164		state_corresponds_to_initialised_b_machine(BState).
165
166
167		% check if state corresponds to an initialised B machine, and if so return expanded State
168		state_corresponds_to_initialised_b_machine(const_and_vars(ConstID,Vars),State) :- !,
169		b_or_z_mode, expand_const_and_vars(ConstID,Vars,State).
170		state_corresponds_to_initialised_b_machine(expanded_const_and_vars(_ConstID,_Vars,FullStore),State) :- !,
171		% generated by prepare_state_for_specfile_trans
172		State=FullStore.
173		state_corresponds_to_initialised_b_machine([],[]).
174		state_corresponds_to_initialised_b_machine([H|T],[H|T]).
175		state_corresponds_to_initialised_b_machine(csp_and_b(_,BState),State) :-
176		csp_with_bz_mode,
177		state_corresponds_to_initialised_b_machine(BState,State).
178
179		% check if all variables, constants setup; also allows concrete_constants if no variables exist
180		state_corresponds_to_fully_setup_b_machine(concrete_constants(_)) :- !, b_or_z_mode,
181		\+ b_machine_has_variables.
182		state_corresponds_to_fully_setup_b_machine(X) :- state_corresponds_to_initialised_b_machine(X).
183
184		state_corresponds_to_fully_setup_b_machine(concrete_constants(Constants),State) :- !, b_or_z_mode,
185		\+ b_machine_has_variables, State=Constants.
186		state_corresponds_to_fully_setup_b_machine(X,State) :- state_corresponds_to_initialised_b_machine(X,State).
187
188		% check if we only have constants, no variable values yet
189		state_corresponds_to_set_up_constants_only(root,State) :- !, animation_mode(b),
190		\+ b_machine_has_constants_or_properties, State=[]. % relevant for test 960
191		state_corresponds_to_set_up_constants_only(concrete_constants(Constants),State) :- !,
192		b_or_z_mode, State=Constants.
193		state_corresponds_to_set_up_constants_only(csp_and_b(_,BState),State) :- !,
194		csp_with_bz_mode,
195		state_corresponds_to_set_up_constants_only(BState,State).
196
197		state_corresponds_to_set_up_constants(const_and_vars(_,_)) :- !. % avoid expansion
198		state_corresponds_to_set_up_constants(X) :- state_corresponds_to_set_up_constants(X,_).
199
200		state_corresponds_to_set_up_constants(const_and_vars(ConstID,Vars),State) :- !,
201		b_or_z_mode, expand_const_and_vars(ConstID,Vars,State).
202		state_corresponds_to_set_up_constants(expanded_const_and_vars(_ConstID,_Vars,FullStore),State) :- !,
203		% generated by prepare_state_for_specfile_trans
204		State=FullStore.
205		state_corresponds_to_set_up_constants(concrete_constants(Constants),State) :- !,
206		b_or_z_mode, State=Constants.
207		state_corresponds_to_set_up_constants(csp_and_b(_,BState),State) :- !,
208		csp_with_bz_mode,
209		state_corresponds_to_set_up_constants(BState,State).
210		state_corresponds_to_set_up_constants([],State) :- !, State=[],
211		animation_mode(b).
212		state_corresponds_to_set_up_constants(State,RState) :-
213		animation_mode(b),
214		(State = root -> \+ b_machine_has_constants_or_properties,RState=[] ; RState=State).
215
216		:- use_module(state_space,[current_expression/2]).
217		current_b_expression(CurBState) :-
218		current_expression(_CurID,CurState),
219		state_corresponds_to_set_up_constants(CurState,CurBState).
220
221		/* TRANSITIONS */
222
223		:- use_module(xtl_interface).
224		:- use_module(tools_meta,[call_residue/2]).
225		% ---------------------------------------------------
226
227
228		% Tries to find successor state for Op in State DB. Fails, if no solution is possible
229		% Input: State DB, Operation Op
230		% Output: DB2 the sucessor state
231		% Residue: Unfinished co-routines (should not happen!)
232		%specfile_trans(DB,Op,DB2,[]) :- !, specfile:i_transition(DB,Op,DB2).
233		specfile_trans(DB,OpName,Op,DB2,TransInfo,Residue) :-
234		% i_transition(DB,OpName,Op,DB2,TransInfo), Residue = []. % is faster, but no residue checking
235	?	animation_mode(MODE),
236	?	call_residue(i_transition(MODE,DB,OpName,Op,DB2,TransInfo),Residue).
237
238	?	i_transition(b,State,OpName,Op,NewState,TransInfo) :- !,
239	?	b_trans(State,OpName,Op,NewState,TransInfo).
240		i_transition(xtl,State,OpName,Op,NewState,[]) :- !,
241		xtl_transition(State,Op,NewState), functor(Op,OpName,_).
242		i_transition(cspm,State,_OpName,Op,NewState,[]) :- !,
243		% Note: the OpName is ignored: we cannot make use of it
244		cspm_transition(State,Op,NewState).
245		%i_transition(promela,State,_OpName,Op,NewState,[]) :- !,
246		% promela_transition(State,Op,NewState).
247		% ; MODE=smv -> smv_transition(State,Op,NewState),TransInfo=[]
248		i_transition(csp_and_b,State,OpName,Op,NewState,TransInfo) :- !, %% print(cspB(OpName,Op,State)),nl, %trace,
249		% Note: the OpName is either the name of a B operation or '$CSP' (or a variable)
250		csp_and_b_transition(State,OpName,Op,NewState,TransInfo).
251
252
253		% if you call specfile_trans multiple times for the same state, it is
254		% more efficient to call this predicate first once
255		prepare_state_for_specfile_trans(const_and_vars(ConstID,Vars),R) :- !, %print(expanding_const(ConstID)),nl,
256		R = expanded_const_and_vars(ConstID,Vars,FullStore),
257		expand_const_and_vars(ConstID,Vars,FullStore). %, print(full(FullStore)),nl.
258		% TO DO: also expand for csp_and_b
259		prepare_state_for_specfile_trans(X,X).
260
261		% a version with a memo argument to store expanded constants
262		prepare_state_for_specfile_trans(const_and_vars(ConstID,Vars),MEMO,R) :- !, %print(expanding_const(ConstID)),nl,
263		R = expanded_const_and_vars(ConstID,Vars,FullStore),
264		(nonvar(MEMO),MEMO = [ConstID/ConstantsStore]
265		-> %tools_printing:print_term_summary(memo(ConstID,ConstantsStore)),nl,
266		append(ConstantsStore,Vars,FullStore) % simply reuse expanded constants in MEMO
267		; % expand_const_and_vars inlined (so as to obtain ConstantsStore
268		state_space:visited_expression(ConstID,concrete_constants(ConstantsStore)), %% This can take a while if the Constants are big !
269		% print(no_memo(ConstID,MEMO)),tools_printing:print_term_summary(ConstantsStore),nl,
270		append(ConstantsStore,Vars,FullStore),
271		(var(MEMO) -> MEMO=[ConstID/ConstantsStore] ; true)
272		). %, print(full(FullStore)),nl.
273		% TO DO: also expand for csp_and_b
274		prepare_state_for_specfile_trans(X,_,X).
275
276
277		/* can be attempted if trans fails to attempt to use partially computed transitions */
278		partial_trans(DB,Op,DB2,Residue) :-
279		call_residue(partial_i_transition(DB,Op,DB2),Residue).
280
281		partial_i_transition(root,'$partial_setup_constants',concrete_constants(ConstantsStore)) :-
282		animation_mode(b),
283		set_error_context(operation('$partial_setup_constants',root)),
284		b_interpreter:b_partial_set_up_concrete_constants(ConstantsStore).
285
286		% a predicate which automatically calls partial_trans :
287		specfile_trans_or_partial_trans(DB,OpName,Op,DB2,TransInfo,Residue) :-
288		if(specfile_trans(DB,OpName,Op,DB2,TransInfo,Residue),true,
289		(OpName='$setup_constants', TransInfo=[],
290		partial_trans(DB,Op,DB2,Residue))).
291
292		/* build up skeletons of possible operations; to be used before time_out call is made */
293		specfile_possible_trans_name(State,OpName) :- animation_mode(MODE),
294		(MODE=b -> b_possible_trans_name(State,OpName)
295		; MODE = csp_and_b -> csp_b_possible_trans_name(State,OpName)
296		; setup_transition_skeleton(MODE,OpName) /* TO DO: add more possible skeletons */
297		).
298
299		% only set up skeletons if it is worth it for computing all successors
300		% 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)
301	?	specfile_possible_trans_name_for_successors(State,OpName) :- animation_mode(MODE),
302	?	(MODE=b -> b_possible_trans_name(State,OpName)
303		; setup_transition_skeleton(MODE,OpName)
304		).
305
306		setup_transition_skeleton(_,_). /* TO DO: add more possible skeletons ? */
307
308		:- use_module(library(random)).
309		b_possible_trans_name(root,OpName) :- !,
310		(b_machine_has_constants_or_properties
311		-> OpName = '$setup_constants'
312		; OpName = '$initialise_machine').
313		b_possible_trans_name(concrete_constants(_),OpName) :- !, OpName = '$initialise_machine'.
314		b_possible_trans_name(_State,OpName) :-
315	?	(preferences:preference(randomise_operation_order,true),random(1,3,1)
316		-> b_machine_operation_names_in_reverse_order(OpName) ; true),
317		%b_get_machine_operation(OpName,_Res,_Params,_,_,_).
318	?	b_top_level_operation(OpName).
319		% we could check: b_operation_cannot_modify_state(OpName) given a preference
320
321		csp_b_possible_trans_name(csp_and_b_root,OpName) :- !,
322		(b_machine_has_constants_or_properties
323		-> OpName = 'tau($setup_constants)'
324		; OpName = 'tau($initialise_machine)').
325		csp_b_possible_trans_name(concrete_constants(_),OpName) :- !,
326		OpName = 'tau($initialise_machine)'.
327		csp_b_possible_trans_name(State,OpName) :-
328		b_possible_trans_name(State,OpName).
329		% TO DO: add non-synchronised channels
330
331		% --------------
332
333		:- use_module(probcspsrc(haskell_csp),[channel_type_list/2]).
334		:- use_module(debug).
335		% check whether a currently open CSP is type compatible with a loaded B machine
336		type_check_csp_and_b :- animation_mode(csp_and_b), debug_println(9,type_check_csp_and_b),
337		b_get_machine_operation(ChannelOpName,Res,Params,_,_,_), append(Params,Res,ParamsRes),
338		channel_type_list(ChannelOpName,CSPTypeList),
339		% TO DO: also check B variable names which match channel name
340		debug_println(9,checking_synchronised_channel(ChannelOpName,ParamsRes,CSPTypeList)),
341		l_check_compatibility(ParamsRes,CSPTypeList,ChannelOpName),
342		fail.
343		type_check_csp_and_b.
344
345		%convert_csp_type_to_list(type(T),R) :- convert_csp_type_to_list2(T,R).
346		%convert_csp_type_to_list2(dotUnitType,[]).
347		%convert_csp_type_to_list2(dotTupleType(T),T).
348
349		l_check_compatibility([],[],_) :- !.
350		l_check_compatibility([B|BT],[CSP|CSPT],ChannelOpName) :- !, check_compatibility(B,CSP,ChannelOpName),
351		l_check_compatibility(BT,CSPT,ChannelOpName).
352		l_check_compatibility([],CSP,ChannelOpName) :- !,
353		add_error(type_check_csp_and_b,'CSP Channel has too many parameters: ', ChannelOpName:CSP).
354		l_check_compatibility(B,[],ChannelOpName) :- !,
355		print('* CSP Channel has too few parameters: '), print(ChannelOpName),nl,
356		print('* B Arguments will be ignored: '), l_print_bexpr_or_subst(B),nl.
357		%add_error(type_check_csp_and_b,'CSP Channel has too few parameters: ', ChannelOpName:B).
358
359		check_compatibility(b(identifier(ID),TYPE,INFO),CSP_TYPE,ChannelOpName) :- !,
360		(type_ok(TYPE,CSP_TYPE) -> true ;
361		% TO DO: pretty print B and CSP Types
362		add_error(type_check_csp_and_b,'Incompatible types between B and CSP: ',ChannelOpName:ID:(TYPE:CSP_TYPE),b(identifier(ID),TYPE,INFO))
363		).
364		check_compatibility(B,CSP,ChannelOpName) :- !,
365		add_internal_error('Illegal types: ',check_compatibility(B,CSP,ChannelOpName)).
366
367		% TO DO: needs to be refined much more;
368		type_ok(Type,CSPType) :-
369		(type_ok2(Type,CSPType) -> true
370		; add_error(type_check_csp_and_b,'Cannot be converted (B:CSP): ',Type:CSPType),fail).
371		type_ok2(boolean,X) :- !, is_csp_boolean_type(X).
372		type_ok2(integer,X) :- !, is_csp_integer_type(X).
373		type_ok2(string,CSP) :- !,is_csp_global_set_type(CSP,string).
374		type_ok2(set(T),CSP) :- !, is_csp_set_type(CSP,T).
375		% TO DO: what if we have set(couple(integer,T)) instead of seq(T) ?
376		% rye
377		% check set(couple(integer,T)) (seq type) in B
378		type_ok2(seq(T),CSP) :- !, is_csp_seq_type(CSP,T).
379		type_ok2(couple(A,B),CSP) :- !, is_csp_couple_type(CSP,A,B).
380		type_ok2(global(GS),CSP) :- !,is_csp_global_set_type(CSP,GS).
381		type_ok2(X,Y) :- print(unkown(X,Y)),nl.
382
383		is_csp_couple_type(setValue([na_tuple([A|Rest])|_]),TA,TB) :- type_ok(TA,setValue([A])),
384		check_rest_couple_els(Rest,TB).
385		is_csp_couple_type(typeTuple([A|Rest]),TA,TB) :- type_ok(TA,A), check_rest_couple(Rest,TB).
386
387		check_rest_couple_els([B],TB) :- !, type_ok(TB,setValue([B])).
388		check_rest_couple_els([B1|BRest],couple(TB1,TBRest)) :- type_ok(TB1,setValue([B1])),
389		check_rest_couple_els(BRest,TBRest).
390		check_rest_couple([B],TB) :- !, type_ok(TB,B).
391		check_rest_couple([B1|BRest],couple(TB1,TBRest)) :- type_ok(TB1,B1),
392		check_rest_couple(BRest,TBRest).
393
394		% rye
395		% check if it is couple(integer, T) type and return T in 2nd arguments
396		couple_int(couple(integer, T), T). % possible sequence
397
398		% rye: it's not correct to check only Head
399		% % for example, for CSP type, {{}, {(1,2),(2,3)}}. Its head is emptyset, but the second one is set of tuple
400		is_csp_set_type('Set'([H|_]),Type) :- type_ok(Type,H). % just check Head
401		% check the 2nd element in set in case the 1st is emptyset
402		is_csp_set_type(setValue([_|T]),Type) :-
403		T = [H1 | _], !,
404		% if it is set(couple(integer, T)), it can be a sequence type
405		(couple_int(Type, TH1) -> is_csp_seq_type(setValue(T), TH1)
406		; type_ok(Type,H1)
407		). % check the 2nd
408		% if it is only one element in set, just check the head
409		is_csp_set_type(setValue([H|T]),Type) :-
410		(couple_int(Type, TH1) -> is_csp_seq_type(setValue([H|T]), TH1)
411		; type_ok(Type,H)
412		). % just check Head
413
414		is_csp_seq_type('Seq'(H),Type) :- type_ok(Type,H).
415		is_csp_seq_type(setValue([H|_]),Type) :- H=list(L), is_csp_list(L,Type).
416		is_csp_list([],_).
417		is_csp_list([H|_],Type) :- type_ok(Type,setValue([H])).
418
419		is_csp_boolean_type(boolType).
420		is_csp_boolean_type(setValue([H|_])) :- is_csp_boolean_value(H).
421		is_csp_boolean_value(true).
422		is_csp_boolean_value(false).
423
424		is_csp_integer_type(intType).
425		is_csp_integer_type(setFromTo(_,_)).
426		is_csp_integer_type(setFrom(_)).
427		is_csp_integer_type(setValue([int(_)|_])).
428
429		is_csp_global_set_type(dataType(_),_GS). % TO DO CHECK MEMBERS
430		is_csp_global_set_type(setValue([]),_GS). % TO DO CHECK MEMBERS
431		is_csp_global_set_type(setValue([_|_]),_GS). % TO DO CHECK MEMBERS
432
433		% --------------
434
435
436		:- use_module(bmachine,[b_get_machine_operation/4]).
437		:- use_module(bsets_clp,[tuple_of/3]).
438		% compute transitions for a CSP || B specification
439		% Note: the OpName is either the name of a B machine operation (even if hidden) or '$CSP' (useful for ltsmin)
440		csp_and_b_transition(root,OpName,Op,NewState,TransInfo) :- !,
441		Op = start_cspm_MAIN, OpName=Op, NewState = csp_and_b_root,TransInfo = [].
442		csp_and_b_transition(csp_and_b_root,OpName,Trans,NewState,TransInfo) :- !,
443		Trans = tau(Op), OpName = '$CSP',
444		b_trans(root,_,Op,InitialBState,TransInfo),
445		(InitialBState = concrete_constants(_)
446		-> NewState = InitialBState
447		; csp_initialisation_for_b(InitialCSPState),
448		NewState = csp_and_b(InitialCSPState,InitialBState)
449		).
450		csp_and_b_transition(concrete_constants(C),OpName,Trans,NewState,TransInfo) :- !,
451		Trans = tau(Op), OpName = '$CSP',
452		b_trans(concrete_constants(C),_,Op,InitialBState,TransInfo),
453		csp_initialisation_for_b(InitialCSPState),
454		NewState = csp_and_b(InitialCSPState,InitialBState).
455		csp_and_b_transition(csp_and_b(CSPState,BState),OpName,EventVisibleToUser,csp_and_b(NewCSP,NewB),TransInfo) :-
456		!,
457		csp_transition_for_b(CSPState,ChOpName,ChArgs,CSPAction,NewCSP),
458		% TO DO: split up csp_transition_for_b: into two parts; second part converts datatypes and only called if linking op exists
459		%% print(csp_trans(ChOpName,ChArgs)),nl, %%
460		length(ChArgs,Len), length(OpArgs,Len),
461		b_transition_for_csp(ChOpName,CSPAction,ChArgs,OpArgs,BState,OpName,Operation,NewB,TransInfo),
462		hide_csp_event(CSPAction,Operation,EventVisibleToUser).
463		csp_and_b_transition(State,'$CSP',Op,NewState,[]) :-
464		% we have a pure CSP state: use CSP-M transition
465		cspm_transition(State,Op,NewState).
466
467		:- use_module(bmachine,[b_is_variable/1,b_is_constant/1]).
468		% compute the B counterpart for a CSP transition:
469		b_transition_for_csp(ChOpName,_CSPAction,ChArgs,OpArgs,BState,OpName,Operation,NewB,TransInfo) :-
470		build_up_b_operation_for_csp(ChOpName,OpArgs,Operation),
471		!,
472		OpName = ChOpName,
473		%% print_message(trying_b_trans(Operation,ChArgs,OpArgs)), %%
474		generate_b_operationargs_from_csp(ChArgs,OpArgs),
475		%% print(trying_b_trans(Operation)),nl, %%
476		b_trans(BState,_,Operation,NewB,TransInfo).
477		%%, print_message(csp_btrans(Operation)), %%.
478		b_transition_for_csp(ChOpName,_CSPAction,ChArgs,OpArgs,BState,OpName,Operation,NewB,TransInfo) :-
479		OpName = ChOpName,
480		(b_is_variable(ChOpName) ; b_is_constant(ChOpName)),
481		%% print(probing(ChOpName)),nl,
482		expand_const_and_vars_to_full_store(BState,FBState),
483		try_lookup_value_in_store_and_global_sets(ChOpName,FBState,IdValue),
484		!,
485		NewB=BState,TransInfo=[],
486		/* interpret as probing operation: get value of var,cst,SET */
487		generate_b_operationargs_from_csp(ChArgs,OpArgs),
488		(OpArgs=[SingleVal]
489		-> SingleVal = IdValue, Operation='-->'(ChOpName,[IdValue])
490		; OpArgs=[Val1,Val2],
491		tuple_of(Val1,Val2,IdValue), /* from bsets_clp, use exact_element_of ??? */
492		OpCall =.. [ChOpName,Val1],
493		Operation='-->'(OpCall,[Val2])
494		).
495		b_transition_for_csp(_ChOpName,CSPAction,_ChArgs,_OpArgs,BState,OpName,Operation,NewB,TransInfo) :-
496		OpName = '$CSP', % all CSP events grouped together
497		NewB=BState,TransInfo=[],
498		/* no B operation of the name; could be tau or tick or extra comm channel */
499		%Op1 =.. [ChOpName|OpArgs],
500		Operation = CSPAction. % removed csp(.) wrapper [for LTL model checker]
501
502		hide_csp_event(CSPAction,_,EventVisibleToUser) :-
503		haskell_csp:symbol('HIDE_CSPB',_,Span,_),!, % if there is a HIDE_CSPB definition then we do MAIN [{| HIDE_CSPB |}] B_MACHINE \ {| HIDE_CSPB |}
504		haskell_csp:evaluate_argument(val_of('HIDE_CSPB',Span),EvCList),
505		% print(hide(EvCList,CSPAction)),nl,
506		~~mnf(haskell_csp:expand_channel_pattern_expression(EvCList,ECList,no_loc_info_available)),
507		haskell_csp:cspm_hide_action(CSPAction,omega,ECList, Span, EventVisibleToUser,_).
508		hide_csp_event(_CSPAction,Operation,EventVisibleToUser) :-
509		% get_preference(csp_event_visible_to_user,true) -> EventVisibleToUser = CSPAction
510		EventVisibleToUser = Operation.
511
512		build_up_b_operation_for_csp(OpName,OpArgs,Operation) :- %print(csp(OpName,OpArgs,Operation)),nl,
513		nonvar(OpName),
514		b_get_machine_operation(OpName,Res,Params,_), %print(get_machine_op(OpName,Res,Params)),nl,
515		specfile:generate_args(OpArgs,Params,Res, BArgs,BResults,OpName), %print(gen_args(BArgs,BResults)),nl,
516		% 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
517		safe_univ(Op1,[OpName|BArgs]), %print(op1(Op1)),nl,
518		(BResults = [] -> Operation = Op1 ; Operation =.. ['-->',Op1,BResults]).
519
520		build_up_b_real_operation(OpName,Operation) :-
521		b_get_machine_operation_for_animation(OpName,Res,Params,_,_,true), %true==TopLevel
522		length(Params,Len), length(OpArgs,Len),
523		length(Res,RLen), length(BResults,RLen),
524		safe_univ(Op1,[OpName|OpArgs]),
525		(BResults = [] -> Operation = Op1 ; Operation =.. ['-->',Op1,BResults]).
526
527		generate_args([],[],Res,[],BRes,_) :- length(Res,L), length(BRes,L).
528		generate_args([],[_Param|T],Res,[_|TA],BRes,OpName) :-
529		generate_args([],T,Res,TA,BRes,OpName).
530		generate_args([CSPArg|TC],[Param|T],Res,[CSPArg|TA],BRes,OpName) :- check_type_for_id(CSPArg,Param,OpName),
531		generate_args(TC,T,Res,TA,BRes,OpName).
532		generate_args([CSPArg|TC],[],[ReturnParam|TRes],[],[CSPArg|TBRes],OpName) :-
533		check_type_for_id(CSPArg,ReturnParam,OpName),
534		generate_args(TC,[],TRes,[],TBRes,OpName).
535		generate_args([H|T],[],[],[],[],OpName) :-
536		add_error(specfile,'CSP provides extra arguments: ',OpName:[H|T]).
537
538		check_type_for_id(Val,TID,OpName) :- get_texpr_type(TID,Type),
539		check_type(Type,Val,OpName:TID).
540
541		:- block check_type(?,-,?).
542		check_type(boolean,pred_true,_) :- !.
543		check_type(boolean,pred_false,_) :- !.
544		check_type(integer,int(_),_) :- !.
545		check_type(string,string(_),_) :- !.
546		check_type(global(GS),fd(_,GS),_) :- !.
547		check_type(couple(A,B),(VA,VB),OID) :- !, check_type(A,VA,OID), check_type(B,VB,OID).
548		check_type(set(_T),[],_) :- !.
549		check_type(set(_T),closure(_,_,_),_) :- !. % TO DO: check type signature of closure
550		check_type(set(T),[H|_],OID) :- !, check_type(T,H,OID).
551		check_type(set(T),avl_set((node(Y,_,_,_L,_R))),OID) :- !, check_type(T,Y,OID).
552		check_type(seq(T),V,OID) :- !, check_type(set(couple(integer,T)),V,OID).
553		% TO DO: record, freetype ; but do not appear in translation from CSP to B yet
554		check_type(Type,Value,OpName:TID) :-
555		def_get_texpr_id(TID,ID),
556		add_error(check_type_for_id,'Illegal CSP value for argument: ',OpName:ID:type(Type):value(Value)),
557		fail.
558
559		get_operation_internal_name(Op,Name) :- var(Op),!,
560		add_error(get_operation_internal_name,'Variable Transition: ',Op), Name=Op.
561		get_operation_internal_name('$initialise_machine',N) :- !, N='$initialise_machine'.
562		get_operation_internal_name('$setup_constants',N) :- !, N='$setup_constants'.
563		get_operation_internal_name('$partial_setup_constants',N) :- !, N='$partial_setup_constants'.
564		get_operation_internal_name(Op,Name) :- get_operation_name(Op,Name).
565
566		% tool to get the basic operation/channel/event name of a transition:
567		get_operation_name(Op,Name) :- var(Op),!, add_error(get_operation_name,'Variable Transition: ',Op), Name=Op.
568		get_operation_name('-->'(F,_),N) :- !, functor(F,N,_).
569		%get_operation_name(io([Action|_],proc(_Nr,_PROC),_SPAN),F) :-
570		% animation_mode(promela),!,functor(Action,F,_).
571		get_operation_name(io(_V,Ch,_SPAN),N) :- csp_mode,!, functor(Ch,N,_).
572		get_operation_name(FullOperation,Name) :- functor(FullOperation,Functor,_),
573		translate_operation_name(Functor,Name).
574
575		get_operation_arguments(Op,Args) :- var(Op),!, add_error(get_operation_arguments,'Variable Transition: ',Op), Args=[].
576		get_operation_arguments('-->'(F,_ReturnValues),Args) :- !, F =.. [_|Args].
577		%get_operation_arguments(io([_Action|V],proc(_Nr,_PROC),_SPAN),Args) :-
578		% animation_mode(promela),!,Args=V.
579		get_operation_arguments(io(V,_Ch,_SPAN),Args) :- csp_mode,!, Args = V.
580		get_operation_arguments(FullOperation,Args) :- FullOperation =.. [_|Args].
581
582		get_operation_return_values_and_arguments('-->'(F,ReturnValues),ReturnValues,Args) :- !,
583		F =.. [_|Args].
584		get_operation_return_values_and_arguments(Op,[],Args) :- get_operation_arguments(Op,Args).
585
586		translate_operation_name('$initialise_machine',T) :- !,T='INITIALISATION'.
587		translate_operation_name('$setup_constants',T) :- !,T='SETUP_CONSTANTS'.
588		translate_operation_name('$partial_setup_constants',T) :- !,T='PARTIAL_SETUP_CONSTANTS'.
589		%translate_operation_name(InternalName,Res) :- !, Res=InternalName.
590		translate_operation_name(X,X).
591
592
593
594
595
596		:- use_module(state_space,[visited_expression/2]).
597		:- use_module(library(between),[between/3]).
598
599		b_trans(State,OpName,Operation,NewState,PathInfo) :-
600	?	compute_operation_effect_max(State,OpName,Operation,NewState,PathInfo,_Max).
601
602		compute_operation_effect_max([],OpName,Operation,NewState,PathInfo,Max) :-
603		compute_operation_on_expanded_store([],OpName,Operation,Updates,PathInfo,Max),
604		store:store_updates_and_normalise(Updates,[],NewState).
605		compute_operation_effect_max([H|T],OpName,Operation,NewState,PathInfo,Max) :-
606		compute_operation_on_expanded_store([H|T],OpName,Operation,Updates,PathInfo,Max),
607		store:store_updates_and_normalise(Updates,[H|T],NewState).
608		compute_operation_effect_max(const_and_vars(ConstID,Vars),OpName,Operation,ResultingStore,PathInfo,Max) :-
609		prepare_state_for_specfile_trans(const_and_vars(ConstID,Vars),R),
610		%print(expanded_const_and_vars(ConstID)),nl,
611		compute_operation_effect_max(R,OpName,Operation,ResultingStore,PathInfo,Max).
612		compute_operation_effect_max(concrete_constants(ConstantsStore),'$initialise_machine',OpInit,ResultingStore,PathInfo,Max) :-
613	?	get_max_enablings_for_init(Max,'$initialise_machine',MaxForCall),
614	?	succeed_max_call_id('$initialise_machine',
615		b_interpreter:b_initialise_machine(ConstantsStore,InitialVars,InitialStore,PathInfo),MaxForCall),
616		create_initialisation_operation(InitialVars,OpInit),
617		%user:do_one_gui_event,
618	?	(\+ preferences:preference(symmetry_mode,flood), /* TO DO : improve permutation to allow using const_and_vars optimisation */
619	?	visited_expression(ConstID,concrete_constants(ConstantsStore))
620		-> ResultingStore = const_and_vars(ConstID,InitialVars) /* avoid storing constant values again */
621		; ResultingStore = InitialStore).
622		compute_operation_effect_max(expanded_const_and_vars(ConstID,Vars,FullStore),OpName,Operation,ResultingStore,PathInfo,Max) :-
623		%print(const_and_vars(ConstID,Vars)),nl,
624	?	compute_operation_on_expanded_store(FullStore,OpName,Operation,Updates,PathInfo,Max),
625		ResultingStore = const_and_vars(ConstID,NewVars),
626		store:store_updates_and_normalise(Updates,Vars,NewVars).
627		%store:store_updates(Updates,Vars,NewVars). % we could use this when operation re-used / cached
628		%ErrorMsg = compute_operation_effect(const_and_vars(ConstID,Vars),Operation,ResultingStore,PathInfo),
629		%reconstruct_constants_store(ConstID,ConstantsStore,NewState,ErrorMsg,ResultingStore).
630		compute_operation_effect_max(root,'$setup_constants',OpSetup,concrete_constants(FilteredConstantsStore),[],Max) :-
631	?	b_machine_has_constants_or_properties,
632	?	get_max_enablings_for_init(Max,'$setup_constants',MaxForCall),
633	?	compute_constants(ConstantsStore,MaxForCall),
634		create_setup_constants_operation(ConstantsStore,OpSetup),
635		%%print_message('FOUND_CONSTANTS'(OpName)),
636		(get_preference(filter_unused_constants,true)
637		-> exclude(unused_binding,ConstantsStore,FilteredConstantsStore)
638		; FilteredConstantsStore=ConstantsStore).
639		%user:do_one_gui_event.
640		compute_operation_effect_max(root,'$initialise_machine',OpInit,InitialStore,PathInfo,Max) :-
641		\+ b_machine_has_constants_or_properties,
642		get_max_enablings_for_init(Max,'$initialise_machine',MaxForCall),
643		%user:do_one_gui_event, user:do_one_gui_event, user:do_one_gui_event,
644		empty_state(EmptyState),
645		succeed_max_call_id('$initialise_machine',
646		b_interpreter:b_initialise_machine(EmptyState,InitialVars,InitialStore,PathInfo),MaxForCall),
647		create_initialisation_operation(InitialVars,OpInit).
648		%user:do_one_gui_event.
649
650		unused_binding(bind(C,_)) :- bmachine:b_is_unused_constant(C).
651
652		compute_constants(ConstantsStore,_Max) :-
653		% check if values have been computed and stored into a file before -- if yes, use them
654		load_constants(Stores,MaxReached),!,
655		choose_loaded_solution(Stores,ConstantsStore,MaxReached).
656		compute_constants(ConstantsStore,Max) :-
657		% print('Searching for valid CONSTANTS'),nl,!,
658	?	succeed_max_call_id('$setup_constants',b_interpreter:b_set_up_concrete_constants(ConstantsStore),Max).
659
660		choose_loaded_solution(Stores,ConstantsStore,_MaxReached) :-
661		member(ConstantsStore,Stores).
662		choose_loaded_solution(_Stores,_ConstantsStore,true) :-
663		% provoke the setting of the "maximum reached flag"
664		succeed_max_call_id('$setup_constants',member(_,_),1),fail.
665
666		expand_const_and_vars_to_full_store(root,R) :- !,R=[].
667		expand_const_and_vars_to_full_store(concrete_constants(ConstantsStore),FullStore) :- !,
668		ConstantsStore = FullStore.
669		expand_const_and_vars_to_full_store(const_and_vars(ConstID,Vars),FullStore) :- !,
670		expand_const_and_vars(ConstID,Vars,FullStore).
671		expand_const_and_vars_to_full_store(expanded_const_and_vars(_ConstID,_Vars,ExpStore),FullStore) :- !,
672		FullStore = ExpStore.
673		expand_const_and_vars_to_full_store(R,R).
674
675		expand_const_and_vars(ConstID,Vars,FullStore) :-
676		state_space:visited_expression(ConstID,concrete_constants(ConstantsStore)), %% This can take a while if the Constants are big !
677		% print('exp: '),tools_printing:print_term_summary(ConstantsStore),nl,
678		append(ConstantsStore,Vars,FullStore).
679
680		expand_to_constants_and_variables(root,[],[]).
681		expand_to_constants_and_variables(concrete_constants(ConstStore),ConstStore,[]).
682		expand_to_constants_and_variables(const_and_vars(ConstID,VarStore),ConstStore,VarStore) :-
683		state_space:visited_expression(ConstID,concrete_constants(ConstStore)).
684		expand_to_constants_and_variables([],[],[]).
685		expand_to_constants_and_variables([H|T],[],[H|T]).
686
687		:- use_module(b_operation_cache,[compute_operation_on_expanded_store_cache/5]).
688
689		% compute operation effect on a store where all constants have been put into the environment
690		compute_operation_on_expanded_store(InState,OpName,Operation,NewState,PathInfo,Max) :-
691		get_preference(try_operation_reuse,full),
692		animation_mode(b), % doesn't seem to work with CSP||B yet; see CSPB/LTSMin/Counters.mch + .csp
693		\+ animation_minor_mode(eventb), % projection seems to confuse Event-B interpreter, see e.g. prob_examples/public_examples/EventBPrologPackages/ABZ_Landing_Gear/Ref3_ControllerSensors_mch.eventb
694		% TO DO: fix
695		!,
696		get_max_enablings_per_operation(Max,OpName,MaxForCall),
697		succeed_max_call_id(OpName,
698		compute_operation_on_expanded_store_cache(OpName,Operation,InState,NewState,PathInfo),
699		MaxForCall).
700		compute_operation_on_expanded_store(InState,OpName,Operation,NewState,PathInfo,Max) :-
701	?	get_max_enablings_per_operation(Max,OpName,MaxForCall),
702	?	succeed_max_call_id(OpName,
703		b_interpreter:b_execute_top_level_operation_update(OpName,Operation,InState,NewState,PathInfo),
704		MaxForCall).
705
706
707		create_initialisation_operation(_InitialVars,'$initialise_machine').
708
709		create_setup_constants_operation(_ConstantVars,'$setup_constants').
710
711		:- use_module(bmachine,[b_get_machine_operation_max/2]). % MAX_OPERATIONS_... DEFINITIONS
712		get_max_enablings_per_operation_aux(OpName,RMax,RandomisedRestart) :-
713		b_get_machine_operation_max(OpName,Max),
714		!,
715		(Max<0 -> RMax is -Max, RandomisedRestart=true ; RMax=Max, RandomisedRestart=false).
716		get_max_enablings_per_operation_aux(_OpName,Max,false) :-
717		preferences:preference(maxNrOfEnablingsPerOperation,Max).
718
719
720		get_max_enablings_per_operation(Max,OpName,MaxForCall) :-
721		(var(Max) -> get_max_enablings_per_operation_aux(OpName,Max,RandomisedRestart) ; RandomisedRestart=false),
722		(RandomisedRestart=true,
723		get_preference(randomise_enumeration_order,true)
724		-> % we succeed Max times with the value 1, thus forcing a randomised restart
725		MaxForCall=1, between(1,Max,Retry), format('Randomised Restart ~w for ~w~n',[Retry,OpName])
726		; % we succeed once with the value Max
727		MaxForCall is Max).
728
729		get_max_enablings_for_init(Max,Op,MaxForCall) :-
730		(var(Max) -> get_preference(maxNrOfInitialisations,Max) ; true),
731		(Max>1,
732		get_preference(randomisedRestartInitalisations,true),
733		get_preference(randomise_enumeration_order,true)
734		-> % we succeed Max times with the value 1, thus forcing a randomised restart
735		MaxForCall=1, between(1,Max,Retry), format('Randomised Restart ~w for ~w~n',[Retry,Op])
736		; % we succeed once with the value Max
737		MaxForCall=Max).
738
739		/* PROPERTIES */
740
741		property(const_and_vars(ConstID,Vars),Property) :- b_or_z_mode,
742		expand_const_and_vars(ConstID,Vars,FullStore),!,
743		property(FullStore,Property).
744		property(csp_and_b(CSPState,BState),Property) :- animation_mode(csp_and_b),!,
745		%% print(checking_csp_and_b(CSPState)),nl,
746		expand_const_and_vars_to_full_store(BState,FBState),
747		(xtl_interface:cspm_property(CSPState,Property) ;
748		b_property(FBState,Property)).
749		property(State,Property) :- animation_mode(AM),
750		(AM = b -> b_property(State,Property)
751		; AM=xtl -> xtl_interface:xtl_property(State,Property)
752		; AM=cspm -> xtl_interface:cspm_property(State,Property)
753		; AM=csp_and_b -> b_property(State,Property) % State should be root
754		).
755
756		%b_property(const_and_vars(ConstID,Vars),Prop) :- !,
757		% expand_const_and_vars(ConstID,Vars,FullStore),
758		% b_property(FullStore,Prop).
759		b_property(root,Prop) :- !, b_preference_par(PARA,Op,VAL), Prop=.. [Op,PARA,VAL].
760		b_property([H|T],non_ground(Var)) :- debug:debug_mode(on),
761		member(bind(Var,Val),[H|T]),\+(ground(Val)).
762		b_property([H|T],Prop) :- elementary_prop([H|T],Prop).
763		b_property([],Prop) :- elementary_prop([],Prop).
764		b_property(concrete_constants(DB),Prop) :- elementary_prop(DB,Prop).
765
766
767
768		:- use_module(preferences).
769		:- use_module(b_global_sets,[b_global_set/1, b_get_fd_type_bounds/3,inferred_minimum_global_set_cardinality/2,
770		inferred_maximum_global_set_cardinality/2, unfixed_deferred_set/1]).
771
772		b_preference_par('MAXINT','=',MaxInt) :- get_preference(maxint,MaxInt).
773		b_preference_par('MININT','=',MinInt) :- get_preference(minint,MinInt).
774		b_preference_par(card(GlobalSet),Op,Card) :-
775		b_global_set(GlobalSet),
776		b_get_fd_type_bounds(GlobalSet,Low,Up), RCard is Up-Low+1,
777		% provide feedback if unfixed_deferred_set
778		(inferred_maximum_global_set_cardinality(GlobalSet,MaxCard),
779		(inferred_minimum_global_set_cardinality(GlobalSet,MinCard) -> true ; MinCard=1),
780		MinCard \= MaxCard,
781		Op = ':', Card = '..'(MinCard,MaxCard)
782
783		;
784
785		inferred_minimum_global_set_cardinality(GlobalSet,MinCard),
786		\+ (inferred_maximum_global_set_cardinality(GlobalSet,_)),
787		Op='>=',Card=MinCard % show minimum cardinality info
788
789		;
790
791		Op= '=', (unfixed_deferred_set(GlobalSet)
792		-> ajoin([RCard,' (assumed for deferred set)'],Card) ; Card=RCard)
793		).
794
795		/* --------------------------------------------------------- */
796
797
798		elementary_prop(DB,Prop) :-
799		member(bind(Var,Val),DB), %print(var_prop(Var)),nl_time,
800		elementary_prop3(Val,Var,Prop).
801
802		:- use_module(custom_explicit_sets,[is_avl_relation/1,is_avl_partial_function/1,get_first_avl_elements/4, avl_approximate_size/3]).
803		elementary_prop3(Val,Var,Prop) :- var(Val),!, Prop = '='(Var,'_VAR_').
804		elementary_prop3(avl_set(Avl),Var,Prop) :- !,
805		(show_avl_set(Avl) % \+ custom_explicit_sets:is_avl_sequence(Avl))
806		-> elementary_fun_prop(avl_set(Avl),Var,Prop)
807		; elementary_var_prop(avl_set(Avl),Var,Prop)).
808		elementary_prop3([H|T],Var,Prop) :- H=(_,_),
809		get_preference(show_function_tuples_in_property,true),!,
810		elementary_fun_prop([H|T],Var,Prop).
811		elementary_prop3(Val,Var,Prop) :- elementary_var_prop(Val,Var,Prop).
812
813		show_avl_set(AVL) :- get_preference(show_function_tuples_in_property,true),
814		is_avl_relation(AVL),
815		avl_approximate_size(AVL,0,Size), Size < 257, % only the first 30 will be shown by get_relation_element anyway
816		is_avl_partial_function(AVL).
817
818
819		:- use_module(bmachine,[b_is_variable/2]).
820		elementary_var_prop(Val,Var,Prop) :-
821		% TODO: use translate:translate_bvalue_for_expression/3
822		animation_minor_mode(tla),!,
823		( identifier_has_tla_type(Var,TlaType) ->
824		translate_bvalue_with_tlatype(Val,TlaType,Text)
825		; otherwise ->
826		translate_bvalue(Val,Text)),
827		Prop = '='(Var,Text).
828		elementary_var_prop(Val,Var,Prop) :-
829		(b_is_variable(Var,Type) % what about constants
830		-> translate_bvalue_with_type_and_limit(Val,Type,320,Text)
831		; translate_bvalue_with_type_and_limit(Val,any,320,Text)), % translate_properties_with_limit uses 320 Limit
832		Prop = '='(Var,Text).
833
834		identifier_has_tla_type(Id,Type) :-
835		get_texpr_id(TId,Id),
836		(b_get_machine_constants(Ids)
837		;b_get_machine_variables(Ids)),
838		member(TId,Ids),!,
839		get_texpr_info(TId,Infos),
840		memberchk(tla_type(Type),Infos).
841		% to do: use b_is_variable + translate_bvalue_with_type
842		elementary_fun_prop(Val,Var,Prop) :-
843		nonvar(Val),
844		get_relation_element(Val,X,Y), % Show value in form: Var(X) = Y
845		create_texpr(identifier(Var),any,[],Fun),
846		create_texpr(value(X),any,[],Arg),
847		create_texpr(function(Fun,Arg),any,[],Lhs),
848		create_texpr(value(Y),any,[],Rhs),
849		create_texpr(equal(Lhs,Rhs),pred,[],Expr),
850		translate_bexpression_with_limit(Expr,80,Prop).
851
852		get_relation_element(avl_set(A),X,Y) :- custom_explicit_sets:is_avl_relation(A),
853		!, %preferences:preference(expand_avl_upto,Limit),
854		Limit=30, % reduced limit, as now we can inspect with evaluation view
855		get_first_avl_elements(A,Limit,Els,CutOff),
856		(member((X,Y),Els), X\=term(_)
857		;
858		CutOff=not_all, X='...', Y='...').
859		get_relation_element(Value,X,Y) :-
860		member((X,Y),Value). /* otherwise we have a record structure */
861
862
863		:- use_module(bmachine,[b_show_machine_representation/3]).
864		:- use_module(probcspsrc(haskell_csp_analyzer),[get_internal_csp_representation/1]).
865		get_internal_representation(X) :- get_internal_representation(X,false).
866		get_internal_representation(X,UnsetMinorMode) :- animation_mode(AM), get_internal_aux(AM,X,UnsetMinorMode).
867		get_internal_aux(b,X,UnsetMinorMode) :- !, b_show_machine_representation(X,true,UnsetMinorMode). % UnsetMinorMode=true means we try and generate classical B syntax
868		get_internal_aux(cspm,X,_) :- !, get_internal_csp_representation(X).
869		get_internal_aux(csp_and_b,Res,UnsetMinorMode) :- !, append("CSP||B - B Part only",X,Res),
870		b_show_machine_representation(X,true,UnsetMinorMode).
871		get_internal_aux(_,X,_) :- X="Internal representation only available in B or CSP mode".
872
873
874		:- use_module(probcspsrc(haskell_csp),[channel/2]).
875		:- use_module(bmachine,[b_top_level_operation/1]).
876		get_possible_event(OpName) :- b_or_z_mode,
877		%b_is_operation_name(OpName).
878		b_top_level_operation(OpName).
879		get_possible_event(Channel) :- csp_mode,
880		channel(Channel,_).
881		% what about csp_and_b mode ?
882
883
884		get_possible_language_specific_top_level_event(OpName,ResultNames,ParameterNames) :-
885		b_or_z_mode,!,
886		get_possible_b_top_level_event(OpName,ResultNames,ParameterNames).
887		get_possible_language_specific_top_level_event(Channel,unknown,unknown) :- csp_mode,
888		channel(Channel,_).
889
890		get_possible_b_top_level_event('$setup_constants',[],Ids) :-
891		b_machine_has_constants_or_properties,
892		b_get_machine_constants(TIds), maplist(get_texpr_id,TIds,Ids).
893		get_possible_b_top_level_event('$initialise_machine',[],Ids) :-
894		b_get_machine_variables(TIds), maplist(get_texpr_id,TIds,Ids).
895		get_possible_b_top_level_event(OpName,ResultNames,ParameterNames) :-
896		b_top_level_operation(OpName),
897		b_get_machine_operation(OpName,Results,RealParameters,_RealBody,_OType,_OpPos),
898		maplist(get_texpr_id,Results,ResultNames),
899		maplist(get_texpr_id,RealParameters,ParameterNames).
900
901		% obtain a textual description of specification category names
902		get_specification_description(Category,Name) :-
903		animation_mode(Mode),
904		(animation_minor_mode(Minor) -> true ; Minor = none), % there could be several minor modes !
905		(get_specific_description(Mode,Minor,Category,N) -> Name=N
906		; get_default_description(Category,N) -> Name = N
907		; add_error(get_specification_description,'Unknown category: ',Category),
908		Name=Category).
909
910		get_specific_description(cspm,_,C,N) :- get_csp_description(C,N).
911		get_specific_description(b,eventb,C,N) :- get_eventb_description(C,N).
912		get_specific_description(b,tla,C,N) :- get_tla_description(C,N).
913
914		get_csp_description(operations,'CHANNELS').
915		get_csp_description(operation,'CHANNEL').
916		get_csp_description(assertions,'CSP_ASSERTIONS').
917		get_csp_description(machine,'CSP_SPECIFICATION').
918		get_csp_description(operations_lc,'events').
919
920		get_tla_description(properties,'ASSUME').
921		get_tla_description(machine,'MODULE').
922		get_tla_description(operation,'ACTION'). % no key word
923		get_tla_description(operations,'ACTIONS'). % no key word
924		get_tla_description(operations_lc,'actions').
925
926		get_eventb_description(properties,'AXIOMS').
927		get_eventb_description(assertions,'THEOREMS').
928		get_eventb_description(operations,'EVENTS').
929		get_eventb_description(operation,'EVENT').
930		get_eventb_description(operations_lc,'events').
931		get_eventb_description(machine,'MODEL').
932
933		get_default_description(properties,'PROPERTIES').
934		get_default_description(assertions,'ASSERTIONS').
935		get_default_description(invariant,'INVARIANT').
936		get_default_description(invariants,'INVARIANTS').
937		get_default_description(operations,'OPERATIONS').
938		get_default_description(operation,'OPERATION').
939		get_default_description(operations_lc,'operations').
940		get_default_description(machine,'MACHINE').
941		get_default_description(constants,'CONSTANTS').
942		get_default_description(variables,'VARIABLES').
943		get_default_description(initialisation,'INITIALISATION').
944		get_default_description(sets,'SETS').
945		get_default_description(goal,'GOAL').
946		get_default_description(definition,'DEFINITION').
947		get_default_description(definitions,'DEFINITIONS').
948		get_default_description(variants,'VARIANTS').