Skip to content
Snippets Groups Projects
Commit 2ed7312f authored by Hans-Peter Deifel's avatar Hans-Peter Deifel :turtle:
Browse files

Disable all testcases involving PML

parent 48e6299b
Branches remove-gmlmip
No related tags found
No related merge requests found
...@@ -118,12 +118,13 @@ let kOrKd_testcases : satCheck list = ...@@ -118,12 +118,13 @@ let kOrKd_testcases : satCheck list =
; c Unsat "((False) + ([r] False))" ; c Unsat "((False) + ([r] False))"
] ]
(* PML is currently disabled. See CoAlgLogics.ml *)
let pml_testcases : testcase_section = let pml_testcases : testcase_section =
use_functor "PML" __ use_functor "PML" __
[ sat "SKIP {>= 1/3} C & {< 1/2} D" [ sat "SKIP {>= 1/3} C & {< 1/2} D"
; sat "SKIP {>= 1/3} C & {< 1/2} C" ; sat "SKIP {>= 1/3} C & {< 1/2} C"
; unsat "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 = let testcases =
...@@ -139,8 +140,8 @@ let testcases = ...@@ -139,8 +140,8 @@ let testcases =
; kAndK_testcases ; kAndK_testcases
; c "K+KD" kOrKd_testcases ; c "K+KD" kOrKd_testcases
; pml_testcases ; pml_testcases
; use_functor "PML + K" __ ; use_functor "PML + K" __ (* PML is currently disabled. See CoAlgLogics.ml *)
[ sat "(P4 + False)" [ sat "SKIP (P4 + False)"
; sat "SKIP (({>= 3/5} p0 & {>= 2/5} p1) + 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)" ; sat "SKIP ({>= 3/5} (False + <R1> True & <R2> True) & {>= 2/5} ({>= 1/10} p0 & {>= 1/10} (~ p0) + False ) + False)"
] ]
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment