From abc6c2637a7e0ed0824a8c312690dba9aff3f458 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:43:20 +0200
Subject: [PATCH] Add testcases for KD
---
src/testsuite/Testsuite.ml | 4 +---
src/testsuite/cool-testsuite.ml | 25 +++++++++++++++++++++++--
2 files changed, 24 insertions(+), 5 deletions(-)
diff --git a/src/testsuite/Testsuite.ml b/src/testsuite/Testsuite.ml
index fecf354..2b1dc92 100644
--- a/src/testsuite/Testsuite.ml
+++ b/src/testsuite/Testsuite.ml
@@ -52,10 +52,8 @@ let runSatCheckVerbose (sc:satCheck) =
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"
+ else PF.printf "%s, it is %s\n"
(cs "1;31" "No")
- (cs "1;31" "Failure")
- (sotr expectation)
(sotr res)
diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml
index 2d610c3..8961a23 100644
--- a/src/testsuite/cool-testsuite.ml
+++ b/src/testsuite/cool-testsuite.ml
@@ -17,11 +17,32 @@ let k_testcases: satCheck list =
; c Unsat "False"
; c ParseError "{Fsdf"
(*; c ParseError "Fsdf}" *)
+ ; c Unsat "<R> True & [R] False"
+ ; c Unsat "C |- <R> ~C"
+ ; c Sat "C |- [R] ~C"
+ ]
+
+let kd_testcases =
+ let c a b = (a,kd,b) in
+ [ c Sat "True"
+ ; c Unsat "False"
+ ; c ParseError "{Fsdf"
+ (*; c ParseError "Fsdf}" *)
+ ; c Unsat "<R> True & [R] False"
+ ; c Unsat "C |- <R> ~C"
+ ; c Unsat "C |- [R] ~C"
+ ]
+
+let testcases =
+ let c name table = (name,table) in
+ [ c "K" k_testcases
+ ; c "KD" kd_testcases
]
let main =
- foreach_l k_testcases (fun tc ->
- runSatCheckVerbose tc
+ foreach_l testcases (fun (name,table) ->
+ Printf.printf "\n==== Testing logic %s ====\n" name;
+ foreach_l table runSatCheckVerbose
)
let _ = main
--
GitLab