From ea6ba7146c028c4a4ea451e98b1634a228a5cca8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Mon, 6 Jul 2015 16:35:33 +0200
Subject: [PATCH] Add crucial testcases for K*K
---
src/testsuite/cool-testsuite.ml | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml
index 4562c8b..3e94b75 100644
--- a/src/testsuite/cool-testsuite.ml
+++ b/src/testsuite/cool-testsuite.ml
@@ -87,6 +87,12 @@ let kAndKd_testcases : testcase_section =
; unsat "i' => [pi2][R] (~i') |- i' & [pi2] [R] i'"
]
+let kAndK_testcases : testcase_section =
+ use_functor "K * K"
+ [ sat "[pi1]<R>c0 | [pi1]<S>c1 | [pi2]<T>c3"
+ ; sat "[pi1]<R>c0 | [pi1]<S>c1 | [pi2]<T>c3 | [pi1][U]c4"
+ ]
+
let kOrKd = [| (CoAlgMisc.Choice, [1; 2]);
(CoAlgMisc.MultiModalK, [0]);
(CoAlgMisc.MultiModalKD, [0])
@@ -115,6 +121,7 @@ let testcases =
; c "KD" kd_testcases
; cl_testcases
; kAndKd_testcases
+ ; kAndK_testcases
; c "K+KD" kOrKd_testcases
; pml_testcases
; use_functor "PML + K"
--
GitLab