ctl/test_ctl.ml

   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
  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 *)