1 % (c) 2014-2022 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 % predicate 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_cs/5]).
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(cbcsrc(enabling_analysis),[translate_enable_res/6, eop_node_predicate/6]).
33
34 % Other modules (used mostly for debugging)
35 :- use_module(dotsrc(dot_graph_generator), [gen_dot_graph/3]).
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 % Unit tests
50 :- 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]])).
51 :- 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]])).
52 :- assert_must_succeed((enable_graph: vertices_edges_predicates_to_egraph([],[],R), R = [])).
53 :- 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-[]])).
54 :- 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-[]])).
55 :- 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]])).
56 :- assert_must_succeed((enable_graph: add_vertex([a-2,b-3,d-4],aa,R), R = [a-2,aa-[],b-3,d-4])).
57 :- assert_must_succeed((enable_graph: add_vertex([a-2,b-3,d-4],'A',R), R = ['A'-[],a-2,b-3,d-4])).
58 :- assert_must_succeed((enable_graph: add_vertex([],'A',R), R = ['A'-[]])).
59
60 vertices_edges_predicates_to_egraph(Vertices,Edges,EnableGraph) :-
61 add_vertices([],Vertices,EnableGraph1),
62 add_edges(EnableGraph1,Edges,EnableGraph).
63
64 add_vertices(EnableGraph,[],EnableGraph).
65 add_vertices(EnableGraph,[V|Vs],NewEnableGraph) :-
66 add_vertex(EnableGraph,V,EnableGraph1),
67 add_vertices(EnableGraph1,Vs,NewEnableGraph).
68
69 %% Using difference lists for constructing the enable graph
70 add_vertex([],V,[V-[]]).
71 add_vertex([V-NB|Rest],V,[V-NB|Rest]) :- !.
72 add_vertex([W-NB|Rest],V,[V-[],W-NB|Rest]) :-
73 W @> V,!.
74 add_vertex([W-NB|Rest],V,[W-NB|S]) :-
75 add_vertex(Rest,V,S).
76
77 add_edges(EnableGraph,[],EnableGraph).
78 add_edges(EnableGraph,[From-Predicate-To|Edges],NewEnableGraph) :-
79 add_neighbour(EnableGraph,From,Predicate,To,EnableGraph1),
80 add_edges(EnableGraph1,Edges,NewEnableGraph).
81
82 add_neighbour([],From,Predicate,To,[From-[To-Predicate]]).
83 add_neighbour([V-Neighbours|Rest],From,Predicate,To,[V-NewNeighbours|Rest]) :-
84 From==V,!,
85 (member(To-Predicate,Neighbours) ->
86 NewNeighbours = Neighbours
87 ; sort([To-Predicate|Neighbours],NewNeighbours)
88 ).
89 add_neighbour([V-Neighbours|Rest],From,Predicate,To,[From-[To-Predicate],V-Neighbours|Rest]) :-
90 V @> From,!.
91 add_neighbour([V-Neighbours|Rest],From,Predicate,To,[V-Neighbours|S]) :-
92 add_neighbour(Rest,From,Predicate,To,S).
93
94 edge_labels(EnableGraph,Labels) :-
95 edge_labels(EnableGraph,[],Labels).
96
97 edge_labels([],Labels,Labels).
98 edge_labels([_V-NB|Rest],LabelsSoFar,Labels) :-
99 maplist(get_vertex_label,NB,Ls),
100 append(LabelsSoFar,Ls,LabelsSoFar1),
101 edge_labels(Rest,LabelsSoFar1,Labels).
102
103 get_vertex_label(_Dst-P,P).
104
105 path_set(EnableGraph,Src,Goals,Module,Predicate,EvaluationDepth,[Src|Path],Length) :-
106 path_set1(EnableGraph,Src,Goals,Module,Predicate,EvaluationDepth,[],Path,0,Length).
107
108 path_set1(_EnableGraph,Goal,Goals,_Module,_Predicate,_EvaluationDepth,_CurPath,[],Length,Length) :-
109 member(Goal,Goals).
110 path_set1(EnableGraph,Src,Goals,Module,Predicate,EvaluationDepth,CurPath,Path,CurLength,Length) :-
111 nonmember(Src,Goals),
112 (EvaluationDepth==0 -> EvaluatePredicate=fail; EvaluatePredicate=true),
113 predicate_edge(EnableGraph,Src,Next,CurPath,Module,Predicate,EvaluatePredicate,NewPredicate),
114 NewLength is CurLength +1,
115 decrease_evaluation_depth(EvaluationDepth,NewEvaluationDepth),
116 Path = [Next|PathTail],
117 path_set1(EnableGraph,Next,Goals,Module,NewPredicate,NewEvaluationDepth,[Next|CurPath],PathTail,NewLength,Length).
118
119 decrease_evaluation_depth(EvaluationDepth,NewEvaluationDepth) :-
120 (EvaluationDepth>0 ->
121 NewEvaluationDepth is EvaluationDepth -1
122 ; NewEvaluationDepth=EvaluationDepth
123 ).
124
125 % Checks if there is an edge between V1 and V2 and additionally tests whether the
126 % Label (e.g. the enabling predicate) evaluates to true. If one of both is not
127 % fullfilled then the call should fail.
128 predicate_edge(EnableGraph,V1,V2,CurPath,Module,Predicate,EvaluatePredicate,NewPredicate) :-
129 edge(EnableGraph,V1,V2,P),
130 nonmember(V2,CurPath),
131 call(Module:Predicate,P,EvaluatePredicate,V1,V2,NewPredicate).
132
133 edge(EnableGraph,V1,V2,Predicate) :-
134 member(V1-NB,EnableGraph),
135 member(V2-Predicate,NB).
136
137 :- public evaluate_enabling_predicate_for_por/7. % used as argument to path_set
138 % TODO: The implementation should be removed to another module
139 % In the context of POR the DoNotVisit set is the set of the currently computed ample set.
140 % predicate(State,DoNotVisit,++EvaluatePredicate,)
141 evaluate_enabling_predicate_for_por(State,DoNotVisit,P,EvaluatePredicate,OpName1,OpName2,NewPredicate) :-
142 nonmember(OpName2,DoNotVisit),
143 empty_state(LocalState),
144 (EvaluatePredicate,State\=[] ->
145 % V2 is enabled after V1, we need to execute V1 in oder to generate the next state
146 % TODO: maybe we should set a sort of time-out to decrease the overhead in some cases
147 !,
148 b_test_boolean_expression_cs(P,LocalState,State,'POR enabling',OpName1:OpName2),
149 % the success of the predicate should guarantee that no well-definedness-errors occur
150 % when OpName1 is executed
151 execute_operation(OpName1,LocalState,State,NextState) % TODO: handle case for non-deterministic operations
152 ; % just checking whether there is an edge between V1 and V2
153 NextState=[] % TODO: what should we give as next state
154 ),
155 NewPredicate = evaluate_enabling_predicate_for_por(NextState,DoNotVisit).
156
157 execute_operation(OpName,LocalState,State,NewState) :-
158 %% (OpName = 'T3writebus' -> trace; true),
159 b_get_machine_operation(OpName,_Res,Par,Body),
160 %% print(expr(Body)),nl,
161 get_texpr_expr(Body,Expr),
162 (Par = [] ->
163 execute_expression(OpName,Expr,LocalState,State,Updates)
164 ; b_interpreter: b_execute_top_level_operation_update(OpName,_FullOp,State,Updates,_Path)
165 %b_interpreter: b_execute_operation_with_parameters(OpName,State,Par,Updates,Res,_Path,_WF,output_required)
166 ),
167 %print(executed_operation(OpName)),nl,
168 % guarantee that Updates is not a variable here
169 %% print(states(Updates,State)),nl,
170 store_updates_and_normalise(Updates,State,NewState).
171
172 :- use_module(probsrc(preferences),[temporary_set_preference/3,reset_temporary_preference/2]).
173 % do not evaluate the precondition
174 execute_expression(_OpName,precondition(_Condition,Body),LocalState,State,Updates) :- !,
175 b_interpreter: b_execute_inner_statement(Body,LocalState,State,Updates,_WF,_IPath,_OR).
176 execute_expression(OpName,Stmt,_LocalState,State,Updates) :-
177 functor(Stmt,rlevent,11),!,
178 % Stmt = rlevent(Name,Section,_Status,_Params,Guard,_Theorems,_Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents)
179 temporary_set_preference(ltsmin_do_not_evaluate_top_level_guards,full,CHNG),
180 %bsyntaxtree:safe_create_texpr(Stmt,event,Event),
181 %b_interpreter_eventb:b_execute_event(OpName,Event,[],[],State,OutputState,_Path),
182 %b_interpreter_eventb:b_event_with_change_set(Event,[],[],State,_ChangeSet,Updates,_Path),
183 b_interpreter:b_execute_top_level_operation_update(OpName,_Operation,State,Updates,_PathInfo),
184 reset_temporary_preference(ltsmin_do_not_evaluate_top_level_guards,CHNG).
185 execute_expression(_OpName,Stmt,LocalState,State,Updates) :-
186 b_interpreter: b_execute_statement(Stmt,LocalState,State,Updates,_WF,_Path).
187 % TODO: export b_execute_inner_statement/7 and b_execute_statement/6 in b_interpreter.pl module
188
189 :- dynamic asserted_enable_graph/1.
190
191 print_enable_graph_dot(EnableGraph,File) :-
192 assertz(asserted_enable_graph(EnableGraph)),
193 gen_dot_graph(File,dot_eop_node_predicate,enable_trans_predicate),
194 retractall(asserted_enable_graph(_)).
195
196 dot_eop_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,Color):-
197 eop_node_predicate(NodeID,SubGraph,NodeDesc,Shape,Style,Color).
198
199 enable_trans_predicate(NodeID,Label,SuccID,Color,Style) :-
200 b_top_level_operation(OpName1),
201 b_top_level_operation(OpName2),
202 asserted_enable_graph(EnableGraph),
203 edge(EnableGraph,OpName1,OpName2,Predicate),
204 translate_bexpression(Predicate,Res),
205 translate_enable_res(Res,NodeID,SuccID,Label,Color,Style).