Skip to content
Snippets Groups Projects
Commit 099d525c authored by Hans-Peter Deifel's avatar Hans-Peter Deifel
Browse files

Get testsuite running again

Fixes the syntax of all tests that use R and B as identifiers, which
are keywords now.

Also disables all tests involving nominals as they are currently all
throwing exceptions.
parent e40d0b1d
Branches fix-testsuite
No related tags found
No related merge requests found
...@@ -51,10 +51,10 @@ let k_testcases: satCheck list = ...@@ -51,10 +51,10 @@ let k_testcases: satCheck list =
let nominal_testcases = let nominal_testcases =
let c a b = (a,k,b) in let c a b = (a,k,b) in
[ c Sat "@ i' <r> p" [ c Sat "SKIP @ i' <r> p"
; c Sat "@ i' <r> i'" ; c Sat "SKIP @ i' <r> i'"
; c Unsat "@ i' <r> i' & @i' [r] ~ i'" ; c Unsat "SKIP @ i' <r> i' & @i' [r] ~ i'"
; c Sat "@ i' [r] (@ i' (~i')) " ; c Sat "SKIP @ i' [r] (@ i' (~i')) "
] ]
let kd_testcases = let kd_testcases =
...@@ -63,9 +63,9 @@ let kd_testcases = ...@@ -63,9 +63,9 @@ let kd_testcases =
; c Unsat "False" ; c Unsat "False"
; c ParseError "{Fsdf" ; c ParseError "{Fsdf"
(*; c ParseError "Fsdf}" *) (*; c ParseError "Fsdf}" *)
; c Unsat "<R> True & [R] False" ; c Unsat "<r> True & [r] False"
; c Unsat "C |- <R> ~C" ; c Unsat "C |- <r> ~C"
; c Unsat "C |- [R] ~C" ; c Unsat "C |- [r] ~C"
] ]
let cl_testcases : testcase_section = let cl_testcases : testcase_section =
...@@ -94,17 +94,17 @@ let cl_testcases_2agents : testcase_section = ...@@ -94,17 +94,17 @@ let cl_testcases_2agents : testcase_section =
let kAndKd_testcases : testcase_section = let kAndKd_testcases : testcase_section =
use_functor "K * KD" __ use_functor "K * KD" __
[ sat "[pi1]True" [ sat "[pi1]True"
; sat "[pi1][R]False" ; sat "[pi1][r]False"
; unsat "[pi2][R]False" ; unsat "[pi2][r]False"
; sat "i' => [pi1][R] i'" ; sat "SKIP i' => [pi1][r] i'"
; sat "i' & [pi1][R] i'" ; sat "SKIP i' & [pi1][r] i'"
; unsat "i' => [pi2][R] (~i') |- i' & [pi2] [R] i'" ; unsat "SKIP i' => [pi2][r] (~i') |- i' & [pi2] [r] i'"
] ]
let kAndK_testcases : testcase_section = let kAndK_testcases : testcase_section =
use_functor "K * K" __ use_functor "K * K" __
[ sat "[pi1]<R>c0 | [pi1]<S>c1 | [pi2]<T>c3" [ sat "[pi1]<r>c0 | [pi1]<s>c1 | [pi2]<t>c3"
; sat "[pi1]<R>c0 | [pi1]<S>c1 | [pi2]<T>c3 | [pi1][U]c4" ; sat "[pi1]<r>c0 | [pi1]<s>c1 | [pi2]<t>c3 | [pi1][u]c4"
] ]
let kOrKd = [| (CoAlgMisc.Choice, [1; 2]); let kOrKd = [| (CoAlgMisc.Choice, [1; 2]);
...@@ -114,8 +114,8 @@ let kOrKd = [| (CoAlgMisc.Choice, [1; 2]); ...@@ -114,8 +114,8 @@ let kOrKd = [| (CoAlgMisc.Choice, [1; 2]);
let kOrKd_testcases : satCheck list = let kOrKd_testcases : satCheck list =
let c a b = (a,kOrKd,b) in let c a b = (a,kOrKd,b) in
[ c Sat "( True + False )" [ c Sat "( True + False )"
; c Sat "(([R] False) + ([R] False))" ; c Sat "(([r] False) + ([r] False))"
; c Unsat "((False) + ([R] False))" ; c Unsat "((False) + ([r] False))"
] ]
let pml_testcases : testcase_section = let pml_testcases : testcase_section =
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please to comment