Commit | Line | Data |
---|---|---|
9f8e26f4 C |
1 | (* |
2 | * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen | |
3 | * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix | |
4 | * This file is part of Coccinelle. | |
5 | * | |
6 | * Coccinelle is free software: you can redistribute it and/or modify | |
7 | * it under the terms of the GNU General Public License as published by | |
8 | * the Free Software Foundation, according to version 2 of the License. | |
9 | * | |
10 | * Coccinelle is distributed in the hope that it will be useful, | |
11 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
12 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
13 | * GNU General Public License for more details. | |
14 | * | |
15 | * You should have received a copy of the GNU General Public License | |
16 | * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>. | |
17 | * | |
18 | * The authors reserve the right to distribute this or future versions of | |
19 | * Coccinelle under other licenses. | |
20 | *) | |
21 | ||
22 | ||
34e49164 C |
23 | |
24 | (* ********************************************************************** *) | |
25 | (* Module: EXAMPLE_ENGINE (instance of CTL_ENGINE) *) | |
26 | (* ********************************************************************** *) | |
27 | ||
28 | (* Simple env.: meta.vars and values are strings *) | |
29 | module SIMPLE_ENV = | |
30 | struct | |
31 | type value = string;; | |
32 | type mvar = string;; | |
33 | let eq_mvar x x' = x = x';; | |
34 | let eq_val v v' = v = v';; | |
35 | let merge_val v v' = v;; | |
36 | end | |
37 | ;; | |
38 | ||
39 | (* Simple predicates *) | |
40 | module WRAPPER_PRED = | |
41 | struct | |
42 | type predicate = string | |
43 | end | |
44 | ||
45 | module EXAMPLE_ENGINE = | |
46 | Wrapper_ctl.CTL_ENGINE_BIS (SIMPLE_ENV) (Ctl_engine.OGRAPHEXT_GRAPH) (WRAPPER_PRED) | |
47 | ||
48 | let top_wit = [] | |
49 | ||
50 | (* ******************************************************************** *) | |
51 | (* *) | |
52 | (* EXAMPLES *) | |
53 | (* *) | |
54 | (* ******************************************************************** *) | |
55 | ||
56 | (* For convenience in the examples *) | |
57 | (* FIX ME: remove *) | |
58 | open Ctl_engine.OGRAPHEXT_GRAPH;; | |
59 | open EXAMPLE_ENGINE;; | |
60 | open Ast_ctl;; | |
61 | ||
62 | (* ---------------------------------------------------------------------- *) | |
63 | (* Helpers *) | |
64 | (* ---------------------------------------------------------------------- *) | |
65 | ||
66 | (* FIX ME: move to ENGINE module *) | |
67 | let (-->) x v = Subst (x,v);; | |
68 | ||
69 | (* FIX ME: move to ENGINE module *) | |
70 | let (-/->) x v = NegSubst(x,v);; | |
71 | ||
72 | let mkgraph nodes edges = | |
73 | let g = ref (new Ograph_extended.ograph_extended) in | |
74 | let addn (n,x) = | |
75 | (* let (g',i) = (!g)#add_node x in *) | |
76 | (* now I need to force the nodei of a node, because of the state(vx) predicates | |
77 | hence add_node -> add_nodei | |
78 | *) | |
79 | let (g', i) = !g#add_nodei n x in | |
80 | assert (i = n); | |
81 | g := g'; (n,i) in | |
82 | let adde anodes (n1,n2,x) = | |
83 | let g' = (!g)#add_arc ((List.assoc n1 anodes,List.assoc n2 anodes),x) in | |
84 | g := g'; () in | |
85 | let add_nodes = List.map addn nodes in | |
86 | let _add_edges = List.map (adde add_nodes) edges in | |
87 | !g | |
88 | ;; | |
89 | ||
90 | ||
91 | (* CTL parameterised on basic predicates and metavar's*) | |
92 | type ('pred,'mvar) old_gen_ctl = | |
93 | | False_ | |
94 | | True_ | |
95 | | Pred_ of 'pred | |
96 | | Not_ of ('pred,'mvar) old_gen_ctl | |
97 | | Exists_ of 'mvar * ('pred,'mvar) old_gen_ctl (* !!! *) | |
98 | | And_ of ('pred,'mvar) old_gen_ctl * ('pred,'mvar) old_gen_ctl | |
99 | | Or_ of ('pred,'mvar) old_gen_ctl * ('pred,'mvar) old_gen_ctl | |
100 | | Implies_ of ('pred,'mvar) old_gen_ctl * ('pred,'mvar) old_gen_ctl | |
101 | | AF_ of ('pred,'mvar) old_gen_ctl | |
102 | | AX_ of ('pred,'mvar) old_gen_ctl | |
103 | | AG_ of ('pred,'mvar) old_gen_ctl | |
104 | | AU_ of ('pred,'mvar) old_gen_ctl * ('pred,'mvar) old_gen_ctl | |
105 | | EF_ of ('pred,'mvar) old_gen_ctl | |
106 | | EX_ of ('pred,'mvar) old_gen_ctl | |
107 | | EG_ of ('pred,'mvar) old_gen_ctl | |
108 | | EU_ of ('pred,'mvar) old_gen_ctl * ('pred,'mvar) old_gen_ctl | |
109 | | Let_ of string * ('pred,'mvar) old_gen_ctl * ('pred,'mvar) old_gen_ctl | |
110 | | Ref_ of string | |
111 | ||
112 | let rec mkanno phi0 = | |
113 | let anno phi = (phi,None) in | |
114 | match phi0 with | |
115 | | False_ -> anno False | |
116 | | True_ -> anno True | |
117 | | Pred_(p) -> anno (Pred(p)) | |
118 | | Not_(phi) -> anno (Not(mkanno phi)) | |
119 | | Exists_(v,phi) -> anno (Exists(v,mkanno phi)) | |
120 | | And_(phi1,phi2) -> anno (And(mkanno phi1,mkanno phi2)) | |
121 | | Or_(phi1,phi2) -> anno (Or(mkanno phi1,mkanno phi2)) | |
122 | | Implies_(phi1,phi2) -> anno (Implies(mkanno phi1,mkanno phi2)) | |
123 | | AF_(phi1) -> anno (AF(mkanno phi1)) | |
124 | | AX_(phi1) -> anno (AX(mkanno phi1)) | |
125 | | AG_(phi1) -> anno (AG(mkanno phi1)) | |
126 | | AU_(phi1,phi2) -> anno (AU(mkanno phi1,mkanno phi2)) | |
127 | | EF_(phi1) -> anno (EF(mkanno phi1)) | |
128 | | EX_(phi1) -> anno (EX(mkanno phi1)) | |
129 | | EG_(phi1) -> anno (EG(mkanno phi1)) | |
130 | | EU_(phi1,phi2) -> anno (EU(mkanno phi1,mkanno phi2)) | |
131 | | Let_ (x,phi1,phi2) -> anno (Let(x,mkanno phi1,mkanno phi2)) | |
132 | | Ref_(s) -> anno (Ref(s)) | |
133 | ||
134 | ||
135 | (* ******************************************************************** *) | |
136 | (* Example 1 *) | |
137 | (* CTL: f(x) /\ AF(Ey.g(y)) *) | |
138 | (* ******************************************************************** *) | |
139 | ||
140 | let ex1lab s = | |
141 | match s with | |
142 | | "f(x)" -> [(0,["x" --> "1"]); (1,["x" --> "2"])] | |
143 | | "g(y)" -> [(3,["y" --> "1"]); (4,["y" --> "2"])] | |
144 | | "f(1)" -> [(0,[])] | |
145 | | "f(2)" -> [(1,[])] | |
146 | | "g(1)" -> [(3,[])] | |
147 | | "g(2)" -> [(4,[])] | |
148 | | _ -> [] | |
149 | ;; | |
150 | ||
151 | let ex1graph = | |
152 | let nodes = | |
153 | [(0,"f(1)");(1,"f(2)");(2,"< >");(3,"g(1)");(4,"g(2)");(5,"<exit>")] in | |
154 | let edges = [(0,2); (1,2); (2,3); (2,4); (3,5); (4,5); (5,5)] in | |
155 | mkgraph nodes (List.map (fun (x,y) -> (x,y,())) edges) | |
156 | ;; | |
157 | ||
158 | let ex1states = List.map fst (ex1graph#nodes)#tolist;; | |
159 | ||
160 | let ex1model = (ex1graph,ex1lab,ex1states);; | |
161 | let ex1model_wrapped = (ex1graph,wrap_label ex1lab,ex1states);; | |
162 | ||
163 | let ex1s0 = Exists_("v0",Pred_ ("f(x)",UnModif "v0"));; | |
164 | let ex1s1 = Exists_("v1",Pred_ ("g(y)",Modif "v1"));; | |
165 | let ex1s2 = Exists_("y",ex1s1);; | |
166 | let ex1s3 = AF_(ex1s2);; | |
167 | let ex1s4 = And_(ex1s0,ex1s3);; | |
168 | ||
169 | let ex1s3a = AX_(ex1s2);; | |
170 | let ex1s4a = AX_(AX_(ex1s2));; | |
171 | let ex1s5a = And_(ex1s0,ex1s4a);; | |
172 | ||
173 | let ex1s0b = Pred_ ("g(y)", Modif "v0");; | |
174 | let ex1s1b = Exists_ ("v0",ex1s0b);; | |
175 | let ex1s2b = Exists_ ("y",ex1s1b);; | |
176 | let ex1s3b = AF_(ex1s2b);; | |
177 | let ex1s4b = AX_(ex1s3b);; | |
178 | let ex1s5b = Pred_ ("f(x)", UnModif "v3");; | |
179 | let ex1s6b = Exists_ ("v3", ex1s5b);; | |
180 | let ex1s7b = Exists_ ("x", ex1s6b);; | |
181 | let ex1s8b = And_(ex1s7b,ex1s4b);; | |
182 | ||
183 | let ex1s7c = And_(ex1s6b,ex1s4b);; | |
184 | let ex1s8c = Exists_("x",ex1s7c);; | |
185 | ||
186 | let ex1phi1 = ex1s4;; | |
187 | let ex1phi2 = ex1s5a;; | |
188 | let ex1phi3 = | |
189 | And_ | |
190 | (Exists_ ("x", | |
191 | (Exists_ ("v3", | |
192 | Pred_ ("f(x)", UnModif "v3")))), | |
193 | AX_ | |
194 | (AF_ | |
195 | (Exists_ ("y", (* change this to Y and have strange behaviour *) | |
196 | (Exists_ ("v0", | |
197 | Pred_ ("g(y)", Modif "v0") | |
198 | ))))));; | |
199 | ||
200 | let ex1phi4 = | |
201 | Exists_ ("x", | |
202 | And_ ( | |
203 | (Exists_ ("v3", | |
204 | Pred_ ("f(x)", UnModif "v3"))), | |
205 | AX_ | |
206 | (AF_ | |
207 | (Exists_ ("y", (* change this to Y and have strange behaviour *) | |
208 | (Exists_ ("v0", | |
209 | Pred_ ("g(y)", Modif "v0") | |
210 | )))))));; | |
211 | ||
212 | ||
213 | let ex1phi5 = AU_(True_,Exists_("y", Exists_("v0",Pred_("g(y)",Modif "v0"))));; | |
214 | ||
215 | let ex1phi6 = | |
216 | AU_( | |
217 | Not_(Exists_("x",Exists_("v1",Pred_("f(x)",UnModif "v1")))), | |
218 | Exists_("y", Exists_("v0",Pred_("g(y)",Modif "v0"))) | |
219 | );; | |
220 | ||
221 | (* use with ex1nc *) | |
222 | let ex1phi7 = | |
223 | AU_( | |
224 | Not_(Or_(Pred_("f(1)",Control),Pred_("f(2)",Control))), | |
225 | Exists_("y", Exists_("v0",Pred_("g(y)",Modif "v0"))) | |
226 | );; | |
227 | ||
228 | let ex1 phi = satbis ex1model (mkanno phi);; | |
229 | let ex1nc phi = satbis_noclean ex1model (mkanno phi);; | |
230 | ||
231 | ||
232 | (* ******************************************************************** *) | |
233 | (* Example 2 *) | |
234 | (* ******************************************************************** *) | |
235 | ||
236 | let ex2lab s = | |
237 | match s with | |
238 | | "p" -> [0,[]] | |
239 | | "{" -> [(1,[]); (2,[])] | |
240 | | "}" -> [(3,[]); (4,[])] | |
241 | | "paren(v)" -> [(1,["v" --> "1"]); (2,["v" --> "2"]); | |
242 | (3,["v" --> "2"]); (4,["v" --> "1"])] | |
243 | | _ -> [] | |
244 | ;; | |
245 | ||
246 | let ex2graph = | |
247 | let nodes = | |
248 | [(0,"p");(1,"{");(2,"{");(3,"}");(4,"}");(5,"<exit>")] in | |
249 | let edges = [(0,1); (1,2); (2,3); (3,4); (4,5); (5,5)] in | |
250 | mkgraph nodes (List.map (fun (x,y) -> (x,y,())) edges) | |
251 | ;; | |
252 | ||
253 | let ex2states = List.map fst (ex2graph#nodes)#tolist;; | |
254 | ||
255 | let ex2model = (ex2graph,ex2lab,ex2states);; | |
256 | let ex2model_wrapped = (ex2graph,wrap_label ex2lab,ex2states);; | |
257 | ||
258 | let ex2s0 = Pred_("p",Control);; | |
259 | let ex2s1 = Pred_("{",Control);; | |
260 | let ex2s2 = Pred_("paren(v)",Control);; | |
261 | let ex2s3 = And_(ex2s1,ex2s2);; | |
262 | let ex2s4 = Pred_("}",Control);; | |
263 | let ex2s5 = Pred_("paren(v)",Control);; | |
264 | let ex2s6 = And_(ex2s4,ex2s5);; | |
265 | let ex2s7 = AF_(ex2s6);; | |
266 | let ex2s8 = And_(ex2s3,ex2s7);; | |
267 | let ex2s9 = Exists_("v",ex2s8);; | |
268 | let ex2s10 = AX_(ex2s9);; | |
269 | let ex2s11 = And_(ex2s0,ex2s10);; | |
270 | ||
271 | let ex2phi1 = ex2s11;; | |
272 | ||
273 | let ex2 phi = satbis_noclean ex2model (mkanno phi) | |
274 | ||
275 | (* | |
276 | +--- s11:& ---+ | |
277 | | | | |
278 | s0:p s10:AX | |
279 | | | |
280 | s9:exists v | |
281 | | | |
282 | +---------- s8:& --------+ | |
283 | | | | |
284 | +-- s3:& --+ s7:AF | |
285 | | | | | |
286 | s1:"{" s2:paren(v) +-- s6:& -+ | |
287 | | | | |
288 | s4:"}" s5:paren(v) | |
289 | ||
290 | s0 : p : (0,_,_) | |
291 | s1 : "{" : (1,_,_); (2,_,_) | |
292 | s2 : paren(v) : (1,v=1,_); (2,v=2,_); (3,v=2,_); (4,v=1,_) | |
293 | s3 : "{" & paren(v) : (1,v=1,_); (2,v=2,_) | |
294 | s4 : "}" : (3,_,_); (4,_,_) | |
295 | s5 : paren(v) : (1,v=1,_); (2,v=2,_); (3,v=2,_); (4,v=1,_) | |
296 | s6 : "}" & paren(v) : (3,v=2,_); (4,v=1,_) | |
297 | s7 : AF(...) : (0;1;2;3,v=2,_); (0;1;2;3;4,v=1,_) | |
298 | s8 : (...&...) & AF(...) : (1,v=1,_); (2,v=2,_) | |
299 | s9 : exists ... : (1,_,(1,v=1)); (2,_,(2,v=2)) | |
300 | s10 : AX(...) : (0,_,(1,v=1)); (1,_,(2,v=2)) | |
301 | s11 : p & AX(...) : (0,_,(1,v=1)) | |
302 | *) |