### Profile

Statistics
| Branch: | Revision:

## cool / gen.ml @ 77f7da85

 1 ```open CoAlgFormula ``` ```(* Generates hard aconjunctive mu-calculus formulas with deep ``` ```nesting of fixpoints *) ``` ```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 ``` ```(* 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) ``` ```let diamond name = const_ex "" (VAR name) ``` ```let circle name = (ID (VAR name)) ``` ```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 ``` ``` (NU("X",const_and (circle "X") (disjoin (List.map inside (iota n))))) ``` ```let psi_neg 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 (circle "X") (conjoin (List.map inside (iota n))))) ``` ```let before_biimpl_neg n = ``` ``` let inside i = const_and (AP (name "q" i)) (circle (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 before_biimpl n = ``` ``` let inside i = const_and (AP (name "q" i)) (circle (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 true 1 under_the_fixes ``` ```let isEven i = i mod 2 = 0 ``` ```let isOdd i = i mod 2 = 1 ``` ```let after_biimpl n = ``` ``` let conjunct j = ``` ``` (MU("X", const_or (NU("Y", const_and (NOT (AP (name "q" j))) (circle "Y"))) ``` ``` (circle "X"))) ``` ``` in ``` ``` let disjunct i = ``` ``` let conjuncts = ``` ``` List.map conjunct (List.filter (fun j -> j > i && isOdd j) (iota n)) ``` ``` in ``` ``` let inside = ``` ``` (NU("X", const_and (MU("Y", const_or (AP (name "q" i)) (circle "Y"))) ``` ``` (circle "X"))) ``` ``` in ``` ``` (const_and inside (conjoin conjuncts)) ``` ``` in ``` ``` let disjuncts = List.map disjunct (List.filter isEven (iota n)) in ``` ``` disjoin disjuncts ``` ```let after_biimpl_neg n = ``` ``` let disjunct j = ``` ``` (NU("X", ``` ``` const_and ``` ``` (MU("Y", const_or (AP (name "q" j)) (circle "Y"))) ``` ``` (circle "X"))) ``` ``` 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 ``` ``` (NU("Y", const_and (NOT (AP (name "q" i))) (circle "Y"))) ``` ``` (circle "X"))) ``` ``` in ``` ``` (const_or inside (disjoin disjuncts)) ``` ``` in ``` ``` let conjuncts = List.map conjunct (List.filter isEven (iota n)) in ``` ``` conjoin conjuncts ``` ```let linear_dpa_is_nba n = ``` ``` 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))) ``` ```let neg_linear_dpa_is_nba n = ``` ``` const_and (psi n) ``` ``` (const_or (const_and (before_biimpl n) (after_biimpl_neg n)) ``` ``` (const_and (before_biimpl_neg n) (after_biimpl n))) ``` ```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) )) ))) ``` ```let pg_even_odd n = ``` ``` const_or ``` ``` (psi_neg2 n) ``` ``` (const_or ``` ``` (pglose n) ``` ``` (egwin n)) ``` ```let neg_pg_even_odd n = ``` ``` const_and (psi2 n) ``` ``` (const_and (pgwin n) ``` ``` (eglose n)) ``` ```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))) ``` ```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 ")" ``` ``` | EX (_, f1) -> ``` ``` Buffer.add_string sb "(<>"; ``` ``` expML f1; ``` ``` Buffer.add_string sb ")" ``` ``` | AX (_, f1) -> ``` ``` Buffer.add_string sb "([]"; ``` ``` expML f1; ``` ``` Buffer.add_string sb ")" ``` ``` | ID (f1) -> ``` ``` Buffer.add_string sb "(()"; ``` ``` expML f1; ``` ``` Buffer.add_string sb ")" ``` ``` | 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 ")" ``` ``` in ``` ``` expML f; ``` ``` Buffer.contents sb ``` ```let print_usage () = ``` ``` 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:"; ``` ``` 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"; ``` ``` print_endline " - pg_even_odd_neg: same, bug negated; unsatisfiable"; ``` ``` print_endline " - pg_domgame: parity games are more expressive than dominator games; valid"; ``` ``` print_endline " - pg_domgame_neg: same, bug negated; unsatisfiable"; ``` ``` print_endline " - enpa_is_enba: transform ex. npa to equivalent ex. nba; valid"; ``` ``` print_endline " - enpa_is_enba_neg: same, bug negated; unsatisfiable"; ``` ``` print_endline " - enpa_to_enba: ex. npa implies ex. nba ``` ``` (left-to-right direction of enpa_is_enba); valid"; ``` ``` print_endline " - enpa_to_enba_neg: same, bug negated; unsatisfiable"; ``` ``` print_endline " - unpa_is_unba: transform univ. npa to equivalent univ. nba; valid"; ``` ``` print_endline " - unpa_is_unba_neg: same, bug negated; satisfiable"; ``` ``` print_endline " - unpa_to_unba: univ. npa implies univ. nba ``` ``` (left-to-right direction of unpa_is_unba); valid"; ``` ``` print_endline " - unpa_to_unba_neg: same, bug negated; satisfiable"; ``` ``` print_endline " - unpa_is_unba_dual: dual formulation of unpa_is_unba, with ``` ``` odd dominators; valid"; ``` ``` print_endline " - unpa_is_unba_dual_neg: same, bug negated; unsatisfiable"; ``` ``` 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" ``` ```let () = ``` ``` if Array.length Sys.argv <> 4 then ``` ``` print_usage () ``` ``` else ``` ``` let syntax = match Sys.argv.(1) with ``` ``` | "cool" -> exportFormula ``` ``` | "mlsolver" -> exportMLSolver ``` ``` | _ -> print_usage (); exit 1 ``` ``` in ``` ``` let family = match Sys.argv.(2) with ``` ``` | "linear_dpa_is_nba" -> linear_dpa_is_nba ``` ``` | "linear_dpa_is_nba_neg" -> neg_linear_dpa_is_nba ``` ``` | "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 ``` ``` | "pg_even_odd" -> pg_even_odd ``` ``` | "pg_even_odd_neg" -> neg_pg_even_odd ``` ``` | "pg_domgame" -> pg_domgame ``` ``` | "pg_domgame_neg" -> neg_pg_domgame ``` ``` | _ -> print_usage (); exit 1 ``` ``` in ``` ``` let n = int_of_string Sys.argv.(3) in ``` ``` print_endline (syntax (family n)); ```