1		% (c) 2009-2019 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_type/2 % machine_type(Name, R) - get the type
9		% (abstract_machine, abstract_model, refinement, implementation) for the machine named Name
10		,machine_references/2 % get a list of references and the type of the reference.
11		% Example: if A refines B, then machine_references('A',X) returns X= [ref(refines'B','')].
12		% The last argument in ref/3 is the prefix
13		,machine_identifiers/7 % gets Params,Sets,Abstract Variables,Concrete Variables,Abstract Constants and Concrete
14		% Constants for a machine. Abstract constants/Variables are introduced in the machine
15		% using the ABSTRACT_VARAIABLES/ABSTARCT_CONSTANTS keyword. The concrete versions
16		% analogously via CONCRETE_VARAIBLES,CONCRETE_CONSTANTS
17		% Example output for
18		% MACHINE xx(T,u)
19		% CONSTRAINTS u:T
20		% SETS A; B={foo, bar}
21		% CONCRETE_CONSTANTS cc
22		% PROPERTIES cc:B
23		% ABSTRACT_VARIABLES xx
24		% CONCRETE_VARIABLES yy
25		% INVARIANT
26		% xx:INT &
27		% yy : T
28		% INITIALISATION xx,yy:= ({1|->2};{2|->4})(1), u
29		% END
30		%
31		% machine_identifiers(A,B,C,D,E,F,G).
32		% A = xx,
33		% B = [identifier(pos(4,1,1,12,1,12),'T'),identifier(pos(5,1,1,14,1,14),u)],
34		% 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)])],
35		% D = [identifier(pos(22,1,6,20,6,21),xx)],
36		% E = [identifier(pos(24,1,7,20,7,21),yy)],
37		% F = [],
38		% G = [identifier(pos(16,1,4,20,4,21),cc)]
39		, get_machine_identifier_names/7 % a version returning atomic identifier names
40		,abstract_constant/2, concrete_constant/2
41		,possibly_abstract_constant/1
42		,machine_operations/2 % machine_operations(M, Ops) gets the names of the Operations defined in Machine M
43		,machine_hash/2 % stores a hash value for the machine
44		,properties_hash/2 % computes a hash over the constants and properties
45		,operation_hash/3 % computes a hash for the operation in a machine
46		,write_dot_hierarchy_to_file/1
47		,write_dot_event_hierarchy_to_file/1
48		]).
49
50		:- use_module(library(lists)).
51		:- use_module(library(ordsets)).
52		:- use_module(bmachine,[b_get_definition/5, b_filenumber/4]).
53		:- use_module(bmachine_construction).
54		:- use_module(self_check).
55		:- use_module(specfile,[get_specification_description/2]).
56		:- use_module(extension('probhash/probhash'),[raw_sha_hash/2]).
57		:- use_module(input_syntax_tree).
58
59		:- use_module(value_persistance,[cache_is_activated/0]).
60
61		:- use_module(module_information,[module_info/2]).
62		:- module_info(group,analysis).
63		:- module_info(description,'This module provides functionality to visualize the dependencies of a B machine (include and sees relations, etc.).').
64
65		:- volatile
66		main_machine_name/1,
67		machine_type/2,
68		machine_references/2,
69		machine_identifiers/7,
70		machine_operations/2,
71		refines_event/4,
72		machine_has_assertions/1,
73		machine_hash/2,
74		raw_machine/2,
75		machine_hash_cached/2,
76		properties_hash_cached/2, operation_hash_cached/3,
77		event_refinement_change/6.
78		:- dynamic
79		main_machine_name/1,
80		machine_type/2,
81		machine_references/2,
82		machine_identifiers/7,
83		machine_operations/2,
84		refines_event/4,
85		machine_has_assertions/1,
86		machine_hash/2,
87		raw_machine/2,
88		machine_hash_cached/2,
89		properties_hash_cached/2, operation_hash_cached/3,
90		event_refinement_change/6.
91		:- volatile abstract_constant/2, concrete_constant/2.
92		:- dynamic abstract_constant/2.
93		:- dynamic concrete_constant/2.
94
95		:- use_module(specfile,[animation_minor_mode/1]).
96		possibly_abstract_constant(ID) :-
97		(abstract_constant(ID,_) ; animation_minor_mode(eventb),concrete_constant(ID,_) ).
98
99		reset_hierarchy :-
100		retract_all(main_machine_name/1),
101		retract_all(machine_type/2),
102		retract_all(machine_references/2),
103		retract_all(machine_identifiers/7),
104		retract_all(abstract_constant/2),
105		retract_all(concrete_constant/2),
106		retract_all(machine_operations/2),
107		retract_all(refines_event/4),
108		retract_all(machine_has_assertions/1),
109		retract_all(machine_hash/2),
110		retract_all(raw_machine/2),
111		retract_all(properties_hash_cached/2),
112		retract_all(operation_hash_cached/3),
113		retract_all(event_refinement_change/6).
114
115		:- use_module(eventhandling,[register_event_listener/3]).
116		:- register_event_listener(clear_specification,reset_hierarchy,
117		'Reset B Machine Hierarchy Facts.').
118
119		retract_all(Functor/Arity) :-
120		functor(Pattern,Functor,Arity),
121		retractall(Pattern).
122
123		analyse_hierarchy(Main,Machines) :-
124		reset_hierarchy,
125		assert(main_machine_name(Main)),
126		analyse_machine(Main,Machines,main).
127
128		:- use_module(error_manager).
129		:- use_module(tools_strings,[ajoin/2]).
130		:- public analyse_machine/3.
131		analyse_machine(Name,_Machines,_) :-
132		% machine already analysed
133		machine_type(Name,_),!.
134		analyse_machine(Name,Machines,_) :-
135		debug:debug_println(9,analysing_machine(Name)),
136		get_machine(Name,Machines,Type,Header,Refines,Body),
137		!,
138		( cache_is_activated -> % we need the machines stored for later analysis
139		assert_all_machines(Machines)
140		; otherwise -> true),
141		assert(machine_type(Name,Type)),
142		( get_raw_section(assertions,Body,_) ->
143		assert(machine_has_assertions(Name))
144		; true),
145		store_identifiers(Name,Header,Body),
146		store_operations(Name,Body),
147		store_references(Name,Refines,Body,Machines).
148		analyse_machine(Name,Machines,RefType) :-
149		b_filenumber(Name,_Ext,Nr,File),
150		get_ref_type_name(RefType,Clause),
151		!,
152		((member(M,Machines),get_constructed_machine_name_and_filenumber(M,OtherName,Nr))
153		-> ajoin(['Cannot use B machine "',Name,'" within ', Clause,
154		' clause. Rename machine "', OtherName,'" to "', Name, '" in file: '],Msg)
155		; ajoin(['Cannot find B machine "',Name,'" within ', Clause,
156		' clause. Check that machine name matches filename in: '],Msg)
157		),
158		add_error_fail(invalid_machine_reference,Msg,File).
159		analyse_machine(Name,_Machines,_) :-
160		add_error_fail(invalid_machine_reference,
161		'Could not find machine in parsed machine list (check that your machine names match your filenames): ',Name).
162
163		% store the un-typed input syntax tree for later analysis
164		assert_all_machines(Machines) :- maplist(assert_raw_machine,Machines).
165		assert_raw_machine(Machine) :-
166		get_raw_machine_name(Machine,Name),
167		assert( raw_machine(Name,Machine) ).
168
169
170		store_identifiers(Name,Header,Body) :-
171		get_parameters(Header,Params),
172		get_sets(Body,Sets),
173		get_identifiers([abstract_variables,variables],Body,AVars),
174		get_identifiers([concrete_variables],Body,CVars),
175		get_identifiers([abstract_constants],Body,AConsts),
176		get_identifiers([concrete_constants,constants],Body,CConsts), % fixed abstract -> concrete
177		assert(machine_identifiers(Name,Params,Sets,AVars,CVars,AConsts,CConsts)),
178		maplist(assert_raw_id_with_position(abstract_constant),AConsts),
179		maplist(assert_raw_id_with_position(concrete_constant),CConsts).
180
181
182		raw_id_is_identifier2(description(_Pos,_Desc,Raw),ID) :- !, raw_id_is_identifier2(Raw,ID).
183		raw_id_is_identifier2(deferred_set(_,ID),ID) :- !.
184		raw_id_is_identifier2(enumerated_set(_,ID,_Elements),ID) :- !.
185		raw_id_is_identifier2(Raw,ID) :- raw_id_is_identifier(Raw,_,ID).
186
187		get_machine_identifier_names(Name,Params,Sets,AVars,CVars,AConsts,CConsts) :-
188		machine_identifiers(Name,RawParams,RawSets,RawAVars,RawCVars,RawAConsts,RawCConsts),
189		maplist(raw_id_is_identifier2,RawParams,Params),
190		maplist(raw_id_is_identifier2,RawSets,Sets),
191		maplist(raw_id_is_identifier2,RawAVars,AVars),
192		maplist(raw_id_is_identifier2,RawCVars,CVars),
193		maplist(raw_id_is_identifier2,RawAConsts,AConsts),
194		maplist(raw_id_is_identifier2,RawCConsts,CConsts).
195
196
197		machine_hash(Name,Hash) :-
198		machine_hash_cached(Name,Hash1),!,Hash=Hash1.
199		machine_hash(Name,Hash) :-
200		compute_machine_hash(Name,Hash1),
201		assert( machine_hash_cached(Name,Hash1) ),
202		Hash=Hash1.
203		compute_machine_hash(Name,Digest) :-
204		raw_machine(Name,Machine),
205		raw_sha_hash(Machine,Digest).
206
207		operation_hash(MachName,OpName,Hash) :-
208		operation_hash_cached(MachName,OpName,Hash1),!,Hash=Hash1.
209		operation_hash(MachName,OpName,Hash) :-
210		compute_operation_hash(MachName,OpName,Hash1),
211		assert( operation_hash_cached(MachName,OpName,Hash1) ),
212		Hash=Hash1.
213		compute_operation_hash(MachName,OpName,Digest) :-
214		raw_machine(MachName,Machine),
215		get_machine(MachName,[Machine],_Type,_Header,_Refines,Body),
216		get_opt_section(operations,Body,Operations),
217		Op = operation(_,identifier(_,OpName),_,_,_),
218		memberchk(Op,Operations),
219		extract_used_np_definitions(Op,Body,UsedDefinitions),
220		remove_raw_position_info(Op,RawOperation),!,
221
222		raw_sha_hash(op(RawOperation,UsedDefinitions),Digest).
223
224
225		:- use_module(debug,[debug_println/2]).
226		assert_raw_id_with_position(PredFunctor,Rid) :-
227		(raw_id_is_identifier(Rid,Pos,ID)
228		-> true
229		; Rid = definition(Pos,ID,_)
230		-> add_error(assert_raw_id_with_position,'Definition cannot be used as identifier here: ',ID,Pos)
231		; add_error_fail(assert_raw_id_with_position,'Not identifier: ',Rid)
232		),
233		Fact =.. [PredFunctor,ID,Pos],
234		assert(Fact), debug_println(9,Fact).
235
236		raw_id_is_identifier(identifier(Pos,ID),Pos,ID).
237		raw_id_is_identifier(unit(_,_,identifier(Pos,ID)),Pos,ID).
238		raw_id_is_identifier(new_unit(_,_,identifier(Pos,ID)),Pos,ID).
239		raw_id_is_identifier(inferred_unit(_,_,identifier(Pos,ID)),Pos,ID).
240		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
241		raw_id_is_identifier(description(_,_,identifier(Pos,ID)),Pos,ID).
242
243		get_raw_identifier(Raw,Res) :- raw_id_is_identifier(Raw,_Pos,Id),!, Res=Id.
244		get_raw_identifier(definition(_Pos,DID,[]),ID) :- % see also expand_definition_to_variable_list
245		atom(DID),!,
246		ajoin([DID,'(DEFINITION)'],ID).
247		get_raw_identifier(Raw,Res) :- add_internal_error('Cannot get identifier:',Raw),Res='???'.
248
249		raw_identifier_member(ID,List) :- member(Raw,List), raw_id_is_identifier(Raw,_Pos,ID).
250
251		store_operations(Name,Body) :-
252		get_opt_section(operations,Body,Operations),
253		findall(I,(member(Op,Operations),get_raw_operation_id(Op,I)),Ids),
254		assert(machine_operations(Name,Ids)).
255
256		get_raw_operation_id(operation(_Pos,Id,_,_,_),Id).
257		get_raw_operation_id(refined_operation(_Pos,Id,_Results,_Args,_RefinesID,_Body),Id).
258
259		store_references(Name,Refines,Body,Machines) :-
260		debug:debug_println(9,store_references(Name)),
261		get_refinements(Refines,Refs1),
262		get_references(Body,Refs2),
263		append(Refs1,Refs2,Refs),
264		assert(machine_references(Name,Refs)),
265		follow_refs(Refs,Machines).
266
267		get_references(Body,Refs) :-
268		findrefs(Body,includes,Includes),
269		findrefs(Body,extends,Extends),
270		findrefs(Body,imports,Imports),
271		findusessees(Body,uses,Uses),
272		findusessees(Body,sees,Sees),
273		append([Includes,Imports,Extends,Uses,Sees],Refs).
274
275		get_refinements([],[]).
276		get_refinements([Name|NRest],[ref(refines,Name,'')|RRest]) :-
277		get_refinements(NRest,RRest).
278
279		findrefs(Body,Type,Refs) :-
280		get_opt_section(Type,Body,RawRefs),
281		findrefs2(RawRefs,Type,Refs).
282		findrefs2([],_Type,[]).
283		findrefs2([machine_reference(_Pos,R,_Params)|MRest],Type,[ref(Type,Name,Prefix)|RRest]) :-
284		bmachine_construction:split_prefix(R,Prefix,Name),
285		findrefs2(MRest,Type,RRest).
286
287		findusessees(Body,Type,Refs) :-
288		get_opt_section(Type,Body,RawRefs),
289		findusessees2(RawRefs,Type,Refs).
290		findusessees2([],_Type,[]).
291		findusessees2([identifier(_Pos,Name)|MRest],Type,[ref(Type,Name,'')|RRest]) :-
292		findusessees2(MRest,Type,RRest).
293
294		follow_refs([],_Machines).
295		follow_refs([ref(RefType,Name,_Prefix)|Rest],Machines) :-
296		analyse_machine(Name,Machines,RefType),
297		follow_refs(Rest,Machines).
298
299		get_parameters(machine_header(_Pos,_Name,Params),Params).
300
301		get_sets(Body,Sets) :-
302		get_opt_section(sets,Body,Sets).
303
304		get_identifiers([],_Body,[]).
305		get_identifiers([Sec|Rest],Body,Ids) :-
306		get_opt_section(Sec,Body,Ids1),
307		append(Ids1,IRest,Ids),
308		get_identifiers(Rest,Body,IRest).
309
310		get_opt_sections([],_Body,[]).
311		get_opt_sections([S|Srest],Body,Contents) :-
312		get_opt_section(S,Body,L),append(L,Rest,Contents),
313		get_opt_sections(Srest,Body,Rest).
314
315		get_opt_section(Sec,Body,Result) :-
316		( get_raw_section(Sec,Body,Content) -> Result=Content; Result=[]).
317		get_raw_section(Sec,Body,Content) :- % look for Sec(_Pos,Content) in Body list
318		functor(Pattern,Sec,2),arg(2,Pattern,Content),
319		memberchk(Pattern,Body).
320
321		get_machine(Name,Machines,Type,Header,Refines,Body) :-
322		get_machine1(Name,Machines,_Machine,Type,Header,Refines,Body).
323		%get_raw_machine(Name,Machines,Machine) :-
324		% get_machine1(Name,Machines,Machine,_Type,_Header,_Refines,_Body).
325		get_machine1(Name,Machines,Machine,Type,Header,Refines,Body) :-
326		Header = machine_header(_Pos,Name,_Params),
327	?	member(Machine,Machines),
328		get_machine2(Machine,Type,Header,Refines,Body),!.
329		get_machine2(abstract_machine(_Pos,MS,Header,Body),TypeOfAbstractMachine,Header,[],Body) :-
330		get_abstract_machine_type(MS,TypeOfAbstractMachine).
331		get_machine2(refinement_machine(_Pos,Header,Refines,Body),refinement,Header,[Refines],Body).
332		get_machine2(implementation_machine(_Pos,Header,Refines,Body),implementation,Header,[Refines],Body).
333		get_machine2(generated(_Pos,Machine),A,B,C,D) :-
334		get_machine2(Machine,A,B,C,D).
335		get_machine2(unit_alias(_Pos,_Name,_Alias,Machine),A,B,C,D) :-
336		get_machine2(Machine,A,B,C,D).
337
338		get_raw_machine_name(Machine,Name) :-
339		get_machine2(Machine,_,machine_header(_,Name,_),_,_).
340
341		get_abstract_machine_type(machine(_Pos2),R) :- !,R=abstract_machine.
342		get_abstract_machine_type(system(_Pos2),R) :- !,R=abstract_machine.
343		get_abstract_machine_type(model(_Pos2),R) :- !,R=abstract_model.
344		get_abstract_machine_type(X,R) :- atomic(X),!,
345		add_error(get_abstract_machine_type,'Your parser seems out-dated. Assuming abstract_machine: ',X),
346		R=abstract_machine.
347
348		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
349		% print hierarchy to dot file
350
351		maxlinelength(30).
352
353		:- use_module(tools_io).
354
355		write_dot_hierarchy_to_file(Filename) :-
356		findall(M,machine_type(M,_),Machines),
357		safe_open_file(Filename,write,S,[]),
358		( print_header(S),
359		print_machines(S,1,Machines,Ids),
360		print_refs(S,Ids,Ids),
361		print_footer(S)
362		-> true
363		; add_internal_error('Command failed:',write_dot_hierarchy_to_file(Filename))
364		),
365		close(S).
366
367		print_header(S) :-
368		write(S,'digraph module_hierarchy {\n'),
369		write(S,' graph [page="8.5, 11",ratio=fill,size="7.5,10"];\n').
370		print_footer(S) :-
371		write(S,'}\n').
372
373		print_machines(_S,_Nr,[],[]).
374		print_machines(S,Nr,[M|Machines],[id(M,Nr)|Ids]) :-
375		print_machine(S,Nr,M),
376		Nr2 is Nr + 1,
377		print_machines(S,Nr2,Machines,Ids).
378		print_machine(S,Nr,M) :-
379		write(S,' '),write(S,Nr),
380		(main_machine_name(M) ->
381		write(S,' [shape=record, style=bold, color=darkgreen, label=\"|{')
382		; write(S,' [shape=record, color=steelblue, label=\"|{')),
383		print_machine_header(S,M),
384		machine_identifiers(M,_Params,Sets,AVars,CVars,AConsts,CConsts),
385		%print_hash(S,M),
386		print_sets(S,Sets),
387		print_identifiers(S,'VARIABLES',AVars),
388		print_identifiers(S,'CONCRETE VARIABLES',CVars),
389		print_identifiers(S,'ABSTRACT CONSTANTS',AConsts),
390		print_identifiers(S,'CONSTANTS',CConsts),
391		( machine_has_assertions(M) ->
392		get_specification_description(assertions,AssStr),
393		print_title(S,AssStr)
394		; otherwise -> true),
395		machine_operations(M,Operations),
396		delete(Operations,identifier(_,'INITIALISATION'),Operations2),
397		exclude(is_refinining_event(M),Operations2,RefiningOperations),
398		include(is_refinining_event(M),Operations2,NewOperations),
399		((RefiningOperations=[] ; NewOperations=[])
400		-> get_specification_description(operations,OpStr),
401		print_identifiers(S,OpStr,Operations2)
402		; print_identifiers(S,'EVENTS (refining)',RefiningOperations),
403		print_identifiers(S,'EVENTS (new)',NewOperations)
404		),
405
406		write(S,'}|\"];\n').
407
408		is_refinining_event(M,identifier(_,Event)) :- (refines_event(M,Event,_,_) -> true).
409
410		%print_hash(S,M) :- machine_hash(M,Digest),!,print_title(S,'Digest'),
411		% maplist(format(S,'~16r'),Digest),write(S,'\\n').
412		%print_hash(_S,_M).
413
414		%get_machine_colour(M,steelblue) :- main_machine_name(M),!.
415		%get_machine_colour(_M,steelblue).
416
417		print_machine_header(S,M) :-
418		machine_type(M,Type),
419		get_machine_type(Type,P),
420		write(S,P),write(S,' '),
421		write(S,M),write(S,'\\n').
422		get_machine_type(abstract_machine,'MACHINE').
423		get_machine_type(abstract_model,'MODEL').
424		get_machine_type(refinement,'REFINEMENT').
425		get_machine_type(implementation,'IMPLEMENTATION').
426		get_machine_type(context,'CONTEXT').
427
428		print_sets(_,[]) :- !.
429		print_sets(S,Sets) :-
430		write(S,'|SETS\\n'),
431		print_sets2(Sets,S).
432		print_sets2([],_).
433		print_sets2([Set|Rest],S) :-
434		print_set(Set,S),
435		write(S,'\\n'),
436		print_sets2(Rest,S).
437		print_set(description(_Pos,_Desc,Raw),S) :- print_set(Raw,S).
438		print_set(deferred_set(_Pos,Name),S) :-
439		write(S,Name).
440		print_set(enumerated_set(_Pos,Name,List),S) :-
441		write(S,Name),write(S,' = \\{'),
442		maxlinelength(Max),
443		preferences:get_preference(dot_hierarchy_max_ids,MaxIdsToPrint),
444		print_set_elements(List,S,Max,MaxIdsToPrint),
445		write(S,'\\}').
446		print_set_elements([],_,_,_).
447		print_set_elements([identifier(_Pos,Name)],S,_LenSoFar,_) :-
448		!,write(S,Name).
449		print_set_elements([identifier(_Pos,Name),B|Rest],S,LenSoFar,MaxIdsToPrint) :-
450		dec_atom_length(LenSoFar,Name,NewLen),
451		(NewLen<0 -> maxlinelength(NL0),NL is NL0-1,write(S,'\\n ') ; NL is NewLen-1),
452		write(S,Name),write(S,','),
453		M1 is MaxIdsToPrint-1,
454		(M1 < 1, Rest \= []
455		-> write(S,'...,'),
456		last([B|Rest],Last), print_set_elements([Last],S,NL,M1)
457		; print_set_elements([B|Rest],S,NL,M1)
458		).
459
460
461		dec_atom_length(Prev,Atom,New) :- atom_codes(Atom,Cs), length(Cs,Len),
462		New is Prev-Len.
463
464		print_title(S,Title) :-
465		write(S,'|'),
466		write(S,Title),write(S,'\\n').
467		print_identifiers(_S,_,[]) :- !.
468		print_identifiers(S,Title,List) :-
469		print_title(S,Title),
470		preferences:get_preference(dot_hierarchy_max_ids,MaxIdsToPrint), % how many do we print overall; -1 means print all of them
471		print_identifiers2(List,0,_,S,MaxIdsToPrint).
472		print_identifiers2([],Count,Count,_,_MaxIdsToPrint).
473		print_identifiers2([RawID|Rest],Count,NCount,S,MaxIdsToPrint) :-
474		get_raw_identifier(RawID,Name),
475		(MaxIdsToPrint = 0,Rest\=[]
476		-> length(Rest,Len), RN is Len+1,
477		format(S,' (~w more)',[RN])
478		; MaxIdsToPrint1 is MaxIdsToPrint-1,
479		print_identifier(Name,Count,ICount,S),
480		(Rest = [] -> true; write(S,',')),
481		print_identifiers2(Rest,ICount,NCount,S,MaxIdsToPrint1)
482		).
483		print_identifier(Name,Count,NewCount,S) :-
484		atom_codes(Name,Codes),
485		length(Codes,Length),
486		NewCount1 is Count+Length,
487		maxlinelength(Max),
488		( Count == 0 -> NewCount1=NewCount
489		; NewCount1 =< Max -> NewCount1=NewCount
490		; otherwise -> NewCount=0,write(S,'\\n')),
491		write(S,Name).
492
493		print_refs(_S,[],_).
494		print_refs(S,[id(M,Nr)|Rest],Ids) :-
495		machine_references(M,Refs),
496		print_refs2(Refs,M,Nr,Ids,S),
497		print_refs(S,Rest,Ids).
498		print_refs2([],_,_,_,_).
499		print_refs2([ref(Type,Dest,_Prefix)|Rest],M,Nr,Ids,S) :-
500		member(id(Dest,DestNr),Ids),!,
501		get_ref_type(Type,Ref,Dir), !,
502		(Dir=reverse ->
503		format(S,' ~w -> ~w ~w;~n',[DestNr,Nr,Ref])
504		; format(S,' ~w -> ~w ~w;~n',[Nr,DestNr,Ref])
505		),
506		print_refs2(Rest,M,Nr,Ids,S).
507		get_ref_type(includes,'[label=\"INCLUDES\",color=navyblue]',normal).
508		get_ref_type(imports,'[label=\"IMPORTS\",color=navyblue]',normal).
509		get_ref_type(extends,'[label=\"EXTENDS\",color=navyblue]',normal).
510		get_ref_type(uses,'[label=\"USES\",color=navyblue,style=dashed]',normal).
511		get_ref_type(sees,'[label=\"SEES\",color=navyblue,style=dashed]',normal).
512		%get_ref_type(sees,'[label=\"SEES\",color=navyblue,style=dashed,dir=back]',reverse).
513		%get_ref_type(refines,'[label=\"REFINES\",color=navyblue,style=bold,dir=back]',reverse).
514		get_ref_type(refines,'[label=\"REFINEMENT\",color=navyblue,style=bold]',reverse). % reverse so that abstract machines are shown on top
515		get_ref_type(UNKNOWN,'[label=\"UNKNOWN\",color=navyblue]',normal) :- add_internal_error('Unknown : ',get_ref_type(UNKNOWN,_,_)).
516
517		get_ref_type_name(includes,'INCLUDES').
518		get_ref_type_name(imports,'IMPORTS').
519		get_ref_type_name(extends,'EXTENDS').
520		get_ref_type_name(uses,'USES').
521		get_ref_type_name(sees,'SEES').
522		get_ref_type_name(refines,'REFINEMENT').
523		get_ref_type_name(main,'MACHINE').
524		get_ref_type_name(UNKNOWN,UNKNOWN).
525		/************************************************************************/
526		/* The same for Event-B */
527		/************************************************************************/
528
529		analyse_eventb_hierarchy(Machines,Contextes) :-
530		reset_hierarchy,
531		get_eventb_name(Machines,Contextes,MainName),
532		assert(main_machine_name(MainName)),
533		maplist(analyse_eventb_machine,Machines),
534		analyse_eventb_refinement_types(Machines),
535		maplist(analyse_eventb_context,Contextes),!.
536		analyse_eventb_hierarchy(Machines,Contextes) :-
537		add_internal_error('Analyzing Event-B Hierarchy Failed: ',analyse_eventb_hierarchy(Machines,Contextes)).
538
539		get_eventb_name([MainMachine|_AbstractMachines],_Contextes,Name) :-
540		event_b_model(MainMachine,Name,_),!.
541		get_eventb_name(_Machines,[MainContext|_AbstractContextes],Name) :-
542		event_b_context(MainContext,Name,_).
543
544		event_b_model(event_b_model(_,Name,Sections),Name,Sections).
545		event_b_context(event_b_context(_,Name,Sections),Name,Sections).
546
547		analyse_eventb_machine(Machine) :-
548		event_b_model(Machine,Name,Sections),
549		%print(analyzing(Name)),nl,
550		( memberchk(refines(_,RName),Sections) -> Type=refinement, RRefs=[ref(refines,RName,'')]
551		; otherwise -> Type=abstract_model, RRefs=[], RName='$none'),
552		get_identifiers([variables],Sections,Vars),
553		get_sees_refs(Sections,SRefs),append(RRefs,SRefs,Refs),
554		get_events(Name,Sections,Events,RName),
555		raw_sha_hash(Machine,Digest),
556		assert(machine_type(Name,Type)),
557		assert(machine_identifiers(Name,[],[],Vars,[],[],[])),
558		assert(machine_references(Name,Refs)),
559		assert(machine_operations(Name,Events)),
560		assert_if_has_theorems(Name,Sections),
561		assert(machine_hash(Name,Digest)).
562
563		% analyze which kinds of refinments we have between events
564		analyse_eventb_refinement_types([]).
565		analyse_eventb_refinement_types([RefMachine,AbsMachine|_]) :-
566		event_b_model(RefMachine,RefName,RefSections),
567		memberchk(refines(_,AbsName),RefSections),
568		event_b_model(AbsMachine,AbsName,AbsSections),
569		get_opt_section(events,RefSections,RawEvents),
570		get_opt_section(events,AbsSections,AbsRawEvents),
571		member(RawEvent,RawEvents),
572		bmachine_eventb:raw_event(RawEvent,_,RefEvName,_St1,Ref,_Prm1,RefGrd,_Thm1,RefAct,_Wit1),
573		Ref = [AbsEvName],
574		member(AbsRawEvent,AbsRawEvents),
575		bmachine_eventb:raw_event(AbsRawEvent,_,AbsEvName,_St2,_,_Prm2,AbsGrd,_Thm2,AbsAct,_Wit2),
576		check_raw_prefix(AbsGrd,RefGrd,SameGuard),
577		check_raw_prefix(AbsAct,RefAct,SameAct),
578		%% format('~nEvent refinement change ~w (~w) -> ~w (~w) guard: ~w, action: ~w~n',[RefEvName,RefName,AbsEvName,AbsName,SameGuard,SameAct]),
579		%print(rawgrd(RefGrd,AbsGrd)), nl, print(rawact(RefAct,AbsAct)),nl,
580		assert(event_refinement_change(RefName,RefEvName,AbsName,AbsEvName,SameGuard,SameAct)),
581		fail.
582		analyse_eventb_refinement_types([_|T]) :- analyse_eventb_refinement_types(T).
583
584		check_raw_prefix([],[],Res) :- !, Res=unchanged.
585		check_raw_prefix([],[_|_],Res) :- !, Res=extends. % the refinement has some more actions/guards
586		check_raw_prefix([Abs|AT],[Ref|RT],Result) :- same_raw_expression(Abs,Ref),!,
587		check_raw_prefix(AT,RT,Result).
588		check_raw_prefix(_,_,refines).
589
590		% TO DO: check if we have a more complete version of this predicate; to do: handle @desc description/3 terms
591		same_raw_expression(identifier(_,A),RHS) :- !, RHS=identifier(_,B), A=B.
592		same_raw_expression(equal(_,A,B),RHS) :- !, RHS=equal(_,A2,B2), same_raw_expression(A,A2), same_raw_expression(B,B2).
593		same_raw_expression(assign(_,A1,A2),RHS) :- !, RHS=assign(_,B1,B2),
594		maplist(same_raw_expression,A1,B1), maplist(same_raw_expression,A2,B2).
595		same_raw_expression(A,B) :- atomic(A),!, A=B.
596		same_raw_expression(A,B) :- A =.. [F,_|AA], % print(match(F,AA)),nl,
597		B=.. [F,_|BB], maplist(same_raw_expression,AA,BB).
598
599
600
601		get_sees_refs(Sections,SRefs) :-
602		get_opt_section(sees,Sections,Seen),
603		findall(ref(sees,I,''),member(I,Seen),SRefs).
604
605		:- use_module(bmachine_eventb,[raw_event/10]).
606		get_events(Name,Sections,Events,AbsMachineName) :-
607		get_opt_section(events,Sections,RawEvents),
608		compute_event_refines(Name,RawEvents,AbsMachineName),
609		findall( identifier(Pos,EvName),
610		( member(RawEvent,RawEvents),
611		raw_event(RawEvent,Pos,EvName,_St,_Rf,_Prm,_Grd,_Thm,_Act,_Wit) ),
612		Events).
613
614		% TO DO: detect when an event extends another one without changing it
615		compute_event_refines(MachineName,RawEvents,AbsMachineName) :-
616		member(RawEvent,RawEvents),
617		bmachine_eventb:raw_event(RawEvent,_Pos,EvName,_St,Refines,_Prm,_Grd,_Thm,_Act,_Wit),
618		member(RefEvent,Refines),
619		% print(refines(MachineName,EvName,AbsMachineName,RefEvent)),nl,
620		assert(refines_event(MachineName,EvName,AbsMachineName,RefEvent)),
621		fail.
622		compute_event_refines(_,_,_).
623
624
625		% try and get the name of the machine we refine
626		%machine_refines(Machine,AbsMachine) :- machine_references(Machine,Refs), member(ref(refines,AbsMachine,_),Refs).
627
628		analyse_eventb_context(Context) :-
629		event_b_context(Context,Name,Sections),
630		get_identifiers([constants],Sections,ConcreteConstants),
631		get_identifiers([abstract_constants],Sections,AbstractConstants),
632		append([ConcreteConstants,AbstractConstants],AllConstants),
633		get_sets(Sections,Sets),
634		get_extends_refs(Sections,Refs),
635		raw_sha_hash(Context,Digest),
636		assert(machine_type(Name,context)),
637		assert(machine_identifiers(Name,[],Sets,[],[],[],AllConstants)),
638		assert(machine_references(Name,Refs)),
639		assert(machine_operations(Name,[])),
640		maplist(assert_raw_id_with_position(concrete_constant),ConcreteConstants),
641		maplist(assert_raw_id_with_position(abstract_constant),AbstractConstants),
642		assert_if_has_theorems(Name,Sections),
643		assert(machine_hash(Name,Digest)).
644
645		get_extends_refs(Sections,Refs) :-
646		get_opt_section(extends,Sections,Extended),
647		findall(ref(extends,E,''),member(E,Extended),Refs).
648
649		assert_if_has_theorems(Name,Sections) :-
650		get_opt_section(theorems,Sections,[_|_]),
651		assert(machine_has_assertions(Name)).
652		assert_if_has_theorems(_Name,_Sections).
653
654
655		% compute a hash based on constants and properties
656		properties_hash(MachineName,Hash) :-
657		properties_hash_cached(MachineName,Hash1),!,
658		Hash=Hash1.
659		properties_hash(MachineName,Hash) :-
660		compute_properties_hash(MachineName,Hash1),
661		assert(properties_hash_cached(MachineName,Hash1)),
662		Hash=Hash1.
663		compute_properties_hash(Name,Hash) :-
664		raw_machine(Name,Machine),
665		get_machine(Name,[Machine],_Type,_Header,_Refines,Body),
666		extract_sorted_np_sets(Body,Sets),
667		extract_sorted_np_constants(Body,Constants),
668		extract_np_properties(Body,Properties),
669		extract_used_np_definitions_from_properties(Body,Definitions),
670		ToHash = [Sets,Constants,Properties,Definitions],
671		raw_sha_hash(ToHash,Hash).
672		% save_properties_hash(Name,ToHash,Hash).
673
674		extract_sorted_np_sets(Body,Sets) :-
675		get_sets(Body,PosSets),
676		remove_raw_position_info(PosSets,UnsortedSets),
677		sort(UnsortedSets,Sets).
678		extract_sorted_np_constants(Body,Constants) :-
679		get_opt_sections([constants,concrete_constants,abstract_constants],Body,PosConstants),
680		remove_raw_position_info(PosConstants,UnsortedConstants),
681		sort(UnsortedConstants,Constants).
682		extract_np_properties(Body,Properties) :-
683		get_opt_section(properties,Body,PosProperties),
684		remove_raw_position_info(PosProperties,Properties).
685		extract_used_np_definitions_from_properties(Body,Definitions) :-
686		get_opt_section(properties,Body,Properties),
687		extract_used_np_definitions(Properties,Body,Definitions).
688		extract_used_np_definitions(RawSyntax,Body,Definitions) :-
689		extract_raw_identifiers(RawSyntax,UsedIds),
690		all_definition_ids(Body,AllDefs),
691		ord_intersection(UsedIds,AllDefs,UsedDefNames),
692		transitive_used_definitions(UsedDefNames,AllUsedDefs),
693		findall( definition(none,Name,Args,DefBody),
694		( member(Name,AllUsedDefs),b_get_definition(Name,_DefType,Args,DefBody,_Deps)),
695		PosDefinitions),
696		maplist(remove_raw_position_info,PosDefinitions,Definitions).
697		all_definition_ids(Body,Ids) :-
698		get_opt_section(definitions,Body,Definitions),
699		convlist(get_definition_name,Definitions,Ids1),
700		sort(Ids1,Ids).
701		transitive_used_definitions(Defs,TransDefs) :-
702		findall( D, reachable_definition(Defs,D), TD1),
703		sort(TD1,TransDefs).
704		reachable_definition(Defs,D) :-
705		member(N,Defs),
706		( D=N
707		; b_get_definition(N,_DefType,_Args,_Body,Deps),
708		reachable_definition(Deps,D)).
709
710
711		/* just for debugging:
712		save_properties_hash(MachineName,ToHash,Hash) :-
713		main_machine_name(Main),
714		open('/home/plagge/hashes.pl',append,S),
715		writeq(S,hash(Main,MachineName,ToHash,Hash)),
716		write(S,'.\n'),
717		close(S).
718		*/
719
720		% ---------------------------
721		:- dynamic event_info/3.
722		analyze_extends_relation :-
723		retractall(event_info(_,_,_)),
724		bmachine:b_get_machine_operation(_Name,_Results,_RealParameters,TBody,_OType,_OpPos),
725		treat_event_body(TBody),fail.
726		analyze_extends_relation.
727
728		treat_event_body(TBody) :-
729		rlevent_info(TBody,EventName,Machine,Status,AbstractEvents),
730		% format('Event ~w:~w ~w~n',[Machine,EventName,Status]),
731		assert(event_info(Machine,EventName,Status)),
732		maplist(treat_event_body,AbstractEvents).
733
734		:- use_module(bsyntaxtree,[get_texpr_expr/2]).
735		rlevent_info(TBody,EventName,Machine,FStatus,AbstractEvents) :-
736		get_texpr_expr(TBody,Event),
737		Event = rlevent(EventName,Machine,TStatus,_Params,_Guard,_Theorems,_Actions,_VWit,_PWit,_Unmod,AbstractEvents),
738		bsyntaxtree:get_texpr_expr(TStatus,Status), %ordinary, convergent, anticipated
739		functor(Status,FStatus,_).
740
741
742		% write the event refinement hierarchy to a dot file
743		% (currently) only makes sense for Event-B models
744
745		:- use_module(dot_graph_generator,[gen_dot_graph/7]).
746		:- use_module(preferences,[get_preference/2]).
747		:- use_module(tools_strings,[ajoin/2]).
748
749		:- public dot_event_node/6.
750		dot_event_node(M:Ev,M,Desc,Shape,Style,Color) :-
751		machine_operations(M,Evs),
752		raw_identifier_member(Ev,Evs),
753		Ev \= 'INITIALISATION',
754		event_info(M,Ev,Status),
755		(event_refinement_change(M,Ev,_,_,SameGuard,SameAction)
756		-> true ; SameGuard=unknown, SameAction=unknown),
757		(Status = convergent -> ajoin([Ev,' (<)'],Desc)
758		; Status = anticipated -> ajoin([Ev, '(<=)'],Desc)
759		; otherwise -> Desc=Ev),
760		dot_get_color_style(M,Ev,Status,SameGuard,SameAction,Shape,Color,Style).
761
762		dot_get_color_style(M,Ev,_Status,_,_,box,Color,Style) :- \+ refines_event(M,Ev,_,_),!,
763		get_preference(dot_event_hierarchy_new_event_colour,Color), Style=none.
764		dot_get_color_style(M,Ev,_,SameGuard,SameAction,box,Color,Style) :-
765		refines_event(M,Ev,_,Ev2), dif(Ev2,Ev),!, % changes name
766		((SameGuard,SameAction)=(unchanged,unchanged)
767		-> get_preference(dot_event_hierarchy_rename_unchanged_event_colour,Color)
768		; get_preference(dot_event_hierarchy_rename_event_colour,Color)), Style=filled.
769		dot_get_color_style(_M,_Ev,_,unchanged,unchanged,box,Color,Style) :- % keeps name and adds no guard or action
770		!,
771		get_preference(dot_event_hierarchy_unchanged_event_colour,Color), Style=filled.
772		dot_get_color_style(_M,_Ev,_,_,unchanged,box,Color,Style) :- % keeps name and adds no guard or action
773		!,
774		get_preference(dot_event_hierarchy_grd_strengthening_event_colour,Color), Style=filled.
775		dot_get_color_style(_M,_Ev,_,unchanged,_,box,Color,Style) :- % keeps name and adds action but keeps guard action
776		!,
777		get_preference(dot_event_hierarchy_grd_keeping_event_colour,Color), Style=filled.
778		dot_get_color_style(_M,_Ev,_,_,_,box,Color,Style) :- % keeps name but adds or modifies
779		% TO DO: distinguish extends from refines
780		get_preference(dot_event_hierarchy_refines_colour,Color), Style=filled.
781
782		:- public dot_refines_event/5.
783		dot_refines_event(M2:Ev2,Label,M1:Ev1,Color,Style) :-
784		Label = '', % TO DO: detect refine, extends, identical
785		refines_event(M1,Ev1,M2,Ev2),
786		Ev1 \= 'INITIALISATION',
787		(event_refinement_change(M1,Ev1,_,_,SameGuard,SameAct)
788		-> arrow_style(SameGuard,SameAct,Style,ColPref), get_preference(ColPref,Color)
789		; Style=solid, Color=red % should not happen
790		).
791
792		arrow_style(unchanged,unchanged,Style,ColPref) :- !,
793		Style=arrowhead(none,solid), ColPref=dot_event_hierarchy_extends_colour.
794		arrow_style(refines,_,Style,ColPref) :- !, Style=solid, ColPref=dot_event_hierarchy_edge_colour.
795		arrow_style(_,refines,Style,ColPref) :- !, Style=solid, ColPref=dot_event_hierarchy_edge_colour.
796		%arrow_style(_,_,Style) :- Style = arrowhead(vee,arrowtail(box,solid)). % we have extends
797		arrow_style(_,_,Style,dot_event_hierarchy_extends_colour) :- Style = arrowhead(vee,solid). % we have extends
798
799		:- public dot_subgraph/3.
800		dot_subgraph(M,filled,Colour) :- get_preference(dot_event_hierarchy_machine_colour,Colour),
801		machine_operations(M,[_|_]).
802
803		:- public dot_same_rank/1.
804		dot_same_rank(SameRankVals) :- machine_operations(M,Evs),
805		findall(M:Ev,raw_identifier_member(Ev,Evs),SameRankVals).
806
807		write_dot_event_hierarchy_to_file(File) :-
808		analyze_extends_relation,
809		(get_preference(dot_event_hierarchy_horizontal,true) -> PageOpts=[horizontal] ; PageOpts=[]),
810		gen_dot_graph(File,PageOpts,b_machine_hierarchy,dot_event_node,dot_refines_event,none,dot_subgraph).
811		%gen_dot_graph(File,b_machine_hierarchy,dot_event_node,dot_refines_event,dot_same_rank,dot_subgraph).