Newer
Older
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 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"
; 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 "[{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 =
; 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 =
[ 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 =
[ 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 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
; 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 skipchecker = Str.regexp "SKIP " in (* skip formulas beginning with "SKIP " *)
let skipped = 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);
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
);
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)
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 : *)