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