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