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		write(file(File)),nl, write(Directory),nl,
1242		safe_absolute_file_name(File,AbsFileName,[relative_to(Directory)]).
1243
1244		get_main_file_name_aux(MainFileName) :- b_or_z_mode, !, b_get_main_filename(MainFileName).
1245		get_main_file_name_aux(MainFileName) :- xtl_mode, !, xtl_interface:xtl_main_file_name(MainFileName).
1246
1247		% call to clear all data stored for machine
1248		b_machine_clear :-
1249		b_machine_reset,
1250		b_reset_filenames_and_numbers.
1251
1252		:- use_module(btypechecker,[reset_typechecker/0]).
1253		:- use_module(b_global_sets,[b_clear_global_set_type_definitions/0]).
1254		:- use_module(bmachine_construction,[reset_bmachine_construction/0]).
1255		b_machine_reset :- % print(b_machine_reset),nl,
1256		retractall(machine(_,_)),
1257		retractall(additional_configuration_machine(_,_)),
1258		retractall(discharged_theorem(_,_,_)),
1259		retractall(discharged_guard_strengthening(_,_,_,_)),
1260		retractall(discharged(_,_,_)),
1261		retractall(wd_po(_,_,_)),
1262		retractall(also_discharged(_,_,_)),
1263		reset_temp_predicate,
1264		retractall(b_machine_additional_property(_)),
1265		reset_typechecker,
1266		b_clear_global_set_type_definitions,
1267		reset_bmachine_construction,
1268		startup_precompiled. % change so that error messages generated if we call them
1269
1270		:- use_module(eventhandling,[register_event_listener/3]).
1271		:- register_event_listener(clear_specification,b_machine_clear,
1272		'Reset bmachine facts.').
1273
1274		% :- use_module(library(random)).
1275		:- use_module(preferences,[get_preference/2]).
1276
1277
1278
1279
1280		% precompiled
1281		:- volatile b_machine_name/1.
1282		:- dynamic b_machine_name/1.
1283		:- public b_machine_name_calc/1.
1284		b_machine_name_calc(Name) :-
1285		get_full_b_machine(Name,_).
1286
1287		b_get_animated_sections(Sections) :-
1288		get_section_from_current_machine(meta,MetaInfos),
1289		( member(animated_sections(Sections), MetaInfos) -> true
1290		; add_error(bmachine,'No animated sections available'), fail).
1291
1292		:- volatile b_get_named_machine_set/3.
1293		:- dynamic b_get_named_machine_set/3.
1294		:- public b_get_named_machine_set_calc/3.
1295		b_get_named_machine_set(Set,Members) :- b_get_named_machine_set(Set,_,Members).
1296		% precompiled: all enumerated sets with their elements (all in atomic form)
1297		b_get_named_machine_set_calc(Set,TExpr,Members) :-
1298		get_section_from_current_machine(enumerated_sets,Sets),
1299		get_section_from_current_machine(enumerated_elements,Elems),
1300		get_texpr_id(TExpr,Set),
1301		get_texpr_type(TExpr,set(Type)),
1302		get_texpr_type(TElem,Type),
1303		member(TExpr,Sets),
1304		findall(E, (member(TElem,Elems), get_texpr_id(TElem,E)), Members).
1305
1306		:- volatile b_enumerated_sets_precompiled/0.
1307		:- dynamic b_enumerated_sets_precompiled/0.
1308		:- public b_enumerated_sets_precompiled_calc/0.
1309		b_enumerated_sets_precompiled_calc :-
1310		b_check_and_precompile_enumerated_sets.
1311
1312		:- volatile b_get_machine_set/2.
1313		:- dynamic b_get_machine_set/2.
1314		:- public b_get_machine_set_calc/2.
1315	?	b_get_machine_set(Set) :- b_get_machine_set(Set,_).
1316		% precompiled: all deferred and enumerated sets (in atomic form)
1317		b_get_machine_set_calc(Set,TExpr) :-
1318		get_section_from_current_machine(deferred_sets,Sets),
1319		get_texpr_id(TExpr,Set),
1320	?	member(TExpr,Sets).
1321		b_get_machine_set_calc(Set,TExpr) :-
1322		b_get_named_machine_set(Set,TExpr,_).
1323
1324		:- 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.
1325		:- 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.
1326		b_machine_has_constants :- b_get_machine_constants([_|_]).
1327		:- public b_get_machine_all_constants_calc/1.
1328		% precompiled: all constants (abstract and concrete) in typed form
1329		b_get_machine_all_constants_calc(AllCsts2) :-
1330		findall(C,get_multi_sections([abstract_constants,concrete_constants],C),AllCsts),
1331		% now try and infer seq(.) type info for the constants; relevant for test 383
1332		b_get_properties_from_machine(Prop),
1333		infer_seq_types_for_tids(AllCsts,Prop,AllCsts2). % TODO: check if a candidate type exists in the constants?
1334
1335		:- public b_get_machine_constants_calc/1.
1336		% precompiled: all constants (abstract and concrete) in typed form; except for constant_represented inside global set
1337		b_get_machine_constants_calc(Csts) :-
1338		b_get_machine_all_constants(AllCsts),
1339		findall(C,
1340		(member(C,AllCsts), get_texpr_id(C,CID),
1341		\+ b_get_constant_represented_inside_global_set(CID,_)), % ignore constants detected as enumerated set elements
1342		Csts).
1343
1344		b_machine_has_variables :- b_get_machine_variables([_|_]).
1345
1346		:- public b_get_machine_variables_in_original_order_calc/1.
1347		% precompiled: all variables (abstract and concrete) in typed form
1348		b_get_machine_variables_in_original_order_calc(Vars) :-
1349		findall(V,get_multi_sections([abstract_variables,concrete_variables],V),Vars).
1350
1351		:- public b_get_machine_variables_calc/1.
1352		% get variables in order suitable for ord_member and optimized update storing
1353		b_get_machine_variables_calc(SVars) :-
1354		b_get_machine_variables_in_original_order(Vars),
1355		sort(Vars,SVars).
1356
1357		get_nr_of_machine_variables(Nr) :- b_get_machine_variables(L), length(L,Nr).
1358		get_nr_of_machine_constants(Nr) :- b_get_machine_constants(L), length(L,Nr).
1359
1360		b_is_constant(C) :- b_is_constant(C,_).
1361		:- public b_is_constant_calc/2.
1362		% precompiled: all constants (abstract and concrete) in atomic form
1363		b_is_constant_calc(Cst,Type) :-
1364		b_get_machine_constants(Constants),
1365		get_texpr_id(Term,Cst),
1366		get_texpr_type(Term,Type),
1367		member(Term,Constants).
1368		b_is_variable(V) :- b_is_variable(V,_).
1369		:- public b_is_variable_calc/2.
1370		% precompiled: all variables (abstract and concrete) in atomic form
1371		b_is_variable_calc(Var,Type) :-
1372		b_get_machine_variables(Vars), % b_get_machine_variables_in_original_order
1373		get_texpr_id(Term,Var),
1374		get_texpr_type(Term,Type),
1375		member(Term,Vars).
1376		% look up elements in several sections of the machine
1377		get_multi_sections(Sections,Elem) :-
1378	?	member(Section,Sections),
1379		get_section_from_current_machine(Section,List),
1380		member(Elem,List).
1381
1382		:- public b_get_constant_variable_description_calc/2.
1383		% get value of description pragmas @desc for variables and constants:
1384		b_get_constant_variable_description_calc(ID,Desc) :-
1385		(b_get_machine_constants(L) ; b_get_machine_variables(L)),
1386		get_texpr_id(Term,ID),
1387		member(Term,L),
1388		get_texpr_description(Term,TDesc),
1389		(simplify_desc(TDesc,Desc) -> true ; TDesc=Desc).
1390
1391		:- use_module(probsrc(tools_strings), [atom_prefix/2]).
1392		simplify_desc(Compound,R) :- compound(Compound),!,
1393		add_error(simplify_desc,'Non-atomic description: ',Compound),
1394		R=Compound.
1395		simplify_desc(memoize,memo).
1396		simplify_desc(memoise,memo).
1397		simplify_desc('"memoize"',memo).
1398		simplify_desc('"memoise"',memo).
1399		simplify_desc('"expand"',expand).
1400		simplify_desc('"memo"',memo). % allow /*@desc "memo" */
1401		simplify_desc(Atom,memo) :- atom_prefix('"memo ',Atom). % allow /*@desc "memo ...additional text" */
1402
1403		% check if a constant or variable is annotated for memoization:
1404		constant_variable_marked_as_memo(ID) :- b_get_constant_variable_description(ID,memo).
1405
1406		% check if a constant or variable is annotated for expansion using @desc expand
1407		constant_variable_marked_as_expand(ID) :- b_get_constant_variable_description(ID,EXPAND), EXPAND=expand.
1408
1409
1410		:- volatile b_get_invariant_from_machine/1,
1411		b_get_linking_invariant_from_machine/1,
1412		b_get_properties_from_machine/1,
1413		b_get_static_assertions_from_machine/1,
1414		b_extract_values_clause_assignment/3,
1415		b_get_unproven_static_assertions_from_machine/1,
1416		b_get_dynamic_assertions_from_machine/1,
1417		b_get_unproven_dynamic_assertions_from_machine/1,
1418		b_get_assertions_from_main_machine/2,
1419		b_get_initialisation_from_machine/2,
1420		b_get_machine_operation/6,b_top_level_operation/1,
1421		b_get_machine_operation_for_animation/7,
1422		b_is_operation_name/1,
1423		b_get_promoted_machine_operations/1.
1424		:- dynamic b_get_invariant_from_machine/1,
1425		b_get_linking_invariant_from_machine/1,
1426		b_get_properties_from_machine/1,
1427		b_get_static_assertions_from_machine/1,
1428		b_extract_values_clause_assignment/3,
1429		b_get_unproven_static_assertions_from_machine/1,
1430		b_get_dynamic_assertions_from_machine/1,
1431		b_get_unproven_dynamic_assertions_from_machine/1,
1432		b_get_assertions_from_main_machine/2,
1433		b_get_initialisation_from_machine/2,
1434		b_get_machine_operation/6,b_top_level_operation/1,
1435		b_get_machine_operation_for_animation/7,
1436		b_is_operation_name/1,
1437		b_get_promoted_machine_operations/1.
1438
1439		:- public b_get_invariant_from_machine_calc/1.
1440		% precompiled: typed invariant (a predicate)
1441		b_get_invariant_from_machine_calc(Inv) :-
1442		get_section_from_current_machine(invariant,Inv).
1443
1444		:- public b_get_linking_invariant_from_machine_calc/1.
1445		% precompiled: typed linking invariant (a predicate)
1446		b_get_linking_invariant_from_machine_calc(Inv) :-
1447		get_section_from_current_machine(linking_invariant,Inv).
1448
1449
1450		:- use_module(tools_lists,[exclude_count/4]).
1451		b_get_non_ignored_properties_from_machine(NonIgnoredProperties,Excluded) :-
1452		b_get_properties_from_machine(MProperties),
1453		(get_preference(use_ignore_pragmas,true) % filter out prob-ignore predicates here
1454		-> conjunction_to_list(MProperties,LMP), % TO DO avoid this conversion and back
1455		exclude_count(predicate_has_ignore_pragma, LMP,LMP2,Excluded), % exclude props marked as prob-ignore
1456		conjunct_predicates(LMP2,NonIgnoredProperties)
1457		; NonIgnoredProperties=MProperties,
1458		Excluded=0
1459		).
1460
1461		:- public b_get_properties_from_machine_calc/1.
1462		% precompiled: typed properties (a predicate)
1463		b_get_properties_from_machine_calc(SortedProp) :-
1464		get_section_from_current_machine(properties,Prop),
1465		(sort_properties(Prop,SortedProp) -> true %(Prop=SortedProp->true ; print(sorted(SortedProp)))
1466		; add_error(sort_properties,'sort_properties failed: ',Prop),
1467		SortedProp=Prop).
1468
1469		sort_properties(Prop,SortedProp) :- % print(sort_properties),nl,statistics(runtime, [R1,_]),
1470		weigh_properties(Prop,1,_,[],SProp),
1471		% statistics(runtime, [R2,_]), RDiff is R2-R1,print(done_weigh(RDiff,SProp)),nl,
1472		sort(SProp,SSProp),
1473		% statistics(runtime, [R3,_]), RDiff2 is R3-R2,print(done_sort(RDiff2)),nl,
1474		remove_weights(SSProp,PropList),
1475		conjunct_predicates(PropList,SortedProp).
1476		% translate:print_bexpr(SortedProp).
1477
1478		remove_weights([],[]).
1479		remove_weights([prop(_W,_Nr,E)|T],[E|RT]) :- remove_weights(T,RT).
1480
1481		weigh_properties(Pred,Nr,ONr,InL,OutL) :-
1482		decompose_conjunct(Pred,LHS,RHS), % will propagate labels down to conjuncts LHS,RHS
1483		!,
1484		weigh_properties(LHS,Nr,N1,InL,L2),
1485		weigh_properties(RHS,N1,ONr,L2,OutL).
1486		weigh_properties(b(Pred,S,I),Nr,N1,T,[prop(Weight,Nr,b(Pred,S,I))|T]) :-
1487		N1 is Nr+1,
1488		(member(contains_wd_condition,I) -> Weight=32000 % do not move properties with WD info
1489		; weigh_properties2(Pred,Weight)).
1490		% translate:print_bexpr(b(Pred,S,I)), print(' WEIGHT: '), print(Weight),nl
1491
1492		weigh_properties2(truth,W) :- !, W=1.
1493		weigh_properties2(falsity,W) :- !, W=1.
1494		weigh_properties2(equal(L,R),W) :- weigh_term(L,W1), !,
1495		( weigh_term(R,W2) -> W is W1*W2
1496		; W is 3200).
1497		% ; W is W1*20). %causes issue with ParityFunction test
1498		%weigh_properties2(equal(_,R),W) :- weigh_term(R,W2), !, W is W2*20.
1499		weigh_properties2(SOp,W) :- comparison(SOp,L,R),!,
1500		( (weigh_term(L,W1), weigh_term(R,W2))
1501		-> W is 7+W1+W2 % try and give things like x>10 priority over x>y (to overcome CLP(FD) limitations)
1502		; W=10).
1503		weigh_properties2(partition(LHS,RHS),W) :- weigh_term(LHS,W1), l_weigh_term(RHS,W2), !, W is W1*W2.
1504		weigh_properties2(not_equal(L,R),W) :- ((id(L),empty(R)) ; (id(R),empty(L))),!, W=1.
1505		weigh_properties2(not_equal(L,R),W) :- weigh_term(L,W1), weigh_term(R,W2),!,
1506		W is 20+W1*W2.
1507		weigh_properties2(_Rest,W) :- W=32000.
1508
1509		comparison(less(L,R),L,R).
1510		comparison(less_equal(L,R),L,R).
1511		comparison(greater(L,R),L,R).
1512		comparison(greater_equal(L,R),L,R).
1513
1514
1515		id(b(identifier(_),_,_)).
1516		empty(b(empty_set,_,_)).
1517		empty(b(empty_sequence,_,_)).
1518
1519		l_weigh_term([],0).
1520		l_weigh_term([H|T],R) :- l_weigh_term(T,TR), weigh_term(H,TH), R is TH+TR.
1521
1522		weigh_term(b(T,_,_),R) :- (weigh_term2(T,R) -> true ; fail). %R=20).
1523
1524		weigh_term2(value(_),1).
1525		weigh_term2(boolean_true,1).
1526		weigh_term2(boolean_false,1).
1527		weigh_term2(empty_set,1).
1528		weigh_term2(empty_sequence,1).
1529		weigh_term2(integer(_),1).
1530		weigh_term2(min_int,1).
1531		weigh_term2(max_int,1).
1532		weigh_term2(string(_),1).
1533		weigh_term2(real(_),1).
1534		weigh_term2(bool_set,2).
1535		weigh_term2(identifier(_),2).
1536		weigh_term2(set_extension(_),3).
1537		weigh_term2(integer_set(_),3).
1538		weigh_term2(interval(L,R),W) :- weigh_term(L,WL), weigh_term(R,WR), W is WL*WR.
1539
1540
1541
1542		b_machine_has_constants_or_properties :-
1543		(b_machine_has_constants -> true
1544		; (b_get_properties_from_machine(Prop)), \+ is_truth(Prop)).
1545
1546		b_get_machine_operation_parameter_types(OpName,ParTypes) :-
1547		b_get_machine_operation_typed_parameters(OpName,Parameters),
1548		maplist(get_texpr_type,Parameters,ParTypes).
1549
1550		b_get_machine_operation_typed_parameters(Operation,Res) :-
1551		b_get_machine_operation_typed_parameters3(Operation,real_paras_only,Res).
1552		b_get_machine_operation_typed_parameters_for_animation(Operation,Res) :-
1553		b_get_machine_operation_typed_parameters3(Operation,for_animation,Res).
1554
1555		b_get_machine_operation_typed_parameters3(Operation,ForAnim,Res) :-
1556		if(b_get_machine_operation_typed_parameters_aux(Operation,ForAnim,Paras),Res=Paras,
1557		(add_internal_error('Cannot get paras: ',b_get_machine_operation_typed_parameters(Operation,ForAnim,Res)),fail)).
1558		% also recognises SETUP_CONSTANTS & INITIALISE_MACHINE
1559		b_get_machine_operation_typed_parameters_aux('$setup_constants',_,Constants) :-
1560		b_machine_has_constants_or_properties,
1561		b_get_machine_constants(Constants).
1562		b_get_machine_operation_typed_parameters_aux('$initialise_machine',_,Variables) :-
1563		b_get_machine_variables(Variables).
1564		b_get_machine_operation_typed_parameters_aux(OpName,real_paras_only,Parameters) :-
1565		b_get_machine_operation(OpName,_R,Parameters,_Body,_OType,_OpPos).
1566		b_get_machine_operation_typed_parameters_aux(OpName,for_animation,Parameters) :-
1567		b_get_machine_operation_for_animation(OpName,_R,Parameters,_Body).
1568
1569		b_get_machine_operation_parameter_names(OpName,ParaNames) :-
1570		b_get_machine_operation_parameter_names(OpName,real_paras_only,ParaNames).
1571		b_get_machine_operation_parameter_names_for_animation(OpName,ParaNames) :-
1572		b_get_machine_operation_parameter_names(OpName,for_animation,ParaNames).
1573
1574		b_get_machine_operation_parameter_names('@INITIALISATION',ForAnim,ParaNames) :- % for Tcl/Tk
1575		b_get_machine_operation_parameter_names('$initialise_machine',ForAnim,ParaNames).
1576		b_get_machine_operation_parameter_names('@PROPERTIES',ForAnim,ParaNames) :- % for Tcl/Tk
1577		b_get_machine_operation_parameter_names('$setup_constants',ForAnim,ParaNames).
1578		b_get_machine_operation_parameter_names(OpName,ForAnim,ParaNames) :-
1579		b_get_machine_operation_typed_parameters3(OpName,ForAnim,Parameters),
1580		get_texpr_ids(Parameters,ParaNames).
1581
1582		b_get_machine_operation_typed_results('$setup_constants',[]).
1583		b_get_machine_operation_typed_results('$initialise_machine',[]).
1584		b_get_machine_operation_typed_results(OpName,Results) :-
1585		b_get_machine_operation(OpName,Results,_Parameters,_Body,_OType,_OpPos).
1586
1587		b_get_machine_operation_result_names('$setup_constants',[]).
1588		b_get_machine_operation_result_names('$initialise_machine',[]).
1589		b_get_machine_operation_result_names(OpName,ResultNames) :-
1590		b_get_machine_operation(OpName,Results,_Parameters,_Body,_OType,_OpPos),
1591		get_texpr_ids(Results,ResultNames).
1592
1593		b_get_machine_operation(Name,Results,Parameters,Body) :-
1594	?	b_get_machine_operation(Name,Results,Parameters,Body,_OType,_OpPos).
1595
1596		:- public b_get_assertions_from_main_machine_calc/2.
1597		b_get_assertions_from_main_machine_calc(static,FProp) :-
1598		((b_get_static_assertions_from_machine(Prop),
1599		exclude(is_not_main_assertion,Prop,FProp)) -> true
1600		; add_error(bmachine,'b_get_assertions_from_main_machine_calc static fails'), FProp=[]).
1601		b_get_assertions_from_main_machine_calc(dynamic,FProp) :-
1602		((b_get_dynamic_assertions_from_machine(Prop),
1603		exclude(is_not_main_assertion,Prop,FProp)) -> true
1604		; add_error(bmachine,'b_get_assertions_from_main_machine_calc dynamic fails'), FProp=[]).
1605		is_not_main_assertion(Assertion) :-
1606		get_texpr_pos(Assertion,Pos),
1607		error_manager:position_is_not_in_main_file(Pos).
1608
1609		% get nr of assertions and nr of main assertions for static/dynamic
1610		b_get_assertion_count(StaticOrDynamic,NrAll,NrMain) :-
1611	?	b_get_assertions(all,StaticOrDynamic,A), length(A,NrAll),
1612		b_get_assertions_from_main_machine(StaticOrDynamic,MA),length(MA,NrMain).
1613
1614		b_get_assertions(main,Mode,Ass) :- !,
1615		b_get_assertions_from_main_machine(Mode,Ass).
1616		b_get_assertions(specific(Label),Mode,LabelAss) :- !,
1617		b_get_assertions(all,Mode,Ass),
1618		%maplist(get_texpr_label,Ass,Labels), print(labels(Labels)),nl,
1619		include(has_label(Label),Ass,LabelAss),
1620		(LabelAss=[] -> ajoin(['No ',Mode,' assertion has label: '],Msg),
1621		add_warning(b_get_assertions,Msg,Label) ; true).
1622		b_get_assertions(_,static,Ass) :- b_get_static_assertions_from_machine(Ass).
1623		b_get_assertions(_,dynamic,Ass) :- b_get_dynamic_assertions_from_machine(Ass).
1624		b_main_machine_has_no_assertions :-
1625		b_get_assertions_from_main_machine(static,[]),
1626		b_get_assertions_from_main_machine(dynamic,[]).
1627
1628
1629		%has_label(Label,Expr) :- get_texpr_label(Expr,Label1), format('Labels ~w =? ~w~n',[Label1,Label]), fail.
1630		has_label(Label,Expr) :- get_texpr_label(Expr,Label).
1631
1632		:- public b_get_static_assertions_from_machine_calc/1.
1633		% precompiled: typed assertions (a list of predicates)
1634		b_get_static_assertions_from_machine_calc(Prop) :-
1635		get_section_from_current_machine(assertions,Prop1),
1636		exclude(predicate_uses_variables,Prop1,Prop),!.
1637		b_get_static_assertions_from_machine_calc(Prop) :-
1638		add_error(bmachine,'b_get_static_assertions_from_machine_calc fails'), Prop=[].
1639
1640		:- dynamic b_machine_has_static_assertions/0.
1641		:- public b_machine_has_static_assertions_calc/0.
1642		b_machine_has_static_assertions_calc :-
1643		b_get_static_assertions_from_machine([_|_]).
1644
1645		:- public b_get_unproven_static_assertions_from_machine_calc/1.
1646		b_get_unproven_static_assertions_from_machine_calc(FAssertions) :-
1647		b_get_static_assertions_from_machine(Assertions),
1648		filter_out_proven_assertions(Assertions,FAssertions),!.
1649		b_get_unproven_static_assertions_from_machine_calc(Prop) :-
1650		add_error(bmachine,'b_get_unproven_static_assertions_from_machine_calc fails'), Prop=[].
1651
1652		filter_out_proven_assertions([],[]).
1653		filter_out_proven_assertions([A1|T],R) :-
1654		(is_discharged_assertion(A1)
1655		-> R = TR %, print('Proven: '), translate:print_bexpr(A1),nl
1656		; R = [A1|TR]),
1657		filter_out_proven_assertions(T,TR).
1658
1659		:- public b_get_dynamic_assertions_from_machine_calc/1.
1660		b_get_dynamic_assertions_from_machine_calc(Prop) :-
1661		get_section_from_current_machine(assertions,Prop1),
1662		include(predicate_uses_variables,Prop1,Prop),!.
1663		b_get_dynamic_assertions_from_machine_calc(Prop) :-
1664		add_error(bmachine,'b_get_dynamic_assertions_from_machine_calc fails'), Prop=[].
1665
1666
1667		:- dynamic b_machine_has_dynamic_assertions/0.
1668		:- public b_machine_has_dynamic_assertions_calc/0.
1669		b_machine_has_dynamic_assertions_calc :-
1670		b_get_dynamic_assertions_from_machine([_|_]).
1671
1672		b_machine_has_assertions :- (b_machine_has_static_assertions -> true ; b_machine_has_dynamic_assertions).
1673
1674		b_machine_has_unproven_assertions :-
1675		b_get_unproven_dynamic_assertions_from_machine([_|_]) -> true
1676		; b_get_unproven_static_assertions_from_machine([_|_]).
1677
1678
1679		get_all_assertions_from_machine(Assertions) :-
1680		findall(A,((SD=static;SD=dynamic),get_assertions_from_machine(SD,SS),member(A,SS)),Assertions).
1681
1682		get_assertions_from_machine(Type,Assertions) :-
1683		( Type=(dynamic) ->
1684		(get_preference(use_po,true)
1685		-> b_get_unproven_dynamic_assertions_from_machine(Assertions)
1686		; b_get_dynamic_assertions_from_machine(Assertions)
1687		)
1688		; Type=(static) ->
1689		(get_preference(use_po,true)
1690		-> b_get_unproven_static_assertions_from_machine(Assertions)
1691		; b_get_static_assertions_from_machine(Assertions)
1692		)
1693		),
1694		Assertions = [_|_].
1695
1696		:- public b_get_unproven_dynamic_assertions_from_machine_calc/1.
1697		b_get_unproven_dynamic_assertions_from_machine_calc(FAssertions) :-
1698		b_get_dynamic_assertions_from_machine(Assertions),
1699		filter_out_proven_assertions(Assertions,FAssertions),!.
1700		b_get_unproven_dynamic_assertions_from_machine_calc(Prop) :-
1701		add_error(bmachine,'b_get_unproven_dynamic_assertions_from_machine_calc fails'), Prop=[].
1702
1703		predicate_uses_variables(Pred) :-
1704		b_get_machine_variables(Vars),
1705		get_texpr_ids(Vars,Ids),
1706		list_to_ord_set(Ids,OrdVars),
1707		find_identifier_uses(Pred,[],UsedVars),
1708		list_to_ord_set(UsedVars,OrdUsedVars),
1709		ord_intersect(OrdVars,OrdUsedVars).
1710
1711		:- public b_get_initialisation_from_machine_calc/2.
1712		% precompiled: typed initialisation (a substitution)
1713		b_get_initialisation_from_machine_calc(Init,OType) :-
1714		get_section_from_current_machine(initialisation,Init),
1715		( get_texpr_expr(Init,rlevent(_Name,_Section,_Status,Params,_Guard,_Theorems,_Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents)) ->
1716		get_operation_type(Init,'INITIALISATION',Params,OType)
1717		;
1718		OType = classic).
1719		% precompiled: operations, Name is in atomic form, Results and Parameters are lists
1720		% of typed identifiers, Body is a typed substitution
1721
1722		b_safe_get_initialisation_from_machine(Init,OType) :-
1723		if(b_get_initialisation_from_machine(Init,OType),true,
1724		add_error(bmachine,'Machine has no INITIALISATION clause')).
1725
1726
1727		:- volatile b_machine_operation_names_in_reverse_order/1.
1728		:- dynamic b_machine_operation_names_in_reverse_order/1.
1729		% a list of operation names in reverse order; this way we can randomize the
1730		% generation of the successor states
1731		precompile_operation_names_in_reverse_order :-
1732		retractall(b_machine_operation_names_in_reverse_order(_)),
1733	?	b_get_machine_operation(Name,_Results,_Parameters,_Body,_OType,_OpPos),
1734		asserta(b_machine_operation_names_in_reverse_order(Name)),
1735		fail.
1736		precompile_operation_names_in_reverse_order.
1737
1738		:- use_module(specfile, [animation_minor_mode/1, classical_b_mode/0]).
1739		:- use_module(extrasrc(b_expression_sharing),[cse_optimize_substitution/2]).
1740		:- public b_get_machine_operation_calc/6.
1741		b_get_machine_operation_calc(Name,Results,Parameters,NewBody,OType,OpPos) :-
1742		%well_def_analyser:get_hyps_for_top_level_operations([],Hyps),
1743		is_ground(Name,NameGround),
1744		get_section_from_current_machine(operation_bodies,Ops),
1745		get_texpr_expr(Op,operation(TId,Results,Parameters,Body)),
1746		get_texpr_id(TId,op(Name)),
1747	?	member(Op,Ops),
1748		% remove choicepoints when name was ground
1749		(NameGround==ground -> !; true),
1750		get_operation_type(Op,Name,Parameters,OType),
1751		(get_texpr_pos(TId,OpPos) -> true ; OpPos = unknown),
1752		( get_preference(use_common_subexpression_also_for_substitutions,true),
1753		get_preference(use_common_subexpression_elimination,true),
1754		\+ animation_minor_mode(eventb) % CSE_SUBST not yet available for Event-B
1755		-> debug_println(19,applying_cse_to(Name)),
1756		cse_optimize_substitution(Body,OpBody)
1757		; OpBody = Body),
1758		NewBody=OpBody.
1759
1760		b_get_machine_operation_signature(Name,SignatureStr) :-
1761		b_get_machine_operation_calc(Name,Results,Parameters,_,_,_),
1762		get_texpr_ids(Parameters,PIds),
1763		ajoin_with_sep(PIds,',',Args),
1764		(Results = []
1765		-> ajoin([Name,'(',Args,')'],SignatureStr)
1766		; get_texpr_ids(Results,RIds),
1767		ajoin_with_sep(RIds,',',Res),
1768		ajoin([Res,'<--',Name,'(',Args,')'],SignatureStr)
1769		).
1770
1771		%well_def_analyser:transform_machine_operation(Name,Results,Parameters,OpBody,Hyps,[create_not_discharged_msg(message)],NewBody).
1772		get_operation_type([],_Name,_Parameters,classic).
1773		get_operation_type(Op,Name,Parameters,OType) :-
1774		get_texpr_info(Op,Info),
1775		( member(eventb(_),Info) ->
1776		OType=eventb_operation(SortedChangeSet,Ps,OpPattern),
1777		member(modifies(ChangeSet),Info),!,
1778		sort(ChangeSet,SortedChangeSet), % maybe not necessary ?
1779		same_length(Parameters,Ps),
1780		OpPattern =.. [Name|Ps]
1781		;
1782		OType=classic).
1783
1784		:- volatile get_operation_info/2, get_operation_description_template_expr/2.
1785		:- dynamic get_operation_info/2, get_operation_description_template_expr/2.
1786		:- public get_operation_info_calc/2, get_operation_description_template_expr_calc/2.
1787		% precompiled: operation infos
1788		get_operation_info_calc(OpName,Info1) :-
1789		get_section_from_current_machine(operation_bodies,Ops),
1790		create_texpr(operation(TId,_Results,_Parameters,_Body),_,Info1,TOp), % rlevent()
1791		get_texpr_id(TId,op(OpName)),
1792	?	member(TOp,Ops).
1793
1794		b_get_operation_description(OpName,Desc) :-
1795		get_operation_info(OpName,Infos),
1796		member(description(Desc),Infos).
1797
1798		get_operation_or_init_info('$setup_constants',[]).
1799		get_operation_or_init_info('$initialise_machine',Info) :-
1800		b_get_initialisation_from_machine(Init,_),
1801		get_texpr_info(Init,Info).
1802	?	get_operation_or_init_info(OpName,Info) :- get_operation_info(OpName,Info).
1803		% todo '$setup_constants'
1804
1805		% get a typed string expression that can compute an operation description (based on vars, paras, ...)
1806		get_operation_description_template_expr_calc(OpName,TemplateStringExpr) :-
1807		get_error_context(Context),
1808		call_cleanup(get_op_desc_template_expr_calc2(OpName,TemplateStringExpr),restore_error_context(Context)).
1809
1810		get_op_desc_template_expr_calc2(OpName,TemplateStringExpr) :-
1811	?	get_operation_or_init_info(OpName,Infos),
1812		(translate_operation_name(OpName,TOpName), % translate $setup_constants,...
1813		b_definition_prefixed(expression, 'DESCRIPTION_FOR_', TOpName, DefName,DefPos),
1814		get_machine_operation_typing_scope(OpName,Scope,[]),
1815		b_get_typed_definition(DefName,Scope,TemplateStringExpr)
1816		% the user provided an explicit DESCRIPTION definition: use this first; useful for SETUP_CONSTANTS
1817		-> (get_texpr_type(TemplateStringExpr,string) -> true
1818		; add_warning(bmachine,'Type of operation description definition must be string: ',DefName,DefPos),
1819		fail
1820		)
1821		; % now look whether we have a description pragma
1822		get_op_desc_template_expr_calc3(OpName,Infos,TemplateStringExpr)
1823		).
1824		get_op_desc_template_expr_calc3(OpName,Infos,TemplateStringExpr) :-
1825		member(description(Desc),Infos),
1826		(member(description_position(OpPos),Infos)
1827		-> true
1828		; get_info_pos(Infos,OpPos)
1829		% Unfortunately this is the entire position from beginning of operation to desc label */
1830		),
1831		atom(Desc),
1832		set_error_context(checking_context('Checking description template for operation: ',OpName)),
1833		transform_string_template(Desc,OpPos,RawTemplateExpr),
1834		%translate:print_raw_bexpr(RawTemplateExpr),nl,
1835		GenerateParseErrors=gen_parse_warnings_for(OpPos),
1836		get_machine_operation_typing_scope(OpName,Scope,[]),
1837		% it could be that the template uses abstract variables that are no longer accessible
1838		b_type_only(RawTemplateExpr,Scope,Type,TemplateStringExpr,GenerateParseErrors),
1839		(debug_mode(off) -> true
1840		; format('Template description expression for operation ~w:~n',[OpName]),
1841		translate:print_bexpr(TemplateStringExpr),nl
1842		),
1843		(Type=string -> true ; add_internal_error('Not string type:',Type)).
1844
1845
1846		:- public b_top_level_operation_calc/1.
1847		% precompiled: operation names (in atomic form) of top-level operations (promoted operations)
1848		b_top_level_operation_calc(Name) :-
1849		is_ground(Name,NameGround),
1850		get_section_from_current_machine(promoted,Promoted),
1851		get_texpr_id(TId,op(Name)),
1852	?	member(TId,Promoted),
1853		(NameGround==ground -> !; true).
1854		:- public b_get_promoted_machine_operations_calc/1.
1855		b_get_promoted_machine_operations_calc(Ops) :-
1856		get_section_from_current_machine(promoted,Ops).
1857
1858		:- volatile b_top_level_feasible_operation/1.
1859		:- dynamic b_top_level_feasible_operation/1.
1860		:- public b_top_level_feasible_operation_calc/1.
1861		% filter out operations which are commented out statically by using 1=2 or similar in guard
1862	?	b_top_level_feasible_operation_calc(Name) :- b_top_level_operation(Name),
1863		b_get_machine_operation(Name,_,_,Body,_,_Pos),
1864		\+ infeasible_tsubst(Body).
1865		% TO DO: investigate how to link up with cbc feasibility analysis
1866
1867		infeasible_tsubst(b(S,_,_)) :- infeasible_subst(S).
1868		infeasible_subst(precondition(G,_)) :- is_falsity(G).
1869		infeasible_subst(select([b(select_when(G,_),_,_)])) :- is_falsity(G).
1870		infeasible_subst(any(_,G,_)) :- is_falsity(G).
1871
1872		% this succeeds not just for top-level operations
1873		%b_is_operation_name(Name) :- b_get_machine_operation(Name,_,_,_,_,_). is slower
1874		:- public b_is_operation_name_calc/1.
1875		b_is_operation_name_calc(Name) :-
1876	?	b_get_machine_operation(Name,_,_,_,_,_).
1877
1878		:- public b_top_level_operation_without_machine_prefix_calc/2.
1879		% if we have a top-level operation M1.op then here we store here that op is mapped to the full name M1.op.
1880		b_top_level_operation_without_machine_prefix_calc(OpName,FullOpName) :-
1881	?	b_top_level_operation(FullOpName),
1882		split_last(FullOpName, '.', _, OpName).
1883
1884		b_get_operation_pos(Name,Pos) :-
1885	?	b_get_machine_operation(Name,_,_,_,_,Pos).
1886
1887		b_get_operation_variant(Name,ConvOrAnt,Variant) :-
1888		b_get_machine_operation(Name,_,_,TBody),
1889		get_texpr_expr(TBody,Body),
1890		Body = rlevent(Name,_Section,Status,
1891		_Params,_Guard,_Theorems,_Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents),
1892		% TO DO: look maybe higher up in refinement hierarchy
1893		get_texpr_expr(Status,S),
1894		functor(S,ConvOrAnt,1),
1895		(ConvOrAnt = convergent ; ConvOrAnt = anticipated),
1896		arg(1,S,Variant).
1897
1898		b_machine_has_operations :-
1899		(b_is_operation_name(_) -> true).
1900		% -----------------------------
1901
1902
1903		% the names of definitions which have a given Prefix,
1904		% Type is expression or predicate, Name is an atomic name
1905		b_definition_prefixed(Type,Prefix,Suffix,Name,Pos) :-
1906		safe_atom_chars(Prefix,PrefixChars,b_definition_prefixed1),
1907		append(PrefixChars,SuffixChars,FullChars),
1908		(ground(Suffix) -> safe_atom_chars(Suffix,SuffixChars,b_definition_prefixed2),
1909		safe_atom_chars(Name,FullChars,b_definition_prefixed3)
1910		; true),
1911	?	b_get_definition_name_with_pos(Name,_Arity,Type,Pos),
1912		safe_atom_chars(Name,FullChars,b_definition_prefixed4),
1913		safe_atom_chars(Suffix,SuffixChars,b_definition_prefixed5).
1914
1915		% TODO: should we also look for theory direct definitions for Event-B models?
1916		% :- use_module(bmachine_eventb,[stored_operator_direct_definition/8]).
1917		% stored_operator_direct_definition(Id,_Proj,_Thy,Parameters,_Def,_WD,_TP,_Kind),
1918		% or add auxiliary definition files for Event-B models
1919
1920
1921		% get definitions in alphabetical order of name:
1922		% predictable order is relevant for SVG_OBJECTS to know which objects are on top of each other
1923		b_sorted_b_definition_prefixed(Type,DEFPREFIX,DefName,DefPos) :-
1924		(b_or_z_mode -> true
1925		; additional_defs_loaded), % allow, e.g., XTL mode for VisB definition files (VISB_DEFINITIONS_FILE);
1926		% TODO: maybe allow other non-B modes (mainly for VisB)
1927		% fail silently if we are not B/Z/TLA+/Alloy mode as machine not pre-compiled
1928		(DEFPREFIX==DefName % only one can definition can match; no need to do findall
1929		-> b_get_definition_name_with_pos(DefName,_,_,DefPos)
1930		; sorted_list_of_defs(Type,DEFPREFIX,SortedList),
1931	?	member(def(DefName,DefPos),SortedList)
1932		).
1933		sorted_list_of_defs(Type,DEFPREFIX,SortedList) :-
1934		findall(def(DefName,DefPos),
1935		b_definition_prefixed(Type,DEFPREFIX,_Tail,DefName,DefPos),
1936		List),
1937		sort(List,SortedList).
1938
1939
1940		:- use_module(bmachine_construction,[type_open_formula/8]).
1941		type_check_definitions :-
1942		temporary_set_preference(allow_untyped_identifiers,true_with_string_type,CHNG), % we may not have all identifiers visible
1943		get_error_context(Context),
1944		call_cleanup(type_check_definitions2,restore_error_context(Context)),
1945		reset_temporary_preference(allow_untyped_identifiers,CHNG).
1946		type_check_definitions2 :-
1947		get_preference(type_check_definitions,true),
1948		full_b_machine(Machine),
1949		b_get_definition_with_pos(Name,Type,DefPos,Args,RawExpr,_Deps),
1950		% TO DO: do not re-analyse definitions already analysed for ANIMATION_FUNCTION,...
1951		(Type = predicate ; Type=expression), % can we also allow substitutions ?
1952		debug_format(9,'Type checking DEFINITION ~w~n',[Name]),
1953		set_error_context(checking_context('Type checking DEFINITION: ',Name)),
1954		Scope = [variables], % prob_ids(visible),
1955		%type_with_errors(RawExpr,Scope,_,_TExpr),
1956		AllowNewIds=true,
1957		% TO DO: improve solution below, e.g., delete Args from visible variables or rename Args to fresh ids!
1958		(Args=[] -> RawExpr2=RawExpr
1959		; Type=predicate -> RawExpr2 = exists(none,Args,conjunct(none,falsity(none),RawExpr))
1960		% wrap Args into quantifier, avoid clash with variables,... ; conjunct used to avoid warnings about body of exists
1961		% it would be better to use unknown_truth_value instead of falsity, but this currently fails in btypechecker
1962		; RawExpr2=exists(none,Args,equal(none,RawExpr,RawExpr)) % TODO: better solution to avoid duplicating RawExpr
1963		),
1964		(type_open_formula(RawExpr2,Scope,AllowNewIds,Machine,FType,Identifiers,_TPred,Errors) % maybe no need to run cleanup?
1965		-> Errors = [_|_],
1966		format('Error for DEFINITION ~w of type ~w over identifiers ~w~n',[Name,FType,Identifiers]),
1967		add_all_perrors_in_context_of_used_filenames(Errors,definition_type_error,error),
1968		fail
1969		% TO DO: check for local clashes?
1970		; add_error(bmachine,'Type checking DEFINITION failed: ',Name,DefPos)
1971		),
1972		fail.
1973		type_check_definitions2 :- debug_format(9,'Finished type checking DEFINITIONs~n',[]).
1974
1975		b_get_definition(Name,DefType,Args,RawExpr,Deps) :-
1976	?	b_get_definition_with_pos(Name,DefType,_DefPos,Args,RawExpr,Deps).
1977
1978		:- public portray_defs/0. % debugging utility
1979		portray_defs :-
1980		b_get_definition_with_pos(Name,DefType,DefPos,_Args,_RawExpr,_),
1981		add_message(bmachine,'DEFINITION: ',Name:DefType,DefPos),fail.
1982		portray_defs.
1983
1984		b_get_definition_with_pos(Name,DefType,DefPos,Args,RawExpr,Deps) :- %print(get_def(Name)),nl,
1985		get_section_from_current_machine(definitions,Defs),
1986	?	member(definition_decl(Name,DefType,_DefInfos,DefPos,Args,RawExpr,Deps),Defs).
1987		b_get_definition_with_pos(Name,DefType,DefPos,Args,RawExpr,Deps) :- %print(get_def(Name)),nl,
1988		additional_configuration_machine(_MchName,Mch),
1989		get_section(definitions,Mch,Defs),
1990		member(definition_decl(Name,DefType,_,DefPos,Args,RawExpr,Deps),Defs).
1991		%flush_output,write(additional_def(Name,DefType,Deps)),nl,flush_output.
1992
1993		% a version where we have already pre-fetched the Defs section to avoid getting full B machine each time
1994		b_get_definition_from_defs_section(Defs,Name,DefType,DefPos,Args,RawExpr,Deps) :- %print(get_def(Name)),nl,
1995	?	member(definition_decl(Name,DefType,_,DefPos,Args,RawExpr,Deps),Defs).
1996		b_get_definition_from_defs_section(_,Name,DefType,DefPos,Args,RawExpr,Deps) :- %print(get_def(Name)),nl,
1997		additional_configuration_machine(_MchName,Mch),
1998		get_section(definitions,Mch,Defs),
1999		member(definition_decl(Name,DefType,_,DefPos,Args,RawExpr,Deps),Defs).
2000
2001
2002		:- use_module(input_syntax_tree,[raw_update_file_nrs/3]).
2003		:- volatile additional_configuration_machine/2.
2004		:- dynamic additional_configuration_machine/2.
2005		% load an additional definitions file for ViB configuration or CUSTOM_GRAPH features
2006		% useful for Event-B, ... models
2007		b_load_additional_definitions_file(File) :-
2008		Options=[],
2009		catch(load_b_machine_as_term(File,Machine,Options),
2010		parse_errors(Errors),
2011		(add_all_perrors_in_context_of_used_filenames(Errors,parse_error,error),fail)),
2012		b_load_additional_definitions_from_term(Machine).
2013
2014		b_load_additional_definitions_from_list_of_facts(ListOfFacts) :-
2015		load_b_machine_list_of_facts_as_term(ListOfFacts, Machine),
2016		b_load_additional_definitions_from_term(Machine).
2017
2018		b_load_additional_definitions_from_term(complete_machine(MainName, Machines, Filenames)) :-
2019		maplist(add_additional_filename,Filenames,NewNrs),
2020		member(definition_file(_,Defs),Machines),
2021		Defs = definitions(_Pos,_List),
2022		raw_update_file_nrs(Defs,NewNrs,NewDefs),
2023		bmachine_construction:extract_only_definitions(MainName,[NewDefs],DefsMachine,Errs),
2024		add_all_perrors_in_context_of_used_filenames(Errs,definition_type_error,error),
2025		retractall(additional_configuration_machine(MainName,_)),
2026		assert(additional_configuration_machine(MainName,DefsMachine)),
2027		b_machine_recompile_for_new_defs.
2028
2029		additional_defs_loaded :- (additional_configuration_machine(_,_) -> true).
2030
2031
2032		% the next calls get typed definitions without parameters:
2033		% (To treat definitions with parameters one would have to add the parameters to the type environment, see type_check_definitions2)
2034		b_get_typed_predicate_definition(Name,Scope,ResTExpr) :-
2035		b_get_definition_name_with_pos(Name,0,predicate,_), % check if it exists first
2036		b_get_definition(Name,predicate,[],RawExpr,_Deps),
2037		type_with_errors_in_context(RawExpr,Scope,_,TExpr,machine_context,error),
2038		ResTExpr=TExpr. % Do unification after to not prevent generation of type errors.
2039		b_get_typed_expression_definition(Name,Scope,ResTExpr) :-
2040		b_get_definition_name_with_pos(Name,0,expression,_), % check if it exists first
2041		b_get_definition(Name,expression,[],RawExpr,_Deps),
2042		type_with_errors_in_context(RawExpr,Scope,_,TExpr,machine_context,error),
2043		ResTExpr=TExpr. % Do unification after to not prevent generation of type errors, e.g., test 1691
2044		b_get_true_expression_definition(Name) :-
2045		b_get_typed_expression_definition(Name,[variables_and_additional_defs],PF),
2046		PF = b(boolean_true,boolean,_).
2047		%b_get_typed_subst_definition(Name,Scope,Parameters,TExpr) :-
2048		% temporary_set_preference(allow_local_operation_calls,true,CHNG),
2049		% b_get_definition(Name,substitution,Parameters,RawExpr,_Deps),
2050		% type_with_errors(RawExpr,[operation_bodies|Scope],_,TExpr), % need to remove variables to avoid clash warnings
2051		% reset_temporary_preference(allow_local_operation_calls,CHNG).
2052		b_get_typed_definition(Name,Scope,TExpr) :-
2053		b_get_definition_name_with_pos(Name,0,_,_), % check if it exists first
2054	?	b_get_definition(Name,_DefType,[],RawExpr,_Deps),
2055		type_with_errors_in_context(RawExpr,Scope,_,TExpr,machine_context,error).
2056
2057
2058		% the following does not send errors to error_manager:
2059		% and requires get_section_from_current_machine(definitions,Defs), to be called before
2060		b_get_typed_definition_with_error_list(Machine,Defs,Name,Scope,TExpr,ErrorsAndWarnings,Success) :-
2061	?	b_get_definition_from_defs_section(Defs,Name,_DefType,_DefPos,[],RawExpr,_Deps),
2062		b_type_expression_nge(Machine,RawExpr,Scope,do_not_ground_types,_Type,TExpr,ErrorsAndWarnings),
2063		(no_real_perror_occurred(ErrorsAndWarnings) -> Success=true ; Success=false).
2064
2065		get_definitions_section(Defs) :- get_section_from_current_machine(definitions,Defs).
2066
2067		type_with_errors(RawExpr,Scope,Type,TExpr) :-
2068		type_with_errors_in_context(RawExpr,Scope,Type,TExpr,not_in_machine_context([]),error).
2069
2070
2071		type_with_errors_in_context(RawExpr,Scope,Type,TExpr,Context,ErrOrWarn) :- % print(scope(Scope)),nl,
2072		b_type_expression(RawExpr,Scope,Type,TExpr,Errors),!,
2073		(Context=not_in_machine_context(Filenames)
2074		-> add_all_perrors(Errors,Filenames,type_expression_error,ErrOrWarn) % [] for REPL, or JSON file for VisB
2075		; add_all_perrors_in_context_of_used_filenames(Errors,type_expression_error,ErrOrWarn)
2076		),
2077		no_real_perror_occurred(Errors). % check that we have no errors, just warnings
2078
2079		% here we do not add perrors; just fail
2080		type_without_errors(RawExpr,Scope,Type,TExpr) :-
2081		b_type_expression(RawExpr,Scope,Type,TExpr,Errors),!,
2082		no_real_perror_occurred(Errors).
2083
2084		% OptionalQuantifier is: forall, exists, no_quantifier
2085		% influences whether we create a forall, exists or no quantifier around the RawPred
2086		b_type_open_predicate_with_errors(OptionalQuantifier,RawPred,Scope,TPred) :-
2087		b_type_open_predicate(OptionalQuantifier,RawPred,Scope,TPred,Errors),
2088		add_all_perrors(Errors,[],type_expression_error),
2089		no_real_perror_occurred(Errors).
2090		b_type_open_predicate(OptionalQuantifier,RawPred,Scope,TPred,Errors) :-
2091		b_type_open_predicate_for_full_b_machine(_Machine,OptionalQuantifier,RawPred,Scope,TPred,Errors).
2092		b_type_open_predicate_for_full_b_machine(Machine,OptionalQuantifier,RawPred,Scope,TPred,Errors) :-
2093		(var(Machine) -> full_b_machine(Machine) ; true),
2094		replace_prob_set_elements_in_scope(Scope,Scope1),
2095		type_open_predicate_with_quantifier(OptionalQuantifier,RawPred,Scope1,Machine,TPred,Errors),!.
2096		b_type_open_exists_predicate(Raw,Typed,Errors) :-
2097		b_type_open_predicate(open(exists),Raw,[prob_ids(visible),variables],Typed,Errors).
2098
2099		% Note: see pre_expand_typing_scope below if you need to type a long list of expressions
2100		b_type_expression(RawExpr,Scope,Type,TExpr,Errors) :-
2101		b_type_expression(_Machine,RawExpr,Scope,Type,TExpr,Errors).
2102		% machine can be variable; will be instantiated upon demand
2103		b_type_expression(_,RawExpr,_Scope,Type,TExpr,Errors) :-
2104		b_type_literal(RawExpr,T,TE),!,
2105		Type=T,TExpr=TE,Errors=[].
2106		b_type_expression(Machine,RawExpr,Scope,Type,TExpr,Errors) :-
2107		b_type_expression_for_full_b_machine(Machine,RawExpr,Scope,Type,TExpr,Errors).
2108		% version where we can pass NonGroundException list or do_not_ground_types:
2109		b_type_expression_nge(Machine,RawExpr,Scope,NonGroundExceptions,Type,TExpr,Errors) :-
2110		b_type_expression_for_full_b_machine_nge(Machine,RawExpr,Scope,NonGroundExceptions,Type,TExpr,Errors).
2111
2112		% type literals without setting up scope, ...
2113		% TODO: also use for type_in_machine_l
2114		b_type_literal(boolean_false(Pos),boolean,b(boolean_false,boolean,[nodeid(Pos)])).
2115		b_type_literal(boolean_true(Pos),boolean,b(boolean_true,boolean,[nodeid(Pos)])).
2116		b_type_literal(integer(Pos,Int),integer,b(integer(Int),integer,[nodeid(Pos)])).
2117		b_type_literal(real(Pos,R),real,b(real(R),real,[nodeid(Pos)])).
2118		b_type_literal(string(Pos,Atom),string,b(string(Atom),string,[nodeid(Pos)])).
2119
2120
2121		b_type_expression_for_full_b_machine(M,RawExpr,Scope,Type,TExpr,Errors) :-
2122		b_type_expressions_l(M,[RawExpr],Scope,[],[Type],[TExpr],Errors).
2123		% version where we can also specify NonGroundExceptions (e.g. to do_not_ground_types)
2124		b_type_expression_for_full_b_machine_nge(M,RawExpr,Scope,NonGroundExceptions,Type,TExpr,Errors) :-
2125		b_type_expressions_l(M,[RawExpr],Scope,NonGroundExceptions,[Type],[TExpr],Errors).
2126
2127		b_type_expressions_l(Machine,RawExprs,Scope,NonGroundExceptions,Types,TExprs,Errors) :-
2128		(var(Machine) -> full_b_machine(Machine) ; true),
2129		% in case you type check multiple expressions for a complex machine it is better to extract the machine once
2130		replace_prob_set_elements_in_scope(Scope,Scope1),
2131		% we need this, for example for tcltk_check_state_sequence_from_file, when deferred set elements written by TLC are in the file
2132		type_in_machine_l(RawExprs,Scope1,NonGroundExceptions,Machine,Types,TExprs,Errors),!.
2133
2134		replace_prob_set_elements_in_scope(Scope,Res) :- var(Scope),!,
2135		add_internal_error('Scope is a variable (use, e.g., [constants,variables,operation_bodies,...]):',replace_prob_set_elements_in_scope(Scope,Res)),
2136		Res=Scope.
2137		replace_prob_set_elements_in_scope(Scope,NewScope) :-
2138	?	( select(prob_ids(AllOrVisible),Scope,identifier(Ids),NewScope)
2139		-> % replaces prob by deferred set element identifiers
2140		% e.g., if we have SETS PID then we would have PID1,... in Ids unless PID1 is known to be another identifier
2141		b_get_prob_deferred_set_elements(DefIDs,AllOrVisible),
2142		exclude(known_identifier,DefIDs,Ids) % exclude those ids that would clash
2143		% TO DO: add option to translate_identifiers using translate:keyword_to_id_cache
2144		;
2145		Scope = NewScope).
2146
2147
2148		known_identifier(X) :- get_texpr_id(X,ID),
2149		(bmachine:b_is_constant(ID,_) ;
2150		bmachine:b_is_variable(ID,_)).
2151
2152
2153		:- use_module(bmachine_construction,[create_scope/6]).
2154		% pre-expand a type-checking scope once; so that we can typecheck a series of formulas
2155		pre_expand_typing_scope(Scope,pre_expanded_scope(Env,Errors)) :-
2156		replace_prob_set_elements_in_scope(Scope,NewScope),
2157		full_b_machine(Machine),
2158		create_scope(NewScope,machine,Machine,Env,Errors,[]).
2159
2160		% ------------------------
2161
2162		% a generic predicate to find all kinds of identifiers
2163
2164		:- use_module(b_global_sets,[b_global_set/1, is_b_global_constant/3]).
2165		:- use_module(probsrc(kernel_freetypes),[registered_freetype/2, freetype_case_db/3]).
2166		:- use_module(probsrc(bmachine_eventb), [ stored_operator/2]).
2167		%! mode get_machine_identifiers(+Category, -ListOfIdentifiers)
2168		get_machine_identifiers(machines,MN) :-
2169		findall(FID, (b_filenumber(FID,Type,_,_),Type \= def),MN).
2170		get_machine_identifiers(definition_files,DFN) :-
2171		findall(FID, b_filenumber(FID,def,_,_),DFN).
2172		get_machine_identifiers(definitions,DN) :-
2173		findall(DefID,b_get_definition(DefID,_,_,_,_),DN).
2174		get_machine_identifiers(sets,Sets) :-
2175		findall(GS,b_global_set(GS),Sets).
2176		get_machine_identifiers(set_constants,Csts) :-
2177		findall(Cst,is_b_global_constant(_GS,_,Cst),Csts).
2178		get_machine_identifiers(constants,CN) :-
2179		b_get_machine_constants(Constants),
2180		get_texpr_ids(Constants,CN).
2181		get_machine_identifiers(freetypes,FN) :-
2182		findall(FID,((registered_freetype(F,_) ; freetype_case_db(F,_,_)),functor(F,FID,_)),FN).
2183		get_machine_identifiers(operators,FN) :-
2184		findall(Name,stored_operator(Name,_Kind),FN). % we could exclude Kind=datatype_definition, as listed in freetypes?
2185		get_machine_identifiers(variables,VN) :-
2186		b_get_machine_variables(Variables),
2187		get_texpr_ids(Variables,VN).
2188		get_machine_identifiers(operations,Ops) :-
2189		findall(Op,b_top_level_operation(Op),Ops).
2190
2191		get_machine_identifiers_with_pp_type(machines,MN) :-
2192		findall([FID,'Machine'], (b_filenumber(FID,Type,_,_),Type \= def),MN).
2193		get_machine_identifiers_with_pp_type(definition_files,DFN) :-
2194		findall([FID,'Definition file'], b_filenumber(FID,def,_,_),DFN).
2195		get_machine_identifiers_with_pp_type(definitions,DN) :-
2196		findall([DefID,DefType],b_get_definition(DefID,DefType,_,_,_),DN).
2197		get_machine_identifiers_with_pp_type(sets,Sets) :-
2198		findall([GS,GS],b_global_set(GS),Sets).
2199		get_machine_identifiers_with_pp_type(set_constants,Csts) :-
2200		findall([Cst,GS],is_b_global_constant(GS,_,Cst),Csts).
2201		get_machine_identifiers_with_pp_type(constants,CN) :-
2202		b_get_machine_constants(Constants),
2203		maplist(extract_id_and_pp_type,Constants,CN).
2204		%get_machine_identifiers_with_pp_type(freetypes,FN) :-
2205		% findall([FID,FID],((registered_freetype(F,_) ; freetype_case_db(F,_,_)),functor(F,FID,_)),FN).
2206		get_machine_identifiers_with_pp_type(operators,FN) :-
2207		findall([Name,''],stored_operator(Name,_Kind),FN). % we could exclude Kind=datatype_definition, as listed in freetypes?
2208		get_machine_identifiers_with_pp_type(variables,VN) :-
2209		b_get_machine_variables(Variables),
2210		maplist(extract_id_and_pp_type,Variables,VN).
2211		get_machine_identifiers_with_pp_type(operations,Ops) :-
2212		findall([Op,'Operation'],b_top_level_operation(Op),Ops).
2213
2214		:- use_module(bsyntaxtree,[get_texpr_id/2, get_texpr_type/2]).
2215		:- use_module(translate,[pretty_type/2]).
2216		extract_id_and_pp_type(TId,[Id,PPType]) :-
2217		get_texpr_id(TId,Id),
2218		get_texpr_type(TId,Type),
2219		pretty_type(Type,PPType).
2220
2221		:- use_module(b_global_sets,[b_global_deferred_set/1,all_elements_of_type/2]).
2222		:- use_module(input_syntax_tree,[get_raw_position_info/2]).
2223		% try and get source code for an identifier
2224		source_code_for_identifier(ID,constant,Type,OriginStr,OriginTerm,Source) :- b_is_constant(ID),!,
2225		get_constant_type_and_origin(ID,Type,OriginStr,OriginTerm),
2226		findall(Def,get_constant_definition(ID,Def),AllDefs),
2227		(AllDefs=[_|_] -> conjunct_predicates(AllDefs,Source)
2228		; % try and find other type of predicates defining ID
2229		findall(Pred,get_constant_predicate(ID,Pred),AllPreds),
2230		conjunct_predicates(AllPreds,Source)).
2231		source_code_for_identifier(ID,variable,Type,OriginStr,OriginTerm,Source) :- b_is_variable(ID),!,
2232		get_variable_type_and_origin(ID,Type,OriginStr,OriginTerm),
2233		Source = b(truth,pred,[]). % TO DO: improve
2234		source_code_for_identifier(ID,Kind,Type,OriginStr,OriginTerm,Source) :- b_get_machine_set(ID,TID),!,
2235		(b_global_deferred_set(ID) -> Kind = deferred_set ; Kind = enumerated_set),
2236		Type = set(global(ID)),
2237		all_elements_of_type(ID,All),
2238		translate:translate_span_with_filename(TID,OriginStr), OriginTerm=TID,
2239		Source = b(equal(TID,b(value(All),Type,[])),pred,[]).
2240		source_code_for_identifier(ID,Kind,Type,OriginStr,OriginTerm,Source) :-
2241		global_set_element(ID,GID),!,
2242		(b_global_deferred_set(GID)
2243		-> Kind = deferred_set_element ; Kind = enumerated_set_element),
2244		b_get_machine_set(GID,TGID),
2245		Type = global(ID),
2246		all_elements_of_type(GID,All),
2247		translate:translate_span_with_filename(TGID,OriginStr), OriginTerm=TGID,
2248		Source = b(equal(TGID,b(value(All),set(Type),[])),pred,[]).
2249		source_code_for_identifier(ID,definition,Type,OriginStr,OriginTerm,Source) :-
2250		b_get_definition(ID,DefType,Args,RawExpr,_Deps),!,
2251		Type = DefType,
2252		% Definitions are only present in RAW form
2253		get_raw_position_info(RawExpr,PosInfo),
2254		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
2255		OriginTerm=PosInfo,
2256		source_code_for_definition(DefType,ID,Args,RawExpr,Source).
2257		source_code_for_identifier(ID,file,Type,OriginStr,OriginTerm,b(string(Source),string,[])) :-
2258		b_filenumber(ID,Kind,_,Filename),
2259		extension_kind(Kind,Type),
2260		!,
2261		ajoin([Type,' ',ID],Source),
2262		OriginTerm =src_position_with_filename(1,0,0,Filename),
2263		OriginStr = Filename.
2264		source_code_for_identifier(ID,Kind,subst,OriginStr,OriginTerm,Source) :-
2265		b_find_operation(ID,Res,TParas,Body,OType),
2266		(OType=classic -> Kind = operation ; Kind=event),
2267		translate:translate_span_with_filename(Body,OriginStr),Body=OriginTerm,
2268		get_texpr_info(Body,Info),
2269		Source=b(operation(b(identifier(ID),subst,[]),Res,TParas,Body),subst,Info).
2270		source_code_for_identifier(ID,assertion,pred,OriginStr,OriginTerm,Assertion) :-
2271		b_get_assertions(all,_,Ass), member(Assertion,Ass),
2272		get_texpr_label(Assertion,ID), OriginTerm = Assertion,
2273		translate:translate_span_with_filename(Assertion,OriginStr).
2274		source_code_for_identifier(ID,invariant,pred,OriginStr,OriginTerm,Invariant) :-
2275		b_get_invariant_from_machine(C), conjunction_to_list(C,L), member(Invariant,L),
2276		get_texpr_label(Invariant,ID), OriginTerm = Invariant,
2277		translate:translate_span_with_filename(Invariant,OriginStr).
2278		% TO DO: look for invariant labels as ids ?
2279
2280		:- use_module(tools,[ split_last/4 ]).
2281		b_find_operation(ID,Res,TParas,Body,OType) :-
2282		b_get_machine_operation(ID,Res,TParas,Body,OType,_Pos).
2283		b_find_operation(ID,Res,TParas,Body,OType) :-
2284		b_get_machine_operation(ID2,Res,TParas,Body,OType,_Pos),
2285		split_last(ID2, '.', _, ID).
2286
2287		extension_kind(mch,'MACHINE').
2288		extension_kind(ref,'REFINEMENT').
2289		extension_kind(def,'DEFINITIONS FILE').
2290		extension_kind(imp,'IMPLEMENTATION').
2291
2292		source_code_for_definition(predicate,ID,_,RawExpr,Source) :-
2293		b_type_open_exists_predicate(RawExpr,Typed,Errors),
2294		(no_real_perror_occurred(Errors) -> true ; debug_println(9,errs(ID,Errors))),
2295		Source=Typed.
2296		source_code_for_definition(expression,ID,Args,RawExpr,Source) :-
2297		% TO DO: add parameters to avoid type errors; but we get Typed anyway
2298		b_type_expression(RawExpr,[prob_ids(visible),variables],Type,Typed,Errors),
2299		(no_real_perror_occurred(Errors) -> true ; debug_println(9,errs(ID,Args,Type,Errors))),
2300		Source=Typed.
2301		% TO DO: treate substitutions
2302		source_code_for_definition(DefType,ID,_Args,_RawExpr,Source) :-
2303		Source=b(identifier(ID),DefType,[]).
2304
2305		:- use_module(b_global_sets,[lookup_global_constant/2,prob_deferred_set_element/4]).
2306		global_set_element(ID,GlobalSetID) :- lookup_global_constant(ID,fd(_,GlobalSetID)).
2307		global_set_element(ID,GlobalSetID) :-
2308		prob_deferred_set_element(GlobalSetID,_Elem,ID,all).
2309
2310		get_constant_span(ID,Span) :-
2311		b_get_machine_constants(Constants),
2312		TID = b(identifier(ID),_,Span),
2313		member(TID,Constants).
2314
2315		get_constant_type_and_origin(ID,Type,OriginStr,OriginTerm) :-
2316		b_get_machine_constants(Constants),
2317		TID = b(identifier(ID),Type,_Infos),
2318		member(TID,Constants),
2319		% we could also use member(origin(Origin),Infos)
2320		translate:translate_span_with_filename(TID,OriginStr), OriginTerm=TID.
2321		get_variable_type_and_origin(ID,Type,OriginStr,OriginTerm) :-
2322		b_get_machine_variables(Vars),
2323		TID = b(identifier(ID),Type,_Infos),
2324		member(TID,Vars),
2325		% we could also use member(origin(Origin),Infos)
2326		translate:translate_span_with_filename(TID,OriginStr), OriginTerm=TID.
2327
2328		get_constant_definition(ID,FullDef) :-
2329		b_get_properties_from_machine(Prop),
2330		EqDef = b(equal(LHS,RHS),pred,_),
2331		member_in_conjunction_cse(FullDef,EqDef,Prop),
2332		(get_texpr_id(LHS,ID) ; get_texpr_id(RHS,ID)).
2333
2334		get_constant_predicate(ID,FullPred) :-
2335		b_get_properties_from_machine(Prop),
2336		member_in_conjunction_cse(FullPred,Pred,Prop),
2337		involves_id(Pred,ID).
2338		involves_id(ID,b(E,_,_)) :- involves_id_aux(E,ID).
2339		involves_id_aux(member(LHS,_),ID) :- get_texpr_id(LHS,ID).
2340		involves_id_aux(subset(LHS,_),ID) :- get_texpr_id(LHS,ID).
2341		involves_id_aux(subset_strict(LHS,_),ID) :- get_texpr_id(LHS,ID).
2342
2343		:- volatile b_get_definition_name_with_pos/4.
2344		:- dynamic b_get_definition_name_with_pos/4.
2345		:- public b_get_definition_name_with_pos_calc/4.
2346		b_get_definition_name_with_pos_calc(Name,Arity,DefType,DefPos) :-
2347	?	b_get_definition_with_pos(Name,DefType,DefPos,Args,_RawExpr,_Deps),
2348		length(Args,Arity).
2349
2350		:- volatile b_get_machine_setscope/2.
2351		:- dynamic b_get_machine_setscope/2.
2352		:- public b_get_machine_setscope_calc/2.
2353		% precompiled: definitions of the form "scope_SET == Expr",
2354		% Set is the name of the Set, TExpr the typed expression
2355		b_get_machine_setscope_calc(Set,TExpr) :-
2356	?	b_definition_prefixed(expression, scope_, Set, Name,_),
2357		% TO DO: check if it is a SET
2358	?	b_get_typed_definition(Name,[constants],TExpr). % [constants] scope so that we have access to other definitions
2359
2360
2361		% get a specific MAX_OPERATIONS Value for an operation
2362		% precompiled: definitions of the form "MAX_OPERATIONS_OpName == Expr"
2363		:- volatile b_get_machine_operation_max/2, b_get_machine_operation_time_out/2.
2364		:- dynamic b_get_machine_operation_max/2, b_get_machine_operation_time_out/2.
2365		:- public b_get_machine_operation_max_calc/2, b_get_machine_operation_time_out_calc/2.
2366
2367		b_get_machine_operation_max_calc(OpName,MaxOp) :-
2368		b_get_machine_operation_integer_def('MAX_OPERATIONS_',
2369		' (negative numbers means using randomised restart)', OpName,MaxOp).
2370		b_get_machine_operation_time_out_calc(OpName,TimeOut) :-
2371		b_get_machine_operation_integer_def('TIME_OUT_','', OpName,TimeOut).
2372
2373		:- use_module(probsrc(pref_definitions),[compute_static_expr_for_pref/3]).
2374		:- use_module(probsrc(tools_matching), [get_possible_operation_matches_msg/2]).
2375		b_get_machine_operation_integer_def(DefPrefix,AdditionalMsg,FullOpName,MaxOp) :-
2376		b_definition_prefixed(expression,DefPrefix,OpName,Name,DefPos),
2377		(b_is_operation_name_or_init_step(OpName) -> FullOpName=OpName
2378		; b_top_level_operation_without_machine_prefix(OpName,_) ->
2379		% we have found a full operation Machine.OpName (there could be more)
2380		% Note: user can currently not use . inside definition names
2381		b_top_level_operation_without_machine_prefix(OpName,FullOpName), % there could be more matches
2382		ajoin(['Assuming DEFINITION refers to operation ', FullOpName,': '], Msg),
2383		add_message(b_get_machine_operation_integer_def,Msg,Name,DefPos)
2384		; get_possible_operation_matches_msg(OpName,FMsg) ->
2385		ajoin(['Unknown operation in DEFINITION (did you mean ',FMsg,' ?) : '], Msg),
2386		add_warning(b_get_machine_operation_integer_def,Msg,Name,DefPos),
2387		fail
2388		; add_warning(b_get_machine_operation_integer_def,'Unknown operation in DEFINITION: ',Name,DefPos),
2389		fail
2390		),
2391		(b_get_typed_definition(Name,[constants],DEF) -> compute_static_expr_for_pref(DEF,Name,Val) ; DEF='??'),
2392		(Val=int(MaxOp)
2393		% TO DO: check if it is an operation, use compute_static_expr from pref_definitions
2394		%, MaxOp >= 0 we now use negative numbers for randomised restart for MAX_OPERATIONS
2395		-> true
2396		; ajoin(['Definition ',Name,' must specify an integer',AdditionalMsg,': '],Msg),
2397		add_warning(b_get_machine_operation_integer_def,Msg,DEF,DefPos),
2398		fail
2399		).
2400
2401		b_is_operation_name_or_init_step(Event) :-
2402		(b_is_operation_name(Event) ; Event='INITIALISATION' ; Event='SETUP_CONSTANTS').
2403
2404		:- volatile b_get_machine_goal/1.
2405		:- dynamic b_get_machine_goal/1.
2406		:- public b_get_machine_goal_calc/1.
2407		% precompiled: definition of GOAL, a typed predicate
2408		b_get_machine_goal_calc(TPred) :- get_goal(TPred).
2409
2410		b_reset_machine_goal_from_DEFINITIONS :-
2411		get_goal(TPred),
2412		b_set_parsed_typed_machine_goal(TPred).
2413		get_goal(Goal) :-
2414		get_proz_settings(Settings),memberchk(goal(Goal),Settings),!.
2415		get_goal(Goal) :- % print(getting_goal),nl,
2416		get_texpr_type(Goal,pred),
2417		b_get_typed_predicate_definition('GOAL',[variables_and_additional_defs],Goal).
2418
2419		:- volatile b_get_machine_searchscope/1.
2420		:- dynamic b_get_machine_searchscope/1.
2421		:- public b_get_machine_searchscope_calc/1.
2422		% precompiled: definition of SCOPE, a typed predicate
2423		b_get_machine_searchscope_calc(TPred) :-
2424		get_texpr_type(TPred,pred),
2425		b_get_typed_definition('SCOPE',[variables_and_additional_defs],TPred).
2426
2427		:- volatile b_get_definition_string_from_machine/3.
2428		:- dynamic b_get_definition_string_from_machine/3.
2429		:- public b_get_definition_string_from_machine_calc/3.
2430		% precompiled: string definitions, Name == "String"
2431		b_get_definition_string_from_machine(Name,String) :-
2432		b_get_definition_string_from_machine(Name,_,String).
2433		b_get_definition_string_from_machine_calc(Name,Pos,String) :-
2434	?	b_get_definition_name_with_pos(Name,0,expression,_), % pre-computed, check if exists first
2435		b_get_definition(Name,expression,[],string(Pos,Str),_Deps),
2436		get_texpr_expr(TExpr,string(String)),
2437		type_with_errors_in_context(string(Pos,Str),[],_,TExpr,machine_context,warning).
2438
2439		get_animation_image(Nr,S) :-
2440		animation_minor_mode(z),
2441		get_proz_animation_function(_,_,Images),!,
2442		nth1(Nr,Images,S).
2443		get_animation_image(Nr,S) :- number(Nr),!,
2444		number_codes(Nr,TailCodes),
2445		/* ANIMATION_IMG */
2446		atom_codes(Def_Name,[65,78,73,77,65,84,73,79,78,95,73,77,71|TailCodes]),
2447		b_get_definition_string_from_machine(Def_Name,S).
2448		get_animation_image(Nr,S) :-
2449		b_get_definition_string_from_machine(Def_Name,S),
2450		/* ANIMATION_IMG */
2451		atom_codes(Def_Name,[65,78,73,77,65,84,73,79,78,95,73,77,71|TailCodes]),
2452		number_codes(Nr,TailCodes).
2453
2454		:- use_module(error_manager,[extract_file_number_and_name/3]).
2455		:- use_module(specfile,[b_or_z_mode/0]).
2456		get_animation_image_source_file(Nr,File) :- b_or_z_mode,
2457		% get source file where Animation image is defined; relevant for finding images
2458		b_get_definition_string_from_machine(Def_Name,Pos,_),
2459		atom_codes(Def_Name,[65,78,73,77,65,84,73,79,78,95,73,77,71|TailCodes]),
2460		number_codes(Nr,TailCodes),
2461		extract_file_number_and_name(Pos,_,File).
2462
2463		get_proz_animation_function(Function,Default,Images) :-
2464		get_proz_settings(Settings),
2465		memberchk(animation_function(Function,Default,Images),Settings).
2466		get_proz_settings(Settings) :-
2467		machine(_,Sections),memberchk(meta/Meta,Sections),
2468		memberchk(proz_settings(Settings),Meta).
2469
2470
2471		:- volatile b_get_machine_animation_function/2.
2472		:- dynamic b_get_machine_animation_function/2.
2473		:- public b_get_machine_animation_function_calc/2.
2474		:- use_module(tools,[safe_number_codes/2]).
2475		:- use_module(bsyntaxtree,[is_set_type/2]).
2476		% precompiled: definition of ANIMATION_FUNCTION, a typed expression
2477		b_get_machine_animation_function_calc(AFun,Nr) :-
2478		get_proz_animation_function(TFun,Default,_),!,
2479		( Nr = -1, AFun = Default
2480		; Nr = 0, TFun \= none, AFun=TFun
2481		).
2482		b_get_machine_animation_function_calc(TFun,Nr) :-
2483		get_definition_with_nr_suffix("ANIMATION_FUNCTION",Nr,Def_Name),
2484		b_get_typed_expression_definition(Def_Name,[variables_and_additional_defs],TFun),
2485		% only type it afterwards; avoid throwing type errors for other definitions
2486		get_texpr_type(TFun,Type),
2487		(is_set_type(Type,couple(_,_)) -> true
2488		; add_warning(b_get_machine_animation_function_calc,'Illegal type for ANIMATION_FUNCTION: ',Def_Name:Type,TFun),
2489		fail).
2490
2491
2492		:- volatile b_get_machine_heuristic_function/1.
2493		:- dynamic b_get_machine_heuristic_function/1.
2494		:- public b_get_machine_heuristic_function_calc/1.
2495		b_get_machine_heuristic_function_calc(TFun) :- %print(extracting_heuristic_fun(TFun)),nl,
2496		get_texpr_type(TFun,integer),
2497		b_get_typed_expression_definition('HEURISTIC_FUNCTION',[variables_and_additional_defs],TFun),
2498		% 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
2499		debug_format(19,'HEURISTIC_FUNCTION DEFINITION detected~n',[]).
2500
2501		:- volatile b_get_machine_animation_expression/2.
2502		:- dynamic b_get_machine_animation_expression/2.
2503		:- public b_get_machine_animation_expression_calc/2.
2504		b_get_machine_animation_expression_calc(STR,AExpr) :- %print(extracting_heuristic_fun(TFun)),nl,
2505	?	useful_animation_expression(STR),
2506		b_get_typed_expression_definition(STR,[variables_and_additional_defs],AExpr).
2507		b_get_machine_animation_expression_calc(DefName,AExpr) :-
2508		b_definition_prefixed(_,'ANIMATION_EXPRESSION',_,DefName,_DefPos),
2509		b_get_typed_expression_definition(DefName,[variables_and_additional_defs],AExpr).
2510
2511		%useful_animation_expression('ANIMATION_EXPRESSION'). % for state viewer
2512		useful_animation_expression('GAME_PLAYER'). % for MCTS, should return "min" or "max"
2513		useful_animation_expression('GAME_OVER').
2514		useful_animation_expression('GAME_VALUE').
2515		useful_animation_expression('GAME_MCTS_RUNS').
2516		useful_animation_expression('GAME_MCTS_TIMEOUT').
2517		useful_animation_expression('GAME_MCTS_CACHE_LAST_TREE').
2518
2519
2520		% Custom nodes and edges for a custom graph representation of a state
2521		:- volatile b_get_machine_custom_nodes_function/2, b_get_machine_custom_edges_function/2,
2522		b_get_machine_custom_graph_function/2.
2523		:- dynamic b_get_machine_custom_nodes_function/2, b_get_machine_custom_edges_function/2,
2524		b_get_machine_custom_graph_function/2.
2525		:- public b_get_machine_custom_nodes_function_calc/2.
2526		b_get_machine_custom_nodes_function_calc(TFun,Nr) :-
2527		get_definition_with_nr_suffix("CUSTOM_GRAPH_NODES",Nr,Def_Name),
2528		b_get_typed_expression_definition(Def_Name,[variables_and_additional_defs],TFun).
2529		:- public b_get_machine_custom_edges_function_calc/2.
2530		b_get_machine_custom_edges_function_calc(TFun,Nr) :-
2531		get_definition_with_nr_suffix("CUSTOM_GRAPH_EDGES",Nr,Def_Name),
2532		b_get_typed_expression_definition(Def_Name,[variables_and_additional_defs],TFun).
2533		:- public b_get_machine_custom_graph_function_calc/2.
2534		b_get_machine_custom_graph_function_calc(TFun,Nr) :-
2535		get_definition_with_nr_suffix("CUSTOM_GRAPH",Nr,Def_Name), % single function for graph attributes, possibly edges and nodes
2536		b_get_typed_expression_definition(Def_Name,[variables_and_additional_defs],TFun).
2537
2538
2539		get_definition_with_nr_suffix(Prefix,Nr,Def_Name) :-
2540	?	b_get_definition_name_with_pos(Def_Name,0,expression,_),
2541		atom_codes(Def_Name,AC),
2542		append(Prefix,TailCodes,AC),
2543		(TailCodes=[] -> Nr=0
2544		; TailCodes = "_DEFAULT" -> Nr = -1
2545		; safe_number_codes(Nr,TailCodes)).
2546
2547
2548		% ------------------------
2549
2550		:- volatile b_get_constant_represented_inside_global_set/2.
2551		:- dynamic b_get_constant_represented_inside_global_set/2.
2552
2553		:- public b_get_constant_represented_inside_global_set_calc/2.
2554		b_get_constant_represented_inside_global_set_calc(X,GlobalSetName) :-
2555		b_get_disjoint_constants_of_type(GlobalSetName, DisjointConstants,_),
2556		member(X,DisjointConstants). /* X will be integrated into the global_set */
2557
2558
2559		:- volatile b_get_disjoint_constants_of_type/3.
2560		:- dynamic b_get_disjoint_constants_of_type/3.
2561		:- public b_get_disjoint_constants_of_type_calc/3.
2562		b_get_disjoint_constants_of_type_calc(GlobalSetName, DisjointConstants, AllConstantsIDs) :-
2563		b_get_machine_all_constants(Constants), /* get all the constants */
2564		b_get_properties_from_machine(Properties),
2565	?	b_get_machine_set(GlobalSetName),
2566		\+ b_get_named_machine_set(GlobalSetName,_), % not an explicitly enumerated set
2567		find_constant_ids_of_type(Constants,GlobalSetName,AllConstantsIDs),
2568		find_inequal_global_set_identifiers(AllConstantsIDs,global(GlobalSetName),Properties,DisjointConstants),
2569		DisjointConstants \= [],
2570		debug_println(9,disjoint_enumerated_constants(GlobalSetName,DisjointConstants)).
2571		% TO DO: remove from Properties irrelevant conjuncts; sort AllConstantsIDs by having first those with max disequalities
2572
2573		find_constant_ids_of_type([],_GS,[]) :- !.
2574		find_constant_ids_of_type([b(identifier(ID),global(GS),_)|T], GS, [ID|IT]) :- !,
2575		find_constant_ids_of_type(T,GS,IT).
2576		find_constant_ids_of_type([b(_,_,_)|T], GS, IT) :- !, find_constant_ids_of_type(T,GS,IT).
2577		find_constant_ids_of_type(X,GS,_) :- print(find_constant_ids_of_type_error(X,GS)),nl,fail.
2578
2579
2580		% ------------------------
2581		:- volatile b_get_all_used_identifiers_in_section/2.
2582		:- dynamic b_get_all_used_identifiers_in_section/2.
2583		:- public b_get_all_used_identifiers_in_section_calc/2.
2584
2585		% Note: may contain var$0 instead of var for becomes_such
2586		b_get_all_used_identifiers_in_section_calc(SECTION,Identifiers) :-
2587		full_b_machine(BMachine),
2588	?	member(SECTION,[constraints,properties,invariant,assertions,
2589		initialisation,operation_bodies]),
2590		findall(I, find_used_identifier_in_machine_section(BMachine,SECTION,I), Ids),
2591		%print(section_ids(SECTION,Ids)),nl,
2592		sort(Ids,Identifiers).
2593
2594		:- volatile b_get_all_used_identifiers/1.
2595		:- dynamic b_get_all_used_identifiers/1.
2596		:- public b_get_all_used_identifiers_calc/1.
2597		:- use_module(library(ordsets),[ord_union/2]).
2598		% Precompiled: b_get_all_used_identifiers_calc/1 returns a list of all
2599		% identifiers used in machine sections that contain expressions and predicates
2600		b_get_all_used_identifiers_calc(Identifiers) :-
2601		findall(I, b_get_all_used_identifiers_in_section(_,I), ListOfList),
2602		ord_union(ListOfList,Identifiers). % ,print(all(Identifiers)),nl.
2603
2604		find_used_identifier_in_machine_section(Machine,Sec,Identifier) :-
2605		% treat it like a list of expressions
2606		get_section_texprs(Sec,Machine,TExprs),
2607		% and find all identifiers in each expression
2608	?	member(TExpr,TExprs),
2609		find_identifier_uses(TExpr,[],Ids),
2610	?	member(Identifier,Ids).
2611
2612		:- volatile b_is_unused_constant/1.
2613		:- dynamic b_is_unused_constant/1.
2614		:- public b_is_unused_constant_calc/1.
2615		b_is_unused_constant_calc(UnusedConstant) :-
2616		findall(C,b_is_constant(C),CL), %b_get_machine_constants(Constants), gives typed ids
2617		CL\=[] ,sort(CL,Constants),
2618		b_get_all_used_identifiers_in_section(invariant,I1),
2619		b_get_all_used_identifiers_in_section(assertions,I2),
2620		b_get_all_used_identifiers_in_section(initialisation,I3),
2621		b_get_all_used_identifiers_in_section(operation_bodies,I4),
2622		% TODO: get constants used in VisB definitions
2623		ord_union([I1,I2,I3,I4],UsedIds),
2624		%print(used(UsedIds)),nl,
2625		ord_subtract(Constants,UsedIds,UnusedConstants),
2626		UnusedConstants\=[],
2627		(b_get_machine_variables([]) -> true
2628		; length(UnusedConstants,NrUC),
2629		(silent_mode(on) -> true
2630		; (NrUC>10,debug_mode(off),UnusedConstants=[C1,C2|_]) ->
2631		print_message_with_max_depth(unused_constants(NrUC,[C1,C2,'...']),500)
2632		; print_message_with_max_depth(unused_constants(NrUC,UnusedConstants),500))
2633		),
2634		member(UnusedConstant,UnusedConstants).
2635
2636
2637		% precompiled: Skel is the operation skeleton, SpecializedInv a typed predicate
2638		% (Skel,SpecializedInv) :-
2639		% b_get_machine_operation(Name,_Res,Params,_Body),
2640		% atom_concat('SIMPLIFIED_INV_OP_',Name,ASNC),
2641		% b_get_typed_definition(ASNC,[variables,identifiers(Params)],SpecializedInv),
2642		% length(Params,Len),
2643		% functor(Skel,Name,Len),
2644		% print(b_specialized_invariant_for_op(Skel)).
2645
2646
2647		get_section_from_current_machine(Section,Content) :-
2648		full_b_machine(BMachine),
2649		get_section(Section,BMachine,Content).
2650
2651		is_ground(X,R) :- ground(X),!,R=ground.
2652		is_ground(_,nonground).
2653
2654		b_set_empty_machine :- debug_println(9,setting_empty_machine),
2655		empty_machine(Main,Machines),
2656		b_set_machine(Main,Machines,[]).
2657
2658		b_get_machine_refinement_hierarchy(Hierarchy) :-
2659		\+ machine(_Name,_M),!,Hierarchy=[]. %No B Machine loaded
2660		b_get_machine_refinement_hierarchy(Hierarchy) :-
2661		get_section_from_current_machine(meta,Infos),
2662		member(hierarchy/Hierarchy,Infos),!.
2663
2664		b_get_refined_machine_name(Machine) :-
2665		b_get_machine_refinement_hierarchy([_Main,Machine|_Rest]).
2666		b_get_refined_ancestors_names(list(AncestorList)) :-
2667		b_get_machine_refinement_hierarchy([_Main|AncestorList]).
2668		b_get_refined_machine(M) :-
2669		get_section_from_current_machine(meta,Infos),
2670		member(refined_machine/M,Infos), !.
2671
2672
2673
2674		b_get_machine_header_position(MachName,Position) :-
2675		get_section_from_current_machine(meta,Infos),
2676		member(header_pos/HeaderPosList,Infos),
2677		% List with elements MachineName/PositionOfMachineHeader
2678		member(MachName/Position,HeaderPosList).
2679
2680		% model type can be system for Atelier-B Event-B
2681		b_get_model_type(M) :-
2682		get_section_from_current_machine(meta,Infos),
2683		member(model_type/M,Infos), !.
2684
2685		% TODO(DP,6.8.2008)
2686		:- volatile b_machine_temp_predicate/1.
2687		:- dynamic b_machine_temp_predicate/1.
2688
2689		%set_temp_predicate(CustomPredicate) :-
2690		% b_parse_machine_predicate(CustomPredicate,TypedPred),
2691		% assert_temp_typed_predicate(TypedPred).
2692		%
2693		%% set a temporary predicate as additional guard
2694		%set_temp_predicate(CustomPredicate,'$initialise_machine') :- !,set_temp_predicate(CustomPredicate).
2695		%set_temp_predicate(CustomPredicate,'$setup_constants') :- !,set_temp_predicate(CustomPredicate).
2696		%set_temp_predicate(CustomPredicate,OpName) :-
2697		% b_parse_machine_operation_pre_post_predicate(CustomPredicate,TypedPred, OpName,true),
2698		% assert_temp_typed_predicate(TypedPred).
2699
2700		% Note: it can be a good idea to use inline_prob_deferred_set_elements_into_bexpr/2 before:
2701		assert_temp_typed_predicate(TypedPred) :-
2702		reset_temp_predicate,
2703		assertz(b_machine_temp_predicate(TypedPred)).
2704
2705
2706		reset_temp_predicate :- retractall(b_machine_temp_predicate(_)).
2707
2708		:- volatile b_machine_additional_property/1.
2709		:- dynamic b_machine_additional_property/1.
2710
2711		% additional properties for set_up_constants
2712		% TO DO: check if there are constants/properties; otherwise raise warning
2713		add_additional_property(CustomPredicate,Description) :-
2714		format('Adding Property: ~w~n',[CustomPredicate]),
2715		b_parse_machine_predicate(CustomPredicate,TypedPred),
2716		add_texpr_info_if_new(TypedPred,description(Description),TP2),
2717		assertz(b_machine_additional_property(TP2)).
2718
2719		:- use_module(btypechecker, [unify_types_strict/2]).
2720		:- use_module(bsyntaxtree, [safe_create_texpr/4]).
2721		:- use_module(probsrc(translate), [pretty_type/2]).
2722
2723		:- public b_extract_values_clause_assignment_calc/3.
2724		b_extract_values_clause_assignment_calc(ID,Type,TVal) :-
2725		% extract equalities from VALUES clause
2726		get_section_from_current_machine(values,Values),
2727		member(b(values_entry(TID,TVal),_,Info),Values),
2728		get_texpr_id(TID,ID),
2729		get_texpr_type(TID,Type),
2730		debug_println(20,values_entry(ID,Type,TVal)),
2731		(b_is_constant(ID,OtherType),
2732		unify_types_strict(Type,OtherType)
2733		-> (member(description(_),Info) -> Info1=Info
2734		; Info1=[description('from VALUES clause') | Info]),
2735		safe_create_texpr(equal(TID,TVal),pred,Info1,Equality),
2736		(debug_mode(off) -> true ; add_message(bmachine,'Adding property for VALUES: ',Equality,Equality)),
2737		assertz(b_machine_additional_property(Equality)),
2738		(b_extract_values_clause_assignment(ID,_,_)
2739		-> add_error(bmachine,'Multiple VALUES entries for constant: ',ID,TID)
2740		; true)
2741		; b_get_machine_set(ID) -> true % will be dealt with in b_global_sets for deferred sets
2742		; b_get_constant_represented_inside_global_set(ID,_) ->
2743		add_message(bmachine,'Ignoring VALUES entry for constant (already detected as enumerated set element): ',ID,TID)
2744		; lookup_global_constant(ID,fd(_,GSET)) ->
2745		ajoin(['Ignoring VALUES entry for element of enumerated set ',GSET,': '],Msg),
2746		add_message(bmachine,Msg,ID,TID)
2747		% TODO: detect case when this is a deferred set element not detected as (virtual) enumerated element
2748		; b_is_constant(ID,OtherType) -> pretty_type(OtherType,OT), pretty_type(Type,TT),
2749		ajoin(['Cannot adapt value type ',TT,' to abstract type ',OT,', ignoring VALUES entry for: '],Msg),
2750		add_warning(bmachine,Msg,ID,TID)
2751		; add_error(bmachine,'VALUES clause for unknown constant: ',ID,TID),
2752		fail
2753		).
2754
2755
2756		% -------------------
2757
2758		:- use_module(specfile,[unset_animation_minor_modes/1,reset_animation_minor_modes/1]).
2759		:- use_module(translate,[set_unicode_mode/0, unset_unicode_mode/0, set_print_type_infos/1]).
2760		b_show_machine_representation_unicode(Rep,AdditionalInfo,UnsetMinorModes,Unicode) :-
2761		Unicode=true,!,
2762		set_unicode_mode,
2763		call_cleanup(b_show_machine_representation(Rep,AdditionalInfo,UnsetMinorModes,none),unset_unicode_mode).
2764		b_show_machine_representation_unicode(Rep,AdditionalInfo,UnsetMinorModes,_) :-
2765		b_show_machine_representation(Rep,AdditionalInfo,UnsetMinorModes,none).
2766
2767
2768		% AdditionalInfo=true means show additional information as comments (promoted, ...)
2769		% UnsetMinorModes will print in default classical B style
2770		% TypeInfos: none, needed or all
2771		b_show_machine_representation(Rep,AdditionalInfo,UnsetMinorModes,TypeInfos) :-
2772		full_b_machine(BMachine),
2773		(UnsetMinorModes==true -> unset_animation_minor_modes(L) ; L=[]),
2774		set_print_type_infos(TypeInfos),
2775		translate_machine(BMachine,Rep,AdditionalInfo),
2776		set_print_type_infos(none),
2777		(UnsetMinorModes==true -> reset_animation_minor_modes(L) ; true).
2778
2779		:- use_module(tools_printing,[nested_write_term_to_codes/2]).
2780		b_get_internal_prolog_representation_as_codes(Codes) :-
2781		full_b_machine(BMachine),
2782		nested_write_term_to_codes(BMachine,Codes).
2783
2784		:- use_module(tools,[get_tail_filename/2,split_filename/3,safe_atom_chars/3]).
2785		% TypingLevel = none, needed or all
2786		b_write_machine_representation_to_file(TypingLevel,PPFILE) :-
2787		b_write_machine_representation_to_file('$auto',TypingLevel,PPFILE).
2788		b_write_machine_representation_to_file('$auto',TypingLevel,PPFILE) :- !, % automatically infer machine name
2789		%get_full_b_machine(Name,M),
2790		get_tail_filename(PPFILE,Tail),
2791		split_filename(Tail,MachName,_Ext),
2792		b_write_machine_representation_to_file3(MachName,TypingLevel,PPFILE).
2793		b_write_machine_representation_to_file(MachName,TypingLevel,PPFILE) :-
2794		% provide explicit machine name; useful for diff checks
2795		b_write_machine_representation_to_file3(MachName,TypingLevel,PPFILE).
2796
2797		:- use_module(translate,[set_print_type_infos/1]).
2798		:- use_module(tools_files, [write_to_utf8_file_or_user_output/2]).
2799		b_write_machine_representation_to_file3(MachName,Level,PPFILE) :-
2800		debug_println(20,'% Pretty-Printing Internal Representation to File: '),
2801		debug_println(20,PPFILE),
2802		translate:set_print_type_infos(Level), % none, needed or all
2803		get_full_b_machine(_Name,M),
2804		(translate_machine_to_classicalb(MachName,M,Rep)
2805		-> translate:set_print_type_infos(none)
2806		; add_internal_error('Translating machine failed: ',b_write_machine_representation_to_file3(MachName,Level,PPFILE)),
2807		set_print_type_infos(none),
2808		fail),
2809		write_to_utf8_file_or_user_output(PPFILE,Rep).
2810
2811		:- use_module(specfile).
2812		translate_machine_to_classicalb(MachName,M,Rep) :-
2813		temporary_set_preference(expand_avl_upto,-1,CHNG), % avoid printing sets using condensed #
2814		(animation_minor_mode(X)
2815		-> remove_animation_minor_mode,
2816		call_cleanup(translate_machine(machine(MachName,M),Rep,false), set_animation_minor_mode(X))
2817		; translate_machine(machine(MachName,M),Rep,false)),
2818		reset_temporary_preference(expand_avl_upto,CHNG).
2819
2820		b_write_eventb_machine_to_classicalb_to_file(PPFILE) :-
2821		get_tail_filename(PPFILE,Tail),
2822		split_filename(Tail,MachName,_Ext),
2823		AdditionalInfo=true,
2824		b_get_eventb_machine_as_classicalb_codes(MachName,AdditionalInfo,Rep),
2825		write_to_utf8_file_or_user_output(PPFILE,Rep).
2826
2827		:- use_module(preferences,[temporary_set_preference/3,reset_temporary_preference/2]).
2828		b_get_eventb_machine_as_classicalb_codes(MachName,AdditionalInfo,Rep) :-
2829		full_b_machine(machine(Name,MachineBody)),
2830		(var(MachName) -> MachName=Name ; true),
2831		% limit abstract level to 0
2832		b_limit_abstract_level_to_zero(MachineBody,MachineBodyLevel0),
2833		temporary_set_preference(translate_print_typing_infos,true,CHNG),
2834		temporary_set_preference(translate_ids_to_parseable_format,true,CHNG2),
2835		temporary_set_preference(expand_avl_upto,-1,CHNG3), % avoid printing sets using condensed #
2836		(translate_eventb_to_classicalb(machine(MachName,MachineBodyLevel0),AdditionalInfo,Rep)
2837		-> reset_temporary_preference(translate_print_typing_infos,CHNG),
2838		reset_temporary_preference(translate_ids_to_parseable_format,CHNG2),
2839		reset_temporary_preference(expand_avl_upto,CHNG3)
2840		; add_internal_error('Translating Event-B machine to Classical B failed: ',b_get_eventb_machine_as_classicalb_codes(MachName,AdditionalInfo,Rep)),
2841		reset_temporary_preference(translate_print_typing_infos,CHNG),
2842		reset_temporary_preference(translate_ids_to_parseable_format,CHNG2),
2843		reset_temporary_preference(expand_avl_upto,CHNG3),
2844		fail).
2845
2846		b_limit_abstract_level_to_zero(MachineBody,MachineBodyLevel0) :-
2847		maplist(b_set_to_level_zero,MachineBody,MachineBodyLevel0).
2848
2849		% TODO: set to level zero also the other events of the Event-B machine
2850		b_set_to_level_zero(initialisation/InitEvent,initialisation/InitEventLevelZero) :-
2851		get_texpr_expr(InitEvent,rlevent(Id,Sec,St,Par,Grd,Thms,Act,VW,PW,Ums,_Abs)),
2852		get_texpr_info(InitEvent,Info),
2853		create_texpr(rlevent(Id,Sec,St,Par,Grd,Thms,Act,VW,PW,Ums,[]),subst,Info,InitEventLevelZero).
2854		b_set_to_level_zero(X,X).
2855
2856		b_show_eventb_as_classicalb(Rep,AdditionalInfo) :-
2857		full_b_machine(BMachine),
2858		translate_eventb_to_classicalb(BMachine,AdditionalInfo,Rep).
2859
2860		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2861
2862		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2863		% precompilation: predicates are precompiled by calling the ..._calc predicate
2864
2865		:- use_module(state_packing).
2866		:- use_module(tools,[start_ms_timer/1,stop_ms_walltimer_with_msg/2, stop_ms_timer_with_debug_msg/2]).
2867		:- use_module(rulesdslsrc(rule_validation),[setup_rules_extras/0]).
2868		% maybe this predicate should be directly called by b_load_machine
2869		b_machine_precompile :- debug_println(9,'Precompiling B Machine'),
2870		start_ms_timer(T1),
2871		get_full_b_machine(_,_),
2872		auto_precompile,
2873		stop_ms_timer_with_debug_msg(T1,'auto_precompile: '),
2874		precompile_operation_names_in_reverse_order,
2875		% TODO(DP, 14.8.2008): remove reference to b_global_sets
2876		start_ms_timer(T2),
2877		b_check_and_precompile_deferred_sets,
2878		stop_ms_timer_with_debug_msg(T2,'precompiling global sets: '),
2879		% Now done in bmachine_construction:clean_up_machine but not yet for Event-B:
2880		get_section_from_current_machine(freetypes,Freetypes),register_freetypes(Freetypes),
2881		auto_precompile_phase2,
2882		b_check_and_precompile_global_set_symmetry,
2883		state_packing:precompile_state_packing,
2884		do_machine_consistency_check,
2885		try_kodkod,
2886		(animation_minor_mode(rules_dsl) -> setup_rules_extras ; true),
2887		stop_ms_timer_with_debug_msg(T1,'complete precompiling B machine: ').
2888
2889		% recompile predicates which change when definitionss are loaded (e.g., CUSTOM_GRAPH or similar)
2890		b_machine_recompile_for_new_defs :-
2891		start_ms_timer(T1),
2892		auto_recompile_for_new_defs,
2893		stop_ms_timer_with_debug_msg(T1,'recompile for defs: ').
2894		auto_recompile_for_new_defs :-
2895		% failure-driven loop
2896		(mandatory_pre_compilation_for_new_defs_or_mch(Pred/Arity)
2897		; requires_pre_compilation_for_new_defs(Pred/Arity)
2898		; precompiled_predicate_no_error_when_not_precompiled(Pred/Arity)
2899		), %print(precompile(Pred/Arity)),nl,
2900		auto_precompile2(Pred,Arity,Pattern),
2901		(Pattern -> true /* this pattern already asserted */
2902		; assertz(Pattern)), fail.
2903		auto_recompile_for_new_defs.
2904
2905		auto_recompile_for_new_main_machine :-
2906	?	mandatory_pre_compilation_for_new_defs_or_mch(Pred/Arity),
2907		% required for b_get_preferences_from_specification / update_preferences_from_spec called beore b_machine_precompile
2908	?	auto_precompile2(Pred,Arity,Pattern),
2909		(Pattern -> true /* this pattern already asserted */
2910		; assertz(Pattern)), fail.
2911		auto_recompile_for_new_main_machine.
2912
2913		% these need to be pre-compiled straightaway; so that b_get_preferences_from_specification works
2914		mandatory_pre_compilation_for_new_defs_or_mch(b_get_definition_name_with_pos/4).
2915		mandatory_pre_compilation_for_new_defs_or_mch(b_get_definition_string_from_machine/3).
2916
2917		requires_pre_compilation_for_new_defs(b_get_machine_goal/1).
2918		requires_pre_compilation_for_new_defs(b_get_machine_searchscope/1).
2919		requires_pre_compilation_for_new_defs(b_get_machine_operation_max/2). % Note: requires b_operation_name to be precompiled
2920		requires_pre_compilation_for_new_defs(b_get_machine_operation_time_out/2). % ditto
2921		% following already covered in precompiled_predicate_no_error_when_not_precompiled:
2922		%requires_pre_compilation_for_new_defs(b_get_machine_heuristic_function/1).
2923		%requires_pre_compilation_for_new_defs(b_get_machine_custom_nodes_function/2).
2924		%requires_pre_compilation_for_new_defs(b_get_machine_custom_graph_function/2).
2925
2926		other_spec_precompile :- retractall(bmachine_is_precompiled),
2927		/* call if you do not animate a B specification */
2928		is_precompiled_predicate(Pred/Arity),
2929		functor(Pattern,Pred,Arity),
2930		retractall(Pattern),
2931		(precompiled_predicate_no_error_when_not_precompiled(Pred/Arity)
2932		-> assertz( (Pattern :- fail ))
2933		; assertz( (Pattern :- print_message('No B machine available for '), print_message(Pattern), fail) )
2934		),
2935		fail.
2936		other_spec_precompile :-
2937		retractall(b_get_machine_constants(_)),
2938		assertz( b_get_machine_constants([]) ),
2939		retractall(b_get_machine_variables_in_original_order(_)),
2940		assertz( b_get_machine_variables_in_original_order([]) ),
2941		retractall(b_get_machine_variables(_)),
2942		assertz( b_get_machine_variables([]) ),
2943		retractall(b_get_static_assertions_from_machine(_)),
2944		assertz( b_get_static_assertions_from_machine([]) ),
2945		retractall(b_machine_has_static_assertions),
2946		retractall(b_get_unproven_static_assertions_from_machine(_)),
2947		assertz( b_get_unproven_static_assertions_from_machine([]) ),
2948		retractall(b_get_dynamic_assertions_from_machine(_)),
2949		assertz( b_get_dynamic_assertions_from_machine([]) ),
2950		retractall(b_machine_has_dynamic_assertions),
2951		retractall(b_get_unproven_dynamic_assertions_from_machine(_)),
2952		assertz( b_get_unproven_dynamic_assertions_from_machine([]) ),
2953		retractall( b_get_machine_searchscope(_) ),
2954		retractall( b_get_machine_goal(_) ),
2955		retractall( b_machine_name(_) ),
2956		retractall( b_is_constant(_,_) ),
2957		retractall( b_is_variable(_,_) ),
2958		assert_bmachine_is_precompiled, debug_println(4,other_spec_precompile).
2959
2960	?	is_precompiled_predicate(P) :- precompiled_predicate(P).
2961	?	is_precompiled_predicate(P) :- precompiled_predicate_phase2(P).
2962
2963		% phase 1 precompilation: required by b_global_sets
2964		precompiled_predicate(b_machine_name/1).
2965		precompiled_predicate(b_get_definition_name_with_pos/4).
2966		precompiled_predicate(b_get_named_machine_set/3).
2967		precompiled_predicate(b_enumerated_sets_precompiled/0).
2968		precompiled_predicate(b_get_properties_from_machine/1).
2969		precompiled_predicate(b_get_machine_all_constants/1).
2970		precompiled_predicate(b_get_machine_set/2).
2971		precompiled_predicate(b_get_disjoint_constants_of_type/3).
2972		precompiled_predicate(b_get_constant_represented_inside_global_set/2).
2973		precompiled_predicate(b_get_machine_constants/1).
2974		precompiled_predicate(b_get_machine_variables_in_original_order/1).
2975		precompiled_predicate(b_get_machine_variables/1).
2976		precompiled_predicate(b_get_invariant_from_machine/1).
2977		precompiled_predicate(b_get_linking_invariant_from_machine/1).
2978		precompiled_predicate(b_is_constant/2).
2979		precompiled_predicate(b_is_variable/2).
2980		precompiled_predicate(b_get_constant_variable_description/2).
2981		precompiled_predicate(b_get_static_assertions_from_machine/1).
2982		precompiled_predicate(b_machine_has_static_assertions/0).
2983		precompiled_predicate(b_get_unproven_static_assertions_from_machine/1).
2984		precompiled_predicate(b_get_dynamic_assertions_from_machine/1).
2985		precompiled_predicate(b_machine_has_dynamic_assertions/0).
2986		precompiled_predicate(b_get_unproven_dynamic_assertions_from_machine/1).
2987		precompiled_predicate(b_get_assertions_from_main_machine/2).
2988		precompiled_predicate(b_get_initialisation_from_machine/2).
2989		precompiled_predicate(b_get_machine_operation/6).
2990		precompiled_predicate(b_top_level_operation/1).
2991		precompiled_predicate(b_is_operation_name/1).
2992		precompiled_predicate(b_top_level_operation_without_machine_prefix/2).
2993		precompiled_predicate(b_top_level_feasible_operation/1).
2994		precompiled_predicate(b_get_promoted_machine_operations/1).
2995		precompiled_predicate(get_operation_info/2).
2996		precompiled_predicate(b_get_machine_operation_for_animation/7).
2997		precompiled_predicate(get_operation_description_template_expr/2).
2998		precompiled_predicate(b_get_machine_goal/1).
2999		precompiled_predicate(b_get_machine_setscope/2).
3000		precompiled_predicate(b_get_machine_operation_max/2).
3001		precompiled_predicate(b_get_machine_operation_time_out/2).
3002		precompiled_predicate(b_get_machine_searchscope/1).
3003		precompiled_predicate(b_get_definition_string_from_machine/3).
3004		precompiled_predicate(b_get_machine_animation_function/2).
3005		precompiled_predicate(b_get_machine_heuristic_function/1).
3006		precompiled_predicate(b_get_machine_animation_expression/2).
3007		precompiled_predicate(b_get_machine_custom_nodes_function/2).
3008		precompiled_predicate(b_get_machine_custom_edges_function/2).
3009		precompiled_predicate(b_get_machine_custom_graph_function/2).
3010		precompiled_predicate(complete_discharged_info/0). % just call it before calling b_specialized_invariant_for_op_calc !
3011		precompiled_predicate(get_proven_invariant/2).
3012		precompiled_predicate(b_nth1_invariant/3).
3013		precompiled_predicate(b_nth1_invariant_is_ignored/1).
3014		precompiled_predicate(b_invariant_number_list/1).
3015		precompiled_predicate(b_specialized_invariant_mask_for_op/2).
3016		precompiled_predicate(b_specialized_invariant_for_op/2).
3017		precompiled_predicate(b_operation_preserves_invariant/2).
3018		precompiled_predicate(b_get_all_used_identifiers_in_section/2).
3019		precompiled_predicate(b_get_all_used_identifiers/1).
3020		precompiled_predicate(b_is_unused_constant/1).
3021		precompiled_predicate(b_extract_values_clause_assignment/3). % depends on b_is_constant/1
3022		precompiled_predicate(b_machine_statistics/2).
3023
3024		% require b_global_sets to be initialised
3025		precompiled_predicate_phase2(b_get_operation_normalized_read_write_info/3).
3026		precompiled_predicate_phase2(b_get_operation_unchanged_variables/2).
3027		precompiled_predicate_phase2(b_operation_cannot_modify_state/1).
3028		precompiled_predicate_phase2(b_operation_reads_output_variables/3).
3029		precompiled_predicate_phase2(b_get_operation_non_det_modifies/2).
3030
3031		% these functions sometimes get called also in csp mode; simply fail silently for those cases in other_spec_precompile
3032		% they also get recompiled when new definition file is added
3033		precompiled_predicate_no_error_when_not_precompiled(b_get_machine_animation_function/2).
3034		precompiled_predicate_no_error_when_not_precompiled(b_get_machine_heuristic_function/1).
3035		precompiled_predicate_no_error_when_not_precompiled(b_get_machine_animation_expression/2).
3036		precompiled_predicate_no_error_when_not_precompiled(b_get_machine_custom_nodes_function/2).
3037		precompiled_predicate_no_error_when_not_precompiled(b_get_machine_custom_edges_function/2).
3038		precompiled_predicate_no_error_when_not_precompiled(b_get_machine_custom_graph_function/2).
3039
3040		% on startup, all precompiled predicates yield error message
3041		startup_precompiled :- retractall(bmachine_is_precompiled),
3042	?	is_precompiled_predicate(Pred/Arity),
3043		functor(Pattern,Pred,Arity),
3044		retractall(Pattern),
3045		assertz( (Pattern :- add_error(bmachine,'B machine not precompiled for ',Pattern),fail) ),
3046		fail.
3047		startup_precompiled :- debug_println(4,startup_precompiled).
3048
3049		:- startup_precompiled.
3050
3051		% for each predicate in "precompiled_predicate", auto_precompile computes
3052		% all solutions by calling the predicate with an appended _calc
3053		auto_precompile :- % startup_precompiled,
3054		% failure-driven loop
3055	?	precompiled_predicate(Pred/Arity), %print(precompile(Pred/Arity)),nl,
3056		%statistics(walltime,[Tot,Delta]), format('Precompiling ~w/~w [~w ms (Delta ~w) ms]~n',[Pred,Arity,Tot,Delta]),
3057	?	auto_precompile2(Pred,Arity,Pattern),
3058		(Pattern -> true /* this pattern already asserted */
3059		; assertz(Pattern)), fail.
3060		auto_precompile :-
3061		assert_bmachine_is_precompiled, debug_println(4,auto_precompile).
3062		auto_precompile_phase2 :-
3063		% failure-driven loop
3064	?	precompiled_predicate_phase2(Pred/Arity), %print(precompile(Pred/Arity)),nl,
3065	?	auto_precompile2(Pred,Arity,Pattern),
3066		(Pattern -> true /* this pattern already asserted */
3067		; assertz(Pattern)), fail.
3068		auto_precompile_phase2.
3069
3070		% if the precompiled predicates is e.g. foo/2 then
3071		% Pattern=foo(A,B) and Call=foo_calc(A,B)
3072		auto_precompile2(Pred,Arity,Pattern) :-
3073		atom_concat(Pred,'_calc',CallFunctor),
3074		functor(Pattern,Pred,Arity),
3075		functor(Call,CallFunctor,Arity),
3076		unify_args(Arity,Call,Pattern),
3077		retractall(Pattern), % probably just removes clause added by startup_precompiled
3078		% the failure-driven loop for one predicate
3079	?	call(Call).
3080
3081		unify_args(0,_,_) :- !.
3082		unify_args(N,A,B) :-
3083		arg(N,A,Arg), arg(N,B,Arg),
3084		N1 is N-1, unify_args(N1,A,B).
3085
3086
3087		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3088		% set machine goal
3089
3090		b_set_machine_goal(Goal) :- b_set_machine_goal(Goal,false).
3091		b_set_machine_goal(Goal,WithDeferredSets) :-
3092		get_tc_scope(WithDeferredSets,Scope),
3093		b_parse_machine_predicate(Goal,Scope,TypedPred),
3094		b_set_parsed_typed_machine_goal(TypedPred).
3095
3096		b_set_parsed_typed_machine_goal(TypedPred) :-
3097		retractall(b_get_machine_goal(_)),
3098		assertz(b_get_machine_goal(TypedPred)).
3099
3100		b_unset_machine_goal :-
3101		retractall(b_get_machine_goal(_)).
3102
3103
3104		% get typechecking scope:
3105		get_tc_scope(with_deferred,Scope) :- !,
3106		Scope = [prob_ids(visible),variables,external_library(all_available_libraries)].
3107		% with external libraries we can use e.g. GET_IS_DET_OUTPUT("OpName")=FALSE
3108		get_tc_scope(with_deferred_and_primed,Scope) :- !,
3109		get_primed_machine_variables(PV), % this can be useful for visualisation, but will not work during mc
3110		Scope = [prob_ids(visible),identifier(PV),variables,external_library(all_available_libraries)].
3111		get_tc_scope(_,[variables]).
3112
3113		% set search_scope, restricting model checking to states which satisfy the SCOPE DEFINITION predicate
3114		b_set_machine_searchscope(Goal) :- b_set_machine_searchscope(Goal,with_deferred).
3115		b_set_machine_searchscope(Goal,WithDeferredSets) :-
3116		get_tc_scope(WithDeferredSets,Scope),
3117		b_parse_machine_predicate(Goal,Scope,TypedPred),
3118		b_set_parsed_typed_machine_searchscope(TypedPred).
3119		b_set_parsed_typed_machine_searchscope(TypedPred) :-
3120		retractall(b_get_machine_searchscope(_)),
3121		assertz(b_get_machine_searchscope(TypedPred)).
3122
3123		% also allow empty string, and #invariant and #not_invariant
3124		b_parse_optional_machine_predicate(TargetString,Target) :-
3125		is_empty_string(TargetString),!,create_texpr(truth,pred,[],Target).
3126		b_parse_optional_machine_predicate('#invariant',Invariant) :- !,
3127		b_get_invariant_from_machine(Invariant).
3128		b_parse_optional_machine_predicate('#not_invariant',TargetPredicate) :- !,
3129		b_get_invariant_from_machine(Invariant),
3130		bsyntaxtree:create_negation(Invariant,TargetPredicate).
3131		b_parse_optional_machine_predicate(TargetString,Target) :-
3132		b_parse_machine_predicate(TargetString,Target).
3133
3134		is_empty_string(Atom) :-
3135		atom_codes(Atom,Codes),
3136		is_empty_string2(Codes).
3137		is_empty_string2([]).
3138		is_empty_string2([32|Codes]) :- is_empty_string2(Codes).
3139
3140
3141		% parsing a string as predicate with deferred set elements
3142		b_parse_machine_predicate(Pred,TypedPred) :- b_parse_machine_predicate(Pred,[variables],TypedPred).
3143		b_parse_machine_predicate(Pred,Scope,TypedPred) :-
3144		atom_codes(Pred,Codes),
3145		b_parse_machine_predicate_from_codes(Codes,Scope,TypedPred).
3146		b_parse_machine_predicate_from_codes(Codes,Scope,TypedPred) :-
3147		b_parse_machine_predicate_from_codes2(Codes,[],Scope,TypedPred,closed).
3148		b_parse_machine_predicate_from_codes_open(OptionalQuantifier,Codes,Defs,Scope,TypedPred) :-
3149		b_parse_machine_predicate_from_codes2(Codes,Defs,Scope,TypedPred,open(OptionalQuantifier)).
3150
3151		b_parse_machine_predicate_from_codes2(Codes,Defs,Scope,TypedPred,Mode) :-
3152		debug_println(9,parse_predicate(Mode)),
3153		(Defs=[] -> true ; debug_println(9,'% Ignoring DEFINITIONS')),
3154		b_parse_wo_type_machine_predicate_from_codes_to_raw_expr(Codes,Parsed),
3155		%format('Raw Parsed AST = ~w~n',[Parsed]),
3156		b_type_check_raw_expr(Parsed,Scope,TypedPred,Mode).
3157
3158		check_codes(X) :- (X=[] ; X=[H|_], number(H)),!.
3159		check_codes(X) :- add_error(bmachine,'Error while parsing: not a code list: ',X),fail.
3160
3161		b_parse_wo_type_machine_predicate_from_codes_to_raw_expr(Codes,ParsedRaw) :-
3162		check_codes(Codes),
3163		catch(
3164		parse_predicate(Codes,ParsedRaw), % ,print(ParsedRaw),nl),
3165		Exception,
3166		( Exception = parse_errors(Errors) -> %print(errors(Errors)),nl,
3167		add_all_perrors(Errors,[],parse_machine_predicate_error),fail
3168		;
3169		add_error(bmachine,'Exception while parsing predicate: ',Exception),
3170		fail)).
3171
3172		b_type_check_raw_expr(ParsedRaw,Scope,TypedPred,Mode) :-
3173		debug_println(9,type_with_errors(ParsedRaw)),
3174		( Mode == closed ->
3175		type_with_errors(ParsedRaw,Scope,pred,TypedPred)
3176		; Mode = open(OptionalQuantifier) ->
3177		b_type_open_predicate_with_errors(OptionalQuantifier,ParsedRaw,Scope,TypedPred)).
3178
3179		% a flexible version: convert atom to codes, but also accept codes list
3180		flexible_atom_codes([],R) :- !, R=[].
3181		flexible_atom_codes(A,R) :- atom(A), !, atom_codes(A,R).
3182		flexible_atom_codes([H|T],List) :- !, List=[H|T].
3183		flexible_atom_codes(Other,List) :- add_internal_error('Not atom or codes list: ',flexible_atom_codes(Other,List)),
3184		List=Other.
3185
3186		b_parse_machine_operation_pre_post_predicate(AtomOrCodes,TypedPred,OpName) :-
3187		b_parse_machine_operation_pre_post_predicate(AtomOrCodes,[],TypedPred,OpName,true).
3188		b_parse_machine_operation_pre_post_predicate(AtomOrCodes,ExtraScope,TypedPred,OpName,GenerateParseErrors) :-
3189		flexible_atom_codes(AtomOrCodes,Codes),
3190		b_parse_predicate(Codes,Parsed,GenerateParseErrors),
3191		(trivial_raw_pred(Parsed) -> Scope=[]
3192		; get_machine_operation_typing_scope(OpName,Scope,ExtraScope)),
3193		b_type_only(Parsed,Scope,pred,TypedPred,GenerateParseErrors).
3194
3195		trivial_raw_pred(truth(_)).
3196		trivial_raw_pred(falsity(_)).
3197
3198		% Note: B and Event-B have different way of priming; this is aimed at classical B
3199		% and supposes predicate used together with execute_operation_by_predicate_in_state
3200		% in classical B x$0 refers to the value before a substitution (e.g., becomes_such)
3201		get_primed_machine_variables(Ids) :-
3202		b_get_machine_variables(Vars),
3203		maplist(prime_variable,Vars,Ids).
3204		:- use_module(btypechecker,[prime_atom0/2]). % add $0 at end of variable
3205		prime_variable(b(identifier(ID),T,I),b(identifier(PID),T,I)) :- prime_atom0(ID,PID).
3206
3207		is_initialisation_op('$setup_constants').
3208		is_initialisation_op('$initialise_machine').
3209
3210		% analog version to b_is_operation_name:
3211		b_is_initialisation_name('$initialise_machine').
3212
3213
3214		get_machine_operation_typing_scope(OpName,Scope,ExtraScope) :-
3215		( get_machine_operation_additional_identifiers(OpName,V) -> true
3216		; add_error_fail(get_machine_operation_typing_scope,'Unknown operation:', OpName)),
3217		Scope = [prob_ids(visible),identifier(V),variables,external_library(all_available_libraries)|ExtraScope].
3218
3219		% get additional ids to add to Scope for typing with identifier(V)
3220		get_machine_operation_additional_identifiers(OpName,V) :- xtl_mode,!,
3221		xtl_interface:get_xtl_paras_as_identifiers(OpName,V).
3222		get_machine_operation_additional_identifiers(OpName,V) :-
3223		is_initialisation_op(OpName),!, V=[].
3224		get_machine_operation_additional_identifiers(OpName,V) :-
3225		b_get_machine_operation_for_animation(OpName,Results,Paras,_),
3226		append(Paras,Results,PR), % b_get_machine_operation_typed_parameters
3227		get_primed_machine_variables(PV),
3228		append(PV,PR,V).
3229
3230		b_get_machine_operation_for_animation(Name,Results,Parameters,Body) :-
3231	?	b_get_machine_operation_for_animation(Name,Results,Parameters,Body,_OType,true).
3232		% interface predicate b_get_machine_operation_for_animation/6
3233		b_get_machine_operation_for_animation(Name,Results,Parameters,Body,OType,TopLevel) :-
3234	?	b_get_machine_operation_for_animation(Name,Results,Parameters,Body,OType,TopLevel,_OpPos).
3235
3236		:- public b_get_machine_operation_for_animation_calc/7.
3237		% adds some additional ANY parameters if preference is set
3238		b_get_machine_operation_for_animation_calc('$initialise_machine',[],Parameters,Body,OType,_TopLevel,OpPos) :-
3239		b_get_machine_variables(DeclaredVars), Parameters=DeclaredVars,
3240		OpPos = unknown, % TODO: improve
3241		b_get_initialisation_from_machine(Body,OType).
3242		b_get_machine_operation_for_animation_calc(Name,Results,Parameters,Body,OType,TopLevel,OpPos) :-
3243		get_preference(show_eventb_any_arguments,EVENTB),
3244	?	b_get_machine_operation(Name,Results,RealParameters,RealBody,OType,OpPos),
3245		% TO DO: check whether we should only keep b_top_level_operation(Name) in case TopLevel==true !
3246		%length(RealParameters,P), format('Get Mach Op ~w ; paras ~w ; EB ~w, TopLevel=~w~n',[Name,P,EVENTB,TopLevel]),
3247		((Results=[_|_] ; RealParameters=[_|_] ; EVENTB=false)
3248		-> Parameters=RealParameters, Body=RealBody
3249		; translate_any_into_parameters(RealBody,FakeParameters,FakeBody),
3250		length(FakeParameters,Len),
3251		(Len > 255
3252		-> add_message(bmachine,'Not adding any parameters to operation, max_arity (255) exceeded: ',Name:Len,OpPos),
3253		Parameters=RealParameters, Body=RealBody
3254		; ( TopLevel=true, Parameters=FakeParameters, Body=FakeBody
3255		; TopLevel=false, Parameters=RealParameters, Body=RealBody
3256		)
3257		)
3258		; Parameters=RealParameters, Body=RealBody
3259		).
3260
3261		% TO DO: limit to max_arity
3262		translate_any_into_parameters(b(E,Type,Info),Parameters,NewSubst) :-
3263		translate_any_into_parameters_aux(E,Type,Info,Parameters,NewSubst).
3264		translate_any_into_parameters_aux(any(Parameters,PreCond,ABody),Type,Info,Parameters,NewSubst) :-
3265		NewSubst=b(select([b(select_when(PreCond,ABody),Type,Info)]),Type,Info). % TO DO: go deeper ? (nested ANY ?)
3266		translate_any_into_parameters_aux(let(Parameters,Defs,LBody),Type,Info,Parameters,NewSubst) :-
3267		NewSubst=b(select([b(select_when(Defs,LBody),Type,Info)]),Type,Info). % TO DO: go deeper ? ANY could have been translated into several LETs ?
3268		translate_any_into_parameters_aux(lazy_let_subst(Id,IdExpr,Body),Type,Info,Parameters,NewSubst) :-
3269		NewSubst=b(lazy_let_subst(Id,IdExpr,NewInnerSubst),Type,Info),
3270		translate_any_into_parameters(Body,Parameters,NewInnerSubst).
3271
3272
3273		% add deferred set prob_ids and external libraries as well
3274		% ExtraScope could e.g. be [identifier(TypedIDLIst)]
3275		b_parse_machine_expression_from_codes_with_prob_ids(Codes,ExtraScope,TypedExpr,GenerateParseErrors) :-
3276		extend_typing_scope_for_stored_lets([prob_ids(visible),variables_and_additional_defs,
3277		external_library(all_available_libraries)|ExtraScope],
3278		Scope),
3279		b_parse_machine_expression_from_codes4(Codes,Scope,TypedExpr,GenerateParseErrors).
3280		b_parse_machine_expression_from_codes_with_prob_ids(Codes,ExtraScope,TypedExpr) :-
3281		b_parse_machine_expression_from_codes_with_prob_ids(Codes,ExtraScope,TypedExpr,true).
3282		b_parse_machine_expression_from_codes_with_prob_ids(Codes,TypedExpr) :-
3283		b_parse_machine_expression_from_codes_with_prob_ids(Codes,[],TypedExpr,true).
3284
3285		b_parse_machine_expression_from_codes(Codes,TypedExpr) :-
3286		b_parse_machine_expression_from_codes4(Codes,[variables],TypedExpr,true).
3287
3288		b_parse_machine_expression_from_codes4(Codes,Scope,TypedExpr,GenerateParseErrors) :-
3289		b_parse_machine_expression_from_codes(Codes,Scope,TypedExpr,_Type,GenerateParseErrors,Error),!,
3290		(Error=none -> true
3291		; generate_parse_errors_for(GenerateParseErrors,Position,ErrOrWarn),
3292		add_msg_warn_or_err(ErrOrWarn,b_parse_machine_expression_from_codes,
3293		'Errors occured during parsing:', Error,Position),
3294		% format(user_error,'Parsing: ~s~n',[Codes]),
3295		fail).
3296
3297
3298		%b_parse_machine_expression_from_codes(Codes,TypedExpr) :-
3299		% b_parse_machine_expression_from_codes(Codes,TypedExpr,_Type,false,Error), Error=none.
3300
3301		b_parse_machine_expression_from_codes(Codes,Typed,Type,GenerateParseErrors,Error) :-
3302		b_parse_machine_expression_from_codes(Codes,[variables],
3303		Typed,Type,GenerateParseErrors,Error).
3304		b_parse_machine_expression_from_codes(Codes,Scope,
3305		Typed,Type,GenerateParseErrors,Error) :-
3306		b_parse_machine_formula_from_codes(expression,Codes,Scope,
3307		Typed,Type,GenerateParseErrors,Error).
3308
3309		% parse substitutions so as to allow operation calls; useful for REPL or trace files:
3310		b_parse_machine_subsitutions_from_codes(Codes,Scope,
3311		Typed,Type,GenerateParseErrors,Error) :-
3312		temporary_set_preference(allow_local_operation_calls,true,CHNG),
3313		call_cleanup(
3314		b_parse_machine_formula_from_codes(substitution,Codes,Scope,
3315		Typed,Type,GenerateParseErrors,Error),
3316		reset_temporary_preference(allow_local_operation_calls,CHNG)).
3317
3318		% a variant of b_parse_machine_predicate that allows also expressions
3319		b_parse_machine_formula(PredOrExpr,Scope,TypedPredOrExpr) :-
3320		atom_codes(PredOrExpr,Codes),
3321		b_parse_machine_formula_from_codes(formula,Codes,Scope,
3322		TypedPredOrExpr,_Type,true,Error), Error=none.
3323
3324		% Kind = expression, predicate, formula, substitution
3325		% GnerateParseErrors = true, false, type_errors_only, gen_parse_errors_for/2
3326		b_parse_machine_formula_from_codes(Kind,Codes,Scope,
3327		Typed,Type,GenerateParseErrors,Error) :-
3328		b_parse_only(Kind,Codes, ParsedAST, GenerateParseErrors, Error),
3329		%print(parsed(Parsed,Error)),nl,
3330		( nonvar(Error) -> true /* either exception or parse error occured */
3331		; generate_no_parse_errors(GenerateParseErrors), type_without_errors(ParsedAST,Scope,Type,Typed) -> Error=none
3332		; b_type_only(ParsedAST,Scope,Type,Typed,GenerateParseErrors) -> Error=none
3333		; Error=type_error).
3334
3335		% typing with or without errors, depending on GenerateParseErrors flag
3336		b_type_only(ParsedAST,Scope,Type,Typed,GenParseErrors) :-
3337		generate_parse_errors_for(GenParseErrors,_Pos,ErrOrWarn),!,
3338		% ParsedAST now contains filenumber for additional file
3339		type_with_errors_in_context(ParsedAST,Scope,Type,Typed,machine_context,ErrOrWarn).
3340		b_type_only(ParsedAST,Scope,Type,Typed,false) :- !,
3341		type_without_errors(ParsedAST,Scope,Type,Typed).
3342		b_type_only(ParsedAST,Scope,Type,Typed,_GenerateParseErrors) :-
3343		type_with_errors_in_context(ParsedAST,Scope,Type,Typed,no_machine_context([]),error).
3344
3345		% GenerateParseErrors can also provide context filename
3346		b_parse_predicate(Codes,ParsedAST,GenerateParseErrors) :-
3347		b_parse_only(predicate,Codes, ParsedAST, GenerateParseErrors,Error),
3348		Error=none.
3349
3350		b_parse_only(Kind,Codes, ParsedAST, _,Error) :- (Codes \= [] , Codes \= [_|_]),!,
3351		add_internal_error('Not a codes list: ',b_parse_only(Kind,Codes, ParsedAST, _, Error)),
3352		Error = internal_error.
3353		b_parse_only(Kind,Codes, ParsedAST, GenerateParseErrors,Error) :-
3354		generate_parse_errors_for(GenerateParseErrors,Position,ErrOrWarn),!,
3355		% we should generate errors in a particular file context
3356		(extract_file_number_and_name(Position,FileNr,Filename)
3357		-> Files=[Filename] ; FileNr = -1, Files=[]),
3358		(number(FileNr) -> NewFileNr=FileNr ; add_additional_filename(Filename,NewFileNr)),
3359		catch( parse_at_position_in_file(Kind,Codes,ParsedAST,Position,NewFileNr),
3360		Exception,
3361		((Exception = parse_errors(Errors) ->
3362		add_all_perrors(Errors,Files,parse_machine_formula_error,ErrOrWarn),
3363		Error=parse_error
3364		;
3365		ajoin(['Exception while parsing ',Kind,': '],Msg),
3366		add_msg_warn_or_err(ErrOrWarn,bmachine,Msg,Exception,Position),
3367		Error=exception))).
3368		b_parse_only(Kind,Codes, ParsedAST, _GenerateParseErrors,_Error) :-
3369		catch( parse(Kind,Codes,ParsedAST),
3370		Exception,
3371		(debug_println(19,parse_exception(Exception)),fail)).
3372
3373		%generate_type_errors_for(type_errors_only,unknown,[]).
3374		%generate_type_errors_for(GenerateParseErrors,Pos) :- generate_parse_errors_for(GenerateParseErrors,Pos).
3375
3376		generate_parse_errors_for(true,unknown,error).
3377		generate_parse_errors_for(gen_parse_errors_for(Pos),Pos,error).
3378		generate_parse_errors_for(gen_parse_warnings_for(Pos),Pos,warning).
3379
3380		generate_no_parse_errors(false).
3381
3382		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3383
3384		% a flexible parsing predicate, useful for dot and table tools to be called from
3385		% either probcli or prob2 with either atoms or with raw ASTs:
3386
3387		:- use_module(eval_let_store,[extend_typing_scope_for_stored_lets/2]).
3388		parse_expression_raw_or_atom_with_prob_ids(Expr,TypedExpr) :-
3389		extend_typing_scope_for_stored_lets([prob_ids(visible),variables,external_library(all_available_libraries)],Scope),
3390		parse_expression_raw_or_atom3(Expr,Scope,TypedExpr).
3391
3392		parse_expression_raw_or_atom3('$VARIABLES',_,TypedExpr) :- !,
3393		b_get_machine_variables(DeclaredVars),
3394		gen_couple_from_list(DeclaredVars,TypedExpr).
3395		parse_expression_raw_or_atom3(RawAST,Scope,TypedExpr) :- compound(RawAST),!, % allow to pass raw AST as well
3396		type_with_errors(RawAST,Scope,Type,TypedExpr),
3397		((Type=pred ; Type=subst)
3398		-> add_error(parse_expression,'Expected expression formula but obtained: ',Type),fail
3399		; true ).
3400		parse_expression_raw_or_atom3(VorE,Scope,TypedExpr) :-
3401		atom_codes(VorE,VorECodes),
3402		% to do: maybe support b_parse_machine_expression_from_codes_with_prob_ids
3403		b_parse_machine_expression_from_codes4(VorECodes,Scope,TypedExpr,true).
3404
3405		:- use_module(bsyntaxtree, [create_couple/3]).
3406		gen_couple_from_list([],string('NO VARIABLES')).
3407		gen_couple_from_list([TID],Res) :- !, Res=TID.
3408		gen_couple_from_list([TID|T],Couple) :-
3409		gen_couple_from_list(T,Rest),
3410		create_couple(TID,Rest,Couple).
3411
3412
3413		:- use_module(btypechecker,[prime_atom0/2]). % add $0 at end of variable
3414		:- use_module(bsyntaxtree, [find_typed_identifier_uses/2,get_texpr_id/2]).
3415		% compute requirements for evaluating formula
3416		% requires_nothing, requires_constants, requires_variables
3417		determine_type_of_formula(TypedExpr,Class) :-
3418		determine_type_of_formula(TypedExpr,_,Class).
3419		determine_type_of_formula(TypedExpr,Identifiers,Class) :-
3420		find_typed_identifier_uses(TypedExpr,Identifiers),
3421		determine_type_of_formula2(Identifiers,Class).
3422		determine_type_of_formula2([],Res) :- !, Res = requires_nothing.
3423		determine_type_of_formula2(Ids,Res) :-
3424		member(TID,Ids), get_texpr_id(TID,ID),
3425		(b_is_variable(ID,_) -> true
3426		; prime_atom0(Original,ID),
3427		(b_is_variable(Original,_) -> true ; add_warning(bmachine,'Unknown primed variable: ',ID))
3428		),
3429		!, Res = requires_variables.
3430		determine_type_of_formula2(Ids,Res) :-
3431		member(TID,Ids), get_texpr_id(TID,ID),
3432		b_is_constant(ID,_),
3433		!, Res = requires_constants.
3434		determine_type_of_formula2(_,requires_nothing).
3435		% only open, implicitly existentially quantified variables
3436		% also, TO DO: check that insert_before_substitution_variables / $0 variables are properly treated
3437		% TODO: there are external functions like ENABLED(.) which implicitly require a state with variables
3438
3439		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3440		% consistency check to spot some errors
3441		do_machine_consistency_check :-
3442		specfile:animation_mode(b), % TODO (dp,27.09.2012): this is just an ugly hack
3443		type_check_definitions,
3444	?	minor_mode_to_check,
3445		%debug:time(bmachine:all_operations_have_valid_read_modifies_infos).
3446		!,
3447		all_operations_have_valid_read_modifies_infos.
3448		do_machine_consistency_check.
3449
3450		% In future, all formalisms should provide the relevent data
3451		minor_mode_to_check :- animation_minor_mode(eventb),!.
3452	?	minor_mode_to_check :- classical_b_mode.
3453
3454		all_operations_have_valid_read_modifies_infos :-
3455		%findall(O,b_get_machine_operation(O,_,_,_,_),OpNames),
3456		%maplist(operation_has_valid_read_modifies_infos,OpNames).
3457	?	b_get_operation_pos(OpName,Pos),
3458		operation_has_valid_read_modifies_infos(OpName,Pos),fail.
3459		all_operations_have_valid_read_modifies_infos.
3460
3461		operation_has_valid_read_modifies_infos(OpName,Pos) :- % print(check(OpName)),nl,
3462		( operation_has_valid_read_modifies_infos2(OpName,Pos) -> true
3463		; add_failed_call_error(operation_has_valid_read_modifies_infos2(OpName,Pos))).
3464		operation_has_valid_read_modifies_infos2(OpName,Pos) :-
3465		b_get_operation_normalized_read_write_info(OpName,Reads,Writes),
3466		maplist(check_read(OpName,Pos),Reads),
3467		%print(operation(OpName,reads(Reads),writes(Writes))),nl,
3468		maplist(check_write(OpName,Pos),Writes).
3469
3470
3471		:- use_module(translate,[translate_span_with_filename/2]).
3472		:- use_module(bmachine_construction,[abstract_variable_removed_in/3]).
3473		check_read(OpName,Pos,Id) :-
3474		( (check_is_var(Id); check_is_constant(Id) ; check_is_operation(Id)) -> true
3475		; abstract_variable_removed_in(Id,Mch,TId) ->
3476		translate_span_with_filename(TId,SP),
3477		ajoin(['Operation reads invisible abstract variable `',Id,'` ',SP,', removed in ',Mch,':'],Msg),
3478		% this shows that in that refinement step we removed a variable without adapting an operation
3479		add_error(bmachine,Msg,OpName,Pos)
3480		;
3481		ajoin(['Unknown identifier `',Id,'` in "reads" information of operation:'],Msg),
3482		add_internal_error(bmachine,Msg,OpName,Pos)).
3483		check_write(OpName,Pos,Id) :-
3484		( check_is_var(Id) -> true
3485		; abstract_variable_removed_in(Id,Mch,TId) ->
3486		translate_span_with_filename(TId,SP),
3487		ajoin(['Operation writes invisible abstract variable `',Id,'` ',SP,', removed in ',Mch,':'],Msg),
3488		% this shows that in that refinement step we removed a variable without adapting an operation
3489		add_error(bmachine,Msg,OpName,Pos)
3490		;
3491		ajoin(['Unknown variable `',Id,'` in "modifies" information of operation:'],Msg),
3492		add_internal_error(bmachine,Msg,OpName,Pos)).
3493
3494		check_is_var(Id) :-
3495		b_is_variable(Id,_).
3496		%get_texpr_id(E,Id),
3497		%b_get_machine_variables(Vars),
3498		%memberchk(E,Vars).
3499		check_is_constant(Id) :- b_is_constant(Id,_).
3500		check_is_constant(Id) :- b_get_constant_represented_inside_global_set(Id,_).
3501		% b_get_machine_all_constants(Constants),
3502		% get_texpr_id(TId,Id),
3503		% memberchk(TId,Constants).
3504		check_is_constant(Id) :- b_get_machine_set(Id).
3505		check_is_constant(Id) :- b_get_named_machine_set(Id,_).
3506		check_is_constant(Id) :-
3507		b_get_named_machine_set(_,Elems),member(Id,Elems).
3508		%check_is_constant(Id) :- % add later when we deal FREETYPE section in classical B as in Z
3509		% kernel_freetypes:freetype_register_db(Id,_) ;
3510		% kernel_freetypes:freetype_case_db(Id,_,_).
3511
3512		check_is_operation(op(ID)) :-
3513		b_is_operation_name(ID), % TO DO: check that other predicates can deal with op(Id) infos
3514		get_preference(allow_operation_calls_in_expr,true).
3515
3516		% provide access to number of constants, ....:
3517
3518		:- volatile b_machine_statistics/2.
3519		:- dynamic b_machine_statistics/2.
3520		:- public b_machine_statistics_calc/2.
3521		b_machine_statistics_calc(files,Nr) :-
3522		b_get_all_used_filenames(L),length(L,Nr).
3523		b_machine_statistics_calc(deferred_sets,Nr) :-
3524		get_section_from_current_machine(deferred_sets,L),length(L,Nr).
3525		b_machine_statistics_calc(enumerated_sets,Nr) :-
3526		get_section_from_current_machine(enumerated_sets,L),length(L,Nr).
3527		b_machine_statistics_calc(definitions,Nr) :-
3528		get_section_from_current_machine(definitions,L),length(L,Nr).
3529		b_machine_statistics_calc(constants,Nr) :- b_get_machine_constants(L), length(L,Nr).
3530		b_machine_statistics_calc(variables,Nr) :- b_get_machine_variables(L), length(L,Nr).
3531		b_machine_statistics_calc(properties,Nr) :-
3532		b_get_properties_from_machine(C), conjunction_to_list(C,L),length(L,Nr).
3533		b_machine_statistics_calc(invariants,Nr) :-
3534		b_get_invariant_from_machine(C), conjunction_to_list(C,L),length(L,Nr).
3535		b_machine_statistics_calc(static_assertions,Nr) :-
3536		b_get_static_assertions_from_machine(L), length(L,Nr).
3537		b_machine_statistics_calc(dynamic_assertions,Nr) :-
3538		b_get_dynamic_assertions_from_machine(L), length(L,Nr).
3539		b_machine_statistics_calc(operations,Nr) :- findall(N,b_is_operation_name(N),L),length(L,Nr).
3540
3541		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
3542		% default and initial machines
3543		b_set_initial_machine :-
3544		initial_machine(Main,Machines),
3545		b_set_machine(Main,Machines,[]).
3546
3547		initial_machine(phonebook,[M]) :-
3548		M = abstract_machine(none,machine(none),machine_header(none,phonebook,[]),Body),
3549		Body = [sets(none, [deferred_set(none,'Name'),
3550		deferred_set(none,'Code')]),
3551		definitions(none,[ScopeName,ScopeCode,TraceTest0]),
3552		variables(none, [identifier(none, db)]),
3553		invariant(none, member(none,
3554		identifier(none, db),
3555		partial_function(none,
3556		identifier(none, 'Name'),
3557		identifier(none, 'Code')))),
3558		initialisation(none,
3559		assign(none, [identifier(none, db)], [empty_set(none)])),
3560		operations(none, [Add,Lookup,Update,Reset])],
3561
3562		% definitions
3563		ScopeName = expression_definition(none,
3564		scope_Name,
3565		[],
3566		interval(none, integer(none, 1), integer(none, 3))),
3567		ScopeCode = expression_definition(none,
3568		scope_Code,
3569		[],
3570		interval(none, integer(none, 1), integer(none, 2))),
3571		TraceTest0 = expression_definition(none, trace_Test0, [], empty_sequence(none)),
3572
3573		% add operation
3574		Add = operation(none,
3575		identifier(none, add),
3576		[],
3577		[identifier(none,cc),identifier(none,nn)],
3578		precondition(none, AddPre, AddAssign)),
3579		AddPre = conjunct(none,
3580		conjunct(none,
3581		member(none, identifier(none,nn), identifier(none,'Name')),
3582		member(none, identifier(none,cc), identifier(none,'Code'))),
3583		not_member(none,
3584		identifier(none,nn),
3585		domain(none, identifier(none,db)))),
3586		AddAssign = assign(none,
3587		[identifier(none,db)],
3588		[union(none,
3589		identifier(none,db),
3590		set_extension(none,
3591		[couple(none,[identifier(none,nn),
3592		identifier(none,cc)])]))]),
3593
3594		% lookup operation
3595		Lookup = operation(none,
3596		identifier(none, lookup),
3597		[identifier(none, cc)],
3598		[identifier(none, nn)],
3599		precondition(none, LookupPre, LookupAssign)),
3600		LookupPre = member(none, identifier(none,nn), domain(none,identifier(none,db))),
3601		LookupAssign = assign(none,
3602		[identifier(none, cc)],
3603		[function(none, identifier(none, db), identifier(none, nn))]),
3604
3605		% update operation
3606		Update = operation(none,
3607		identifier(none, update),
3608		[],
3609		[identifier(none,nn),identifier(none,cc)],
3610		precondition(none, UpdatePre, UpdateAssign)),
3611		UpdatePre = conjunct(none,
3612		conjunct(none,
3613		member(none, identifier(none,nn), identifier(none,'Name')),
3614		member(none, identifier(none,cc), identifier(none,'Code'))),
3615		member(none,
3616		identifier(none,nn),
3617		domain(none, identifier(none,db)))),
3618		UpdateAssign = assign(none,
3619		[function(none, identifier(none,db), identifier(none,nn))],
3620		[identifier(none, cc)]),
3621
3622		% reset operation
3623		Reset = operation(none,
3624		identifier(none,reset),
3625		[],
3626		[],
3627		precondition(none, ResetPre, ResetAssign)),
3628		ResetPre = member(none,
3629		identifier(none, db),
3630		total_function(none, identifier(none,'Name'), identifier(none,'Code'))),
3631		ResetAssign = assign(none,[identifier(none,db)],[empty_set(none)]).
3632
3633		empty_machine(empty_machine,[M]) :-
3634		M = abstract_machine(none,machine(none),machine_header(none,empty_machine,[]),Body),
3635		Body = [].
3636
3637		% after transformation this gives
3638		% 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]]])
3639
3640		% Code to inspect sizes of operations:
3641		% 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.