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