Project

General

Profile

Revision 77f7da85

View differences:

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 mu-calculus 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 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";
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