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  * 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.
  31  *
  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.
  35  *
  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.
  40  *
  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/>.
  43  *
  44  * The authors reserve the right to distribute this or future versions of
  45  * Coccinelle under other licenses.
  46  *)
  47
  48
  49
  50 (* ********************************************************************** *)
  51 (* Module: EXAMPLE_ENGINE (instance of CTL_ENGINE)                        *)
  52 (* ********************************************************************** *)
  53
  54 (* Simple env.: meta.vars and values are strings *)
  55 module SIMPLE_ENV =
  56   struct
  57     type value = string;;
  58     type mvar = string;;
  59     let eq_mvar x x' = x = x';;
  60     let eq_val v v' = v = v';;
  61     let merge_val v v' = v;;
  62   end
  63 ;;
  64
  65 (* Simple predicates *)
  66 module WRAPPER_PRED =
  67   struct
  68     type predicate = string
  69   end
  70
  71 module EXAMPLE_ENGINE =
  72   Wrapper_ctl.CTL_ENGINE_BIS (SIMPLE_ENV) (Ctl_engine.OGRAPHEXT_GRAPH) (WRAPPER_PRED)
  73
  74 let top_wit = []
  75
  76 (* ******************************************************************** *)
  77 (*                                                                      *)
  78 (* EXAMPLES                                                             *)
  79 (*                                                                      *)
  80 (* ******************************************************************** *)
  81
  82 (* For convenience in the examples *)
  83 (* FIX ME: remove *)
  84 open Ctl_engine.OGRAPHEXT_GRAPH;;
  85 open EXAMPLE_ENGINE;;
  86 open Ast_ctl;;
  87
  88 (* ---------------------------------------------------------------------- *)
  89 (* Helpers                                                                *)
  90 (* ---------------------------------------------------------------------- *)
  91
  92 (* FIX ME: move to ENGINE module *)
  93 let (-->) x v = Subst (x,v);;
  94
  95 (* FIX ME: move to ENGINE module *)
  96 let (-/->) x v = NegSubst(x,v);;
  97
  98 let mkgraph nodes edges =
  99   let g = ref (new Ograph_extended.ograph_extended) in
 100   let addn (n,x) =
 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
 104      *)
 105     let (g', i) = !g#add_nodei n x in
 106     assert (i = n);
 107     g := g'; (n,i) in
 108   let adde anodes (n1,n2,x) =
 109     let g' = (!g)#add_arc ((List.assoc n1 anodes,List.assoc n2 anodes),x) in
 110     g := g'; () in
 111   let add_nodes = List.map addn nodes in
 112   let _add_edges = List.map (adde add_nodes) edges in
 113   !g
 114 ;;
 115
 116
 117 (* CTL parameterised on basic predicates and metavar's*)
 118 type ('pred,'mvar) old_gen_ctl =
 119   | False_
 120   | True_
 121   | Pred_ of 'pred
 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
 136   | Ref_ of string
 137
 138 let rec mkanno phi0 =
 139   let anno phi = (phi,None) in
 140   match phi0 with
 141     | False_              -> anno False
 142     | True_               -> anno True
 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))
 159
 160
 161 (* ******************************************************************** *)
 162 (* Example 1                                                            *)
 163 (*   CTL: f(x) /\ AF(Ey.g(y))                                           *)
 164 (* ******************************************************************** *)
 165
 166 let ex1lab s =
 167   match s with
 168     | "f(x)" -> [(0,["x" --> "1"]); (1,["x" --> "2"])]
 169     | "g(y)" -> [(3,["y" --> "1"]); (4,["y" --> "2"])]
 170     | "f(1)" -> [(0,[])]
 171     | "f(2)" -> [(1,[])]
 172     | "g(1)" -> [(3,[])]
 173     | "g(2)" -> [(4,[])]
 174     | _ -> []
 175 ;;
 176
 177 let ex1graph =
 178   let nodes =
 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)
 182 ;;
 183
 184 let ex1states = List.map fst (ex1graph#nodes)#tolist;;
 185
 186 let ex1model = (ex1graph,ex1lab,ex1states);;
 187 let ex1model_wrapped = (ex1graph,wrap_label ex1lab,ex1states);;
 188
 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);;
 194
 195 let ex1s3a = AX_(ex1s2);;
 196 let ex1s4a = AX_(AX_(ex1s2));;
 197 let ex1s5a = And_(ex1s0,ex1s4a);;
 198
 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);;
 208
 209 let ex1s7c = And_(ex1s6b,ex1s4b);;
 210 let ex1s8c = Exists_("x",ex1s7c);;
 211
 212 let ex1phi1 = ex1s4;;
 213 let ex1phi2 = ex1s5a;;
 214 let ex1phi3 =
 215   And_
 216  (Exists_ ("x",
 217   (Exists_ ("v3",
 218     Pred_ ("f(x)", UnModif "v3")))),
 219   AX_
 220    (AF_
 221     (Exists_ ("y", (* change this to Y and have strange behaviour *)
 222       (Exists_ ("v0",
 223        Pred_ ("g(y)", Modif "v0")
 224                       ))))));;
 225
 226 let ex1phi4 =
 227   Exists_ ("x",
 228            And_ (
 229             (Exists_ ("v3",
 230                      Pred_ ("f(x)", UnModif "v3"))),
 231             AX_
 232               (AF_
 233                  (Exists_ ("y", (* change this to Y and have strange behaviour *)
 234                           (Exists_ ("v0",
 235                                    Pred_ ("g(y)", Modif "v0")
 236                                   )))))));;
 237
 238
 239 let ex1phi5 = AU_(True_,Exists_("y", Exists_("v0",Pred_("g(y)",Modif "v0"))));;
 240
 241 let ex1phi6 =
 242   AU_(
 243     Not_(Exists_("x",Exists_("v1",Pred_("f(x)",UnModif "v1")))),
 244     Exists_("y", Exists_("v0",Pred_("g(y)",Modif "v0")))
 245   );;
 246
 247 (* use with ex1nc *)
 248 let ex1phi7 =
 249   AU_(
 250     Not_(Or_(Pred_("f(1)",Control),Pred_("f(2)",Control))),
 251     Exists_("y", Exists_("v0",Pred_("g(y)",Modif "v0")))
 252   );;
 253
 254 let ex1 phi = satbis ex1model (mkanno phi);;
 255 let ex1nc phi = satbis_noclean ex1model (mkanno phi);;
 256
 257
 258 (* ******************************************************************** *)
 259 (* Example 2                                                            *)
 260 (* ******************************************************************** *)
 261
 262 let ex2lab s =
 263   match s with
 264     | "p"        -> [0,[]]
 265     | "{"        -> [(1,[]); (2,[])]
 266     | "}"        -> [(3,[]); (4,[])]
 267     | "paren(v)" -> [(1,["v" --> "1"]); (2,["v" --> "2"]);
 268                      (3,["v" --> "2"]); (4,["v" --> "1"])]
 269     | _          -> []
 270 ;;
 271
 272 let ex2graph =
 273   let nodes =
 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)
 277 ;;
 278
 279 let ex2states = List.map fst (ex2graph#nodes)#tolist;;
 280
 281 let ex2model = (ex2graph,ex2lab,ex2states);;
 282 let ex2model_wrapped = (ex2graph,wrap_label ex2lab,ex2states);;
 283
 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);;
 296
 297 let ex2phi1 = ex2s11;;
 298
 299 let ex2 phi = satbis_noclean ex2model (mkanno phi)
 300
 301 (*
 302            +--- s11:& ---+
 303            |             |
 304          s0:p         s10:AX
 305                          |
 306                      s9:exists v
 307                          |
 308            +---------- s8:& --------+
 309            |                        |
 310      +-- s3:& --+                 s7:AF
 311      |          |                   |
 312    s1:"{"     s2:paren(v)     +--  s6:& -+
 313                               |          |
 314                             s4:"}"     s5:paren(v)
 315
 316   s0 : p                   : (0,_,_)
 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))
 328 *)