From 5043b2580ccf5f6237aed3983deaa8dd18378e84 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Fri, 11 Jul 2014 19:06:08 +0200
Subject: [PATCH] Add more testcases for K
---
src/testsuite/Testsuite.ml | 2 +-
src/testsuite/cool-testsuite.ml | 11 +++++++++--
2 files changed, 10 insertions(+), 3 deletions(-)
diff --git a/src/testsuite/Testsuite.ml b/src/testsuite/Testsuite.ml
index 9bd812c..80e053d 100644
--- a/src/testsuite/Testsuite.ml
+++ b/src/testsuite/Testsuite.ml
@@ -56,7 +56,7 @@ let runSatCheckVerbose (sc:satCheck) =
let cs = colored_string in
let sotr = terminal_string_of_testResult in
let (expectation,_,title) = sc in
- PF.printf "Is %s " (cs "1" (columnCreate 50 title));
+ PF.printf "Is %s " (cs "1" (columnCreate 60 title));
PF.printf "%s? → " (sotr expectation);
let res = runSatCheck sc in
(if (res = expectation)
diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml
index 7d0f144..e8517d4 100644
--- a/src/testsuite/cool-testsuite.ml
+++ b/src/testsuite/cool-testsuite.ml
@@ -23,8 +23,15 @@ let k_testcases: satCheck list =
; c Unsat "<R> ((<R> C) & (<S> False))"
; c Unsat "<X> (<S> False) | <R> ((<R> C) & (<S> False))"
; c Unsat "<X> (<S> False) | <R> ((<R> C) & (<S> False))"
-
- (* Some DL98-Testcases *)
+ ; c Sat "<R> A & <R> B |- [R] C"
+ ; c Unsat "<R> A & <R> B |- [R] (~A & ~B)"
+ ; c Unsat "<R> A & <R> B |- [R] ~B"
+ ; c Sat "<R> A & <R> ~A |- [R] B"
+ ; c Unsat "<R> A & <R> ~A & (B => [R] ~A) |- [R] B"
+ ; c Sat "<R> A & <R> ~A & (B => [R] ~A) & (C => ~D) & (D => ~E) & <R> C & <R> D & <R> E |- True"
+ ; c Unsat "<R> D & <R> E & ((<R> D & <R> E) => [R] E) & ~(D & E) |- True"
+ ; c Sat "(<R> D | <R> E) & ((<R> D & <R> E) => [R] E) & ~(D & E) |- True"
+ ; c Sat "<R> D & <R> E & ((<R> D & <R> E) => [R] E) & (D & E => <R> ~(D&E)) |- True"
]
--
GitLab