diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index f72e7f67534930f6c562728b068268f5ff52397d..1af782123b1bec761bc1a634704e4ecd31611e53 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -2390,6 +2390,42 @@ let rec hc_freeIn variable (f: hcFormula) =
(* Do we need to exclude bound variables here? *)
hc_freeIn variable f1
+let rec hc_freeIn2 variable (f: hcFormula) =
+ match f.HC.node with
+ | HCTRUE
+ | HCFALSE
+ | HCAP _
+ | HCNOT _
+ | HCCONST _
+ | HCCONSTN _ -> false
+ | HCVAR s ->
+ if compare variable s == 0
+ then true
+ else false
+ | HCAT (s, f1) ->
+ hc_freeIn variable f1
+ | HCOR (f1, f2)
+ | HCAND (f1, f2) ->
+ hc_freeIn variable f1 || hc_freeIn variable f2
+ | HCEX (_, f1)
+ | HCAX (_, f1)
+ | HCENFORCES (_, f1)
+ | HCALLOWS (_, f1)
+ | HCMORETHAN (_, _, f1)
+ | HCMAXEXCEPT (_, _, f1)
+ | HCATLEASTPROB (_, f1)
+ | HCLESSPROBFAIL (_, f1)
+ | HCID f1 ->
+ hc_freeIn variable f1
+ | HCNORM (f1, f2)
+ | HCNORMN (f1, f2)
+ | HCCHC (f1, f2) ->
+ hc_freeIn variable f1 || hc_freeIn variable f2
+ | HCFUS (first, f1) ->
+ hc_freeIn variable f1
+ | HCMU (var, f1)
+ | HCNU (var, f1) ->
+ if variable = var then false else hc_freeIn variable f1
(** An instantiation of a hash table (of the standard library)
for hash-consed formulae. The test for equality
diff --git a/src/lib/CoAlgFormula.mli b/src/lib/CoAlgFormula.mli
index cee483d6e346dc2286d16be9d6a87ab75afd4d8a..6231f7d77c6e7aff802d20c8a985fa10f1379cd9 100644
--- a/src/lib/CoAlgFormula.mli
+++ b/src/lib/CoAlgFormula.mli
@@ -177,6 +177,11 @@ val hc_formula : HcFormula.t -> formula -> hcFormula
val hc_replace : HcFormula.t -> string -> hcFormula -> hcFormula -> hcFormula
val hc_freeIn : string -> hcFormula -> bool
+(* Variant of freeIn that respects bound variables
+ FIXME: Merge into regular freeIn
+ *)
+val hc_freeIn2 : string -> hcFormula -> bool
+
module HcFHt : (Hashtbl.S with type key = hcFormula)
(* vim: set et sw=2 sts=2 ts=8 : *)
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 8daf890dd49e3f9b498beab59c8b413198fdc48a..3916a80d3b766a9a6d0bcb46990d9072b1294eb8 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -940,13 +940,95 @@ let fragment = ref AlternationFree
let getFragment () = !fragment
+type fixpoint_type = MU | NU
+type bound_vars = (fixpoint_type * string) list
+
+let alternationLevel bound_vars =
+ let rec intern current count = function
+ | [] -> count
+ | (MU, _) :: xs ->
+ let count = if current = MU then count else count + 1 in
+ intern MU count xs
+ | (NU, _) :: xs ->
+ let count = if current = NU then count else count + 1 in
+ intern NU count xs
+ in
+ intern NU 0 bound_vars
+
+let rec outerMU bound_vars = match bound_vars with
+ | [] -> None
+ | (MU, x) :: xs -> Some x
+ | _ :: xs -> outerMU xs
+
+let formulaAlternationLevel nomTbl hcF altLevel s f =
+ let seen = Array.init (Array.length !sortTable) (fun _ -> C.HcFHt.create 128) in
+ let rec intern fixpoints s f =
+ if C.HcFHt.mem seen.(s) f then ()
+ else begin
+ let free_vars = List.filter (fun (_,x) -> C.hc_freeIn2 x f) fixpoints in
+ C.HcFHt.replace altLevel.(s) f (alternationLevel free_vars);
+ C.HcFHt.replace seen.(s) f ();
+ let (func, sortlst) = !sortTable.(s) in
+ match f.HC.node with
+ | C.HCVAR _
+ | C.HCTRUE
+ | C.HCFALSE
+ | C.HCAP _
+ | C.HCNOT _
+ | C.HCCONST _
+ | C.HCCONSTN _ -> ()
+ | C.HCAT (name, f1) ->
+ let s1 =
+ match nomTbl name with
+ | None -> raise (C.CoAlgException ("Unknown nominal: " ^ name))
+ | Some sort -> sort
+ in
+ let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in
+ intern fixpoints s1 hcnom;
+ intern fixpoints s1 f1
+ | C.HCOR (f1, f2)
+ | C.HCAND (f1, f2) ->
+ intern fixpoints s f1;
+ intern fixpoints s f2
+ | C.HCEX (_, f1)
+ | C.HCAX (_, f1)
+ | C.HCENFORCES (_, f1)
+ | C.HCALLOWS (_, f1)
+ | C.HCMORETHAN (_,_,f1)
+ | C.HCMAXEXCEPT (_,_,f1)
+ | C.HCATLEASTPROB (_,f1)
+ | C.HCLESSPROBFAIL (_,f1)
+ | C.HCID f1 ->
+ intern fixpoints (List.hd sortlst) f1;
+ | C.HCNORM (f1, f2)
+ | C.HCNORMN(f1, f2)
+ | C.HCCHC (f1, f2) ->
+ intern fixpoints (List.nth sortlst 0) f1;
+ intern fixpoints (List.nth sortlst 1) f2
+ | C.HCFUS (first, f1) ->
+ let s1 = List.nth sortlst (if first then 0 else 1) in
+ intern fixpoints s1 f1
+ | C.HCMU (name, f1) ->
+ let unfold = C.hc_replace hcF name f f1 in
+ let appendvars = List.append free_vars [(MU,name)] in
+ C.HcFHt.replace altLevel.(s) f (alternationLevel appendvars);
+ intern appendvars s unfold
+ | C.HCNU (name, f1) ->
+ let unfold = C.hc_replace hcF name f f1 in
+ let appendvars = List.append free_vars [(NU, name)] in
+ C.HcFHt.replace altLevel.(s) f (alternationLevel appendvars);
+ intern appendvars s unfold
+ end
+ in
+ intern [] s f
+
(* Calculate all possible formulae. This includes all subformulae and
in the case of μ-Calculus the Fischer-Ladner closure.
TODO: variable sort needs to match epected sort
*)
let rec detClosure vars nomTbl hcF fset vset atset nomset s f =
- let newvars = List.filter (fun (x) -> C.hc_freeIn x f) vars in
+ let newvars = List.filter (fun x -> C.hc_freeIn x f) vars in
let detClosure_ = detClosure newvars in
let deferral = if List.length newvars > 0
then (List.hd newvars)
@@ -1080,7 +1162,6 @@ let rec detClosure vars nomTbl hcF fset vset atset nomset s f =
let unfold = C.hc_replace hcF name f f1 in
detClosure_ nomTbl hcF fset vset atset nomset s unfold
-
let detClosureAt hcF atset name f () =
match f.HC.node with
| C.HCTRUE
@@ -1279,17 +1360,26 @@ let ppFormulae fragSpec nomTbl tbox (s, f) =
let fset = Array.init card (fun _ -> C.HcFHt.create 128) in
let vset = Array.init card (fun _ -> C.HcFHt.create 128) in
+ let altLevel = Array.init card (fun _ -> C.HcFHt.create 128) in
let atset = C.HcFHt.create 64 in
let nomset = Hashtbl.create 16 in
for i = 0 to card-1 do
detClosure [] nomTbl hcF fset vset atset nomset i hcfalse;
+ formulaAlternationLevel nomTbl hcF altLevel i hcfalse;
detClosure [] nomTbl hcF fset vset atset nomset i hctrue;
+ formulaAlternationLevel nomTbl hcF altLevel i hctrue;
done;
detClosure [] nomTbl hcF fset vset atset nomset s hcf;
+ formulaAlternationLevel nomTbl hcF altLevel s hcf;
detClosure [] nomTbl hcF fset vset atset nomset s nhcf;
- List.iter (fun (s, f) -> detClosure [] nomTbl hcF fset vset atset nomset s f)
+ formulaAlternationLevel nomTbl hcF altLevel s nhcf;
+ List.iter (fun (s, f) ->
+ detClosure [] nomTbl hcF fset vset atset nomset s f;
+ formulaAlternationLevel nomTbl hcF altLevel s f)
hctbox;
- List.iter (fun (s, f) -> detClosure [] nomTbl hcF fset vset atset nomset s f)
+ List.iter (fun (s, f) ->
+ detClosure [] nomTbl hcF fset vset atset nomset s f;
+ formulaAlternationLevel nomTbl hcF altLevel s f)
nhctbox;
Hashtbl.iter (fun n s -> C.HcFHt.iter (detClosureAt hcF atset n) fset.(s)) nomset;
diff --git a/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli
index 7815d8df5d25c5c6472608e1bdc5f1c1dd8cd30f..40eed0b240c4aa00d841746ecc68a6585e0a7c33 100644
--- a/src/lib/CoAlgMisc.mli
+++ b/src/lib/CoAlgMisc.mli
@@ -399,6 +399,21 @@ type fragment_spec = Auto | Fragment of fragment
(** Return the fragment of the mu-calculus that the original formula uses *)
val getFragment : unit -> fragment
+
+type fixpoint_type = MU | NU
+type bound_vars = (fixpoint_type * string) list
+
+(** Calculate the level of alternation between fixpoint types.
+
+ Bound vars must be ordered outer-first. *)
+val alternationLevel : bound_vars -> int
+
+val formulaAlternationLevel : (string -> int option) -> CoAlgFormula.HcFormula.t
+ -> int CoAlgFormula.HcFHt.t array (* table for alternation levels *)
+ -> sort
+ -> (CoAlgFormula.hcFormula_node, CoAlgFormula.formula) HashConsing.hash_consed
+ -> unit
+
(** [ppFormulae fragment nomTbl tbox sf] initializes the array representation and various
tables for the formula.
diff --git a/src/unit-tests/CoAlgMisc_tests.ml b/src/unit-tests/CoAlgMisc_tests.ml
new file mode 100644
index 0000000000000000000000000000000000000000..4606c92535b9bbffab4ebf9c6c83825e44eecdd2
--- /dev/null
+++ b/src/unit-tests/CoAlgMisc_tests.ml
@@ -0,0 +1,43 @@
+open OUnit2
+open CoAlgMisc
+
+module C = CoAlgFormula
+
+let alternationLevel_test _ =
+ assert_equal (alternationLevel []) 0;
+ assert_equal (alternationLevel [(MU,"x")]) 1;
+ assert_equal (alternationLevel [(NU,"x")]) 0;
+ assert_equal (alternationLevel [(NU,"x"); (MU,"y")]) 1;
+ assert_equal (alternationLevel [(NU,"x"); (NU, "y")]) 0;
+ assert_equal (alternationLevel [(NU,"x"); (MU, "y"); (NU, "z")]) 2;
+ assert_equal (alternationLevel [(NU,"x"); (MU, "a"); (MU, "y"); (NU, "z")]) 2
+
+let formulaAlternationLevel_test _ =
+ let wrapper formula subformula =
+ sortTable := FunctorParsing.sortTableFromString "K";
+ let hcF = C.HcFormula.create true in
+ let hcf = C.hc_formula hcF formula in
+ let nomTbl _ = Some 0 in
+ let altLevel = Array.init (Array.length !sortTable) (fun _ -> C.HcFHt.create 128) in
+ formulaAlternationLevel nomTbl hcF altLevel 0 hcf;
+ let hcSubF = C.hc_formula hcF subformula in
+ C.HcFHt.find altLevel.(0) hcSubF
+ in
+ let equal msg = assert_equal ~printer:string_of_int ~msg:msg in
+ equal "p & q" 0 (wrapper (C.AND(C.AP "p", C.AP "q")) (C.AP "q"));
+ equal "νX.[]X" 0 (wrapper (C.NU("X",(C.AX("", C.VAR "X")))) (C.NU("X",(C.AX("", C.VAR "X")))));
+ equal "µX.[]X" 1 (wrapper (C.MU("X",(C.AX("", C.VAR "X")))) (C.MU("X",(C.AX("", C.VAR "X")))));
+ (* ɸ = µX.p & νY.(<>(Y & p) | <>X) *)
+ let psi = C.NU("Y",C.OR(C.EX("",(C.AND(C.VAR "Y", C.AP "p"))) ,C.EX("",(C.VAR "X")))) in
+ let phi = (C.MU("X",(C.AND(C.AP "p", psi)))) in
+ equal "ɸ in ɸ" 1 (wrapper phi phi);
+ equal "p in ɸ" 0 (wrapper phi (C.AP "p"));
+ let psi1 = C.NU("Y",C.OR(C.EX("",(C.AND(C.VAR "Y", C.AP "p"))) ,C.EX("",phi))) in
+ equal "ψ in ɸ" 2 (wrapper phi psi1)
+
+let tests = "CoAlgMisc" >:::
+ [ ("alternationLevel" >:: alternationLevel_test)
+ ; ("formulaAlternationLevel" >:: formulaAlternationLevel_test)
+ ]
+
+(* vim: set et sw=2 sts=2 ts=8 : *)
diff --git a/src/unit-tests/CoAlgMisc_tests.mli b/src/unit-tests/CoAlgMisc_tests.mli
new file mode 100644
index 0000000000000000000000000000000000000000..ac3e6e6da69f9f977785c220e30ef4bf3a11e645
--- /dev/null
+++ b/src/unit-tests/CoAlgMisc_tests.mli
@@ -0,0 +1,3 @@
+val tests : OUnit2.test
+
+(* vim: set et sw=2 sts=2 ts=8 : *)
diff --git a/src/unit-tests/cool_unit_tests.ml b/src/unit-tests/cool_unit_tests.ml
index 65954fb02793073bee8fd49dda3dfa3b725462c8..291ddd78ccce6f5d96b943b6400b223ce17c2165 100644
--- a/src/unit-tests/cool_unit_tests.ml
+++ b/src/unit-tests/cool_unit_tests.ml
@@ -3,6 +3,7 @@ open OUnit2
let tests =
[ CoolUtils_tests.tests
; CoAlgFormula_tests.tests
+ ; CoAlgMisc_tests.tests
]
let () = run_test_tt_main (test_list tests)