Make agent list configurable via --agents

CoAlgLogics.ml

@@ -194,7 +194,10 @@ let compatible sort (a: bset) formula1 =
      /\ n                         /\ m              all C_i ⊆ D
     /  \i=1 a_i        /\    b   /  \j=1 c_j
 *)
-let agents = [|1;2;3;4;5;6;7;8;9;10|]
+let agents = ref ([|1;2;3;4;5;6;7;8;9;10|])
+
+let cl_get_agents () = !agents
+let cl_set_agents arr = ignore (agents := arr)
 
 let mkRule_CL sort bs sl =
   assert (List.length sl = 1); (* TODO: Why? *)
@@ -205,7 +208,7 @@ let mkRule_CL sort bs sl =
   let nCands = bsetMakeRealEmpty () in (* all N-diamonds *)
   let hasFullAgentList formula =
     let aglist = lfGetDestAg sort formula in
-    let value = TArray.all (fun x -> TArray.elem x aglist) agents in
+    let value = TArray.all (fun x -> TArray.elem x aglist) !agents in
     if (value) then bsetAdd nCands formula else () ;
     value
   in

CoAlgLogics.mli

@@ -6,5 +6,7 @@
 open CoAlgMisc
 
 
-val agents : int array
+val cl_get_agents : unit -> int array
+val cl_set_agents : int array -> unit
+
 val getExpandingFunctionProducer : functors -> sort -> bset -> sort list -> stateExpander

coalg.ml

@@ -35,11 +35,17 @@ let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increm
 
 
 let printUsage () =
-  print_endline "Usage: \"alc <task> <functor> [<verbose>]\" where";
+  print_endline "Usage: \"alc <task> <functor> [<flags>]\" where";
   print_endline "       <task> in { sat print }";
   print_endline "       <functor> in { MultiModalK MultiModalKD CoalitionLogic GML";
   print_endline "                      (or: K)     (or: KD)     (or: CL)       }";
-  print_endline "       <verbose> = any (second) argument";
+  print_endline "       <flags> = a list of the following items";
+  print_endline "           --agents AGLIST";
+  print_endline "             expects the next argument AGLIST to be a list of integers";
+  print_endline "             which is treaten as the set of agents for CL formulas";
+  print_endline "             it defaults to 1,2,3,4,5,6,7,8,9,10";
+  print_endline "           --verbose";
+  print_endline "             print verbose output for sat task";
   print_endline "";
   print_endline "Examples:";
   print_endline "  OCAMLRUNPARAM=b ./coalg sat K <<< '[R] False'";
@@ -48,6 +54,7 @@ let printUsage () =
   exit 1
 
 let counter = ref 0
+let verbose = ref false
 
 let parseFunctor str =
     match str with
@@ -61,7 +68,7 @@ let parseFunctor str =
     | _ -> raise (CoAlgFormula.CoAlgException ("Unknown Functor name »" ^ str ^ "«"))
 
 let choiceSat () =
-    let verb = Array.length Sys.argv > 3 in
+    let verb = !verbose in
     let sorts = [| (parseFunctor Sys.argv.(2), [0]) |] in
     let printRes sat =
       if not verb then
@@ -95,11 +102,32 @@ let choicePrint () =
       done
     with End_of_file -> ()
 
+let rec parseFlags arr offs : unit =
+    let offs = ref (offs) in
+    let getParam () =
+        if ((!offs + 1) >= Array.length arr) then
+            raise (CoAlgFormula.CoAlgException ("Parameter missing for flag »" ^ (arr.(!offs)) ^ "«"))
+        else
+            offs := !offs + 1;
+            arr.(!offs)
+    in
+    if (!offs >= Array.length arr) then ()
+    else (ignore (match arr.(!offs) with
+         | "--verbose" -> verbose := true
+         | "--agents" ->
+            let strAglist = getParam () in
+            let aglist = List.map int_of_string (Str.split (Str.regexp ",") strAglist) in
+            CoAlgLogics.cl_set_agents (Array.of_list aglist)
+         | _ ->
+            raise (CoAlgFormula.CoAlgException ("Unknown flag »" ^ (arr.(!offs)) ^ "«"))
+         ) ; parseFlags arr (!offs + 1)
+     )
 
 let _ =
   if Array.length Sys.argv < 3 then printUsage()
   else
     let choice = Sys.argv.(1) in
+    parseFlags Sys.argv 3;
     match choice with
     | "sat" -> choiceSat ()
     | "print" -> choicePrint ()