From 2ed7312f891662ee63c878d28e5e529b35b16a7c Mon Sep 17 00:00:00 2001
From: Hans-Peter Deifel <hans-peter.deifel@fau.de>
Date: Thu, 16 Mar 2017 18:36:12 +0100
Subject: [PATCH] Disable all testcases involving PML
---
src/testsuite/cool-testsuite.ml | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml
index c905d15..dfe5430 100644
--- a/src/testsuite/cool-testsuite.ml
+++ b/src/testsuite/cool-testsuite.ml
@@ -118,12 +118,13 @@ let kOrKd_testcases : satCheck list =
; c Unsat "((False) + ([r] False))"
]
+(* PML is currently disabled. See CoAlgLogics.ml *)
let pml_testcases : testcase_section =
use_functor "PML" __
[ sat "SKIP {>= 1/3} C & {< 1/2} D"
; sat "SKIP {>= 1/3} C & {< 1/2} C"
; unsat "SKIP {< 1/3} C & {>= 1/2} C"
- ; sat "{< 1/3} C & {< 1/2} C"
+ ; sat "SKIP {< 1/3} C & {< 1/2} C"
]
let testcases =
@@ -139,8 +140,8 @@ let testcases =
; kAndK_testcases
; c "K+KD" kOrKd_testcases
; pml_testcases
- ; use_functor "PML + K" __
- [ sat "(P4 + False)"
+ ; use_functor "PML + K" __ (* PML is currently disabled. See CoAlgLogics.ml *)
+ [ sat "SKIP (P4 + False)"
; sat "SKIP (({>= 3/5} p0 & {>= 2/5} p1) + False)"
; sat "SKIP ({>= 3/5} (False + <R1> True & <R2> True) & {>= 2/5} ({>= 1/10} p0 & {>= 1/10} (~ p0) + False ) + False)"
]
--
GitLab