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