## cool / benchmarks / aconjunctive_mu / aconjunctive_mu_generator.ml @ a80babbf

History | View | Annotate | Download (25.8 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 |
let ag psi = NU("X", const_and psi (box "X")) |

450 | |

451 |
let early_init x m = |

452 |
let conjuncts = List.map (fun i -> (NOT (AP (name x (i-1))))) (iota m) |

453 |
in ag (const_and |

454 |
(const_imp (AP ("start" ^ x)) |

455 |
(const_and (AP x) (conjoin conjuncts))) |

456 |
(const_imp (AP x) (diamond x))) |

457 | |

458 |
let rec early_psi n x i = match i with |

459 |
| 0 -> TRUE (* FIXME *) |

460 |
| _ -> |

461 |
conjoin |

462 |
[ const_or (NOT (AP (name x (n-i)))) (box (name x (n-i))) |

463 |
; const_or (AP (name x (n-i))) (const_ax "" (NOT (AP (name x (n-i))))) |

464 |
; early_psi n x (i-1) |

465 |
] |

466 | |

467 |
let rec early_c_n n x i = match i with |

468 |
| 0 -> TRUE (* FIXME *) |

469 |
| _ -> |

470 |
const_or |

471 |
(conjoin [ NOT (AP (name x (n-i))) |

472 |
; box (name x (n-i)) |

473 |
; early_psi n x (i-1)]) |

474 |
(conjoin [ (AP (name x (n-i))) |

475 |
; const_ax "" (NOT (AP (name x (n-i)))) |

476 |
; early_c_n n x (i-1) ]) |

477 | |

478 |
let early_c x n = early_c_n n x n |

479 | |

480 |
let pow2 x = 1 lsl x |

481 | |

482 |
let bitlist j x = List.map (fun i -> x land (1 lsl (i-1)) <> 0) (iota j) |

483 | |

484 |
let early_bin r j i = |

485 |
conjoin |

486 |
(List.mapi |

487 |
(fun i bit -> if bit then (AP (name r i)) else (NOT (AP (name r i)))) |

488 |
(bitlist j i)) |

489 | |

490 |
let early_theta j = |

491 |
let n = pow2 j in |

492 |
let inside i = const_and (early_bin "r" j (i-1)) (diamond (name "X" i)) in |

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

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

495 |
let rec wrap fix_lit i f = |

496 |
if i > n then f |

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

498 |
in |

499 |
wrap false 1 under_the_fixes |

500 |
(* let early_theta _ = MU ("Y", (const_or (AP "p") (diamond "Y"))) *) |

501 | |

502 |
let early_ac n j k = |

503 |
conjoin |

504 |
[ (AP "startp") |

505 |
; early_init "p" n |

506 |
; early_init "r" k |

507 |
; ag (const_and |

508 |
(const_imp (AP "r") (early_c "r" k)) |

509 |
(const_imp (AP "p") (early_c "p" n))) |

510 |
; ag (conjoin |

511 |
[ const_imp |

512 |
(conjoin (List.map (fun i -> AP (name "p" (i - 1))) (iota (min j n)))) |

513 |
(const_ex "" (const_and (AP "startr") (early_theta k))) |

514 |
; NOT (const_and (AP "p") (AP "r")) |

515 |
; const_imp (AP "r") (box "r") |

516 |
] |

517 |
) |

518 |
] |

519 | |

520 |
let af psi = MU("Y", const_or psi (box "Y")) |

521 | |

522 |
let early_caching_ac n j k = |

523 |
conjoin |

524 |
[ early_ac n j k |

525 |
; (AP "b") |

526 |
; early_init "q" n |

527 |
; ag (conjoin [ NOT (const_and (AP "p") (AP "q")) |

528 |
; NOT (const_and (AP "q") (AP "r")) |

529 |
; const_imp (AP "q") (early_c "q" n) |

530 |
]) |

531 |
; ag (const_and (af (AP "b")) (const_imp (AP "b") |

532 |
(conjoin [ diamond "p" |

533 |
; diamond "startq" |

534 |
; const_ax "" (NOT (AP "b"))]) |

535 |
)) |

536 |
] |

537 | |

538 |
exception CTLException of string |

539 | |

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

541 |
@param f A formula. |

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

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

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

545 |
*) |

546 |
let exportMLSolver f = |

547 |
let sb = Buffer.create 3000 in |

548 |
let rec expML = function |

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

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

551 |
| AP s -> |

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

553 |
Buffer.add_string sb s; |

554 |
end |

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

556 |
| VAR s -> |

557 |
Buffer.add_string sb " "; |

558 |
Buffer.add_string sb s; |

559 |
Buffer.add_string sb " " |

560 |
| NOT f1 -> |

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

562 |
expML f1; |

563 |
Buffer.add_string sb ")" |

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

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

566 |
expML f1; |

567 |
Buffer.add_string sb ")" |

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

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

570 |
expML f1; |

571 |
Buffer.add_string sb ")" |

572 |
| ID (f1) -> |

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

574 |
expML f1; |

575 |
Buffer.add_string sb ")" |

576 |
| EF f1 -> |

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

578 |
expML f1; |

579 |
Buffer.add_string sb ")" |

580 |
| AF f1 -> |

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

582 |
expML f1; |

583 |
Buffer.add_string sb ")" |

584 |
| EG f1 -> |

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

586 |
expML f1; |

587 |
Buffer.add_string sb ")" |

588 |
| AG f1 -> |

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

590 |
expML f1; |

591 |
Buffer.add_string sb ")" |

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

593 |
Buffer.add_string sb "("; |

594 |
expML f1; |

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

596 |
expML f2; |

597 |
Buffer.add_string sb ")" |

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

599 |
Buffer.add_string sb "("; |

600 |
expML f1; |

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

602 |
expML f2; |

603 |
Buffer.add_string sb ")" |

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

605 |
Buffer.add_string sb "("; |

606 |
expML f1; |

607 |
Buffer.add_string sb " | "; |

608 |
expML f2; |

609 |
Buffer.add_string sb ")" |

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

611 |
Buffer.add_string sb "("; |

612 |
expML f1; |

613 |
Buffer.add_string sb " & "; |

614 |
expML f2; |

615 |
Buffer.add_string sb ")" |

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

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

618 |
expML f1; |

619 |
Buffer.add_string sb " U "; |

620 |
expML f2; |

621 |
Buffer.add_string sb "))" |

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

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

624 |
expML f1; |

625 |
Buffer.add_string sb " U "; |

626 |
expML f2; |

627 |
Buffer.add_string sb "))" |

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

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

630 |
expML f1; |

631 |
Buffer.add_string sb " R "; |

632 |
expML (NOT f2); |

633 |
Buffer.add_string sb "))" |

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

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

636 |
expML f1; |

637 |
Buffer.add_string sb " R "; |

638 |
expML (NOT f2); |

639 |
Buffer.add_string sb "))" |

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

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

642 |
expML f1; |

643 |
Buffer.add_string sb ")" |

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

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

646 |
expML f1; |

647 |
Buffer.add_string sb ")" |

648 |
| _ -> raise (CTLException "exportMLSolver: Unsupported formula"); |

649 |
in |

650 |
expML f; |

651 |
Buffer.contents sb |

652 | |

653 |
let print_usage () = |

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

655 |
print_endline ""; |

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

657 |
print_endline ""; |

658 |
print_endline "FORMULA_FAMILY:"; |

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

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

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

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

663 |
print_endline " - pg_even_odd_neg: same, but negated; unsatisfiable"; |

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

665 |
print_endline " - pg_domgame_neg: same, but negated; unsatisfiable"; |

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

667 |
print_endline " - enpa_is_enba_neg: same, but negated; unsatisfiable"; |

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

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

670 |
print_endline " - enpa_to_enba_neg: same, but negated; unsatisfiable"; |

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

672 |
print_endline " - unpa_is_unba_neg: same, but negated; satisfiable"; |

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

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

675 |
print_endline " - unpa_to_unba_neg: same, but negated; satisfiable"; |

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

677 |
odd dominators; valid"; |

678 |
print_endline " - unpa_is_unba_dual_neg: same, but negated; unsatisfiable"; |

679 |
print_endline ""; |

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

681 |
print_endline ""; |

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

683 | |

684 |
let () = |

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

686 |
print_usage () |

687 |
else |

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

689 |
| "cool" -> exportFormula |

690 |
| "mlsolver" -> exportMLSolver |

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

692 |
in |

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

694 |
| "linear_dpa_is_nba" -> linear_dpa_is_nba |

695 |
| "linear_dpa_is_nba_neg" -> neg_linear_dpa_is_nba |

696 |
| "enpa_is_enba" -> enpa_is_enba |

697 |
| "enpa_is_enba_neg" -> neg_enpa_is_enba |

698 |
| "enpa_to_enba" -> enpa_to_enba |

699 |
| "enpa_to_enba_neg" -> neg_enpa_to_enba |

700 |
| "unpa_is_unba" -> unpa_is_unba |

701 |
| "unpa_is_unba_neg" -> neg_unpa_is_unba |

702 |
| "unpa_to_unba" -> unpa_to_unba |

703 |
| "unpa_to_unba_neg" -> neg_unpa_to_unba |

704 |
| "unpa_is_unba_dual" -> unpa_is_unba_dual |

705 |
| "unpa_is_unba_dual_neg" -> neg_unpa_is_unba_dual |

706 |
| "pg_even_odd" -> pg_even_odd |

707 |
| "pg_even_odd_neg" -> neg_pg_even_odd |

708 |
| "pg_domgame" -> pg_domgame |

709 |
| "pg_domgame_neg" -> neg_pg_domgame |

710 |
| "early_ac" -> fun i -> early_ac i 4 2 |

711 |
| "early_caching_ac" -> fun i -> early_caching_ac i 4 2 |

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

713 |
in |

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

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