Skip to content
Snippets Groups Projects
Commit 910d5f05 authored by Thorsten Wißmann's avatar Thorsten Wißmann :guitar:
Browse files

Remove redundancy from testsuite file

parent d193f4aa
No related branches found
No related tags found
No related merge requests found
......@@ -7,11 +7,23 @@ module CM = CoAlgMisc
module L = List
module FP = FunctorParsing
let k = [| (CM.MultiModalK, [0]) |]
let kd = [| (CM.MultiModalKD, [0]) |]
let cl = [| (CM.CoalitionLogic, [0]) |]
let gml = [| (CM.GML, [0]) |]
type testcase_section = string * satCheck list
let sat x = (Sat,x)
let unsat x = (Unsat,x)
let parseerror x = (ParseError,x)
let use_functor (functors_: string) (cases: (testResult*string) list): testcase_section =
let sortTable = FP.sortTableFromString functors_ in
let satchecks : satCheck list = List.map (fun (a,b) -> (a,sortTable,b)) cases in
(functors_, satchecks)
let k_testcases: satCheck list =
let c a b = (a,k,b) in
[ c Sat "True"
......@@ -55,26 +67,24 @@ let kd_testcases =
; c Unsat "C |- [R] ~C"
]
let cl_testcases : satCheck list =
let c a b = (a,cl,b) in
[ c Unsat "[{1}] C & [{ 2 }] ~C"
; c Sat "[{1}] C & <{ 2 }> ~C"
; c Unsat "[{1}] C & <{ 1 2 }> ~C"
; c Sat "<{ 1 2 }> C & <{ 1 2 }> ~C"
; c Unsat "<{ 1 2 }> C & [{ 1 2 }] ~C"
; c Sat "([{1 3}] C) & ([{ 2 3 }] ~C )"
let cl_testcases : testcase_section =
use_functor "CL"
[ unsat "[{1}] C & [{ 2 }] ~C"
; sat "[{1}] C & <{ 2 }> ~C"
; unsat "[{1}] C & <{ 1 2 }> ~C"
; sat "<{ 1 2 }> C & <{ 1 2 }> ~C"
; unsat "<{ 1 2 }> C & [{ 1 2 }] ~C"
; sat "([{1 3}] C) & ([{ 2 3 }] ~C )"
]
let kAndKd = FunctorParsing.sortTableFromString "K * KD"
let kAndKd_testcases : satCheck list =
let c a b = (a,kAndKd,b) in
[ c Sat "[pi1]True"
; c Sat "[pi1][R]False"
; c Unsat "[pi2][R]False"
; c Sat "i' => [pi1][R] i'"
; c Sat "i' & [pi1][R] i'"
; c Unsat "i' => [pi2][R] (~i') |- i' & [pi2] [R] i'"
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'"
]
let kOrKd = [| (CoAlgMisc.Choice, [1; 2]);
......@@ -95,8 +105,8 @@ let testcases =
; c "K" k_testcases
; c "Nominals" nominal_testcases
; c "KD" kd_testcases
; c "CL" cl_testcases
; c "K*KD" kAndKd_testcases
; cl_testcases
; kAndKd_testcases
; c "K+KD" kOrKd_testcases
]
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment