From ee45f2fdd552a6c857de1d7320402f8adbdadded 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:49:29 +0200
Subject: [PATCH] Add testcases for nominal
---
src/testsuite/cool-testsuite.ml | 12 +++++++++++-
1 file changed, 11 insertions(+), 1 deletion(-)
diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml
index 8961a23..649a26b 100644
--- a/src/testsuite/cool-testsuite.ml
+++ b/src/testsuite/cool-testsuite.ml
@@ -22,6 +22,15 @@ let k_testcases: satCheck list =
; c Sat "C |- [R] ~C"
]
+
+let nominal_testcases =
+ let c a b = (a,k,b) in
+ [ c Sat "@ i' <r> p"
+ ; c Sat "@ i' <r> i'"
+ ; c Unsat "@ i' <r> i' & @i' [r] ~ i'"
+ ; c Sat "@ i' [r] (@ i' (~i')) "
+ ]
+
let kd_testcases =
let c a b = (a,kd,b) in
[ c Sat "True"
@@ -36,12 +45,13 @@ let kd_testcases =
let testcases =
let c name table = (name,table) in
[ c "K" k_testcases
+ ; c "Nominals" nominal_testcases
; c "KD" kd_testcases
]
let main =
foreach_l testcases (fun (name,table) ->
- Printf.printf "\n==== Testing logic %s ====\n" name;
+ Printf.printf "\n==== Testing %s ====\n" name;
foreach_l table runSatCheckVerbose
)
--
GitLab