Skip to content
Snippets Groups Projects
Commit 9fdc9f4d authored by Hans-Peter Deifel's avatar Hans-Peter Deifel Committed by 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 3c42e3f1
Branches
No related tags found
No related merge requests found
......@@ -51,10 +51,10 @@ let k_testcases: satCheck list =
let nominal_testcases =
let c a b = (a,k,b) in
[ c Sat "@ i' <r> p"
; c Sat "@ i' <r> i'"
; c Unsat "@ i' <r> i' & @i' [r] ~ i'"
; c Sat "@ i' [r] (@ i' (~i')) "
[ c Sat "SKIP @ i' <r> p"
; c Sat "SKIP @ i' <r> i'"
; c Unsat "SKIP @ i' <r> i' & @i' [r] ~ i'"
; c Sat "SKIP @ i' [r] (@ i' (~i')) "
]
let kd_testcases =
......@@ -63,9 +63,9 @@ let kd_testcases =
; c Unsat "False"
; c ParseError "{Fsdf"
(*; c ParseError "Fsdf}" *)
; c Unsat "<R> True & [R] False"
; c Unsat "C |- <R> ~C"
; c Unsat "C |- [R] ~C"
; c Unsat "<r> True & [r] False"
; c Unsat "C |- <r> ~C"
; c Unsat "C |- [r] ~C"
]
let cl_testcases : testcase_section =
......@@ -94,17 +94,17 @@ let cl_testcases_2agents : testcase_section =
let kAndKd_testcases : testcase_section =
use_functor "K * KD" __
[ sat "[pi1]True"
; sat "[pi1][R]False"
; unsat "[pi2][R]False"
; sat "i' => [pi1][R] i'"
; sat "i' & [pi1][R] i'"
; unsat "i' => [pi2][R] (~i') |- i' & [pi2] [R] i'"
; sat "[pi1][r]False"
; unsat "[pi2][r]False"
; sat "SKIP i' => [pi1][r] i'"
; sat "SKIP i' & [pi1][r] i'"
; unsat "SKIP 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"
[ 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]);
......@@ -114,8 +114,8 @@ let kOrKd = [| (CoAlgMisc.Choice, [1; 2]);
let kOrKd_testcases : satCheck list =
let c a b = (a,kOrKd,b) in
[ c Sat "( True + False )"
; c Sat "(([R] False) + ([R] False))"
; c Unsat "((False) + ([R] False))"
; c Sat "(([r] False) + ([r] False))"
; c Unsat "((False) + ([r] False))"
]
let pml_testcases : testcase_section =
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment