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