ctl/test_ctl.ml

   1 (*
   2  * Copyright 2012, INRIA
   3  * Julia Lawall, Gilles Muller
   4  * Copyright 2010-2011, INRIA, University of Copenhagen
   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
  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 *)
  44 module WRAPPER_PRED =
  45   struct
  46     type predicate = string
  47   end
  48
  49 module EXAMPLE_ENGINE =
  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
  76 let mkgraph nodes edges =
  77   let g = ref (new Ograph_extended.ograph_extended) in
  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
  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
  86   let adde anodes (n1,n2,x) =
  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*)
  96 type ('pred,'mvar) old_gen_ctl =
  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
 155 let ex1graph =
 156   let nodes =
 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;;
 192 let ex1phi3 =
 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
 204 let ex1phi4 =
 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
 219 let ex1phi6 =
 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 *)
 226 let ex1phi7 =
 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,[])]
 245     | "paren(v)" -> [(1,["v" --> "1"]); (2,["v" --> "2"]);
 246                      (3,["v" --> "2"]); (4,["v" --> "1"])]
 247     | _          -> []
 248 ;;
 249
 250 let ex2graph =
 251   let nodes =
 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 *)