1 % (c) 2014-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(enable_graph, [
6 print_enable_graph_dot/2, path_enable_graph/8 % predicates called from Tcl/Tk interface
7 ,add_vertex/3, add_neighbour/5, edge_labels/2 % should be deleted (exported just for testing)
8 ,path_set/8
9 ]).
10
11 /* Modules and Infos for the code coverage analysis */
12 :- use_module(probsrc(module_information)).
13 :- module_info(group,model_checker).
14 :- module_info(description,'This module provides operations of directed enable graphs.').
15
16 % Standard SICSTUS prolog libraries
17 :- use_module(library(lists)).
18
19 % Classical B prolog modules
20 :- use_module(probsrc(bmachine),[b_get_machine_operation/4,b_top_level_operation/1]).
21 :- use_module(probsrc(b_interpreter),[b_test_boolean_expression_wf/3]).
22 :- use_module(probsrc(bsyntaxtree), [get_texpr_expr/2]).
23
24 % Event-B prolog modules
25 %:- use_module(probsrc(b_interpreter_eventb),[b_event/6, b_event_with_change_set/7]).
26
27 % Prolog modules handling the state space
28 :- use_module(probsrc(store), [empty_state/1,store_updates_and_normalise/3]).
29
30 % Prolog modules declaring predicates relevant for partial order reduction optimisation
31 %% :- use_module(probporsrc(static_analysis),[dependent_act/2]).
32 :- use_module(probsrc(enabling_analysis),[translate_enable_res/6]).
33
34 % Other modules (used mostly for debugging)
35 :- use_module(probsrc(dot_graph_generator),[gen_dot_graph/6]).
36 :- use_module(probsrc(translate),[translate_bexpression/2]).
37 %:- use_module(probsrc(preferences),[get_preference/2]).
38
39 % Importing unit tests predicates
40 :- use_module(probsrc(self_check)).
41
42 /*
43 An enable graph is represented as a list of pairs (vertex-edgelist), the edge list is a list of pairs (neighbor-enabling_predicate).
44 The module follows the definition of enable graph from 'Automatic Flow Analysis for Event-B'. An enable graph can be used, for example,
45 for the analysis of the event relations in a Event-B machine that is necessary for optimisations like partial order reduction and
46 partial guard evaluation.
47 */
48
49 % path_enable_graph(+V1,+V2,+N,+ST,+VertexSet,+EnableGraph,-Path,-Length)
50 % is true if 'Path' is a list of vertices constituting a path of the length 'Length'
51 % from 'V1' to 'V2' in 'EnableGraph' and thereby each vertex of the 'Path' is
52 % not in 'VertexSet' and 'ST' is a state (predicate expresison) in respect of which the enable guard of the first
53 % edge will be evaluated.
54 % Special cases:
55 % 1. If 'ST' is the empty state and 'VertexSet' is an empty list, then path_enable_graph can be used to
56 % find some path from 'V1' to 'V2' in 'EnableGraph' without taking into account the enabling predicates of the edges.
57 % 2. If 'N' is equal to 0, then the predicate will search just for a path connecting 'V1' with 'V2'.
58
59 path_enable_graph(V1,V2,N,ST,VertexSet,EnableGraph,Path,Length) :-
60 path(V1,V2,N,ST,VertexSet,EnableGraph,Path,Length).
61
62 % Unit tests
63 :- assert_must_succeed((enable_graph: vertices_edges_predicates_to_egraph([a,b,d,e,q],[a-1-d,a-2-b,d-4-q,e-1-a,e-4-b,q-3-c],R), R = [a-[b-2,d-1],b-[],d-[q-4],e-[a-1,b-4],q-[c-3]])).
64 :- assert_must_succeed((enable_graph: vertices_edges_predicates_to_egraph([],[a-1-d,a-2-b,d-4-q,e-1-a,e-4-b,q-3-c],R), R = [a-[b-2,d-1],d-[q-4],e-[a-1,b-4],q-[c-3]])).
65 :- assert_must_succeed((enable_graph: vertices_edges_predicates_to_egraph([],[],R), R = [])).
66 :- assert_must_succeed((enable_graph: add_neighbour([2-[3-v],4-[1-w,4-p],5-[]],2,q,3,R), R = [2-[3-q,3-v],4-[1-w,4-p],5-[]])).
67 :- assert_must_succeed((enable_graph: add_neighbour([2-[3-v],4-[1-w,4-p],5-[]],1,q,3,R), R = [1-[3-q],2-[3-v],4-[1-w,4-p],5-[]])).
68 :- assert_must_succeed((enable_graph: add_neighbour([2-[3-v],4-[1-w,4-p],5-[]],6,q,3,R), R = [2-[3-v],4-[1-w,4-p],5-[],6-[3-q]])).
69 :- assert_must_succeed((enable_graph: add_vertex([a-2,b-3,d-4],aa,R), R = [a-2,aa-[],b-3,d-4])).
70 :- assert_must_succeed((enable_graph: add_vertex([a-2,b-3,d-4],'A',R), R = ['A'-[],a-2,b-3,d-4])).
71 :- assert_must_succeed((enable_graph: add_vertex([],'A',R), R = ['A'-[]])).
72
73 vertices_edges_predicates_to_egraph(Vertices,Edges,EnableGraph) :-
74 add_vertices([],Vertices,EnableGraph1),
75 add_edges(EnableGraph1,Edges,EnableGraph).
76
77 add_vertices(EnableGraph,[],EnableGraph).
78 add_vertices(EnableGraph,[V|Vs],NewEnableGraph) :-
79 add_vertex(EnableGraph,V,EnableGraph1),
80 add_vertices(EnableGraph1,Vs,NewEnableGraph).
81
82 %% Using difference lists for constructing the enable graph
83 add_vertex([],V,[V-[]]).
84 add_vertex([V-NB|Rest],V,[V-NB|Rest]) :- !.
85 add_vertex([W-NB|Rest],V,[V-[],W-NB|Rest]) :-
86 W @> V,!.
87 add_vertex([W-NB|Rest],V,[W-NB|S]) :-
88 add_vertex(Rest,V,S).
89
90 add_edges(EnableGraph,[],EnableGraph).
91 add_edges(EnableGraph,[From-Predicate-To|Edges],NewEnableGraph) :-
92 add_neighbour(EnableGraph,From,Predicate,To,EnableGraph1),
93 add_edges(EnableGraph1,Edges,NewEnableGraph).
94
95 add_neighbour([],From,Predicate,To,[From-[To-Predicate]]).
96 add_neighbour([V-Neighbours|Rest],From,Predicate,To,[V-NewNeighbours|Rest]) :-
97 From==V,!,
98 (member(To-Predicate,Neighbours) ->
99 NewNeighbours = Neighbours
100 ; otherwise -> %trace,
101 sort([To-Predicate|Neighbours],NewNeighbours)
102 ).
103 add_neighbour([V-Neighbours|Rest],From,Predicate,To,[From-[To-Predicate],V-Neighbours|Rest]) :-
104 V @> From,!.
105 add_neighbour([V-Neighbours|Rest],From,Predicate,To,[V-Neighbours|S]) :-
106 add_neighbour(Rest,From,Predicate,To,S).
107
108 edge_labels(EnableGraph,Labels) :-
109 edge_labels(EnableGraph,[],Labels).
110
111 edge_labels([],Labels,Labels).
112 edge_labels([_V-NB|Rest],LabelsSoFar,Labels) :-
113 maplist(get_vertex_label,NB,Ls),
114 append(LabelsSoFar,Ls,LabelsSoFar1),
115 edge_labels(Rest,LabelsSoFar1,Labels).
116
117 get_vertex_label(_Dst-P,P).
118
119 path_set(EnableGraph,Src,Goals,Module,Predicate,EvaluationDepth,[Src|Path],Length) :-
120 path_set1(EnableGraph,Src,Goals,Module,Predicate,EvaluationDepth,[],Path,0,Length).
121
122 path_set1(_EnableGraph,Goal,Goals,_Module,_Predicate,_EvaluationDepth,_CurPath,[],Length,Length) :-
123 member(Goal,Goals).
124 path_set1(EnableGraph,Src,Goals,Module,Predicate,EvaluationDepth,CurPath,Path,CurLength,Length) :-
125 nonmember(Src,Goals),
126 (EvaluationDepth==0 -> EvaluatePredicate=fail; EvaluatePredicate=true),
127 predicate_edge(EnableGraph,Src,Next,CurPath,Module,Predicate,EvaluatePredicate,NewPredicate),
128 NewLength is CurLength +1,
129 decrease_evaluation_depth(EvaluationDepth,NewEvaluationDepth),
130 Path = [Next|PathTail],
131 path_set1(EnableGraph,Next,Goals,Module,NewPredicate,NewEvaluationDepth,[Next|CurPath],PathTail,NewLength,Length).
132
133
134 % Predicates for finding a path from Src to Goal in the enable graph
135 path(EnableGraph,Src,Goal,Module,Predicate,EvaluationDepth,[Src|Path],Length) :-
136 path1(EnableGraph,Src,Goal,Module,Predicate,EvaluationDepth,[],Path,0,Length).
137
138 path1(_EnableGraph,Goal,Goal,_Module,_Predicate,_EvaluationDepth,_CurPath,[],Length,Length).
139 path1(EnableGraph,Src,Goal,Module,Predicate,EvaluationDepth,CurPath,Path,CurLength,Length) :-
140 Src\=Goal,
141 (EvaluationDepth==0 -> EvaluatePredicate=fail; EvaluatePredicate=true),
142 predicate_edge(EnableGraph,Src,Next,CurPath,Module,Predicate,EvaluatePredicate,NewPredicate),
143 NewLength is CurLength +1,
144 decrease_evaluation_depth(EvaluationDepth,NewEvaluationDepth),
145 Path = [Next|PathTail],
146 path1(EnableGraph,Next,Goal,Module,NewPredicate,NewEvaluationDepth,[Next|CurPath],PathTail,NewLength,Length).
147
148 decrease_evaluation_depth(EvaluationDepth,NewEvaluationDepth) :-
149 (EvaluationDepth>0 ->
150 NewEvaluationDepth is EvaluationDepth -1
151 ; NewEvaluationDepth=EvaluationDepth
152 ).
153
154 % Checks if there is an edge between V1 and V2 and additionally tests whether the
155 % Label (e.g. the enabling predicate) evaluates to true. If one of both is not
156 % fullfilled then the call should fail.
157 predicate_edge(EnableGraph,V1,V2,CurPath,Module,Predicate,EvaluatePredicate,NewPredicate) :-
158 edge(EnableGraph,V1,V2,P),
159 nonmember(V2,CurPath),
160 call(Module:Predicate,P,EvaluatePredicate,V1,V2,NewPredicate).
161
162 edge(EnableGraph,V1,V2,Predicate) :-
163 member(V1-NB,EnableGraph),
164 member(V2-Predicate,NB).
165
166 :- public evaluate_enabling_predicate_for_por/7. % used as argument to path_set
167 % TODO: The implementation should be removed to another module
168 % In the context of POR the DoNotVisit set is the set of the currently computed ample set.
169 % predicate(State,DoNotVisit,++EvaluatePredicate,)
170 evaluate_enabling_predicate_for_por(State,DoNotVisit,P,EvaluatePredicate,OpName1,OpName2,NewPredicate) :-
171 nonmember(OpName2,DoNotVisit),
172 empty_state(LocalState),
173 ((EvaluatePredicate,State\=[]) ->
174 % V2 is enabled after V1, we need to execute V1 in oder to generate the next state
175 % TODO: maybe we should set a sort of time-out to decrease the overhead in some cases
176 !,
177 %% translate:print_bexpr(P),nl,
178 %% translate:print_bstate(State),nl,
179 b_test_boolean_expression_wf(P,LocalState,State),
180 % the success of the predicate should guarantee that no well-definedness-errors occur
181 % when OpName1 is executed
182 %% print(b_test_boolean_expression_wf_true),nl,
183 %% print(execute_operation(OpName1)),nl,
184 execute_operation(OpName1,LocalState,State,NextState) % TODO: handle case for non-deterministic operations
185 %% ,translate:print_bstate(NextState),nl
186 ; otherwise -> % just checking whether there is an edge between V1 and V2
187 NextState=[] % TODO: what should we give as next state
188 ),
189 NewPredicate = evaluate_enabling_predicate_for_por(NextState,DoNotVisit).
190
191 execute_operation(OpName,LocalState,State,NewState) :-
192 %% (OpName = 'T3writebus' -> trace; true),
193 b_get_machine_operation(OpName,_Res,Par,Body),
194 %% print(expr(Body)),nl,
195 get_texpr_expr(Body,Expr),
196 (Par = [] ->
197 execute_expression(OpName,Expr,LocalState,State,Updates)
198 ; b_interpreter: b_execute_top_level_operation_update(OpName,_FullOp,State,Updates,_Path)
199 %b_interpreter: b_execute_operation_with_parameters(OpName,State,Par,Updates,Res,_Path,_WF,output_required)
200 ),
201 %print(executed_operation(OpName)),nl,
202 % guarantee that Updates is not a variable here
203 %% print(states(Updates,State)),nl,
204 store_updates_and_normalise(Updates,State,NewState).
205
206 % do not evaluate the precondition
207 execute_expression(_OpName,precondition(_Condition,Body),LocalState,State,Updates) :- !,
208 b_interpreter: b_execute_inner_statement(Body,LocalState,State,Updates,_WF,_IPath,_OR).
209 execute_expression(OpName,Stmt,_LocalState,State,Updates) :-
210 functor(Stmt,rlevent,11),!,
211 % Stmt = rlevent(Name,Section,_Status,_Params,Guard,_Theorems,_Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents)
212 assert(pge_algo: do_not_evaluate_guard),
213 %bsyntaxtree:safe_create_texpr(Stmt,event,Event),
214 %b_interpreter_eventb:b_event(Event,[],[],State,OutputState,_Path),
215 %b_interpreter_eventb:b_event_with_change_set(Event,[],[],State,_ChangeSet,Updates,_Path),
216 b_interpreter:b_execute_top_level_operation_update(OpName,_Operation,State,Updates,_PathInfo),
217 retractall(pge_algo: do_not_evaluate_guard).
218 execute_expression(_OpName,Stmt,LocalState,State,Updates) :-
219 b_interpreter: b_execute_statement(Stmt,LocalState,State,Updates,_WF,_Path).
220 % TODO: export b_execute_inner_statement/7 and b_execute_statement/6 in b_interpreter.pl module
221
222 :- dynamic asserted_enable_graph/1.
223
224 print_enable_graph_dot(EnableGraph,File) :-
225 assert(asserted_enable_graph(EnableGraph)),
226 gen_dot_graph(File,enable_graph,eop_node_predicate,enable_trans_predicate,none,none),
227 retractall(asserted_enable_graph(_)).
228
229 :- public eop_node_predicate/6.
230 eop_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,Color):-
231 enabling_analysis: eop_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,Color).
232
233 :- public enable_trans_predicate/5.
234 enable_trans_predicate(NodeID,Label,SuccID,Color,Style) :-
235 b_top_level_operation(OpName1),
236 b_top_level_operation(OpName2),
237 asserted_enable_graph(EnableGraph),
238 edge(EnableGraph,OpName1,OpName2,Predicate),
239 translate_bexpression(Predicate,Res),
240 translate_enable_res(Res,NodeID,SuccID,Label,Color,Style).