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