Enable tboxes for tatl cl solver

CoolUtils.ml

@@ -32,6 +32,9 @@ module TList = struct
                   let oth = List.map (fun x -> h::x) pt in
                   List.append pt oth
     let prod la lb = List.concat (List.map (fun a -> List.map (fun b -> (a,b)) lb) la)
+    let empty l = match l with
+                  | (_::_) -> false
+                  | [] -> true
 end
 
 let agents = ref ([|1;2;3;4;5|])

CoolUtils.mli

@@ -14,6 +14,7 @@ module TList : sig
     val zip : ('a list) -> ('b list) -> ('a * 'b) list
     val powerset : ('a list) -> ('a list list)
     val prod : ('a list) -> ('b list) -> (('a * 'b) list)
+    val empty : ('a list) -> bool
 end
 
 val cl_get_agents : unit -> int array

coalgcompare.ml

@@ -142,7 +142,11 @@ let solvFact (tbox, sf) timeout =
 
 let solvTatl agents (tbox,(_,sf)) timeout = (* ignore the TBox... *)
   let tatl = "./tatl" in
-  let inp = CoAlgFormula.exportTatlFormula (C.AND (sf, C.ALLOWS (agents,C.TRUE))) in
+  let tboxlist = List.map (fun (_,f) -> CoAlgFormula.exportTatlFormula f) tbox in
+  let agstr = String.concat "," (List.map string_of_int agents) in
+  let tboxstr = "~<<"^agstr^">>F~ ("^(String.concat " /\\ " tboxlist) ^ ") /\\ " in
+  let inp = CoAlgFormula.exportTatlFormula sf in
+  let inp = if TList.empty tbox then inp else (tboxstr ^ "(" ^ inp ^ ")") in
   G.callExt (Some ("1\n"^inp^"\n4")) tatl [] (Str.regexp_string "The formula is satisfiable") timeout
 
 let solvCool functorname (tbox,sf) timeout =