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