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