08fbb4d79c9997cfe383a0f7b9efe31469979f1e
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.
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.
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.
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/>.
20 * The authors reserve the right to distribute this or future versions of
21 * Coccinelle under other licenses.
26 * Copyright 2010, INRIA, University of Copenhagen
27 * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
28 * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
29 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
30 * This file is part of Coccinelle.
32 * Coccinelle is free software: you can redistribute it and/or modify
33 * it under the terms of the GNU General Public License as published by
34 * the Free Software Foundation, according to version 2 of the License.
36 * Coccinelle is distributed in the hope that it will be useful,
37 * but WITHOUT ANY WARRANTY; without even the implied warranty of
38 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
39 * GNU General Public License for more details.
41 * You should have received a copy of the GNU General Public License
42 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
44 * The authors reserve the right to distribute this or future versions of
45 * Coccinelle under other licenses.
50 (* ********************************************************************** *)
51 (* Module: EXAMPLE_ENGINE (instance of CTL_ENGINE) *)
52 (* ********************************************************************** *)
54 (* Simple env.: meta.vars and values are strings *)
59 let eq_mvar x x'
= x
= x'
;;
60 let eq_val v v'
= v
= v'
;;
61 let merge_val v v'
= v
;;
65 (* Simple predicates *)
68 type predicate
= string
71 module EXAMPLE_ENGINE
=
72 Wrapper_ctl.CTL_ENGINE_BIS
(SIMPLE_ENV
) (Ctl_engine.OGRAPHEXT_GRAPH
) (WRAPPER_PRED
)
76 (* ******************************************************************** *)
80 (* ******************************************************************** *)
82 (* For convenience in the examples *)
84 open Ctl_engine.OGRAPHEXT_GRAPH
;;
88 (* ---------------------------------------------------------------------- *)
90 (* ---------------------------------------------------------------------- *)
92 (* FIX ME: move to ENGINE module *)
93 let (-->) x v
= Subst
(x
,v
);;
95 (* FIX ME: move to ENGINE module *)
96 let (-/->) x v
= NegSubst
(x
,v
);;
98 let mkgraph nodes edges
=
99 let g = ref (new Ograph_extended.ograph_extended
) in
101 (* let (g',i) = (!g)#add_node x in *)
102 (* now I need to force the nodei of a node, because of the state(vx) predicates
103 hence add_node -> add_nodei
105 let (g'
, i
) = !g#add_nodei n x
in
108 let adde anodes
(n1
,n2
,x
) =
109 let g'
= (!g)#add_arc
((List.assoc n1 anodes
,List.assoc n2 anodes
),x
) in
111 let add_nodes = List.map
addn nodes
in
112 let _add_edges = List.map
(adde add_nodes) edges
in
117 (* CTL parameterised on basic predicates and metavar's*)
118 type ('pred
,'mvar
) old_gen_ctl
=
122 | Not_
of ('pred
,'mvar
) old_gen_ctl
123 | Exists_
of 'mvar
* ('pred
,'mvar
) old_gen_ctl
(* !!! *)
124 | And_
of ('pred
,'mvar
) old_gen_ctl
* ('pred
,'mvar
) old_gen_ctl
125 | Or_
of ('pred
,'mvar
) old_gen_ctl
* ('pred
,'mvar
) old_gen_ctl
126 | Implies_
of ('pred
,'mvar
) old_gen_ctl
* ('pred
,'mvar
) old_gen_ctl
127 | AF_
of ('pred
,'mvar
) old_gen_ctl
128 | AX_
of ('pred
,'mvar
) old_gen_ctl
129 | AG_
of ('pred
,'mvar
) old_gen_ctl
130 | AU_
of ('pred
,'mvar
) old_gen_ctl
* ('pred
,'mvar
) old_gen_ctl
131 | EF_
of ('pred
,'mvar
) old_gen_ctl
132 | EX_
of ('pred
,'mvar
) old_gen_ctl
133 | EG_
of ('pred
,'mvar
) old_gen_ctl
134 | EU_
of ('pred
,'mvar
) old_gen_ctl
* ('pred
,'mvar
) old_gen_ctl
135 | Let_
of string * ('pred
,'mvar
) old_gen_ctl
* ('pred
,'mvar
) old_gen_ctl
138 let rec mkanno phi0
=
139 let anno phi
= (phi
,None
) in
141 | False_
-> anno False
143 | Pred_
(p
) -> anno (Pred
(p
))
144 | Not_
(phi
) -> anno (Not
(mkanno phi
))
145 | Exists_
(v
,phi
) -> anno (Exists
(v
,mkanno phi
))
146 | And_
(phi1
,phi2
) -> anno (And
(mkanno phi1
,mkanno phi2
))
147 | Or_
(phi1
,phi2
) -> anno (Or
(mkanno phi1
,mkanno phi2
))
148 | Implies_
(phi1
,phi2
) -> anno (Implies
(mkanno phi1
,mkanno phi2
))
149 | AF_
(phi1
) -> anno (AF
(mkanno phi1
))
150 | AX_
(phi1
) -> anno (AX
(mkanno phi1
))
151 | AG_
(phi1
) -> anno (AG
(mkanno phi1
))
152 | AU_
(phi1
,phi2
) -> anno (AU
(mkanno phi1
,mkanno phi2
))
153 | EF_
(phi1
) -> anno (EF
(mkanno phi1
))
154 | EX_
(phi1
) -> anno (EX
(mkanno phi1
))
155 | EG_
(phi1
) -> anno (EG
(mkanno phi1
))
156 | EU_
(phi1
,phi2
) -> anno (EU
(mkanno phi1
,mkanno phi2
))
157 | Let_
(x
,phi1
,phi2
) -> anno (Let
(x
,mkanno phi1
,mkanno phi2
))
158 | Ref_
(s
) -> anno (Ref
(s
))
161 (* ******************************************************************** *)
163 (* CTL: f(x) /\ AF(Ey.g(y)) *)
164 (* ******************************************************************** *)
168 | "f(x)" -> [(0,["x" --> "1"]); (1,["x" --> "2"])]
169 | "g(y)" -> [(3,["y" --> "1"]); (4,["y" --> "2"])]
179 [(0,"f(1)");(1,"f(2)");(2,"< >");(3,"g(1)");(4,"g(2)");(5,"<exit>")] in
180 let edges = [(0,2); (1,2); (2,3); (2,4); (3,5); (4,5); (5,5)] in
181 mkgraph nodes (List.map
(fun (x
,y
) -> (x
,y
,())) edges)
184 let ex1states = List.map fst
(ex1graph#
nodes)#tolist
;;
186 let ex1model = (ex1graph,ex1lab,ex1states);;
187 let ex1model_wrapped = (ex1graph,wrap_label
ex1lab,ex1states);;
189 let ex1s0 = Exists_
("v0",Pred_
("f(x)",UnModif
"v0"));;
190 let ex1s1 = Exists_
("v1",Pred_
("g(y)",Modif
"v1"));;
191 let ex1s2 = Exists_
("y",ex1s1);;
192 let ex1s3 = AF_
(ex1s2);;
193 let ex1s4 = And_
(ex1s0,ex1s3);;
195 let ex1s3a = AX_
(ex1s2);;
196 let ex1s4a = AX_
(AX_
(ex1s2));;
197 let ex1s5a = And_
(ex1s0,ex1s4a);;
199 let ex1s0b = Pred_
("g(y)", Modif
"v0");;
200 let ex1s1b = Exists_
("v0",ex1s0b);;
201 let ex1s2b = Exists_
("y",ex1s1b);;
202 let ex1s3b = AF_
(ex1s2b);;
203 let ex1s4b = AX_
(ex1s3b);;
204 let ex1s5b = Pred_
("f(x)", UnModif
"v3");;
205 let ex1s6b = Exists_
("v3", ex1s5b);;
206 let ex1s7b = Exists_
("x", ex1s6b);;
207 let ex1s8b = And_
(ex1s7b,ex1s4b);;
209 let ex1s7c = And_
(ex1s6b,ex1s4b);;
210 let ex1s8c = Exists_
("x",ex1s7c);;
212 let ex1phi1 = ex1s4;;
213 let ex1phi2 = ex1s5a;;
218 Pred_
("f(x)", UnModif
"v3")))),
221 (Exists_
("y", (* change this to Y and have strange behaviour *)
223 Pred_
("g(y)", Modif
"v0")
230 Pred_
("f(x)", UnModif
"v3"))),
233 (Exists_
("y", (* change this to Y and have strange behaviour *)
235 Pred_
("g(y)", Modif
"v0")
239 let ex1phi5 = AU_
(True_
,Exists_
("y", Exists_
("v0",Pred_
("g(y)",Modif
"v0"))));;
243 Not_
(Exists_
("x",Exists_
("v1",Pred_
("f(x)",UnModif
"v1")))),
244 Exists_
("y", Exists_
("v0",Pred_
("g(y)",Modif
"v0")))
250 Not_
(Or_
(Pred_
("f(1)",Control
),Pred_
("f(2)",Control
))),
251 Exists_
("y", Exists_
("v0",Pred_
("g(y)",Modif
"v0")))
254 let ex1 phi
= satbis
ex1model (mkanno phi
);;
255 let ex1nc phi
= satbis_noclean
ex1model (mkanno phi
);;
258 (* ******************************************************************** *)
260 (* ******************************************************************** *)
265 | "{" -> [(1,[]); (2,[])]
266 | "}" -> [(3,[]); (4,[])]
267 | "paren(v)" -> [(1,["v" --> "1"]); (2,["v" --> "2"]);
268 (3,["v" --> "2"]); (4,["v" --> "1"])]
274 [(0,"p");(1,"{");(2,"{");(3,"}");(4,"}");(5,"<exit>")] in
275 let edges = [(0,1); (1,2); (2,3); (3,4); (4,5); (5,5)] in
276 mkgraph nodes (List.map
(fun (x
,y
) -> (x
,y
,())) edges)
279 let ex2states = List.map fst
(ex2graph#
nodes)#tolist
;;
281 let ex2model = (ex2graph,ex2lab,ex2states);;
282 let ex2model_wrapped = (ex2graph,wrap_label
ex2lab,ex2states);;
284 let ex2s0 = Pred_
("p",Control
);;
285 let ex2s1 = Pred_
("{",Control
);;
286 let ex2s2 = Pred_
("paren(v)",Control
);;
287 let ex2s3 = And_
(ex2s1,ex2s2);;
288 let ex2s4 = Pred_
("}",Control
);;
289 let ex2s5 = Pred_
("paren(v)",Control
);;
290 let ex2s6 = And_
(ex2s4,ex2s5);;
291 let ex2s7 = AF_
(ex2s6);;
292 let ex2s8 = And_
(ex2s3,ex2s7);;
293 let ex2s9 = Exists_
("v",ex2s8);;
294 let ex2s10 = AX_
(ex2s9);;
295 let ex2s11 = And_
(ex2s0,ex2s10);;
297 let ex2phi1 = ex2s11;;
299 let ex2 phi
= satbis_noclean
ex2model (mkanno phi
)
308 +---------- s8:& --------+
312 s1:"{" s2:paren(v) +-- s6:& -+
317 s1 : "{" : (1,_,_); (2,_,_)
318 s2 : paren(v) : (1,v=1,_); (2,v=2,_); (3,v=2,_); (4,v=1,_)
319 s3 : "{" & paren(v) : (1,v=1,_); (2,v=2,_)
320 s4 : "}" : (3,_,_); (4,_,_)
321 s5 : paren(v) : (1,v=1,_); (2,v=2,_); (3,v=2,_); (4,v=1,_)
322 s6 : "}" & paren(v) : (3,v=2,_); (4,v=1,_)
323 s7 : AF(...) : (0;1;2;3,v=2,_); (0;1;2;3;4,v=1,_)
324 s8 : (...&...) & AF(...) : (1,v=1,_); (2,v=2,_)
325 s9 : exists ... : (1,_,(1,v=1)); (2,_,(2,v=2))
326 s10 : AX(...) : (0,_,(1,v=1)); (1,_,(2,v=2))
327 s11 : p & AX(...) : (0,_,(1,v=1))