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