cool-testsuite.ml

open CoolUtils
open Testsuite
module DL98 = DL98TestCases
module CTL = CTLTestCases
module CF = CoAlgFormula
module CR = CoAlgReasoner
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 * (unit -> unit)* satCheck list

let sat x = (Sat,x)
let unsat x = (Unsat,x)
let parseerror x = (ParseError,x)
let __ () = ()

let use_functor (functors_: string) (init_globals: unit->unit) (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_, init_globals, satchecks)

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}" *)
    ; c Unsat "<r> True & [r] False"
    ; c Unsat "c |- <r> ~c"
    ; c Sat   "c |- [r] ~c"
    ; 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))"
    ; 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"
    ]

let aconjunctive_testcases: satCheck list =
  let c a b = (a, k, b) in
  [ (* These formulas are aconjunctive *)
    c Sat "ν x. ν y. ([r] x & <r> y)"
  ; c Unsat "ν x. ν y. ([r] x & <r> y & False)"
  (* These formulas aren't *)
  ; c Unsat "μ x. μ y. ([r] x & <r> y)"
  ; c Unsat "(ν x. (<r> True & [r] x)) & (μ x. ((p0 | [r] x) & (~p0 | [r] x)))"
  ]

let nominal_testcases =
    let c a b = (a,k,b) in
    [ c Sat "SKIP @ i' <r> p"
    ; c Sat "SKIP @ i' <r>  i'"
    ; c Unsat "SKIP @ i' <r>  i' & @i' [r] ~ i'"
    ; c Sat "SKIP @ i' [r] (@ i' (~i')) "
    ]

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

let cl_testcases : testcase_section =
    use_functor "CL" (fun () -> CoolUtils.cl_set_agents [|1;2;3;4;5|])
    [ unsat "[{1}] C & [{ 2 }] ~C"
    ; sat   "[{1}] C & <{ 2 }> ~C"
    ; unsat "[{1}] C & <{ 1 2 }> ~C"
    ; sat   "<{ 1 2 }> C & <{ 1 2 }> ~C"
    ; sat   "~([{ }] ~ phi <=>  ~ [{1 2}] phi)"
    ; unsat "<{ 1 2 }> C & [{ 1 2 }] ~C"
    ; unsat "<{ 1 2 3 4 5 }> C & <{ 1 2 3 4 5 }> ~C"
    ; sat   "([{1 3}] C) & ([{ 2 3 }] ~C )"
    ; unsat "[{1}](p3 | ~p5) & ([{1}](p3 | p5) | [{1 2}](p1 | p3)) & ~[{1}](p5 | ~p4) & ([{}](~(p1 | ~p2)) | [{}](~(p1 | ~p4))) & [{}](~(p3 | ~p4)) & (~[{1}](p1 | ~p2) | ~[{1}](p1 | ~p5))"
    ; sat "[{1}](p3 | ~p5) & ([{1}](p3 | p5) | [{1 2}](p1 | p3)) & ~[{1}](p5 | ~p4) & (~[{1 2 }]((p1 | ~p2)) | ~[{1 2}]((p1 | ~p4))) & ~[{1 2}]((p3 | ~p4)) & (~[{1}](p1 | ~p2) | ~[{1}](p1 | ~p5))"
    ]

let cl_testcases_2agents : testcase_section =
    use_functor "CL" (fun () -> CoolUtils.cl_set_agents [|1;2|])
    [ unsat "[{1}] C & [{ 2 }] ~C"
    ; unsat "<{ 1 2 }> C & <{ 1 2 }> ~C"
    ; unsat "~([{ }] ~ phi <=>  ~ [{1 2}] phi)"
    ; unsat "[{1}](p3 | ~p5) & ([{1}](p3 | p5) | [{1 2}](p1 | p3)) & ~[{1}](p5 | ~p4) & ([{}](~(p1 | ~p2)) | [{}](~(p1 | ~p4))) & [{}](~(p3 | ~p4)) & (~[{1}](p1 | ~p2) | ~[{1}](p1 | ~p5))"
    ; unsat "[{1}](p3 | ~p5) & ([{1}](p3 | p5) | [{1 2}](p1 | p3)) & ~[{1}](p5 | ~p4) & (~[{1 2 }]((p1 | ~p2)) | ~[{1 2}]((p1 | ~p4))) & ~[{1 2}]((p3 | ~p4)) & (~[{1}](p1 | ~p2) | ~[{1}](p1 | ~p5))"
    ]

let kAndKd_testcases : testcase_section =
    use_functor "K * KD" __
    [ sat   "[pi1]True"
    ; sat   "[pi1][r]False"
    ; unsat "[pi2][r]False"
    ; sat   "SKIP i' => [pi1][r] i'"
    ; sat   "SKIP i' & [pi1][r] i'"
    ; unsat "SKIP i' => [pi2][r] (~i') |- i' & [pi2] [r] i'"
    ]

let kAndK_testcases : testcase_section =
    use_functor "K * K" __
    [ sat   "[pi1]<r>c0 | [pi1]<s>c1 | [pi2]<t>c3"
    ; sat   "[pi1]<r>c0 | [pi1]<s>c1 | [pi2]<t>c3 | [pi1][u]c4"
    ]

let kOrKd = [| (CoAlgMisc.Choice, [1; 2]);
               (CoAlgMisc.MultiModalK, [0]);
               (CoAlgMisc.MultiModalKD, [0])
            |]
let kOrKd_testcases : satCheck list =
    let c a b = (a,kOrKd,b) in
    [ c Sat   "( True + False )"
    ; c Sat   "(([r] False) + ([r] False))"
    ; c Unsat "((False) + ([r] False))"
    ]

(* PML is currently disabled. See CoAlgLogics.ml *)
let pml_testcases : testcase_section =
    use_functor "PML" __
    [ sat   "SKIP {>= 1/3} C & {< 1/2} D"
    ; sat   "SKIP {>= 1/3} C & {< 1/2} C"
    ; unsat "SKIP {< 1/3} C & {>= 1/2} C"
    ; sat   "SKIP {< 1/3} C & {< 1/2} C"
    ]

let testcases ~(slow:bool) =
    let c name table = (name,__,table) in
    [ c "DL98 (Sat)"    DL98.satCasesList
    ; c "DL98 (Unsat)"  DL98.unsatCasesList
    ; if slow then c "CTL (slow)" CTL.slowTests
      else c "CTL (fast)" CTL.fastTests
    ; c "K"  k_testcases
    ; c "Nominals" nominal_testcases
    ; c "KD" kd_testcases
    ; cl_testcases
    ; cl_testcases_2agents
    ; kAndKd_testcases
    ; kAndK_testcases
    ; c "K+KD" kOrKd_testcases
    ; pml_testcases
    ; use_functor "PML + K" __ (* PML is currently disabled. See CoAlgLogics.ml *)
        [ sat "SKIP (P4 + False)"
        ; sat "SKIP (({>= 3/5} p0 & {>= 2/5} p1) + False)"
        ; sat "SKIP ({>= 3/5} (False + <R1> True & <R2> True) & {>= 2/5} ({>= 1/10} p0 & {>= 1/10} (~ p0) + False ) + False)"
        ]
    ; c "K-mu (aconjunctive fragment)" aconjunctive_testcases
    ]

let doTests ~(slow:bool) =
    let skipchecker = Str.regexp "SKIP " in (* skip formulas beginning with "SKIP " *)
    let success = ref 0 in
    let skipped = ref 0 in
    let failed = ref 0 in
    foreach_l (testcases slow) (fun (name,init_globals,table) ->
        Printf.printf "==== Testing %s ====\n" name;
        (*
        let (_,sorts,_) = List.hd table in
        Printf.printf "sortTable = %s\n" (FP.stringFromSortTable sorts);
        *)
        init_globals();
        foreach_l table (fun sc ->
            let (expected,sort,formula) = sc in
            if Str.string_match skipchecker formula 0
            then begin
                print_endline ("Skipping formula »"^formula^"«");
                skipped := !skipped + 1
            end else begin
                let actual = runSatCheckVerbose sc in
                (* compare the expected and the actual result *)
                if actual = expected
                then success := !success + 1
                else failed := !failed + 1
            end
        );
        print_endline ""
    );
    let s n = if n = 1 then "testcase" else "testcases" in
    Printf.printf "=> %d %s succeeded, %d %s failed, %d skipped.\n"
        !success (s !success)
        !failed (s !failed)
        !skipped


let printUsage name =
  print_endline ("Usage: " ^ name ^ " [--slow]");
  print_endline "";
  print_endline "Options:";
  print_endline "  --slow                Enable tests that take a while to complete";
  print_endline "  -h/--help             Show this help.";
  exit 1

let _ =
  let argument = if Array.length Sys.argv == 2 then Some Sys.argv.(1) else None in

  match argument with
  | None -> doTests ~slow:false
  | Some "--slow" -> doTests ~slow:true
  | Some "--help" | Some "-h" -> printUsage (Sys.argv.(0))
  | Some other -> begin
      print_endline ("Option " ^ other ^ " not understood.\n");
      printUsage (Sys.argv.(0))
    end
(* vim: set et sw=2 sts=2 ts=8 : *)