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

Add basic testcase checking

parent b33c1f3f
module CM = CoAlgMisc
module PF = Printf
module CR = CoAlgReasoner
......@@ -8,9 +9,54 @@ module CR = CoAlgReasoner
sorts = [| (parseFunctor Sys.argv.(2), [0]) |]
*)
type satCheck = bool * (CoAlgMisc.sortTable) * string (* sat * functors * formula *)
type testResult = | Sat
| Unsat
| ParseError
type satCheck = testResult * (CoAlgMisc.sortTable) * string (* sat * functors * formula *)
let colored_string_of_testResult tr =
match tr with
| Sat -> ("1;33","sat")
| Unsat -> ("1;34","unsat")
| ParseError -> ("31","unparseable")
let colored_string col str =
"\027["^col^"m"^str^"\027[0m"
let terminal_string_of_testResult tr =
let (col,str) = colored_string_of_testResult tr in
colored_string col str
let runSatCheck (_,logic,input) =
try
let nomTable name =
assert (CoAlgFormula.isNominal name);
Some 0
in
let (tbox, f) = CoAlgFormula.importQuery input in
let res = CoAlgReasoner.isSat logic nomTable tbox f in
if res then Sat else Unsat
with | Stream.Error _ -> ParseError
| CoAlgFormula.CoAlgException _ -> ParseError
let runSatCheckVerbose (sc:satCheck) =
let cs = colored_string in
let sotr = terminal_string_of_testResult in
let (expectation,_,title) = sc in
PF.printf "Is %-50s " (cs "1" title);
PF.printf "%s?… " (sotr expectation);
let res = runSatCheck sc in
if (res = expectation)
then PF.printf "%s\n" (cs "1;32" "Yes")
else PF.printf "%s\n -> %s: Expected %s but got %s!\n"
(cs "1;31" "No")
(cs "1;31" "Failure")
(sotr expectation)
(sotr res)
type testResult = | Correct | WrongAnswer | ParseError
let runSatCheck sc =
WrongAnswer
......@@ -4,9 +4,13 @@
sorts = [| (parseFunctor Sys.argv.(2), [0]) |]
*)
type satCheck = bool * (CoAlgMisc.sortTable) * string (* sat * functors * formula *)
type testResult = | Correct | WrongAnswer | ParseError
type testResult = | Sat
| Unsat
| ParseError
type satCheck = testResult * (CoAlgMisc.sortTable) * string (* expected * functors * formula *)
val runSatCheck : satCheck -> testResult
val runSatCheckVerbose : satCheck -> unit
......@@ -10,9 +10,19 @@ let kd = [| (CM.MultiModalKD, [0]) |]
let cl = [| (CM.CoalitionLogic, [0]) |]
let gml = [| (CM.GML, [0]) |]
let main =
print_endline "todo"
(* ============ multi modal K ============ *)
let k_testcases: satCheck list =
let c a b = (a,k,b) in
[ c Sat "True"
; c Unsat "False"
; c ParseError "{Fsdf"
(*; c ParseError "Fsdf}" *)
]
let main =
foreach_l k_testcases (fun tc ->
runSatCheckVerbose tc
)
let _ = main
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