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

Add more testcases for K

parent e5426cbb
......@@ -56,7 +56,7 @@ let runSatCheckVerbose (sc:satCheck) =
let cs = colored_string in
let sotr = terminal_string_of_testResult in
let (expectation,_,title) = sc in
PF.printf "Is %s " (cs "1" (columnCreate 50 title));
PF.printf "Is %s " (cs "1" (columnCreate 60 title));
PF.printf "%s? → " (sotr expectation);
let res = runSatCheck sc in
(if (res = expectation)
......
......@@ -23,8 +23,15 @@ let k_testcases: satCheck list =
; c Unsat "<R> ((<R> C) & (<S> False))"
; c Unsat "<X> (<S> False) | <R> ((<R> C) & (<S> False))"
; c Unsat "<X> (<S> False) | <R> ((<R> C) & (<S> False))"
(* Some DL98-Testcases *)
; c Sat "<R> A & <R> B |- [R] C"
; c Unsat "<R> A & <R> B |- [R] (~A & ~B)"
; c Unsat "<R> A & <R> B |- [R] ~B"
; c Sat "<R> A & <R> ~A |- [R] B"
; c Unsat "<R> A & <R> ~A & (B => [R] ~A) |- [R] B"
; c Sat "<R> A & <R> ~A & (B => [R] ~A) & (C => ~D) & (D => ~E) & <R> C & <R> D & <R> E |- True"
; c Unsat "<R> D & <R> E & ((<R> D & <R> E) => [R] E) & ~(D & E) |- True"
; c Sat "(<R> D | <R> E) & ((<R> D & <R> E) => [R] E) & ~(D & E) |- True"
; c Sat "<R> D & <R> E & ((<R> D & <R> E) => [R] E) & (D & E => <R> ~(D&E)) |- True"
]
......
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