Add statistics to testsuite output

src/testsuite/Testsuite.ml

@@ -50,11 +50,11 @@ let runSatCheckVerbose (sc:satCheck) =
     PF.printf "Is %-50s " (cs "1" title);
     PF.printf "%s?… " (sotr expectation);
     let res = runSatCheck sc in
-    if (res = expectation)
+    (if (res = expectation)
     then PF.printf "%s\n" (cs "1;32" "Yes")
     else PF.printf "%s, it is %s\n"
                     (cs "1;31" "No")
-                    (sotr res)
-
+                    (sotr res));
+    res
 
 

src/testsuite/Testsuite.mli

@@ -12,5 +12,5 @@ type testResult = | Sat
 type satCheck = testResult * (CoAlgMisc.sortTable) * string (* expected * functors * formula *)
 
 val runSatCheck : satCheck -> testResult
-val runSatCheckVerbose : satCheck -> unit
+val runSatCheckVerbose : satCheck -> testResult
 

src/testsuite/cool-testsuite.ml

@@ -10,7 +10,6 @@ let kd  = [| (CM.MultiModalKD, [0]) |]
 let cl  = [| (CM.CoalitionLogic, [0]) |]
 let gml = [| (CM.GML, [0]) |]
 
-(* ============ multi modal K ============ *)
 let k_testcases: satCheck list =
     let c a b = (a,k,b) in
     [ c Sat   "True"
@@ -50,10 +49,24 @@ let testcases =
     ]
 
 let main =
+    let success = ref 0 in
+    let failed = ref 0 in
     foreach_l testcases (fun (name,table) ->
-        Printf.printf "\n==== Testing %s ====\n" name;
-        foreach_l table runSatCheckVerbose
-    )
+        Printf.printf "==== Testing %s ====\n" name;
+        foreach_l table (fun sc ->
+            let (expected,_,_) = sc in
+            let actual = runSatCheckVerbose sc in
+            (* compare the expected and the actual result *)
+            if actual = expected
+            then success := !success + 1
+            else failed := !failed + 1
+        );
+        Printf.printf "\n"
+    );
+    let s n = if n = 1 then "testcase" else "testcases" in
+    Printf.printf "=> %d %s succeeded, %d %s failed.\n"
+        !success (s !success)
+        !failed (s !failed)
 
 let _ = main