1		% (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4		% Flow analysis
5		% Filename: flow.pl
6
7		:- module(flow, [create_enable_graph/1, create_enable_graphs/1, reset_flow/0, print_base_guide/1,print_event_guide/2]).
8
9		:- use_module(tools).
10		:- use_module(self_check).
11
12		:- use_module(module_information,[module_info/2]).
13		:- module_info(group,experimental).
14		:- module_info(description,'Flow Analysis for Event-B models. Extracts a flow graph from a model.').
15
16		:- use_module(library(lists)).
17		:- use_module(library(ordsets)).
18
19		:-use_module(bmachine,[b_top_level_operation/1,b_get_invariant_from_machine/1,wp_untyped/3,clear_wp/0,nonchanging_guard/2]).
20		:-use_module(bsyntaxtree).
21
22		:- use_module(translate, [translate_bexpression/2]).
23
24		:- dynamic eventnumber/2.
25		:- dynamic guide_wp/3.
26		:- dynamic wp_typed/3, event_wp/3.
27
28		:- use_module(error_manager).
29		:- use_module(bmachine,[typecheck_predicates/4]).
30
31		add_wp(S,D,TypedPred) :-
32		assert( wp_typed(S,D,TypedPred) ).
33		update_typed_wp :-
34		retract( wp_untyped(S,D,P) ),
35		bmachine:typecheck_predicates(P,TypedPred,S,D),
36		add_wp(S,D,TypedPred),
37		fail.
38		update_typed_wp.
39
40		wp(S,D,TypedPred) :-
41		update_typed_wp,
42		wp_typed(S,D,TypedPred).
43
44		% ---------------------------------- Interface
45
46		:- meta_predicate print_single_enable_graph(*,3).
47		:- meta_predicate print_single_enable_graph(*,3,*).
48
49		create_enable_graph(X):- build_enable_graph,
50		print_single_enable_graph(X,wp).
51
52		create_enable_graphs(X):- build_enable_graph,
53		print_multiple_enable_graphs(X).
54
55		print_base_guide(X) :- build_enable_graph,
56		print_single_enable_graph(X,guide_wp).
57
58		print_event_guide(X,E) :- build_enable_graph,
59		retractall(event_wp(_,_,_)),
60		build_guide(E,N),
61		print_single_enable_graph(X,event_wp,N).
62
63
64		reset_flow :- retractall(done_flow(_)), retractall(guide_wp(_,_,_)).
65
66		:- use_module(eventhandling,[register_event_listener/3]).
67		:- register_event_listener(clear_specification,reset_flow,
68		'Reset flow analysis.').
69
70		:- public backward_analysis/1. % still useful ??
71		backward_analysis(Event) :- build_enable_graph,
72		print_flow_automaton(Event).
73
74		% -------------------------------- Flow Automaton
75
76		print_flow_automaton(E) :- calculate_flow_automaton([E],[],X), print(X), nl.
77
78		calculate_flow_automaton([],A,A).
79		calculate_flow_automaton([H|T],A,R) :- findall((S,P),(wp(S,H,P), \+false_predicate(P)),L), append(L,A,NA), calculate_flow_automaton(T,NA,R).
80
81
82		% -------------------------------- Enable Graph
83
84
85
86		:- dynamic done_flow/1.
87
88		build_enable_graph :- (done_flow(enable_graph) -> true;
89		((print('Computing enable_graph'),nl,
90		enumerate_events,
91		prepare_input,
92		find_contradictions,
93		add_init_edges,
94		law_of_motion,
95		build_base_guide,
96		print('Done'),nl)
97		-> assert(done_flow(enable_graph))
98		; add_error(flow,'Could not build enable_graph'),fail)).
99
100		print_single_enable_graph(File,NameEdges) :- events(Nodes), print_single_enable_graph(File,NameEdges,Nodes).
101
102		print_single_enable_graph(File,NameEdges,Nodes) :-
103		print(writing_to_dot_file(File)),nl,
104		tell(File),
105		dot_header('EnableGraph'),
106		dot_node(Nodes),
107		findall((S,D,P), call(NameEdges,S,D,P),WL),
108		dot_edge(WL),
109		dot_footer,
110		told,
111		print(closing(File)),nl.
112
113		print_multiple_enable_graphs(File) :-
114		print(writing_to_dot_file(File)),nl,
115		tell(File),
116		dot_header('EnableGraphs'), print('rankdir=LR'),nl, events(L), dot_node(L), print_subgraph(L),
117		dot_footer, told,
118		print(closing(File)),nl.
119
120		print_subgraph([]).
121		print_subgraph([H|T]) :- findall((H,D,P), wp(H,D,P),WL),
122		print_edges(WL),
123		print_subgraph(T).
124
125		% -------------------------------- Prepare Input / Normalize
126
127		prepare_input :- statistics(runtime,_),
128		normalize_inv,
129		normalize_wp,
130		statistics(runtime,[_,T2]), print(normalizing(T2)),nl.
131
132		normalize_wp :- findall((S,D,P), wp(S,D,P), L), clear_wp, normalize_wps(L).
133
134		normalize_wps([]).
135		normalize_wps([(S,D,P)|T]) :- conjunct_predicates(P,P3),conjunction_to_list(P3,P2),normalize_list(P2,R), add_wp(S,D,R), normalize_wps(T).
136
137
138		normalize_inv :- b_get_invariant_from_machine(Invariant),
139		conjunction_to_list(Invariant,L),
140		normalize_invs(L).
141		normalize_invs([]).
142		normalize_invs([H|T]) :- translate_bexpression(H,HP),
143		print(normalizing_inv(HP)),nl, normalize(H,HX), get_texpr_expr(HX,HR),
144		((HR =.. [Op,X,Y] ,keep(Op)) -> assert_pred_inv(X,Op,Y);true),
145		normalize_invs(T).
146
147		normalize_guards(E) :- findall((E,X),nonchanging_guard(E,X), L),
148		print(mormalizing_grd(E,L)),nl,
149		normalize_guards2(L).
150
151		normalize_guards2([]).
152		normalize_guards2([(E,P)|T]) :- normalize_list(P,R), assert_guards(R,E), normalize_guards2(T).
153
154		assert_guards([],_).
155		assert_guards([H|T],E) :- get_texpr_expr(H,truth),!, assert_guards(T,E).
156		assert_guards([H|T],E) :- get_texpr_expr(H,HR),
157		HR =.. [Op,X,Y],!, (keep(Op) -> assert_pred_guard(Op,X,Y);true), assert_guards(T,E).
158		assert_guards([H|_],_) :- add_error(flow,'Cannot normalize: ',H),fail.
159
160		% ------------------------------ Normalizer
161
162		normalize(TExpr,TNExpr) :- remove_bt(TExpr,Expr,NExpr,TNExpr), normalize2(Expr,NExpr).
163
164		normalize2(not_equal(X,boolean_true),equal(X,boolean_false)) :- !.
165		normalize2(not_equal(X,boolean_false),equal(X,boolean_true)) :- !.
166		normalize2(negation(TExpr),R) :- !,
167		remove_bt(TExpr,Expr,NExpr,_), negate_boolean_expression(Expr,NExpr), normalize2(NExpr,R).
168		normalize2(TExpr, R) :-
169		syntaxtransformation(TExpr,TSubExpr,_,TNSubExpr,R),!, normalize_list(TSubExpr, TNSubExpr).
170		normalize2(TExpr,_) :- add_error(flow,'Unknown expression in normalize2: ',TExpr),fail.
171
172		normalize_list([],R) :- !,R=[].
173		normalize_list([H|T],[HR|TR]) :- !, normalize(H,HR),normalize_list(T,TR).
174		normalize_list(A,B) :- add_error(flow,'Illegal arguments in normalize_list: ',(A,B)),fail.
175
176		/** keep is used to specify which invariants shall be kept
177		(we keep only those parts that can be handled by the builtin prover) */
178		keep(boolean_false).
179		keep(boolean_true).
180		keep(equal).
181		keep(not_equal).
182		keep(member).
183		keep(not_member).
184		keep(less).
185		keep(greater).
186		keep(less_equal).
187		keep(greater_equal).
188
189		negate_boolean_expression(A,B) :-
190		if(neg(A,B),true, add_error_fail(flow,'Unknown operator in negate: ',neg(A,B))).
191
192
193		neg(boolean_true,boolean_false).
194		neg(boolean_false,boolean_true).
195		neg(equal(X,Y),not_equal(X,Y)).
196		neg(not_equal(X,Y),equal(X,Y)).
197		neg(equal(X,Y),not_equal(X,Y)).
198		neg(member(X,Y),not_member(X,Y)).
199		neg(not_member(X,Y),member(X,Y)).
200		neg(less(X,Y),greater_equal(X,Y)).
201		neg(less_equal(X,Y),greater(X,Y)).
202		neg(greater_equal(X,Y),less(X,Y)).
203		neg(greater(X,Y),less_equal(X,Y)).
204		neg(subset_strict(X,Y),not_subset_strict(X,Y)).
205		neg(not_subset_strict(X,Y),subset_strict(X,Y)).
206		neg(subset(X,Y),not_subset(X,Y)).
207		neg(not_subset(X,Y),subset(X,Y)).
208
209
210		:- assert_must_succeed((flow:neg(boolean_true, boolean_false))).
211		:- assert_must_succeed((flow:neg(boolean_false, boolean_true))).
212
213		:- assert_must_succeed((flow:neg(equal(1,3), not_equal(1,3)))).
214		:- assert_must_succeed((flow:neg(not_equal(1,3), equal(1,3)))).
215
216		:- assert_must_succeed((flow:neg(member(1,{2}), not_member(1,{2})))).
217		:- assert_must_succeed((flow:neg(not_member(1,{2}), member(1,{2})))).
218
219		:- assert_must_succeed((flow:neg(greater(1,2), less_equal(1,2)))).
220		:- assert_must_succeed((flow:neg(greater_equal(1,2), less(1,2)))).
221		:- assert_must_succeed((flow:neg(less(1,2), greater_equal(1,2)))).
222		:- assert_must_succeed((flow:neg(less_equal(1,2), greater(1,2)))).
223
224		:- assert_must_succeed((flow:neg(not_subset_strict(foo,bar), subset_strict(foo,bar)))).
225		:- assert_must_succeed((flow:neg(subset_strict(foo,bar), not_subset_strict(foo,bar)))).
226		:- assert_must_succeed((flow:neg(subset(foo,bar), not_subset(foo,bar)))).
227		:- assert_must_succeed((flow:neg(not_subset(foo,bar), subset(foo,bar)))).
228
229
230		% -------------------------------- Init Edges
231		add_init_edges :- events(L), add_init_edges(L).
232		add_init_edges([]).
233		add_init_edges(['INITIALISATION'|T]) :- !, add_init_edges(T).
234		add_init_edges([H|T]) :- H\='INITIALISATION',(wp('INITIALISATION',H,_)->true;add_wp('INITIALISATION',H,[])),add_init_edges(T).
235
236		% -------------------------------- Law of motion
237		law_of_motion :- events(L), law_of_motion(L).
238		law_of_motion([]).
239		law_of_motion(['INITIALISATION'|T]) :- !, law_of_motion(T).
240		law_of_motion([H|T]) :- H\='INITIALISATION',(wp(H,H,_)->true;add_wp(H,H,[])),law_of_motion(T).
241
242
243		% -------------------------------- Base Guiding Automaton
244
245		build_base_guide :- findall((S,D,P),wp(S,D,P),L), build_base_guide(L).
246		build_base_guide([]).
247		build_base_guide([(S,D,P)|T]) :- (false_predicate(P) -> true; assert(guide_wp(S,D,P))), build_base_guide(T).
248
249		build_guide(E,RV) :- guide_dfs([E],RV), retractall(event_wp(_,_,_)),filter_from_guide(RV).
250
251		guide_dfs(Stack, Visited) :- guide_dfs(Stack,[],Visited).
252
253		guide_dfs([],SeenSoFar,SeenSoFar).
254		guide_dfs([Event|Tail],SeenSoFar,Visited) :- member(Event,SeenSoFar),!, guide_dfs(Tail,SeenSoFar,Visited). % ignore!
255		guide_dfs([Event|Tail],SeenSoFar,Visited) :- findall(S,guide_wp(S,Event,_),L), append(L,Tail,Todo), guide_dfs(Todo,[Event|SeenSoFar],Visited).
256
257
258		filter_from_guide(V) :- guide_wp(S,D,P), member(S,V), member(D,V), assert(event_wp(S,D,P)), fail.
259		filter_from_guide(_).
260
261
262		% -------------------------------- Flow Graph
263
264
265
266
267
268		% --------------------------------- Prover
269		:- dynamic pred_grd/3, pred_new/3.
270		:- dynamic pred_guard/3.
271		:- dynamic pred_inv/3.
272		:- dynamic change/0.
273		:- dynamic inconsistent/0.
274		%:- dynamic trans/3.
275
276		false_predicate([b(boolean_false,boolean,[nodeid(none)])]).
277
278		find_contradictions :- findall((S,D,P), wp(S,D,P), L), clear_wp, find_contradictions(L).
279
280		find_contradictions([]).
281		find_contradictions([(S,D,P)|T]) :- retractall(inconsistent),
282		retractall(pred_grd(_,_,_)),
283		retractall(pred_new(_,_,_)),
284		retractall(pred_guard(_,_,_)),
285		normalize_guards(S),
286		find_contradictions2(P),
287		(inconsistent -> false_predicate(F), add_wp(S,D,F)
288		; otherwise -> (simplify(P,PR), add_wp(S,D,PR))),
289		find_contradictions(T).
290
291		find_contradictions2([]).
292		find_contradictions2([H|_]) :- get_texpr_expr(H,boolean_false), !, assert(inconsistent).
293		find_contradictions2([H|T]) :- get_texpr_expr(H,HR), (HR =.. [Op,X,Y] -> assert_pred(Op,X,Y); true), (\+inconsistent -> huelle, find_contradictions2(T);true).
294
295
296		huelle :- pred(Op,X,Y),pred(Op2,Y,Z), combine(Op,Op2,Op3),
297		assert_pred(Op3,X,Z),fail.
298		huelle :- (retract(change) -> huelle2 ; true).
299
300		huelle2 :- retract(pred_new(X,Op,Y)), huelle2(X,Op,Y).
301		huelle2 :- (retract(change) -> huelle2 ; true).
302
303		huelle2(X,Op,Y) :- pred(Op2,Y,Z), combine(Op,Op2,Op3), assert_pred(Op3,X,Z),fail.
304		huelle2(Y,Op,Z) :- pred(Op2,X,Y), combine(Op2,Op,Op3), assert_pred(Op3,X,Z),fail.
305
306		assert_pred(Op,X,Y) :- %print(try(Op,X,Y)),nl,
307		pred(Op,X,Y) -> true
308		; (assert(pred_grd(X,Op,Y)), %print(pred_grd(Op,X,Y)),nl,
309		assert(pred_new(X,Op,Y)),
310		(change -> true ; assert(change)),
311
312		%nl,print(check_inconsistent(Op,X,Y)),nl,
313
314		(inconsistent_fact(Op,X,Y) -> (assert(inconsistent), print('INCONSISTENT'), nl) ; true),
315		((sym(Op),X\=Y)
316		-> assert(pred_grd(Y,Op,X)), assert(pred_new(X,Op,Y)) ; true)).
317
318		assert_pred_inv(Op,Y,Z) :-
319		pred_inv(Y,Op,Z) -> true
320		; assert(pred_inv(Y,Op,Z)),
321		((sym(Op),Z\=Y) -> assert(pred_inv(Z,Op,Y)) ; true).
322		assert_pred_guard(Op,Y,Z) :-
323		pred_guard(Y,Op,Z) -> true
324		; assert(pred_guard(Y,Op,Z)),
325		((sym(Op),Z\=Y) -> assert(pred_guard(Z,Op,Y)) ; true).
326
327		pred(Op,Y,Z) :- pred_grd(Y,Op,Z).
328		pred(Op,Y,Z) :- pred_inv(Y,Op,Z).
329		pred(Op,Y,Z) :- pred_guard(Y,Op,Z).
330
331		inconsistent_fact(not_equal,X,X).
332		inconsistent_fact(less,X,X).
333		inconsistent_fact(greater,X,X).
334		inconsistent_fact(equal,X,Y) :- value(X), value(Y), X \= Y.
335		inconsistent_fact(subset_strict,X,X).
336		inconsistent_fact(member,_,empty_set).
337
338		:- assert_must_succeed((flow:inconsistent_fact(not_equal,4,4))).
339		:- assert_must_succeed((flow:inconsistent_fact(less,4,4))).
340		:- assert_must_succeed((flow:inconsistent_fact(subset_strict,{4},{4}))).
341		:- assert_must_succeed((flow:inconsistent_fact(member,4,empty_set))).
342
343		:- assert_must_succeed((flow:value2(4))).
344		:- assert_must_succeed((flow:value2(boolean_false))).
345		:- assert_must_succeed((flow:value2(boolean_true))).
346		:- assert_must_succeed((flow:value2(integer(_,7)))).
347
348		value(X) :- get_texpr_expr(X,Y), value2(Y).
349
350		value2(X) :- number(X).
351		value2(boolean_false).
352		value2(boolean_true).
353		value2(integer(_,_)).
354
355		sym(equal).
356		sym(not_equal).
357
358		combine(equal,X,X).
359		combine(less_equal,less,less).
360		combine(less_equal,less_equal,less_equal).
361		combine(less,less,less).
362		combine(greater,greater,greater).
363		combine(greater_equal,greater,greater).
364		combine(greater_equal,greater_equal,greater_equal).
365		combine(subset_strict,subset_strict,subset_strict).
366
367		% ------------------------------ Simplifier
368
369		simplify([],[]).
370		simplify([H|T],R) :- (member(H,T) -> R=RT; %remove duplicates
371		otherwise -> (tautology(H) -> R=RT; %remove tautologies
372		otherwise -> R=[H|RT])),
373		simplify(T,RT).
374
375		tautology(X) :- get_texpr_expr(X,Y), tautology2(Y).
376
377		tautology2(boolean_true).
378		tautology2(equal(A,A)).
379		tautology2(subset(A,A)).
380		tautology2(less_equal(A,A)).
381		tautology2(greater_equal(A,A)).
382
383
384		% -------------------------------- Helper
385		:- dynamic count/1.
386		reset_count :- retractall(count(_)), assert(count(0)).
387		inc :- count(X), retract(count(_)), X1 is X+1, assert(count(X1)).
388
389		print_edges([]).
390		print_edges([(S,D,P)|T]) :- print_node(S,D,C,X), format_edge(C,X,P), print_edges(T).
391
392		print_node(S,D,C,X) :- eventnumber(S,C), count(X), inc, format_node(X,D).
393
394		enumerate_events :- reset_count, events(L), enumerate_events(L).
395		enumerate_events([]).
396		enumerate_events([S|T]) :- count(C), assert(eventnumber(S,C)), inc, enumerate_events(T).
397
398		events(['INITIALISATION'|L]) :- findall(OperationName, b_top_level_operation(OperationName), L).
399
400		dot_header(Name) :- print('digraph '), print(Name),print(' {'),nl.
401
402		dot_node([]).
403		dot_node([S|T]) :- eventnumber(S,C), format_node(C,S), dot_node(T).
404
405		format_node(Number,Text) :- print(Number), print(' '), print('[label="'), print(Text), print('"]'),nl.
406
407		dot_edge([]).
408		dot_edge([(S,D,P)|T]) :- eventnumber(S,SN), eventnumber(D,DN), format_edge(SN,DN,P), dot_edge(T).
409
410		format_edge(FromNumber,ToNumber,[]) :- format_edge2(FromNumber,ToNumber, green).
411		format_edge(FromNumber,ToNumber,F) :- false_predicate(F),!,format_edge2(FromNumber,ToNumber, red).
412		format_edge(FromNumber, ToNumber, LP) :- conjunct_predicates(LP,P),translate_bexpression(P,Label), print(FromNumber), print('->'), print(ToNumber), print(' '), print('[label="'), print(Label), print('"]') ,nl.
413
414		format_edge2(FromNumber, ToNumber, green) :- print(FromNumber), print('->'), print(ToNumber), print(' '), print('[color="forestgreen" label=true]') ,nl.
415		format_edge2(FromNumber, ToNumber, red) :- print(FromNumber), print('->'), print(ToNumber), print(' '), print('[color="crimson" label=false]') ,nl.
416
417		dot_footer :- print('}').
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456		% ---------------------------------- Main Program
457
458
459		% build_flow_graph:- (open(State) -> (process(State,State), retract(open(State)), count(C), inc, assert(node(State,C)), build_flow_graph);
460		% otherwise -> true).
461
462
463		% process([],_).
464		% process([H|T],State) :- findall((D,P),trans(H,D,P),L), add_edges(L,State),
465		% process(T,State).
466
467		%join_nonchanging(X,OS,NS) :- list_to_ord_set(X,OX),no_effect(X,NE),list_to_ord_set(NE,ONE), ord_intersection(OX,ONE,NonChanging),list_to_ord_set(OS,Changed),ord_union(Changed,NonChanging,NS).
468
469		% add_edges([],_).
470		% add_edges([(Dest,Pred)|T],Src) :- assert(edge(Src,Dest,Pred)), assert_open(Dest), add_edges(T,Src).
471
472		% process([],A,A).
473		% process([H|T],A,R) :- trans(H,_,S), append(S,A,NS), process(T,NS,R).
474
475		% assert_open(R) :- ( open(R) -> true; (node(R,_) -> true ; assert(open(R)))).
476
477		% no_effect(X,R) :- events(All),list_to_ord_set(All,OA),no_effect(X,OA,R).
478		% no_effect([],A,A).
479		% no_effect([H|T],A,R) :- findall(Y,wp(H,Y,_),Z), list_to_ord_set(Z,OE), ord_subtract(A,OE,NA), no_effect(T,NA,R).
480
481
482		% ---------------------------------- Output
483
484
485		% print_dot2(Name) :- atom_codes(Name,NameString), append(NameString,"_components.dot",FileName),atom_codes(File,FileName),tell(File),
486		% dot_header(Name),findall((S,D,P), trans(S,D,P),WL), print_transitions(WL),
487		% dot_footer, told.
488
489
490		% print_flow(Name) :- atom_codes(Name,NameString), append(NameString,"_flow.dot",FileName),atom_codes(File,FileName),tell(File),dot_header(Name),
491		% flow_nodes, flow_edges,
492		% dot_footer, told.
493
494		% flow_nodes :- findall((S,C),node(S,C),L), flow_node(L).
495		% flow_node([]).
496		% flow_node([(S,C)|T]) :- print(C), print(' '), print('[label="'), print(S), print('"]'),nl,flow_node(T).
497		% flow_edges :- findall((S,D,P), edge(S,P,D), L), flow_edge(L).
498		% flow_edge([]).
499		% flow_edge([(S,P,D)|T]) :- node(S,SN), node(D,DN), print(SN), print('->'), print(DN), print(' '), print('[label="'),
500		% print_pred(P),
501		% print('"]') ,nl,flow_edge(T).
502
503		% :- dynamic graph2/2.
504
505		% print_transitions([]).
506		% print_transitions([(S,D,P)|T]) :- put_node(S,SN), put_node(D,DN),
507		% print(SN), print('->'), print(DN), print(' '), print('[label="'), print(P), print('"]') ,nl, print_transitions(T).
508
509		%put_node(X,XN) :- graph2(X,XN),!.
510		% put_node(X,XN) :- count(XN),inc, assert(graph2(X,XN)), print(XN), print(' '), print('[label="'), print(X), print('"]'),nl.
511