Commit ee45f2fd authored by Thorsten Wißmann's avatar Thorsten Wißmann 🐧
Browse files

Add testcases for nominal

parent abc6c263
......@@ -22,6 +22,15 @@ let k_testcases: satCheck list =
; c Sat "C |- [R] ~C"
]
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')) "
]
let kd_testcases =
let c a b = (a,kd,b) in
[ c Sat "True"
......@@ -36,12 +45,13 @@ let kd_testcases =
let testcases =
let c name table = (name,table) in
[ c "K" k_testcases
; c "Nominals" nominal_testcases
; c "KD" kd_testcases
]
let main =
foreach_l testcases (fun (name,table) ->
Printf.printf "\n==== Testing logic %s ====\n" name;
Printf.printf "\n==== Testing %s ====\n" name;
foreach_l table runSatCheckVerbose
)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment