Commit | Line | Data |
---|---|---|
34e49164 C |
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 | *) |