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 % bmachine provides access to the currently loaded B-machine and all its subsidiary machines
6
7 :- module(bmachine,[bmachine_is_precompiled/0,
8 b_enumerated_sets_precompiled/0,
9 b_set_initial_machine/0,
10 b_set_empty_machine/0,
11 b_set_machine/3,
12 b_set_typed_machine/2,
13 b_load_eventb_project/1, % used for loading .eventb files
14 b_set_eventb_project_flat/3, % set an Event-B project from terms
15
16 % used for loading additional VisB/... defs
17 b_load_additional_definitions_file/1,
18 b_load_additional_definitions_from_list_of_facts/1,
19 b_load_additional_definitions_from_term/1,
20
21 get_full_b_machine/2,
22 full_b_machine/1,
23 get_full_b_machine_sha_hash/1, % get SHA hash of loaded and type-checked B machine
24 b_machine_is_loaded/0,
25
26 get_proven_invariant/2,
27 get_unproven_invariants/1,
28 get_invariant_list_with_proof_info/1,
29 load_additional_information/1,
30 %% generate_specialized_invariants/0, %% no longer exists
31 get_operation_info/2,
32 b_get_operation_description/2,
33 get_operation_description_template_expr/2,
34
35 b_load_machine_from_file/1, b_load_machine_from_file/2,
36 b_load_machine_probfile/1, b_load_machine_probfile/2,
37 b_load_machine_from_list_of_facts/2,
38 b_load_machine_from_term/2, % used for Alloy
39 b_machine_precompile/0, other_spec_precompile/0,
40 b_machine_reset/0,
41
42 b_machine_name/1,
43
44 b_get_all_used_filenames/1, b_get_main_filename/1,
45 add_additional_filename/2,
46 set_additional_filename_as_parsing_default/3, reset_filename_parsing_default/2,
47 b_get_main_filenumber/1, b_filenumber/4, portray_filenumbers/0,
48 get_machine_file_number/4,
49 b_absolute_file_name_relative_to_main_machine/2,
50 b_get_animated_sections/1,
51
52 b_get_machine_set/1, b_get_machine_set/2,
53 b_get_named_machine_set/2, b_get_named_machine_set/3,
54 b_get_disjoint_constants_of_type/3, b_get_constant_represented_inside_global_set/2,
55 b_get_machine_constants/1, b_get_machine_all_constants/1,
56 b_machine_has_constants/0, b_machine_has_constants_or_properties/0,
57 b_is_constant/2, b_is_constant/1, b_is_unused_constant/1,
58 get_constant_span/2,
59 b_machine_has_variables/0,
60 b_is_variable/1, b_is_variable/2,
61 b_get_constant_variable_description/2,
62 constant_variable_marked_as_memo/1, constant_variable_marked_as_expand/1,
63 b_get_machine_variables_in_original_order/1, b_get_machine_variables/1,
64 get_primed_machine_variables/1,
65 get_nr_of_machine_variables/1, get_nr_of_machine_constants/1,
66 b_get_all_used_identifiers/1, % Note: may contain var$0 instead of var for becomes_such
67 b_get_all_used_identifiers_in_section/2, % ditto
68 get_machine_identifiers/2, get_machine_identifiers_with_pp_type/2,
69 source_code_for_identifier/6,
70
71 b_get_properties_from_machine/1,
72 b_get_invariant_from_machine/1,
73 b_get_linking_invariant_from_machine/1,
74 b_machine_has_assertions/0,
75 b_get_static_assertions_from_machine/1, b_machine_has_static_assertions/0,
76 b_get_unproven_static_assertions_from_machine/1,
77 b_get_dynamic_assertions_from_machine/1, b_machine_has_dynamic_assertions/0,
78 b_get_unproven_dynamic_assertions_from_machine/1,
79 b_get_assertions_from_main_machine/2, b_main_machine_has_no_assertions/0,
80 b_machine_has_unproven_assertions/0, get_assertions_from_machine/2,
81 get_all_assertions_from_machine/1,
82 b_machine_has_proven_invariants/0,
83 b_get_assertions/3,
84 b_get_assertion_count/3,
85 is_discharged_assertion/1,
86
87 b_get_initialisation_from_machine/2,
88 b_safe_get_initialisation_from_machine/2, % raise error if no INIT clause
89 b_machine_has_operations/0,
90 b_get_machine_operation/4, b_get_machine_operation/6,
91 b_get_machine_operation_for_animation/4, % does some rewriting for ANY parameters
92 b_get_machine_operation_for_animation/6, % does some rewriting for ANY parameters for TopLevel=true
93 b_get_machine_operation_for_animation/7, % additional Pos parameter
94 b_get_promoted_machine_operations/1,
95 b_top_level_operation/1, b_top_level_feasible_operation/1,
96 b_is_initialisation_name/1,
97 b_is_operation_name/1, b_get_operation_pos/2,
98 b_get_machine_operation_parameter_types/2,
99 b_get_machine_operation_parameter_names/2,
100 b_get_machine_operation_parameter_names_for_animation/2,
101 b_get_machine_operation_result_names/2,
102 b_get_machine_operation_typed_parameters/2,
103 b_get_machine_operation_typed_parameters_for_animation/2,
104 b_get_machine_operation_typed_results/2,
105 b_get_machine_operation_signature/2,
106 b_machine_operation_names_in_reverse_order/1,
107 b_get_operation_variant/3,
108
109 b_get_machine_setscope/2,
110 b_get_machine_operation_max/2,
111 b_get_machine_goal/1,
112 b_set_machine_goal/1, b_set_machine_goal/2,
113 b_set_machine_searchscope/1, b_set_machine_searchscope/2,
114 b_set_parsed_typed_machine_goal/1, b_unset_machine_goal/0,
115 b_reset_machine_goal_from_DEFINITIONS/0,
116 b_parse_machine_expression_from_codes/2,
117 b_parse_machine_expression_from_codes_with_prob_ids/2,
118 b_parse_machine_expression_from_codes_with_prob_ids/3,
119 b_parse_machine_expression_from_codes_with_prob_ids/4,
120 b_parse_machine_expression_from_codes/5,
121 b_parse_machine_expression_from_codes/6,
122 b_parse_machine_subsitutions_from_codes/6,
123 b_parse_machine_formula/3, b_parse_machine_formula_from_codes/7,
124 b_parse_machine_predicate/2, b_parse_machine_predicate/3,
125 b_parse_optional_machine_predicate/2,
126 b_parse_machine_predicate_from_codes/3,
127 b_parse_machine_predicate_from_codes_open/5,
128 b_parse_machine_operation_pre_post_predicate/3, b_parse_machine_operation_pre_post_predicate/5,
129 get_machine_operation_additional_identifiers/2,
130
131 determine_type_of_formula/2, determine_type_of_formula/3,
132
133 parse_expression_raw_or_atom_with_prob_ids/2,
134
135 % a version where parsing and type checking are separate:
136 b_parse_wo_type_machine_predicate_from_codes_to_raw_expr/2,
137 b_type_check_raw_expr/4,
138
139 b_get_machine_searchscope/1,
140 b_get_machine_animation_function/2,
141 b_get_machine_heuristic_function/1,
142 b_get_machine_animation_expression/2,
143 b_get_machine_custom_edges_function/2,
144 b_get_machine_custom_nodes_function/2,
145 b_get_machine_custom_graph_function/2,
146 b_machine_temp_predicate/1,
147 %set_temp_predicate/2,
148 assert_temp_typed_predicate/1,
149 reset_temp_predicate/0,
150 add_additional_property/2, b_machine_additional_property/1,
151
152 get_animation_image/2, get_animation_image_source_file/2,
153 b_get_definition/5, b_get_definition_with_pos/6,
154 b_get_definition_string_from_machine/2, b_get_definition_string_from_machine/3,
155 b_definition_prefixed/5, b_sorted_b_definition_prefixed/4,
156 % get typed definitions without parameters:
157 b_get_typed_definition/3, b_get_typed_definition_with_error_list/5,
158 b_get_typed_predicate_definition/3,
159 b_get_typed_expression_definition/3, b_get_true_expression_definition/1,
160
161 b_nth1_invariant/3, % get nth invariant with used Ids
162 b_invariant_number_list/1,
163 b_specialized_invariant_for_op/2,
164 b_specialized_invariant_mask_for_op/2,
165 b_operation_preserves_full_invariant/1, b_operation_preserves_invariant/2,
166 tcltk_get_specialized_invariant_for_op/2, tcltk_get_specialized_invariants_for_ops/1,
167 b_get_operation_normalized_read_write_info/3, % used to be b_normalized_rwsets_for_op/3,
168 b_get_operation_unchanged_variables/2,
169 b_operation_cannot_modify_state/1,
170 b_operation_reads_output_variables/3,
171 b_get_operation_non_det_modifies/2,
172
173 b_extract_values_clause_assignment/3,
174
175 b_type_expression/5,b_type_expression_for_full_b_machine/6,
176 b_type_open_predicate/5,b_type_open_predicate_with_errors/4,
177 b_type_open_exists_predicate/3,
178 type_with_errors/4,
179
180 b_show_machine_representation_unicode/4, b_show_machine_representation/4,
181 b_get_internal_prolog_representation_as_codes/1,
182 b_write_machine_representation_to_file/2,
183 b_write_machine_representation_to_file/3,
184 b_write_eventb_machine_to_classicalb_to_file/1,
185 b_get_eventb_machine_as_classicalb_codes/3,
186 b_show_eventb_as_classicalb/2,
187
188 b_get_machine_refinement_hierarchy/1,
189 b_get_refined_machine/1, b_get_refined_machine_name/1, b_get_refined_ancestors_names/1,
190 b_get_machine_header_position/2,
191 b_get_model_type/1,
192 b_machine_statistics/2,
193
194 % More Proof Information:
195 discharged_guard_strengthening/4,
196
197 % Flow information
198 wp_untyped/3, clear_wp/0,
199 nonchanging_guard/2,
200 typecheck_predicates/4
201 ]).
202
203 :- use_module(library(lists)).
204 :- use_module(library(ordsets)).
205
206 :- use_module(self_check).
207 :- use_module(error_manager).
208 :- use_module(debug).
209 :- use_module(bmachine_construction,[check_machine/4,type_in_machine_l/6,type_open_predicate_with_quantifier/6]).
210 :- use_module(bsyntaxtree).
211 :- use_module(bmachine_structure,[get_section/3,write_section/4,get_section_texprs/3]).
212 :- use_module(parsercall).
213 :- use_module(tools).
214 :- use_module(translate,[translate_machine/3,translate_eventb_to_classicalb/3]).
215 :- use_module(bmachine_eventb,[check_event_b_project/4,is_eventb_additional_info/1]).
216 :- use_module(kernel_freetypes,[register_freetypes/1]).
217 :- use_module(b_machine_hierarchy).
218 :- use_module(kodkodsrc(kodkod), [replace_by_kodkod/3]).
219
220 :- use_module(b_global_sets,[find_inequal_global_set_identifiers/4,
221 b_get_prob_deferred_set_elements/2,
222 b_check_and_precompile_enumerated_sets/0,
223 b_check_and_precompile_deferred_sets/0,
224 b_check_and_precompile_global_set_symmetry/0]).
225
226 % for applying transformations on the machines
227 :- use_module(record_detection,[replace_sets_by_records/2]).
228 :- use_module(partition_detection,[detect_partitions/2]).
229
230 :- use_module(module_information,[module_info/2]).
231 :- module_info(group,ast).
232 :- module_info(description,'This module provides access to the various parts of the loaded B machine.').
233
234 :- set_prolog_flag(double_quotes, codes).
235
236 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
237 % bmachine: module for storing the currently loaded machine
238 % Contains predicates for getting (already typed) information about
239 % different parts of the machine
240 % many predicates are precompiled by b_precompile_machine/0, see below for
241 % details.
242
243 :- volatile bmachine_is_precompiled/0.
244 :- dynamic bmachine_is_precompiled/0. /* TRUE if the precompiled predicates have been set */
245
246 assert_bmachine_is_precompiled :-
247 (bmachine_is_precompiled -> true ; assertz(bmachine_is_precompiled), debug_println(4,bmachine_is_precompiled)).
248
249 :- volatile machine/2.
250 :- dynamic machine/2.
251 % there is only one main machine fact
252
253 % true if a machine is loaded
254 b_machine_is_loaded :- (machine(_,_) -> true).
255
256 get_full_b_machine(Name,Res) :-
257 (machine(Name,M) -> Res=M
258 ; ground(Name) -> add_error(bmachine,'No B machine with this name loaded:',Name), fail
259 ; add_error(bmachine,'No B machine loaded'), fail
260 ).
261
262 full_b_machine(machine(Name,M)) :- get_full_b_machine(Name,M).
263
264 :- use_module(extension('probhash/probhash'),[raw_sha_hash/2]).
265 get_full_b_machine_sha_hash(Hash) :- full_b_machine(FM), raw_sha_hash(FM,Hash).
266
267 b_set_machine(Main,Machines,Errors) :-
268 b_machine_reset,
269 ? check_machine(Main,Machines,M1,Errors1),!,
270 apply_machine_transformations(M1,ResultMachine),
271 ( no_real_perror_occurred(Errors1) ->
272 %% get_memory_used(M1), %%
273 assert_main_machine(ResultMachine)
274 %%, get_memory_used(M2),print_memory_used(M2), print_memory_used_difference(M1,M2),nl %%
275 ;
276 true),
277 Errors=Errors1.
278
279 assert_main_machine(X) :- %tools_printing:trace_print(X),nl,
280 nonvar(X), X=machine(A,B),
281 !,
282 assertz(machine(A,B)). %, print(machine_asserted),nl.
283 assert_main_machine(X) :- add_internal_error('Illegal format: ',assert_main_machine(X)),fail.
284
285 :- meta_predicate apply_transformation_step(*,2,*,*).
286 % apply some transformations on the machine that require global information
287 % (other local transformations can be found in ast_cleanup)
288 apply_machine_transformations -->
289 apply_transformation_step('record definition detection', replace_sets_by_records),
290 apply_transformation_step('partition detection', detect_partitions). % is this necessary?? done in ast_cleanup
291
292 apply_transformation_step(Name,Pred,In,Out) :-
293 ( call(Pred, In, Out) -> true
294 ;
295 ajoin(['applying ', Name, ' failed, skipping.'], Msg),
296 add_error(bmachine,Msg),
297 In=Out).
298
299 % try to translate (parts of) the properties to Kodkod
300 % if it succeeds, replace the translated predicates by
301 % calls to the Kodkod process
302 try_kodkod :-
303 get_preference(use_solver_on_load,kodkod),
304 b_get_machine_constants(Constants),
305 Constants = [_|_],!,
306 b_get_properties_from_machine(OldPredicate),
307 ( replace_by_kodkod(Constants,OldPredicate,NewPredicate) ->
308 retract(machine(N,OldMachine)),
309 retractall( b_get_properties_from_machine(_) ),
310 write_section(properties,NewPredicate,machine(N,OldMachine),NewMachine),
311 assertz( NewMachine ),
312 assertz( b_get_properties_from_machine(NewPredicate) )
313 ;
314 true).
315 try_kodkod.
316
317 :- use_module(bmachine_static_checks, [static_check_main_machine/1]).
318 % set a machine term as current machine, without calling type checking
319 % (used for Z translations)
320 b_set_typed_machine(M1,FromFile) :-
321 b_machine_clear,
322 static_check_main_machine(M1), % done by check_machine in b_set_machine above
323 apply_machine_transformations(M1,ResultMachine),
324 assert_main_machine(ResultMachine),
325 set_all_used_filenames([FromFile]).
326
327 b_set_eventb_project_flat(Models,Contextes,Proofs) :-
328 b_machine_clear,
329 set_animation_mode(b), set_animation_minor_mode(eventb),
330 analyse_eventb_hierarchy(Models,Contextes),
331 ( check_event_b_project(Models,Contextes,Proofs,M1) ->
332 apply_machine_transformations(M1,ResultMachine),
333 assert_main_machine(ResultMachine) % has the form machine/2
334 ;
335 % Note: if there are typecheck errors due to missing .ptm files for axiomatic operators it is not an internal error!
336 fail).
337
338 b_load_eventb_project(Filename) :-
339 read_eventb_project_from_file(Filename,Machines,Contexts,Proofs,Errors,Prefs),
340 (Errors=[] -> true ; add_error(b_load_eventb_project,'Errors in Event-B Package: ',Errors)),
341 set_stored_prefs(Prefs),
342 set_all_used_filenames([Filename]),
343 b_set_eventb_project_flat(Machines,Contexts,Proofs),
344 clear_wp,
345 (load_additional_information(Proofs) -> true ; add_error(b_load_eventb_project,'Failed to load proof information',Proofs)).
346 % generate_specialized_invariants.
347
348 read_eventb_project_from_file(Filename, Machines, Contexts, Proofs, Errors, Prefs) :-
349 open(Filename, read, Stream, [encoding(utf8)]),
350 call_cleanup(read_eventb_project_from_stream(Stream, Filename, LoadCommand, Prefs), close(Stream)),
351 (eventb_load_command(LoadCommand, Machines, Contexts, Proofs, Errors)
352 -> true
353 ; add_error_and_fail(b_load_eventb_project, 'This is not a valid EventB Project file:', Filename)
354 ).
355
356 read_eventb_project_from_stream(Stream, Filename, LC, Prefs) :-
357 safe_read(Stream, Filename, Term),
358 (Term == end_of_file
359 -> Prefs = []
360 ; process_eventb_project_term(Term, LC, Prefs, PrefsTail),
361 read_eventb_project_from_stream(Stream, Filename, LC, PrefsTail)
362 ).
363
364 safe_read(Stream,Filename,T) :-
365 catch(read(Stream,T), E, (
366 ajoin(['.eventb file "', Filename, '" is corrupted; exception occurred while reading:'],Msg),
367 add_error(safe_read,Msg,E),
368 T=end_of_file
369 )).
370
371 process_eventb_project_term(Term, _LC, Prefs, Prefs) :-
372 %tools_printing:nested_write_term_to_codes(Term,Cs), format('~s~n',[Cs]),
373 var(Term),
374 !,
375 add_warning(b_load_eventb_project, 'Bare variable term in Event-B project: ', Term).
376 process_eventb_project_term(package(LoadCommand), LC, Prefs, Prefs) :-
377 !,
378 (nonvar(LC)
379 -> add_error_and_fail(b_load_eventb_project, 'Duplicate package/1 term in Event-B project: ', package(LoadCommand))
380 ; LC = LoadCommand
381 ).
382 process_eventb_project_term(stored_preference(Pref,Val), _LC, [stored_preference(Pref,Val)|Prefs], Prefs) :- !.
383 process_eventb_project_term(emf_model(_Name,_Base64Xml), _LC, Prefs, Prefs) :- !. % not used
384 process_eventb_project_term(Term, _LC, Prefs, Prefs) :-
385 functor(Term, F, N),
386 add_warning(b_load_eventb_project, 'Unrecognized term in Event-B project: ', F/N).
387
388 eventb_load_command(LoadCommand, _, _, _, _) :- var(LoadCommand), !, fail.
389 eventb_load_command(load_event_b_project(Machines,Contexts,Proofs,Errors), Machines, Contexts, Proofs, Errors).
390 eventb_load_command(load_event_b_project(Machines,Contexts,Errors), Machines, Contexts, [], Errors) :-
391 print('% Deprecated EventB Project without Proof Info.'), nl.
392
393 set_stored_prefs([stored_preference(Pref,Val)|Prefs]) :-
394 printsilent(stored_preference(Pref,Val)), nls,
395 preferences:set_preference(Pref,Val),
396 set_stored_prefs(Prefs).
397 set_stored_prefs([]).
398
399 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
400 % Collect Proof Information from Event B
401
402 :- volatile discharged/3.
403 :- volatile discharged_theorem/3, wd_po/3, wp_untyped/3.
404 :- volatile nonchanging_guard/2, discharged_guard_strengthening/4.
405 :- dynamic discharged/3.
406 % discharged(Model,Event,Name) : invariant Name in model Model is preserved by Event (no matter which Event at which refinement level)
407 :- dynamic discharged_theorem/3.
408 :- dynamic wd_po/3.
409 :- dynamic wp_untyped/3.
410 :- dynamic nonchanging_guard/2.
411 :- dynamic discharged_guard_strengthening/4.
412
413 :- volatile b_specialized_invariant_for_op/2, b_operation_preserves_invariant/2.
414 :- dynamic b_specialized_invariant_for_op/2, b_operation_preserves_invariant/2.
415 :- volatile b_nth1_invariant/3, b_invariant_number_list/1,
416 b_specialized_invariant_mask_for_op/2, get_proven_invariant/2.
417 :- dynamic b_nth1_invariant/3, b_invariant_number_list/1, b_specialized_invariant_mask_for_op/2, get_proven_invariant/2.
418 :- volatile complete_discharged_info/0.
419 :- dynamic complete_discharged_info/0.
420
421
422 clear_wp :-
423 retractall( wp_untyped(_,_,_) ).
424 %retractall( wp_typed(_,_,_) ). only in flow.pl
425
426 load_additional_information([]) :- !.
427 load_additional_information([H|T]) :-
428 ? load_additional_information_fact(H),!,
429 load_additional_information(T).
430 load_additional_information([H|T]) :- !,
431 add_internal_error('Unknown additional info: ',load_additional_information_fact(H)),
432 load_additional_information(T).
433 load_additional_information(I) :- !,
434 add_internal_error('Additional info not a list: ',load_additional_information_fact(I)).
435
436 % old style proof info
437 load_additional_information_fact(discharged(Machine,Theorem)) :- % a discharged theorem
438 debug_println(9,discharged_theorem(Machine,old_style_proof_info,Theorem)),
439 assertz(discharged_theorem(Machine,invariant,Theorem)).
440 load_additional_information_fact(discharged(Machine,Event,Invariant)) :-
441 debug_println(9,discharged(Machine,Event,Invariant)),
442 assertz(discharged(Machine,Event,Invariant)).
443 load_additional_information_fact(Term) :- % theories are handled in bmachine_eventb.pl already
444 is_eventb_additional_info(Term).
445
446 % new style proof info po(Machine,Info,SourceList,Discharged)
447
448 load_additional_information_fact(po(Machine,'Invariant preservation',Source,true)) :- % invariant preservation
449 add_discharged_po_infos(Source,Machine).
450
451 load_additional_information_fact(po(Machine,'Invariant establishment',Source,true)) :- % invariant establishment
452 add_discharged_po_infos(Source,Machine).
453
454 load_additional_information_fact(po(Machine,Text,Source,Proven)) :- % invariant wd
455 Text = 'Well-definedness of Invariant',
456 (member(invariant(Invariant),Source)
457 -> debug_println(9,wd_po(Machine,Invariant,Proven)),
458 assertz(wd_po(Machine,Invariant,Proven))
459 ; add_warning(bmachine,'Could not locate source of invariant WD-PO in machine ',Machine)
460 % this could be due to some plug-in generating invariants
461 ).
462 load_additional_information_fact(po(Machine,Text,Source,Proven)) :- % axiom wd
463 Text = 'Well-definedness of Axiom',
464 (member(axiom(Axiom),Source)
465 -> debug_println(9,wd_axiom(Machine,Axiom,Proven)) % TO DO: assert and use
466 ; add_warning(bmachine,'Could not locate source of axiom WD-PO in machine ',Machine)
467 % this could be due to some plug-in generating invariants
468 ).
469 load_additional_information_fact(po(Machine,Text,Source,Proven)) :-
470 Text = 'Well-definedness of Theorem', % could be invariant or axiom or guard
471 member(invariant(Invariant),Source),
472 debug_println(9,wd_po(Machine,Invariant,Proven)),
473 assertz(wd_po(Machine,Invariant,Proven)).
474 load_additional_information_fact(po(Machine,Text,Source,Proven)) :- % try axiom theorem wd
475 Text = 'Well-definedness of Theorem',
476 member(axiom(Axiom),Source),
477 debug_println(9,wd_axiom(Machine,Axiom,Proven)). % TO DO: assert and use
478 load_additional_information_fact(po(Machine,Text,Source,Proven)) :- % try proven theorem as guard
479 Text = 'Well-definedness of Theorem',
480 ? (member(guard(Grd),Source),
481 member(event(Evt),Source)
482 -> debug_println(9,wd_guard(Machine,Evt/Grd,Proven)) % TO DO: assert and use
483 ; add_warning(bmachine,'Could not locate source of theorem WD-PO in machine ',Machine)
484 % this could be due to some plug-in generating invariants
485 ).
486 load_additional_information_fact(po(Machine,Text,Source,Proven)) :- % wd of action
487 Text = 'Well-definedness of action',
488 (member(action(ACT),Source) % probably the guard in the last event with discharged info ??
489 -> debug_println(9,wd_action(Machine,ACT,Proven)) % TO DO: assert and use, if false: discard proven invariants?!
490 ; format('Illegal Rodin PO source in ~w for ~w: ~w~n',[Machine,Text,Source])
491 ).
492 load_additional_information_fact(po(Machine,Text,Source,Proven)) :- % wd of guard
493 Text = 'Well-definedness of Guard',
494 ? (member(guard(GRD),Source) % probably the guard in the last event with discharged info ??
495 -> debug_println(9,wd_guard(Machine,GRD,Proven)) % TO DO: assert and use
496 ; format('Illegal Rodin PO source in ~w for ~w: ~w~n',[Machine,Text,Source])
497 ).
498 load_additional_information_fact(po(Machine,'Theorem',[invariant(Theorem)],true)) :- % a theorem
499 debug_println(9,discharged_theorem(Machine,invariant,Theorem)),
500 assertz(discharged_theorem(Machine,invariant,Theorem)).
501 load_additional_information_fact(po(Machine,'Theorem',[axiom(Theorem)],true)) :- % a theorem
502 debug_println(9,discharged_theorem(Machine,axiom,Theorem)),
503 assertz(discharged_theorem(Machine,axiom,Theorem)).
504 load_additional_information_fact(po(Machine,'Theorem',[guard(GuardTheorem),event(Event)],true)) :- % a theorem in a guard
505 debug_println(9,discharged_theorem(Machine,guard(Event),GuardTheorem)),
506 assertz(discharged_theorem(Machine,guard(Event),GuardTheorem)).
507
508 % stuff we don't yet care about
509 load_additional_information_fact(po(Machine,Text,Infos,Proven)) :-
510 ( Text = 'Guard strengthening (split)'
511 ; Text = 'Guard strengthening (merge)'
512 ; Text = 'Guard strengthening' ),
513 !,
514 (Proven=true, Infos = [event(AbsEvent),guard(Guard),event(ConcreteEvent)]
515 -> assertz(discharged_guard_strengthening(Machine,AbsEvent,Guard,ConcreteEvent)),
516 debug_println(19,discharged_guard_strengthening(Machine,AbsEvent,Guard,ConcreteEvent))
517 ; true
518 ).
519 load_additional_information_fact(po(_,'Variant of event',_,_)).
520 load_additional_information_fact(po(_,'Natural number variant of event',_,_)).
521 load_additional_information_fact(po(_,'Action simulation',_,_)).
522 load_additional_information_fact(po(_,'Feasibility of witness',_,_)).
523 load_additional_information_fact(po(_,'Feasibility of action',_,_)).
524 load_additional_information_fact(po(_,'Well-definedness of witness',_,_)).
525 load_additional_information_fact(po(_,'Well-definedness of variant',_,_)).
526 load_additional_information_fact(po(_,'Finiteness of variant',_,_)).
527 load_additional_information_fact(po(_,'Equality of common variables',_,_)).
528
529 load_additional_information_fact(po(_Machine,_Kind,_Source,false)). % ignore everything that is not proven
530
531 load_additional_information_fact(po(_Machine,_Kind,_Source,reviewed)). % ignore everything that is only reviewed
532
533 % ignore exporter version for now
534 % we are compatible to both versions 2 and 3 (added abstract constants)
535 load_additional_information_fact(exporter_version(V)) :- V=2 ; V=3.
536
537 % ignored because the pragmas are attached to the machine in load_event_b_project/4
538 load_additional_information_fact(pragma(_Type,_Source,_AttachedTo,_Content)).
539
540 load_additional_information_fact(wp(S,D,P)) :-
541 assertz( wp_untyped(S,D,P) ).
542
543 load_additional_information_fact(nonchanging_guard(E,P)) :-
544 typecheck_predicates(P,TypedPred,E,_),
545 assertz(nonchanging_guard(E,TypedPred)).
546
547 load_additional_information_fact(invariant(_I)). %ignore
548
549 typecheck_predicates([],[],_,_).
550 typecheck_predicates([H|T],[TH|TT],S,D) :-
551 (S='INITIALISATION' -> Scope1 = []; Scope1=[operation(S)]),
552 ((D='INITIALISATION';var(D)) -> Scope2 = Scope1; Scope2=[operation(D)|Scope1]),
553 Scope = [variables|Scope2],
554 b_type_expression(H,Scope, _, TH, _),
555 typecheck_predicates(T,TT,S,D).
556
557
558 add_discharged_po_infos(Source,Machine) :-
559 % Source = [event(A1),...,event(CurMachineEvent),invariant(Inv)]
560 % note that CurMachineEvent could be equal to A1; A1 can be split up into multiple events (one of which could have the same name as A1; see Ticket PROB-292)
561 get_bottom_event(Source,Event),
562 member(invariant(Invariant),Source),
563 debug_println(9,discharged(Machine,Event,Invariant)),
564 assertz(discharged(Machine,Event,Invariant)),
565 % TO DO: should we propagate info up to abstract events which are not split up or where all refinements preserve a certain invariant ??
566 fail.
567 add_discharged_po_infos(_Source,_Machine).
568
569 % get the last event entry in proof info source list
570 get_bottom_event(Source,Event) :-
571 (bottom_event(Source,'$NONE'(none),Event) -> true
572 ; add_error(bmachine,'Could not determine event for proof info: ',Source),fail).
573 bottom_event([],Ev,Ev) :- Ev \= '$NONE'(none).
574 bottom_event([event(E)|T],_,Res) :- !,bottom_event(T,E,Res).
575 bottom_event([_|T],E,Res) :- bottom_event(T,E,Res).
576
577 :- use_module(debug).
578
579 tcltk_get_specialized_invariants_for_ops(list(Res)) :-
580 findall([Name,InvHeader,TI | Tail],
581 ((b_top_level_operation(Name) ; Name='$initialise_machine'),
582 tcltk_get_specialized_invariant_for_op_single(Name,TI,NrUnProven),
583 tcltk_get_proven_invariant_for_op(Name,PI),
584 ajoin([' INVARIANT (',NrUnProven,')'],InvHeader),
585 (PI='none' -> Tail = ['END;']
586 ; Tail = [' NON-TRIVIAL PROVEN INVARIANT:', PI, 'END;']
587 )
588 ), Res).
589 tcltk_get_specialized_invariant_for_op_single(Event,TI,NrUnProven) :-
590 (b_specialized_invariant_for_op(Event,Invariant) ->
591 conjunction_to_list(Invariant,IL), length(IL,NrUnProven),
592 translate:translate_bexpression(Invariant,TI)
593 ; TI = 'not_simplified', NrUnProven='-').
594 tcltk_get_specialized_invariant_for_op(Event,list(TI)) :-
595 (b_specialized_invariant_for_op(Event,Invariant) ->
596 conjunction_to_list(Invariant,IL),
597 (IL=[] -> TI = ['fully_proven']
598 ; maplist(translate:translate_bexpression,IL,TI))
599 ; TI = ['not_simplified']).
600 tcltk_get_proven_invariant_for_op(Event,TI) :- % get non-trivially proven invariants
601 (get_proven_invariant(Event,Invariant), \+ is_truth(Invariant) ->
602 translate:translate_bexpression(Invariant,TI)
603 ; TI = 'none').
604
605
606 :- public b_nth1_invariant_calc/3.
607 b_nth1_invariant_calc(Nr,Invariant,UsedIds) :-
608 get_invariant_list_with_used_ids(IL,IL_Ids),
609 ? nth1(Nr,IL,Invariant),
610 nth1(Nr,IL_Ids,UsedIds).
611
612 % bmachine:b_nth1_invariant(Nr,Inv,Used), format('~nInvariant ~w over ~w~n',[Nr,Used]), translate:print_bexpr(Inv),nl,fail
613 % bmachine:b_specialized_invariant_mask_for_op(Op,Mask), format('Mask ~w : ~w~n',[Op,Mask]),fail
614
615 :- public b_invariant_number_list_calc/1.
616 b_invariant_number_list_calc(InvList) :-
617 findall(nth1_invariant(Nr),b_nth1_invariant(Nr,_,_),InvList).
618
619 % use proof information to compute subset of invariant that needs to be checked for operations
620
621 % one fact including the position of all unproven invariants
622 :- public b_specialized_invariant_mask_for_op_calc/2.
623 b_specialized_invariant_mask_for_op_calc(Event,Mask) :-
624 preferences:get_preference(use_po,true),
625 get_invariant_list_with_used_ids(IL,IL_Ids),
626 % Note: we can have interference with CSE here, as lazy_let_pred at top-level can merge several conjuncts (but CSE is now disabled for the invariant if PROOF_INFO = TRUE)
627 IL \= [], % otherwise: Invariant already trivial; no sense in keeping track of information
628 ? get_op_or_init_and_syntax_filter(Event,ProofInfoEventName,IL,IL_Ids,RIL),
629 exclude(is_proven_invariant(ProofInfoEventName),RIL,RL), % Warning !! The invariants are not all from Model; the discharged information could be for a proven invariant with the same label from another model, see examples/EventBPrologPackages/ProofDirected/TestR_label_reuse.eventb; this should now properly be dealt with by filter_proven_invariants
630 IL\=RL, /* something filtered out */
631 (RL=[]
632 -> Mask = [] % fully proven
633 ; findall(Nr,(nth1(Nr,IL,Inv),member(Inv,RL)),Mask)
634 ),
635 debug_println(4,b_specialized_invariant_mask_for_op(Event,Mask)).
636
637 % TODO: investigate whether we should pre-compute this or simply re-compute it as needed
638 :- public b_specialized_invariant_for_op_calc/2.
639 b_specialized_invariant_for_op_calc(Event,Invariant) :-
640 ? b_specialized_invariant_mask_for_op(Event,Mask),
641 findall(Inv,(member(Nr,Mask),b_nth1_invariant(Nr,Inv,_)),RL),
642 conjunct_predicates(RL,Invariant). %, print(simplified),nl,translate:print_bexpr(Invariant),nl.
643
644
645 get_op_or_init_and_syntax_filter('$initialise_machine','INITIALISATION',IL,_,IL). % INIT always sets all variables
646 get_op_or_init_and_syntax_filter(Event,Event,IL,IL_Ids,RIL) :-
647 ? b_is_operation_name(Event),
648 filter_syntactically_relevant_invariants(IL,IL_Ids,Event,RIL). % filter out all invariants not modified by Event
649
650 :- public b_operation_preserves_invariant_calc/2.
651 % check if an operation preserves the full invariant; according to proof information
652 b_operation_preserves_invariant_calc(Event,Preserved) :-
653 ? b_specialized_invariant_mask_for_op(Event,Mask),
654 (Mask=[] -> Preserved=full_invariant ; Preserved=partial_invariant).
655
656 b_operation_preserves_full_invariant(Op) :- b_specialized_invariant_mask_for_op(Op,[]).
657
658 :- public get_proven_invariant_calc/2.
659 % computes proven, relevant invariants (not trivial ones which are unaffected by Event) for main model
660 get_proven_invariant_calc(Event, Invariant) :-
661 preferences:get_preference(use_po,true),
662 b_machine_name(Model),
663 get_invariant_list_with_used_ids(IL,IL_Ids),
664 ? b_is_operation_name(Event),
665 %print(filter_syntactically_relevant_invariants(Event,Model)),debug:nl_time,
666 filter_syntactically_relevant_invariants(IL,IL_Ids,Event,RIL),
667 %print(select_proven_invariants(Event,Model)),debug:nl_time,
668 select_proven_invariants(RIL,Model,Event,RL),
669 %print(conjunct_predicates(Event,Model)),debug:nl_time,
670 conjunct_predicates(RL,Invariant).
671
672 get_invariant_list_with_used_ids(IL,IL_Ids) :-
673 b_get_invariant_from_machine(I),
674 conjunction_to_list_with_rodin_labels(I,IL),
675 maplist(find_id_uses_for_maplist,IL,IL_Ids).
676 find_id_uses_for_maplist(Inv,IDs) :- find_identifier_uses(Inv,[],IDs).
677
678 % get list of invariants with proof info (discharged(_)) added
679 get_invariant_list_with_proof_info(InvariantList) :-
680 findall(I,get_invariant_with_proof_status_calc(I,_),InvariantList).
681
682 :- use_module(probsrc(tools_lists),[count_occurences/2]).
683
684 % compute all invariants which are not fully proven for events (initialisation is not examined!):
685 get_unproven_invariants(UnProvenList) :-
686 findall(I,get_invariant_with_proof_status_calc(I,unproven),UnProvenList).
687
688 get_invariant_with_proof_status_calc(Invariant,Proven) :- % not precompiled at the moment
689 b_machine_name(Model),
690 b_get_invariant_from_machine(I),
691 conjunction_to_list_with_rodin_labels(I,IL), % ensure rodin labels are propagated down for proof info
692 ? member(Inv,IL),
693 findall(Status,invariant_proof_status_for_event(Inv,Model,_Event,Status),StatusList),
694 count_occurences(StatusList,Occs),
695 (member(unproven-_,Occs)
696 -> Proven=unproven
697 ; (debug_mode(on) -> print('INVARIANT proven for all events: '), translate:print_bexpr(Inv),nl ; true),
698 Proven=proven
699 ),
700 add_texpr_info_if_new(Inv,proof_status(Proven,Occs),Invariant).
701
702 %is_unproven_inv_for_model(_Invariant,_Model,_Event) :-
703 % preferences:get_preference(use_po,false),!. % information is used in bvisual2,...
704 invariant_proof_status_for_event(Invariant,Model,Event,Status) :-
705 ? b_is_operation_name(Event),
706 proof_status_for_inv2(Invariant,Model,Event,Status).
707
708 proof_status_for_inv2(Invariant,_,Event,unchanged) :-
709 \+ is_syntactically_relevant_invariant_for_event(Event,Invariant),!. % invariant unaffected by Event/Operation
710 proof_status_for_inv2(Invariant,Model,Event,proven) :-
711 ? is_proven_invariant_for_model(Model,Event,Invariant),!.
712 proof_status_for_inv2(_,_,_,unproven).
713
714
715 % filter_syntactically_relevant_invariants(+InvariantsList, +UsedIDs, +EventName, -RelevantItemsFromInvariantsList)
716 filter_syntactically_relevant_invariants(Invariants,IL_Ids,Event,Result) :-
717 get_operation_info(Event,SubstitutionInfo),
718 get_modifies_from_info(SubstitutionInfo,SortedModIds),
719 filter_syntactically_relevant_invariants2(Invariants,IL_Ids,SortedModIds,Result).
720 % noticeably faster than include, see e.g. public_examples/B/PerformanceTests/Generated/Generated4000.mch
721 %include(is_syntactically_relevant_inv(SortedModIds),Invariants,IL_Ids,Result).
722
723 is_syntactically_relevant_inv(SortedModIds,_Inv,IDs) :-
724 ord_intersect(SortedModIds,IDs).
725
726 filter_syntactically_relevant_invariants2([],_,_,[]).
727 filter_syntactically_relevant_invariants2([Inv|T],[IDs|TI],SortedModIds,R) :-
728 (is_syntactically_relevant_inv(SortedModIds,Inv,IDs)
729 -> R=[Inv|TR] ; R=TR),
730 filter_syntactically_relevant_invariants2(T,TI,SortedModIds,TR).
731
732 is_syntactically_relevant_invariant_for_event(Event,Inv) :-
733 get_operation_info(Event,SubstitutionInfo),
734 get_modifies_from_info(SubstitutionInfo,SortedModIds),
735 find_id_uses_for_maplist(Inv,IDs),
736 is_syntactically_relevant_inv(SortedModIds,_Inv,IDs).
737
738 get_modifies_from_info(SubstitutionInfo,SortedModIds) :-
739 ((memberchk(modifies(ModID),SubstitutionInfo) -> ground(ModID))
740 -> list_to_ord_set(ModID,SortedModIds) % is this necessary ?
741 ; SortedModIds=[]).
742
743 % filter_proven_invariants(+InvariantsList, +ModelName, +EventName, -RelevantItemsFromInvariantsList)
744 % this gets called during model checking time
745 is_proven_invariant(Event,E) :-
746 % print('Filter Check: '), print(Event), print(' : '),translate:print_bexpr(E),nl,
747 get_precise_rodin_model_and_name(E,Model,Name),
748 !,
749 ? discharged_invariant(Model,Name,Event),
750 % now check that if E is not always well-defined that there are no unproven WD proof obligations !
751 check_wd_discharged_inv_or_thm(E,Model,Name,Event). %% print('DISCHARGED'(Model,Event,Name)),nl.
752
753 check_wd_discharged_inv_or_thm(E,_,_,_) :- always_well_defined(E),!.
754 check_wd_discharged_inv_or_thm(_,Model,Name,_Event) :- wd_po(Model,Name,ProofStatus),!,
755 ProofStatus=true.
756 check_wd_discharged_inv_or_thm(_,Model,Name,Event) :-
757 % no WD_PO associated or stored
758 % TO DO: we could try ProB-WD prover; but this situation only happens with old-style exports; we could use add_message
759 format('% Assuming invariant/theorem ~w is well-defined for event ~w:~w (no WD PO found).~n',[Name,Model,Event]).
760
761 % select_proven_invariants(+InvariantsList, +ModelName, +EventName, -RelevantItemsFromInvariantsList)
762 select_proven_invariants(Invariants,Model,Event,Result) :-
763 include(is_proven_invariant_for_model(Model,Event),Invariants,Result).
764
765 % Note: different from is_proven_invariant; TO DO: merge (here we assume main model)
766 is_proven_invariant_for_model(MainModel,Event,E) :-
767 ? get_rodin_name(E,Name), % if we do not have a rodin position we consider this as not proved
768 (get_rodin_model_name(E,Model) -> true
769 ; debug_format(19,'Could not get Rodin model name for invariant (deprecated .eventb format): ~w~n',[Name]),
770 Model=MainModel,
771 fail % we have an old style .eventb file; safer to assume not proven as there can be clashes of labels
772 ),
773 ? discharged_invariant(Model,Name,Event).
774
775 is_discharged_assertion(Theorem) :-
776 if( get_precise_rodin_model_and_name(Theorem,Model,Name),
777 (discharged_theorem(Model,_,Name), % does not matter if invariant or axiom
778 check_wd_discharged_inv_or_thm(Theorem,Model,Name,assertion) ) % check that well-defined
779 , (animation_minor_mode(eventb),
780 (silent_mode(on) -> true
781 ; print('Could not get position information for theorem: '),
782 translate:print_bexpr(Theorem),nl,
783 get_texpr_pos(Theorem,POS),debug_println(19,get_texpr_pos(POS))
784 ),
785 fail)
786 ).
787
788 get_precise_rodin_model_and_name(Theorem,Model,Name) :-
789 get_texpr_pos(Theorem,Pos),
790 (Pos = rodinpos(Model,Name,_)
791 -> true % only accept new rodinpos information with three parameters !
792 % the old one with two parameters could lead to confusion as labels can be reused
793 % we also do not accept rodin_derived_context_pos(Model,_Context,Name); not sure if this would be sound
794 ).
795
796 % derived predicate
797 discharged_invariant(Model,InvariantName,Event) :-
798 % InvariantName from model Model is preserved by Event and any of its refinements
799 discharged(Model,Event,InvariantName).
800 discharged_invariant(Model,InvariantName,Event) :-
801 % InvariantName from model Model is preserved by Event and any of its refinements
802 also_discharged(Model,Event,InvariantName).
803
804 b_machine_has_proven_invariants :-
805 ? (discharged(_,_,_) -> true).
806
807 % complete the discharged/3 information: propagating information from abstract events
808 % down to refined top-level events
809 :- public complete_discharged_info/0.
810 :- public complete_discharged_info_calc/0.
811 complete_discharged_info_calc :- debug_println(4,'completing discharged info: '),
812 statistics(runtime,[Start,_]),
813 (complete_discharged_info2 -> true ; true),
814 statistics(runtime,[Stop,_]), T is Stop-Start, debug_print(4,T), debug_println(4,' ms').
815 :- volatile discharged2/2, also_discharged/3.
816 :- dynamic discharged2/2.
817 :- dynamic also_discharged/3.
818 ?discharged_info_exists :- discharged2(_,_),!.
819 complete_discharged_info2 :- retractall(also_discharged(_,_,_)),
820 retractall(discharged2(_,_)),
821 ? discharged(Model,Event,_), % find out which Model and Events are used in discharged info
822 \+ discharged2(Model,Event), %print(discharged(Model,Event)),nl,
823 assertz(discharged2(Model,Event)),fail.
824 complete_discharged_info2 :- discharged_info_exists,
825 b_get_animated_sections(Sections),
826 ? discharged2(Model,Event), % Event in Model was proven to preserve an invariant in Model
827 b_get_abstract_events(Event,RModel,AbstractEvents), % search for a refinement of Model where the same event exists
828 RModel \= Model,
829 % i.e., invariant Name was proven in an abstract Model for Event
830 ? \+ is_abstract_event_in_list(Event,Model,AbstractEvents), % this event is *NOT* a refinement of the proven one
831 debug_println(4,removing_discharged(Model,Event)),
832 retractall(discharged(Model,Event,_Name)),
833 ? member(model(Model),Sections), % only generate error message if the Model is also animated using b_get_animated_sections, see example EventBPrologPackages/ProofDirected/TestInvPreserv_M2_ko_mch.eventb
834 % (otherwise the refinement may well exist but has been filtered out by restricting the animation levels)
835 add_error(event_refinement,'An event does not refine an abstract event of the same name: ',Event:Model:RModel),
836 % This will could cause errors in the proof information usage !
837 %print(AbstractEvents),nl,
838 fail.
839 complete_discharged_info2 :- discharged_info_exists,
840 complete_discharged_info3(_Model,_Event,_Name).
841 complete_discharged_info3(InvNameModel,AbsEvent,Name) :-
842 ? b_get_abstract_events(EventInRefinement,_RefModel,AbstrEvents),
843 ? is_abstract_event_in_list(AbsEvent,InvNameModel,AbstrEvents), % Event in InvNameModel is an abstract event of EventInRefinement
844 %print(check(InvNameModel,Event, EventInRefinement,RefModel)),nl,
845 ? discharged(InvNameModel,AbsEvent,Name), % print(chck2(Model,Event,Name)),nl,
846 %InvNameModel:Name has been proven for AbsEvent *at all relevant* levels
847 \+ discharged(InvNameModel,EventInRefinement,Name),
848 \+ also_discharged(InvNameModel,EventInRefinement,Name),
849 % this invariant has not yet been marked as proven for EventInRefinement
850 debug_println(4,also_discharged_in_refinement(InvNameModel:Name,EventInRefinement,refined_from(AbsEvent))),
851 assertz(also_discharged(InvNameModel,EventInRefinement,Name)),
852 fail.
853
854 %abstract_event_of_calc(TopLevelEvent,RModel,Event,Model) :-
855 % b_get_abstract_events(TopLevelEvent,RModel,AbstrEvents),
856 % is_abstract_event_in_list(Event,Model,AbstrEvents) , print(abs(TopLevelEvent,RModel,Event,Model)),nl.
857
858 is_abstract_event_in_list(Event,Model,AbstractEvents) :-
859 ? member(b(rlevent(AEvent,AModel,_S,_P,_G,_Thm,_Act,_VW,_PW,_Unm,AbstractEvents2),_,_),AbstractEvents),
860 (Event=AEvent, Model=AModel;
861 ? is_abstract_event_in_list(Event,Model,AbstractEvents2)).
862
863 % get events that are refined by an event
864 b_get_abstract_events(Name,Section,AbsEvents) :-
865 ? b_get_machine_operation(Name,_R,_P,Body,_OType,_OpPos),
866 get_texpr_expr(Body,RLEVENT),
867 RLEVENT = rlevent(_Name,Section,_Stat,_Parameters,_Grd,_Thm,_Act,_VWit,_PWit,_Unmod,AbsEvents).
868
869 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
870
871 :- volatile b_operation_reads_output_variables/3, b_operation_cannot_modify_state/1.
872 :- dynamic b_operation_reads_output_variables/3, b_operation_cannot_modify_state/1.
873
874 % test if we have a query or skip operation which cannot modify the state
875 % (preconditions, assertions could still fail though !)
876 :- public b_operation_cannot_modify_state_calc/1.
877 b_operation_cannot_modify_state_calc(Event) :-
878 ? b_get_operation_normalized_read_write_info(Event,_ReadVariables,[]).
879
880 :- use_module(b_read_write_info, [get_accessed_vars/4]).
881 % check if classical B operation reads its output variables
882 :- public b_operation_reads_output_variables_calc/3.
883 b_operation_reads_output_variables_calc(Event,ReadOutputVariablesIds,ReadOutputTypedInfo) :-
884 ? b_get_machine_operation(Event,ResultTuple,_TParas,TBody,_OType,_Pos),
885 def_get_texpr_ids(ResultTuple,ResIds),
886 sort(ResIds,SResIds),
887 get_operation_info(Event,SubstitutionInfo),
888 ? member(reads_locals(Reads),SubstitutionInfo), % locals are either arguments or return output variables
889 ord_intersection(Reads,SResIds,ReadOutputVariablesIds),
890 ReadOutputVariablesIds \= [],
891 % now recompute the information based on TBody after ast_cleanup: typing predicates have been removed
892 get_accessed_vars(TBody,[],_,AllReadsAfterAstCleanup), % important to pass [] as local variables
893 ord_intersection(AllReadsAfterAstCleanup,ReadOutputVariablesIds,ReadOutputVariablesIds2),
894 ReadOutputVariablesIds2 \= [],
895 (get_preference(allow_operations_to_read_outputs,true), debug_mode(off) -> true
896 ; ajoin(['Operation ', Event, ' is possibly reading or not always assigning to output parameters: '],Msg),
897 add_message(bmachine,Msg,ReadOutputVariablesIds2,ResultTuple)
898 % Note: analysis is not always precise: /public_examples/B/NewSyntax/CallOperationInExprSimple2.mch
899 ),
900 findall(reads_result(Index,ID,Type),
901 (nth1(Index,ResultTuple,b(identifier(ID),Type,_)), ord_member(ID,ReadOutputVariablesIds2)),
902 ReadOutputTypedInfo).
903
904
905
906 :- volatile b_get_operation_normalized_read_write_info/3, b_get_operation_unchanged_variables/2.
907 :- dynamic b_get_operation_normalized_read_write_info/3, b_get_operation_unchanged_variables/2.
908
909
910 :- use_module(bsyntaxtree,[get_global_identifiers/1]).
911
912 :- public b_get_operation_normalized_read_write_info_calc/3.
913 /* compute Read and Written Variables by an operation */
914 b_get_operation_normalized_read_write_info_calc(Event,SortedReadVariables,SortedWrittenVariables) :-
915 get_global_identifiers(IS), % Note: find identifier uses was called before global sets precompiled
916 ? get_operation_info(Event,SubstitutionInfo),
917 (memberchk(modifies(WrittenVariables),SubstitutionInfo)
918 -> sort(WrittenVariables,SWV), % normally not necessary; just to be sure
919 ord_subtract(SWV,IS,SortedWrittenVariables)
920 ; print(no_modifies_info(Event)),nl,fail),
921 (memberchk(reads(ReadVariables),SubstitutionInfo)
922 -> sort(ReadVariables,SWR),
923 ord_subtract(SWR,IS,SortedReadVariables)
924 ; debug_println(9,no_reads_info(Event)),fail). % happens currently in Event-B !
925 %% , print(read_write_set(Event,ReadVariables,WrittenVariables)),nl.
926
927 :- public b_get_operation_unchanged_variables_calc/2.
928 b_get_operation_unchanged_variables_calc(Event,UnchangedVariables) :-
929 b_get_machine_variables(TVars),
930 def_get_texpr_ids(TVars,V),
931 sort(V,SAllVars),
932 ? b_get_operation_normalized_read_write_info(Event,_,WrittenVars),
933 ord_subtract(SAllVars,WrittenVars,UnchangedVariables).
934
935
936
937 :- volatile b_get_operation_non_det_modifies/2.
938 :- dynamic b_get_operation_non_det_modifies/2.
939 :- public b_get_operation_non_det_modifies_calc/2.
940 :- use_module(b_read_write_info,[get_nondet_modified_vars/3]).
941 % determine which variables are non-deterministically written by an operation
942 % note: this can depend on the parameters, hence show_eventb_any_arguments is relevant
943 b_get_operation_non_det_modifies_calc(OpName,NonDetModifies) :-
944 ? b_get_machine_operation_for_animation(OpName,Results,Parameters,Body),
945 append(Results,Parameters,TLocalVars),
946 get_texpr_ids(TLocalVars,LocalVars),
947 get_nondet_modified_vars(Body,LocalVars,NonDetModifies).
948 b_get_operation_non_det_modifies_calc('$initialise_machine',NonDetModifies) :-
949 b_get_initialisation_from_machine(Body,_),
950 get_nondet_modified_vars(Body,[],NonDetModifies),debug_println(19,init_not_det_modifies(NonDetModifies)).
951
952
953 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
954
955
956 :- volatile b_get_all_used_filenames/1, b_get_main_filename/1, b_get_main_filenumber/1.
957 :- dynamic b_get_all_used_filenames/1. % can be used, e.g., for second argument of pos info field
958 :- dynamic b_get_main_filename/1. % can be used in above list; there is also specfile:currently_opened_file
959 :- dynamic b_get_main_filenumber/1. % the number of the main_file in the b_get_all_used_filenames list (useful for pos information)
960 b_get_all_used_filenames([]).
961
962 % add an additional filename and obtain its number
963 add_additional_filename(Filename,ResNr) :- functor(Filename,unknown,_),!,
964 format('Unknown additional filename: ~w~n',[Filename]),
965 ResNr = -1.
966 add_additional_filename(Filename,ResNr) :-
967 b_get_all_used_filenames(Fs),
968 ? nth1(Nr,Fs,Filename),!,
969 ResNr=Nr.
970 add_additional_filename(Filename,ResNr) :-
971 retract(b_get_all_used_filenames(Fs)),
972 length(Fs,Len),
973 append(Fs,[Filename],NewFs),
974 assert(b_get_all_used_filenames(NewFs)),
975 ResNr is Len+1,
976 format('Registering new filename ~w with number ~w~n',[Filename,ResNr]).
977
978 % add additional filename and add as default for parsercalls
979 set_additional_filename_as_parsing_default(Filename,NewNr,OldNr) :-
980 add_additional_filename(Filename,NewNr),
981 set_default_filenumber(NewNr,OldNr).
982 reset_filename_parsing_default(NewNr,OldNr) :- % reset default filenumber back
983 reset_default_filenumber(NewNr,OldNr).
984
985 b_load_machine_from_file(Filename) :- b_load_machine_from_file(Filename,[]).
986 b_load_machine_from_file(Filename,Options) :-
987 (debug_mode(on)
988 -> get_parser_version(Version),
989 format('Java Parser Version: ~w~n',[Version]) % used to be called unconditionally to be sure to catch error if java or BParser.jar not available; but now we do not want the Java startup time unless really necessary
990 ; true),
991 b_reset_filenames_and_numbers,
992 debug_stats(loading(Filename)),
993 catch(load_b_machine_as_term(Filename,Machine,Options),
994 parse_errors(Errors),
995 (add_all_perrors_in_context_of_used_filenames(Errors,parse_error,error),fail)),
996 b_load_machine_from_term(Filename,Machine).
997
998
999 % add parse errors in context of current machine and its filenames
1000 add_all_perrors_in_context_of_used_filenames(Errors,TypeOfError,ErrOrWarn) :- Errors\=[],
1001 b_get_all_used_filenames(Filenames), Filenames \= [],
1002 !,
1003 add_all_perrors(Errors,Filenames,TypeOfError,ErrOrWarn).
1004 add_all_perrors_in_context_of_used_filenames(Errors,TypeOfError,ErrOrWarn) :-
1005 (Errors=[] -> true ; debug_println(19,'Unable to obtain filenames for parse errors, probably preparse_error')),
1006 add_all_perrors(Errors,[],TypeOfError,ErrOrWarn).
1007
1008
1009 % a way to load .prob files directly
1010 b_load_machine_probfile(Filename) :- b_load_machine_probfile(Filename,[]).
1011 b_load_machine_probfile(Filename,Options) :- b_reset_filenames_and_numbers,
1012 load_b_machine_probfile_as_term(Filename,Options,Machine),
1013 Machine = complete_machine(_MainName,_,Filenames),
1014 Filenames = [BFilename|_], % assume first file is the main file
1015 b_load_machine_from_term(BFilename,Machine).
1016
1017
1018 % a way to load form a list of Facts which would be found in the .prob file
1019 b_load_machine_from_list_of_facts(Filename,ListOfFacts) :- % Filename only used below for find_main_file_name and later to find out about position infos if they are in the main file or not
1020 load_b_machine_list_of_facts_as_term(ListOfFacts,Machine),
1021 b_load_machine_from_term(Filename,Machine).
1022
1023
1024 b_reset_filenames_and_numbers :-
1025 set_all_used_filenames([]),
1026 retractall(b_get_main_filename(_)),
1027 retractall(b_get_main_filenumber(_)),
1028 retractall(b_filenumber(_,_,_,_)).
1029
1030 set_all_used_filenames(AllFilenames) :-
1031 retractall(b_get_all_used_filenames(_)),
1032 assertz(b_get_all_used_filenames(AllFilenames)).
1033
1034
1035 b_load_machine_from_term(Filename,complete_machine(MainName,Machines,Filenames)) :-
1036 b_reset_filenames_and_numbers, % call in case we call this predicate directly from outside
1037 !,
1038 assertz(b_get_main_filename(Filename)),
1039 set_all_used_filenames(Filenames),
1040 store_filenumbers(Filenames),
1041 (find_main_file_name(Nr,Filenames,Filename) -> assertz(b_get_main_filenumber(Nr))
1042 ; ajoin(['Main filename ', Filename, ' does not appear in filenames list: '],Msg),
1043 add_warning(bmachine,Msg,Filenames)
1044 ),
1045 %print(find_main_file_name(Nr,Filenames,Filename)),nl,
1046 check_valid_machine_name(MainName),
1047 debug_stats(analyse_hierarchy(MainName,Filename)),
1048 (rewrite_complete_machine(MainName,Machines,Machines1) -> true ; Machines1 = Machines),
1049 (analyse_hierarchy(MainName,Machines1)
1050 -> true ; add_error(b_load_machine,'Analyse Hierarchy failed'),fail),
1051 debug_stats(type_check(MainName,Filename)),
1052 b_set_machine(MainName,Machines1,Errors), % Typechecking
1053 debug_stats(checked_machine(MainName,Filename)),
1054 add_all_perrors(Errors,Filenames,type_error), % TO DO: use type_check as source as this may also generate warnings
1055 no_real_perror_occurred(Errors).
1056 b_load_machine_from_term(F,X) :- add_internal_error('Illegal machine: ',b_load_machine_from_term(F,X)),
1057 fail.
1058
1059 rewrite_complete_machine(MainName,[DefMachine],[NewMachine]) :-
1060 DefMachine=definition_file(Pos,Defs),
1061 %print(defs(Defs)),nl,
1062 % Generate virtual abstract machine when loading a .def DEFINITION file
1063 debug_println(19,creating_virtual_abstract_machine_for_definition_file),
1064 Header = machine_header(Pos,MainName,[]),
1065 NewMachine = abstract_machine(Pos,machine(Pos),Header,[Defs]).
1066
1067 check_valid_machine_name(Name) :- atom(Name),atom_codes(Name,Codes),
1068 invalid_chars(Invalid),
1069 ? (member(C,Codes),ord_member(C,Invalid)
1070 -> ajoin(['Machine name ', Name, ' contains illegal character: '],Msg),
1071 atom_codes(IChar,[C]),
1072 add_warning(bmachine,Msg,IChar)
1073 ; true),
1074 !.
1075 check_valid_machine_name(Name) :- add_internal_error('Illegal machine name:',check_valid_machine_name(Name)).
1076
1077 invalid_chars(".").
1078
1079 :- use_module(tools_matching,[codes_to_lower_case/2]).
1080 find_main_file_name(Nr,_Filenames,File) :- safe_absolute_file_name(File,AF),
1081 tools:get_modulename_filename(AF,TAF), tools:get_filename_extension(AF,ExtF),
1082 (ExtF = prob
1083 -> when(nonvar(EXT), member(EXT,[mch,ref,imp,tla,rmch])) % any machine extension is ok for .prob file
1084 ; EXT =ExtF),
1085 (b_filenumber(TAF,EXT,Nr,_) -> true
1086 ; atom_codes(TAF,TAFCodes), codes_to_lower_case(TAFCodes,Low),
1087 b_filenumber(TAF2,EXT,Nr,_),
1088 atom_codes(TAF2,C2), codes_to_lower_case(C2,Low)
1089 -> ajoin(['Case mis-match between main filename ',TAF,' and stored filename: '],Msg),
1090 % can happen on some file-systems which are case-insensitive or when transferring .prob files from one OS to another
1091 add_message(bmachine,Msg,TAF2)
1092 ).
1093
1094
1095
1096 % remember as facts all B filenames, their extension and their number
1097 :- volatile b_filenumber/4.
1098 :- dynamic b_filenumber/4.
1099 store_filenumbers(Filenames) :- retractall(b_filenumber(_,_,_,_)),
1100 store_filenumbers(Filenames,1).
1101 store_filenumbers([],_).
1102 store_filenumbers([H|T],Nr) :-
1103 safe_absolute_file_name(H,AbsFname),tools:get_modulename_filename(AbsFname,ModuleName),
1104 tools:get_filename_extension(AbsFname,ExtF),
1105 assertz(b_filenumber(ModuleName,ExtF,Nr,AbsFname)),
1106 debug_println(9,b_filenumber(ModuleName,ExtF,Nr,AbsFname)),
1107 N1 is Nr+1,
1108 store_filenumbers(T,N1).
1109
1110 portray_filenumbers :-
1111 format('~w : ~w : ~w (~w)~n',['Nr','ext','Name','Full path']),
1112 b_filenumber(ModuleName,ExtF,Nr,AbsFname),
1113 format('~w : ~w : ~w (~w)~n',[Nr,ExtF,ModuleName,AbsFname]),
1114 fail.
1115 portray_filenumbers.
1116
1117 :- use_module(tools,[same_file_name/2]).
1118 get_machine_file_number(Name,Ext,Nr,File) :-
1119 ? if(b_filenumber(Name,Ext,Nr,File),
1120 true,
1121 ? (b_filenumber(StoredName,Ext,Nr,File),
1122 % on Windows the capitalisation of the stored name maybe different from the name in machine
1123 same_file_name(Name,StoredName)
1124 )).
1125
1126
1127 :- use_module(tools,[safe_absolute_file_name/3, get_parent_directory/2]).
1128 % open a file relateive to the main B file
1129 b_absolute_file_name_relative_to_main_machine(File,AbsFileName) :-
1130 b_get_main_filename(MainFileName),
1131 get_parent_directory(MainFileName,Directory),
1132 % in Jupyter: MainFileName does not exist; SICStus then treats it as a directory
1133 safe_absolute_file_name(File,AbsFileName,[relative_to(Directory)]).
1134
1135 % call to clear all data stored for machine
1136 b_machine_clear :-
1137 b_machine_reset,
1138 b_reset_filenames_and_numbers.
1139
1140 :- use_module(btypechecker,[reset_typechecker/0]).
1141 :- use_module(b_global_sets,[b_clear_global_set_type_definitions/0]).
1142 :- use_module(bmachine_construction,[reset_bmachine_construction/0]).
1143 b_machine_reset :- % print(b_machine_reset),nl,
1144 retractall(machine(_,_)),
1145 retractall(additional_configuration_machine(_,_)),
1146 retractall(discharged_theorem(_,_,_)),
1147 retractall(discharged_guard_strengthening(_,_,_,_)),
1148 retractall(discharged(_,_,_)),
1149 retractall(wd_po(_,_,_)),
1150 retractall(also_discharged(_,_,_)),
1151 reset_temp_predicate,
1152 retractall(b_machine_additional_property(_)),
1153 reset_typechecker,
1154 b_clear_global_set_type_definitions,
1155 reset_bmachine_construction,
1156 startup_precompiled. % change so that error messages generated if we call them
1157
1158 :- use_module(eventhandling,[register_event_listener/3]).
1159 :- register_event_listener(clear_specification,b_machine_clear,
1160 'Reset bmachine facts.').
1161
1162 % :- use_module(library(random)).
1163 :- use_module(preferences,[get_preference/2]).
1164
1165
1166
1167
1168 % precompiled
1169 :- volatile b_machine_name/1.
1170 :- dynamic b_machine_name/1.
1171 :- public b_machine_name_calc/1.
1172 b_machine_name_calc(Name) :-
1173 get_full_b_machine(Name,_).
1174
1175 b_get_animated_sections(Sections) :-
1176 get_section_from_current_machine(meta,MetaInfos),
1177 ( member(animated_sections(Sections), MetaInfos) -> true
1178 ; add_error(bmachine,'No animated sections available'), fail).
1179
1180 :- volatile b_get_named_machine_set/3.
1181 :- dynamic b_get_named_machine_set/3.
1182 :- public b_get_named_machine_set_calc/3.
1183 ?b_get_named_machine_set(Set,Members) :- b_get_named_machine_set(Set,_,Members).
1184 % precompiled: all enumerated sets with their elements (all in atomic form)
1185 b_get_named_machine_set_calc(Set,TExpr,Members) :-
1186 get_section_from_current_machine(enumerated_sets,Sets),
1187 get_section_from_current_machine(enumerated_elements,Elems),
1188 get_texpr_id(TExpr,Set),
1189 get_texpr_type(TExpr,set(Type)),
1190 get_texpr_type(TElem,Type),
1191 ? member(TExpr,Sets),
1192 findall(E, (member(TElem,Elems), get_texpr_id(TElem,E)), Members).
1193
1194 :- volatile b_enumerated_sets_precompiled/0.
1195 :- dynamic b_enumerated_sets_precompiled/0.
1196 :- public b_enumerated_sets_precompiled_calc/0.
1197 b_enumerated_sets_precompiled_calc :-
1198 b_check_and_precompile_enumerated_sets.
1199
1200 :- volatile b_get_machine_set/2.
1201 :- dynamic b_get_machine_set/2.
1202 :- public b_get_machine_set_calc/2.
1203 ?b_get_machine_set(Set) :- b_get_machine_set(Set,_).
1204 % precompiled: all deferred and enumerated sets (in atomic form)
1205 b_get_machine_set_calc(Set,TExpr) :-
1206 get_section_from_current_machine(deferred_sets,Sets),
1207 get_texpr_id(TExpr,Set),
1208 ? member(TExpr,Sets).
1209 b_get_machine_set_calc(Set,TExpr) :-
1210 ? b_get_named_machine_set(Set,TExpr,_).
1211
1212 :- volatile b_get_machine_constants/1, b_get_machine_all_constants/1, b_get_machine_variables/1, b_get_machine_variables_in_original_order/1, b_is_constant/2, b_is_variable/2, b_get_constant_variable_description/2.
1213 :- dynamic b_get_machine_constants/1, b_get_machine_all_constants/1, b_get_machine_variables/1, b_get_machine_variables_in_original_order/1, b_is_constant/2, b_is_variable/2, b_get_constant_variable_description/2.
1214 b_machine_has_constants :- b_get_machine_constants([_|_]).
1215 :- public b_get_machine_all_constants_calc/1.
1216 % precompiled: all constants (abstract and concrete) in typed form
1217 b_get_machine_all_constants_calc(Csts) :-
1218 findall(C,get_multi_sections([abstract_constants,concrete_constants],C),Csts).
1219 :- public b_get_machine_constants_calc/1.
1220 % precompiled: all constants (abstract and concrete) in typed form; except for constant_represented inside global set
1221 b_get_machine_constants_calc(Csts) :-
1222 findall(C,
1223 (get_multi_sections([abstract_constants,concrete_constants],C),
1224 get_texpr_id(C,CID),
1225 \+ b_get_constant_represented_inside_global_set(CID,_)), % ignore constants detected as enumerated set elements
1226 Csts).
1227
1228 b_machine_has_variables :- b_get_machine_variables([_|_]).
1229
1230 :- public b_get_machine_variables_in_original_order_calc/1.
1231 % precompiled: all variables (abstract and concrete) in typed form
1232 b_get_machine_variables_in_original_order_calc(Vars) :-
1233 findall(V,get_multi_sections([abstract_variables,concrete_variables],V),Vars).
1234
1235 :- public b_get_machine_variables_calc/1.
1236 % get variables in order suitable for ord_member and optimized update storing
1237 b_get_machine_variables_calc(SVars) :-
1238 b_get_machine_variables_in_original_order(Vars),
1239 sort(Vars,SVars).
1240
1241 get_nr_of_machine_variables(Nr) :- b_get_machine_variables(L), length(L,Nr).
1242 get_nr_of_machine_constants(Nr) :- b_get_machine_constants(L), length(L,Nr).
1243
1244 ?b_is_constant(C) :- b_is_constant(C,_).
1245 :- public b_is_constant_calc/2.
1246 % precompiled: all constants (abstract and concrete) in atomic form
1247 b_is_constant_calc(Cst,Type) :-
1248 b_get_machine_constants(Constants),
1249 get_texpr_id(Term,Cst),
1250 get_texpr_type(Term,Type),
1251 ? member(Term,Constants).
1252 b_is_variable(V) :- b_is_variable(V,_).
1253 :- public b_is_variable_calc/2.
1254 % precompiled: all variables (abstract and concrete) in atomic form
1255 b_is_variable_calc(Var,Type) :-
1256 b_get_machine_variables(Vars), % b_get_machine_variables_in_original_order
1257 get_texpr_id(Term,Var),
1258 get_texpr_type(Term,Type),
1259 ? member(Term,Vars).
1260 % look up elements in several sections of the machine
1261 get_multi_sections(Sections,Elem) :-
1262 ? member(Section,Sections),
1263 get_section_from_current_machine(Section,List),
1264 ? member(Elem,List).
1265
1266 :- public b_get_constant_variable_description_calc/2.
1267 % get value of description pragmas @desc for variables and constants:
1268 b_get_constant_variable_description_calc(ID,Desc) :-
1269 (b_get_machine_constants(L) ; b_get_machine_variables(L)),
1270 get_texpr_id(Term,ID),
1271 ? member(Term,L),
1272 get_texpr_description(Term,TDesc),
1273 (simplify_desc(TDesc,Desc) -> true ; TDesc=Desc).
1274
1275 :- use_module(probsrc(tools_strings), [atom_prefix/2]).
1276 simplify_desc(Compound,R) :- compound(Compound),!,
1277 add_error(simplify_desc,'Non-atomic description: ',Compound),
1278 R=Compound.
1279 simplify_desc(memoize,memo).
1280 simplify_desc(memoise,memo).
1281 simplify_desc('"memoize"',memo).
1282 simplify_desc('"memoise"',memo).
1283 simplify_desc('"expand"',expand).
1284 simplify_desc('"memo"',memo). % allow /*@desc "memo" */
1285 simplify_desc(Atom,memo) :- atom_prefix('"memo ',Atom). % allow /*@desc "memo ...additional text" */
1286
1287 % check if a constant or variable is annotated for memoization:
1288 constant_variable_marked_as_memo(ID) :- b_get_constant_variable_description(ID,memo).
1289
1290 % check if a constant or variable is annotated for expansion using @desc expand
1291 constant_variable_marked_as_expand(ID) :- b_get_constant_variable_description(ID,EXPAND), EXPAND=expand.
1292
1293
1294 :- volatile b_get_invariant_from_machine/1,
1295 b_get_linking_invariant_from_machine/1,
1296 b_get_properties_from_machine/1,
1297 b_get_static_assertions_from_machine/1,
1298 b_extract_values_clause_assignment/3,
1299 b_get_unproven_static_assertions_from_machine/1,
1300 b_get_dynamic_assertions_from_machine/1,
1301 b_get_unproven_dynamic_assertions_from_machine/1,
1302 b_get_assertions_from_main_machine/2,
1303 b_get_initialisation_from_machine/2,
1304 b_get_machine_operation/6,b_top_level_operation/1,
1305 b_get_machine_operation_for_animation/7,
1306 b_is_operation_name/1,
1307 b_get_promoted_machine_operations/1.
1308 :- dynamic b_get_invariant_from_machine/1,
1309 b_get_linking_invariant_from_machine/1,
1310 b_get_properties_from_machine/1,
1311 b_get_static_assertions_from_machine/1,
1312 b_extract_values_clause_assignment/3,
1313 b_get_unproven_static_assertions_from_machine/1,
1314 b_get_dynamic_assertions_from_machine/1,
1315 b_get_unproven_dynamic_assertions_from_machine/1,
1316 b_get_assertions_from_main_machine/2,
1317 b_get_initialisation_from_machine/2,
1318 b_get_machine_operation/6,b_top_level_operation/1,
1319 b_get_machine_operation_for_animation/7,
1320 b_is_operation_name/1,
1321 b_get_promoted_machine_operations/1.
1322
1323 :- public b_get_invariant_from_machine_calc/1.
1324 % precompiled: typed invariant (a predicate)
1325 b_get_invariant_from_machine_calc(Inv) :-
1326 get_section_from_current_machine(invariant,Inv).
1327
1328 :- public b_get_linking_invariant_from_machine_calc/1.
1329 % precompiled: typed linking invariant (a predicate)
1330 b_get_linking_invariant_from_machine_calc(Inv) :-
1331 get_section_from_current_machine(linking_invariant,Inv).
1332
1333 :- public b_get_properties_from_machine_calc/1.
1334 % precompiled: typed properties (a predicate)
1335 b_get_properties_from_machine_calc(SortedProp) :-
1336 get_section_from_current_machine(properties,Prop),
1337 (sort_properties(Prop,SortedProp) -> true %(Prop=SortedProp->true ; print(sorted(SortedProp)))
1338 ; add_error(sort_properties,'sort_properties failed: ',Prop),
1339 SortedProp=Prop).
1340
1341 sort_properties(Prop,SortedProp) :- % print(sort_properties),nl,statistics(runtime, [R1,_]),
1342 weigh_properties(Prop,1,_,[],SProp),
1343 % statistics(runtime, [R2,_]), RDiff is R2-R1,print(done_weigh(RDiff,SProp)),nl,
1344 sort(SProp,SSProp),
1345 % statistics(runtime, [R3,_]), RDiff2 is R3-R2,print(done_sort(RDiff2)),nl,
1346 remove_weights(SSProp,PropList),
1347 conjunct_predicates(PropList,SortedProp).
1348 % translate:print_bexpr(SortedProp).
1349
1350 remove_weights([],[]).
1351 remove_weights([prop(_W,_Nr,E)|T],[E|RT]) :- remove_weights(T,RT).
1352
1353 weigh_properties(Pred,Nr,ONr,InL,OutL) :-
1354 decompose_conjunct(Pred,LHS,RHS), % will propagate labels down to conjuncts LHS,RHS
1355 !,
1356 weigh_properties(LHS,Nr,N1,InL,L2),
1357 weigh_properties(RHS,N1,ONr,L2,OutL).
1358 weigh_properties(b(Pred,S,I),Nr,N1,T,[prop(Weight,Nr,b(Pred,S,I))|T]) :-
1359 N1 is Nr+1,
1360 ? (member(contains_wd_condition,I) -> Weight=32000 % do not move properties with WD info
1361 ; weigh_properties2(Pred,Weight)).
1362 % translate:print_bexpr(b(Pred,S,I)), print(' WEIGHT: '), print(Weight),nl
1363
1364 weigh_properties2(truth,W) :- !, W=1.
1365 weigh_properties2(falsity,W) :- !, W=1.
1366 weigh_properties2(equal(L,R),W) :- weigh_term(L,W1), !,
1367 ( weigh_term(R,W2) -> W is W1*W2
1368 ; W is 3200).
1369 % ; W is W1*20). %causes issue with ParityFunction test
1370 %weigh_properties2(equal(_,R),W) :- weigh_term(R,W2), !, W is W2*20.
1371 weigh_properties2(SOp,W) :- comparison(SOp,L,R),!,
1372 ( (weigh_term(L,W1), weigh_term(R,W2))
1373 -> W is 7+W1+W2 % try and give things like x>10 priority over x>y (to overcome CLP(FD) limitations)
1374 ; W=10).
1375 weigh_properties2(partition(LHS,RHS),W) :- weigh_term(LHS,W1), l_weigh_term(RHS,W2), !, W is W1*W2.
1376 ?weigh_properties2(not_equal(L,R),W) :- ((id(L),empty(R)) ; (id(R),empty(L))),!, W=1.
1377 weigh_properties2(not_equal(L,R),W) :- weigh_term(L,W1), weigh_term(R,W2),!,
1378 W is 20+W1*W2.
1379 weigh_properties2(_Rest,W) :- W=32000.
1380
1381 comparison(less(L,R),L,R).
1382 comparison(less_equal(L,R),L,R).
1383 comparison(greater(L,R),L,R).
1384 comparison(greater_equal(L,R),L,R).
1385
1386
1387 id(b(identifier(_),_,_)).
1388 empty(b(empty_set,_,_)).
1389 empty(b(empty_sequence,_,_)).
1390
1391 l_weigh_term([],0).
1392 l_weigh_term([H|T],R) :- l_weigh_term(T,TR), weigh_term(H,TH), R is TH+TR.
1393
1394 weigh_term(b(T,_,_),R) :- (weigh_term2(T,R) -> true ; fail). %R=20).
1395
1396 weigh_term2(value(_),1).
1397 weigh_term2(boolean_true,1).
1398 weigh_term2(boolean_false,1).
1399 weigh_term2(empty_set,1).
1400 weigh_term2(empty_sequence,1).
1401 weigh_term2(integer(_),1).
1402 weigh_term2(min_int,1).
1403 weigh_term2(max_int,1).
1404 weigh_term2(string(_),1).
1405 weigh_term2(real(_),1).
1406 weigh_term2(bool_set,2).
1407 weigh_term2(identifier(_),2).
1408 weigh_term2(set_extension(_),3).
1409 weigh_term2(integer_set(_),3).
1410 weigh_term2(interval(L,R),W) :- weigh_term(L,WL), weigh_term(R,WR), W is WL*WR.
1411
1412
1413
1414 b_machine_has_constants_or_properties :-
1415 (b_machine_has_constants -> true
1416 ; (b_get_properties_from_machine(Prop)), \+ is_truth(Prop)).
1417
1418 b_get_machine_operation_parameter_types(OpName,ParTypes) :-
1419 ? b_get_machine_operation_typed_parameters(OpName,Parameters),
1420 maplist(get_texpr_type,Parameters,ParTypes).
1421
1422 b_get_machine_operation_typed_parameters(Operation,Res) :-
1423 ? b_get_machine_operation_typed_parameters3(Operation,real_paras_only,Res).
1424 b_get_machine_operation_typed_parameters_for_animation(Operation,Res) :-
1425 b_get_machine_operation_typed_parameters3(Operation,for_animation,Res).
1426
1427 b_get_machine_operation_typed_parameters3(Operation,ForAnim,Res) :-
1428 ? if(b_get_machine_operation_typed_parameters_aux(Operation,ForAnim,Paras),Res=Paras,
1429 (add_internal_error('Cannot get paras: ',b_get_machine_operation_typed_parameters(Operation,ForAnim,Res)),fail)).
1430 % also recognises SETUP_CONSTANTS & INITIALISE_MACHINE
1431 b_get_machine_operation_typed_parameters_aux('$setup_constants',_,Constants) :-
1432 b_machine_has_constants_or_properties,
1433 b_get_machine_constants(Constants).
1434 b_get_machine_operation_typed_parameters_aux('$initialise_machine',_,Variables) :-
1435 b_get_machine_variables(Variables).
1436 b_get_machine_operation_typed_parameters_aux(OpName,real_paras_only,Parameters) :-
1437 b_get_machine_operation(OpName,_R,Parameters,_Body,_OType,_OpPos).
1438 b_get_machine_operation_typed_parameters_aux(OpName,for_animation,Parameters) :-
1439 b_get_machine_operation_for_animation(OpName,_R,Parameters,_Body).
1440
1441 b_get_machine_operation_parameter_names(OpName,ParaNames) :-
1442 b_get_machine_operation_parameter_names(OpName,real_paras_only,ParaNames).
1443 b_get_machine_operation_parameter_names_for_animation(OpName,ParaNames) :-
1444 b_get_machine_operation_parameter_names(OpName,for_animation,ParaNames).
1445
1446 b_get_machine_operation_parameter_names('@INITIALISATION',ForAnim,ParaNames) :- % for Tcl/Tk
1447 b_get_machine_operation_parameter_names('$initialise_machine',ForAnim,ParaNames).
1448 b_get_machine_operation_parameter_names('@PROPERTIES',ForAnim,ParaNames) :- % for Tcl/Tk
1449 b_get_machine_operation_parameter_names('$setup_constants',ForAnim,ParaNames).
1450 b_get_machine_operation_parameter_names(OpName,ForAnim,ParaNames) :-
1451 b_get_machine_operation_typed_parameters3(OpName,ForAnim,Parameters),
1452 get_texpr_ids(Parameters,ParaNames).
1453
1454 b_get_machine_operation_typed_results('$setup_constants',[]).
1455 b_get_machine_operation_typed_results('$initialise_machine',[]).
1456 b_get_machine_operation_typed_results(OpName,Results) :-
1457 b_get_machine_operation(OpName,Results,_Parameters,_Body,_OType,_OpPos).
1458
1459 b_get_machine_operation_result_names('$setup_constants',[]).
1460 b_get_machine_operation_result_names('$initialise_machine',[]).
1461 b_get_machine_operation_result_names(OpName,ResultNames) :-
1462 b_get_machine_operation(OpName,Results,_Parameters,_Body,_OType,_OpPos),
1463 get_texpr_ids(Results,ResultNames).
1464
1465 b_get_machine_operation(Name,Results,Parameters,Body) :-
1466 ? b_get_machine_operation(Name,Results,Parameters,Body,_OType,_OpPos).
1467
1468 :- public b_get_assertions_from_main_machine_calc/2.
1469 b_get_assertions_from_main_machine_calc(static,FProp) :-
1470 ((b_get_static_assertions_from_machine(Prop),
1471 exclude(is_not_main_assertion,Prop,FProp)) -> true
1472 ; add_error(bmachine,'b_get_assertions_from_main_machine_calc static fails'), FProp=[]).
1473 b_get_assertions_from_main_machine_calc(dynamic,FProp) :-
1474 ((b_get_dynamic_assertions_from_machine(Prop),
1475 exclude(is_not_main_assertion,Prop,FProp)) -> true
1476 ; add_error(bmachine,'b_get_assertions_from_main_machine_calc dynamic fails'), FProp=[]).
1477 is_not_main_assertion(Assertion) :-
1478 get_texpr_pos(Assertion,Pos),
1479 error_manager:position_is_not_in_main_file(Pos).
1480
1481 % get nr of assertions and nr of main assertions for static/dynamic
1482 b_get_assertion_count(StaticOrDynamic,NrAll,NrMain) :-
1483 ? b_get_assertions(all,StaticOrDynamic,A), length(A,NrAll),
1484 b_get_assertions_from_main_machine(StaticOrDynamic,MA),length(MA,NrMain).
1485
1486 b_get_assertions(main,Mode,Ass) :- !,
1487 b_get_assertions_from_main_machine(Mode,Ass).
1488 b_get_assertions(specific(Label),Mode,LabelAss) :- !,
1489 ? b_get_assertions(all,Mode,Ass),
1490 %maplist(get_texpr_label,Ass,Labels), print(labels(Labels)),nl,
1491 include(has_label(Label),Ass,LabelAss),
1492 (LabelAss=[] -> ajoin(['No ',Mode,' assertion has label: '],Msg),
1493 add_warning(b_get_assertions,Msg,Label) ; true).
1494 b_get_assertions(_,static,Ass) :- b_get_static_assertions_from_machine(Ass).
1495 b_get_assertions(_,dynamic,Ass) :- b_get_dynamic_assertions_from_machine(Ass).
1496 b_main_machine_has_no_assertions :-
1497 b_get_assertions_from_main_machine(static,[]),
1498 b_get_assertions_from_main_machine(dynamic,[]).
1499
1500
1501 %has_label(Label,Expr) :- get_texpr_label(Expr,Label1), format('Labels ~w =? ~w~n',[Label1,Label]), fail.
1502 has_label(Label,Expr) :- get_texpr_label(Expr,Label).
1503
1504 :- public b_get_static_assertions_from_machine_calc/1.
1505 % precompiled: typed assertions (a list of predicates)
1506 b_get_static_assertions_from_machine_calc(Prop) :-
1507 get_section_from_current_machine(assertions,Prop1),
1508 exclude(predicate_uses_variables,Prop1,Prop),!.
1509 b_get_static_assertions_from_machine_calc(Prop) :-
1510 add_error(bmachine,'b_get_static_assertions_from_machine_calc fails'), Prop=[].
1511
1512 :- dynamic b_machine_has_static_assertions/0.
1513 :- public b_machine_has_static_assertions_calc/0.
1514 b_machine_has_static_assertions_calc :-
1515 b_get_static_assertions_from_machine([_|_]).
1516
1517 :- public b_get_unproven_static_assertions_from_machine_calc/1.
1518 b_get_unproven_static_assertions_from_machine_calc(FAssertions) :-
1519 b_get_static_assertions_from_machine(Assertions),
1520 filter_out_proven_assertions(Assertions,FAssertions),!.
1521 b_get_unproven_static_assertions_from_machine_calc(Prop) :-
1522 add_error(bmachine,'b_get_unproven_static_assertions_from_machine_calc fails'), Prop=[].
1523
1524 filter_out_proven_assertions([],[]).
1525 filter_out_proven_assertions([A1|T],R) :-
1526 (is_discharged_assertion(A1)
1527 -> R = TR %, print('Proven: '), translate:print_bexpr(A1),nl
1528 ; R = [A1|TR]),
1529 filter_out_proven_assertions(T,TR).
1530
1531 :- public b_get_dynamic_assertions_from_machine_calc/1.
1532 b_get_dynamic_assertions_from_machine_calc(Prop) :-
1533 get_section_from_current_machine(assertions,Prop1),
1534 include(predicate_uses_variables,Prop1,Prop),!.
1535 b_get_dynamic_assertions_from_machine_calc(Prop) :-
1536 add_error(bmachine,'b_get_dynamic_assertions_from_machine_calc fails'), Prop=[].
1537
1538
1539 :- dynamic b_machine_has_dynamic_assertions/0.
1540 :- public b_machine_has_dynamic_assertions_calc/0.
1541 b_machine_has_dynamic_assertions_calc :-
1542 b_get_dynamic_assertions_from_machine([_|_]).
1543
1544 b_machine_has_assertions :- (b_machine_has_static_assertions -> true ; b_machine_has_dynamic_assertions).
1545
1546 b_machine_has_unproven_assertions :-
1547 b_get_unproven_dynamic_assertions_from_machine([_|_]) -> true
1548 ; b_get_unproven_static_assertions_from_machine([_|_]).
1549
1550
1551 get_all_assertions_from_machine(Assertions) :-
1552 findall(A,((SD=static;SD=dynamic),get_assertions_from_machine(SD,SS),member(A,SS)),Assertions).
1553
1554 get_assertions_from_machine(Type,Assertions) :-
1555 ( Type=(dynamic) ->
1556 (get_preference(use_po,true)
1557 -> b_get_unproven_dynamic_assertions_from_machine(Assertions)
1558 ; b_get_dynamic_assertions_from_machine(Assertions)
1559 )
1560 ; Type=(static) ->
1561 (get_preference(use_po,true)
1562 -> b_get_unproven_static_assertions_from_machine(Assertions)
1563 ; b_get_static_assertions_from_machine(Assertions)
1564 )
1565 ),
1566 Assertions = [_|_].
1567
1568 :- public b_get_unproven_dynamic_assertions_from_machine_calc/1.
1569 b_get_unproven_dynamic_assertions_from_machine_calc(FAssertions) :-
1570 b_get_dynamic_assertions_from_machine(Assertions),
1571 filter_out_proven_assertions(Assertions,FAssertions),!.
1572 b_get_unproven_dynamic_assertions_from_machine_calc(Prop) :-
1573 add_error(bmachine,'b_get_unproven_dynamic_assertions_from_machine_calc fails'), Prop=[].
1574
1575 predicate_uses_variables(Pred) :-
1576 b_get_machine_variables(Vars),
1577 get_texpr_ids(Vars,Ids),
1578 list_to_ord_set(Ids,OrdVars),
1579 find_identifier_uses(Pred,[],UsedVars),
1580 list_to_ord_set(UsedVars,OrdUsedVars),
1581 ord_intersect(OrdVars,OrdUsedVars).
1582
1583 :- public b_get_initialisation_from_machine_calc/2.
1584 % precompiled: typed initialisation (a substitution)
1585 b_get_initialisation_from_machine_calc(Init,OType) :-
1586 get_section_from_current_machine(initialisation,Init),
1587 ( get_texpr_expr(Init,rlevent(_Name,_Section,_Status,Params,_Guard,_Theorems,_Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents)) ->
1588 get_operation_type(Init,'INITIALISATION',Params,OType)
1589 ;
1590 OType = classic).
1591 % precompiled: operations, Name is in atomic form, Results and Parameters are lists
1592 % of typed identifiers, Body is a typed substitution
1593
1594 b_safe_get_initialisation_from_machine(Init,OType) :-
1595 if(b_get_initialisation_from_machine(Init,OType),true,
1596 add_error(bmachine,'Machine has no INITIALISATION clause')).
1597
1598
1599 :- volatile b_machine_operation_names_in_reverse_order/1.
1600 :- dynamic b_machine_operation_names_in_reverse_order/1.
1601 % a list of operation names in reverse order; this way we can randomize the
1602 % generation of the successor states
1603 precompile_operation_names_in_reverse_order :-
1604 retractall(b_machine_operation_names_in_reverse_order(_)),
1605 ? b_get_machine_operation(Name,_Results,_Parameters,_Body,_OType,_OpPos),
1606 asserta(b_machine_operation_names_in_reverse_order(Name)),
1607 fail.
1608 precompile_operation_names_in_reverse_order.
1609
1610 :- use_module(specfile, [animation_minor_mode/1, classical_b_mode/0]).
1611 :- use_module(extrasrc(b_expression_sharing),[cse_optimize_substitution/2]).
1612 :- public b_get_machine_operation_calc/6.
1613 b_get_machine_operation_calc(Name,Results,Parameters,NewBody,OType,OpPos) :-
1614 %well_def_analyser:get_hyps_for_top_level_operations([],Hyps),
1615 is_ground(Name,NameGround),
1616 get_section_from_current_machine(operation_bodies,Ops),
1617 get_texpr_expr(Op,operation(TId,Results,Parameters,Body)),
1618 get_texpr_id(TId,op(Name)),
1619 ? member(Op,Ops),
1620 % remove choicepoints when name was ground
1621 (NameGround==ground -> !; true),
1622 get_operation_type(Op,Name,Parameters,OType),
1623 (get_texpr_pos(TId,OpPos) -> true ; OpPos = unknown),
1624 ( get_preference(use_common_subexpression_also_for_substitutions,true),
1625 get_preference(use_common_subexpression_elimination,true),
1626 \+ animation_minor_mode(eventb) % CSE_SUBST not yet available for Event-B
1627 -> debug_println(19,applying_cse_to(Name)),
1628 cse_optimize_substitution(Body,OpBody)
1629 ; OpBody = Body),
1630 NewBody=OpBody.
1631
1632 b_get_machine_operation_signature(Name,SignatureStr) :-
1633 b_get_machine_operation_calc(Name,Results,Parameters,_,_,_),
1634 get_texpr_ids(Parameters,PIds),
1635 ajoin_with_sep(PIds,',',Args),
1636 (Results = []
1637 -> ajoin([Name,'(',Args,')'],SignatureStr)
1638 ; get_texpr_ids(Results,RIds),
1639 ajoin_with_sep(RIds,',',Res),
1640 ajoin([Res,'<--',Name,'(',Args,')'],SignatureStr)
1641 ).
1642
1643 %well_def_analyser:transform_machine_operation(Name,Results,Parameters,OpBody,Hyps,[create_not_discharged_msg(message)],NewBody).
1644 get_operation_type([],_Name,_Parameters,classic).
1645 get_operation_type(Op,Name,Parameters,OType) :-
1646 get_texpr_info(Op,Info),
1647 ? ( member(eventb(_),Info) ->
1648 OType=eventb_operation(SortedChangeSet,Ps,OpPattern),
1649 ? member(modifies(ChangeSet),Info),!,
1650 sort(ChangeSet,SortedChangeSet), % maybe not necessary ?
1651 same_length(Parameters,Ps),
1652 OpPattern =.. [Name|Ps]
1653 ;
1654 OType=classic).
1655
1656 :- volatile get_operation_info/2, get_operation_description_template_expr/2.
1657 :- dynamic get_operation_info/2, get_operation_description_template_expr/2.
1658 :- public get_operation_info_calc/2, get_operation_description_template_expr_calc/2.
1659 % precompiled: operation infos
1660 get_operation_info_calc(OpName,Info1) :-
1661 get_section_from_current_machine(operation_bodies,Ops),
1662 create_texpr(operation(TId,_Results,_Parameters,_Body),_,Info1,TOp), % rlevent()
1663 get_texpr_id(TId,op(OpName)),
1664 ? member(TOp,Ops).
1665
1666 b_get_operation_description(OpName,Desc) :-
1667 get_operation_info(OpName,Infos),
1668 member(description(Desc),Infos).
1669
1670 % get a typed string expression that can compute an operation description (based on vars, paras, ...)
1671 get_operation_description_template_expr_calc(OpName,TemplateStringExpr) :-
1672 get_error_context(Context),
1673 ? call_cleanup(get_op_desc_template_expr_calc2(OpName,TemplateStringExpr),restore_error_context(Context)).
1674
1675 get_op_desc_template_expr_calc2(OpName,TemplateStringExpr) :-
1676 ? get_operation_info(OpName,Infos),
1677 member(description(Desc),Infos),
1678 (member(description_position(OpPos),Infos)
1679 -> true
1680 ; get_info_pos(Infos,OpPos)
1681 % Unfortunately this is the entire position from beginning of operation to desc label */
1682 ),
1683 atom(Desc),
1684 set_error_context(checking_context('Checking description template for operation: ',OpName)),
1685 ? transform_string_template(Desc,OpPos,RawTemplateExpr),
1686 %translate:print_raw_bexpr(RawTemplateExpr),nl,
1687 GenerateParseErrors=gen_parse_warnings_for(OpPos),
1688 get_machine_operation_typing_scope(OpName,Scope,[]),
1689 % it could be that the template uses abstract variables that are no longer accessible
1690 b_type_only(RawTemplateExpr,Scope,Type,TemplateStringExpr,GenerateParseErrors),
1691 (debug_mode(off) -> true
1692 ; format('Template description expression for operation ~w:~n ',[OpName]),
1693 translate:print_bexpr(TemplateStringExpr),nl
1694 ),
1695 (Type=string -> true ; add_internal_error('Not string type:',Type)).
1696
1697
1698 :- public b_top_level_operation_calc/1.
1699 % precompiled: operation names (in atomic form) of top-level operations (promoted operations)
1700 b_top_level_operation_calc(Name) :-
1701 is_ground(Name,NameGround),
1702 get_section_from_current_machine(promoted,Promoted),
1703 get_texpr_id(TId,op(Name)),
1704 ? member(TId,Promoted),
1705 (NameGround==ground -> !; true).
1706 :- public b_get_promoted_machine_operations_calc/1.
1707 b_get_promoted_machine_operations_calc(Ops) :-
1708 get_section_from_current_machine(promoted,Ops).
1709
1710 :- volatile b_top_level_feasible_operation/1.
1711 :- dynamic b_top_level_feasible_operation/1.
1712 :- public b_top_level_feasible_operation_calc/1.
1713 % filter out operations which are commented out statically by using 1=2 or similar in guard
1714 ?b_top_level_feasible_operation_calc(Name) :- b_top_level_operation(Name),
1715 b_get_machine_operation(Name,_,_,Body,_,_Pos),
1716 \+ infeasible_tsubst(Body).
1717 % TO DO: investigate how to link up with cbc feasibility analysis
1718
1719 infeasible_tsubst(b(S,_,_)) :- infeasible_subst(S).
1720 infeasible_subst(precondition(G,_)) :- is_falsity(G).
1721 infeasible_subst(select([b(select_when(G,_),_,_)])) :- is_falsity(G).
1722 infeasible_subst(any(_,G,_)) :- is_falsity(G).
1723
1724 % this succeeds not just for top-level operations
1725 %b_is_operation_name(Name) :- b_get_machine_operation(Name,_,_,_,_,_). is slower
1726 :- public b_is_operation_name_calc/1.
1727 b_is_operation_name_calc(Name) :-
1728 ? b_get_machine_operation(Name,_,_,_,_,_).
1729
1730 b_get_operation_pos(Name,Pos) :-
1731 ? b_get_machine_operation(Name,_,_,_,_,Pos).
1732
1733 b_get_operation_variant(Name,ConvOrAnt,Variant) :-
1734 ? b_get_machine_operation(Name,_,_,TBody),
1735 get_texpr_expr(TBody,Body),
1736 Body = rlevent(Name,_Section,Status,
1737 _Params,_Guard,_Theorems,_Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents),
1738 % TO DO: look maybe higher up in refinement hierarchy
1739 get_texpr_expr(Status,S),
1740 functor(S,ConvOrAnt,1),
1741 (ConvOrAnt = convergent ; ConvOrAnt = anticipated),
1742 arg(1,S,Variant).
1743
1744 b_machine_has_operations :-
1745 (b_is_operation_name(_) -> true).
1746 % -----------------------------
1747
1748
1749 % the names of definitions which have a given Prefix,
1750 % Type is expression or predicate, Name is an atomic name
1751 b_definition_prefixed(Type,Prefix,Suffix,Name,Pos) :-
1752 safe_atom_chars(Prefix,PrefixChars,b_definition_prefixed1),
1753 append(PrefixChars,SuffixChars,FullChars),
1754 (ground(Suffix) -> safe_atom_chars(Suffix,SuffixChars,b_definition_prefixed2),
1755 safe_atom_chars(Name,FullChars,b_definition_prefixed3)
1756 ; true),
1757 ? b_get_definition_with_pos(Name,Type,Pos,_,_,_),
1758 safe_atom_chars(Name,FullChars,b_definition_prefixed4),
1759 safe_atom_chars(Suffix,SuffixChars,b_definition_prefixed5).
1760
1761 % TODO: should we also look for theory direct definitions for Event-B models?
1762 % :- use_module(bmachine_eventb,[stored_operator_direct_definition/8]).
1763 % stored_operator_direct_definition(Id,_Proj,_Thy,Parameters,_Def,_WD,_TP,_Kind),
1764 % or add auxiliary definition files for Event-B models
1765
1766
1767 % get definitions in alphabetical order of name:
1768 % predictable order is relevant for SVG_OBJECTS to know which objects are on top of each other
1769 b_sorted_b_definition_prefixed(Type,DEFPREFIX,DefName,DefPos) :-
1770 (b_or_z_mode; xtl_mode), % allow XTL mode for VisB definition files; TODO: maybe allow other non-B modes (mainly for VisB)
1771 % fail silently if we are not B/Z/TLA+/Alloy mode as machine not pre-compiled
1772 sorted_list_of_defs(Type,DEFPREFIX,SortedList),
1773 ? member(def(DefName,DefPos),SortedList).
1774 sorted_list_of_defs(Type,DEFPREFIX,SortedList) :-
1775 findall(def(DefName,DefPos),
1776 b_definition_prefixed(Type,DEFPREFIX,_Tail,DefName,DefPos),
1777 List),
1778 sort(List,SortedList).
1779
1780 :- use_module(bmachine_construction,[type_open_formula/8]).
1781 type_check_definitions :-
1782 temporary_set_preference(allow_untyped_identifiers,true_with_string_type,CHNG), % we may not have all identifiers visible
1783 get_error_context(Context),
1784 call_cleanup(type_check_definitions2,restore_error_context(Context)),
1785 reset_temporary_preference(allow_untyped_identifiers,CHNG).
1786 type_check_definitions2 :-
1787 get_preference(type_check_definitions,true),
1788 full_b_machine(Machine),
1789 ? b_get_definition_with_pos(Name,Type,DefPos,Args,RawExpr,_Deps),
1790 % TO DO: do not re-analyse definitions already analysed for ANIMATION_FUNCTION,...
1791 (Type = predicate ; Type=expression), % can we also allow substitutions ?
1792 debug_format(9,'Type checking DEFINITION ~w~n',[Name]),
1793 set_error_context(checking_context('Type checking DEFINITION: ',Name)),
1794 Scope = [variables], % prob_ids(visible),
1795 %type_with_errors(RawExpr,Scope,_,_TExpr),
1796 AllowNewIds=true,
1797 % TO DO: improve solution below, e.g., delete Args from visible variables or rename Args to fresh ids!
1798 (Args=[] -> RawExpr2=RawExpr
1799 ; Type=predicate -> RawExpr2 = exists(none,Args,conjunct(none,truth(none),RawExpr)) % wrap Args into quantifier, avoid clash with variables,... ; conjunct used to avoid warnings about body of exists
1800 ; RawExpr2=exists(none,Args,equal(none,RawExpr,RawExpr)) % TODO: better solution to avoid duplicating RawExpr
1801 ),
1802 ? (type_open_formula(RawExpr2,Scope,AllowNewIds,Machine,FType,Identifiers,_TPred,Errors) % maybe no need to run cleanup?
1803 -> Errors = [_|_],
1804 format('Error for DEFINITION ~w of type ~w over identifiers ~w~n',[Name,FType,Identifiers]),
1805 add_all_perrors_in_context_of_used_filenames(Errors,definition_type_error,error),
1806 fail
1807 % TO DO: check for local clashes?
1808 ; add_error(bmachine,'Type checking DEFINITION failed: ',Name,DefPos)
1809 ),
1810 fail.
1811 type_check_definitions2 :- debug_format(9,'Finished type checking DEFINITIONs~n',[]).
1812
1813 b_get_definition(Name,DefType,Args,RawExpr,Deps) :-
1814 ? b_get_definition_with_pos(Name,DefType,_DefPos,Args,RawExpr,Deps).
1815
1816 :- public portray_defs/0. % debugging utility
1817 portray_defs :-
1818 b_get_definition_with_pos(Name,DefType,DefPos,_Args,_RawExpr,_),
1819 add_message(bmachine,'DEFINITION: ',Name:DefType,DefPos),fail.
1820 portray_defs.
1821
1822 b_get_definition_with_pos(Name,DefType,DefPos,Args,RawExpr,Deps) :- %print(get_def(Name)),nl,
1823 get_section_from_current_machine(definitions,Defs),
1824 ? member(definition_decl(Name,DefType,DefPos,Args,RawExpr,Deps),Defs).
1825 b_get_definition_with_pos(Name,DefType,DefPos,Args,RawExpr,Deps) :- %print(get_def(Name)),nl,
1826 additional_configuration_machine(_MchName,Mch),
1827 get_section(definitions,Mch,Defs),
1828 member(definition_decl(Name,DefType,DefPos,Args,RawExpr,Deps),Defs).
1829 %flush_output,write(additional_def(Name,DefType,Deps)),nl,flush_output.
1830
1831
1832 :- use_module(input_syntax_tree,[raw_update_file_nrs/3]).
1833 :- volatile additional_configuration_machine/2.
1834 :- dynamic additional_configuration_machine/2.
1835 % load an additional definitions file for ViB configuration or CUSTOM_GRAPH features
1836 % useful for Event-B, ... models
1837 b_load_additional_definitions_file(File) :-
1838 Options=[],
1839 catch(load_b_machine_as_term(File,Machine,Options),
1840 parse_errors(Errors),
1841 (add_all_perrors_in_context_of_used_filenames(Errors,parse_error,error),fail)),
1842 b_load_additional_definitions_from_term(Machine).
1843
1844 b_load_additional_definitions_from_list_of_facts(ListOfFacts) :-
1845 load_b_machine_list_of_facts_as_term(ListOfFacts, Machine),
1846 b_load_additional_definitions_from_term(Machine).
1847
1848 b_load_additional_definitions_from_term(complete_machine(MainName, Machines, Filenames)) :-
1849 maplist(add_additional_filename,Filenames,NewNrs),
1850 member(definition_file(_,Defs),Machines),
1851 Defs = definitions(_Pos,_List),
1852 raw_update_file_nrs(Defs,NewNrs,NewDefs),
1853 bmachine_construction:extract_only_definitions(MainName,[NewDefs],DefsMachine,Errs),
1854 add_all_perrors_in_context_of_used_filenames(Errs,definition_type_error,error),
1855 retractall(additional_configuration_machine(MainName,_)),
1856 assert(additional_configuration_machine(MainName,DefsMachine)),
1857 b_machine_recompile_for_new_defs.
1858
1859
1860
1861
1862 % the next calls get typed definitions without parameters:
1863 % (To treat definitions with parameters one would have to add the parameters to the type environment, see type_check_definitions2)
1864 b_get_typed_predicate_definition(Name,Scope,ResTExpr) :-
1865 ? b_get_definition(Name,predicate,[],RawExpr,_Deps),
1866 type_with_errors_in_context(RawExpr,Scope,_,TExpr,machine_context,error),
1867 ResTExpr=TExpr. % Do unification after to not prevent generation of type errors.
1868 b_get_typed_expression_definition(Name,Scope,ResTExpr) :-
1869 ? b_get_definition(Name,expression,[],RawExpr,_Deps),
1870 type_with_errors_in_context(RawExpr,Scope,_,TExpr,machine_context,error),
1871 ResTExpr=TExpr. % Do unification after to not prevent generation of type errors, e.g., test 1691
1872 b_get_true_expression_definition(Name) :-
1873 b_get_typed_expression_definition(Name,[variables],PF),
1874 PF = b(boolean_true,boolean,_).
1875 %b_get_typed_subst_definition(Name,Scope,Parameters,TExpr) :-
1876 % temporary_set_preference(allow_local_operation_calls,true,CHNG),
1877 % b_get_definition(Name,substitution,Parameters,RawExpr,_Deps),
1878 % type_with_errors(RawExpr,[operation_bodies|Scope],_,TExpr), % need to remove variables to avoid clash warnings
1879 % reset_temporary_preference(allow_local_operation_calls,CHNG).
1880 b_get_typed_definition(Name,Scope,TExpr) :-
1881 ? b_get_definition(Name,_DefType,[],RawExpr,_Deps),
1882 type_with_errors_in_context(RawExpr,Scope,_,TExpr,machine_context,error).
1883
1884 % the following does not send errors to error_manager:
1885 b_get_typed_definition_with_error_list(Name,Scope,TExpr,ErrorsAndWarnings,Success) :-
1886 ? b_get_definition(Name,_DefType,[],RawExpr,_Deps),
1887 b_type_expression(RawExpr,Scope,_Type,TExpr,ErrorsAndWarnings),
1888 (no_real_perror_occurred(ErrorsAndWarnings) -> Success=true ; Success=false).
1889
1890 type_with_errors(RawExpr,Scope,Type,TExpr) :-
1891 type_with_errors_in_context(RawExpr,Scope,Type,TExpr,not_in_machine_context([]),error).
1892
1893
1894 type_with_errors_in_context(RawExpr,Scope,Type,TExpr,Context,ErrOrWarn) :- % print(scope(Scope)),nl,
1895 b_type_expression(RawExpr,Scope,Type,TExpr,Errors),!,
1896 (Context=not_in_machine_context(Filenames)
1897 -> add_all_perrors(Errors,Filenames,type_expression_error,ErrOrWarn) % [] for REPL, or JSON file for VisB
1898 ; add_all_perrors_in_context_of_used_filenames(Errors,type_expression_error,ErrOrWarn)
1899 ),
1900 no_real_perror_occurred(Errors). % check that we have no errors, just warnings
1901
1902 % here we do not add perrors; just fail
1903 type_without_errors(RawExpr,Scope,Type,TExpr) :-
1904 b_type_expression(RawExpr,Scope,Type,TExpr,Errors),!,
1905 no_real_perror_occurred(Errors).
1906
1907
1908 b_type_open_predicate_with_errors(OptionalQuantifier,RawPred,Scope,TPred) :-
1909 b_type_open_predicate(OptionalQuantifier,RawPred,Scope,TPred,Errors),
1910 add_all_perrors(Errors,[],type_expression_error),
1911 no_real_perror_occurred(Errors).
1912 b_type_open_predicate(OptionalQuantifier,RawPred,Scope,TPred,Errors) :-
1913 b_type_open_predicate_for_full_b_machine(_Machine,OptionalQuantifier,RawPred,Scope,TPred,Errors).
1914 b_type_open_predicate_for_full_b_machine(Machine,OptionalQuantifier,RawPred,Scope,TPred,Errors) :-
1915 (var(Machine) -> full_b_machine(Machine) ; true),
1916 replace_prob_set_elements_in_scope(Scope,Scope1),
1917 ? type_open_predicate_with_quantifier(OptionalQuantifier,RawPred,Scope1,Machine,TPred,Errors),!.
1918 b_type_open_exists_predicate(Raw,Typed,Errors) :-
1919 b_type_open_predicate(open(exists),Raw,[prob_ids(visible),variables],Typed,Errors).
1920
1921 b_type_expression(RawExpr,_Scope,Type,TExpr,Errors) :-
1922 b_type_literal(RawExpr,T,TE),!,
1923 Type=T,TExpr=TE,Errors=[].
1924 b_type_expression(RawExpr,Scope,Type,TExpr,Errors) :-
1925 b_type_expression_for_full_b_machine(_,RawExpr,Scope,Type,TExpr,Errors).
1926
1927 % type literals without setting up scope, ...
1928 % TODO: also use for type_in_machine_l
1929 b_type_literal(boolean_false(Pos),boolean,b(boolean_false,boolean,[nodeid(Pos)])).
1930 b_type_literal(boolean_true(Pos),boolean,b(boolean_true,boolean,[nodeid(Pos)])).
1931 b_type_literal(integer(Pos,Int),integer,b(integer(Int),integer,[nodeid(Pos)])).
1932 b_type_literal(real(Pos,R),real,b(real(R),real,[nodeid(Pos)])).
1933 b_type_literal(string(Pos,Atom),string,b(string(Atom),string,[nodeid(Pos)])).
1934
1935
1936 b_type_expression_for_full_b_machine(M,RawExpr,Scope,Type,TExpr,Errors) :-
1937 b_type_expressions_l(M,[RawExpr],Scope,[Type],[TExpr],Errors).
1938
1939 b_type_expressions_l(Machine,RawExprs,Scope,Types,TExprs,Errors) :-
1940 (var(Machine) -> full_b_machine(Machine) ; true),
1941 % in case you type check multiple expressions for a complex machine it is better to extract the machine once
1942 replace_prob_set_elements_in_scope(Scope,Scope1),
1943 % we need this, for example for tcltk_check_state_sequence_from_file, when deferred set elements written by TLC are in the file
1944 ? type_in_machine_l(RawExprs,Scope1,Machine,Types,TExprs,Errors),!.
1945
1946 replace_prob_set_elements_in_scope(Scope,Res) :- var(Scope),!,
1947 add_internal_error('Scope is a variable (use, e.g., [constants,variables,operation_bodies,...]):',replace_prob_set_elements_in_scope(Scope,Res)),
1948 Res=Scope.
1949 replace_prob_set_elements_in_scope(Scope,NewScope) :-
1950 ? ( select(prob_ids(AllOrVisible),Scope,identifier(Ids),NewScope) -> % replaces prob by deferred set element identifiers
1951 % for example if we have SETS PID then we would have PID1,... in Ids unless PID1 is known to be another identifier
1952 b_get_prob_deferred_set_elements(DefIDs,AllOrVisible),
1953 exclude(known_identifier,DefIDs,Ids) % exclude those ids that would clash
1954 % TO DO: add option to translate_identifiers using translate:keyword_to_id_cache
1955 ;
1956 Scope = NewScope).
1957
1958
1959 known_identifier(X) :- get_texpr_id(X,ID),
1960 (bmachine:b_is_constant(ID,_) ;
1961 bmachine:b_is_variable(ID,_)).
1962
1963 % ------------------------
1964
1965 % a generic predicate to find all kinds of identifiers
1966
1967 :- use_module(b_global_sets,[b_global_set/1, is_b_global_constant/3]).
1968 :- use_module(probsrc(kernel_freetypes),[registered_freetype/2, freetype_case_db/3]).
1969 :- use_module(probsrc(bmachine_eventb), [ stored_operator/2]).
1970 %! mode get_machine_identifiers(+Category, -ListOfIdentifiers)
1971 get_machine_identifiers(machines,MN) :-
1972 findall(FID, (b_filenumber(FID,Type,_,_),Type \= def),MN).
1973 get_machine_identifiers(definition_files,DFN) :-
1974 findall(FID, b_filenumber(FID,def,_,_),DFN).
1975 get_machine_identifiers(definitions,DN) :-
1976 findall(DefID,b_get_definition(DefID,_,_,_,_),DN).
1977 get_machine_identifiers(sets,Sets) :-
1978 findall(GS,b_global_set(GS),Sets).
1979 get_machine_identifiers(set_constants,Csts) :-
1980 findall(Cst,is_b_global_constant(_GS,_,Cst),Csts).
1981 get_machine_identifiers(constants,CN) :-
1982 b_get_machine_constants(Constants),
1983 get_texpr_ids(Constants,CN).
1984 get_machine_identifiers(freetypes,FN) :-
1985 findall(FID,((registered_freetype(F,_) ; freetype_case_db(F,_,_)),functor(F,FID,_)),FN).
1986 get_machine_identifiers(operators,FN) :-
1987 findall(Name,stored_operator(Name,_Kind),FN). % we could exclude Kind=datatype_definition, as listed in freetypes?
1988 get_machine_identifiers(variables,VN) :-
1989 b_get_machine_variables(Variables),
1990 get_texpr_ids(Variables,VN).
1991 get_machine_identifiers(operations,Ops) :-
1992 findall(Op,b_top_level_operation(Op),Ops).
1993
1994 get_machine_identifiers_with_pp_type(machines,MN) :-
1995 findall([FID,'Machine'], (b_filenumber(FID,Type,_,_),Type \= def),MN).
1996 get_machine_identifiers_with_pp_type(definition_files,DFN) :-
1997 findall([FID,'Definition file'], b_filenumber(FID,def,_,_),DFN).
1998 get_machine_identifiers_with_pp_type(definitions,DN) :-
1999 findall([DefID,DefType],b_get_definition(DefID,DefType,_,_,_),DN).
2000 get_machine_identifiers_with_pp_type(sets,Sets) :-
2001 findall([GS,GS],b_global_set(GS),Sets).
2002 get_machine_identifiers_with_pp_type(set_constants,Csts) :-
2003 findall([Cst,GS],is_b_global_constant(GS,_,Cst),Csts).
2004 get_machine_identifiers_with_pp_type(constants,CN) :-
2005 b_get_machine_constants(Constants),
2006 maplist(extract_id_and_pp_type,Constants,CN).
2007 %get_machine_identifiers_with_pp_type(freetypes,FN) :-
2008 % findall([FID,FID],((registered_freetype(F,_) ; freetype_case_db(F,_,_)),functor(F,FID,_)),FN).
2009 get_machine_identifiers_with_pp_type(operators,FN) :-
2010 findall([Name,''],stored_operator(Name,_Kind),FN). % we could exclude Kind=datatype_definition, as listed in freetypes?
2011 get_machine_identifiers_with_pp_type(variables,VN) :-
2012 b_get_machine_variables(Variables),
2013 maplist(extract_id_and_pp_type,Variables,VN).
2014 get_machine_identifiers_with_pp_type(operations,Ops) :-
2015 findall([Op,'Operation'],b_top_level_operation(Op),Ops).
2016
2017 :- use_module(bsyntaxtree,[get_texpr_id/2, get_texpr_type/2]).
2018 :- use_module(translate,[pretty_type/2]).
2019 extract_id_and_pp_type(TId,[Id,PPType]) :-
2020 get_texpr_id(TId,Id),
2021 get_texpr_type(TId,Type),
2022 pretty_type(Type,PPType).
2023
2024 :- use_module(b_global_sets,[b_global_deferred_set/1,all_elements_of_type/2]).
2025 :- use_module(input_syntax_tree,[get_raw_position_info/2]).
2026 % try and get source code for an identifier
2027 source_code_for_identifier(ID,constant,Type,OriginStr,OriginTerm,Source) :- b_is_constant(ID),!,
2028 get_constant_type_and_origin(ID,Type,OriginStr,OriginTerm),
2029 findall(Def,get_constant_definition(ID,Def),AllDefs),
2030 (AllDefs=[_|_] -> conjunct_predicates(AllDefs,Source)
2031 ; % try and find other type of predicates defining ID
2032 findall(Pred,get_constant_predicate(ID,Pred),AllPreds),
2033 conjunct_predicates(AllPreds,Source)).
2034 source_code_for_identifier(ID,variable,Type,OriginStr,OriginTerm,Source) :- b_is_variable(ID),!,
2035 get_variable_type_and_origin(ID,Type,OriginStr,OriginTerm),
2036 Source = b(truth,pred,[]). % TO DO: improve
2037 source_code_for_identifier(ID,Kind,Type,OriginStr,OriginTerm,Source) :- b_get_machine_set(ID,TID),!,
2038 (b_global_deferred_set(ID) -> Kind = deferred_set ; Kind = enumerated_set),
2039 Type = set(global(ID)),
2040 all_elements_of_type(ID,All),
2041 translate:translate_span_with_filename(TID,OriginStr), OriginTerm=TID,
2042 Source = b(equal(TID,b(value(All),Type,[])),pred,[]).
2043 source_code_for_identifier(ID,Kind,Type,OriginStr,OriginTerm,Source) :-
2044 global_set_element(ID,GID),!,
2045 (b_global_deferred_set(GID)
2046 -> Kind = deferred_set_element ; Kind = enumerated_set_element),
2047 b_get_machine_set(GID,TGID),
2048 Type = global(ID),
2049 all_elements_of_type(GID,All),
2050 translate:translate_span_with_filename(TGID,OriginStr), OriginTerm=TGID,
2051 Source = b(equal(TGID,b(value(All),set(Type),[])),pred,[]).
2052 source_code_for_identifier(ID,definition,Type,OriginStr,OriginTerm,Source) :-
2053 b_get_definition(ID,DefType,Args,RawExpr,_Deps),!,
2054 Type = DefType,
2055 % Definitions are only present in RAW form
2056 get_raw_position_info(RawExpr,PosInfo),
2057 translate:translate_span_with_filename(PosInfo,OriginStr), % the position info does not always seem to be valid (when coming from DEFINITION FILE) !??! TO DO fix
2058 OriginTerm=PosInfo,
2059 source_code_for_definition(DefType,ID,Args,RawExpr,Source).
2060 source_code_for_identifier(ID,file,Type,OriginStr,OriginTerm,b(string(Source),string,[])) :-
2061 b_filenumber(ID,Kind,_,Filename),
2062 extension_kind(Kind,Type),
2063 !,
2064 ajoin([Type,' ',ID],Source),
2065 OriginTerm =src_position_with_filename(1,0,0,Filename),
2066 OriginStr = Filename.
2067 source_code_for_identifier(ID,Kind,subst,OriginStr,OriginTerm,Source) :-
2068 b_find_operation(ID,Res,TParas,Body,OType),
2069 (OType=classic -> Kind = operation ; Kind=event),
2070 translate:translate_span_with_filename(Body,OriginStr),Body=OriginTerm,
2071 get_texpr_info(Body,Info),
2072 Source=b(operation(b(identifier(ID),subst,[]),Res,TParas,Body),subst,Info).
2073 source_code_for_identifier(ID,assertion,pred,OriginStr,OriginTerm,Assertion) :-
2074 b_get_assertions(all,_,Ass), member(Assertion,Ass),
2075 get_texpr_label(Assertion,ID), OriginTerm = Assertion,
2076 translate:translate_span_with_filename(Assertion,OriginStr).
2077 source_code_for_identifier(ID,invariant,pred,OriginStr,OriginTerm,Invariant) :-
2078 b_get_invariant_from_machine(C), conjunction_to_list(C,L), member(Invariant,L),
2079 get_texpr_label(Invariant,ID), OriginTerm = Invariant,
2080 translate:translate_span_with_filename(Invariant,OriginStr).
2081 % TO DO: look for invariant labels as ids ?
2082
2083 :- use_module(tools,[ split_last/4 ]).
2084 b_find_operation(ID,Res,TParas,Body,OType) :-
2085 b_get_machine_operation(ID,Res,TParas,Body,OType,_Pos).
2086 b_find_operation(ID,Res,TParas,Body,OType) :-
2087 b_get_machine_operation(ID2,Res,TParas,Body,OType,_Pos),
2088 split_last(ID2, '.', _, ID).
2089
2090 extension_kind(mch,'MACHINE').
2091 extension_kind(ref,'REFINEMENT').
2092 extension_kind(def,'DEFINITIONS FILE').
2093 extension_kind(imp,'IMPLEMENTATION').
2094
2095 source_code_for_definition(predicate,ID,_,RawExpr,Source) :-
2096 b_type_open_exists_predicate(RawExpr,Typed,Errors),
2097 (no_real_perror_occurred(Errors) -> true ; debug_println(9,errs(ID,Errors))),
2098 Source=Typed.
2099 source_code_for_definition(expression,ID,Args,RawExpr,Source) :-
2100 % TO DO: add parameters to avoid type errors; but we get Typed anyway
2101 b_type_expression(RawExpr,[prob_ids(visible),variables],Type,Typed,Errors),
2102 (no_real_perror_occurred(Errors) -> true ; debug_println(9,errs(ID,Args,Type,Errors))),
2103 Source=Typed.
2104 % TO DO: treate substitutions
2105 source_code_for_definition(DefType,ID,_Args,_RawExpr,Source) :-
2106 Source=b(identifier(ID),DefType,[]).
2107
2108 :- use_module(b_global_sets,[lookup_global_constant/2,prob_deferred_set_element/4]).
2109 global_set_element(ID,GlobalSetID) :- lookup_global_constant(ID,fd(_,GlobalSetID)).
2110 global_set_element(ID,GlobalSetID) :-
2111 prob_deferred_set_element(GlobalSetID,_Elem,ID,all).
2112
2113 get_constant_span(ID,Span) :-
2114 b_get_machine_constants(Constants),
2115 TID = b(identifier(ID),_,Span),
2116 member(TID,Constants).
2117
2118 get_constant_type_and_origin(ID,Type,OriginStr,OriginTerm) :-
2119 b_get_machine_constants(Constants),
2120 TID = b(identifier(ID),Type,_Infos),
2121 member(TID,Constants),
2122 % we could also use member(origin(Origin),Infos)
2123 translate:translate_span_with_filename(TID,OriginStr), OriginTerm=TID.
2124 get_variable_type_and_origin(ID,Type,OriginStr,OriginTerm) :-
2125 b_get_machine_variables(Vars),
2126 TID = b(identifier(ID),Type,_Infos),
2127 member(TID,Vars),
2128 % we could also use member(origin(Origin),Infos)
2129 translate:translate_span_with_filename(TID,OriginStr), OriginTerm=TID.
2130
2131 get_constant_definition(ID,FullDef) :-
2132 b_get_properties_from_machine(Prop),
2133 EqDef = b(equal(LHS,RHS),pred,_),
2134 member_in_conjunction_cse(FullDef,EqDef,Prop),
2135 (get_texpr_id(LHS,ID) ; get_texpr_id(RHS,ID)).
2136
2137 get_constant_predicate(ID,FullPred) :-
2138 b_get_properties_from_machine(Prop),
2139 member_in_conjunction_cse(FullPred,Pred,Prop),
2140 involves_id(Pred,ID).
2141 involves_id(ID,b(E,_,_)) :- involves_id_aux(E,ID).
2142 involves_id_aux(member(LHS,_),ID) :- get_texpr_id(LHS,ID).
2143 involves_id_aux(subset(LHS,_),ID) :- get_texpr_id(LHS,ID).
2144 involves_id_aux(subset_strict(LHS,_),ID) :- get_texpr_id(LHS,ID).
2145
2146 :- volatile b_get_machine_setscope/2.
2147 :- dynamic b_get_machine_setscope/2.
2148 :- public b_get_machine_setscope_calc/2.
2149 % precompiled: definitions of the form "scope_SET == Expr",
2150 % Set is the name of the Set, TExpr the typed expression
2151 b_get_machine_setscope_calc(Set,TExpr) :-
2152 ? b_definition_prefixed(expression, scope_, Set, Name,_),
2153 % TO DO: check if it is a SET
2154 ? b_get_typed_definition(Name,[constants],TExpr). % [constants] scope so that we have access to other definitions
2155
2156
2157 % get a specific MAX_OPERATIONS Value for an operation
2158 :- volatile b_get_machine_operation_max/2.
2159 :- dynamic b_get_machine_operation_max/2.
2160 :- public b_get_machine_operation_max_calc/2.
2161 % precompiled: definitions of the form "scope_SET == Expr",
2162 % Set is the name of the Set, TExpr the typed expression
2163 b_get_machine_operation_max_calc(Set,MaxOp) :-
2164 b_definition_prefixed(expression, 'MAX_OPERATIONS_', Set, Name,DefPos),
2165 (b_get_typed_definition(Name,[constants],DEF), % scope=constants allows to use other definitions
2166 DEF=b(integer(MaxOp),integer,_)
2167 % TO DO: check if it is an operation
2168 %, MaxOp >= 0 we now use negative numbers for randomised restart
2169 -> true
2170 ; add_warning(b_get_machine_operation_max_calc,'Definition must specify an integer (negative numbers means using randomised restart) ',Name,DefPos),
2171 fail
2172 ).
2173
2174 :- volatile b_get_machine_goal/1.
2175 :- dynamic b_get_machine_goal/1.
2176 :- public b_get_machine_goal_calc/1.
2177 % precompiled: definition of GOAL, a typed predicate
2178 ?b_get_machine_goal_calc(TPred) :- get_goal(TPred).
2179
2180 b_reset_machine_goal_from_DEFINITIONS :-
2181 get_goal(TPred),
2182 b_set_parsed_typed_machine_goal(TPred).
2183 get_goal(Goal) :-
2184 get_proz_settings(Settings),memberchk(goal(Goal),Settings),!.
2185 get_goal(Goal) :- % print(getting_goal),nl,
2186 get_texpr_type(Goal,pred),
2187 ? b_get_typed_predicate_definition('GOAL',[variables],Goal).
2188
2189 :- volatile b_get_machine_searchscope/1.
2190 :- dynamic b_get_machine_searchscope/1.
2191 :- public b_get_machine_searchscope_calc/1.
2192 % precompiled: definition of SCOPE, a typed predicate
2193 b_get_machine_searchscope_calc(TPred) :-
2194 get_texpr_type(TPred,pred),
2195 ? b_get_typed_definition('SCOPE',[variables],TPred).
2196
2197 :- volatile b_get_definition_string_from_machine/3.
2198 :- dynamic b_get_definition_string_from_machine/3.
2199 :- public b_get_definition_string_from_machine_calc/3.
2200 % precompiled: string definitions, Name == "String"
2201 b_get_definition_string_from_machine(Name,String) :-
2202 b_get_definition_string_from_machine(Name,_,String).
2203 b_get_definition_string_from_machine_calc(Name,Pos,String) :-
2204 ? b_get_definition(Name,expression,[],string(Pos,Str),_Deps),
2205 get_texpr_expr(TExpr,string(String)),
2206 type_with_errors_in_context(string(Pos,Str),[],_,TExpr,machine_context,warning).
2207
2208 get_animation_image(Nr,S) :-
2209 animation_minor_mode(z),
2210 get_proz_animation_function(_,_,Images),!,
2211 nth1(Nr,Images,S).
2212 get_animation_image(Nr,S) :- number(Nr),!,
2213 number_codes(Nr,TailCodes),
2214 /* ANIMATION_IMG */
2215 atom_codes(Def_Name,[65,78,73,77,65,84,73,79,78,95,73,77,71|TailCodes]),
2216 b_get_definition_string_from_machine(Def_Name,S).
2217 get_animation_image(Nr,S) :-
2218 b_get_definition_string_from_machine(Def_Name,S),
2219 /* ANIMATION_IMG */
2220 atom_codes(Def_Name,[65,78,73,77,65,84,73,79,78,95,73,77,71|TailCodes]),
2221 number_codes(Nr,TailCodes).
2222
2223 :- use_module(error_manager,[extract_file_number_and_name/3]).
2224 :- use_module(specfile,[b_or_z_mode/0]).
2225 get_animation_image_source_file(Nr,File) :- b_or_z_mode,
2226 % get source file where Animation image is defined; relevant for finding images
2227 b_get_definition_string_from_machine(Def_Name,Pos,_),
2228 atom_codes(Def_Name,[65,78,73,77,65,84,73,79,78,95,73,77,71|TailCodes]),
2229 number_codes(Nr,TailCodes),
2230 extract_file_number_and_name(Pos,_,File).
2231
2232 get_proz_animation_function(Function,Default,Images) :-
2233 get_proz_settings(Settings),
2234 memberchk(animation_function(Function,Default,Images),Settings).
2235 get_proz_settings(Settings) :-
2236 machine(_,Sections),memberchk(meta/Meta,Sections),
2237 memberchk(proz_settings(Settings),Meta).
2238
2239
2240 :- volatile b_get_machine_animation_function/2.
2241 :- dynamic b_get_machine_animation_function/2.
2242 :- public b_get_machine_animation_function_calc/2.
2243 :- use_module(tools,[safe_number_codes/2]).
2244 :- use_module(bsyntaxtree,[is_set_type/2]).
2245 % precompiled: definition of ANIMATION_FUNCTION, a typed expression
2246 b_get_machine_animation_function_calc(AFun,Nr) :-
2247 get_proz_animation_function(TFun,Default,_),!,
2248 ( Nr = -1, AFun = Default
2249 ; Nr = 0, TFun \= none, AFun=TFun
2250 ).
2251 b_get_machine_animation_function_calc(TFun,Nr) :-
2252 ? get_definition_with_nr_suffix("ANIMATION_FUNCTION",Nr,Def_Name),
2253 ? b_get_typed_expression_definition(Def_Name,[variables],TFun), % only type it afterwards; avoid throwing type errors for other definitions
2254 get_texpr_type(TFun,Type),
2255 (is_set_type(Type,couple(_,_)) -> true
2256 ; add_warning(b_get_machine_animation_function_calc,'Illegal type for ANIMATION_FUNCTION: ',Def_Name:Type,TFun),
2257 fail).
2258
2259
2260 :- volatile b_get_machine_heuristic_function/1.
2261 :- dynamic b_get_machine_heuristic_function/1.
2262 :- public b_get_machine_heuristic_function_calc/1.
2263 b_get_machine_heuristic_function_calc(TFun) :- %print(extracting_heuristic_fun(TFun)),nl,
2264 get_texpr_type(TFun,integer),
2265 ? b_get_typed_expression_definition('HEURISTIC_FUNCTION',[variables],TFun).
2266
2267 :- volatile b_get_machine_animation_expression/2.
2268 :- dynamic b_get_machine_animation_expression/2.
2269 :- public b_get_machine_animation_expression_calc/2.
2270 b_get_machine_animation_expression_calc(STR,AExpr) :- %print(extracting_heuristic_fun(TFun)),nl,
2271 ? useful_animation_expression(STR),
2272 ? b_get_typed_expression_definition(STR,[variables],AExpr).
2273 b_get_machine_animation_expression_calc(DefName,AExpr) :-
2274 ? b_definition_prefixed(_,'ANIMATION_EXPRESSION',_,DefName,_DefPos),
2275 ? b_get_typed_expression_definition(DefName,[variables],AExpr).
2276
2277 %useful_animation_expression('ANIMATION_EXPRESSION'). % for state viewer
2278 useful_animation_expression('GAME_PLAYER'). % for MCTS, should return "min" or "max"
2279 useful_animation_expression('GAME_OVER').
2280 useful_animation_expression('GAME_VALUE').
2281 useful_animation_expression('GAME_MCTS_RUNS').
2282 useful_animation_expression('GAME_MCTS_TIMEOUT').
2283 useful_animation_expression('GAME_MCTS_CACHE_LAST_TREE').
2284
2285
2286 % Custom nodes and edges for a custom graph representation of a state
2287 :- volatile b_get_machine_custom_nodes_function/2, b_get_machine_custom_edges_function/2,
2288 b_get_machine_custom_graph_function/2.
2289 :- dynamic b_get_machine_custom_nodes_function/2, b_get_machine_custom_edges_function/2,
2290 b_get_machine_custom_graph_function/2.
2291 :- public b_get_machine_custom_nodes_function_calc/2.
2292 b_get_machine_custom_nodes_function_calc(TFun,Nr) :-
2293 ? get_definition_with_nr_suffix("CUSTOM_GRAPH_NODES",Nr,Def_Name),
2294 ? b_get_typed_expression_definition(Def_Name,[variables],TFun).
2295 :- public b_get_machine_custom_edges_function_calc/2.
2296 b_get_machine_custom_edges_function_calc(TFun,Nr) :-
2297 ? get_definition_with_nr_suffix("CUSTOM_GRAPH_EDGES",Nr,Def_Name),
2298 ? b_get_typed_expression_definition(Def_Name,[variables],TFun).
2299 :- public b_get_machine_custom_graph_function_calc/2.
2300 b_get_machine_custom_graph_function_calc(TFun,Nr) :-
2301 ? get_definition_with_nr_suffix("CUSTOM_GRAPH",Nr,Def_Name), % single function for graph attributes, possibly edges and nodes
2302 ? b_get_typed_expression_definition(Def_Name,[variables],TFun).
2303
2304
2305 get_definition_with_nr_suffix(Prefix,Nr,Def_Name) :-
2306 ? b_get_definition(Def_Name,expression,[],_RawExpr,_Deps),
2307 atom_codes(Def_Name,AC),
2308 append(Prefix,TailCodes,AC),
2309 (TailCodes=[] -> Nr=0
2310 ; TailCodes = "_DEFAULT" -> Nr = -1
2311 ; safe_number_codes(Nr,TailCodes)).
2312
2313
2314 % ------------------------
2315
2316 :- volatile b_get_constant_represented_inside_global_set/2.
2317 :- dynamic b_get_constant_represented_inside_global_set/2.
2318
2319 :- public b_get_constant_represented_inside_global_set_calc/2.
2320 b_get_constant_represented_inside_global_set_calc(X,GlobalSetName) :-
2321 ? b_get_disjoint_constants_of_type(GlobalSetName, DisjointConstants,_),
2322 ? member(X,DisjointConstants). /* X will be integrated into the global_set */
2323
2324
2325 :- volatile b_get_disjoint_constants_of_type/3.
2326 :- dynamic b_get_disjoint_constants_of_type/3.
2327 :- public b_get_disjoint_constants_of_type_calc/3.
2328 b_get_disjoint_constants_of_type_calc(GlobalSetName, DisjointConstants, AllConstantsIDs) :-
2329 b_get_machine_all_constants(Constants), /* get all the constants */
2330 b_get_properties_from_machine(Properties),
2331 ? b_get_machine_set(GlobalSetName),
2332 \+ b_get_named_machine_set(GlobalSetName,_), % not an explicitly enumerated set
2333 find_constants_of_type(Constants,GlobalSetName,AllConstantsIDs,_GSConstants),
2334 find_inequal_global_set_identifiers(AllConstantsIDs,global(GlobalSetName),Properties,DisjointConstants),
2335 DisjointConstants \= [],
2336 debug_println(9,disjoint_enumerated_constants(GlobalSetName,DisjointConstants)).
2337 % TO DO: remove from Properties irrelevant conjuncts; sort AllConstantsIDs by having first those with max disequalities
2338
2339 find_constants_of_type([],_GS,[],[]) :- !.
2340 find_constants_of_type([b(identifier(ID),global(GS),INFO)|T], GS, [ID|IT],
2341 [b(identifier(ID),global(GS),INFO)|TT]) :- !,
2342 find_constants_of_type(T,GS,IT,TT).
2343 find_constants_of_type([b(_,_,_)|T], GS, IT, TT) :- !,
2344 find_constants_of_type(T,GS,IT,TT).
2345 find_constants_of_type(X,GS,_,_) :- print(find_constants_of_type_error(X,GS)),nl,fail.
2346
2347
2348 % ------------------------
2349 :- volatile b_get_all_used_identifiers_in_section/2.
2350 :- dynamic b_get_all_used_identifiers_in_section/2.
2351 :- public b_get_all_used_identifiers_in_section_calc/2.
2352
2353 % Note: may contain var$0 instead of var for becomes_such
2354 b_get_all_used_identifiers_in_section_calc(SECTION,Identifiers) :-
2355 full_b_machine(BMachine),
2356 ? member(SECTION,[constraints,properties,invariant,assertions,
2357 initialisation,operation_bodies]),
2358 findall(I, find_used_identifier_in_machine_section(BMachine,SECTION,I), Ids),
2359 %print(section_ids(SECTION,Ids)),nl,
2360 sort(Ids,Identifiers).
2361
2362 :- volatile b_get_all_used_identifiers/1.
2363 :- dynamic b_get_all_used_identifiers/1.
2364 :- public b_get_all_used_identifiers_calc/1.
2365 :- use_module(library(ordsets),[ord_union/2]).
2366 % Precompiled: b_get_all_used_identifiers_calc/1 returns a list of all
2367 % identifiers used in machine sections that contain expressions and predicates
2368 b_get_all_used_identifiers_calc(Identifiers) :-
2369 findall(I, b_get_all_used_identifiers_in_section(_,I), ListOfList),
2370 ord_union(ListOfList,Identifiers). % ,print(all(Identifiers)),nl.
2371
2372 find_used_identifier_in_machine_section(Machine,Sec,Identifier) :-
2373 % treat it like a list of expressions
2374 ? get_section_texprs(Sec,Machine,TExprs),
2375 % and find all identifiers in each expression
2376 ? member(TExpr,TExprs),
2377 find_identifier_uses(TExpr,[],Ids),
2378 ? member(Identifier,Ids).
2379
2380 :- volatile b_is_unused_constant/1.
2381 :- dynamic b_is_unused_constant/1.
2382 :- public b_is_unused_constant_calc/1.
2383 b_is_unused_constant_calc(UnusedConstant) :-
2384 findall(C,b_is_constant(C),CL), %b_get_machine_constants(Constants), gives typed ids
2385 CL\=[] ,sort(CL,Constants),
2386 b_get_all_used_identifiers_in_section(invariant,I1),
2387 b_get_all_used_identifiers_in_section(assertions,I2),
2388 b_get_all_used_identifiers_in_section(initialisation,I3),
2389 b_get_all_used_identifiers_in_section(operation_bodies,I4),
2390 % TODO: get constants used in VisB definitions
2391 ord_union([I1,I2,I3,I4],UsedIds),
2392 %print(used(UsedIds)),nl,
2393 ord_subtract(Constants,UsedIds,UnusedConstants),
2394 UnusedConstants\=[],
2395 (b_get_machine_variables([]) -> true
2396 ; length(UnusedConstants,NrUC),
2397 (silent_mode(on) -> true
2398 ; (NrUC>10,debug_mode(off),UnusedConstants=[C1,C2|_]) ->
2399 print_message_with_max_depth(unused_constants(NrUC,[C1,C2,'...']),500)
2400 ; print_message_with_max_depth(unused_constants(NrUC,UnusedConstants),500))
2401 ),
2402 ? member(UnusedConstant,UnusedConstants).
2403
2404
2405 % precompiled: Skel is the operation skeleton, SpecializedInv a typed predicate
2406 % (Skel,SpecializedInv) :-
2407 % b_get_machine_operation(Name,_Res,Params,_Body),
2408 % atom_concat('SIMPLIFIED_INV_OP_',Name,ASNC),
2409 % b_get_typed_definition(ASNC,[variables,identifiers(Params)],SpecializedInv),
2410 % length(Params,Len),
2411 % functor(Skel,Name,Len),
2412 % print(b_specialized_invariant_for_op(Skel)).
2413
2414
2415 get_section_from_current_machine(Section,Content) :-
2416 full_b_machine(BMachine),
2417 get_section(Section,BMachine,Content).
2418
2419 is_ground(X,R) :- ground(X),!,R=ground.
2420 is_ground(_,nonground).
2421
2422 b_set_empty_machine :- debug_println(9,setting_empty_machine),
2423 empty_machine(Main,Machines),
2424 b_set_machine(Main,Machines,[]).
2425
2426 b_get_machine_refinement_hierarchy(Hierarchy) :-
2427 \+ machine(_Name,_M),!,Hierarchy=[]. %No B Machine loaded
2428 b_get_machine_refinement_hierarchy(Hierarchy) :-
2429 get_section_from_current_machine(meta,Infos),
2430 ? member(hierarchy/Hierarchy,Infos),!.
2431
2432 b_get_refined_machine_name(Machine) :-
2433 b_get_machine_refinement_hierarchy([_Main,Machine|_Rest]).
2434 b_get_refined_ancestors_names(list(AncestorList)) :-
2435 b_get_machine_refinement_hierarchy([_Main|AncestorList]).
2436 b_get_refined_machine(M) :-
2437 get_section_from_current_machine(meta,Infos),
2438 member(refined_machine/M,Infos), !.
2439
2440
2441
2442 b_get_machine_header_position(MachName,Position) :-
2443 get_section_from_current_machine(meta,Infos),
2444 member(header_pos/HeaderPosList,Infos),
2445 % List with elements MachineName/PositionOfMachineHeader
2446 member(MachName/Position,HeaderPosList).
2447
2448 % model type can be system for Atelier-B Event-B
2449 b_get_model_type(M) :-
2450 get_section_from_current_machine(meta,Infos),
2451 member(model_type/M,Infos), !.
2452
2453 % TODO(DP,6.8.2008)
2454 :- volatile b_machine_temp_predicate/1.
2455 :- dynamic b_machine_temp_predicate/1.
2456
2457 %set_temp_predicate(CustomPredicate) :-
2458 % b_parse_machine_predicate(CustomPredicate,TypedPred),
2459 % assert_temp_typed_predicate(TypedPred).
2460 %
2461 %% set a temporary predicate as additional guard
2462 %set_temp_predicate(CustomPredicate,'$initialise_machine') :- !,set_temp_predicate(CustomPredicate).
2463 %set_temp_predicate(CustomPredicate,'$setup_constants') :- !,set_temp_predicate(CustomPredicate).
2464 %set_temp_predicate(CustomPredicate,OpName) :-
2465 % b_parse_machine_operation_pre_post_predicate(CustomPredicate,TypedPred, OpName,true),
2466 % assert_temp_typed_predicate(TypedPred).
2467
2468 % Note: it can be a good idea to use inline_prob_deferred_set_elements_into_bexpr/2 before:
2469 assert_temp_typed_predicate(TypedPred) :-
2470 reset_temp_predicate,
2471 assertz(b_machine_temp_predicate(TypedPred)).
2472
2473
2474 reset_temp_predicate :- retractall(b_machine_temp_predicate(_)).
2475
2476 :- volatile b_machine_additional_property/1.
2477 :- dynamic b_machine_additional_property/1.
2478
2479 % additional properties for set_up_constants
2480 % TO DO: check if there are constants/properties; otherwise raise warning
2481 add_additional_property(CustomPredicate,Description) :-
2482 format('Adding Property: ~w~n',[CustomPredicate]),
2483 b_parse_machine_predicate(CustomPredicate,TypedPred),
2484 add_texpr_info_if_new(TypedPred,description(Description),TP2),
2485 assertz(b_machine_additional_property(TP2)).
2486
2487 :- use_module(btypechecker, [unify_types_strict/2]).
2488 :- use_module(bsyntaxtree, [safe_create_texpr/4]).
2489 :- use_module(probsrc(translate), [pretty_type/2]).
2490
2491 :- public b_extract_values_clause_assignment_calc/3.
2492 b_extract_values_clause_assignment_calc(ID,Type,TVal) :-
2493 % extract equalities from VALUES clause
2494 get_section_from_current_machine(values,Values),
2495 ? member(b(values_entry(TID,TVal),_,Info),Values),
2496 get_texpr_id(TID,ID),
2497 get_texpr_type(TID,Type),
2498 debug_println(20,values_entry(ID,Type,TVal)),
2499 (b_is_constant(ID,OtherType),
2500 unify_types_strict(Type,OtherType)
2501 -> (member(description(_),Info) -> Info1=Info
2502 ; Info1=[description('from VALUES clause') | Info]),
2503 safe_create_texpr(equal(TID,TVal),pred,Info1,Equality),
2504 (debug_mode(off) -> true ; add_message(bmachine,'Adding property for VALUES: ',Equality,Equality)),
2505 assertz(b_machine_additional_property(Equality)),
2506 (b_extract_values_clause_assignment(ID,_,_)
2507 -> add_error(bmachine,'Multiple VALUES entries for constant: ',ID,TID)
2508 ; true)
2509 ; b_get_machine_set(ID) -> true % will be dealt with in b_global_sets for deferred sets
2510 ; b_get_constant_represented_inside_global_set(ID,_) ->
2511 add_message(bmachine,'Ignoring VALUES entry for constant (already detected as enumerated set element): ',ID,TID)
2512 ; lookup_global_constant(ID,fd(_,GSET)) ->
2513 ajoin(['Ignoring VALUES entry for element of enumerated set ',GSET,': '],Msg),
2514 add_message(bmachine,Msg,ID,TID)
2515 % TODO: detect case when this is a deferred set element not detected as (virtual) enumerated element
2516 ; b_is_constant(ID,OtherType) -> pretty_type(OtherType,OT), pretty_type(Type,TT),
2517 ajoin(['Cannot adapt value type ',TT,' to abstract type ',OT,', ignoring VALUES entry for: '],Msg),
2518 add_warning(bmachine,Msg,ID,TID)
2519 ; add_error(bmachine,'VALUES clause for unknown constant: ',ID,TID),
2520 fail
2521 ).
2522
2523
2524 % -------------------
2525
2526 :- use_module(specfile,[unset_animation_minor_modes/1,reset_animation_minor_modes/1]).
2527 :- use_module(translate,[set_unicode_mode/0, unset_unicode_mode/0, set_print_type_infos/1]).
2528 b_show_machine_representation_unicode(Rep,AdditionalInfo,UnsetMinorModes,Unicode) :-
2529 Unicode=true,!,
2530 set_unicode_mode,
2531 call_cleanup(b_show_machine_representation(Rep,AdditionalInfo,UnsetMinorModes,none),unset_unicode_mode).
2532 b_show_machine_representation_unicode(Rep,AdditionalInfo,UnsetMinorModes,_) :-
2533 b_show_machine_representation(Rep,AdditionalInfo,UnsetMinorModes,none).
2534
2535
2536 % AdditionalInfo=true means show additional information as comments (promoted, ...)
2537 % UnsetMinorModes will print in default classical B style
2538 % TypeInfos: none, needed or all
2539 b_show_machine_representation(Rep,AdditionalInfo,UnsetMinorModes,TypeInfos) :-
2540 full_b_machine(BMachine),
2541 (UnsetMinorModes==true -> unset_animation_minor_modes(L) ; L=[]),
2542 set_print_type_infos(TypeInfos),
2543 translate_machine(BMachine,Rep,AdditionalInfo),
2544 set_print_type_infos(none),
2545 (UnsetMinorModes==true -> reset_animation_minor_modes(L) ; true).
2546
2547 :- use_module(tools_printing,[nested_write_term_to_codes/2]).
2548 b_get_internal_prolog_representation_as_codes(Codes) :-
2549 full_b_machine(BMachine),
2550 nested_write_term_to_codes(BMachine,Codes).
2551
2552 :- use_module(tools,[get_tail_filename/2,split_filename/3,safe_atom_chars/3]).
2553 % TypingLevel = none, needed or all
2554 b_write_machine_representation_to_file(TypingLevel,PPFILE) :-
2555 b_write_machine_representation_to_file('$auto',TypingLevel,PPFILE).
2556 b_write_machine_representation_to_file('$auto',TypingLevel,PPFILE) :- !, % automatically infer machine name
2557 %get_full_b_machine(Name,M),
2558 get_tail_filename(PPFILE,Tail),
2559 split_filename(Tail,MachName,_Ext),
2560 b_write_machine_representation_to_file3(MachName,TypingLevel,PPFILE).
2561 b_write_machine_representation_to_file(MachName,TypingLevel,PPFILE) :-
2562 % provide explicit machine name; useful for diff checks
2563 b_write_machine_representation_to_file3(MachName,TypingLevel,PPFILE).
2564
2565 :- use_module(translate,[set_print_type_infos/1]).
2566 :- use_module(tools_files, [write_to_utf8_file_or_user_output/2]).
2567 b_write_machine_representation_to_file3(MachName,Level,PPFILE) :-
2568 debug_println(20,'% Pretty-Printing Internal Representation to File: '),
2569 debug_println(20,PPFILE),
2570 translate:set_print_type_infos(Level), % none, needed or all
2571 get_full_b_machine(_Name,M),
2572 (translate_machine_to_classicalb(MachName,M,Rep)
2573 -> translate:set_print_type_infos(none)
2574 ; add_internal_error('Translating machine failed: ',b_write_machine_representation_to_file3(MachName,Level,PPFILE)),
2575 set_print_type_infos(none),
2576 fail),
2577 write_to_utf8_file_or_user_output(PPFILE,Rep).
2578
2579 :- use_module(specfile).
2580 translate_machine_to_classicalb(MachName,M,Rep) :-
2581 temporary_set_preference(expand_avl_upto,-1,CHNG), % avoid printing sets using condensed #
2582 (animation_minor_mode(X)
2583 -> remove_animation_minor_mode,
2584 call_cleanup(translate_machine(machine(MachName,M),Rep,false), set_animation_minor_mode(X))
2585 ; translate_machine(machine(MachName,M),Rep,false)),
2586 reset_temporary_preference(expand_avl_upto,CHNG).
2587
2588 b_write_eventb_machine_to_classicalb_to_file(PPFILE) :-
2589 get_tail_filename(PPFILE,Tail),
2590 split_filename(Tail,MachName,_Ext),
2591 AdditionalInfo=true,
2592 b_get_eventb_machine_as_classicalb_codes(MachName,AdditionalInfo,Rep),
2593 write_to_utf8_file_or_user_output(PPFILE,Rep).
2594
2595 :- use_module(preferences,[temporary_set_preference/3,reset_temporary_preference/2]).
2596 b_get_eventb_machine_as_classicalb_codes(MachName,AdditionalInfo,Rep) :-
2597 full_b_machine(machine(Name,MachineBody)),
2598 (var(MachName) -> MachName=Name ; true),
2599 % limit abstract level to 0
2600 b_limit_abstract_level_to_zero(MachineBody,MachineBodyLevel0),
2601 temporary_set_preference(translate_print_typing_infos,true,CHNG),
2602 temporary_set_preference(translate_ids_to_parseable_format,true,CHNG2),
2603 temporary_set_preference(expand_avl_upto,-1,CHNG3), % avoid printing sets using condensed #
2604 (translate_eventb_to_classicalb(machine(MachName,MachineBodyLevel0),AdditionalInfo,Rep)
2605 -> reset_temporary_preference(translate_print_typing_infos,CHNG),
2606 reset_temporary_preference(translate_ids_to_parseable_format,CHNG2),
2607 reset_temporary_preference(expand_avl_upto,CHNG3)
2608 ; add_internal_error('Translating Event-B machine to Classical B failed: ',b_get_eventb_machine_as_classicalb_codes(MachName,AdditionalInfo,Rep)),
2609 reset_temporary_preference(translate_print_typing_infos,CHNG),
2610 reset_temporary_preference(translate_ids_to_parseable_format,CHNG2),
2611 reset_temporary_preference(expand_avl_upto,CHNG3),
2612 fail).
2613
2614 b_limit_abstract_level_to_zero(MachineBody,MachineBodyLevel0) :-
2615 maplist(b_set_to_level_zero,MachineBody,MachineBodyLevel0).
2616
2617 % TODO: set to level zero also the other events of the Event-B machine
2618 b_set_to_level_zero(initialisation/InitEvent,initialisation/InitEventLevelZero) :-
2619 get_texpr_expr(InitEvent,rlevent(Id,Sec,St,Par,Grd,Thms,Act,VW,PW,Ums,_Abs)),
2620 get_texpr_info(InitEvent,Info),
2621 create_texpr(rlevent(Id,Sec,St,Par,Grd,Thms,Act,VW,PW,Ums,[]),subst,Info,InitEventLevelZero).
2622 b_set_to_level_zero(X,X).
2623
2624 b_show_eventb_as_classicalb(Rep,AdditionalInfo) :-
2625 full_b_machine(BMachine),
2626 translate_eventb_to_classicalb(BMachine,AdditionalInfo,Rep).
2627
2628 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2629
2630 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2631 % precompilation: predicates are precompiled by calling the ..._calc predicate
2632
2633 :- use_module(state_packing).
2634 :- use_module(tools,[start_ms_timer/1,stop_ms_walltimer_with_msg/2]).
2635 :- use_module(rulesdslsrc(rule_validation),[setup_rules_extras/0]).
2636 % maybe this predicate should be directly called by b_load_machine
2637 b_machine_precompile :- debug_println(9,'Precompiling B Machine'),
2638 start_ms_timer(T1),
2639 get_full_b_machine(_,_),
2640 auto_precompile,
2641 (debug_mode(on) -> stop_ms_walltimer_with_msg(T1,'auto_precompile: ') ; true),
2642 precompile_operation_names_in_reverse_order,
2643 % TODO(DP, 14.8.2008): remove reference to b_global_sets
2644 start_ms_timer(T2),
2645 b_check_and_precompile_deferred_sets,
2646 (debug_mode(on) -> stop_ms_walltimer_with_msg(T2,'precompiling global sets: ') ; true),
2647 % Now done in bmachine_construction:clean_up_machine but not yet for Event-B:
2648 get_section_from_current_machine(freetypes,Freetypes),register_freetypes(Freetypes),
2649 auto_precompile_phase2,
2650 b_check_and_precompile_global_set_symmetry,
2651 state_packing:precompile_state_packing,
2652 do_machine_consistency_check,
2653 try_kodkod,
2654 (animation_minor_mode(rules_dsl) -> setup_rules_extras ; true),
2655 (debug_mode(on) -> stop_ms_walltimer_with_msg(T1,'complete precompiling B machine: ') ; true).
2656
2657 % recompile predicates which change when defs are loaded (e.g., CUSTOM_GRAPH or similar)
2658 b_machine_recompile_for_new_defs :-
2659 start_ms_timer(T1),
2660 auto_recompile_for_new_defs,
2661 (debug_mode(on) -> stop_ms_walltimer_with_msg(T1,'recompile for defs: ') ; true).
2662 auto_recompile_for_new_defs :-
2663 % failure-driven loop
2664 precompiled_predicate_no_error_when_not_precompiled(Pred/Arity), %print(precompile(Pred/Arity)),nl,
2665 auto_precompile2(Pred,Arity,Pattern),
2666 (Pattern -> true /* this pattern already asserted */
2667 ; assertz(Pattern)), fail.
2668 auto_recompile_for_new_defs.
2669
2670
2671
2672 other_spec_precompile :- retractall(bmachine_is_precompiled),
2673 /* call if you do not animate a B specification */
2674 ? is_precompiled_predicate(Pred/Arity),
2675 functor(Pattern,Pred,Arity),
2676 retractall(Pattern),
2677 ? (precompiled_predicate_no_error_when_not_precompiled(Pred/Arity)
2678 -> assertz( (Pattern :- fail ))
2679 ; assertz( (Pattern :- print_message('No B machine available for '),print_message(Pattern),fail) )
2680 ),
2681 fail.
2682 other_spec_precompile :-
2683 retractall(b_get_machine_constants(_)),
2684 assertz( b_get_machine_constants([]) ),
2685 retractall(b_get_machine_variables_in_original_order(_)),
2686 assertz( b_get_machine_variables_in_original_order([]) ),
2687 retractall(b_get_machine_variables(_)),
2688 assertz( b_get_machine_variables([]) ),
2689 retractall(b_get_static_assertions_from_machine(_)),
2690 assertz( b_get_static_assertions_from_machine([]) ),
2691 retractall(b_machine_has_static_assertions),
2692 retractall(b_get_unproven_static_assertions_from_machine(_)),
2693 assertz( b_get_unproven_static_assertions_from_machine([]) ),
2694 retractall(b_get_dynamic_assertions_from_machine(_)),
2695 assertz( b_get_dynamic_assertions_from_machine([]) ),
2696 retractall(b_machine_has_dynamic_assertions),
2697 retractall(b_get_unproven_dynamic_assertions_from_machine(_)),
2698 assertz( b_get_unproven_dynamic_assertions_from_machine([]) ),
2699 retractall( b_get_machine_searchscope(_) ),
2700 retractall( b_get_machine_goal(_) ),
2701 assert_bmachine_is_precompiled, debug_println(4,other_spec_precompile).
2702
2703 ?is_precompiled_predicate(P) :- precompiled_predicate(P).
2704 ?is_precompiled_predicate(P) :- precompiled_predicate_phase2(P).
2705
2706 % phase 1 precompilation: required by b_global_sets
2707 precompiled_predicate(b_machine_name/1).
2708 precompiled_predicate(b_get_named_machine_set/3).
2709 precompiled_predicate(b_enumerated_sets_precompiled/0).
2710 precompiled_predicate(b_get_properties_from_machine/1).
2711 precompiled_predicate(b_get_machine_all_constants/1).
2712 precompiled_predicate(b_get_machine_set/2).
2713 precompiled_predicate(b_get_disjoint_constants_of_type/3).
2714 precompiled_predicate(b_get_constant_represented_inside_global_set/2).
2715 precompiled_predicate(b_get_machine_constants/1).
2716 precompiled_predicate(b_get_machine_variables_in_original_order/1).
2717 precompiled_predicate(b_get_machine_variables/1).
2718 precompiled_predicate(b_get_invariant_from_machine/1).
2719 precompiled_predicate(b_get_linking_invariant_from_machine/1).
2720 precompiled_predicate(b_is_constant/2).
2721 precompiled_predicate(b_is_variable/2).
2722 precompiled_predicate(b_get_constant_variable_description/2).
2723 precompiled_predicate(b_get_static_assertions_from_machine/1).
2724 precompiled_predicate(b_machine_has_static_assertions/0).
2725 precompiled_predicate(b_get_unproven_static_assertions_from_machine/1).
2726 precompiled_predicate(b_get_dynamic_assertions_from_machine/1).
2727 precompiled_predicate(b_machine_has_dynamic_assertions/0).
2728 precompiled_predicate(b_get_unproven_dynamic_assertions_from_machine/1).
2729 precompiled_predicate(b_get_assertions_from_main_machine/2).
2730 precompiled_predicate(b_get_initialisation_from_machine/2).
2731 precompiled_predicate(b_get_machine_operation/6).
2732 precompiled_predicate(b_top_level_operation/1).
2733 precompiled_predicate(b_is_operation_name/1).
2734 precompiled_predicate(b_top_level_feasible_operation/1).
2735 precompiled_predicate(b_get_promoted_machine_operations/1).
2736 precompiled_predicate(get_operation_info/2).
2737 precompiled_predicate(b_get_machine_operation_for_animation/7).
2738 precompiled_predicate(get_operation_description_template_expr/2).
2739 precompiled_predicate(b_get_machine_goal/1).
2740 precompiled_predicate(b_get_machine_setscope/2).
2741 precompiled_predicate(b_get_machine_operation_max/2).
2742 precompiled_predicate(b_get_machine_searchscope/1).
2743 precompiled_predicate(b_get_definition_string_from_machine/3).
2744 precompiled_predicate(b_get_machine_animation_function/2).
2745 precompiled_predicate(b_get_machine_heuristic_function/1).
2746 precompiled_predicate(b_get_machine_animation_expression/2).
2747 precompiled_predicate(b_get_machine_custom_nodes_function/2).
2748 precompiled_predicate(b_get_machine_custom_edges_function/2).
2749 precompiled_predicate(b_get_machine_custom_graph_function/2).
2750 precompiled_predicate(complete_discharged_info/0). % just call it before calling b_specialized_invariant_for_op_calc !
2751 precompiled_predicate(get_proven_invariant/2).
2752 precompiled_predicate(b_nth1_invariant/3).
2753 precompiled_predicate(b_invariant_number_list/1).
2754 precompiled_predicate(b_specialized_invariant_mask_for_op/2).
2755 precompiled_predicate(b_specialized_invariant_for_op/2).
2756 precompiled_predicate(b_operation_preserves_invariant/2).
2757 precompiled_predicate(b_get_all_used_identifiers_in_section/2).
2758 precompiled_predicate(b_get_all_used_identifiers/1).
2759 precompiled_predicate(b_is_unused_constant/1).
2760 precompiled_predicate(b_extract_values_clause_assignment/3). % depends on b_is_constant/1
2761 precompiled_predicate(b_machine_statistics/2).
2762
2763 % require b_global_sets to be initialised
2764 precompiled_predicate_phase2(b_get_operation_normalized_read_write_info/3).
2765 precompiled_predicate_phase2(b_get_operation_unchanged_variables/2).
2766 precompiled_predicate_phase2(b_operation_cannot_modify_state/1).
2767 precompiled_predicate_phase2(b_operation_reads_output_variables/3).
2768 precompiled_predicate_phase2(b_get_operation_non_det_modifies/2).
2769
2770 % these functions sometimes get called also in csp mode; simply fail silently for those cases in other_spec_precompile
2771 % they also get recompiled when new definition file is added
2772 precompiled_predicate_no_error_when_not_precompiled(b_get_machine_animation_function/2).
2773 precompiled_predicate_no_error_when_not_precompiled(b_get_machine_heuristic_function/1).
2774 precompiled_predicate_no_error_when_not_precompiled(b_get_machine_animation_expression/2).
2775 precompiled_predicate_no_error_when_not_precompiled(b_get_machine_custom_nodes_function/2).
2776 precompiled_predicate_no_error_when_not_precompiled(b_get_machine_custom_edges_function/2).
2777 precompiled_predicate_no_error_when_not_precompiled(b_get_machine_custom_graph_function/2).
2778
2779 % on startup, all precompiled predicates yield error message
2780 startup_precompiled :- retractall(bmachine_is_precompiled),
2781 ? is_precompiled_predicate(Pred/Arity),
2782 functor(Pattern,Pred,Arity),
2783 retractall(Pattern),
2784 assertz( (Pattern :- add_error(bmachine,'B machine not precompiled for ',Pattern),fail) ),
2785 fail.
2786 startup_precompiled :- debug_println(4,startup_precompiled).
2787
2788 :- startup_precompiled.
2789
2790 % for each predicate in "precompiled_predicate", auto_precompile computes
2791 % all solutions by calling the predicate with an appended _calc
2792 auto_precompile :- % startup_precompiled,
2793 % failure-driven loop
2794 ? precompiled_predicate(Pred/Arity), %print(precompile(Pred/Arity)),nl,
2795 %statistics(walltime,[Tot,Delta]), format('Precompiling ~w/~w [~w ms (Delta ~w) ms]~n',[Pred,Arity,Tot,Delta]),
2796 ? auto_precompile2(Pred,Arity,Pattern),
2797 (Pattern -> true /* this pattern already asserted */
2798 ; assertz(Pattern)), fail.
2799 auto_precompile :-
2800 assert_bmachine_is_precompiled, debug_println(4,auto_precompile).
2801 auto_precompile_phase2 :-
2802 % failure-driven loop
2803 ? precompiled_predicate_phase2(Pred/Arity), %print(precompile(Pred/Arity)),nl,
2804 ? auto_precompile2(Pred,Arity,Pattern),
2805 (Pattern -> true /* this pattern already asserted */
2806 ; assertz(Pattern)), fail.
2807 auto_precompile_phase2.
2808
2809 % if the precompiled predicates is e.g. foo/2 then
2810 % Pattern=foo(A,B) and Call=foo_calc(A,B)
2811 auto_precompile2(Pred,Arity,Pattern) :-
2812 atom_concat(Pred,'_calc',CallFunctor),
2813 functor(Pattern,Pred,Arity),
2814 functor(Call,CallFunctor,Arity),
2815 unify_args(Arity,Call,Pattern),
2816 retractall(Pattern), % probably just removes clause added by startup_precompiled
2817 % the failure-driven loop for one predicate
2818 ? call(Call).
2819
2820 unify_args(0,_,_) :- !.
2821 unify_args(N,A,B) :-
2822 arg(N,A,Arg), arg(N,B,Arg),
2823 N1 is N-1, unify_args(N1,A,B).
2824
2825
2826 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2827 % set machine goal
2828
2829 b_set_machine_goal(Goal) :- b_set_machine_goal(Goal,false).
2830 b_set_machine_goal(Goal,WithDeferredSets) :-
2831 get_tc_scope(WithDeferredSets,Scope),
2832 b_parse_machine_predicate(Goal,Scope,TypedPred),
2833 b_set_parsed_typed_machine_goal(TypedPred).
2834
2835 b_set_parsed_typed_machine_goal(TypedPred) :-
2836 retractall(b_get_machine_goal(_)),
2837 assertz(b_get_machine_goal(TypedPred)).
2838
2839 b_unset_machine_goal :-
2840 retractall(b_get_machine_goal(_)).
2841
2842
2843 % get typechecking scope:
2844 get_tc_scope(with_deferred,Scope) :- !,
2845 Scope = [prob_ids(visible),variables,external_library(all_available_libraries)].
2846 % with external libraries we can use e.g. GET_IS_DET_OUTPUT("OpName")=FALSE
2847 get_tc_scope(with_deferred_and_primed,Scope) :- !,
2848 get_primed_machine_variables(PV), % this can be useful for visualisation, but will not work during mc
2849 Scope = [prob_ids(visible),identifier(PV),variables,external_library(all_available_libraries)].
2850 get_tc_scope(_,[variables]).
2851
2852 % set search_scope, restricting model checking to states which satisfy the SCOPE DEFINITION predicate
2853 b_set_machine_searchscope(Goal) :- b_set_machine_searchscope(Goal,with_deferred).
2854 b_set_machine_searchscope(Goal,WithDeferredSets) :-
2855 get_tc_scope(WithDeferredSets,Scope),
2856 b_parse_machine_predicate(Goal,Scope,TypedPred),
2857 b_set_parsed_typed_machine_searchscope(TypedPred).
2858 b_set_parsed_typed_machine_searchscope(TypedPred) :-
2859 retractall(b_get_machine_searchscope(_)),
2860 assertz(b_get_machine_searchscope(TypedPred)).
2861
2862 % also allow empty string, and #invariant and #not_invariant
2863 b_parse_optional_machine_predicate(TargetString,Target) :-
2864 is_empty_string(TargetString),!,create_texpr(truth,pred,[],Target).
2865 b_parse_optional_machine_predicate('#invariant',Invariant) :- !,
2866 b_get_invariant_from_machine(Invariant).
2867 b_parse_optional_machine_predicate('#not_invariant',TargetPredicate) :- !,
2868 b_get_invariant_from_machine(Invariant),
2869 bsyntaxtree:create_negation(Invariant,TargetPredicate).
2870 b_parse_optional_machine_predicate(TargetString,Target) :-
2871 b_parse_machine_predicate(TargetString,Target).
2872
2873 is_empty_string(Atom) :-
2874 atom_codes(Atom,Codes),
2875 is_empty_string2(Codes).
2876 is_empty_string2([]).
2877 is_empty_string2([32|Codes]) :- is_empty_string2(Codes).
2878
2879
2880 % parsing a string as predicate with deferred set elements
2881 b_parse_machine_predicate(Pred,TypedPred) :- b_parse_machine_predicate(Pred,[variables],TypedPred).
2882 b_parse_machine_predicate(Pred,Scope,TypedPred) :-
2883 atom_codes(Pred,Codes),
2884 b_parse_machine_predicate_from_codes(Codes,Scope,TypedPred).
2885 b_parse_machine_predicate_from_codes(Codes,Scope,TypedPred) :-
2886 b_parse_machine_predicate_from_codes2(Codes,[],Scope,TypedPred,closed).
2887 b_parse_machine_predicate_from_codes_open(OptionalQuantifier,Codes,Defs,Scope,TypedPred) :-
2888 b_parse_machine_predicate_from_codes2(Codes,Defs,Scope,TypedPred,open(OptionalQuantifier)).
2889
2890 b_parse_machine_predicate_from_codes2(Codes,Defs,Scope,TypedPred,Mode) :-
2891 debug_println(9,parse_predicate(Mode)),
2892 (Defs=[] -> true ; debug_println(9,'% Ignoring DEFINITIONS')),
2893 b_parse_wo_type_machine_predicate_from_codes_to_raw_expr(Codes,Parsed),
2894 %format('Raw Parsed AST = ~w~n',[Parsed]),
2895 b_type_check_raw_expr(Parsed,Scope,TypedPred,Mode).
2896
2897 check_codes(X) :- (X=[] ; X=[H|_], number(H)),!.
2898 check_codes(X) :- add_error(bmachine,'Error while parsing: not a code list: ',X),fail.
2899
2900 b_parse_wo_type_machine_predicate_from_codes_to_raw_expr(Codes,ParsedRaw) :-
2901 check_codes(Codes),
2902 catch(
2903 parse_predicate(Codes,ParsedRaw), % ,print(ParsedRaw),nl),
2904 Exception,
2905 ( Exception = parse_errors(Errors) -> %print(errors(Errors)),nl,
2906 add_all_perrors(Errors,[],parse_machine_predicate_error),fail
2907 ;
2908 add_error(bmachine,'Exception while parsing predicate: ',Exception),
2909 fail)).
2910
2911 b_type_check_raw_expr(ParsedRaw,Scope,TypedPred,Mode) :-
2912 debug_println(9,type_with_errors(ParsedRaw)),
2913 ( Mode == closed ->
2914 type_with_errors(ParsedRaw,Scope,pred,TypedPred)
2915 ; Mode = open(OptionalQuantifier) ->
2916 b_type_open_predicate_with_errors(OptionalQuantifier,ParsedRaw,Scope,TypedPred)).
2917
2918 % a flexible version: convert atom to codes, but also accept codes list
2919 flexible_atom_codes([],R) :- !, R=[].
2920 flexible_atom_codes(A,R) :- atom(A), !, atom_codes(A,R).
2921 flexible_atom_codes([H|T],List) :- !, List=[H|T].
2922 flexible_atom_codes(Other,List) :- add_internal_error('Not atom or codes list: ',flexible_atom_codes(Other,List)),
2923 List=Other.
2924
2925 b_parse_machine_operation_pre_post_predicate(AtomOrCodes,TypedPred,OpName) :-
2926 b_parse_machine_operation_pre_post_predicate(AtomOrCodes,[],TypedPred,OpName,true).
2927 b_parse_machine_operation_pre_post_predicate(AtomOrCodes,ExtraScope,TypedPred,OpName,GenerateParseErrors) :-
2928 flexible_atom_codes(AtomOrCodes,Codes),
2929 b_parse_predicate(Codes,Parsed,GenerateParseErrors),
2930 get_machine_operation_typing_scope(OpName,Scope,ExtraScope),
2931 b_type_only(Parsed,Scope,pred,TypedPred,GenerateParseErrors).
2932
2933 % Note: B and Event-B have different way of priming; this is aimed at classical B
2934 % and supposes predicate used together with execute_operation_by_predicate_in_state
2935 % in classical B x$0 refers to the value before a substitution (e.g., becomes_such)
2936 get_primed_machine_variables(Ids) :-
2937 b_get_machine_variables(Vars),
2938 maplist(prime_variable,Vars,Ids).
2939 :- use_module(btypechecker,[prime_atom0/2]). % add $0 at end of variable
2940 prime_variable(b(identifier(ID),T,I),b(identifier(PID),T,I)) :- prime_atom0(ID,PID).
2941
2942 is_initialisation_op('$setup_constants').
2943 is_initialisation_op('$initialise_machine').
2944
2945 % analog version to b_is_operation_name:
2946 b_is_initialisation_name('$initialise_machine').
2947
2948
2949 get_machine_operation_typing_scope(OpName,Scope,ExtraScope) :-
2950 ( get_machine_operation_additional_identifiers(OpName,V) -> true
2951 ; add_error_fail(get_machine_operation_typing_scope,'Unknown operation:', OpName)),
2952 Scope = [prob_ids(visible),identifier(V),variables,external_library(all_available_libraries)|ExtraScope].
2953
2954 % get additional ids to add to Scope for typing with identifier(V)
2955 get_machine_operation_additional_identifiers(OpName,V) :-
2956 is_initialisation_op(OpName),!, V=[].
2957 get_machine_operation_additional_identifiers(OpName,V) :-
2958 b_get_machine_operation_for_animation(OpName,Results,Paras,_),
2959 append(Paras,Results,PR), % b_get_machine_operation_typed_parameters
2960 get_primed_machine_variables(PV),
2961 append(PV,PR,V).
2962
2963 b_get_machine_operation_for_animation(Name,Results,Parameters,Body) :-
2964 ? b_get_machine_operation_for_animation(Name,Results,Parameters,Body,_OType,true).
2965 % interface predicate b_get_machine_operation_for_animation/6
2966 b_get_machine_operation_for_animation(Name,Results,Parameters,Body,OType,TopLevel) :-
2967 ? b_get_machine_operation_for_animation(Name,Results,Parameters,Body,OType,TopLevel,_OpPos).
2968
2969 :- public b_get_machine_operation_for_animation_calc/7.
2970 % adds some additional ANY parameters if preference is set
2971 b_get_machine_operation_for_animation_calc('$initialise_machine',[],Parameters,Body,OType,_TopLevel,OpPos) :-
2972 b_get_machine_variables(DeclaredVars), Parameters=DeclaredVars,
2973 OpPos = unknown, % TODO: improve
2974 b_get_initialisation_from_machine(Body,OType).
2975 b_get_machine_operation_for_animation_calc(Name,Results,Parameters,Body,OType,TopLevel,OpPos) :-
2976 get_preference(show_eventb_any_arguments,EVENTB),
2977 ? b_get_machine_operation(Name,Results,RealParameters,RealBody,OType,OpPos),
2978 % TO DO: check whether we should only keep b_top_level_operation(Name) in case TopLevel==true !
2979 %length(RealParameters,P), format('Get Mach Op ~w ; paras ~w ; EB ~w, TopLevel=~w~n',[Name,P,EVENTB,TopLevel]),
2980 ((Results=[_|_] ; RealParameters=[_|_] ; EVENTB=false)
2981 -> Parameters=RealParameters, Body=RealBody
2982 ; translate_any_into_parameters(RealBody,FakeParameters,FakeBody),
2983 length(FakeParameters,Len),
2984 (Len > 255
2985 -> add_message(bmachine,'Not adding any parameters to operation, max_arity (255) exceeded: ',Name:Len,OpPos),
2986 Parameters=RealParameters, Body=RealBody
2987 ; ( TopLevel=true, Parameters=FakeParameters, Body=FakeBody
2988 ; TopLevel=false, Parameters=RealParameters, Body=RealBody
2989 )
2990 )
2991 ; Parameters=RealParameters, Body=RealBody
2992 ).
2993
2994 % TO DO: limit to max_arity
2995 translate_any_into_parameters(b(E,Type,Info),Parameters,NewSubst) :-
2996 translate_any_into_parameters_aux(E,Type,Info,Parameters,NewSubst).
2997 translate_any_into_parameters_aux(any(Parameters,PreCond,ABody),Type,Info,Parameters,NewSubst) :-
2998 NewSubst=b(select([b(select_when(PreCond,ABody),Type,Info)]),Type,Info). % TO DO: go deeper ? (nested ANY ?)
2999 translate_any_into_parameters_aux(let(Parameters,Defs,LBody),Type,Info,Parameters,NewSubst) :-
3000 NewSubst=b(select([b(select_when(Defs,LBody),Type,Info)]),Type,Info). % TO DO: go deeper ? ANY could have been translated into several LETs ?
3001 translate_any_into_parameters_aux(lazy_let_subst(Id,IdExpr,Body),Type,Info,Parameters,NewSubst) :-
3002 NewSubst=b(lazy_let_subst(Id,IdExpr,NewInnerSubst),Type,Info),
3003 translate_any_into_parameters(Body,Parameters,NewInnerSubst).
3004
3005
3006 % add deferred set prob_ids and external libraries as well
3007 % ExtraScope could e.g. be [identifier(TypedIDLIst)]
3008 b_parse_machine_expression_from_codes_with_prob_ids(Codes,ExtraScope,TypedExpr,GenerateParseErrors) :-
3009 extend_typing_scope_for_stored_lets([prob_ids(visible),variables,
3010 external_library(all_available_libraries)|ExtraScope],
3011 Scope),
3012 b_parse_machine_expression_from_codes4(Codes,Scope,TypedExpr,GenerateParseErrors).
3013 b_parse_machine_expression_from_codes_with_prob_ids(Codes,ExtraScope,TypedExpr) :-
3014 b_parse_machine_expression_from_codes_with_prob_ids(Codes,ExtraScope,TypedExpr,true).
3015 b_parse_machine_expression_from_codes_with_prob_ids(Codes,TypedExpr) :-
3016 b_parse_machine_expression_from_codes_with_prob_ids(Codes,[],TypedExpr,true).
3017
3018 b_parse_machine_expression_from_codes(Codes,TypedExpr) :-
3019 b_parse_machine_expression_from_codes4(Codes,[variables],TypedExpr,true).
3020
3021 b_parse_machine_expression_from_codes4(Codes,Scope,TypedExpr,GenerateParseErrors) :-
3022 b_parse_machine_expression_from_codes(Codes,Scope,TypedExpr,_Type,GenerateParseErrors,Error),!,
3023 (Error=none -> true
3024 ; generate_parse_errors_for(GenerateParseErrors,Position,ErrOrWarn),
3025 add_msg_warn_or_err(ErrOrWarn,b_parse_machine_expression_from_codes,
3026 'Errors occured during parsing:', Error,Position),
3027 % format(user_error,'Parsing: ~s~n',[Codes]),
3028 fail).
3029
3030
3031 %b_parse_machine_expression_from_codes(Codes,TypedExpr) :-
3032 % b_parse_machine_expression_from_codes(Codes,TypedExpr,_Type,false,Error), Error=none.
3033
3034 b_parse_machine_expression_from_codes(Codes,Typed,Type,GenerateParseErrors,Error) :-
3035 b_parse_machine_expression_from_codes(Codes,[variables],
3036 Typed,Type,GenerateParseErrors,Error).
3037 b_parse_machine_expression_from_codes(Codes,Scope,
3038 Typed,Type,GenerateParseErrors,Error) :-
3039 b_parse_machine_formula_from_codes(expression,Codes,Scope,
3040 Typed,Type,GenerateParseErrors,Error).
3041
3042 % parse substitutions so as to allow operation calls; useful for REPL or trace files:
3043 b_parse_machine_subsitutions_from_codes(Codes,Scope,
3044 Typed,Type,GenerateParseErrors,Error) :-
3045 temporary_set_preference(allow_local_operation_calls,true,CHNG),
3046 call_cleanup(
3047 b_parse_machine_formula_from_codes(substitution,Codes,Scope,
3048 Typed,Type,GenerateParseErrors,Error),
3049 reset_temporary_preference(allow_local_operation_calls,CHNG)).
3050
3051 % a variant of b_parse_machine_predicate that allows also expressions
3052 b_parse_machine_formula(PredOrExpr,Scope,TypedPredOrExpr) :-
3053 atom_codes(PredOrExpr,Codes),
3054 b_parse_machine_formula_from_codes(formula,Codes,Scope,
3055 TypedPredOrExpr,_Type,true,Error), Error=none.
3056
3057 % Kind = expression, predicate, formula, substitution
3058 % GnerateParseErrors = true, false, type_errors_only, gen_parse_errors_for/2
3059 b_parse_machine_formula_from_codes(Kind,Codes,Scope,
3060 Typed,Type,GenerateParseErrors,Error) :-
3061 b_parse_only(Kind,Codes, ParsedAST, GenerateParseErrors, Error),
3062 %print(parsed(Parsed,Error)),nl,
3063 ( nonvar(Error) -> true /* either exception or parse error occured */
3064 ; generate_no_parse_errors(GenerateParseErrors), type_without_errors(ParsedAST,Scope,Type,Typed) -> Error=none
3065 ; b_type_only(ParsedAST,Scope,Type,Typed,GenerateParseErrors) -> Error=none
3066 ; Error=type_error).
3067
3068 % typing with or without errors, depending on GenerateParseErrors flag
3069 b_type_only(ParsedAST,Scope,Type,Typed,GenParseErrors) :-
3070 generate_parse_errors_for(GenParseErrors,_Pos,ErrOrWarn),!,
3071 % ParsedAST now contains filenumber for additional file
3072 type_with_errors_in_context(ParsedAST,Scope,Type,Typed,machine_context,ErrOrWarn).
3073 b_type_only(ParsedAST,Scope,Type,Typed,false) :- !,
3074 type_without_errors(ParsedAST,Scope,Type,Typed).
3075 b_type_only(ParsedAST,Scope,Type,Typed,_GenerateParseErrors) :-
3076 type_with_errors_in_context(ParsedAST,Scope,Type,Typed,no_machine_context([]),error).
3077
3078 % GenerateParseErrors can also provide context filename
3079 b_parse_predicate(Codes,ParsedAST,GenerateParseErrors) :-
3080 b_parse_only(predicate,Codes, ParsedAST, GenerateParseErrors,Error),
3081 Error=none.
3082
3083 b_parse_only(Kind,Codes, ParsedAST, _,Error) :- (Codes \= [] , Codes \= [_|_]),!,
3084 add_internal_error('Not a codes list: ',b_parse_only(Kind,Codes, ParsedAST, _, Error)),
3085 Error = internal_error.
3086 b_parse_only(Kind,Codes, ParsedAST, GenerateParseErrors,Error) :-
3087 generate_parse_errors_for(GenerateParseErrors,Position,ErrOrWarn),!,
3088 % we should generate errors in a particular file context
3089 (extract_file_number_and_name(Position,FileNr,Filename)
3090 -> Files=[Filename] ; FileNr = -1, Files=[]),
3091 (number(FileNr) -> NewFileNr=FileNr ; add_additional_filename(Filename,NewFileNr)),
3092 catch( parse_at_position_in_file(Kind,Codes,ParsedAST,Position,NewFileNr),
3093 Exception,
3094 ((Exception = parse_errors(Errors) ->
3095 add_all_perrors(Errors,Files,parse_machine_formula_error,ErrOrWarn),
3096 Error=parse_error
3097 ;
3098 ajoin(['Exception while parsing ',Kind,': '],Msg),
3099 add_msg_warn_or_err(ErrOrWarn,bmachine,Msg,Exception,Position),
3100 Error=exception))).
3101 b_parse_only(Kind,Codes, ParsedAST, _GenerateParseErrors,_Error) :-
3102 catch( parse(Kind,Codes,ParsedAST),
3103 Exception,
3104 (debug_println(19,parse_exception(Exception)),fail)).
3105
3106 %generate_type_errors_for(type_errors_only,unknown,[]).
3107 %generate_type_errors_for(GenerateParseErrors,Pos) :- generate_parse_errors_for(GenerateParseErrors,Pos).
3108
3109 generate_parse_errors_for(true,unknown,error).
3110 generate_parse_errors_for(gen_parse_errors_for(Pos),Pos,error).
3111 generate_parse_errors_for(gen_parse_warnings_for(Pos),Pos,warning).
3112
3113 generate_no_parse_errors(false).
3114
3115 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3116
3117 % a flexible parsing predicate, useful for dot and table tools to be called from
3118 % either probcli or prob2 with either atoms or with raw ASTs:
3119
3120 :- use_module(eval_let_store,[extend_typing_scope_for_stored_lets/2]).
3121 parse_expression_raw_or_atom_with_prob_ids(Expr,TypedExpr) :-
3122 extend_typing_scope_for_stored_lets([prob_ids(visible),variables,external_library(all_available_libraries)],Scope),
3123 parse_expression_raw_or_atom3(Expr,Scope,TypedExpr).
3124
3125 parse_expression_raw_or_atom3('$VARIABLES',_,TypedExpr) :- !,
3126 b_get_machine_variables(DeclaredVars),
3127 gen_couple_from_list(DeclaredVars,TypedExpr).
3128 parse_expression_raw_or_atom3(RawAST,Scope,TypedExpr) :- compound(RawAST),!, % allow to pass raw AST as well
3129 type_with_errors(RawAST,Scope,Type,TypedExpr),
3130 ((Type=pred ; Type=subst)
3131 -> add_error(parse_expression,'Expected expression formula but obtained: ',Type),fail
3132 ; true ).
3133 parse_expression_raw_or_atom3(VorE,Scope,TypedExpr) :-
3134 atom_codes(VorE,VorECodes),
3135 % to do: maybe support b_parse_machine_expression_from_codes_with_prob_ids
3136 b_parse_machine_expression_from_codes4(VorECodes,Scope,TypedExpr,true).
3137
3138 :- use_module(bsyntaxtree, [create_couple/3]).
3139 gen_couple_from_list([],string('NO VARIABLES')).
3140 gen_couple_from_list([TID],Res) :- !, Res=TID.
3141 gen_couple_from_list([TID|T],Couple) :-
3142 gen_couple_from_list(T,Rest),
3143 create_couple(TID,Rest,Couple).
3144
3145
3146 :- use_module(btypechecker,[prime_atom0/2]). % add $0 at end of variable
3147 :- use_module(bsyntaxtree, [find_typed_identifier_uses/2,get_texpr_id/2]).
3148 % compute requirements for evaluating formula
3149 % requires_nothing, requires_constants, requires_variables
3150 determine_type_of_formula(TypedExpr,Class) :-
3151 determine_type_of_formula(TypedExpr,_,Class).
3152 determine_type_of_formula(TypedExpr,Identifiers,Class) :-
3153 find_typed_identifier_uses(TypedExpr,Identifiers),
3154 determine_type_of_formula2(Identifiers,Class).
3155 determine_type_of_formula2([],Res) :- !, Res = requires_nothing.
3156 determine_type_of_formula2(Ids,Res) :-
3157 ? member(TID,Ids), get_texpr_id(TID,ID),
3158 (b_is_variable(ID,_) -> true
3159 ; prime_atom0(Original,ID),
3160 (b_is_variable(Original,_) -> true ; add_warning(bmachine,'Unknown primed variable: ',ID))
3161 ),
3162 !, Res = requires_variables.
3163 determine_type_of_formula2(Ids,Res) :-
3164 ? member(TID,Ids), get_texpr_id(TID,ID),
3165 b_is_constant(ID,_),
3166 !, Res = requires_constants.
3167 determine_type_of_formula2(_,requires_nothing).
3168 % only open, implicitly existentially quantified variables
3169 % also, TO DO: check that insert_before_substitution_variables / $0 variables are properly treated
3170 % TODO: there are external functions like ENABLED(.) which implicitly require a state with variables
3171
3172 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3173 % consistency check to spot some errors
3174 do_machine_consistency_check :-
3175 specfile:animation_mode(b), % TODO (dp,27.09.2012): this is just an ugly hack
3176 type_check_definitions,
3177 ? minor_mode_to_check,
3178 %debug:time(bmachine:all_operations_have_valid_read_modifies_infos).
3179 !,
3180 all_operations_have_valid_read_modifies_infos.
3181 do_machine_consistency_check.
3182
3183 % In future, all formalisms should provide the relevent data
3184 minor_mode_to_check :- animation_minor_mode(eventb),!.
3185 ?minor_mode_to_check :- classical_b_mode.
3186
3187 all_operations_have_valid_read_modifies_infos :-
3188 %findall(O,b_get_machine_operation(O,_,_,_,_),OpNames),
3189 %maplist(operation_has_valid_read_modifies_infos,OpNames).
3190 ? b_get_operation_pos(OpName,Pos),
3191 operation_has_valid_read_modifies_infos(OpName,Pos),fail.
3192 all_operations_have_valid_read_modifies_infos.
3193
3194 operation_has_valid_read_modifies_infos(OpName,Pos) :- % print(check(OpName)),nl,
3195 ( operation_has_valid_read_modifies_infos2(OpName,Pos) -> true
3196 ; add_failed_call_error(operation_has_valid_read_modifies_infos2(OpName,Pos))).
3197 operation_has_valid_read_modifies_infos2(OpName,Pos) :-
3198 b_get_operation_normalized_read_write_info(OpName,Reads,Writes),
3199 maplist(check_read(OpName,Pos),Reads),
3200 %print(operation(OpName,reads(Reads),writes(Writes))),nl,
3201 maplist(check_write(OpName,Pos),Writes).
3202
3203
3204 :- use_module(translate,[translate_span_with_filename/2]).
3205 :- use_module(bmachine_construction,[abstract_variable_removed_in/3]).
3206 check_read(OpName,Pos,Id) :-
3207 ? ( (check_is_var(Id); check_is_constant(Id) ; check_is_operation(Id)) -> true
3208 ; abstract_variable_removed_in(Id,Mch,TId) ->
3209 translate_span_with_filename(TId,SP),
3210 ajoin(['Operation reads invisible abstract variable `',Id,'` ',SP,', removed in ',Mch,':'],Msg),
3211 % this shows that in that refinement step we removed a variable without adapting an operation
3212 add_error(bmachine,Msg,OpName,Pos)
3213 ;
3214 ajoin(['Unknown identifier `',Id,'` in "reads" information of operation:'],Msg),
3215 add_internal_error(bmachine,Msg,OpName,Pos)).
3216 check_write(OpName,Pos,Id) :-
3217 ( check_is_var(Id) -> true
3218 ; abstract_variable_removed_in(Id,Mch,TId) ->
3219 translate_span_with_filename(TId,SP),
3220 ajoin(['Operation writes invisible abstract variable `',Id,'` ',SP,', removed in ',Mch,':'],Msg),
3221 % this shows that in that refinement step we removed a variable without adapting an operation
3222 add_error(bmachine,Msg,OpName,Pos)
3223 ;
3224 ajoin(['Unknown variable `',Id,'` in "modifies" information of operation:'],Msg),
3225 add_internal_error(bmachine,Msg,OpName,Pos)).
3226
3227 check_is_var(Id) :-
3228 b_is_variable(Id,_).
3229 %get_texpr_id(E,Id),
3230 %b_get_machine_variables(Vars),
3231 %memberchk(E,Vars).
3232 check_is_constant(Id) :- b_is_constant(Id,_).
3233 check_is_constant(Id) :- b_get_constant_represented_inside_global_set(Id,_).
3234 % b_get_machine_all_constants(Constants),
3235 % get_texpr_id(TId,Id),
3236 % memberchk(TId,Constants).
3237 check_is_constant(Id) :- b_get_machine_set(Id).
3238 check_is_constant(Id) :- b_get_named_machine_set(Id,_).
3239 check_is_constant(Id) :-
3240 b_get_named_machine_set(_,Elems),member(Id,Elems).
3241 %check_is_constant(Id) :- % add later when we deal FREETYPE section in classical B as in Z
3242 % kernel_freetypes:freetype_register_db(Id,_) ;
3243 % kernel_freetypes:freetype_case_db(Id,_,_).
3244
3245 check_is_operation(op(ID)) :-
3246 b_is_operation_name(ID), % TO DO: check that other predicates can deal with op(Id) infos
3247 get_preference(allow_operation_calls_in_expr,true).
3248
3249 % provide access to number of constants, ....:
3250
3251 :- volatile b_machine_statistics/2.
3252 :- dynamic b_machine_statistics/2.
3253 :- public b_machine_statistics_calc/2.
3254 b_machine_statistics_calc(files,Nr) :-
3255 b_get_all_used_filenames(L),length(L,Nr).
3256 b_machine_statistics_calc(deferred_sets,Nr) :-
3257 get_section_from_current_machine(deferred_sets,L),length(L,Nr).
3258 b_machine_statistics_calc(enumerated_sets,Nr) :-
3259 get_section_from_current_machine(enumerated_sets,L),length(L,Nr).
3260 b_machine_statistics_calc(definitions,Nr) :-
3261 get_section_from_current_machine(definitions,L),length(L,Nr).
3262 b_machine_statistics_calc(constants,Nr) :- b_get_machine_constants(L), length(L,Nr).
3263 b_machine_statistics_calc(variables,Nr) :- b_get_machine_variables(L), length(L,Nr).
3264 b_machine_statistics_calc(properties,Nr) :-
3265 b_get_properties_from_machine(C), conjunction_to_list(C,L),length(L,Nr).
3266 b_machine_statistics_calc(invariants,Nr) :-
3267 b_get_invariant_from_machine(C), conjunction_to_list(C,L),length(L,Nr).
3268 b_machine_statistics_calc(static_assertions,Nr) :-
3269 b_get_static_assertions_from_machine(L), length(L,Nr).
3270 b_machine_statistics_calc(dynamic_assertions,Nr) :-
3271 b_get_dynamic_assertions_from_machine(L), length(L,Nr).
3272 b_machine_statistics_calc(operations,Nr) :- findall(N,b_is_operation_name(N),L),length(L,Nr).
3273
3274 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3275 % default and initial machines
3276 b_set_initial_machine :-
3277 initial_machine(Main,Machines),
3278 b_set_machine(Main,Machines,[]).
3279
3280 initial_machine(phonebook,[M]) :-
3281 M = abstract_machine(none,machine(none),machine_header(none,phonebook,[]),Body),
3282 Body = [sets(none, [deferred_set(none,'Name'),
3283 deferred_set(none,'Code')]),
3284 definitions(none,[ScopeName,ScopeCode,TraceTest0]),
3285 variables(none, [identifier(none, db)]),
3286 invariant(none, member(none,
3287 identifier(none, db),
3288 partial_function(none,
3289 identifier(none, 'Name'),
3290 identifier(none, 'Code')))),
3291 initialisation(none,
3292 assign(none, [identifier(none, db)], [empty_set(none)])),
3293 operations(none, [Add,Lookup,Update,Reset])],
3294
3295 % definitions
3296 ScopeName = expression_definition(none,
3297 scope_Name,
3298 [],
3299 interval(none, integer(none, 1), integer(none, 3))),
3300 ScopeCode = expression_definition(none,
3301 scope_Code,
3302 [],
3303 interval(none, integer(none, 1), integer(none, 2))),
3304 TraceTest0 = expression_definition(none, trace_Test0, [], empty_sequence(none)),
3305
3306 % add operation
3307 Add = operation(none,
3308 identifier(none, add),
3309 [],
3310 [identifier(none,cc),identifier(none,nn)],
3311 precondition(none, AddPre, AddAssign)),
3312 AddPre = conjunct(none,
3313 conjunct(none,
3314 member(none, identifier(none,nn), identifier(none,'Name')),
3315 member(none, identifier(none,cc), identifier(none,'Code'))),
3316 not_member(none,
3317 identifier(none,nn),
3318 domain(none, identifier(none,db)))),
3319 AddAssign = assign(none,
3320 [identifier(none,db)],
3321 [union(none,
3322 identifier(none,db),
3323 set_extension(none,
3324 [couple(none,[identifier(none,nn),
3325 identifier(none,cc)])]))]),
3326
3327 % lookup operation
3328 Lookup = operation(none,
3329 identifier(none, lookup),
3330 [identifier(none, cc)],
3331 [identifier(none, nn)],
3332 precondition(none, LookupPre, LookupAssign)),
3333 LookupPre = member(none, identifier(none,nn), domain(none,identifier(none,db))),
3334 LookupAssign = assign(none,
3335 [identifier(none, cc)],
3336 [function(none, identifier(none, db), identifier(none, nn))]),
3337
3338 % update operation
3339 Update = operation(none,
3340 identifier(none, update),
3341 [],
3342 [identifier(none,nn),identifier(none,cc)],
3343 precondition(none, UpdatePre, UpdateAssign)),
3344 UpdatePre = conjunct(none,
3345 conjunct(none,
3346 member(none, identifier(none,nn), identifier(none,'Name')),
3347 member(none, identifier(none,cc), identifier(none,'Code'))),
3348 member(none,
3349 identifier(none,nn),
3350 domain(none, identifier(none,db)))),
3351 UpdateAssign = assign(none,
3352 [function(none, identifier(none,db), identifier(none,nn))],
3353 [identifier(none, cc)]),
3354
3355 % reset operation
3356 Reset = operation(none,
3357 identifier(none,reset),
3358 [],
3359 [],
3360 precondition(none, ResetPre, ResetAssign)),
3361 ResetPre = member(none,
3362 identifier(none, db),
3363 total_function(none, identifier(none,'Name'), identifier(none,'Code'))),
3364 ResetAssign = assign(none,[identifier(none,db)],[empty_set(none)]).
3365
3366 empty_machine(empty_machine,[M]) :-
3367 M = abstract_machine(none,machine(none),machine_header(none,empty_machine,[]),Body),
3368 Body = [].
3369
3370 % after transformation this gives
3371 % machine(empty_machine,[deferred_sets/[],enumerated_sets/[],enumerated_elements/[],parameters/[],internal_parameters/[],abstract_constants/[],concrete_constants/[],abstract_variables/[],concrete_variables/[],promoted/[],unpromoted/[],(constraints)/b(truth,pred,[]),properties/b(truth,pred,[initial]),invariant/b(truth,pred,[initial]),linking_invariant/b(truth,pred,[initial]),assertions/[],initialisation/b(skip,subst,[generated]),operation_bodies/[],definitions/[],used/[],freetypes/[],operators/[],values/[],meta/[model_type/machine,hierarchy/[empty_machine],header_pos/[empty_machine/none]]])
3372
3373 % Code to inspect sizes of operations:
3374 % findall(op(Sz,Op),(bmachine:b_get_machine_operation_for_animation(Op,_,_,Body,_,_Top), terms:term_size(Body,Sz)),L), sort(L,SL), print(SL),nl.