counterexampleで元のBIRDSにあったoptionを指定できるように

bin/counterexample.ml

@@ -1,10 +1,22 @@
 open Birds
 open Expr
 
-
-let log = false
-let cex_max = 5
-let timeout = 180
+let parse_args =
+  let log = ref false in
+  let cex_max = ref 5 in
+  let timeout = ref 180 in
+  let inputs = ref [] in
+  let anon_fun input = inputs := input :: !inputs in
+  let usage = "usage: dune exec counterexample [getput|putget|disdelta] [filename]" in
+  let speclist = [
+    ("--log", Arg.Unit (fun () -> log := true), " Print running information");
+    ("-x", Arg.Int (fun d -> cex_max := d), "<size> Get a counterexample with the maximum size if the program is not well-behaved");
+    ("--counterexample", Arg.Int (fun d -> cex_max := d), "<size> The same as -x");
+    ("-t", Arg.Int (fun d -> timeout := d), "<timeout> Timeout (second) (default: 180s)");
+    ("--timeout", Arg.Int (fun d -> timeout := d), "<timeout> The same as -t");
+  ] in
+  let _ = Arg.parse (Arg.align speclist) anon_fun usage in
+  (!log, !cex_max, !timeout, !inputs |> List.rev |> Array.of_list)
 
 let parse_property (property: string) =
   match property with
@@ -13,13 +25,14 @@ let parse_property (property: string) =
   | "disdelta" -> Result.Ok Counterexample.Disdelta
   | p -> Result.Error ("function gen_counterexample called with an unkown property: " ^ p)
 
-
 let _ =
-  if Array.length Sys.argv < 3 then
+  let (log, cex_max, timeout, inputs) = parse_args in
+  if Array.length inputs < 2 then
     print_endline "Invalid arguments. File name must be passed."
   else begin
-    let filename = Sys.argv.(2) in
-    match parse_property Sys.argv.(1) with
+    let _ = Array.iter print_endline inputs in
+    let filename = inputs.(1) in
+    match parse_property inputs.(0) with
     | Result.Error err ->
       print_endline @@ err
     | Result.Ok property ->