ctl/test_ctl.ml

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