cool-testsuite.ml 2.95 KB
Newer Older
1
2
open CoolUtils
open Testsuite
3
module DL98 = DL98TestCases
4
5
6
7
8
9
10
11
12
13
module CF = CoAlgFormula
module CR = CoAlgReasoner
module CM = CoAlgMisc
module L = List

let k   = [| (CM.MultiModalK,  [0]) |]
let kd  = [| (CM.MultiModalKD, [0]) |]
let cl  = [| (CM.CoalitionLogic, [0]) |]
let gml = [| (CM.GML, [0]) |]

14
15
16
17
18
19
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}" *)
Thorsten Wißmann's avatar
Thorsten Wißmann committed
20
21
22
    ; c Unsat "<R> True & [R] False"
    ; c Unsat "C |- <R> ~C"
    ; c Sat   "C |- [R] ~C"
23
24
25
    ; 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))"
Thorsten Wißmann's avatar
Thorsten Wißmann committed
26
27
28
29
30
31
32
33
34
    ; 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"
Thorsten Wißmann's avatar
Thorsten Wißmann committed
35
36
    ]

Thorsten Wißmann's avatar
Thorsten Wißmann committed
37
38
39
40
41
42
43
44
45

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')) "
    ]

Thorsten Wißmann's avatar
Thorsten Wißmann committed
46
47
48
49
50
51
52
53
54
55
56
let kd_testcases =
    let c a b = (a,kd,b) in
    [ c Sat   "True"
    ; 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"
    ]

57
let cl_testcases : satCheck list =
Thorsten Wißmann's avatar
Thorsten Wißmann committed
58
59
60
61
62
63
64
65
66
    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 )"
    ]

Thorsten Wißmann's avatar
Thorsten Wißmann committed
67
68
let testcases =
    let c name table = (name,table) in
69
70
71
    [ c "DL98 (Sat)"    DL98.satCasesList
    ; c "DL98 (Unsat)"  DL98.unsatCasesList
    ; c "K"  k_testcases
Thorsten Wißmann's avatar
Thorsten Wißmann committed
72
    ; c "Nominals" nominal_testcases
Thorsten Wißmann's avatar
Thorsten Wißmann committed
73
    ; c "KD" kd_testcases
Thorsten Wißmann's avatar
Thorsten Wißmann committed
74
    ; c "CL" cl_testcases
75
    ]
76

77
let main =
78
79
    let success = ref 0 in
    let failed = ref 0 in
Thorsten Wißmann's avatar
Thorsten Wißmann committed
80
    foreach_l testcases (fun (name,table) ->
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
        Printf.printf "==== Testing %s ====\n" name;
        foreach_l table (fun sc ->
            let (expected,_,_) = sc in
            let actual = runSatCheckVerbose sc in
            (* compare the expected and the actual result *)
            if actual = expected
            then success := !success + 1
            else failed := !failed + 1
        );
        Printf.printf "\n"
    );
    let s n = if n = 1 then "testcase" else "testcases" in
    Printf.printf "=> %d %s succeeded, %d %s failed.\n"
        !success (s !success)
        !failed (s !failed)
96
97
98

let _ = main