## cool / gen.ml @ 77f7da85

History | View | Annotate | Download (22.9 KB)

1 |
open CoAlgFormula |
---|---|

2 | |

3 |
(* Generates hard aconjunctive mu-calculus formulas with deep |

4 |
nesting of fixpoints *) |

5 | |

6 |
let iota n = |

7 |
let rec intern i n = |

8 |
if i = n then [i] |

9 |
else i::intern (i+1) n |

10 |
in |

11 |
intern 1 n |

12 | |

13 |
let name n i = n ^ string_of_int i |

14 | |

15 |
(* Join a list of formulas with OR *) |

16 |
let disjoin list = match list with |

17 |
| [] -> FALSE |

18 |
| h :: tl -> List.fold_left const_or h tl |

19 | |

20 |
(* Join a list of formulas with AND *) |

21 |
let conjoin list = match list with |

22 |
| [] -> TRUE |

23 |
| h :: tl -> List.fold_left const_and h tl |

24 | |

25 |
let box name = const_ax "" (VAR name) |

26 |
let diamond name = const_ex "" (VAR name) |

27 |
let circle name = (ID (VAR name)) |

28 | |

29 |
let psi n = |

30 |
let inside i = |

31 |
let not_qis = |

32 |
List.map (fun j -> (NOT (AP (name "q" j)))) |

33 |
(List.filter (fun x -> x <> i) (iota n)) |

34 |
in |

35 |
(const_and (AP (name "q" i)) (conjoin not_qis)) |

36 |
in |

37 | |

38 |
(NU("X",const_and (circle "X") (disjoin (List.map inside (iota n))))) |

39 | |

40 |
let psi_neg n = |

41 |
let inside i = |

42 |
let qis = |

43 |
List.map (fun j -> (AP (name "q" j))) |

44 |
(List.filter (fun x -> x <> i) (iota n)) |

45 |
in |

46 |
disjoin (NOT (AP (name "q" i)) :: qis) |

47 |
in |

48 | |

49 |
(MU("X", const_or (circle "X") (conjoin (List.map inside (iota n))))) |

50 | |

51 |
let before_biimpl_neg n = |

52 |
let inside i = const_and (AP (name "q" i)) (circle (name "X" i)) in |

53 |
let under_the_fixes = disjoin (List.map inside (iota n)) in |

54 |
let fix mu x f = if mu then MU(x, f) else NU(x, f) in |

55 |
let rec wrap fix_lit i f = |

56 |
if i > n then f |

57 |
else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f) |

58 |
in |

59 |
wrap false 1 under_the_fixes |

60 | |

61 |
let before_biimpl n = |

62 |
let inside i = const_and (AP (name "q" i)) (circle (name "X" i)) in |

63 |
let under_the_fixes = disjoin (List.map inside (iota n)) in |

64 |
let fix mu x f = if mu then MU(x, f) else NU(x, f) in |

65 |
let rec wrap fix_lit i f = |

66 |
if i > n then f |

67 |
else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f) |

68 |
in |

69 |
wrap true 1 under_the_fixes |

70 | |

71 |
let isEven i = i mod 2 = 0 |

72 |
let isOdd i = i mod 2 = 1 |

73 | |

74 |
let after_biimpl n = |

75 |
let conjunct j = |

76 |
(MU("X", const_or (NU("Y", const_and (NOT (AP (name "q" j))) (circle "Y"))) |

77 |
(circle "X"))) |

78 |
in |

79 |
let disjunct i = |

80 |
let conjuncts = |

81 |
List.map conjunct (List.filter (fun j -> j > i && isOdd j) (iota n)) |

82 |
in |

83 |
let inside = |

84 |
(NU("X", const_and (MU("Y", const_or (AP (name "q" i)) (circle "Y"))) |

85 |
(circle "X"))) |

86 |
in |

87 |
(const_and inside (conjoin conjuncts)) |

88 |
in |

89 |
let disjuncts = List.map disjunct (List.filter isEven (iota n)) in |

90 |
disjoin disjuncts |

91 | |

92 |
let after_biimpl_neg n = |

93 |
let disjunct j = |

94 |
(NU("X", |

95 |
const_and |

96 |
(MU("Y", const_or (AP (name "q" j)) (circle "Y"))) |

97 |
(circle "X"))) |

98 |
in |

99 |
let conjunct i = |

100 |
let disjuncts = |

101 |
List.map disjunct (List.filter (fun j -> j > i && isOdd j) (iota n)) |

102 |
in |

103 |
let inside = |

104 |
(MU("X", |

105 |
const_or |

106 |
(NU("Y", const_and (NOT (AP (name "q" i))) (circle "Y"))) |

107 |
(circle "X"))) |

108 |
in |

109 |
(const_or inside (disjoin disjuncts)) |

110 |
in |

111 |
let conjuncts = List.map conjunct (List.filter isEven (iota n)) in |

112 |
conjoin conjuncts |

113 | |

114 |
let linear_dpa_is_nba n = |

115 |
const_or |

116 |
(psi_neg n) |

117 |
(const_and |

118 |
(const_or (before_biimpl_neg n) (after_biimpl n)) |

119 |
(const_or (before_biimpl n) (after_biimpl_neg n))) |

120 | |

121 |
let neg_linear_dpa_is_nba n = |

122 |
const_and (psi n) |

123 |
(const_or (const_and (before_biimpl n) (after_biimpl_neg n)) |

124 |
(const_and (before_biimpl_neg n) (after_biimpl n))) |

125 | |

126 |
let psi2 n = |

127 |
let inside i = |

128 |
let not_qis = |

129 |
List.map (fun j -> (NOT (AP (name "q" j)))) |

130 |
(List.filter (fun x -> x <> i) (iota n)) |

131 |
in |

132 |
(const_and (AP (name "q" i)) (conjoin not_qis)) |

133 |
in |

134 | |

135 |
(const_and (NU("X",const_and (box "X") (disjoin (List.map inside (iota n))))) |

136 |
(NU("X",const_and (box "X") (const_or (const_and (NOT (AP (name "q" (n+2)))) |

137 |
(AP (name "q" (n+1)))) (const_and (NOT (AP (name "q" (n+1)))) (AP (name "q" (n+2)))))))) |

138 | |

139 |
let psi_neg2 n = |

140 |
let inside i = |

141 |
let qis = |

142 |
List.map (fun j -> (AP (name "q" j))) |

143 |
(List.filter (fun x -> x <> i) (iota n)) |

144 |
in |

145 |
disjoin (NOT (AP (name "q" i)) :: qis) |

146 |
in |

147 | |

148 |
(const_or (MU("X",const_or (diamond "X") (conjoin (List.map inside (iota n))))) |

149 |
(MU("X",const_or (diamond "X") (const_and (const_or (NOT (AP (name "q" (n+1)))) |

150 |
(AP (name "q" (n+2)))) (const_or (NOT (AP (name "q" (n+2)))) (AP (name "q" (n+1)))))))) |

151 | |

152 |
let pgwin n = |

153 |
let inside_e i = const_and (AP (name "q" i)) (diamond (name "X" i)) in |

154 |
let inside_a i = const_and (AP (name "q" i)) (box (name "X" i)) in |

155 |
let under_the_fixes = (const_or (const_and ((AP (name "q" (n+2)))) (disjoin (List.map inside_e (iota n)))) |

156 |
(const_and ((AP (name "q" (n+1)))) (disjoin (List.map inside_a (iota n))))) in |

157 |
let fix mu x f = if mu then MU(x, f) else NU(x, f) in |

158 |
let rec wrap fix_lit i f = |

159 |
if i > n then f |

160 |
else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f) |

161 |
in |

162 |
wrap true 1 under_the_fixes |

163 | |

164 |
let pglose n = |

165 |
let inside_e i = const_and (AP (name "q" i)) (box (name "X" i)) in |

166 |
let inside_a i = const_and (AP (name "q" i)) (diamond (name "X" i)) in |

167 |
let under_the_fixes = (const_or (const_and ((AP (name "q" (n+2)))) (disjoin (List.map inside_e (iota n)))) |

168 |
(const_and ((AP (name "q" (n+1)))) (disjoin (List.map inside_a (iota n))))) in |

169 |
let fix mu x f = if mu then MU(x, f) else NU(x, f) in |

170 |
let rec wrap fix_lit i f = |

171 |
if i > n then f |

172 |
else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f) |

173 |
in |

174 |
wrap false 1 under_the_fixes |

175 | |

176 |
let egwin n = |

177 |
let disjunct_ee i = const_and (AP (name "q" i)) (diamond "X") in |

178 |
let disjunct_eo i = const_and (AP (name "q" i)) (diamond "Y") in |

179 |
let disjunct_ae i = const_and (AP (name "q" i)) (box "X") in |

180 |
let disjunct_ao i = const_and (AP (name "q" i)) (box "Y") in |

181 |
let disjuncts_ee = List.map disjunct_ee (List.filter isEven (iota n)) in |

182 |
let disjuncts_eo = List.map disjunct_eo (List.filter isOdd (iota n)) in |

183 |
let disjuncts_ae = List.map disjunct_ae (List.filter isEven (iota n)) in |

184 |
let disjuncts_ao = List.map disjunct_ao (List.filter isOdd (iota n)) in |

185 | |

186 |
(NU("X",MU("Y",const_or (const_and ((AP (name "q" (n+2)))) (const_or (disjoin disjuncts_ee) (disjoin disjuncts_eo) )) |

187 |
(const_and ((AP (name "q" (n+1)))) (const_or (disjoin disjuncts_ae) (disjoin disjuncts_ao) )) ))) |

188 | |

189 |
let eglose n = |

190 |
let disjunct_ee i = const_and (AP (name "q" i)) (box "X") in |

191 |
let disjunct_eo i = const_and (AP (name "q" i)) (box "Y") in |

192 |
let disjunct_ae i = const_and (AP (name "q" i)) (diamond "X") in |

193 |
let disjunct_ao i = const_and (AP (name "q" i)) (diamond "Y") in |

194 |
let disjuncts_ee = List.map disjunct_ee (List.filter isEven (iota n)) in |

195 |
let disjuncts_eo = List.map disjunct_eo (List.filter isOdd (iota n)) in |

196 |
let disjuncts_ae = List.map disjunct_ae (List.filter isEven (iota n)) in |

197 |
let disjuncts_ao = List.map disjunct_ao (List.filter isOdd (iota n)) in |

198 | |

199 |
(MU("X",NU("Y",const_or (const_and ((AP (name "q" (n+2)))) (const_or (disjoin disjuncts_ee) (disjoin disjuncts_eo) )) |

200 |
(const_and ((AP (name "q" (n+1)))) (const_or (disjoin disjuncts_ae) (disjoin disjuncts_ao) )) ))) |

201 | |

202 |
let pg_even_odd n = |

203 |
const_or |

204 |
(psi_neg2 n) |

205 |
(const_or |

206 |
(pglose n) |

207 |
(egwin n)) |

208 | |

209 |
let neg_pg_even_odd n = |

210 |
const_and (psi2 n) |

211 |
(const_and (pgwin n) |

212 |
(eglose n)) |

213 | |

214 | |

215 |
let dgwin n = |

216 |
let disjunct_eg i = const_and (AP (name "q" i)) (diamond "X") in |

217 |
let disjunct_el i = const_and (AP (name "q" i)) (diamond "Z") in |

218 |
let disjunct_ag i = const_and (AP (name "q" i)) (box "X") in |

219 |
let disjunct_al i = const_and (AP (name "q" i)) (box "Z") in |

220 |
let disjuncts_eg i = List.map disjunct_eg (List.filter (fun j -> j > i) (iota n)) in |

221 |
let disjuncts_el i = List.map disjunct_el (List.filter (fun j -> j < i) (iota n)) in |

222 |
let disjuncts_ag i = List.map disjunct_ag (List.filter (fun j -> j > i) (iota n)) in |

223 |
let disjuncts_al i = List.map disjunct_al (List.filter (fun j -> j < i) (iota n)) in |

224 |
let dom_game n i = (NU("X",(MU("Y",NU("Z", (const_or (const_and (AP (name "q" (n+2))) |

225 |
(const_or (const_and (AP (name "q" i)) (diamond "Y")) |

226 |
(const_or (disjoin (disjuncts_eg i)) (disjoin |

227 |
(disjuncts_el i)))) ) (const_and (AP (name "q" (n+1))) (const_or (const_and (AP (name "q" i)) (box "Y")) |

228 |
(const_or (disjoin (disjuncts_ag i)) (disjoin (disjuncts_al i)) )) ))))))) in |

229 |
let conjuncts = List.map (dom_game n) (List.filter isOdd (iota n)) in |

230 | |

231 |
conjoin conjuncts |

232 | |

233 |
let dglose n = |

234 |
let disjunct_eg i = const_and (AP (name "q" i)) (diamond "X") in |

235 |
let disjunct_el i = const_and (AP (name "q" i)) (diamond "Z") in |

236 |
let disjunct_ag i = const_and (AP (name "q" i)) (box "X") in |

237 |
let disjunct_al i = const_and (AP (name "q" i)) (box "Z") in |

238 |
let disjuncts_eg i = List.map disjunct_eg (List.filter (fun j -> j > i) (iota n)) in |

239 |
let disjuncts_el i = List.map disjunct_el (List.filter (fun j -> j < i) (iota n)) in |

240 |
let disjuncts_ag i = List.map disjunct_ag (List.filter (fun j -> j > i) (iota n)) in |

241 |
let disjuncts_al i = List.map disjunct_al (List.filter (fun j -> j < i) (iota n)) in |

242 |
let neg_dom_game n i = (MU("X",(NU("Y",MU("Z", (const_or (const_and (AP (name "q" (n+2))) |

243 |
(const_or (const_and (AP (name "q" i)) (box "Y")) |

244 |
(const_or (disjoin (disjuncts_ag i)) (disjoin |

245 |
(disjuncts_al i)))) ) (const_and (AP (name "q" (n+1))) (const_or (const_and (AP (name "q" i)) (diamond "Y")) |

246 |
(const_or (disjoin (disjuncts_eg i)) (disjoin (disjuncts_el i)) )) ))))))) in |

247 |
let disjuncts = List.map (neg_dom_game n) (List.filter isOdd (iota n)) in |

248 | |

249 |
disjoin disjuncts |

250 | |

251 |
let pg_domgame n = |

252 |
const_or |

253 |
(psi_neg2 n) |

254 |
(const_or |

255 |
(pglose n) |

256 |
(dgwin n)) |

257 | |

258 |
let neg_pg_domgame n = |

259 |
const_and (psi2 n) |

260 |
(const_and (pgwin n) |

261 |
(dglose n)) |

262 | |

263 | |

264 |
let psi3 n = |

265 |
let inside i = |

266 |
let not_qis = |

267 |
List.map (fun j -> (NOT (AP (name "q" j)))) |

268 |
(List.filter (fun x -> x <> i) (iota n)) |

269 |
in |

270 |
(const_and (AP (name "q" i)) (conjoin not_qis)) |

271 |
in |

272 | |

273 |
(NU("X",const_and (box "X") (disjoin (List.map inside (iota n))))) |

274 | |

275 |
let psi_neg3 n = |

276 |
let inside i = |

277 |
let qis = |

278 |
List.map (fun j -> (AP (name "q" j))) |

279 |
(List.filter (fun x -> x <> i) (iota n)) |

280 |
in |

281 |
disjoin (NOT (AP (name "q" i)) :: qis) |

282 |
in |

283 | |

284 |
(MU("X",const_or (diamond "X") (conjoin (List.map inside (iota n))))) |

285 | |

286 |
let epa_acc n = |

287 |
let inside_e i = const_and (AP (name "q" i)) (diamond (name "X" i)) in |

288 |
let under_the_fixes = disjoin (List.map inside_e (iota n)) in |

289 |
let fix mu x f = if mu then MU(x, f) else NU(x, f) in |

290 |
let rec wrap fix_lit i f = |

291 |
if i > n then f |

292 |
else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f) |

293 |
in |

294 |
wrap true 1 under_the_fixes |

295 | |

296 |
let epa_nacc n = |

297 |
let inside_a i = const_and (AP (name "q" i)) (box (name "X" i)) in |

298 |
let under_the_fixes = disjoin (List.map inside_a (iota n)) in |

299 |
let fix mu x f = if mu then MU(x, f) else NU(x, f) in |

300 |
let rec wrap fix_lit i f = |

301 |
if i > n then f |

302 |
else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f) |

303 |
in |

304 |
wrap false 1 under_the_fixes |

305 | |

306 |
let enba_acc n = |

307 |
let disjunct_eg i = const_and (AP (name "q" i)) (diamond "X") in |

308 |
let disjunct_el i = const_and (AP (name "q" i)) (diamond "Z") in |

309 |
let disjuncts_eg i = List.map disjunct_eg (List.filter (fun j -> j > i) (iota n)) in |

310 |
let disjuncts_el i = List.map disjunct_el (List.filter (fun j -> j < i) (iota n)) in |

311 |
let dom_aut i = (MU("X",(NU("Y",MU("Z", (const_or (const_and (AP (name "q" i)) (diamond "Y")) |

312 |
(const_or (disjoin (disjuncts_eg i)) (disjoin (disjuncts_el i)) )) ))))) in |

313 |
let disjuncts = List.map dom_aut (List.filter isEven (iota n)) in |

314 | |

315 |
disjoin disjuncts |

316 | |

317 |
let enba_nacc n = |

318 |
let disjunct_ag i = const_and (AP (name "q" i)) (box "X") in |

319 |
let disjunct_al i = const_and (AP (name "q" i)) (box "Z") in |

320 |
let disjuncts_ag i = List.map disjunct_ag (List.filter (fun j -> j > i) (iota n)) in |

321 |
let disjuncts_al i = List.map disjunct_al (List.filter (fun j -> j < i) (iota n)) in |

322 |
let neg_dom_aut i = (NU("X",(MU("Y",NU("Z", (const_or (const_and (AP (name "q" i)) (box "Y")) (const_or (disjoin (disjuncts_ag i)) (disjoin (disjuncts_al i)) )) ))))) in |

323 |
let conjuncts = List.map neg_dom_aut (List.filter isEven (iota n)) in |

324 | |

325 |
conjoin conjuncts |

326 | |

327 |
let enpa_is_enba n = |

328 |
const_or |

329 |
(psi_neg3 n) |

330 |
(const_and |

331 |
(const_or (epa_nacc n) (enba_acc n)) |

332 |
(const_or (epa_acc n) (enba_nacc n))) |

333 | |

334 |
let neg_enpa_is_enba n = |

335 |
const_and (psi3 n) |

336 |
(const_or (const_and (epa_acc n) (enba_nacc n)) |

337 |
(const_and (epa_nacc n) (enba_acc n))) |

338 | |

339 |
let enpa_to_enba n = |

340 |
const_or |

341 |
(psi_neg3 n) |

342 |
(const_or |

343 |
(epa_nacc n) |

344 |
(enba_acc n)) |

345 | |

346 |
let neg_enpa_to_enba n = |

347 |
const_and (psi3 n) |

348 |
(const_and (epa_acc n) |

349 |
(enba_nacc n)) |

350 | |

351 |
let upa_acc n = |

352 |
let inside_a i = const_and (AP (name "q" i)) (box (name "X" i)) in |

353 |
let under_the_fixes = disjoin (List.map inside_a (iota n)) in |

354 |
let fix mu x f = if mu then MU(x, f) else NU(x, f) in |

355 |
let rec wrap fix_lit i f = |

356 |
if i > n then f |

357 |
else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f) |

358 |
in |

359 |
wrap true 1 under_the_fixes |

360 | |

361 |
let upa_nacc n = |

362 |
let inside_e i = const_and (AP (name "q" i)) (diamond (name "X" i)) in |

363 |
let under_the_fixes = disjoin (List.map inside_e (iota n)) in |

364 |
let fix mu x f = if mu then MU(x, f) else NU(x, f) in |

365 |
let rec wrap fix_lit i f = |

366 |
if i > n then f |

367 |
else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f) |

368 |
in |

369 |
wrap false 1 under_the_fixes |

370 | |

371 |
let unba_acc n = |

372 |
let disjunct_ag i = const_and (AP (name "q" i)) (box "X") in |

373 |
let disjunct_al i = const_and (AP (name "q" i)) (box "Z") in |

374 |
let disjuncts_ag i = List.map disjunct_ag (List.filter (fun j -> j > i) (iota n)) in |

375 |
let disjuncts_al i = List.map disjunct_al (List.filter (fun j -> j < i) (iota n)) in |

376 |
let dom_aut i = (MU("X",(NU("Y",MU("Z", (const_or (const_and (AP (name "q" i)) (box "Y")) |

377 |
(const_or (disjoin (disjuncts_ag i)) (disjoin (disjuncts_al i)) )) ))))) in |

378 |
let disjuncts = List.map dom_aut (List.filter isEven (iota n)) in |

379 | |

380 |
disjoin disjuncts |

381 | |

382 |
let unba_nacc n = |

383 |
let disjunct_eg i = const_and (AP (name "q" i)) (diamond "X") in |

384 |
let disjunct_el i = const_and (AP (name "q" i)) (diamond "Z") in |

385 |
let disjuncts_eg i = List.map disjunct_eg (List.filter (fun j -> j > i) (iota n)) in |

386 |
let disjuncts_el i = List.map disjunct_el (List.filter (fun j -> j < i) (iota n)) in |

387 |
let neg_dom_aut i = (NU("X",(MU("Y",NU("Z", (const_or (const_and (AP (name "q" i)) (diamond "Y")) (const_or (disjoin (disjuncts_eg i)) (disjoin (disjuncts_el i)) )) ))))) in |

388 |
let conjuncts = List.map neg_dom_aut (List.filter isEven (iota n)) in |

389 | |

390 |
conjoin conjuncts |

391 | |

392 |
let unpa_is_unba n = |

393 |
const_or |

394 |
(psi_neg3 n) |

395 |
(const_and |

396 |
(const_or (upa_nacc n) (unba_acc n)) |

397 |
(const_or (upa_acc n) (unba_nacc n))) |

398 | |

399 |
let neg_unpa_is_unba n = |

400 |
const_and (psi3 n) |

401 |
(const_or (const_and (upa_acc n) (unba_nacc n)) |

402 |
(const_and (upa_nacc n) (unba_acc n))) |

403 | |

404 |
let unpa_to_unba n = |

405 |
const_or |

406 |
(psi_neg3 n) |

407 |
(const_or |

408 |
(upa_nacc n) |

409 |
(unba_acc n)) |

410 | |

411 |
let neg_unpa_to_unba n = |

412 |
const_and (psi3 n) |

413 |
(const_and (upa_acc n) |

414 |
(unba_nacc n)) |

415 | |

416 |
let unba_acc_dual n = |

417 |
let disjunct_ag i = const_and (AP (name "q" i)) (box "X") in |

418 |
let disjunct_al i = const_and (AP (name "q" i)) (box "Z") in |

419 |
let disjuncts_ag i = List.map disjunct_ag (List.filter (fun j -> j > i) (iota n)) in |

420 |
let disjuncts_al i = List.map disjunct_al (List.filter (fun j -> j < i) (iota n)) in |

421 |
let dom_aut i = (NU("X",(MU("Y",NU("Z", (const_or (const_and (AP (name "q" i)) (box "Y")) |

422 |
(const_or (disjoin (disjuncts_ag i)) (disjoin (disjuncts_al i)) )) ))))) in |

423 |
let conjuncts = List.map dom_aut (List.filter isOdd (iota n)) in |

424 | |

425 |
conjoin conjuncts |

426 | |

427 |
let unba_nacc_dual n = |

428 |
let disjunct_eg i = const_and (AP (name "q" i)) (diamond "X") in |

429 |
let disjunct_el i = const_and (AP (name "q" i)) (diamond "Z") in |

430 |
let disjuncts_eg i = List.map disjunct_eg (List.filter (fun j -> j > i) (iota n)) in |

431 |
let disjuncts_el i = List.map disjunct_el (List.filter (fun j -> j < i) (iota n)) in |

432 |
let neg_dom_aut i = (MU("X",(NU("Y",MU("Z", (const_or (const_and (AP (name "q" i)) (diamond "Y")) (const_or (disjoin (disjuncts_eg i)) (disjoin (disjuncts_el i)) )) ))))) in |

433 |
let disjuncts = List.map neg_dom_aut (List.filter isOdd (iota n)) in |

434 | |

435 |
disjoin disjuncts |

436 | |

437 |
let unpa_is_unba_dual n = |

438 |
const_or |

439 |
(psi_neg3 n) |

440 |
(const_and |

441 |
(const_or (upa_nacc n) (unba_acc_dual n)) |

442 |
(const_or (upa_acc n) (unba_nacc_dual n))) |

443 | |

444 |
let neg_unpa_is_unba_dual n = |

445 |
const_and (psi3 n) |

446 |
(const_or (const_and (upa_acc n) (unba_nacc_dual n)) |

447 |
(const_and (upa_nacc n) (unba_acc_dual n))) |

448 | |

449 | |

450 |
exception CTLException of string |

451 | |

452 |
(** Converts a formula into a string representation for MLSolver. |

453 |
@param f A formula. |

454 |
@return A string representing f for MLSolver. |

455 |
@raise CTLException If the name of an atomic program |

456 |
or a propositional variable in f is "tt" or "ff". |

457 |
*) |

458 |
let exportMLSolver f = |

459 |
let sb = Buffer.create 3000 in |

460 |
let rec expML = function |

461 |
| TRUE -> Buffer.add_string sb "(tt)" |

462 |
| FALSE -> Buffer.add_string sb "(ff)" |

463 |
| AP s -> |

464 |
if s <> "tt" && s <> "ff" then begin |

465 |
Buffer.add_string sb s; |

466 |
end |

467 |
else raise (CTLException "Formula contains ff or tt.") |

468 |
| VAR s -> |

469 |
Buffer.add_string sb " "; |

470 |
Buffer.add_string sb s; |

471 |
Buffer.add_string sb " " |

472 |
| NOT f1 -> |

473 |
Buffer.add_string sb "(!"; |

474 |
expML f1; |

475 |
Buffer.add_string sb ")" |

476 |
| EX (_, f1) -> |

477 |
Buffer.add_string sb "(<>"; |

478 |
expML f1; |

479 |
Buffer.add_string sb ")" |

480 |
| AX (_, f1) -> |

481 |
Buffer.add_string sb "([]"; |

482 |
expML f1; |

483 |
Buffer.add_string sb ")" |

484 |
| ID (f1) -> |

485 |
Buffer.add_string sb "(()"; |

486 |
expML f1; |

487 |
Buffer.add_string sb ")" |

488 |
| EF f1 -> |

489 |
Buffer.add_string sb "(E F"; |

490 |
expML f1; |

491 |
Buffer.add_string sb ")" |

492 |
| AF f1 -> |

493 |
Buffer.add_string sb "(A F"; |

494 |
expML f1; |

495 |
Buffer.add_string sb ")" |

496 |
| EG f1 -> |

497 |
Buffer.add_string sb "(E G"; |

498 |
expML f1; |

499 |
Buffer.add_string sb ")" |

500 |
| AG f1 -> |

501 |
Buffer.add_string sb "(A G"; |

502 |
expML f1; |

503 |
Buffer.add_string sb ")" |

504 |
| EQU (f1, f2) -> |

505 |
Buffer.add_string sb "("; |

506 |
expML f1; |

507 |
Buffer.add_string sb " <==> "; |

508 |
expML f2; |

509 |
Buffer.add_string sb ")" |

510 |
| IMP (f1, f2) -> |

511 |
Buffer.add_string sb "("; |

512 |
expML f1; |

513 |
Buffer.add_string sb " ==> "; |

514 |
expML f2; |

515 |
Buffer.add_string sb ")" |

516 |
| OR (f1, f2) -> |

517 |
Buffer.add_string sb "("; |

518 |
expML f1; |

519 |
Buffer.add_string sb " | "; |

520 |
expML f2; |

521 |
Buffer.add_string sb ")" |

522 |
| AND (f1, f2) -> |

523 |
Buffer.add_string sb "("; |

524 |
expML f1; |

525 |
Buffer.add_string sb " & "; |

526 |
expML f2; |

527 |
Buffer.add_string sb ")" |

528 |
| EU (f1, f2) -> |

529 |
Buffer.add_string sb "(E ("; |

530 |
expML f1; |

531 |
Buffer.add_string sb " U "; |

532 |
expML f2; |

533 |
Buffer.add_string sb "))" |

534 |
| AU (f1, f2) -> |

535 |
Buffer.add_string sb "(A ("; |

536 |
expML f1; |

537 |
Buffer.add_string sb " U "; |

538 |
expML f2; |

539 |
Buffer.add_string sb "))" |

540 |
| EB (f1, f2) -> |

541 |
Buffer.add_string sb "(E ("; |

542 |
expML f1; |

543 |
Buffer.add_string sb " R "; |

544 |
expML (NOT f2); |

545 |
Buffer.add_string sb "))" |

546 |
| AB (f1, f2) -> |

547 |
Buffer.add_string sb "(A ("; |

548 |
expML f1; |

549 |
Buffer.add_string sb " R "; |

550 |
expML (NOT f2); |

551 |
Buffer.add_string sb "))" |

552 |
| NU (var, f1) -> |

553 |
Buffer.add_string sb ("(nu " ^ var ^ ". "); |

554 |
expML f1; |

555 |
Buffer.add_string sb ")" |

556 |
| MU (var, f1) -> |

557 |
Buffer.add_string sb ("(mu " ^ var ^ ". "); |

558 |
expML f1; |

559 |
Buffer.add_string sb ")" |

560 |
in |

561 |
expML f; |

562 |
Buffer.contents sb |

563 | |

564 |
let print_usage () = |

565 |
print_endline ("Usage: " ^ Sys.argv.(0) ^ " SYNTAX FORMULA_FAMILY n"); |

566 |
print_endline ""; |

567 |
print_endline "SYNTAX: Either 'cool' or 'mlsolver'"; |

568 |
print_endline ""; |

569 |
print_endline "FORMULA_FAMILY:"; |

570 |
print_endline " - linear_dpa_is_nba: linear parity condition is |

571 |
nondet. büchi condition [1]; valid"; |

572 |
print_endline " - linear_dpa_is_nba_neg: same, but negated; unsatisfiable"; |

573 |
print_endline " - pg_even_odd: parity games are more expressive than even-odd games; valid"; |

574 |
print_endline " - pg_even_odd_neg: same, bug negated; unsatisfiable"; |

575 |
print_endline " - pg_domgame: parity games are more expressive than dominator games; valid"; |

576 |
print_endline " - pg_domgame_neg: same, bug negated; unsatisfiable"; |

577 |
print_endline " - enpa_is_enba: transform ex. npa to equivalent ex. nba; valid"; |

578 |
print_endline " - enpa_is_enba_neg: same, bug negated; unsatisfiable"; |

579 |
print_endline " - enpa_to_enba: ex. npa implies ex. nba |

580 |
(left-to-right direction of enpa_is_enba); valid"; |

581 |
print_endline " - enpa_to_enba_neg: same, bug negated; unsatisfiable"; |

582 |
print_endline " - unpa_is_unba: transform univ. npa to equivalent univ. nba; valid"; |

583 |
print_endline " - unpa_is_unba_neg: same, bug negated; satisfiable"; |

584 |
print_endline " - unpa_to_unba: univ. npa implies univ. nba |

585 |
(left-to-right direction of unpa_is_unba); valid"; |

586 |
print_endline " - unpa_to_unba_neg: same, bug negated; satisfiable"; |

587 |
print_endline " - unpa_is_unba_dual: dual formulation of unpa_is_unba, with |

588 |
odd dominators; valid"; |

589 |
print_endline " - unpa_is_unba_dual_neg: same, bug negated; unsatisfiable"; |

590 |
print_endline ""; |

591 |
print_endline "n: Index of the formula in the family"; |

592 |
print_endline ""; |

593 |
print_endline "[1]: http://files.oliverfriedmann.de/papers/a_solver_for_modal_fixpoint_logics.pdf, page 7" |

594 | |

595 |
let () = |

596 |
if Array.length Sys.argv <> 4 then |

597 |
print_usage () |

598 |
else |

599 |
let syntax = match Sys.argv.(1) with |

600 |
| "cool" -> exportFormula |

601 |
| "mlsolver" -> exportMLSolver |

602 |
| _ -> print_usage (); exit 1 |

603 |
in |

604 |
let family = match Sys.argv.(2) with |

605 |
| "linear_dpa_is_nba" -> linear_dpa_is_nba |

606 |
| "linear_dpa_is_nba_neg" -> neg_linear_dpa_is_nba |

607 |
| "enpa_is_enba" -> enpa_is_enba |

608 |
| "enpa_is_enba_neg" -> neg_enpa_is_enba |

609 |
| "enpa_to_enba" -> enpa_to_enba |

610 |
| "enpa_to_enba_neg" -> neg_enpa_to_enba |

611 |
| "unpa_is_unba" -> unpa_is_unba |

612 |
| "unpa_is_unba_neg" -> neg_unpa_is_unba |

613 |
| "unpa_to_unba" -> unpa_to_unba |

614 |
| "unpa_to_unba_neg" -> neg_unpa_to_unba |

615 |
| "unpa_is_unba_dual" -> unpa_is_unba_dual |

616 |
| "unpa_is_unba_dual_neg" -> neg_unpa_is_unba_dual |

617 |
| "pg_even_odd" -> pg_even_odd |

618 |
| "pg_even_odd_neg" -> neg_pg_even_odd |

619 |
| "pg_domgame" -> pg_domgame |

620 |
| "pg_domgame_neg" -> neg_pg_domgame |

621 |
| _ -> print_usage (); exit 1 |

622 |
in |

623 |
let n = int_of_string Sys.argv.(3) in |

624 |
print_endline (syntax (family n)); |