ctl/test_ctl.ml

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