diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml index c905d1596ac2333ab61f76d231a0523f70cc0706..dfe5430a0176e3424cc53d92b2d645873550d459 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)" ]