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). |