Add lots of test cases for CTL.

This imports some of the quickly decidable ctl comparision benchmark
formulas into the test suite.

The testsuite also gained a --slow parameter, that enables slower (but
still fairly fast) formulas.

src/testsuite/CTLFormulas.mli

+val unsat_fast : string list
+val unsat_slow : string list
+val sat_fast : string list
+val sat_slow : string list

src/testsuite/CTLTestCases.ml

+(** Test Cases for CTL. See ctl/README.md *)
+
+open Testsuite
+open CTLFormulas
+
+
+let kd   = [| (CoAlgMisc.MultiModalKD,  [0]) |]
+
+let getCases (lines:string list) (res:testResult) : satCheck list =
+  let f line : satCheck = (res, kd, line) in
+  List.map f lines
+
+let fastTests : satCheck list =
+  (getCases sat_fast Sat) @ (getCases unsat_fast Unsat)
+
+let slowTests : satCheck list =
+  fastTests @ (getCases sat_slow Sat) @ (getCases unsat_slow Unsat)

src/testsuite/CTLTestCases.mli

+open Testsuite
+
+val fastTests : satCheck list
+val slowTests : satCheck list

src/testsuite/cool-testsuite.ml

 open CoolUtils
 open Testsuite
 module DL98 = DL98TestCases
+module CTL = CTLTestCases
 module CF = CoAlgFormula
 module CR = CoAlgReasoner
 module CM = CoAlgMisc
@@ -127,10 +128,12 @@ let pml_testcases : testcase_section =
     ; sat   "SKIP {< 1/3} C & {< 1/2} C"
     ]
 
-let testcases =
+let testcases ~(slow:bool) =
     let c name table = (name,__,table) in
     [ c "DL98 (Sat)"    DL98.satCasesList
     ; c "DL98 (Unsat)"  DL98.unsatCasesList
+    ; if slow then c "CTL (slow)" CTL.slowTests
+      else c "CTL (fast)" CTL.fastTests
     ; c "K"  k_testcases
     ; c "Nominals" nominal_testcases
     ; c "KD" kd_testcases
@@ -147,12 +150,12 @@ let testcases =
         ]
     ]
 
-let main =
+let doTests ~(slow:bool) =
     let skipchecker = Str.regexp "SKIP " in (* skip formulas beginning with "SKIP " *)
     let success = ref 0 in
     let skipped = ref 0 in
     let failed = ref 0 in
-    foreach_l testcases (fun (name,init_globals,table) ->
+    foreach_l (testcases slow) (fun (name,init_globals,table) ->
         Printf.printf "==== Testing %s ====\n" name;
         (*
         let (_,sorts,_) = List.hd table in
@@ -181,7 +184,24 @@ let main =
         !failed (s !failed)
         !skipped
 
-let _ = main
-
 
+let printUsage name =
+  print_endline ("Usage: " ^ name ^ " [--slow]");
+  print_endline "";
+  print_endline "Options:";
+  print_endline "  --slow                Enable tests that take a while to complete";
+  print_endline "  -h/--help             Show this help.";
+  exit 1
+
+let _ =
+  let argument = if Array.length Sys.argv == 2 then Some Sys.argv.(1) else None in
+
+  match argument with
+  | None -> doTests ~slow:false
+  | Some "--slow" -> doTests ~slow:true
+  | Some "--help" | Some "-h" -> printUsage (Sys.argv.(0))
+  | Some other -> begin
+      print_endline ("Option " ^ other ^ " not understood.\n");
+      printUsage (Sys.argv.(0))
+    end
 (* vim: set et sw=2 sts=2 ts=8 : *)

src/testsuite/ctl/README.md

+# CTL Testsuite
+
+The tests in `CTLFormulas.ml` are selected formulas from [this benchmark suite].
+
+They are separated into two groups. Those that didn't take longer than
+0.03 seconds on my system to decide and those that did, but finished
+in under 2 seconds.
+
+Here is a one liner to find formulas that take less than a certain
+amount of time to decide:
+
+    while read i; do timeout 0.03s ./coalg.native sat KD < $i >/dev/null && echo $i; done < list.txt
+    
+To import the formulas from a list of files into OCaml, the script
+`formulas_to_ocaml.sh` in this directory can be used:
+
+    ./formulas_to_ocaml.sh VAR-NAME < list.txt
+    
+Run this without arguments to get help.
+
+[this benchmark suite]: http://rsise.anu.edu.au/~rpg/CTLComparisonBenchmarks/CTLComparisonBenchmarksNew.tgz

src/testsuite/ctl/formulas_to_ocaml.sh

+#!/bin/bash
+
+if [[ -z "$1" ]]; then
+    echo "Usage: $0 VAR-NAME" 1>&2
+    echo "" 1>&2
+    echo "Reads a list of files from stdin and generates an ocaml list with the formulas in" 1>&2
+    echo "those files on stdout. The files are expected to contain a single formula and no" 1>&2
+    echo "final newline." 1>&2
+    echo "" 1>&2
+    echo "VAR-NAME: The name of the OCaml variable of the generated list" 1>&2
+    exit 1
+fi
+
+echo "let $1 ="
+
+while read line; do
+    echo -n "  "
+    [[ -z "$first" ]] && echo -n "[" || echo -n ";"
+    echo -n " \""
+    first=true
+    cat $line
+    echo "\""
+done
+
+echo "  ]"