diff --git a/CoAlgFormula.ml b/CoAlgFormula.ml
index 0a4c2ad4ad75b6a36f38f404b8f67ed244bd5b91..cecfb1fe5c19444465ea5d023757f2af0fe03b3c 100644
--- a/CoAlgFormula.ml
+++ b/CoAlgFormula.ml
@@ -371,6 +371,14 @@ and parse_rest ts =
       let (_, s) = boxinternals true "]" in
       let f1 = parse_rest ts in
       AX (s, f1)
+  | A.Kwd "[{" -> 
+      let ls = agentlist "}]" in
+      let f1 = parse_rest ts in
+      ENFORCES (ls, f1)
+  | A.Kwd "<{" -> 
+      let ls = agentlist "}>" in
+      let f1 = parse_rest ts in
+      ALLOWS (ls, f1)
   | A.Kwd "{>=" -> 
       let (n, s) = boxinternals false "}" in
       let f1 = parse_rest ts in
diff --git a/coalg.ml b/coalg.ml
index ee1ca1942e3277b17468f8ee7d2c66e910667231..5bad759b1986a5ea0d53e3007ff5a7cc81b408a2 100644
--- a/coalg.ml
+++ b/coalg.ml
@@ -19,7 +19,7 @@ let sorts = [| (CoAlgMisc.MultiModalKD, [0])
             ;  (CoAlgMisc.Fusion, [1; 1]) *)
             |]
 *)
-let sorts = [| (CoAlgMisc.CoalitionLogic, [0])
+let sorts = [| (CoAlgMisc.MultiModalK, [0])
             (*;  (CoAlgMisc.MultiModalKD, [1])
             ;  (CoAlgMisc.Fusion, [1; 1]) *)
             |]
@@ -34,22 +34,15 @@ let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increm
 
 
 let printUsage () =
-  print_endline "Usage: \"alc <solver> [<verbose>]\" where";
-  print_endline "       <solver> in { sat }";
+  print_endline "Usage: \"alc <task> <functor> [<verbose>]\" where";
+  print_endline "       <task> in { sat print }";
+  print_endline "       <functor> in { MultiModalK MultiModalKD CoalitionLogic }";
   print_endline "       <verbose> = any (second) argument";
   exit 1
 
 let counter = ref 0
 
-let _ = 
-  if Array.length Sys.argv < 2 then printUsage()
-  else
-    let choice = Sys.argv.(1) in
-    let _ =
-      match choice with
-      | "sat" -> ()
-      | _ -> printUsage ()
-    in
+let choiceSat () =
     let verb = Array.length Sys.argv > 2 in
     let printRes sat =
       if not verb then
@@ -64,9 +57,34 @@ let _ =
           incr counter;
           print_string ("\nFormula " ^ (string_of_int !counter) ^ ": ");
           flush stdout;
-          match choice with
-          | "sat" -> printRes (CoAlgReasoner.isSat ~verbose:verb sorts nomTable f tbox)
-          | _ -> printUsage ()
+          printRes (CoAlgReasoner.isSat ~verbose:verb sorts nomTable f tbox)
+        else ()
+      done
+    with End_of_file -> ()
+
+
+let choicePrint () =
+    try
+      while true do
+        let input = read_line () in
+        if not (GenAndComp.isEmptyString input) then
+          let f = CoAlgFormula.importFormula input in
+          let str = CoAlgFormula.exportFormula f in
+          incr counter;
+          print_string ("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
+          flush stdout;
         else ()
       done
     with End_of_file -> ()
+
+
+let _ = 
+  if Array.length Sys.argv < 2 then printUsage()
+  else
+    let choice = Sys.argv.(1) in
+    match choice with
+    | "sat" -> choiceSat ()
+    | "print" -> choicePrint ()
+    | _ -> printUsage ()
+
+