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