### Profile

Statistics
| Branch: | Revision:

## cool / benchmarks / aconjunctive_mu / gen.ml @ 6c3793cb

1 2 3 867cefeb Hans-Peter Deifel ```open CoAlgFormula ``` 77f7da85 Daniel Hausmann ```(* Generates hard aconjunctive mu-calculus formulas with deep ``` ```nesting of fixpoints *) ``` 867cefeb Hans-Peter Deifel ```let iota n = ``` ``` let rec intern i n = ``` ``` if i = n then [i] ``` ``` else i::intern (i+1) n ``` ``` in ``` ``` intern 1 n ``` ```let name n i = n ^ string_of_int i ``` 7915d13f Hans-Peter Deifel ```(* Join a list of formulas with OR *) ``` ```let disjoin list = match list with ``` ``` | [] -> FALSE ``` ``` | h :: tl -> List.fold_left const_or h tl ``` ```(* Join a list of formulas with AND *) ``` ```let conjoin list = match list with ``` ``` | [] -> TRUE ``` ``` | h :: tl -> List.fold_left const_and h tl ``` ```let box name = const_ax "" (VAR name) ``` fdfe3dcc Hans-Peter Deifel ```let diamond name = const_ex "" (VAR name) ``` 88a1a18b Hans-Peter Deifel ```let circle name = (ID (VAR name)) ``` 7915d13f Hans-Peter Deifel c9dbb509 Hans-Peter Deifel ```let psi n = ``` ``` let inside i = ``` ``` let not_qis = ``` ``` List.map (fun j -> (NOT (AP (name "q" j)))) ``` ``` (List.filter (fun x -> x <> i) (iota n)) ``` ``` in ``` ``` (const_and (AP (name "q" i)) (conjoin not_qis)) ``` ``` in ``` 88a1a18b Hans-Peter Deifel ``` (NU("X",const_and (circle "X") (disjoin (List.map inside (iota n))))) ``` c9dbb509 Hans-Peter Deifel 7915d13f Hans-Peter Deifel ```let psi_neg n = ``` 867cefeb Hans-Peter Deifel ``` let inside i = ``` 7915d13f Hans-Peter Deifel ``` let qis = ``` ``` List.map (fun j -> (AP (name "q" j))) ``` 867cefeb Hans-Peter Deifel ``` (List.filter (fun x -> x <> i) (iota n)) ``` ``` in ``` 7915d13f Hans-Peter Deifel ``` disjoin (NOT (AP (name "q" i)) :: qis) ``` 867cefeb Hans-Peter Deifel ``` in ``` 88a1a18b Hans-Peter Deifel ``` (MU("X", const_or (circle "X") (conjoin (List.map inside (iota n))))) ``` 867cefeb Hans-Peter Deifel 7915d13f Hans-Peter Deifel ```let before_biimpl_neg n = ``` 88a1a18b Hans-Peter Deifel ``` let inside i = const_and (AP (name "q" i)) (circle (name "X" i)) in ``` 7915d13f Hans-Peter Deifel ``` let under_the_fixes = disjoin (List.map inside (iota n)) in ``` 867cefeb Hans-Peter Deifel ``` let fix mu x f = if mu then MU(x, f) else NU(x, f) in ``` ``` let rec wrap fix_lit i f = ``` ``` if i > n then f ``` ``` else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f) ``` ``` in ``` 7915d13f Hans-Peter Deifel ``` wrap false 1 under_the_fixes ``` 867cefeb Hans-Peter Deifel ae7e01ca Hans-Peter Deifel ```let before_biimpl n = ``` 88a1a18b Hans-Peter Deifel ``` let inside i = const_and (AP (name "q" i)) (circle (name "X" i)) in ``` 7915d13f Hans-Peter Deifel ``` let under_the_fixes = disjoin (List.map inside (iota n)) in ``` ae7e01ca Hans-Peter Deifel ``` let fix mu x f = if mu then MU(x, f) else NU(x, f) in ``` ``` let rec wrap fix_lit i f = ``` ``` if i > n then f ``` ``` else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f) ``` ``` in ``` 7915d13f Hans-Peter Deifel ``` wrap true 1 under_the_fixes ``` ae7e01ca Hans-Peter Deifel 867cefeb Hans-Peter Deifel ```let isEven i = i mod 2 = 0 ``` ```let isOdd i = i mod 2 = 1 ``` ```let after_biimpl n = ``` ``` let conjunct j = ``` 88a1a18b Hans-Peter Deifel ``` (MU("X", const_or (NU("Y", const_and (NOT (AP (name "q" j))) (circle "Y"))) ``` ``` (circle "X"))) ``` 867cefeb Hans-Peter Deifel ``` in ``` 7915d13f Hans-Peter Deifel ``` let disjunct i = ``` ``` let conjuncts = ``` ``` List.map conjunct (List.filter (fun j -> j > i && isOdd j) (iota n)) ``` ``` in ``` ``` let inside = ``` 88a1a18b Hans-Peter Deifel ``` (NU("X", const_and (MU("Y", const_or (AP (name "q" i)) (circle "Y"))) ``` ``` (circle "X"))) ``` 7915d13f Hans-Peter Deifel ``` in ``` ``` (const_and inside (conjoin conjuncts)) ``` ``` in ``` ``` let disjuncts = List.map disjunct (List.filter isEven (iota n)) in ``` ``` disjoin disjuncts ``` 867cefeb Hans-Peter Deifel 7915d13f Hans-Peter Deifel ```let after_biimpl_neg n = ``` ``` let disjunct j = ``` ``` (NU("X", ``` ``` const_and ``` 88a1a18b Hans-Peter Deifel ``` (MU("Y", const_or (AP (name "q" j)) (circle "Y"))) ``` ``` (circle "X"))) ``` 7915d13f Hans-Peter Deifel ``` in ``` ``` let conjunct i = ``` ``` let disjuncts = ``` ``` List.map disjunct (List.filter (fun j -> j > i && isOdd j) (iota n)) ``` ``` in ``` ``` let inside = ``` ``` (MU("X", ``` ``` const_or ``` 88a1a18b Hans-Peter Deifel ``` (NU("Y", const_and (NOT (AP (name "q" i))) (circle "Y"))) ``` ``` (circle "X"))) ``` 7915d13f Hans-Peter Deifel ``` in ``` ``` (const_or inside (disjoin disjuncts)) ``` ``` in ``` ``` let conjuncts = List.map conjunct (List.filter isEven (iota n)) in ``` ``` conjoin conjuncts ``` 867cefeb Hans-Peter Deifel 682787c5 Hans-Peter Deifel ```let linear_dpa_is_nba n = ``` 7915d13f Hans-Peter Deifel ``` const_or ``` ``` (psi_neg n) ``` ``` (const_and ``` ``` (const_or (before_biimpl_neg n) (after_biimpl n)) ``` ``` (const_or (before_biimpl n) (after_biimpl_neg n))) ``` 682787c5 Hans-Peter Deifel ```let neg_linear_dpa_is_nba n = ``` c9dbb509 Hans-Peter Deifel ``` const_and (psi n) ``` ``` (const_or (const_and (before_biimpl n) (after_biimpl_neg n)) ``` ``` (const_and (before_biimpl_neg n) (after_biimpl n))) ``` 867cefeb Hans-Peter Deifel fdfe3dcc Hans-Peter Deifel ```let psi2 n = ``` ``` let inside i = ``` ``` let not_qis = ``` ``` List.map (fun j -> (NOT (AP (name "q" j)))) ``` ``` (List.filter (fun x -> x <> i) (iota n)) ``` ``` in ``` ``` (const_and (AP (name "q" i)) (conjoin not_qis)) ``` ``` in ``` ``` (const_and (NU("X",const_and (box "X") (disjoin (List.map inside (iota n))))) ``` ``` (NU("X",const_and (box "X") (const_or (const_and (NOT (AP (name "q" (n+2)))) ``` ``` (AP (name "q" (n+1)))) (const_and (NOT (AP (name "q" (n+1)))) (AP (name "q" (n+2)))))))) ``` ```let psi_neg2 n = ``` ``` let inside i = ``` ``` let qis = ``` ``` List.map (fun j -> (AP (name "q" j))) ``` ``` (List.filter (fun x -> x <> i) (iota n)) ``` ``` in ``` ``` disjoin (NOT (AP (name "q" i)) :: qis) ``` ``` in ``` ``` (const_or (MU("X",const_or (diamond "X") (conjoin (List.map inside (iota n))))) ``` ``` (MU("X",const_or (diamond "X") (const_and (const_or (NOT (AP (name "q" (n+1)))) ``` ``` (AP (name "q" (n+2)))) (const_or (NOT (AP (name "q" (n+2)))) (AP (name "q" (n+1)))))))) ``` ```let pgwin n = ``` ``` let inside_e i = const_and (AP (name "q" i)) (diamond (name "X" i)) in ``` ``` let inside_a i = const_and (AP (name "q" i)) (box (name "X" i)) in ``` ``` let under_the_fixes = (const_or (const_and ((AP (name "q" (n+2)))) (disjoin (List.map inside_e (iota n)))) ``` ``` (const_and ((AP (name "q" (n+1)))) (disjoin (List.map inside_a (iota n))))) in ``` ``` let fix mu x f = if mu then MU(x, f) else NU(x, f) in ``` ``` let rec wrap fix_lit i f = ``` ``` if i > n then f ``` ``` else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f) ``` ``` in ``` ``` wrap true 1 under_the_fixes ``` ```let pglose n = ``` ``` let inside_e i = const_and (AP (name "q" i)) (box (name "X" i)) in ``` ``` let inside_a i = const_and (AP (name "q" i)) (diamond (name "X" i)) in ``` ``` let under_the_fixes = (const_or (const_and ((AP (name "q" (n+2)))) (disjoin (List.map inside_e (iota n)))) ``` ``` (const_and ((AP (name "q" (n+1)))) (disjoin (List.map inside_a (iota n))))) in ``` ``` let fix mu x f = if mu then MU(x, f) else NU(x, f) in ``` ``` let rec wrap fix_lit i f = ``` ``` if i > n then f ``` ``` else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f) ``` ``` in ``` ``` wrap false 1 under_the_fixes ``` ```let egwin n = ``` ``` let disjunct_ee i = const_and (AP (name "q" i)) (diamond "X") in ``` ``` let disjunct_eo i = const_and (AP (name "q" i)) (diamond "Y") in ``` ``` let disjunct_ae i = const_and (AP (name "q" i)) (box "X") in ``` ``` let disjunct_ao i = const_and (AP (name "q" i)) (box "Y") in ``` ``` let disjuncts_ee = List.map disjunct_ee (List.filter isEven (iota n)) in ``` ``` let disjuncts_eo = List.map disjunct_eo (List.filter isOdd (iota n)) in ``` ``` let disjuncts_ae = List.map disjunct_ae (List.filter isEven (iota n)) in ``` ``` let disjuncts_ao = List.map disjunct_ao (List.filter isOdd (iota n)) in ``` ``` (NU("X",MU("Y",const_or (const_and ((AP (name "q" (n+2)))) (const_or (disjoin disjuncts_ee) (disjoin disjuncts_eo) )) ``` ``` (const_and ((AP (name "q" (n+1)))) (const_or (disjoin disjuncts_ae) (disjoin disjuncts_ao) )) ))) ``` ```let eglose n = ``` ``` let disjunct_ee i = const_and (AP (name "q" i)) (box "X") in ``` ``` let disjunct_eo i = const_and (AP (name "q" i)) (box "Y") in ``` ``` let disjunct_ae i = const_and (AP (name "q" i)) (diamond "X") in ``` ``` let disjunct_ao i = const_and (AP (name "q" i)) (diamond "Y") in ``` ``` let disjuncts_ee = List.map disjunct_ee (List.filter isEven (iota n)) in ``` ``` let disjuncts_eo = List.map disjunct_eo (List.filter isOdd (iota n)) in ``` ``` let disjuncts_ae = List.map disjunct_ae (List.filter isEven (iota n)) in ``` ``` let disjuncts_ao = List.map disjunct_ao (List.filter isOdd (iota n)) in ``` ``` (MU("X",NU("Y",const_or (const_and ((AP (name "q" (n+2)))) (const_or (disjoin disjuncts_ee) (disjoin disjuncts_eo) )) ``` ``` (const_and ((AP (name "q" (n+1)))) (const_or (disjoin disjuncts_ae) (disjoin disjuncts_ao) )) ))) ``` 682787c5 Hans-Peter Deifel ```let pg_even_odd n = ``` fdfe3dcc Hans-Peter Deifel ``` const_or ``` ``` (psi_neg2 n) ``` ``` (const_or ``` ``` (pglose n) ``` ``` (egwin n)) ``` 682787c5 Hans-Peter Deifel ```let neg_pg_even_odd n = ``` fdfe3dcc Hans-Peter Deifel ``` const_and (psi2 n) ``` ``` (const_and (pgwin n) ``` ``` (eglose n)) ``` 77f7da85 Daniel Hausmann ```let dgwin n = ``` ``` let disjunct_eg i = const_and (AP (name "q" i)) (diamond "X") in ``` ``` let disjunct_el i = const_and (AP (name "q" i)) (diamond "Z") in ``` ``` let disjunct_ag i = const_and (AP (name "q" i)) (box "X") in ``` ``` let disjunct_al i = const_and (AP (name "q" i)) (box "Z") in ``` ``` let disjuncts_eg i = List.map disjunct_eg (List.filter (fun j -> j > i) (iota n)) in ``` ``` let disjuncts_el i = List.map disjunct_el (List.filter (fun j -> j < i) (iota n)) in ``` ``` let disjuncts_ag i = List.map disjunct_ag (List.filter (fun j -> j > i) (iota n)) in ``` ``` let disjuncts_al i = List.map disjunct_al (List.filter (fun j -> j < i) (iota n)) in ``` ``` let dom_game n i = (NU("X",(MU("Y",NU("Z", (const_or (const_and (AP (name "q" (n+2))) ``` ``` (const_or (const_and (AP (name "q" i)) (diamond "Y")) ``` ``` (const_or (disjoin (disjuncts_eg i)) (disjoin ``` ```(disjuncts_el i)))) ) (const_and (AP (name "q" (n+1))) (const_or (const_and (AP (name "q" i)) (box "Y")) ``` ``` (const_or (disjoin (disjuncts_ag i)) (disjoin (disjuncts_al i)) )) ))))))) in ``` ``` let conjuncts = List.map (dom_game n) (List.filter isOdd (iota n)) in ``` ``` conjoin conjuncts ``` ```let dglose n = ``` ``` let disjunct_eg i = const_and (AP (name "q" i)) (diamond "X") in ``` ``` let disjunct_el i = const_and (AP (name "q" i)) (diamond "Z") in ``` ``` let disjunct_ag i = const_and (AP (name "q" i)) (box "X") in ``` ``` let disjunct_al i = const_and (AP (name "q" i)) (box "Z") in ``` ``` let disjuncts_eg i = List.map disjunct_eg (List.filter (fun j -> j > i) (iota n)) in ``` ``` let disjuncts_el i = List.map disjunct_el (List.filter (fun j -> j < i) (iota n)) in ``` ``` let disjuncts_ag i = List.map disjunct_ag (List.filter (fun j -> j > i) (iota n)) in ``` ``` let disjuncts_al i = List.map disjunct_al (List.filter (fun j -> j < i) (iota n)) in ``` ``` let neg_dom_game n i = (MU("X",(NU("Y",MU("Z", (const_or (const_and (AP (name "q" (n+2))) ``` ``` (const_or (const_and (AP (name "q" i)) (box "Y")) ``` ``` (const_or (disjoin (disjuncts_ag i)) (disjoin ``` ```(disjuncts_al i)))) ) (const_and (AP (name "q" (n+1))) (const_or (const_and (AP (name "q" i)) (diamond "Y")) ``` ``` (const_or (disjoin (disjuncts_eg i)) (disjoin (disjuncts_el i)) )) ))))))) in ``` ``` let disjuncts = List.map (neg_dom_game n) (List.filter isOdd (iota n)) in ``` ``` disjoin disjuncts ``` ```let pg_domgame n = ``` ``` const_or ``` ``` (psi_neg2 n) ``` ``` (const_or ``` ``` (pglose n) ``` ``` (dgwin n)) ``` ```let neg_pg_domgame n = ``` ``` const_and (psi2 n) ``` ``` (const_and (pgwin n) ``` ``` (dglose n)) ``` ```let psi3 n = ``` ``` let inside i = ``` ``` let not_qis = ``` ``` List.map (fun j -> (NOT (AP (name "q" j)))) ``` ``` (List.filter (fun x -> x <> i) (iota n)) ``` ``` in ``` ``` (const_and (AP (name "q" i)) (conjoin not_qis)) ``` ``` in ``` ``` (NU("X",const_and (box "X") (disjoin (List.map inside (iota n))))) ``` ```let psi_neg3 n = ``` ``` let inside i = ``` ``` let qis = ``` ``` List.map (fun j -> (AP (name "q" j))) ``` ``` (List.filter (fun x -> x <> i) (iota n)) ``` ``` in ``` ``` disjoin (NOT (AP (name "q" i)) :: qis) ``` ``` in ``` ``` (MU("X",const_or (diamond "X") (conjoin (List.map inside (iota n))))) ``` ```let epa_acc n = ``` ``` let inside_e i = const_and (AP (name "q" i)) (diamond (name "X" i)) in ``` ``` let under_the_fixes = disjoin (List.map inside_e (iota n)) in ``` ``` let fix mu x f = if mu then MU(x, f) else NU(x, f) in ``` ``` let rec wrap fix_lit i f = ``` ``` if i > n then f ``` ``` else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f) ``` ``` in ``` ``` wrap true 1 under_the_fixes ``` ```let epa_nacc n = ``` ``` let inside_a i = const_and (AP (name "q" i)) (box (name "X" i)) in ``` ``` let under_the_fixes = disjoin (List.map inside_a (iota n)) in ``` ``` let fix mu x f = if mu then MU(x, f) else NU(x, f) in ``` ``` let rec wrap fix_lit i f = ``` ``` if i > n then f ``` ``` else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f) ``` ``` in ``` ``` wrap false 1 under_the_fixes ``` ```let enba_acc n = ``` ``` let disjunct_eg i = const_and (AP (name "q" i)) (diamond "X") in ``` ``` let disjunct_el i = const_and (AP (name "q" i)) (diamond "Z") in ``` ``` let disjuncts_eg i = List.map disjunct_eg (List.filter (fun j -> j > i) (iota n)) in ``` ``` let disjuncts_el i = List.map disjunct_el (List.filter (fun j -> j < i) (iota n)) in ``` ``` let 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 ``` ``` let disjuncts = List.map dom_aut (List.filter isEven (iota n)) in ``` ``` disjoin disjuncts ``` ```let enba_nacc n = ``` ``` let disjunct_ag i = const_and (AP (name "q" i)) (box "X") in ``` ``` let disjunct_al i = const_and (AP (name "q" i)) (box "Z") in ``` ``` let disjuncts_ag i = List.map disjunct_ag (List.filter (fun j -> j > i) (iota n)) in ``` ``` let disjuncts_al i = List.map disjunct_al (List.filter (fun j -> j < i) (iota n)) in ``` ``` 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 ``` ``` let conjuncts = List.map neg_dom_aut (List.filter isEven (iota n)) in ``` ``` conjoin conjuncts ``` ```let enpa_is_enba n = ``` ``` const_or ``` ``` (psi_neg3 n) ``` ``` (const_and ``` ``` (const_or (epa_nacc n) (enba_acc n)) ``` ``` (const_or (epa_acc n) (enba_nacc n))) ``` ```let neg_enpa_is_enba n = ``` ``` const_and (psi3 n) ``` ``` (const_or (const_and (epa_acc n) (enba_nacc n)) ``` ``` (const_and (epa_nacc n) (enba_acc n))) ``` ```let enpa_to_enba n = ``` ``` const_or ``` ``` (psi_neg3 n) ``` ``` (const_or ``` ``` (epa_nacc n) ``` ``` (enba_acc n)) ``` ```let neg_enpa_to_enba n = ``` ``` const_and (psi3 n) ``` ``` (const_and (epa_acc n) ``` ``` (enba_nacc n)) ``` ```let upa_acc n = ``` ``` let inside_a i = const_and (AP (name "q" i)) (box (name "X" i)) in ``` ``` let under_the_fixes = disjoin (List.map inside_a (iota n)) in ``` ``` let fix mu x f = if mu then MU(x, f) else NU(x, f) in ``` ``` let rec wrap fix_lit i f = ``` ``` if i > n then f ``` ``` else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f) ``` ``` in ``` ``` wrap true 1 under_the_fixes ``` ```let upa_nacc n = ``` ``` let inside_e i = const_and (AP (name "q" i)) (diamond (name "X" i)) in ``` ``` let under_the_fixes = disjoin (List.map inside_e (iota n)) in ``` ``` let fix mu x f = if mu then MU(x, f) else NU(x, f) in ``` ``` let rec wrap fix_lit i f = ``` ``` if i > n then f ``` ``` else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f) ``` ``` in ``` ``` wrap false 1 under_the_fixes ``` ```let unba_acc n = ``` ``` let disjunct_ag i = const_and (AP (name "q" i)) (box "X") in ``` ``` let disjunct_al i = const_and (AP (name "q" i)) (box "Z") in ``` ``` let disjuncts_ag i = List.map disjunct_ag (List.filter (fun j -> j > i) (iota n)) in ``` ``` let disjuncts_al i = List.map disjunct_al (List.filter (fun j -> j < i) (iota n)) in ``` ``` let dom_aut i = (MU("X",(NU("Y",MU("Z", (const_or (const_and (AP (name "q" i)) (box "Y")) ``` ``` (const_or (disjoin (disjuncts_ag i)) (disjoin (disjuncts_al i)) )) ))))) in ``` ``` let disjuncts = List.map dom_aut (List.filter isEven (iota n)) in ``` ``` disjoin disjuncts ``` ```let unba_nacc n = ``` ``` let disjunct_eg i = const_and (AP (name "q" i)) (diamond "X") in ``` ``` let disjunct_el i = const_and (AP (name "q" i)) (diamond "Z") in ``` ``` let disjuncts_eg i = List.map disjunct_eg (List.filter (fun j -> j > i) (iota n)) in ``` ``` let disjuncts_el i = List.map disjunct_el (List.filter (fun j -> j < i) (iota n)) in ``` ``` 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 ``` ``` let conjuncts = List.map neg_dom_aut (List.filter isEven (iota n)) in ``` ``` conjoin conjuncts ``` ```let unpa_is_unba n = ``` ``` const_or ``` ``` (psi_neg3 n) ``` ``` (const_and ``` ``` (const_or (upa_nacc n) (unba_acc n)) ``` ``` (const_or (upa_acc n) (unba_nacc n))) ``` ```let neg_unpa_is_unba n = ``` ``` const_and (psi3 n) ``` ``` (const_or (const_and (upa_acc n) (unba_nacc n)) ``` ``` (const_and (upa_nacc n) (unba_acc n))) ``` ```let unpa_to_unba n = ``` ``` const_or ``` ``` (psi_neg3 n) ``` ``` (const_or ``` ``` (upa_nacc n) ``` ``` (unba_acc n)) ``` ```let neg_unpa_to_unba n = ``` ``` const_and (psi3 n) ``` ``` (const_and (upa_acc n) ``` ``` (unba_nacc n)) ``` ```let unba_acc_dual n = ``` ``` let disjunct_ag i = const_and (AP (name "q" i)) (box "X") in ``` ``` let disjunct_al i = const_and (AP (name "q" i)) (box "Z") in ``` ``` let disjuncts_ag i = List.map disjunct_ag (List.filter (fun j -> j > i) (iota n)) in ``` ``` let disjuncts_al i = List.map disjunct_al (List.filter (fun j -> j < i) (iota n)) in ``` ``` let 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 ``` ``` let conjuncts = List.map dom_aut (List.filter isOdd (iota n)) in ``` ``` conjoin conjuncts ``` ```let unba_nacc_dual n = ``` ``` let disjunct_eg i = const_and (AP (name "q" i)) (diamond "X") in ``` ``` let disjunct_el i = const_and (AP (name "q" i)) (diamond "Z") in ``` ``` let disjuncts_eg i = List.map disjunct_eg (List.filter (fun j -> j > i) (iota n)) in ``` ``` let disjuncts_el i = List.map disjunct_el (List.filter (fun j -> j < i) (iota n)) in ``` ``` 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 ``` ``` let disjuncts = List.map neg_dom_aut (List.filter isOdd (iota n)) in ``` ``` disjoin disjuncts ``` ```let unpa_is_unba_dual n = ``` ``` const_or ``` ``` (psi_neg3 n) ``` ``` (const_and ``` ``` (const_or (upa_nacc n) (unba_acc_dual n)) ``` ``` (const_or (upa_acc n) (unba_nacc_dual n))) ``` ```let neg_unpa_is_unba_dual n = ``` ``` const_and (psi3 n) ``` ``` (const_or (const_and (upa_acc n) (unba_nacc_dual n)) ``` ``` (const_and (upa_nacc n) (unba_acc_dual n))) ``` db56eb9d Hans-Peter Deifel ```let ag psi = NU("X", const_and psi (box "X")) ``` ```let early_init x m = ``` ``` let conjuncts = List.map (fun i -> (NOT (AP (name x (i-1))))) (iota m) ``` ``` in ag (const_and ``` ``` (const_imp (AP ("start" ^ x)) ``` ``` (const_and (AP x) (conjoin conjuncts))) ``` ``` (const_imp (AP x) (diamond x))) ``` ```let rec early_psi n x i = match i with ``` ``` | 0 -> TRUE (* FIXME *) ``` ``` | _ -> ``` ``` conjoin ``` ``` [ const_or (NOT (AP (name x (n-i)))) (box (name x (n-i))) ``` ``` ; const_or (AP (name x (n-i))) (const_ax "" (NOT (AP (name x (n-i))))) ``` ``` ; early_psi n x (i-1) ``` ``` ] ``` ```let rec early_c_n n x i = match i with ``` ``` | 0 -> TRUE (* FIXME *) ``` ``` | _ -> ``` ``` const_or ``` ``` (conjoin [ NOT (AP (name x (n-i))) ``` ``` ; box (name x (n-i)) ``` ``` ; early_psi n x (i-1)]) ``` ``` (conjoin [ (AP (name x (n-i))) ``` ``` ; const_ax "" (NOT (AP (name x (n-i)))) ``` ``` ; early_c_n n x (i-1) ]) ``` ```let early_c x n = early_c_n n x n ``` ```let pow2 x = 1 lsl x ``` ```let bitlist j x = List.map (fun i -> x land (1 lsl (i-1)) <> 0) (iota j) ``` ```let early_bin r j i = ``` ``` conjoin ``` ``` (List.mapi ``` ``` (fun i bit -> if bit then (AP (name r i)) else (NOT (AP (name r i)))) ``` ``` (bitlist j i)) ``` ```let early_theta j = ``` ``` let n = pow2 j in ``` ``` let inside i = const_and (early_bin "r" j (i-1)) (diamond (name "X" i)) in ``` ``` let under_the_fixes = disjoin (List.map inside (iota n)) in ``` ``` let fix mu x f = if mu then MU(x, f) else NU(x, f) in ``` ``` let rec wrap fix_lit i f = ``` ``` if i > n then f ``` ``` else wrap (not fix_lit) (i+1) (fix fix_lit (name "X" i) f) ``` ``` in ``` ``` wrap false 1 under_the_fixes ``` ```(* let early_theta _ = MU ("Y", (const_or (AP "p") (diamond "Y"))) *) ``` ```let early_ac n j k = ``` ``` conjoin ``` ``` [ (AP "startp") ``` ``` ; early_init "p" n ``` ``` ; early_init "r" k ``` ``` ; ag (const_and ``` ``` (const_imp (AP "r") (early_c "r" k)) ``` ``` (const_imp (AP "p") (early_c "p" n))) ``` ``` ; ag (conjoin ``` ``` [ const_imp ``` ``` (conjoin (List.map (fun i -> AP (name "p" (i - 1))) (iota (min j n)))) ``` ``` (const_ex "" (const_and (AP "startr") (early_theta k))) ``` ``` ; NOT (const_and (AP "p") (AP "r")) ``` ``` ; const_imp (AP "r") (box "r") ``` ``` ] ``` ``` ) ``` ``` ] ``` ```let af psi = MU("Y", const_or psi (box "Y")) ``` ```let early_caching_ac n j k = ``` ``` conjoin ``` ``` [ early_ac n j k ``` ``` ; (AP "b") ``` ``` ; early_init "q" n ``` ``` ; ag (conjoin [ NOT (const_and (AP "p") (AP "q")) ``` ``` ; NOT (const_and (AP "q") (AP "r")) ``` 6c3793cb Hans-Peter Deifel ``` ; const_imp (AP "q") (early_c "q" n) ``` db56eb9d Hans-Peter Deifel ``` ]) ``` ``` ; ag (const_and (af (AP "b")) (const_imp (AP "b") ``` ``` (conjoin [ diamond "p" ``` ``` ; diamond "startq" ``` ``` ; const_ax "" (NOT (AP "b"))]) ``` ``` )) ``` ``` ] ``` 77f7da85 Daniel Hausmann 867cefeb Hans-Peter Deifel ```exception CTLException of string ``` ```(** Converts a formula into a string representation for MLSolver. ``` ``` @param f A formula. ``` ``` @return A string representing f for MLSolver. ``` ``` @raise CTLException If the name of an atomic program ``` ``` or a propositional variable in f is "tt" or "ff". ``` ``` *) ``` ```let exportMLSolver f = ``` ``` let sb = Buffer.create 3000 in ``` ``` let rec expML = function ``` ``` | TRUE -> Buffer.add_string sb "(tt)" ``` ``` | FALSE -> Buffer.add_string sb "(ff)" ``` ``` | AP s -> ``` ``` if s <> "tt" && s <> "ff" then begin ``` ``` Buffer.add_string sb s; ``` ``` end ``` ``` else raise (CTLException "Formula contains ff or tt.") ``` ``` | VAR s -> ``` ``` Buffer.add_string sb " "; ``` ``` Buffer.add_string sb s; ``` ``` Buffer.add_string sb " " ``` ``` | NOT f1 -> ``` ``` Buffer.add_string sb "(!"; ``` ``` expML f1; ``` ``` Buffer.add_string sb ")" ``` fdfe3dcc Hans-Peter Deifel ``` | EX (_, f1) -> ``` ``` Buffer.add_string sb "(<>"; ``` ``` expML f1; ``` ``` Buffer.add_string sb ")" ``` ``` | AX (_, f1) -> ``` ``` Buffer.add_string sb "([]"; ``` ``` expML f1; ``` ``` Buffer.add_string sb ")" ``` 88a1a18b Hans-Peter Deifel ``` | ID (f1) -> ``` ``` Buffer.add_string sb "(()"; ``` ``` expML f1; ``` ``` Buffer.add_string sb ")" ``` 867cefeb Hans-Peter Deifel ``` | EF f1 -> ``` ``` Buffer.add_string sb "(E F"; ``` ``` expML f1; ``` ``` Buffer.add_string sb ")" ``` ``` | AF f1 -> ``` ``` Buffer.add_string sb "(A F"; ``` ``` expML f1; ``` ``` Buffer.add_string sb ")" ``` ``` | EG f1 -> ``` ``` Buffer.add_string sb "(E G"; ``` ``` expML f1; ``` ``` Buffer.add_string sb ")" ``` ``` | AG f1 -> ``` ``` Buffer.add_string sb "(A G"; ``` ``` expML f1; ``` ``` Buffer.add_string sb ")" ``` ``` | EQU (f1, f2) -> ``` ``` Buffer.add_string sb "("; ``` ``` expML f1; ``` ``` Buffer.add_string sb " <==> "; ``` ``` expML f2; ``` ``` Buffer.add_string sb ")" ``` ``` | IMP (f1, f2) -> ``` ``` Buffer.add_string sb "("; ``` ``` expML f1; ``` ``` Buffer.add_string sb " ==> "; ``` ``` expML f2; ``` ``` Buffer.add_string sb ")" ``` ``` | OR (f1, f2) -> ``` ``` Buffer.add_string sb "("; ``` ``` expML f1; ``` ``` Buffer.add_string sb " | "; ``` ``` expML f2; ``` ``` Buffer.add_string sb ")" ``` ``` | AND (f1, f2) -> ``` ``` Buffer.add_string sb "("; ``` ``` expML f1; ``` ``` Buffer.add_string sb " & "; ``` ``` expML f2; ``` ``` Buffer.add_string sb ")" ``` ``` | EU (f1, f2) -> ``` ``` Buffer.add_string sb "(E ("; ``` ``` expML f1; ``` ``` Buffer.add_string sb " U "; ``` ``` expML f2; ``` ``` Buffer.add_string sb "))" ``` ``` | AU (f1, f2) -> ``` ``` Buffer.add_string sb "(A ("; ``` ``` expML f1; ``` ``` Buffer.add_string sb " U "; ``` ``` expML f2; ``` ``` Buffer.add_string sb "))" ``` ``` | EB (f1, f2) -> ``` ``` Buffer.add_string sb "(E ("; ``` ``` expML f1; ``` ``` Buffer.add_string sb " R "; ``` ``` expML (NOT f2); ``` ``` Buffer.add_string sb "))" ``` ``` | AB (f1, f2) -> ``` ``` Buffer.add_string sb "(A ("; ``` ``` expML f1; ``` ``` Buffer.add_string sb " R "; ``` ``` expML (NOT f2); ``` ``` Buffer.add_string sb "))" ``` ``` | NU (var, f1) -> ``` ``` Buffer.add_string sb ("(nu " ^ var ^ ". "); ``` ``` expML f1; ``` ``` Buffer.add_string sb ")" ``` ``` | MU (var, f1) -> ``` ``` Buffer.add_string sb ("(mu " ^ var ^ ". "); ``` ``` expML f1; ``` ``` Buffer.add_string sb ")" ``` db56eb9d Hans-Peter Deifel ``` | _ -> raise (CTLException "exportMLSolver: Unsupported formula"); ``` 867cefeb Hans-Peter Deifel ``` in ``` ``` expML f; ``` ``` Buffer.contents sb ``` c9dbb509 Hans-Peter Deifel ```let print_usage () = ``` 467e8bbc Hans-Peter Deifel ``` print_endline ("Usage: " ^ Sys.argv.(0) ^ " SYNTAX FORMULA_FAMILY n"); ``` ``` print_endline ""; ``` ``` print_endline "SYNTAX: Either 'cool' or 'mlsolver'"; ``` ``` print_endline ""; ``` ``` print_endline "FORMULA_FAMILY:"; ``` 77f7da85 Daniel Hausmann ``` print_endline " - linear_dpa_is_nba: linear parity condition is ``` ``` nondet. büchi condition [1]; valid"; ``` ``` print_endline " - linear_dpa_is_nba_neg: same, but negated; unsatisfiable"; ``` ``` print_endline " - pg_even_odd: parity games are more expressive than even-odd games; valid"; ``` 45386aae Hans-Peter Deifel ``` print_endline " - pg_even_odd_neg: same, but negated; unsatisfiable"; ``` 77f7da85 Daniel Hausmann ``` print_endline " - pg_domgame: parity games are more expressive than dominator games; valid"; ``` 45386aae Hans-Peter Deifel ``` print_endline " - pg_domgame_neg: same, but negated; unsatisfiable"; ``` 77f7da85 Daniel Hausmann ``` print_endline " - enpa_is_enba: transform ex. npa to equivalent ex. nba; valid"; ``` 45386aae Hans-Peter Deifel ``` print_endline " - enpa_is_enba_neg: same, but negated; unsatisfiable"; ``` 77f7da85 Daniel Hausmann ``` print_endline " - enpa_to_enba: ex. npa implies ex. nba ``` ``` (left-to-right direction of enpa_is_enba); valid"; ``` 45386aae Hans-Peter Deifel ``` print_endline " - enpa_to_enba_neg: same, but negated; unsatisfiable"; ``` 77f7da85 Daniel Hausmann ``` print_endline " - unpa_is_unba: transform univ. npa to equivalent univ. nba; valid"; ``` 45386aae Hans-Peter Deifel ``` print_endline " - unpa_is_unba_neg: same, but negated; satisfiable"; ``` 77f7da85 Daniel Hausmann ``` print_endline " - unpa_to_unba: univ. npa implies univ. nba ``` ``` (left-to-right direction of unpa_is_unba); valid"; ``` 45386aae Hans-Peter Deifel ``` print_endline " - unpa_to_unba_neg: same, but negated; satisfiable"; ``` 77f7da85 Daniel Hausmann ``` print_endline " - unpa_is_unba_dual: dual formulation of unpa_is_unba, with ``` ``` odd dominators; valid"; ``` 45386aae Hans-Peter Deifel ``` print_endline " - unpa_is_unba_dual_neg: same, but negated; unsatisfiable"; ``` 467e8bbc Hans-Peter Deifel ``` print_endline ""; ``` ``` print_endline "n: Index of the formula in the family"; ``` ``` print_endline ""; ``` ``` print_endline "[1]: http://files.oliverfriedmann.de/papers/a_solver_for_modal_fixpoint_logics.pdf, page 7" ``` c9dbb509 Hans-Peter Deifel 867cefeb Hans-Peter Deifel ```let () = ``` c9dbb509 Hans-Peter Deifel ``` if Array.length Sys.argv <> 4 then ``` ``` print_usage () ``` ``` else ``` 467e8bbc Hans-Peter Deifel ``` let syntax = match Sys.argv.(1) with ``` ``` | "cool" -> exportFormula ``` ``` | "mlsolver" -> exportMLSolver ``` fdfe3dcc Hans-Peter Deifel ``` | _ -> print_usage (); exit 1 ``` 467e8bbc Hans-Peter Deifel ``` in ``` ``` let family = match Sys.argv.(2) with ``` 682787c5 Hans-Peter Deifel ``` | "linear_dpa_is_nba" -> linear_dpa_is_nba ``` ``` | "linear_dpa_is_nba_neg" -> neg_linear_dpa_is_nba ``` 77f7da85 Daniel Hausmann ``` | "enpa_is_enba" -> enpa_is_enba ``` ``` | "enpa_is_enba_neg" -> neg_enpa_is_enba ``` ``` | "enpa_to_enba" -> enpa_to_enba ``` ``` | "enpa_to_enba_neg" -> neg_enpa_to_enba ``` ``` | "unpa_is_unba" -> unpa_is_unba ``` ``` | "unpa_is_unba_neg" -> neg_unpa_is_unba ``` ``` | "unpa_to_unba" -> unpa_to_unba ``` ``` | "unpa_to_unba_neg" -> neg_unpa_to_unba ``` ``` | "unpa_is_unba_dual" -> unpa_is_unba_dual ``` ``` | "unpa_is_unba_dual_neg" -> neg_unpa_is_unba_dual ``` 682787c5 Hans-Peter Deifel ``` | "pg_even_odd" -> pg_even_odd ``` ``` | "pg_even_odd_neg" -> neg_pg_even_odd ``` 77f7da85 Daniel Hausmann ``` | "pg_domgame" -> pg_domgame ``` ``` | "pg_domgame_neg" -> neg_pg_domgame ``` db56eb9d Hans-Peter Deifel ``` | "early_ac" -> fun i -> early_ac i 4 2 ``` ``` | "early_caching_ac" -> fun i -> early_caching_ac i 4 2 ``` c9dbb509 Hans-Peter Deifel ``` | _ -> print_usage (); exit 1 ``` ``` in ``` 467e8bbc Hans-Peter Deifel ``` let n = int_of_string Sys.argv.(3) in ``` ` print_endline (syntax (family n));`