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		:- module(b_machine_hierarchy,[analyse_hierarchy/2
6		,analyse_eventb_hierarchy/2
7		,main_machine_name/1 % find out name of main machine
8		,machine_name/1 % can be used to find out machine names
9		,machine_type/2 % machine_type(Name, R) - get the type
10		% (abstract_machine, abstract_model, refinement, implementation) for the machine named Name
11		,machine_references/2 % get a list of references and the type of the reference.
12		% Example: if A refines B, then machine_references('A',X) returns X= [ref(refines'B','')].
13		% The last argument in ref/3 is the prefix
14		,machine_identifiers/7 % gets Params,Sets,Abstract Variables,Concrete Variables,Abstract Constants and Concrete
15		% Constants for a machine. Abstract constants/Variables are introduced in the machine
16		% using the ABSTRACT_VARAIABLES/ABSTARCT_CONSTANTS keyword. The concrete versions
17		% analogously via CONCRETE_VARAIBLES,CONCRETE_CONSTANTS
18		% Example output for
19		% MACHINE xx(T,u)
20		% CONSTRAINTS u:T
21		% SETS A; B={foo, bar}
22		% CONCRETE_CONSTANTS cc
23		% PROPERTIES cc:B
24		% ABSTRACT_VARIABLES xx
25		% CONCRETE_VARIABLES yy
26		% INVARIANT
27		% xx:INT &
28		% yy : T
29		% INITIALISATION xx,yy:= ({1|->2};{2|->4})(1), u
30		% END
31		%
32		% machine_identifiers(A,B,C,D,E,F,G).
33		% A = xx,
34		% B = [identifier(pos(4,1,1,12,1,12),'T'),identifier(pos(5,1,1,14,1,14),u)],
35		% C = [deferred_set(pos(11,1,3,6,3,6),'A'),enumerated_set(pos(12,1,3,9,3,20),'B',[identifier(pos(13,1,3,12,3,14),foo),identifier(pos(14,1,3,17,3,19),bar)])],
36		% D = [identifier(pos(22,1,6,20,6,21),xx)],
37		% E = [identifier(pos(24,1,7,20,7,21),yy)],
38		% F = [],
39		% G = [identifier(pos(16,1,4,20,4,21),cc)]
40		,get_machine_identifier_names/7 % a version returning atomic identifier names
41		,machine_has_constants/1 % check if machine has some constants
42		,get_machine_short_desc/2
43		,abstract_constant/2, concrete_constant/2
44		,possibly_abstract_constant/1
45		,machine_operations/2 % machine_operations(M, Ops) gets the names of the Operations defined in Machine M
46		,machine_operation_calls/2
47		,machine_hash/2 % stores a hash value for the machine
48		,properties_hash/2 % computes a hash over the constants and properties
49		,operation_hash/3 % computes a hash for the operation in a machine
50		,write_dot_hierarchy_to_file/1
51		,write_dot_op_hierarchy_to_file/1
52		,write_dot_event_hierarchy_to_file/1
53		,write_dot_variable_hierarchy_to_file/1
54		,get_machine_inclusion_graph/3
55		,get_machine_topological_order/1
56		,print_machine_topological_order/0
57		]).
58
59		:- use_module(library(lists)).
60		:- use_module(library(ordsets)).
61		:- use_module(bmachine,[b_get_definition/5, get_machine_file_number/4, b_get_relative_file_name_for_machine/2]).
62		:- use_module(bmachine_construction).
63		:- use_module(debug).
64		:- use_module(self_check).
65		:- use_module(specfile,[get_specification_description/2]).
66		:- use_module(extension('probhash/probhash'),[raw_sha_hash/2]).
67		:- use_module(input_syntax_tree).
68		:- use_module(dotsrc(dot_graph_generator), [gen_dot_graph/6, dot_no_same_rank/1,
69		use_new_dot_attr_pred/7, get_dot_cluster_name/2]).
70
71		:- use_module(value_persistance,[cache_is_activated/0]).
72		:- use_module(probsrc(tools),[split_list/4]).
73
74		:- use_module(module_information,[module_info/2]).
75		:- module_info(group,ast).
76		:- module_info(description,'This module provides functionality to visualize the dependencies of a B machine (include and sees relations, etc.).').
77
78		:- volatile
79		main_machine_name/1,
80		machine_type/2,
81		machine_package_directory/2,
82		machine_references/2,
83		machine_identifiers/7,
84		machine_operations/2,
85		machine_operation_calls/2,
86		machine_values_identifiers/2,
87		refines_event/4,
88		machine_has_assertions/1,
89		raw_machine/2,
90		machine_hash_cached/2,
91		properties_hash_cached/2, operation_hash_cached/3,
92		basic_operation_hash/4,
93		event_refinement_change/6.
94		:- dynamic
95		main_machine_name/1,
96		machine_type/2,
97		machine_package_directory/2,
98		machine_references/2,
99		machine_identifiers/7,
100		machine_operations/2,
101		machine_operation_calls/2,
102		machine_values_identifiers/2,
103		refines_event/4,
104		machine_has_assertions/1,
105		raw_machine/2,
106		machine_hash_cached/2,
107		properties_hash_cached/2, operation_hash_cached/3,
108		basic_operation_hash/4,
109		event_refinement_change/6.
110		:- volatile abstract_constant/2, concrete_constant/2.
111		:- dynamic abstract_constant/2.
112		:- dynamic concrete_constant/2.
113
114		:- use_module(specfile,[animation_minor_mode/1]).
115		possibly_abstract_constant(ID) :-
116		(abstract_constant(ID,_) ; animation_minor_mode(eventb),concrete_constant(ID,_) ).
117
118		reset_hierarchy :-
119		retract_all(main_machine_name/1),
120		retract_all(machine_type/2),
121		retract_all(machine_package_directory/2),
122		retract_all(machine_references/2),
123		retract_all(machine_identifiers/7),
124		retract_all(abstract_constant/2),
125		retract_all(concrete_constant/2),
126		retract_all(machine_operations/2),
127		retract_all(machine_operation_calls/2),
128		retract_all(machine_values_identifiers/2),
129		retract_all(refines_event/4),
130		retract_all(machine_has_assertions/1),
131		retract_all(machine_hash_cached/2),
132		retract_all(raw_machine/2),
133		retract_all(properties_hash_cached/2),
134		retract_all(operation_hash_cached/3),
135		retract_all(basic_operation_hash/4),
136		retract_all(event_refinement_change/6).
137
138		machine_name(Name) :- machine_type(Name,_).
139
140		:- use_module(eventhandling,[register_event_listener/3]).
141		:- register_event_listener(clear_specification,reset_hierarchy,
142		'Reset B Machine Hierarchy Facts.').
143
144		retract_all(Functor/Arity) :-
145		functor(Pattern,Functor,Arity),
146		retractall(Pattern).
147
148		analyse_hierarchy(Main,Machines) :- (var(Main) ; var(Machines)),!,
149		add_internal_error('Illegal call:',analyse_hierarchy(Main,Machines)).
150		analyse_hierarchy(Main,Machines) :-
151		reset_hierarchy,
152		assertz(main_machine_name(Main)),
153		analyse_machine(Main,Machines,main).
154
155		:- use_module(error_manager).
156		:- use_module(tools_strings,[ajoin/2]).
157		:- use_module(bmachine,[b_filenumber/4]).
158		:- public analyse_machine/3.
159		analyse_machine(Name,_Machines,_) :-
160		% machine already analysed
161		machine_type(Name,_),!.
162		analyse_machine(Name,Machines,_) :-
163		debug:debug_println(19,analysing_machine(Name)),
164		get_machine(Name,Machines,Type,Header,Refines,Body),
165		!,
166		( cache_is_activated -> % we need the machines stored for later analysis
167		assert_all_machines(Machines)
168		; true),
169		assertz(machine_type(Name,Type)),
170		(get_machine_parent_directory(Name,Dir) -> assertz(machine_package_directory(Name,Dir)) ; true),
171		( get_raw_section(assertions,Body,_) ->
172		assertz(machine_has_assertions(Name))
173		; true),
174		store_identifiers(Name,Header,Body),
175		store_operations(Name,Body),
176		store_values(Name,Body),
177		store_references(Name,Refines,Body,Machines).
178		analyse_machine(Name,Machines,RefType) :-
179		get_machine_file_number(Name,_Ext,Nr,File),
180		get_ref_type_name(RefType,Clause),
181		!,
182		( member(M,Machines),get_constructed_machine_name_and_filenumber(M,OtherName,Nr)
183		-> ajoin(['Cannot use B machine "',Name,'" within ', Clause,
184		' clause. Rename machine "', OtherName,'" to "', Name, '" in file: '],Msg)
185		; findall(ModuleName,b_filenumber(ModuleName,_,_,_),List),
186		ajoin(['Cannot find B machine "',Name,'" within ', Clause,
187		' clause (available: ',List,'). Check that machine name matches filename in: '],Msg)
188		),
189		add_error_fail(invalid_machine_reference,Msg,File).
190		analyse_machine(Name,_Machines,_RefType) :-
191		bmachine:portray_filenumbers,
192		add_error_fail(invalid_machine_reference,
193		'Could not find machine in parsed machine list (check that your machine names match your filenames): ',Name).
194
195		:- use_module(tools,[get_parent_directory_name/2]).
196		get_machine_parent_directory(Name,DirName) :-
197		% try and get parent directory name; useful to distinguish different packages when using package pragma
198		get_machine_file_number(Name,_Ext,_Nr,File),
199		get_parent_directory_name(File,DirName).
200
201
202		% store the un-typed input syntax tree for later analysis
203		assert_all_machines(Machines) :-
204		(raw_machine(_,_)
205		-> true % machines already asserted
206		; maplist(assert_raw_machine,Machines)).
207		assert_raw_machine(Machine) :-
208		get_raw_machine_name(Machine,Name),
209		(raw_machine(Name,_) -> add_warning(b_machine_hierarchy,'Raw machine already exists: ',Name) ; true),
210		assertz( raw_machine(Name,Machine) ).
211
212		machine_has_constants(MachName) :-
213		machine_identifiers(MachName,_,_,_,_,AConsts,CConsts),
214		(AConsts=[] -> CConsts = [_|_] ; true).
215
216		get_machine_short_desc(MachName,Text) :-
217		machine_identifiers(MachName,Params,Sets,AVars,CVars,AConsts,CConsts),
218		length(Params,PL), length(Sets,SL), length(AVars,AVL), length(CVars,CVL), VL is AVL+CVL,
219		length(AConsts,ACL), length(CConsts,CCL), CL is ACL+CCL,
220		(machine_operations(MachName,Ops), length(Ops,OL) -> true ; OL=0),
221		ajoin(['SETS:',SL,' CONSTANTS:',CL,' VARIABLES:',VL, ' PARAMETERS:',PL, ' OPERATIONS:',OL],Text).
222
223		store_identifiers(Name,Header,Body) :-
224		get_parameters(Header,Params),
225		get_sets(Body,Sets),
226		get_identifiers([abstract_variables,variables],Body,AVars),
227		get_identifiers([concrete_variables],Body,CVars),
228		get_identifiers([abstract_constants],Body,AConsts),
229		get_identifiers([concrete_constants,constants],Body,CConsts), % fixed abstract -> concrete
230		assertz(machine_identifiers(Name,Params,Sets,AVars,CVars,AConsts,CConsts)),
231		maplist(assert_raw_id_with_position(abstract_constant),AConsts),
232		maplist(assert_raw_id_with_position(concrete_constant),CConsts).
233
234
235		raw_id_is_identifier2(description(_Pos,_Desc,Raw),ID) :- !, raw_id_is_identifier2(Raw,ID).
236		raw_id_is_identifier2(deferred_set(_,ID),ID) :- !.
237		raw_id_is_identifier2(enumerated_set(_,ID,_Elements),ID) :- !.
238		raw_id_is_identifier2(Raw,ID) :- raw_id_is_identifier(Raw,_,ID).
239
240		get_machine_identifier_names(Name,Params,Sets,AVars,CVars,AConsts,CConsts) :-
241		machine_identifiers(Name,RawParams,RawSets,RawAVars,RawCVars,RawAConsts,RawCConsts),
242		(maplist(raw_id_is_identifier2,RawParams,Params),
243		maplist(raw_id_is_identifier2,RawSets,Sets),
244		maplist(raw_id_is_identifier2,RawAVars,AVars),
245		maplist(raw_id_is_identifier2,RawCVars,CVars),
246		maplist(raw_id_is_identifier2,RawAConsts,AConsts),
247		maplist(raw_id_is_identifier2,RawCConsts,CConsts) -> true
248		; add_internal_error('Could not extract raw identifiers:',Name)).
249
250
251		machine_hash(Name,Hash) :-
252		machine_hash_cached(Name,Hash1),!,Hash=Hash1.
253		machine_hash(Name,Hash) :-
254		compute_machine_hash(Name,Hash1),
255		assertz( machine_hash_cached(Name,Hash1) ),
256		Hash=Hash1.
257		compute_machine_hash(Name,Digest) :-
258		if(raw_machine(Name,Machine),
259		raw_sha_hash(Machine,Digest),
260		add_error_and_fail(compute_machine_hash,'Machine does not exist or has not been processed:',Name)
261		).
262
263		:- use_module(pathes_extensions_db, [compile_time_unavailable_extension/2]).
264		:- if(\+ compile_time_unavailable_extension(probhash_extension, _)).
265		store_eventb_hash(Name,ContextMachTerm) :-
266		raw_sha_hash(ContextMachTerm,Digest),
267		assertz(machine_hash_cached(Name,Digest)).
268		:- else.
269		store_eventb_hash(Name,_) :-
270		assertz( (machine_hash_cached(Name,_) :-
271		add_error(b_machine_hierarchy,'prob_hash_extension not available for: ',Name),fail) ).
272		:- endif.
273
274		:- use_module(tools_strings,[get_hex_bytes/2]).
275		operation_hash(MachName,OpName,Hash) :-
276		operation_hash_cached(MachName,OpName,Hash1),!,Hash=Hash1.
277		operation_hash(MachName,OpName,Hash) :-
278		computed_basic_operation_hashes,
279		basic_operation_hash(OpName,MachName,Hash1,OpCalls),
280		(OpCalls = []
281		-> FinalHash=Hash1 % no recursive call of other operations
282		; maplist(get_basic_op_hash,OpCalls,OpDigests),
283		raw_sha_hash(op(Hash1,OpDigests),FinalHash) % also include hash of called operations
284		),
285		assertz( operation_hash_cached(MachName,OpName,FinalHash) ),
286		get_hex_bytes(FinalHash,Hex),
287		debug_format(19,'value caching: operation ~w in machine ~w has hash: ~s~n',[OpName,MachName,Hex]),
288		Hash=FinalHash.
289
290		get_basic_op_hash(OpName,Digest) :-
291		basic_operation_hash(OpName,_MachName,Digest,_OpCalls).
292
293		% compute basic hash, without taking recursive operation calls into account
294		computed_basic_operation_hashes :-
295		basic_operation_hash(_,_,_,_),!. % already computed
296		computed_basic_operation_hashes :-
297		get_raw_machine_operation_hash(MachName,OpName,Digest,OpCalls),
298		(basic_operation_hash(OpName,_,_,_)
299		-> add_warning(computed_basic_operation_hashes,'Multiple hashes for operation: ',OpName)
300		; true),
301		assertz(basic_operation_hash(OpName,MachName,Digest,OpCalls)),
302		get_hex_bytes(Digest,Hex),
303		debug_format(19,'value caching: basic operation hash ~w in machine ~w: ~s (calls ~w)~n',
304		[OpName,MachName,Hex,OpCalls]),
305		fail.
306		computed_basic_operation_hashes.
307
308		% first computed basic, independent operation hashes:
309		% only look up used definitions, but not yet called operations
310		get_raw_machine_operation_hash(MachName,OpName,Digest,SOpCalls) :-
311		raw_machine(MachName,Machine),
312		get_machine(MachName,[Machine],_Type,_Header,_Refines,MachBody),
313		get_opt_section(operations,MachBody,Operations),
314		Op = operation(_,identifier(_,OpName),_,_,_),
315		member(Op,Operations),
316		get_raw_operation_id_and_body(Op,identifier(_,OpName),OpBody),
317		extract_used_np_definitions(Op,MachBody,UsedDefinitions,DefsWithPos),
318		remove_raw_position_info(Op,RawOperation),
319		raw_sha_hash(op(RawOperation,UsedDefinitions),Digest),
320		findall(Id, (get_raw_operation_call_id(OpBody,Id) % extract op calls in body of operation
321		; get_def_body(Def,DefsWithPos), get_raw_operation_call_id(Def,Id) % extract op calls in definitions
322		),
323		OpCalls),
324		sort(OpCalls,SOpCalls).
325
326		get_def_body(Body,Defs) :- member(definition(_,_DefName,_,Body),Defs).
327
328
329		:- use_module(debug,[debug_println/2]).
330		assert_raw_id_with_position(PredFunctor,Rid) :-
331		(raw_id_is_identifier(Rid,Pos,ID)
332		-> true
333		; peel_desc(Rid,PRid), PRid = definition(Pos,ID,_)
334		-> add_error(illegal_definition_use,'Definition cannot be used as identifier here: ',ID,Pos)
335		; add_error_fail(assert_raw_id_with_position,'Not identifier: ',Rid)
336		),
337		Fact =.. [PredFunctor,ID,Pos],
338		assertz(Fact), debug_println(9,Fact).
339
340		raw_id_is_identifier(identifier(Pos,ID),Pos,ID).
341		raw_id_is_identifier(unit(_,_,identifier(Pos,ID)),Pos,ID).
342		raw_id_is_identifier(new_unit(_,_,identifier(Pos,ID)),Pos,ID).
343		raw_id_is_identifier(inferred_unit(_,_,identifier(Pos,ID)),Pos,ID).
344		raw_id_is_identifier(inferredunit(_,_,identifier(Pos,ID)),Pos,ID). % the (new?) parser seems to generate the wrong pragma in the .prob file; TO DO: investigate
345		raw_id_is_identifier(description(_,_,RawID),Pos,ID) :-
346		raw_id_is_identifier(RawID,Pos,ID).
347
348		peel_desc(description(_,_,E),R) :- !, peel_desc(E,R).
349		peel_desc(R,R).
350
351		get_raw_identifier(Raw,Res) :- raw_id_is_identifier(Raw,_Pos,Id),!, Res=Id.
352		get_raw_identifier(definition(_Pos,DID,[]),ID) :- % see also expand_definition_to_variable_list
353		atom(DID),!,
354		ajoin([DID,'(DEFINITION)'],ID).
355		get_raw_identifier(deferred_set(_Pos,DID),ID) :- atom(DID),!, ID=DID.
356		get_raw_identifier(enumerated_set(_Pos,DID,_List),ID) :- atom(DID),!, ID=DID.
357		get_raw_identifier(description(_,_,RawID),ID) :- !,
358		get_raw_identifier(RawID,ID).
359		get_raw_identifier(Raw,Res) :- add_internal_error('Cannot get identifier:',Raw),Res='???'.
360
361		raw_identifier_member(ID,List) :- member(Raw,List), raw_id_is_identifier(Raw,_Pos,ID).
362
363		store_operations(MachName,Body) :-
364		get_opt_section(operations,Body,Operations),
365		findall(I,(member(Op,Operations),get_raw_operation_id_and_body(Op,I,_)),Ids),
366		assertz(machine_operations(MachName,Ids)),
367		findall(calls(I1,I2),(member(Op,Operations),get_raw_operation_call(Op,I1,I2)),Calls),
368		sort(Calls,SCalls),
369		debug_println(9,machine_operation_calls(MachName,SCalls)),
370		assertz(machine_operation_calls(MachName,SCalls)).
371
372		get_raw_operation_id_and_body(operation(_Pos,Id,_,_,Body),Id,Body).
373		get_raw_operation_id_and_body(refined_operation(_Pos,Id,_Results,_Args,_RefinesID,Body),Id,Body).
374		get_raw_operation_id_and_body(description_operation(_Pos,_,Op),Id,Body) :- get_raw_operation_id_and_body(Op,Id,Body).
375
376		% get operations called in body
377		get_raw_operation_call(Op,Id,CallsId) :-
378		get_raw_operation_id_and_body(Op,identifier(_,Id),Body),
379		get_raw_operation_call(Body,identifier(_,CallsId)).
380
381		:- use_module(debug,[debug_format/3]).
382		get_raw_operation_call(block(_,Body),ID) :- !, get_raw_operation_call(Body,ID).
383		get_raw_operation_call(precondition(_,_,Body),ID) :- !, get_raw_operation_call(Body,ID).
384		get_raw_operation_call(assertion(_,_,Body),ID) :- !, get_raw_operation_call(Body,ID).
385		get_raw_operation_call(witness_then(_,_,Body),ID) :- !, get_raw_operation_call(Body,ID).
386		get_raw_operation_call(var(_,_,Body),ID) :- !, get_raw_operation_call(Body,ID).
387		get_raw_operation_call(select_when(_,_,Body),ID) :- !, get_raw_operation_call(Body,ID).
388		get_raw_operation_call(if_elsif(_,_,Body),ID) :- !, get_raw_operation_call(Body,ID).
389		get_raw_operation_call(let(_,_,_,Body),ID) :- !, get_raw_operation_call(Body,ID).
390		get_raw_operation_call(any(_,_,_,Body),ID) :- !, get_raw_operation_call(Body,ID).
391		get_raw_operation_call(case(_,_,_,_,_,Body),ID) :- !, get_raw_operation_call(Body,ID).
392		get_raw_operation_call(while(_,_Cond,Body,_,_),ID) :- !, get_raw_operation_call(Body,ID).
393		get_raw_operation_call(parallel(_,List),ID) :- !,member(A,List), get_raw_operation_call(A,ID).
394		get_raw_operation_call(sequence(_,List),ID) :- !,member(A,List), get_raw_operation_call(A,ID).
395		get_raw_operation_call(if(_,_Test,Then,List,Else),ID) :- !,member(A,[Then,Else|List]), get_raw_operation_call(A,ID).
396		get_raw_operation_call(select(_,_Cond,Body,List),ID) :- !,member(A,[Body|List]), get_raw_operation_call(A,ID).
397		get_raw_operation_call(select(_,_Cond,Body,List,Else),ID) :- !,member(A,[Body,Else|List]), get_raw_operation_call(A,ID).
398		get_raw_operation_call(choice(_,List),ID) :- !,member(A,List), get_raw_operation_call(A,ID).
399		get_raw_operation_call(choice_or(_,Body),ID) :- !, get_raw_operation_call(Body,ID).
400		get_raw_operation_call(operation_call(_,ID,_,_),ID) :- !.
401		get_raw_operation_call(skip(_),_) :- !, fail.
402		get_raw_operation_call(assign(_,_,_),_) :- !, fail.
403		get_raw_operation_call(becomes_element_of(_,_,_),_) :- !, fail.
404		get_raw_operation_call(becomes_such(_,_,_),_) :- !, fail.
405		get_raw_operation_call(definition(_,Name,_),_) :- !, % TO DO: improve
406		debug_format(19,'Ignoring operation calls in DEFINITION ~w for operation call diagram~n',[Name]),
407		% b_get_definition(Name,_DefType,_Args,DefBody,_Deps), not yet precompiled !
408		fail.
409		get_raw_operation_call(Subst,_) :- functor(Subst,F,N),print(uncovered_subst(F,N,Subst)),nl,fail.
410		% we also do not find operation calls in expressions
411
412		:- use_module(input_syntax_tree,[raw_operator_term/1, raw_literal_term/1, raw_special_set_term/1]).
413		% avoid spurious uncovered_subst messages in a context where we are not sure we have a subst
414		try_get_raw_operation_call(Term,_) :- raw_literal_term(Term),!, fail.
415		try_get_raw_operation_call(Term,_) :- raw_operator_term(Term),!, fail.
416		try_get_raw_operation_call(Term,_) :- raw_special_set_term(Term),!, fail.
417		try_get_raw_operation_call(Term,_) :- functor(Term,F,_), definitely_not_subst(F),!, fail.
418		try_get_raw_operation_call(Body,ID) :- get_raw_operation_call(Body,ID).
419
420		% definitely expression:
421		definitely_not_subst(let_expression).
422		definitely_not_subst(let_predicate).
423		% definitely predicate:
424		definitely_not_subst(external_function_call).
425		definitely_not_subst(external_pred_call).
426
427		get_raw_operation_call_id(OpBody,CalledId) :-
428		try_get_raw_operation_call(OpBody,identifier(_,CalledId)).
429
430		store_references(Name,Refines,Body,Machines) :-
431		get_refinements(Refines,Refs1),
432		get_references(Body,Refs2),
433		append(Refs1,Refs2,Refs),
434		assertz(machine_references(Name,Refs)),
435		follow_refs(Refs,Machines).
436
437		get_references(Body,Refs) :-
438		findrefs(Body,includes,Includes),
439		findrefs(Body,extends,Extends),
440		findrefs(Body,imports,Imports),
441		findusessees(Body,uses,Uses),
442		findusessees(Body,sees,Sees),
443		append([Includes,Imports,Extends,Uses,Sees],Refs).
444
445		get_refinements([],[]).
446		get_refinements([Name|NRest],[ref(refines,Name,'')|RRest]) :-
447		get_refinements(NRest,RRest).
448
449		findrefs(Body,Type,Refs) :-
450		get_opt_section(Type,Body,RawRefs),
451		findrefs2(RawRefs,Type,Refs).
452		findrefs2([],_Type,[]).
453		findrefs2([MID|MRest],Type,[ref(Type,Name,Prefix)|RRest]) :-
454		get_machine_id(MID,FullName), % should be machine_reference
455		bmachine_construction:split_prefix(FullName,Prefix,Name),
456		findrefs2(MRest,Type,RRest).
457
458		findusessees(Body,Type,Refs) :-
459		get_opt_section(Type,Body,RawRefs),
460		findusessees2(RawRefs,Type,Refs).
461		findusessees2([],_Type,[]).
462		findusessees2([MID|MRest],Type,[ref(Type,Name,Prefix)|RRest]) :-
463		get_machine_id(MID,FullName), % should be machine_reference
464		% USE and SEES do not have machine_reference in AST but identifier
465		bmachine_construction:split_prefix(FullName,Prefix,Name),
466		findusessees2(MRest,Type,RRest).
467
468		get_machine_id(identifier(_Pos,FN),FullName) :- !, FullName=FN.
469		get_machine_id(machine_reference(_Pos,FN,_Params),FullName) :- !, FullName=FN.
470		get_machine_id(Other,_) :- add_internal_error('Illegal machine id: ',get_machine_id(Other,_)),fail.
471
472
473		follow_refs([],_Machines).
474		follow_refs([ref(RefType,Name,_Prefix)|Rest],Machines) :-
475		analyse_machine(Name,Machines,RefType),
476		follow_refs(Rest,Machines).
477
478		get_parameters(machine_header(_Pos,_Name,Params),Params).
479
480		get_sets(Body,Sets) :-
481		get_opt_section(sets,Body,Sets).
482
483		get_identifiers([],_Body,[]).
484		get_identifiers([Sec|Rest],Body,Ids) :-
485		get_opt_section(Sec,Body,Ids1),
486		append(Ids1,IRest,Ids),
487		get_identifiers(Rest,Body,IRest).
488
489		get_opt_sections([],_Body,[]).
490		get_opt_sections([S|Srest],Body,Contents) :-
491		get_opt_section(S,Body,L),append(L,Rest,Contents),
492		get_opt_sections(Srest,Body,Rest).
493
494		get_opt_section(Sec,Body,Result) :-
495		( get_raw_section(Sec,Body,Content) -> Result=Content; Result=[]).
496		get_raw_section(Sec,Body,Content) :- % look for Sec(_Pos,Content) in Body list
497		functor(Pattern,Sec,2),arg(2,Pattern,Content),
498		memberchk(Pattern,Body).
499
500		get_machine(Name,Machines,Type,Header,Refines,Body) :-
501		get_machine1(Name,Machines,_Machine,Type,Header,Refines,Body).
502		%get_raw_machine(Name,Machines,Machine) :-
503		% get_machine1(Name,Machines,Machine,_Type,_Header,_Refines,_Body).
504		get_machine1(Name,Machines,Machine,Type,Header,Refines,Body) :-
505		Header = machine_header(_Pos,Name,_Params),
506		member(Machine,Machines),
507		get_machine2(Machine,Type,Header,Refines,Body),!.
508		get_machine2(abstract_machine(_Pos,MS,Header,Body),TypeOfAbstractMachine,RHeader,Refines,RBody) :- !,
509		Refines = [], RBody = Body, RHeader=Header,
510		get_abstract_machine_type(MS,TypeOfAbstractMachine).
511		get_machine2(refinement_machine(_Pos,Header,Refines,Body),refinement,RHeader,RRefines,RBody) :- !,
512		RRefines = [Refines], RBody = Body, RHeader=Header.
513		get_machine2(implementation_machine(_Pos,Header,Refines,Body),implementation,RHeader,RRefines,RBody) :- !,
514		RRefines = [Refines], RBody = Body, RHeader=Header.
515		get_machine2(generated(_Pos,Machine),A,B,C,D) :- !, % @generated Pragma used at top of file
516		get_machine2(Machine,A,B,C,D).
517		get_machine2(unit_alias(_Pos,_Name,_Alias,Machine),A,B,C,D) :- !,
518		get_machine2(Machine,A,B,C,D).
519		get_machine2(Other,A,B,C,D) :-
520		add_internal_error('Illegal machine:',get_machine2(Other,A,B,C,D)), fail.
521
522		get_raw_machine_name(Machine,Name) :-
523		get_machine2(Machine,_,machine_header(_,Name,_),_,_).
524
525		get_abstract_machine_type(machine(_Pos2),R) :- !,R=abstract_machine.
526		get_abstract_machine_type(system(_Pos2),R) :- !,R=abstract_machine.
527		get_abstract_machine_type(model(_Pos2),R) :- !,R=abstract_model.
528		get_abstract_machine_type(X,R) :- atomic(X),!,
529		add_error(get_abstract_machine_type,'Your parser seems out-dated. Assuming abstract_machine: ',X),
530		R=abstract_machine.
531
532
533		get_values_id(values_entry(Pos,ID,_Val),identifier(Pos,ID)).
534		% Store the identifiers assigned to in VALUES clauses
535		store_values(Name,Body) :-
536		get_opt_section('values',Body,Values),!,
537		maplist(get_values_id,Values,ValuesIDs),
538		assertz(machine_values_identifiers(Name,ValuesIDs)).
539		store_values(_,_).
540
541		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
542
543		% write dot operation call graph
544		write_dot_op_hierarchy_to_file(File) :-
545		(get_preference(dot_event_hierarchy_horizontal,true) -> PageOpts=[rankdir/'LR'] ; PageOpts=[]),
546		gen_dot_graph(File,PageOpts,dot_operation_node,dot_op_calls_op,dot_no_same_rank,dot_subgraph(op_hierarchy)).
547
548
549		:- use_module(bmachine,[b_top_level_operation/1, b_top_level_feasible_operation/1]).
550		dot_operation_node(OpName,M,Desc,Shape,Style,Color) :-
551		machine_operations(M,Operations),
552		(machine_promotes_operations(M,Promotes) -> true ; Promotes=[]),
553		raw_identifier_member(OpName,Operations),
554		(b_top_level_feasible_operation(OpName) -> Color=lightgray
555		; b_top_level_operation(OpName) -> Color='OldLace' % commented out operation
556		; raw_identifier_member(OpName,Promotes) -> Color='gray98' % promoted but not to top_level
557		; Color=white),
558		Desc=OpName, Shape=box, Style=filled.
559
560		dot_op_calls_op(Op1,Label,Op2,Color,Style) :- Style=solid, Color=steelblue,
561		Label = '', % TO DO: different colors for local operation calls, detect op calls in expressions?
562		machine_operation_calls(_,Operations),
563		member(calls(Op1,Op2),Operations).
564
565
566
567		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
568		% print hierarchy to dot file
569
570		maxlinelength(30).
571
572		:- use_module(tools_io).
573
574		% write hierarchy of machines, with inclusion/refinement links
575		write_dot_hierarchy_to_file(Filename) :-
576		findall(M,machine_type(M,_),Machines),
577		safe_open_file(Filename,write,S,[]),
578		( print_header(S),
579		print_machines(S,1,Machines,Ids),
580		print_refs_for_dot(S,Ids,Ids),
581		print_footer(S)
582		-> true
583		; add_internal_error('Command failed:',write_dot_hierarchy_to_file(Filename))
584		),
585		close(S).
586
587		print_header(S) :-
588		write(S,'digraph module_hierarchy {\n'),
589		write(S,' graph [page="8.5, 11",ratio=fill,size="7.5,10"];\n').
590		print_footer(S) :-
591		write(S,'}\n').
592
593		print_machines(_S,_Nr,[],[]).
594		print_machines(S,Nr,[M|Machines],[id(M,Nr)|Ids]) :-
595		(print_machine(S,Nr,M) -> true
596		; add_internal_error('Printing machine for hierarchy failed: ',print_machine(S,Nr,M))
597		),
598		Nr2 is Nr + 1,
599		print_machines(S,Nr2,Machines,Ids).
600		print_machine(S,Nr,M) :-
601		write(S,' '),write(S,Nr),
602		(main_machine_name(M) ->
603		write(S,' [shape=record, style=bold, color=darkgreen, label=\"|{')
604		; write(S,' [shape=record, color=steelblue, label=\"|{')),
605		print_machine_header(S,M),
606		machine_identifiers(M,_Params,Sets,AVars,CVars,AConsts,CConsts),
607		%print_hash(S,M),
608		print_sets(S,Sets),
609		print_identifiers(S,'VARIABLES',AVars),
610		print_identifiers(S,'CONCRETE VARIABLES',CVars),
611		print_identifiers(S,'ABSTRACT CONSTANTS',AConsts),
612		print_identifiers(S,'CONSTANTS',CConsts),
613		(machine_values_identifiers(M,VConsts)
614		-> print_identifiers(S,'VALUES',VConsts)
615		; true),
616		( machine_has_assertions(M) ->
617		get_specification_description(assertions,AssStr),
618		print_title(S,AssStr)
619		; true
620		),
621		(machine_promotes_operations(M,Promotes)
622		-> print_identifiers(S,'PROMOTES',Promotes) ; true),
623		machine_operations(M,Operations),
624		delete(Operations,identifier(_,'INITIALISATION'),Operations2),
625		exclude(is_refinining_event(M),Operations2,RefiningOperations),
626		include(is_refinining_event(M),Operations2,NewOperations),
627		((RefiningOperations=[] ; NewOperations=[])
628		-> get_specification_description(operations,OpStr),
629		print_identifiers(S,OpStr,Operations2)
630		; print_identifiers(S,'EVENTS (refining)',RefiningOperations),
631		print_identifiers(S,'EVENTS (new)',NewOperations)
632		),
633
634		write(S,'}|\"];\n').
635
636		is_refinining_event(M,identifier(_,Event)) :- (refines_event(M,Event,_,_) -> true).
637
638		%print_hash(S,M) :- machine_hash(M,Digest),!,print_title(S,'Digest'),
639		% maplist(format(S,'~16r'),Digest),write(S,'\\n').
640		%print_hash(_S,_M).
641
642		%get_machine_colour(M,steelblue) :- main_machine_name(M),!.
643		%get_machine_colour(_M,steelblue).
644
645		print_machine_header(S,M) :-
646		machine_type(M,Type),
647		get_machine_type_keyw(Type,P),
648		write(S,P),write(S,' '),
649		write(S,M),
650		(machine_package_directory(M,Dir), machine_package_directory(_M2,D2), D2 \= Dir
651		-> format(S,' (~w)',[Dir]) % show the name of the directory; probably the package pragma was used
652		; true),
653		write(S,'\\n').
654		get_machine_type_keyw(abstract_machine,'MACHINE').
655		get_machine_type_keyw(abstract_model,'MODEL').
656		get_machine_type_keyw(refinement,'REFINEMENT').
657		get_machine_type_keyw(implementation,'IMPLEMENTATION').
658		get_machine_type_keyw(context,'CONTEXT').
659
660		print_sets(_,[]) :- !.
661		print_sets(S,Sets) :-
662		write(S,'|SETS\\n'),
663		print_sets2(Sets,S).
664		print_sets2([],_).
665		print_sets2([Set|Rest],S) :-
666		print_set(Set,S),
667		write(S,'\\n'),
668		print_sets2(Rest,S).
669		print_set(description(_Pos,_Desc,Raw),S) :- print_set(Raw,S).
670		print_set(deferred_set(_Pos,Name),S) :-
671		write_id(S,Name).
672		print_set(enumerated_set(_Pos,Name,List),S) :-
673		write_id(S,Name),write(S,' = \\{'),
674		maxlinelength(Max),
675		preferences:get_preference(dot_hierarchy_max_ids,MaxIdsToPrint),
676		print_set_elements(List,S,Max,MaxIdsToPrint),
677		write(S,'\\}').
678		print_set_elements([],_,_,_).
679		print_set_elements([RawID],S,_LenSoFar,_) :-
680		raw_id_is_identifier(RawID,_,Name),
681		!,write_id(S,Name).
682		print_set_elements([RawID,B|Rest],S,LenSoFar,MaxIdsToPrint) :-
683		raw_id_is_identifier(RawID,_,Name),
684		dec_atom_length(LenSoFar,Name,NewLen),
685		(NewLen<0 -> maxlinelength(NL0),NL is NL0-1,write(S,'\\n ') ; NL is NewLen-1),
686		write_id(S,Name),write(S,','),
687		M1 is MaxIdsToPrint-1,
688		(M1 < 1, Rest \= []
689		-> write(S,'...,'),
690		last([B|Rest],Last), print_set_elements([Last],S,NL,M1)
691		; print_set_elements([B|Rest],S,NL,M1)
692		).
693
694		:- use_module(tools,[string_escape/2]).
695		% write identifier and escape it for dot
696		write_id(S,Name) :- string_escape(Name,EName), write(S,EName).
697
698		dec_atom_length(Prev,Atom,New) :- atom_length(Atom,Len),
699		New is Prev-Len.
700
701		print_title(S,Title) :-
702		write(S,'|'),
703		write(S,Title),write(S,'\\n').
704		print_identifiers(_S,_,[]) :- !.
705		print_identifiers(S,Title,List) :-
706		print_title(S,Title),
707		preferences:get_preference(dot_hierarchy_max_ids,MaxIdsToPrint), % how many do we print overall; -1 means print all of them
708		print_identifiers2(List,0,_,S,MaxIdsToPrint).
709		print_identifiers2([],Count,Count,_,_MaxIdsToPrint).
710		print_identifiers2([RawID|Rest],Count,NCount,S,MaxIdsToPrint) :-
711		get_raw_identifier(RawID,Name),
712		(MaxIdsToPrint = 0,Rest\=[]
713		-> length(Rest,Len), RN is Len+1,
714		format(S,' (~w more)',[RN])
715		; MaxIdsToPrint1 is MaxIdsToPrint-1,
716		print_identifier(Name,Count,ICount,S),
717		(Rest = [] -> true; write(S,',')),
718		print_identifiers2(Rest,ICount,NCount,S,MaxIdsToPrint1)
719		).
720		print_identifier(Name,Count,NewCount,S) :-
721		atom_codes(Name,Codes),
722		length(Codes,Length),
723		NewCount1 is Count+Length,
724		maxlinelength(Max),
725		( Count == 0 -> NewCount1=NewCount
726		; NewCount1 =< Max -> NewCount1=NewCount
727		; NewCount=0,write(S,'\\n')),
728		write_id(S,Name).
729
730		% print machine inclusion references for dot graph
731		print_refs_for_dot(_S,[],_).
732		print_refs_for_dot(S,[id(M,Nr)|Rest],Ids) :-
733		machine_references(M,Refs),
734		filter_redundant_refs(Refs,Refs,UsefulRefs),
735		sort(UsefulRefs,SUsefulRefs),
736		print_refs2(SUsefulRefs,M,Nr,Ids,S),
737		print_refs_for_dot(S,Rest,Ids).
738		print_refs2([],_,_,_,_).
739		print_refs2([ref(Type,Dest,Prefix)|Rest],M,Nr,Ids,S) :-
740		member(id(Dest,DestNr),Ids),!,
741		(get_preference(dot_hierarchy_group_includes,true)
742		-> get_same_dest(Rest,Type,Dest,OtherPrefixes,Rest2)
743		; OtherPrefixes=[], Rest2=Rest
744		), length(OtherPrefixes,Len),
745		get_ref_type_name(Type,RefName),
746		(Prefix='' -> Label=RefName
747		; OtherPrefixes=[Prefix2] -> ajoin([RefName,' (',Prefix,',',Prefix2,')'],Label)
748		; Len>1 -> ajoin([RefName,' (',Prefix,',...',Len,' more)',Len],Label)
749		; ajoin([RefName,' (',Prefix,')'],Label)
750		),
751		get_ref_type(Type,Col,Style,Dir), !, % TO DO: add prefix info
752		(Dir=reverse -> From=DestNr, To=Nr ; To=DestNr, From=Nr),
753		(Len>0, L1 is Len+1
754		-> format(S,' ~w -> ~w [label=\"~w\",color=~w,style=\"~w\",penwidth=~w];~n',[From,To,Label,Col,Style,L1])
755		; format(S,' ~w -> ~w [label=\"~w\",color=~w,style=\"~w\"];~n',[From,To,Label,Col,Style])
756		),
757		print_refs2(Rest2,M,Nr,Ids,S).
758		get_ref_type(includes,navyblue,'',normal).
759		get_ref_type(imports,navyblue,'',normal).
760		get_ref_type(extends,navyblue,'',normal).
761		get_ref_type(uses,navyblue,dashed,normal).
762		get_ref_type(sees,navyblue,dashed,normal).
763		get_ref_type(refines,navyblue,bold,reverse). % reverse so that abstract machines are shown on top
764		get_ref_type(UNKNOWN,red,bold,normal) :-
765		add_internal_error('Unknown : ',get_ref_type(UNKNOWN,_,_,_)).
766
767		% get references to same machine with same inclusion type, with different prefix
768		get_same_dest([ref(Type,Dest,Prefix)|T],Type,Dest,[Prefix|PT],Rest) :- !, get_same_dest(T,Type,Dest,PT,Rest).
769		get_same_dest(Rest,_,_,[],Rest).
770
771		get_ref_type_name(includes,'INCLUDES').
772		get_ref_type_name(imports,'IMPORTS').
773		get_ref_type_name(extends,'EXTENDS').
774		get_ref_type_name(uses,'USES').
775		get_ref_type_name(sees,'SEES').
776		get_ref_type_name(refines,'REFINEMENT').
777		get_ref_type_name(main,'MACHINE').
778		get_ref_type_name(UNKNOWN,UNKNOWN).
779
780
781		% remove redundant references (has to be done after analyse_eventb_machine has asserted all facts)
782		filter_redundant_refs([],_,[]).
783		filter_redundant_refs([ref(sees,Dest,_)|T],All,R) :-
784		machine_type(Dest,context),
785		member(ref(sees,Other,_),All),
786		machine_references(Other,Refs),
787		member(ref(extends,Dest,_),Refs), % Dest already seen by other seen context;
788		% Note: Rodin export contains transitive sees relation;
789		% if the user had included Dest in the sees clause we would have a warning "Redundant seen context"
790		!,
791		%format(user_output,'Redundant sees of ~w (~w)~n',[Dest,Other]),
792		filter_redundant_refs(T,All,R).
793		filter_redundant_refs([H|T],All,[H|R]) :-
794		filter_redundant_refs(T,All,R).
795
796		/************************************************************************/
797		/* The same for Event-B */
798		/************************************************************************/
799
800		analyse_eventb_hierarchy(Machines,Contextes) :-
801		reset_hierarchy,
802		get_eventb_name(Machines,Contextes,MainName),
803		assertz(main_machine_name(MainName)),
804		maplist(analyse_eventb_machine,Machines),
805		analyse_eventb_refinement_types(Machines),
806		maplist(analyse_eventb_context,Contextes),!.
807		analyse_eventb_hierarchy(Machines,Contextes) :-
808		add_internal_error('Analyzing Event-B Hierarchy Failed: ',analyse_eventb_hierarchy(Machines,Contextes)).
809
810		get_eventb_name([MainMachine|_AbstractMachines],_Contextes,Name) :-
811		event_b_model(MainMachine,Name,_),!.
812		get_eventb_name(_Machines,[MainContext|_AbstractContextes],Name) :-
813		event_b_context(MainContext,Name,_).
814
815		event_b_model(event_b_model(_,Name,Sections),Name,Sections).
816		event_b_context(event_b_context(_,Name,Sections),Name,Sections).
817
818		analyse_eventb_machine(Machine) :-
819		event_b_model(Machine,Name,Sections),
820		% print(analyzing(Name)),nl,
821		( memberchk(refines(_,RName),Sections) -> Type=refinement, RRefs=[ref(refines,RName,'')]
822		; Type=abstract_model, RRefs=[], RName='$none'),
823		get_identifiers([variables],Sections,Vars),
824		get_sees_context_refs(Sections,SRefs),
825		append(RRefs,SRefs,Refs),
826		get_events(Name,Sections,Events,RName),
827		store_eventb_hash(Name,Machine),
828		assertz(machine_type(Name,Type)),
829		assertz(machine_identifiers(Name,[],[],Vars,[],[],[])),
830		assertz(machine_references(Name,Refs)),
831		assertz(machine_operations(Name,Events)),
832		assertz(machine_operation_calls(Name,[])), % Event-B events cannot call other events
833		assert_if_has_theorems(Name,Sections).
834
835
836		% analyze which kinds of refinments we have between events
837		analyse_eventb_refinement_types([]).
838		analyse_eventb_refinement_types([RefMachine,AbsMachine|_]) :-
839		event_b_model(RefMachine,RefName,RefSections),
840		memberchk(refines(_,AbsName),RefSections),
841		event_b_model(AbsMachine,AbsName,AbsSections),
842		get_opt_section(events,RefSections,RawEvents),
843		get_opt_section(events,AbsSections,AbsRawEvents),
844		member(RawEvent,RawEvents),
845		bmachine_eventb:raw_event(RawEvent,_,RefEvName,_St1,Ref,_Prm1,RefGrd,_Thm1,RefAct,_Wit1,_Desc1),
846		Ref = [AbsEvName],
847		member(AbsRawEvent,AbsRawEvents),
848		bmachine_eventb:raw_event(AbsRawEvent,_,AbsEvName,_St2,_,_Prm2,AbsGrd,_Thm2,AbsAct,_Wit2,_Desc2),
849		check_raw_prefix(AbsGrd,RefGrd,SameGuard),
850		check_raw_prefix(AbsAct,RefAct,SameAct),
851		%% format('~nEvent refinement change ~w (~w) -> ~w (~w) guard: ~w, action: ~w~n',[RefEvName,RefName,AbsEvName,AbsName,SameGuard,SameAct]),
852		%print(rawgrd(RefGrd,AbsGrd)), nl, print(rawact(RefAct,AbsAct)),nl,
853		assertz(event_refinement_change(RefName,RefEvName,AbsName,AbsEvName,SameGuard,SameAct)),
854		fail.
855		analyse_eventb_refinement_types([_|T]) :- analyse_eventb_refinement_types(T).
856
857		check_raw_prefix([],[],Res) :- !, Res=unchanged.
858		check_raw_prefix([],[_|_],Res) :- !, Res=extends. % the refinement has some more actions/guards
859		check_raw_prefix([Abs|AT],[Ref|RT],Result) :- same_raw_expression(Abs,Ref),!,
860		check_raw_prefix(AT,RT,Result).
861		check_raw_prefix(_,_,refines).
862
863		% TO DO: check if we have a more complete version of this predicate; to do: handle @desc description/3 terms
864		same_raw_expression(identifier(_,A),RHS) :- !, RHS=identifier(_,B), A=B.
865		same_raw_expression(equal(_,A,B),RHS) :- !, RHS=equal(_,A2,B2), same_raw_expression(A,A2), same_raw_expression(B,B2).
866		same_raw_expression(assign(_,A1,A2),RHS) :- !, RHS=assign(_,B1,B2),
867		maplist(same_raw_expression,A1,B1), maplist(same_raw_expression,A2,B2).
868		same_raw_expression(A,B) :- atomic(A),!, A=B.
869		same_raw_expression(A,B) :- A =.. [F,_|AA], % print(match(F,AA)),nl,
870		B=.. [F,_|BB], maplist(same_raw_expression,AA,BB).
871
872
873
874		get_sees_context_refs(Sections,SRefs) :-
875		get_opt_section(sees,Sections,Seen),
876		findall(ref(sees,I,''),member(I,Seen),SRefs).
877
878		:- use_module(bmachine_eventb,[raw_event/11]).
879		get_events(Name,Sections,Events,AbsMachineName) :-
880		get_opt_section(events,Sections,RawEvents),
881		compute_event_refines(Name,RawEvents,AbsMachineName),
882		findall( identifier(Pos,EvName),
883		( member(RawEvent,RawEvents),
884		raw_event(RawEvent,Pos,EvName,_St,_Rf,_Prm,_Grd,_Thm,_Act,_Wit,_Desc) ),
885		Events).
886
887		% TO DO: detect when an event extends another one without changing it
888		compute_event_refines(MachineName,RawEvents,AbsMachineName) :-
889		member(RawEvent,RawEvents),
890		bmachine_eventb:raw_event(RawEvent,_Pos,EvName,_St,Refines,_Prm,_Grd,_Thm,_Act,_Wit,_Desc),
891		member(RefEvent,Refines),
892		% print(refines(MachineName,EvName,AbsMachineName,RefEvent)),nl,
893		assertz(refines_event(MachineName,EvName,AbsMachineName,RefEvent)),
894		fail.
895		compute_event_refines(_,_,_).
896
897
898		% try and get the name of the machine we refine
899		%machine_refines(Machine,AbsMachine) :- machine_references(Machine,Refs), member(ref(refines,AbsMachine,_),Refs).
900
901		analyse_eventb_context(Context) :-
902		event_b_context(Context,Name,Sections),
903		get_identifiers([constants],Sections,ConcreteConstants),
904		get_identifiers([abstract_constants],Sections,AbstractConstants),
905		append([ConcreteConstants,AbstractConstants],AllConstants),
906		get_sets(Sections,Sets),
907		get_extends_refs(Sections,Refs),
908		store_eventb_hash(Name,Context),
909		assertz(machine_type(Name,context)),
910		assertz(machine_identifiers(Name,[],Sets,[],[],[],AllConstants)),
911		assertz(machine_references(Name,Refs)),
912		assertz(machine_operations(Name,[])),
913		assertz(machine_operation_calls(Name,[])),
914		maplist(assert_raw_id_with_position(concrete_constant),ConcreteConstants),
915		maplist(assert_raw_id_with_position(abstract_constant),AbstractConstants),
916		assert_if_has_theorems(Name,Sections).
917
918		get_extends_refs(Sections,Refs) :-
919		get_opt_section(extends,Sections,Extended),
920		findall(ref(extends,E,''),member(E,Extended),Refs).
921
922		assert_if_has_theorems(Name,Sections) :-
923		get_opt_section(theorems,Sections,[_|_]),
924		assertz(machine_has_assertions(Name)).
925		assert_if_has_theorems(_Name,_Sections).
926
927
928		% compute a hash based on constants and properties
929		properties_hash(MachineName,Hash) :-
930		properties_hash_cached(MachineName,Hash1),!,
931		Hash=Hash1.
932		properties_hash(MachineName,Hash) :-
933		compute_properties_hash(MachineName,Hash1),
934		assertz(properties_hash_cached(MachineName,Hash1)),
935		Hash=Hash1.
936		compute_properties_hash(Name,Hash) :-
937		raw_machine(Name,Machine),
938		get_machine(Name,[Machine],_Type,_Header,_Refines,Body),
939		extract_sorted_np_sets(Body,Sets),
940		extract_sorted_np_constants(Body,Constants),
941		extract_np_properties(Body,Properties),
942		extract_used_np_definitions_from_properties(Body,Definitions),
943		ToHash = [Sets,Constants,Properties,Definitions],
944		raw_sha_hash(ToHash,Hash).
945		% save_properties_hash(Name,ToHash,Hash).
946
947		extract_sorted_np_sets(Body,Sets) :-
948		get_sets(Body,PosSets),
949		remove_raw_position_info(PosSets,UnsortedSets),
950		sort(UnsortedSets,Sets).
951		extract_sorted_np_constants(Body,Constants) :-
952		get_opt_sections([constants,concrete_constants,abstract_constants],Body,PosConstants),
953		remove_raw_position_info(PosConstants,UnsortedConstants),
954		sort(UnsortedConstants,Constants).
955		extract_np_properties(Body,Properties) :-
956		get_opt_section(properties,Body,PosProperties),
957		remove_raw_position_info(PosProperties,Properties).
958		extract_used_np_definitions_from_properties(Body,Definitions) :-
959		get_opt_section(properties,Body,Properties),
960		extract_used_np_definitions(Properties,Body,Definitions,_).
961		extract_used_np_definitions(RawSyntax,Body,Definitions,PosDefinitions) :-
962		extract_raw_identifiers(RawSyntax,UsedIds),
963		all_definition_ids(Body,AllDefs),
964		ord_intersection(UsedIds,AllDefs,UsedDefNames),
965		transitive_used_definitions(UsedDefNames,AllUsedDefs),
966		findall( definition(none,Name,Args,DefBody),
967		( member(Name,AllUsedDefs),b_get_definition(Name,_DefType,Args,DefBody,_Deps)),
968		PosDefinitions),
969		maplist(remove_raw_position_info,PosDefinitions,Definitions).
970		all_definition_ids(Body,Ids) :-
971		get_opt_section(definitions,Body,Definitions),
972		convlist(get_definition_name,Definitions,Ids1),
973		sort(Ids1,Ids).
974		transitive_used_definitions(Defs,TransDefs) :-
975		findall( D, reachable_definition(Defs,D), TD1),
976		sort(TD1,TransDefs).
977		reachable_definition(Defs,D) :-
978		member(N,Defs),
979		( D=N
980		; b_get_definition(N,_DefType,_Args,_Body,Deps),
981		reachable_definition(Deps,D)).
982
983
984		/* just for debugging:
985		save_properties_hash(MachineName,ToHash,Hash) :-
986		main_machine_name(Main),
987		open('/home/plagge/hashes.pl',append,S),
988		writeq(S,hash(Main,MachineName,ToHash,Hash)),
989		write(S,'.\n'),
990		close(S).
991		*/
992
993		% ---------------------------
994		:- dynamic event_info/3.
995		analyze_extends_relation :-
996		retractall(event_info(_,_,_)),
997		bmachine:b_get_machine_operation(_Name,_Results,_RealParameters,TBody,_OType,_OpPos),
998		treat_event_body(TBody),fail.
999		analyze_extends_relation.
1000
1001		treat_event_body(TBody) :-
1002		rlevent_info(TBody,EventName,Machine,Status,AbstractEvents),
1003		% format('Event ~w:~w ~w~n',[Machine,EventName,Status]),
1004		assertz(event_info(Machine,EventName,Status)),
1005		maplist(treat_event_body,AbstractEvents).
1006
1007		:- use_module(bsyntaxtree,[get_texpr_expr/2]).
1008		rlevent_info(TBody,EventName,Machine,FStatus,AbstractEvents) :-
1009		get_texpr_expr(TBody,Event),
1010		Event = rlevent(EventName,Machine,TStatus,_Params,_Guard,_Theorems,_Actions,_VWit,_PWit,_Unmod,AbstractEvents),
1011		bsyntaxtree:get_texpr_expr(TStatus,Status), %ordinary, convergent, anticipated
1012		functor(Status,FStatus,_).
1013
1014
1015		% write the event refinement hierarchy to a dot file
1016		% (currently) only makes sense for Event-B models
1017
1018		:- use_module(preferences,[get_preference/2]).
1019		:- use_module(tools_strings,[ajoin/2, ajoin_with_sep/3]).
1020
1021		:- public dot_refinement_node_new/4.
1022		% variation for: use_new_dot_attr_pred
1023		dot_refinement_node_new(event_refinement,M:Ev,M,[label/Desc,shape/Shape,tooltip/Tooltip|T1]) :-
1024		dot_event_node(M:Ev,M,Desc,Shape,Style,Color),
1025		(Style=none -> T1=T2 ; T1=[style/Style|T2]),
1026		(Color=none -> T2=[] ; T2=[color/Color]),
1027		(event_info(M,Ev,Status) -> true ; Status=unknown),
1028		(event_refinement_change(M,Ev,AbsName,AbsEvName,SameGuard,SameAct)
1029		-> ajoin(['Event ',Ev,' in ',M,
1030		'\n status: ',Status,
1031		'\n refines ',AbsEvName,' in ',AbsName,
1032		'\n guard: ',SameGuard,
1033		'\n action: ',SameAct], Tooltip)
1034		; ajoin(['Event ',Ev,' in ',M,
1035		'\n status: ',Status], Tooltip)).
1036		dot_refinement_node_new(variable_refinement(With),M:Var,M,[label/Desc,shape/Shape,color/Color,tooltip/Tooltip|T1]) :-
1037		(With=with_constants -> machine_ids(M,Vars) ; machine_variables(M,Vars)),
1038		member(Var,Vars),
1039		Desc=Var,
1040		(id_exists_in_abstraction(M,Anc,Var)
1041		-> get_preference(dot_event_hierarchy_unchanged_event_colour,Color), T1=[style/filled],
1042		Shape = rect, % we could use plain; makes kept events smaller
1043		ajoin(['Variable kept from abstraction ',Anc],Tooltip)
1044		; machine_type(M,context), machine_sets(M,Sets), member(Var,Sets) ->
1045		get_preference(dot_event_hierarchy_refines_colour,Color), T1=[style/'rounded,filled'],
1046		Shape = rect,
1047		ajoin(['New set in ',M],Tooltip)
1048		; machine_type(M,context) -> % it must be a constant
1049		get_preference(dot_event_hierarchy_new_event_colour,Color), T1=[style/rounded],
1050		Shape = rect,
1051		ajoin(['New constant in ',M],Tooltip)
1052		; get_preference(dot_event_hierarchy_new_event_colour,Color), T1=[],
1053		Shape = rect,
1054		ajoin(['New variable in ',M],Tooltip)
1055		).
1056		%dot_refinement_node_new(variable_refinement(_),C:Cst,M,[label/Desc,shape/rect,color/Color,tooltip/Desc|T1]) :-
1057		% new_seen_context(M,C), machine_constants(C,Csts), member(Cst,Csts),
1058		% Desc=Cst, T1=[style/rounded], get_preference(dot_event_hierarchy_extends_colour,Color).
1059
1060		% the node ide is M:Ev as Ev can and usually does occur multiple times
1061		dot_event_node(M:Ev,M,Desc,Shape,Style,Color) :-
1062		findall(showev(M,Ev),event_to_show(M,Ev),List), sort(List,SList),
1063		member(showev(M,Ev),SList),
1064		(event_info(M,Ev,Status) -> true ; Status=unknown),
1065		(event_refinement_change(M,Ev,_,_,SameGuard,SameAction)
1066		-> true ; SameGuard=unknown, SameAction=unknown),
1067		(SameGuard=SameAction, SameGuard \= unknown -> ajoin([Ev,'\\n(',SameAction,')'],Ev2)
1068		; SameGuard=unchanged ,SameAction=extends-> ajoin([Ev,'\\n(same grd, extends act)'],Ev2)
1069		; SameGuard=unchanged -> ajoin([Ev,'\\n(same grd)'],Ev2)
1070		; SameGuard=extends,SameAction=unchanged -> ajoin([Ev,'\\n(same act, extends grd)'],Ev2)
1071		; SameAction=unchanged -> ajoin([Ev,'\\n(same act)'],Ev2)
1072		; SameGuard=extends -> ajoin([Ev,'\\n(extends grd)'],Ev2)
1073		; SameAction=extends -> ajoin([Ev,'\\n(extends act)'],Ev2)
1074		; Ev2=Ev),
1075		(Status = convergent -> ajoin([Ev2,' (<)'],Desc)
1076		; Status = anticipated -> ajoin([Ev2, ' (<=)'],Desc)
1077		; Desc=Ev2),
1078		% format(user_output,'event ~w, status:~w, same guard:~w, same action:~w~n',[Ev,Status,SameGuard,SameAction]),
1079		dot_get_color_style(M,Ev,Status,SameGuard,SameAction,Shape,Color,Style).
1080
1081		event_to_show(M,Ev) :- machine_operations(M,Evs),
1082		raw_identifier_member(Ev,Evs), Ev \= 'INITIALISATION'.
1083		event_to_show(M,Ev) :-
1084		event_refinement_change(M,Ev,_,_,_,_), % for events that disappear, i.e., are not refined until bottom level
1085		Ev \= 'INITIALISATION'.
1086
1087
1088		dot_get_color_style(M,Ev,_Status,_,_,box,Color,Style) :- \+ refines_event(M,Ev,_,_),!,
1089		get_preference(dot_event_hierarchy_new_event_colour,Color), Style=none.
1090		dot_get_color_style(M,Ev,_,SameGuard,SameAction,box,Color,Style) :-
1091		refines_event(M,Ev,_,Ev2), dif(Ev2,Ev),!, % changes name
1092		((SameGuard,SameAction)=(unchanged,unchanged)
1093		-> get_preference(dot_event_hierarchy_rename_unchanged_event_colour,Color)
1094		; get_preference(dot_event_hierarchy_rename_event_colour,Color)), Style=filled.
1095		dot_get_color_style(_M,_Ev,_,unchanged,unchanged,plain,Color,Style) :- % keeps name and adds no guard or action
1096		!,
1097		get_preference(dot_event_hierarchy_unchanged_event_colour,Color), Style=filled.
1098		dot_get_color_style(_M,_Ev,_,_,unchanged,box,Color,Style) :- % keeps name and adds no action, but modifies guard
1099		!,
1100		get_preference(dot_event_hierarchy_grd_strengthening_event_colour,Color), Style=filled.
1101		dot_get_color_style(_M,_Ev,_,unchanged,_,box,Color,Style) :- % keeps name and adds action but keeps guard
1102		!,
1103		get_preference(dot_event_hierarchy_grd_keeping_event_colour,Color), Style=filled.
1104		dot_get_color_style(_M,_Ev,_,_,_,box,Color,Style) :- % keeps name but adds or modifies
1105		% TO DO: distinguish extends from refines
1106		get_preference(dot_event_hierarchy_refines_colour,Color), Style=filled.
1107
1108		:- public dot_refines_event/4.
1109		% dot transition predicate for event and variable refinement hierarchy diagram
1110		dot_refines_event(event_refinement,M2:Ev2,M1:Ev1,[label/Label,color/Color,style/Style]) :-
1111		Label = '', % TO DO: detect refine, extends, identical
1112		refines_event(M1,Ev1,M2,Ev2),
1113		Ev1 \= 'INITIALISATION',
1114		(event_refinement_change(M1,Ev1,_,_,SameGuard,SameAct)
1115		-> arrow_style(SameGuard,SameAct,Style,ColPref), get_preference(ColPref,Color)
1116		; Style=solid, Color=red % should not happen
1117		).
1118		dot_refines_event(variable_refinement(With),M1:Var,M2:Var2,[label/Label,color/Color,style/Style|T1]) :-
1119		get_preference(dot_event_hierarchy_edge_colour,Color),
1120		(With=with_constants -> machine_ids(M2,Vars2) ; machine_variables(M2,Vars2)),
1121		if((member(Var,Vars2),
1122		id_exists_in_abstraction(M2,M1,Var)),
1123		(Label='',Var2=Var,Style=dashed, T1=[]),
1124		(% no variable of M2 exists in M1
1125		refines_or_extends_machine(M2,M1),
1126		machine_ids(M1,[Var|_]), % get first variable of M1
1127		Vars2=[Var2|_], Style=dotted, % add virtual edge to first variable of M2 if no variable is kept
1128		get_dot_cluster_name(M1,M1C), get_dot_cluster_name(M2,M2C),
1129		T1 = [ltail/M1C, lhead/M2C],
1130		(machine_type(M2,context) -> Label='extends' ; Label='')
1131		)
1132		).
1133		dot_refines_event(variable_refinement(with_constants),M1:Var1,M2:Cst2,[label/Label,color/Color,style/Style|T1]) :- Label='sees',
1134		Color=gray80, Style=solid,
1135		new_seen_context(M1,M2),
1136		machine_ids(M1,[Var1|_]),
1137		machine_ids(M2,[Cst2|_]),
1138		get_dot_cluster_name(M1,M1C), get_dot_cluster_name(M2,M2C),
1139		T1 = [ltail/M1C, lhead/M2C, dir/forward].
1140
1141		arrow_style(unchanged,unchanged,Style,ColPref) :- !,
1142		Style=arrowhead(none,solid), ColPref=dot_event_hierarchy_extends_colour.
1143		arrow_style(refines,_,Style,ColPref) :- !, Style=solid, ColPref=dot_event_hierarchy_edge_colour.
1144		arrow_style(_,refines,Style,ColPref) :- !, Style=solid, ColPref=dot_event_hierarchy_edge_colour.
1145		%arrow_style(_,_,Style) :- Style = arrowhead(vee,arrowtail(box,solid)). % we have extends
1146		arrow_style(_,_,Style,dot_event_hierarchy_extends_colour) :- Style = arrowhead(vee,solid). % we have extends
1147
1148
1149		%dot_same_rank(SameRankVals) :- machine_operations(M,Evs),
1150		% findall(M:Ev,raw_identifier_member(Ev,Evs),SameRankVals).
1151
1152		dot_subgraph(Kind,sub_graph_with_attributes(M,Attrs), filled,Colour) :-
1153		get_preference(dot_event_hierarchy_machine_colour,MColour),
1154		Attrs = [label/Label, tooltip/ToolTip],
1155		machine_operations(M,Ops),
1156		(Kind=event_refinement -> Ops=[_|_] ; true),
1157		(machine_type(M,context) -> IDS = 'csts', Colour=gray90
1158		; IDS = 'vars', Colour=MColour),
1159		(machine_ids(M,Vars)
1160		-> length(Vars,V),
1161		findall(C,new_seen_context(M,C),NewC),
1162		split_list(id_exists_in_abstraction(M),Vars,_Old,NewVars),
1163		length(NewVars,NewNr),
1164		findall(Del,(var_exists_in_abstraction(M,Del), nonmember(Del,Vars)),DelVars),
1165		length(DelVars,DelNr),
1166		(Kind=event_refinement, get_preference(dot_hierarchy_show_extra_detail,false)
1167		-> Label=M
1168		; ajoin([M,'\\n#',IDS,'=',V, ' (+',NewNr,',-', DelNr,')'],Label)
1169		),
1170		ajoin_with_sep(NewVars,',',NV),
1171		ajoin_with_sep(DelVars,',',DV),
1172		ajoin_with_sep(NewC,',',NC),
1173		ajoin(['machine ',M,'\\n#',IDS,'=',V, ' (+',NewNr,',-', DelNr,')',
1174		'\\nnew sees=',NC,
1175		'\\nnew ',IDS,'=',NV,
1176		'\\ndel ',IDS,'=',DV],ToolTip)
1177		; Label=M, ToolTip=M).
1178
1179		machine_variables(M,Vars) :- machine_identifiers(M,_Params,_Sets,AVars,CVars,_AConsts,_CConsts),
1180		append(CVars,AVars,RVars), % for Event-B: CVars=[]
1181		maplist(get_raw_identifier,RVars,Vars).
1182		%machine_constants(M,Consts) :- machine_identifiers(M,_Params,_Sets,_AVars,_CVars,AConsts,CConsts),
1183		% append(CConsts,AConsts,Raw),
1184		% maplist(get_raw_identifier,Raw,Consts).
1185		machine_ids(M,Vars) :- machine_identifiers(M,_Params,Sets,AVars,CVars,AConsts,CConsts),
1186		append([Sets,CConsts,CVars,AConsts,AVars],RVars),
1187		maplist(get_raw_identifier,RVars,Vars).
1188		machine_sets(M,Vars) :- machine_identifiers(M,_,Sets,_,_,_,_),
1189		maplist(get_raw_identifier,Sets,Vars).
1190
1191		var_exists_in_abstraction(M,Var) :-
1192		var_exists_in_abstraction(M,_Anc,Var).
1193		var_exists_in_abstraction(M,Anc,Var) :-
1194		refines_machine(M,Anc),
1195		machine_variables(Anc,AncVars),
1196		member(Var,AncVars).
1197
1198		refines_machine(M,Anc) :-
1199		machine_references(M,Refs),
1200		member(ref(refines,Anc,_),Refs).
1201
1202		% variable or constant exists in abstraction
1203		id_exists_in_abstraction(M,Var) :-
1204		id_exists_in_abstraction(M,_Anc,Var).
1205		id_exists_in_abstraction(M,Anc,Var) :-
1206		refines_or_extends_machine(M,Anc),
1207		machine_ids(Anc,AncVars),
1208		member(Var,AncVars).
1209
1210		refines_or_extends_machine(M,Anc) :-
1211		machine_references(M,Refs),
1212		(member(ref(refines,Anc,_),Refs) -> true ; member(ref(extends,Anc,_),Refs)).
1213
1214		new_seen_context(M,Context) :- machine_references(M,Refs),
1215		member(ref(sees,Context,_),Refs),
1216		\+ (member(ref(refines,Anc,_),Refs),
1217		sees_context(Anc,Context)).
1218
1219		sees_context(M,Context) :- machine_references(M,Refs), member(ref(sees,Context,_),Refs).
1220
1221
1222		write_dot_event_hierarchy_to_file(File) :-
1223		write_dot_ref_hierarchy_to_file(event_refinement,File).
1224		write_dot_variable_hierarchy_to_file(File) :-
1225		(get_preference(dot_hierarchy_show_extra_detail,false) -> With=no_constants ; With=with_constants),
1226		write_dot_ref_hierarchy_to_file(variable_refinement(With),File).
1227		write_dot_ref_hierarchy_to_file(Kind,File) :-
1228		analyze_extends_relation,
1229		(get_preference(dot_event_hierarchy_horizontal,true)
1230		-> PageOpts=[compound/true,rankdir/'LR',no_page_size]
1231		; PageOpts=[compound/true]),
1232		gen_dot_graph(File,PageOpts,
1233		use_new_dot_attr_pred(b_machine_hierarchy:dot_refinement_node_new(Kind)),
1234		use_new_dot_attr_pred(b_machine_hierarchy:dot_refines_event(Kind)),
1235		dot_no_same_rank,dot_subgraph(Kind)).
1236		%gen_dot_graph(File,PageOpts,dot_event_node,dot_refines_event,dot_no_same_rank,dot_subgraph).
1237
1238		% --------------------
1239
1240		reference_link(FromMachine,DestMachine) :-
1241		machine_references(FromMachine,Refs),
1242		filter_redundant_refs(Refs,Refs,UsefulRefs),
1243		member(ref(_Type,DestMachine,_Prefix),UsefulRefs).
1244
1245		:- use_module(library(ugraphs),[vertices_edges_to_ugraph/3, top_sort/2, transitive_closure/2,
1246		min_paths/3, min_path/5, neighbours/3, del_vertices/3]).
1247
1248		% b_machine_hierarchy:get_machine_topological_order(V)
1249		% get machine in topological order of inclusion
1250		get_machine_topological_order(SortedVertices) :-
1251		get_machine_inclusion_graph(_Vertices,_Edges,Graph),
1252		top_sort(Graph,SortedVertices).
1253
1254		% get machine inclusion graph in format for ugraphs (unweighted graphs) library
1255		get_machine_inclusion_graph(Vertices,Edges,Graph) :-
1256		findall(Mach,machine_name(Mach),Vertices),
1257		findall(From-To,reference_link(From,To),Edges),
1258		vertices_edges_to_ugraph(Vertices, Edges, Graph).
1259
1260		print_machine_topological_order :-
1261		format('Topological sorting of B machine references~n',[]),
1262		get_machine_inclusion_graph(Vertices,Edges,Graph),
1263		length(Vertices,LenV),format(' * number of machines: ~w~n',[LenV]),
1264		length(Edges,LenE), format(' * number of reference links: ~w~n',[LenE]),
1265		top_sort(Graph,SortedVertices),
1266		main_machine_name(Main),
1267		%min_paths(Main,Graph,MinPaths),
1268		transitive_closure(Graph,TGraph),
1269		maplist(top_print_machine(Main,Graph,TGraph),SortedVertices),
1270		greedy_cover(Main,Graph,TGraph,GreedyCover), length(GreedyCover,GLen),
1271		get_rel_file_name(GreedyCover,FGreedy),
1272		ajoin_with_sep(FGreedy,' ',GreedyList), % generate list which can be used for probcli or Makefile
1273		format(' * sufficient includes (~w) to cover all machines: ~w~n',[GLen,GreedyList]),
1274
1275		format(' (for each machine do: probcli FILE.mch -init -cache DIR)~n',[]).
1276
1277		top_print_machine(Main,Graph,TGraph,M) :-
1278		(machine_references(M,Refs) -> length(Refs,Len) ; Len=0),
1279		neighbours(M,TGraph,N), length(N,Len2),
1280		format(' ~w has ~w direct references and ~w indirect ones~n',[M,Len,Len2]),
1281		min_path(Main, M, Graph, Path, Length),
1282		format(' inclusion length ~w: ~w~n',[Length,Path]).
1283
1284		get_rel_file_name([],[]).
1285		get_rel_file_name([Machine|T],[File|TF]) :-
1286		(b_get_relative_file_name_for_machine(Machine,File) -> true ; File=Machine),
1287		get_rel_file_name(T,TF).
1288
1289		greedy_cover(Main,Graph,TGraph,GreedyCover) :-
1290		neighbours(Main,Graph,TopLevelIncludes),
1291		greedy_cover(TopLevelIncludes,TGraph,GreedyCover).
1292
1293		% compute a list of included machines which cover all required inclusions
1294		% we try to make this inclusion minimal, using a greedy algorithm
1295		greedy_cover([],_TGraph,Cover) :- !, Cover=[].
1296		greedy_cover(RemainingIncludes,TGraph, GreedyCover) :-
1297		findall(candidate(NrCovered,Machine),
1298		(member(Machine,RemainingIncludes),
1299		neighbours(Machine,TGraph,N), length(N,NrCovered)), Cands),
1300		(max_member(candidate(MaxNrCov,NextChoice),Cands) % pick the machine covering the most other ones
1301		->
1302		(MaxNrCov =< 0
1303		-> GreedyCover = [] % everything is included already
1304		; GreedyCover = [NextChoice|TGreedyCover],
1305		select(NextChoice,RemainingIncludes,Rem2), % this include is no longer available
1306		neighbours(NextChoice,TGraph,NowCovered),
1307		del_vertices(TGraph, [NextChoice|NowCovered], TGraph2), % delete all machines included by NextChoice
1308		greedy_cover(Rem2,TGraph2,TGreedyCover)
1309		)
1310		; GreedyCover = [] % everything is included already; no node appears in the graph anymore
1311		).
1312