Revision 77f7da85
gen.ml  

1  1 
open CoAlgFormula 
2  2  
3 
(* Generates formulas in the style of http://files.oliverfriedmann.de/papers/a_solver_for_modal_fixpoint_logics.pdf, page 7 *) 

3 
(* Generates hard aconjunctive mucalculus formulas with deep 

4 
nesting of fixpoints *) 

4  5  
5  6 
let iota n = 
6  7 
let rec intern i n = 
...  ...  
210  211 
(const_and (pgwin n) 
211  212 
(eglose n)) 
212  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  
213  450 
exception CTLException of string 
214  451  
215  452 
(** Converts a formula into a string representation for MLSolver. 
...  ...  
330  567 
print_endline "SYNTAX: Either 'cool' or 'mlsolver'"; 
331  568 
print_endline ""; 
332  569 
print_endline "FORMULA_FAMILY:"; 
333 
print_endline "  linear_dpa_is_nba: Formula of in the style of [1]"; 

334 
print_endline "  linear_dpa_is_nba_neg: same, but negated"; 

335 
print_endline "  pg_even_odd: TODO"; 

336 
print_endline "  pg_even_odd_neg: same, bug negated"; 

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 evenodd 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 
(lefttoright 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 
(lefttoright 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"; 

337  590 
print_endline ""; 
338  591 
print_endline "n: Index of the formula in the family"; 
339  592 
print_endline ""; 
...  ...  
351  604 
let family = match Sys.argv.(2) with 
352  605 
 "linear_dpa_is_nba" > linear_dpa_is_nba 
353  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 

354  617 
 "pg_even_odd" > pg_even_odd 
355  618 
 "pg_even_odd_neg" > neg_pg_even_odd 
619 
 "pg_domgame" > pg_domgame 

620 
 "pg_domgame_neg" > neg_pg_domgame 

356  621 
 _ > print_usage (); exit 1 
357  622 
in 
358  623 
let n = int_of_string Sys.argv.(3) in 
Also available in: Unified diff