From ab2d3adcafbb574cb16b73faba508756e5612599 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Fri, 16 May 2014 20:17:28 +0200
Subject: [PATCH] Add basic testcase checking
---
src/testsuite/Testsuite.ml | 54 ++++++++++++++++++++++++++++++---
src/testsuite/Testsuite.mli | 8 +++--
src/testsuite/cool-testsuite.ml | 14 +++++++--
3 files changed, 68 insertions(+), 8 deletions(-)
diff --git a/src/testsuite/Testsuite.ml b/src/testsuite/Testsuite.ml
index 22359e2..fecf354 100644
--- a/src/testsuite/Testsuite.ml
+++ b/src/testsuite/Testsuite.ml
@@ -1,6 +1,7 @@
module CM = CoAlgMisc
+module PF = Printf
module CR = CoAlgReasoner
@@ -8,9 +9,54 @@ module CR = CoAlgReasoner
sorts = [| (parseFunctor Sys.argv.(2), [0]) |]
*)
-type satCheck = bool * (CoAlgMisc.sortTable) * string (* sat * functors * formula *)
+type testResult = | Sat
+ | Unsat
+ | ParseError
+
+type satCheck = testResult * (CoAlgMisc.sortTable) * string (* sat * functors * formula *)
+
+
+
+let colored_string_of_testResult tr =
+ match tr with
+ | Sat -> ("1;33","sat")
+ | Unsat -> ("1;34","unsat")
+ | ParseError -> ("31","unparseable")
+
+let colored_string col str =
+ "\027["^col^"m"^str^"\027[0m"
+
+let terminal_string_of_testResult tr =
+ let (col,str) = colored_string_of_testResult tr in
+ colored_string col str
+
+let runSatCheck (_,logic,input) =
+ try
+ let nomTable name =
+ assert (CoAlgFormula.isNominal name);
+ Some 0
+ in
+ let (tbox, f) = CoAlgFormula.importQuery input in
+ let res = CoAlgReasoner.isSat logic nomTable tbox f in
+ if res then Sat else Unsat
+ with | Stream.Error _ -> ParseError
+ | CoAlgFormula.CoAlgException _ -> ParseError
+
+
+let runSatCheckVerbose (sc:satCheck) =
+ let cs = colored_string in
+ let sotr = terminal_string_of_testResult in
+ let (expectation,_,title) = sc in
+ PF.printf "Is %-50s " (cs "1" title);
+ PF.printf "%s?… " (sotr expectation);
+ let res = runSatCheck sc in
+ if (res = expectation)
+ then PF.printf "%s\n" (cs "1;32" "Yes")
+ else PF.printf "%s\n -> %s: Expected %s but got %s!\n"
+ (cs "1;31" "No")
+ (cs "1;31" "Failure")
+ (sotr expectation)
+ (sotr res)
+
-type testResult = | Correct | WrongAnswer | ParseError
-let runSatCheck sc =
- WrongAnswer
diff --git a/src/testsuite/Testsuite.mli b/src/testsuite/Testsuite.mli
index ae17962..2276f95 100644
--- a/src/testsuite/Testsuite.mli
+++ b/src/testsuite/Testsuite.mli
@@ -4,9 +4,13 @@
sorts = [| (parseFunctor Sys.argv.(2), [0]) |]
*)
-type satCheck = bool * (CoAlgMisc.sortTable) * string (* sat * functors * formula *)
-type testResult = | Correct | WrongAnswer | ParseError
+type testResult = | Sat
+ | Unsat
+ | ParseError
+
+type satCheck = testResult * (CoAlgMisc.sortTable) * string (* expected * functors * formula *)
val runSatCheck : satCheck -> testResult
+val runSatCheckVerbose : satCheck -> unit
diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml
index ab625be..2d610c3 100644
--- a/src/testsuite/cool-testsuite.ml
+++ b/src/testsuite/cool-testsuite.ml
@@ -10,9 +10,19 @@ let kd = [| (CM.MultiModalKD, [0]) |]
let cl = [| (CM.CoalitionLogic, [0]) |]
let gml = [| (CM.GML, [0]) |]
-let main =
- print_endline "todo"
+(* ============ multi modal K ============ *)
+let k_testcases: satCheck list =
+ let c a b = (a,k,b) in
+ [ c Sat "True"
+ ; c Unsat "False"
+ ; c ParseError "{Fsdf"
+ (*; c ParseError "Fsdf}" *)
+ ]
+let main =
+ foreach_l k_testcases (fun tc ->
+ runSatCheckVerbose tc
+ )
let _ = main
--
GitLab