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