diff --git a/HACKING b/HACKING
index 35fdb70fe01aae676911ad58a6d3d19e446292a6..0d66b0a631849c1f6d8a09fea3de5b53f2dcb039 100644
--- a/HACKING
+++ b/HACKING
@@ -11,6 +11,21 @@ As most of the API currently doesn't have documentation comments, this is mainly
useful for getting hyperlinked `.mli`-files. But please feel free to add more
comments.
+== Tests
+
+There are two sets of tests: Integration tests in `src/testsuite` and unit tests
+in `src/unit-tests`. The former can be used to test the whole reasoner on
+example formulas with known satisfiability, the latter is for individual
+functions.
+
+To run all tests, run `make test`. You will need to install the additional
+dependency `ounit`. The individual test suites can be run with
+`./cool-testsuite.native` and `./cool_unit_tests.native` respectively.
+
+If unit tests are not being build, use
+
+ ocaml setup.ml -configure --enable-tests
+
Adding another Functor
----------------------
diff --git a/Makefile b/Makefile
index 8adf527eae31067ba9dfd11cde9904161eadaa59..3bfc7f64fdf813be52ef3b18b7c0becfcae46973 100644
--- a/Makefile
+++ b/Makefile
@@ -1,16 +1,44 @@
+# OASIS_START
+# DO NOT EDIT (digest: a3c674b4239234cbbe53afe090018954)
-.PHONY: all clean
+SETUP = ocaml setup.ml
+
+build: setup.data
+ $(SETUP) -build $(BUILDFLAGS)
+
+doc: setup.data build
+ $(SETUP) -doc $(DOCFLAGS)
+
+test: setup.data build
+ $(SETUP) -test $(TESTFLAGS)
all: setup.ml
- ocaml setup.ml -build
+ $(SETUP) -all $(ALLFLAGS)
+
+install: setup.data
+ $(SETUP) -install $(INSTALLFLAGS)
+
+uninstall: setup.data
+ $(SETUP) -uninstall $(UNINSTALLFLAGS)
+
+reinstall: setup.data
+ $(SETUP) -reinstall $(REINSTALLFLAGS)
+
+clean: setup.ml
+ $(SETUP) -clean $(CLEANFLAGS)
+
+distclean: setup.ml
+ $(SETUP) -distclean $(DISTCLEANFLAGS)
+
+setup.data: setup.ml
+ $(SETUP) -configure $(CONFIGUREFLAGS)
+
+configure: setup.ml
+ $(SETUP) -configure $(CONFIGUREFLAGS)
setup.ml: _oasis
oasis setup
- ocaml setup.ml -configure
-
-clean:
- ! [ -f setup.ml ] || ocaml setup.ml -clean
- oasis setup-clean
- $(RM) -f _tags
- $(RM) -f setup.data setup.ml
- $(RM) -f myocamlbuild.ml
+
+.PHONY: build doc test all install uninstall reinstall clean distclean configure
+
+# OASIS_STOP
diff --git a/_oasis b/_oasis
index ff624cdb8c1733a092799361c402e95805327c6c..ef192680963de7ef70d2a361982f3ccfb3ef79f0 100644
--- a/_oasis
+++ b/_oasis
@@ -1,4 +1,5 @@
OASISFormat: 0.4
+BuildTools: ocamlbuild
Name: cool
Version: 0.1
Synopsis: Coalgebraic Ontology Logic solver
@@ -100,6 +101,25 @@ Executable testsuite
if flag(static)
CCLib: -static
+Test testsuite
+ TestTools: testsuite
+ Command: $testsuite
+
+Executable unit_tests
+ Build$: flag(tests)
+ CompiledObject: native
+ Path: src/unit-tests/
+ BuildTools: ocamlbuild
+ MainIs: cool_unit_tests.ml
+ BuildDepends: libcool, oUnit
+ if flag(static)
+ CCLib: -static
+
+Test unit_tests
+ Run$: flag(tests)
+ TestTools: unit_tests
+ Command: $unit_tests
+
Executable replexample
CompiledObject: native
Path: src/repl-example
diff --git a/src/coalg/coalg.ml b/src/coalg/coalg.ml
index 2ccd7014eaf53a9468cbdce993b9f2742f670603..f06bde32d14471a0a77261d94a882e905fa22a48 100644
--- a/src/coalg/coalg.ml
+++ b/src/coalg/coalg.ml
@@ -12,25 +12,6 @@ module FE = FunctorParsing
open CoolUtils
-(* The type of formulae that are accepted. *)
-(*
-let sorts = Array.make 1 (CoAlgMisc.MultiModalK, [0])
-*)
-(*
-let sorts = Array.make 3 (CoAlgMisc.MultiModalK, [0])
-let _ = sorts.(0) <- (CoAlgMisc.Choice, [1; 2])
-*)
-(*
-let sorts = [| (CoAlgMisc.MultiModalKD, [0])
- (*; (CoAlgMisc.MultiModalKD, [1])
- ; (CoAlgMisc.Fusion, [1; 1]) *)
- |]
-let sorts = [| (CM.MultiModalK, [0])
- (*; (CoAlgMisc.MultiModalKD, [1])
- ; (CoAlgMisc.Fusion, [1; 1]) *)
- |]
-*)
-
(* A partial function mapping nominals to their sorts. *)
let nomTable name =
assert (CoAlgFormula.isNominal name);
@@ -39,11 +20,47 @@ let nomTable name =
let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increment = 67108864; space_overhead = 120 }
-(*
-let _ =
- let str = "A . B C" in
- print_endline (FE.stringFromFunctorExp (FE.functorExpFromString str))
-*)
+type options =
+ { verbose : bool
+ ; fragment : CM.fragment_spec
+ }
+
+let defaultOpts = { verbose = false; fragment = CM.Auto }
+
+let options =
+ [ { Args.long = "verbose"
+ ; Args.short = Some 'v'
+ ; Args.description = "print verbose output with statistics"
+ ; Args.argument = Args.No_arg (fun a -> { a with verbose = true })
+ }
+ ; { Args.long = "agents"
+ ; Args.short = None
+ ; Args.description = "expects the next argument AGLIST to be a list of integers\n"
+ ^ "which is treaten as the set of agents for CL formulas\n"
+ ^ "it defaults to 1,2,3,4,5,6,7,8,9,10"
+ ; Args.argument =
+ let parse_agents strAglist =
+ let aglist = List.map int_of_string (Str.split (Str.regexp ",") strAglist) in
+ CoolUtils.cl_set_agents (Array.of_list aglist)
+ in
+ Args.Required_arg ("AGLIST", fun s a -> parse_agents s; a)
+ }
+ ; { Args.long = "fragment"
+ ; Args.short = None
+ ; Args.description = "Use reasoner algorithm specialized to FRAGMENT.\n"
+ ^ "Possible values are: auto, altfree, altfreeaconj\n"
+ ^ "where \"auto\" detects the fragment from the given formulas"
+ ; Args.argument =
+ let parse_fragment s = match s with
+ | "auto" -> CM.Auto
+ | "altfree" -> CM.Fragment CM.AlternationFree
+ | "altfreeaconj" -> CM.Fragment CM.AconjunctiveAltFree
+ | _ -> raise (Args.ParseError ("Unknown fragment " ^ s))
+ in
+ Args.Required_arg
+ ("FRAGMENT", fun s a -> { a with fragment = parse_fragment s })
+ }
+ ]
let printUsage name =
print_endline ("Usage: \"" ^ name ^ " <task> <functor> [<flags>]\" where");
@@ -61,12 +78,7 @@ let printUsage name =
print_endline " or <functor> . <functor> (binds strongest)";
print_endline " (so K+KD.CL*Id stand for (K + ((KD.CL) * Id)))";
print_endline " <flags> = a list of the following items";
- print_endline " --agents AGLIST";
- print_endline " expects the next argument AGLIST to be a list of integers";
- print_endline " which is treaten as the set of agents for CL formulas";
- print_endline " it defaults to 1,2,3,4,5,6,7,8,9,10";
- print_endline " --verbose";
- print_endline " print verbose output for sat task";
+ Args.help stdout 11 options;
print_endline "";
print_endline "Problems are read from standard input and have the form";
print_endline " [ ass_1; .. ; ass_n |- ] concept";
@@ -90,10 +102,9 @@ let printUsage name =
exit 1
let counter = ref 0
-let verbose = ref false
-let choiceSat () =
- let verb = !verbose in
+let choiceSat opts =
+ let verb = opts.verbose in
let sorts = (FE.sortTableFromString Sys.argv.(2)) in
(* test if GML or PML occurs in sort table *)
@@ -114,13 +125,13 @@ let choiceSat () =
incr counter;
print_string ("\nFormula " ^ (string_of_int !counter) ^ ": ");
flush stdout;
- printRes (CoAlgReasoner.isSat ~verbose:verb sorts nomTable tbox f)
+ printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox f)
else ()
done
with End_of_file -> ()
-let choiceProvable () =
- let verb = !verbose in
+let choiceProvable opts =
+ let verb = opts.verbose in
let sorted_not ((s,f):CF.sortedFormula) : CF.sortedFormula =
(s,CF.NOT f)
in
@@ -139,12 +150,12 @@ let choiceProvable () =
incr counter;
print_string ("\nFormula " ^ (string_of_int !counter) ^ ": ");
flush stdout;
- printRes (CoAlgReasoner.isSat ~verbose:verb sorts nomTable tbox fneg)
+ printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox fneg)
else ()
done
with End_of_file -> ()
-let choicePrint () =
+let choicePrint opts =
try
while true do
let input = read_line () in
@@ -158,7 +169,7 @@ let choicePrint () =
done
with End_of_file -> ()
-let choiceNom2fix () =
+let choiceNom2fix opts =
try
while true do
let input = read_line () in
@@ -173,7 +184,7 @@ let choiceNom2fix () =
done
with End_of_file -> ()
-let choiceNNF () =
+let choiceNNF opts =
try
while true do
let input = read_line () in
@@ -187,11 +198,15 @@ let choiceNNF () =
done
with End_of_file -> ()
-let choiceGraph () =
- choiceSat ();
+let choiceGraph opts =
+ let sorts = (FE.sortTableFromString Sys.argv.(2)) in
+
+ let input = read_line () in
+ let (tbox, f) = CoAlgFormula.importQuery input in
+ ignore(CoAlgReasoner.isSat opts.fragment sorts nomTable tbox f);
print_endline (CM.graphToDot ())
-let choiceVerify () =
+let choiceVerify opts =
try
while true do
print_string "> ";
@@ -208,40 +223,21 @@ let choiceVerify () =
done
with End_of_file -> ()
-let rec parseFlags arr offs : unit =
- let offs = ref (offs) in
- let getParam () =
- if ((!offs + 1) >= Array.length arr) then
- raise (CoAlgFormula.CoAlgException ("Parameter missing for flag »" ^ (arr.(!offs)) ^ "«"))
- else
- offs := !offs + 1;
- arr.(!offs)
- in
- if (!offs >= Array.length arr) then ()
- else (ignore (match arr.(!offs) with
- | "--verbose" -> verbose := true
- | "--agents" ->
- let strAglist = getParam () in
- let aglist = List.map int_of_string (Str.split (Str.regexp ",") strAglist) in
- CoolUtils.cl_set_agents (Array.of_list aglist)
- | _ ->
- raise (CoAlgFormula.CoAlgException ("Unknown flag »" ^ (arr.(!offs)) ^ "«"))
- ) ; parseFlags arr (!offs + 1)
- )
-
let _ =
if Array.length Sys.argv < 3 then printUsage (Sys.argv.(0))
else
let choice = Sys.argv.(1) in
- parseFlags Sys.argv 3;
- match choice with
- | "sat" -> choiceSat ()
- | "prov" -> choiceProvable ()
- | "print" -> choicePrint ()
- | "nnf" -> choiceNNF ()
- | "verify" -> choiceVerify ()
- | "graph" -> choiceGraph ()
- | "nom2fix" -> choiceNom2fix()
- | _ -> printUsage (Sys.argv.(0))
+ match Args.parse Sys.argv 3 options defaultOpts with
+ | Args.Error e -> Printf.printf "%s\n\n" e; printUsage (Sys.argv.(0))
+ | Args.Ok opts ->
+ match choice with
+ | "sat" -> choiceSat opts
+ | "prov" -> choiceProvable opts
+ | "print" -> choicePrint opts
+ | "nnf" -> choiceNNF opts
+ | "verify" -> choiceVerify opts
+ | "graph" -> choiceGraph opts
+ | "nom2fix" -> choiceNom2fix opts
+ | _ -> printUsage (Sys.argv.(0))
(* vim: set et sw=2 sts=2 ts=8 : *)
diff --git a/src/coalgcompare/coalgcompare.ml b/src/coalgcompare/coalgcompare.ml
index 8ef8daa3451454ad8076a0e07f69e30f716d3229..548b6bd34deded1400f872e46d48175169064358 100644
--- a/src/coalgcompare/coalgcompare.ml
+++ b/src/coalgcompare/coalgcompare.ml
@@ -124,7 +124,7 @@ let exportALCQuery tbox (_, f) =
let solvCoalg sortTable args =
- G.evaluateFkt (fun (tbox, sf) -> CoAlgReasoner.isSat sortTable nomTable tbox sf) args
+ G.evaluateFkt (fun (tbox, sf) -> CoAlgReasoner.isSat CoAlgMisc.Auto sortTable nomTable tbox sf) args
let solvALC (tbox, sf) =
let args = exportALCQuery tbox sf in
diff --git a/src/debugger/debugger.ml b/src/debugger/debugger.ml
index 7f75b176ecf945dc43933b068ad087c6582b80b3..7efe4f585456a60d7e247914612b9b0e535dc973 100644
--- a/src/debugger/debugger.ml
+++ b/src/debugger/debugger.ml
@@ -100,7 +100,7 @@ let _ =
let formula = Sys.argv.(2) in
let sorts = (FE.sortTableFromString Sys.argv.(1)) in
let (tbox, f) = CoAlgFormula.importQuery formula in
- Reasoner.initReasoner sorts nomTable tbox f;
+ Reasoner.initReasoner CoAlgMisc.Auto sorts nomTable tbox f;
let session = {
Repl.prompt = "> ";
Repl.bindings = Repl.addHelpBinding [
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 6472add496dd83380077f8893889a256752f1e82..f72e7f67534930f6c562728b068268f5ff52397d 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -723,6 +723,56 @@ let rec verifyMuAltFree formula =
raise (CoAlgException ("verifyMuAltFree: CTL should have been removed at this point"))
+exception NotAconjunctive of unit
+
+let isMuAconjunctive (formula:formula) : bool =
+ let module SS = Set.Make(String) in
+
+ (* Accepts formula f and a set of currently bound mu variables. Returns a subset
+ * of those, which actually occured free in the formula.
+ * Raises an CoAlgException if the formula is determined not to be aconjunctive *)
+ let rec verifyMuAconjunctiveInternal (formula:formula) (bound_mu_vars: SS.t) : SS.t =
+ let proc f = verifyMuAconjunctiveInternal f bound_mu_vars in
+ match formula with
+ | VAR s when SS.mem s bound_mu_vars -> SS.singleton s
+ | VAR s -> SS.empty
+ (* s is now bound by a nu and shadows any privious binding s *)
+ | NU (s, a) -> verifyMuAconjunctiveInternal a (SS.remove s bound_mu_vars)
+ (* Bind s in the recursive call but don't return it as occuring free *)
+ | MU (s, a) ->
+ SS.remove s (verifyMuAconjunctiveInternal a (SS.add s bound_mu_vars))
+
+ (* This is the interesting case *)
+ | AND (a, b) ->
+ let a_vars = proc a in
+ let b_vars = proc b in
+
+ (* If both subformulas contain free mu variables, the formula is not aconjunctive *)
+ if not (SS.is_empty a_vars) && not (SS.is_empty b_vars) then
+ raise (NotAconjunctive ())
+ else
+ SS.union a_vars b_vars (* one of them is empty anyways *)
+
+ (* The other cases just pass argument and return value through *)
+ | TRUE | FALSE | AP _
+ | CONST _ | CONSTN _ -> SS.empty
+ | AT (_,a) | NOT a
+ | EX (_,a) | AX (_,a) -> proc a
+ | OR (a,b) | EQU (a,b) | IMP (a,b) -> SS.union (proc a) (proc b)
+ | ENFORCES (_,a) | ALLOWS (_,a)
+ | MIN (_,_,a) | MAX (_,_,a)
+ | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
+ | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
+ | ID(a) -> proc a
+ | NORM(a, b) | NORMN(a, b)
+ | CHC (a,b) -> SS.union (proc a) (proc b)
+ | FUS (_,a) -> proc a
+ | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ ->
+ raise (CoAlgException ("verifyMuAconjunctiveInternal: CTL should have been removed at this point"))
+ in
+ try ignore (verifyMuAconjunctiveInternal formula SS.empty); true
+ with NotAconjunctive () -> false
+
(** Process from outside in. For every variable bound keep the tuple
(name, negations). For every negation crossed map a +1 over snd on
that list. For every variable met check that the matching
@@ -791,7 +841,7 @@ let rec verifyMuGuarded unguarded formula =
raise (CoAlgException ("verifyMuGuarded: CTL should have been removed at this point"))
let verifyFormula formula =
- ignore (verifyMuAltFree formula);
+ verifyMuAltFree formula;
verifyMuMonotone [] formula;
verifyMuGuarded [] formula
diff --git a/src/lib/CoAlgFormula.mli b/src/lib/CoAlgFormula.mli
index 3fb17edfc6d14e294f745249ede320cd6ef0aba1..cee483d6e346dc2286d16be9d6a87ab75afd4d8a 100644
--- a/src/lib/CoAlgFormula.mli
+++ b/src/lib/CoAlgFormula.mli
@@ -79,6 +79,12 @@ val importFormula : string -> formula
val importSortedFormula : string -> sortedFormula
val importQuery : string -> sortedFormula list * sortedFormula
+(** Decides whether a fomula is aconjunctive.
+
+ A formula is aconjunctive if for every conjunction (a ʌ b), at most one of
+ the conjuncts a, b contains a free μ-variable. *)
+val isMuAconjunctive : formula -> bool
+
val verifyFormula : formula -> unit
val nnfNeg : formula -> formula
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 6d20a7ac4da9096ac1e9d3c49ccc5930e2c457eb..447c4427138564f63ecbd09bf8d0c87391b1ef2f 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -663,6 +663,10 @@ let bsetMakeRealEmpty () =
let res = bsetMake () in
bsetRem res !S.bstrue; (* remove bstrue which is initially in an empty bset *)
res
+let bsetSingleton lf =
+ let res = bsetMakeRealEmpty () in
+ bsetAdd res lf;
+ res
let bsetCopy bs = S.copyBS bs
let bsetFold fkt bs init = S.foldBS fkt bs init
let bsetIter fkt bset = S.iterBS fkt bset
@@ -890,6 +894,13 @@ let atFormulaGetNominal f =
let lfToAt _ lf = lf
+
+type fragment = AlternationFree | AconjunctiveAltFree
+type fragment_spec = Auto | Fragment of fragment
+let fragment = ref AlternationFree
+let getFragment () = !fragment
+
+
(* Calculate all possible formulae. This includes all subformulae and
in the case of μ-Calculus the Fischer-Ladner closure.
@@ -1207,7 +1218,7 @@ let initTablesAt hcF htF name sort =
in
C.HcFHt.iter addAt htF.(sort)
-let ppFormulae nomTbl tbox (s, f) =
+let ppFormulae fragSpec nomTbl tbox (s, f) =
let card = Array.length !sortTable in
if card <= 0 then
raise (C.CoAlgException "Number of sorts must be positive.")
@@ -1268,6 +1279,28 @@ let ppFormulae nomTbl tbox (s, f) =
if size2 > !size then size := size2 else ()
done;
+ begin match fragSpec with
+ | Auto -> if C.isMuAconjunctive f then
+ fragment := AconjunctiveAltFree
+ else
+ fragment := AlternationFree
+ | Fragment AconjunctiveAltFree ->
+ if not (C.isMuAconjunctive f) then
+ raise (CoAlgFormula.CoAlgException "Formula not in required fragment")
+ else fragment := AconjunctiveAltFree
+ | Fragment AlternationFree ->
+ if C.isMuAconjunctive f then
+ raise (CoAlgFormula.CoAlgException "Formula not in required fragment")
+ else fragment := AlternationFree
+ end;
+
+ (* if (fragSpec = Auto || fragSpec = Fragment AconjunctiveAltFree) && C.isMuAconjunctive f then *)
+ (* fragment := AconjunctiveAltFree; *)
+ (* else if (fragSpec = Auto || fragSpec = Fragment AlternationFree) && (not (C.isMuAconjunctive f)) *)
+ (* fragment := AlternationFree; *)
+ (* else *)
+ (* raise (CoAlgFormula.CoAlgException "Formula not in required fragment"); *)
+
arrayFormula := Array.init card (fun _ -> Array.make !size C.TRUE);
arrayType := Array.init card (fun _ -> Array.make !size Other);
arrayDest1 := Array.init card (fun _ -> Array.make !size (-1));
diff --git a/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli
index b38722f508fda56701adccfe04381727a07918f0..d03a537d35dc9b5117cbb6015295ba997c1c364e 100644
--- a/src/lib/CoAlgMisc.mli
+++ b/src/lib/CoAlgMisc.mli
@@ -321,6 +321,7 @@ val nhtFold : (nominal -> bset -> 'a -> 'a) -> nht -> 'a -> 'a
val bsetMake : unit -> bset (* a new bset which only contains True *)
val bsetMakeRealEmpty : unit -> bset (* a new bset without containing True *)
+val bsetSingleton : localFormula -> bset
val bsetAdd : bset -> localFormula -> unit
val bsetMem : bset -> localFormula -> bool
val bsetRem : bset -> int -> unit
@@ -368,8 +369,26 @@ val atFormulaGetNominal : atFormula -> nominal
val lfToAt : sort -> localFormula -> atFormula
-val ppFormulae : (string -> sort option) -> CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula ->
- CoAlgFormula.sortedFormula list * CoAlgFormula.sortedFormula * bset
+(** Sum of different fragments of the full mu-calculus.
+
+ Used by the reasoner to select between different specific algorithms for
+ individual fragments.
+ *)
+type fragment = AlternationFree | AconjunctiveAltFree
+
+type fragment_spec = Auto | Fragment of fragment
+
+(** Return the fragment of the mu-calculus that the original formula uses *)
+val getFragment : unit -> fragment
+
+(** [ppFormulae fragment nomTbl tbox sf] initializes the array representation and various
+ tables for the formula.
+
+ @return (simplified NNF of f, simplified nnf of tbox, bitset containing f)
+ *)
+val ppFormulae : fragment_spec -> (string -> sort option) -> CoAlgFormula.sortedFormula list
+ -> CoAlgFormula.sortedFormula
+ -> CoAlgFormula.sortedFormula list * CoAlgFormula.sortedFormula * bset
(* vim: set et sw=2 sts=2 ts=8 : *)
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index fca69aaf78c08132e7c8dc9bff98cc8815e9c440..583153fdd09eab0d0b3989142858d9c85ca2c775 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -939,36 +939,56 @@ let insertCore sort bs defer =
c
| Some c -> c
+(** Insert cores for the children generated by a modal rule application.
+ *
+ * @return true if all new cores are already unsatisfiable, false otherwise
+ *)
let insertRule state dep chldrn =
let chldrn = listFromLazylist chldrn in
- let insert (isUns, acc) (sort, bs, defer) =
+ let mkCores (sort, bs, defer) =
let bs1 = bsetAddTBox sort bs in
- let core = insertCore sort bs1 defer in
- let isUns1 = if coreGetStatus core = Unsat then isUns else false in
- (isUns1, core::acc)
+ (* For the aconjunctive fragment, instead of adding a core annotated with
+ * all deferrals, we add a core for each formula in the deferral set. *)
+ let deferSingletons =
+ if getFragment () = AconjunctiveAltFree
+ && bsetCompare defer (bsetMakeRealEmpty ()) <> 0 then
+ bsetFold (fun f list -> bsetSingleton f::list) defer []
+ else
+ [defer] in
+ List.map (insertCore sort (bsetCopy bs1)) deferSingletons
+ in
+ (* A list of cores for each child: [[child1a;child1b]; [child2a;child2b]] *)
+ let coresPerChild = List.map mkCores chldrn in
+ (* All combinations that take a core from each child:
+ * [[ch1a;ch2a]; [ch1a;ch2b]; [ch1b;ch2a]; [ch1b;ch2b]]
+ * Neccesary because stateAddRule expects each child to have only one core. *)
+ let coresPerRule = CU.TList.combinations coresPerChild in
+ let addRule cores =
+ let idx = stateAddRule state dep cores in
+ List.iter (fun c -> coreAddParent c state idx) cores;
+ if List.for_all (fun core -> coreGetStatus core = Unsat) cores then begin
+ propagateUnsat [UState (state, Some idx)];
+ true
+ end else
+ false
in
- let (isUnsat, children) = List.fold_left insert (true, []) chldrn in
- let idx = stateAddRule state dep (List.rev children) in
- List.iter (fun c -> coreAddParent c state idx) children;
- if isUnsat then begin
- propagateUnsat [UState (state, Some idx)];
- false
- end else true
-
-let rec insertAllRules state = function
- | [] -> true
- | (dep, chldrn)::tl ->
- let notUnsat = insertRule state dep chldrn in
- if notUnsat then insertAllRules state tl else false
+ List.mem true (List.map (fun r -> addRule r) coresPerRule)
+
+
+(** Call insertRule on all rules
+ * @return true if any rule application generated only unsat cores
+ *)
+let rec insertAllRules state rules =
+ List.mem true (List.map (fun (dep, children) -> insertRule state dep children) rules)
let expandState state =
match stateNextRule state with
| MultipleElements rules ->
- let notUnsat = insertAllRules state rules in
- if notUnsat then stateSetStatus state Open
+ let unsat = insertAllRules state rules in
+ if not unsat then stateSetStatus state Open
| SingleElement (dep, chldrn) ->
- let notUnsat = insertRule state dep chldrn in
- if notUnsat then queueInsertState state else ()
+ let unsat = insertRule state dep chldrn in
+ if not unsat then queueInsertState state else ()
| NoMoreElements -> stateSetStatus state Open
@@ -1050,9 +1070,9 @@ let rec buildGraphLoop () =
(* if propagating nominals added some more queue members, do all again.. *)
if queueIsEmpty () then () else buildGraphLoop ()
-let initReasoner sorts nomTable tbox sf =
+let initReasoner fragSpec sorts nomTable tbox sf =
sortTable := Array.copy sorts;
- let (tbox1, sf1, bs) = ppFormulae nomTable tbox sf in
+ let (tbox1, sf1, bs) = ppFormulae fragSpec nomTable tbox sf in
let sort = fst sf in
let bs1 = bsetAddTBox sort bs in
let deferrals = bsetMakeRealEmpty() in
@@ -1094,9 +1114,9 @@ let reasonerFinished () =
@return True if sf is satisfiable wrt tbox, false otherwise.
*)
-let isSat ?(verbose = false) sorts nomTable tbox sf =
+let isSat ?(verbose = false) fragSpec sorts nomTable tbox sf =
let start = if verbose then Unix.gettimeofday () else 0. in
- initReasoner sorts nomTable tbox sf;
+ initReasoner fragSpec sorts nomTable tbox sf;
let sat =
try
buildGraphLoop ();
diff --git a/src/lib/CoAlgReasoner.mli b/src/lib/CoAlgReasoner.mli
index 52bb178a7fca3ea8b51d142e4282b4b5087d87ad..506af70642ac0269d51226a36d28585eb52aea5a 100644
--- a/src/lib/CoAlgReasoner.mli
+++ b/src/lib/CoAlgReasoner.mli
@@ -13,12 +13,15 @@ type input = sortTable * nomTable * assumptions * CoAlgFormula.sortedFormula
exception ReasonerError of string
-val isSat : ?verbose:bool -> sortTable -> (string -> CoAlgFormula.sort option) ->
- CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool
+val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> sortTable
+ -> (string -> CoAlgFormula.sort option) ->
+ CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool
-val initReasoner : sortTable -> (string -> CoAlgFormula.sort option) ->
- CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> unit
+val initReasoner : CoAlgMisc.fragment_spec -> sortTable
+ -> (string -> CoAlgFormula.sort option) ->
+ CoAlgFormula.sortedFormula list
+ -> CoAlgFormula.sortedFormula -> unit
(** Run a single step of the reasoner. That is: Expand one node and perform sat
propagation.
diff --git a/src/lib/CoolUtils.ml b/src/lib/CoolUtils.ml
index 20141603128437e8d97c304194d29229cd4d86ea..ef61ee63a037780cd295ac16f678aa4d38b3f23c 100644
--- a/src/lib/CoolUtils.ml
+++ b/src/lib/CoolUtils.ml
@@ -35,6 +35,87 @@ module TList = struct
let empty l = match l with
| (_::_) -> false
| [] -> true
+ let rec combinations list = match list with
+ | [] -> []
+ | [l] -> List.map (fun x -> [x]) l
+ | (l::ls) ->
+ let tail = combinations ls in
+ List.fold_left (fun acc x -> acc @ List.map (fun lst -> x::lst) tail) [] l
+end
+
+module Args = struct
+ type 'a param_parser = 'a -> 'a
+ type 'a argument = Required_arg of string * (string -> 'a param_parser)
+ | No_arg of 'a param_parser
+
+ type 'a description =
+ { long : string
+ ; short : char option
+ ; description : string
+ ; argument : 'a argument
+ }
+
+ exception ParseError of string
+
+ let find str mapping =
+ try (List.find (fun arg -> arg.long = str) mapping)
+ with
+ Not_found -> raise (ParseError (Printf.sprintf "Unknown option %s" str))
+
+ let findShort char mapping =
+ try (List.find (fun arg -> arg.short = Some char) mapping)
+ with
+ Not_found -> raise (ParseError (Printf.sprintf "Unknown option %c" char))
+
+ type 'a result = Ok of 'a | Error of string
+
+ let parse ~argv ~offset ~options ~default =
+ let rec parseImpl offs args =
+ let offs = ref (offs) in
+ let getParam () =
+ if ((!offs + 1) >= Array.length argv) then
+ raise (ParseError (Printf.sprintf "Parameter missing for flag »%s«" argv.(!offs)))
+ else
+ offs := !offs + 1;
+ argv.(!offs)
+ in
+ if (!offs >= Array.length argv) then args
+ else
+ let arg = argv.(!offs) in
+ let arg_desc = if String.length arg > 2 && String.sub arg 0 2 = "--" then
+ find (String.sub arg 2 (String.length arg - 2)) options
+ else if String.length arg > 1 && String.get arg 0 = '-' then
+ findShort (String.get arg 1) options
+ else
+ raise (ParseError (Printf.sprintf "Unknown argument %s" arg))
+ in
+ let args = match arg_desc.argument with
+ | Required_arg (_,p) -> p (getParam ()) args
+ | No_arg p -> p args
+ in
+ parseImpl (!offs+1) args
+
+ in
+ try Ok (parseImpl offset default)
+ with ParseError e -> Error e
+
+ let help channel offset mapping =
+ let padding offset = String.make offset ' ' in
+ let help_option desc =
+ let long = "--" ^ desc.long in
+ let short = match desc.short with
+ | Some x -> ",-" ^ Char.escaped x
+ | None -> ""
+ in
+ let var = match desc.argument with
+ | No_arg _ -> ""
+ | Required_arg (a,_) -> " " ^ a
+ in
+ Printf.fprintf channel "%s%s%s%s\n" (padding offset) long short var;
+ (* TODO split_on_char is not available in ocaml < 4.04 *)
+ List.iter (Printf.fprintf channel "%s%s\n" (padding (offset+2))) (String.split_on_char '\n' desc.description)
+ in
+ List.iter help_option mapping
end
let agents = ref ([|1;2;3;4;5|])
diff --git a/src/lib/CoolUtils.mli b/src/lib/CoolUtils.mli
index 62aa41db4e03135a4d2fafc56b36f833ff216931..df6a0b2519191697f8b648a5efbb71d2872f6253 100644
--- a/src/lib/CoolUtils.mli
+++ b/src/lib/CoolUtils.mli
@@ -1,20 +1,69 @@
-(* Some basic utilities as they are known from haskell prelude and so on... *)
+(** Some basic utilities as they are known from haskell prelude and so on... *)
+(** Additional utility functions for the Array module *)
module TArray : sig
val all : ('a -> bool) -> 'a array -> bool
val any : ('a -> bool) -> 'a array -> bool
val elem : 'a -> 'a array -> bool
val included : 'a array -> 'a array -> bool
val to_string : ('a -> string) -> 'a array -> string
- val uniq : 'a array -> 'a array (* delete consecutive duplicates *)
+ val uniq : 'a array -> 'a array (** delete consecutive duplicates *)
end
+(** Additional utility functions for the List module *)
module TList : sig
val zip : ('a list) -> ('b list) -> ('a * 'b) list
val powerset : ('a list) -> ('a list list)
val prod : ('a list) -> ('b list) -> (('a * 'b) list)
val empty : ('a list) -> bool
+
+ (** Compute possible combinations of the sublists.
+
+ [combinations [[1;2];[3;4]] = [[1;3];[1;4];[2;3];[2;4]]]
+ *)
+ val combinations : 'a list list -> 'a list list
+end
+
+(** Command line argument parser *)
+module Args : sig
+ type 'a param_parser = 'a -> 'a
+
+ (** Specifies whether the option takes an addition paramter. *)
+ type 'a argument = Required_arg of string * (string -> 'a param_parser)
+ (** name of the argument and parser.
+ Parser can throw ParseErrors
+ *)
+ | No_arg of 'a param_parser
+
+ type 'a description =
+ { long : string
+ ; short : char option
+ ; description : string
+ ; argument : 'a argument
+ }
+
+ exception ParseError of string
+
+ type 'a result = Ok of 'a | Error of string
+
+ (** parses command line options.
+
+ The user can choose the type 'a, provided they provide parsers and a
+ default value.
+
+ @param argv The Sys.argv array
+ @param offset The index in [argv] where option parsing should start
+ @param options Descriptions of all available options
+ @param default Default value for the option type
+ @return The option type or a parse error
+ *)
+ val parse : argv:string array -> offset:int -> options:'a description list
+ -> default:'a -> 'a result
+
+ (** [help out indent options] prints help for [options] to [out] indented
+ by [indent] characters *)
+ val help : out_channel -> int -> 'a description list -> unit
end
val cl_get_agents : unit -> int array
diff --git a/src/owl/cool-owl.ml b/src/owl/cool-owl.ml
index 55a25b6cfe4f559b58c33c247529776982bcef49..87a2ad2f435de4dc59f0076afffb78cd70e7384c 100644
--- a/src/owl/cool-owl.ml
+++ b/src/owl/cool-owl.ml
@@ -45,7 +45,7 @@ let consistency () =
| (_, []) -> raise (Exception "File needs to contain at least one ontology")
in
let (sorts,nomTable,axioms) = OWL.to_coalg ontology in
- let cons = CR.isSat sorts nomTable axioms (0,CF.TRUE) in
+ let cons = CR.isSat CoAlgMisc.Auto sorts nomTable axioms (0,CF.TRUE) in
let cons = if cons then "yes" else "no" in
let (ontoname, _) = ontology in
Printf.printf "%s consistent: %s\n" ontoname cons
diff --git a/src/testsuite/Testsuite.ml b/src/testsuite/Testsuite.ml
index 1d99e4ae7e668c50fb731e53cd02ea7e6ba8c11c..1cddc01131fdf9055dee5f884cca272ae99c06f5 100644
--- a/src/testsuite/Testsuite.ml
+++ b/src/testsuite/Testsuite.ml
@@ -41,7 +41,7 @@ let runSatCheck (_,logic,input) =
(* isSat leaks tons of memory. Call it in new process to allow the OS to
reclaim that memory between calls. *)
match Unix.fork () with
- | 0 -> let res = CoAlgReasoner.isSat logic nomTable tbox f in
+ | 0 -> let res = CoAlgReasoner.isSat CoAlgMisc.Auto logic nomTable tbox f in
if res then exit 0 else exit 1
| -1 -> raise (CoAlgFormula.CoAlgException "fork() failed")
| _ -> match Unix.wait () with
@@ -68,14 +68,23 @@ let runSatCheckVerbose (sc:satCheck) =
PF.printf "%s? → " (sotr expectation);
flush stdout;
let res = runSatCheck sc in
- (if (res = expectation)
- then PF.printf "%s\n" (cs "1;32" "Yes")
- else PF.printf "%s, cool claims it is %s\n"
- (cs "1;31" "No")
- (sotr res));
+ if (res = expectation) then
+ PF.printf "%s\n" (cs "1;32" "Yes")
+ else
+ PF.printf "%s, cool claims it is %s\n" (cs "1;31" "No") (sotr res);
flush stdout;
res
+let reportFailed (failed : (satCheck*testResult) list) =
+ if failed <> [] then begin
+ Printf.printf "=> Failed tests:\n";
+ let printTest ((_,_,title),res) =
+ let res_string = terminal_string_of_testResult res in
+ Printf.printf " not %s: %s\n" res_string title
+ in
+ List.iter printTest failed;
+ Printf.printf "\n"
+ end;
(* vim: set et sw=2 sts=2 ts=8 : *)
diff --git a/src/testsuite/Testsuite.mli b/src/testsuite/Testsuite.mli
index f2e31ca0228e731f0c75b4da093253dbbdc32abf..a85adb403098d923f63fcde962ec42e9d1c269c1 100644
--- a/src/testsuite/Testsuite.mli
+++ b/src/testsuite/Testsuite.mli
@@ -15,5 +15,8 @@ type satCheck = testResult * (CoAlgMisc.sortTable) * string
val runSatCheck : satCheck -> testResult
val runSatCheckVerbose : satCheck -> testResult
+(** Print a summary for failed testcases.
+ * @param failedTests a list of failed testcases *)
+val reportFailed : (satCheck * testResult) list -> unit
(* vim: set et sw=2 sts=2 ts=8 : *)
diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml
index 129471f7297cf5fba4042d46041b9f4d2729c0c1..fc089600f3ab07311094930aa88ccd1f35bfc54e 100644
--- a/src/testsuite/cool-testsuite.ml
+++ b/src/testsuite/cool-testsuite.ml
@@ -49,6 +49,18 @@ let k_testcases: satCheck list =
; 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)))"
+ (* This is not aconjunctive and should be answered wrongly by the algorithm
+ * for aconjunctive formulas *)
+ ; c Unsat "µ x. ( [](~p | x) & <>(p | x) )"
+ ]
let nominal_testcases =
let c a b = (a,k,b) in
@@ -148,13 +160,14 @@ let testcases ~(slow:bool) =
; 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
+ let failed = ref [] in
foreach_l (testcases slow) (fun (name,init_globals,table) ->
Printf.printf "==== Testing %s ====\n" name;
(*
@@ -173,16 +186,18 @@ let doTests ~(slow:bool) =
(* compare the expected and the actual result *)
if actual = expected
then success := !success + 1
- else failed := !failed + 1
+ else failed := (sc,actual) :: !failed
end
);
print_endline ""
);
let s n = if n = 1 then "testcase" else "testcases" in
+ reportFailed !failed;
Printf.printf "=> %d %s succeeded, %d %s failed, %d skipped.\n"
!success (s !success)
- !failed (s !failed)
- !skipped
+ (List.length !failed) (s (List.length !failed))
+ !skipped;
+ if !failed = [] then exit 0 else exit 1
let printUsage name =
diff --git a/src/unit-tests/CoAlgFormula_tests.ml b/src/unit-tests/CoAlgFormula_tests.ml
new file mode 100644
index 0000000000000000000000000000000000000000..b87e81625726c478ce580d9a078e0ad2b71c4a13
--- /dev/null
+++ b/src/unit-tests/CoAlgFormula_tests.ml
@@ -0,0 +1,14 @@
+open OUnit2
+open CoAlgFormula
+
+let isMuAconjunctive_test _ =
+ let with_formula str action = action (importFormula str) str in
+
+ with_formula "ν x. ν y. ([r] x & <r> y)" (fun f f_str ->
+ assert_bool f_str (isMuAconjunctive f));
+ with_formula "μ x. μ y. ([r] x & <r> y)" (fun f f_str ->
+ assert_bool f_str (not (isMuAconjunctive f)))
+
+let tests = "CoAlgFormula" >: ("isMuAconjunctive" >:: isMuAconjunctive_test)
+
+(* vim: set et sw=2 sts=2 ts=8 : *)
diff --git a/src/unit-tests/CoAlgFormula_tests.mli b/src/unit-tests/CoAlgFormula_tests.mli
new file mode 100644
index 0000000000000000000000000000000000000000..ac3e6e6da69f9f977785c220e30ef4bf3a11e645
--- /dev/null
+++ b/src/unit-tests/CoAlgFormula_tests.mli
@@ -0,0 +1,3 @@
+val tests : OUnit2.test
+
+(* vim: set et sw=2 sts=2 ts=8 : *)
diff --git a/src/unit-tests/CoolUtils_tests.ml b/src/unit-tests/CoolUtils_tests.ml
new file mode 100644
index 0000000000000000000000000000000000000000..3266675602423114a8f4edf18de599a3774946c7
--- /dev/null
+++ b/src/unit-tests/CoolUtils_tests.ml
@@ -0,0 +1,79 @@
+open OUnit2
+
+let string_of_list (printer: 'a -> string) (lst: 'a list) : string =
+ "[" ^ (String.concat ";" (List.map printer lst)) ^ "]"
+
+module TList_tests : (sig val tests : test end) = struct
+ open CoolUtils.TList
+
+ let combinations_test _ =
+ let list_printer = string_of_list (string_of_list string_of_int) in
+ assert_equal ~msg:"empty list" ~printer:list_printer [] (combinations []);
+ assert_equal ~msg:"two elements" ~printer:list_printer
+ [[1;2]] (combinations [[1]; [2]]);
+ assert_equal ~msg:"two lists" ~printer:list_printer
+ [[1;3]; [1;4]; [2;3]; [2;4]] (combinations [[1;2]; [3;4]])
+
+ let tests = "TList" >: ("combinations" >:: combinations_test)
+end
+
+module Args_tests : (sig val tests : test end) = struct
+ open CoolUtils.Args
+
+ type opt = { verbose : bool; file : string option }
+
+ let def_opts = { verbose = false; file = None }
+
+ let options =
+ [ { long = "verbose"
+ ; short = Some 'v'
+ ; description = "Print verbose ouput"
+ ; argument = No_arg (fun o -> { o with verbose = true })
+ }
+ ; { long = "file"
+ ; short = None
+ ; description = "File to load"
+ ; argument = Required_arg ("FILE", fun s o -> { o with file = Some s })
+ }
+ ]
+
+ let print_opts { verbose; file } = match file with
+ | None -> Printf.sprintf "{ verbose = \"%B\"; file = None}" verbose
+ | Some f -> Printf.sprintf "{ verbose = \"%B\"; file = Some \"%s\"}" verbose f
+
+ let parse_test _ =
+ let print_maybe = function
+ | Error e -> "Error \"" ^ e ^ "\""
+ | Ok x -> "Ok " ^ print_opts x
+ in
+ let cmp_maybe a b = match (a, b) with
+ | Error _, Error _ -> true
+ | Ok x, Ok y -> x = y
+ | _ -> false
+ in
+ let assert_parse argv res =
+ assert_equal ~msg:(string_of_list (fun x -> x) argv)
+ ~printer:print_maybe
+ ~cmp:cmp_maybe
+ res (parse (Array.of_list argv) 0 options def_opts)
+ in
+
+ assert_parse ["--verbose"] (Ok { verbose = true; file = None });
+ assert_parse ["-v"] (Ok { verbose = true; file = None });
+ assert_parse [] (Ok { verbose = false; file = None });
+ assert_parse ["--file"; "foo"] (Ok { verbose = false; file = Some "foo" });
+ assert_parse ["--verbose"; "--file"; "foo"]
+ (Ok { verbose = true; file = Some "foo" });
+ assert_parse ["--file"; "foo"; "--verbose"]
+ (Ok { verbose = true; file = Some "foo" });
+
+ assert_parse ["--verbuse"] (Error "");
+ assert_parse ["--file"] (Error "");
+ assert_parse ["file"] (Error "")
+
+ let tests = "Args" >: ("parse" >:: parse_test)
+end
+
+let tests = "CoolUtils" >::: [TList_tests.tests; Args_tests.tests]
+
+(* vim: set et sw=2 sts=2 ts=8 : *)
diff --git a/src/unit-tests/CoolUtils_tests.mli b/src/unit-tests/CoolUtils_tests.mli
new file mode 100644
index 0000000000000000000000000000000000000000..ac3e6e6da69f9f977785c220e30ef4bf3a11e645
--- /dev/null
+++ b/src/unit-tests/CoolUtils_tests.mli
@@ -0,0 +1,3 @@
+val tests : OUnit2.test
+
+(* vim: set et sw=2 sts=2 ts=8 : *)
diff --git a/src/unit-tests/cool_unit_tests.ml b/src/unit-tests/cool_unit_tests.ml
new file mode 100644
index 0000000000000000000000000000000000000000..65954fb02793073bee8fd49dda3dfa3b725462c8
--- /dev/null
+++ b/src/unit-tests/cool_unit_tests.ml
@@ -0,0 +1,10 @@
+open OUnit2
+
+let tests =
+ [ CoolUtils_tests.tests
+ ; CoAlgFormula_tests.tests
+ ]
+
+let () = run_test_tt_main (test_list tests)
+
+(* vim: set et sw=2 sts=2 ts=8 : *)