diff --git a/CoAlgFormula.ml b/CoAlgFormula.ml
index 4097ef91917eb8e29a125dd1719028d6778d5f7e..22da4d0550ae61a8e0cb012b4fc117b36c0717ad 100644
--- a/CoAlgFormula.ml
+++ b/CoAlgFormula.ml
@@ -1161,6 +1161,12 @@ let const_max n s f =
   if n < 0 then raise (CoAlgException "Negative cardinality constraint.")
   else MAX (n, s, f)
 
+let const_enforces p f =
+    ENFORCES (p,f)
+
+let const_allows p f =
+    ALLOWS (p,f)
+
 (** Constructs a choice formula from two formulae.
     @param f1 The first formula (LHS).
     @param f2 The second formula (LHS).
diff --git a/CoAlgFormula.mli b/CoAlgFormula.mli
index 69a7ecffa2f89f92c88f1b47f6337f036f0dfb27..8d99da64016de628139e8d425295a07584c7efde 100644
--- a/CoAlgFormula.mli
+++ b/CoAlgFormula.mli
@@ -95,6 +95,8 @@ val const_ex : string -> formula -> formula
 val const_ax : string -> formula -> formula
 val const_min : int -> string -> formula -> formula
 val const_max : int -> string -> formula -> formula
+val const_enforces : int list -> formula -> formula
+val const_allows : int list -> formula -> formula
 val const_choice : formula -> formula -> formula
 val const_fusion : bool -> formula -> formula
 
diff --git a/CoolUtils.ml b/CoolUtils.ml
index ffb4bfbc9c2bb7ead1680fc05ddf1d739d6aec2c..bf60d093209ad929114761b1911e999a92b13d3b 100644
--- a/CoolUtils.ml
+++ b/CoolUtils.ml
@@ -26,6 +26,11 @@ module TList = struct
                                      | h2::t2 -> (h1,h2)::(zip t1 t2)
                                      | [] -> [])
                         | [] -> []
+    let rec powerset l = match l with
+        | [] -> [[]]
+        | h::t -> let pt = powerset t in
+                  let oth = List.map (fun x -> h::x) pt in
+                  List.append pt oth
 end
 
 let agents = ref ([|1;2;3;4;5;6;7;8;9;10|])
diff --git a/CoolUtils.mli b/CoolUtils.mli
index daa96bbe6dbab8dde3ee1940c4a054ad2023377a..73e7e53eacd0eecd30988334368851013011b1e0 100644
--- a/CoolUtils.mli
+++ b/CoolUtils.mli
@@ -12,6 +12,7 @@ end
 
 module TList : sig
     val zip : ('a list) -> ('b list) -> ('a * 'b) list
+    val powerset : ('a list) -> ('a list list)
 end
 
 val cl_get_agents : unit -> int array
diff --git a/coalgcompare.ml b/coalgcompare.ml
index 0f73a30726075efc6ca8ee3354cbcf8de5f84dbd..81a9edb0a07c6f3a8e4d3b3fc696aada392fa809 100644
--- a/coalgcompare.ml
+++ b/coalgcompare.ml
@@ -129,7 +129,7 @@ let solvALC (tbox, sf) =
 let solvFact (tbox, sf) timeout =
   let (fl, tboxND, tboxD) = exportALCQuery tbox sf in
   A.createFactTBox "fact.tbox" fl tboxND tboxD;
-  let fact = "/usr/bin/FaCT++" in
+  let fact = "./FaCT++" in
   let reg = "is satisfiable" in
   let call () = G.callExt None fact ["fact.conf"] (Str.regexp_string reg) timeout in
   let ignore_exception = false in
@@ -200,6 +200,35 @@ let printRawData ((rn,results):testresults) : unit =
     let lines = List.map format_line results in
     print_endline (String.concat "\n" lines)
 
+let doGenCL aglist sizelist : unit =
+  let solvs = [(solvFact, "fact"); (solvCoalg sortK, "cool")] in
+  (*
+    lF A list of pairs (f, n), e.g. (p, 1).
+    The list must not be empty.
+    lFF A list of pairs (f->f, n), e.g. (~., 1).
+    The list must not be empty.
+    lFFF A list of pairs (f->f->f, n), e.g. (.&., 1).
+    lPFF A list of pairs (p->f->f, n), e.g. (<.>., 1).
+    lP A list of pairs (p, n), e.g. (a, 1).
+    The list must not be empty unless lPFF is also empty.
+    lPP A list of pairs (p->p, n), e.g. ( *., 1).
+    lFP A list of pairs (f->p, n), e.g. (?., 1).
+    lPPP A list of pairs (p->p->p, n), e.g. (.+., 1).
+  *)
+  let lF = List.map (fun p -> (C.AP (string_of_int p), 1)) (0--10) in
+  let lFF = [(C.const_not,1)] in
+  let lFFF = [(C.const_and,1); (C.const_or, 1)] in
+  let lPFF = [(C.const_enforces,1); (C.const_allows, 1)] in
+  (* role names *)
+  let lP = List.map (fun p -> (p, 1)) (TList.powerset aglist) in
+  let lPP : ((int list -> int list) * int) list= [] in
+  let lFP = [] in
+  let lPPP = [] in
+  let (genF,_) = G.mk_generator lF lFF lFFF lPFF lP lPP lFP lPPP in
+  let printformula f =
+    print_endline (CoAlgFormula.exportFormula f)
+  in
+  List.iter (fun sz -> printformula (genF sz)) sizelist
 
 let _ =
     if Array.length Sys.argv < 2 then printUsage ()