diff --git a/_oasis b/_oasis
index 044ad498ed1c6fea4a182af54b90b6c0c864d69c..707258ad5d3999092020f6af8b711e11b5852a64 100644
--- a/_oasis
+++ b/_oasis
@@ -100,7 +100,7 @@ Executable coalg
ByteOpt: -cc g++
CCOpt: -std=c++98 -x c++
if flag(static)
- CCLib: -static
+ CCLib: -static -ltinfo -lgpm -lz -ldl -lltdl
Executable "cool-owl"
CompiledObject: native
@@ -160,7 +160,7 @@ Executable debugger
ByteOpt: -cc g++
CCOpt: -std=c++98 -x c++
if flag(static)
- CCLib: -static
+ CCLib: -static -lz -ldl -lltdl
diff --git a/randmu.py b/randmu.py
new file mode 100755
index 0000000000000000000000000000000000000000..2c52877ddcb6fb8750290211d219abf20ee83eab
--- /dev/null
+++ b/randmu.py
@@ -0,0 +1,610 @@
+#!/usr/bin/python3
+#
+# Ideal:
+
+# Start with a single variable. While formula is still below the
+# target size, replace a random variable by a random
+# connective. once the target size has been reached, replace all
+# unguarded variables by propositional atoms. Replace all remaining
+# variables by either an allowed fixpoint variable or a
+# propositional atom
+
+import random
+import string
+import argparse
+import os
+
+
+variables = []
+syntax = 'cool'
+
+
+def _gensym():
+ i = 0
+ while True:
+ i = i + 1
+ yield "G%d" % i
+
+
+gensym = iter(_gensym())
+
+
+
+class Connective:
+ pass
+
+
+
+class Propositional(Connective):
+ pass
+
+
+
+class And(Propositional):
+ def __init__(self):
+ self._left = Variable(self)
+ self._right = Variable(self)
+
+
+ def __str__(self):
+ left = str(self._left)
+ right = str(self._right)
+ if syntax == 'tatl':
+ return "((%s) /\ (%s))" % (left, right)
+ else:
+ return "((%s) & (%s))" % (left, right)
+
+
+ def replace(self, what, withw):
+ if what == self._left:
+ self._left = withw
+ else:
+ assert self._right == what
+ self._right = withw
+
+
+ def finalize(self, atoms, guarded, unguarded, fixpoint):
+ self._left.finalize(atoms, guarded, unguarded, fixpoint)
+ self._right.finalize(atoms, guarded, unguarded, fixpoint)
+
+
+
+class Or(Propositional):
+ def __init__(self):
+ self._left = Variable(self)
+ self._right = Variable(self)
+
+
+ def __str__(self):
+ left = str(self._left)
+ right = str(self._right)
+ if syntax == 'tatl':
+ return "((%s) \/ (%s))" % (left, right)
+ else:
+ return "((%s) | (%s))" % (left, right)
+
+
+ def replace(self, what, withw):
+ if what == self._left:
+ self._left = withw
+ else:
+ assert self._right == what
+ self._right = withw
+
+
+ def finalize(self, atoms, guarded, unguarded, fixpoint):
+ self._left.finalize(atoms, guarded, unguarded, fixpoint)
+ self._right.finalize(atoms, guarded, unguarded, fixpoint)
+
+
+
+class Modal(Connective):
+ pass
+
+
+class Box(Modal):
+ def __init__(self):
+ self._subformula = Variable(self)
+
+
+ def __str__(self):
+ subformula = str(self._subformula)
+ if syntax == 'ctl':
+ return "AX (%s)" % (subformula,)
+ else:
+ return "[] (%s)" % (subformula,)
+
+
+ def replace(self, what, withw):
+ assert self._subformula == what
+ self._subformula = withw
+
+
+ def finalize(self, atoms, guarded, unguarded, fixpoint):
+ self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
+
+
+
+class Diamond(Modal):
+ def __init__(self):
+ self._subformula = Variable(self)
+
+
+ def __str__(self):
+ subformula = str(self._subformula)
+ if syntax == 'ctl':
+ return "EX (%s)" % (subformula,)
+ else:
+ return "<> (%s)" % (subformula,)
+
+
+ def replace(self, what, withw):
+ assert self._subformula == what
+ self._subformula = withw
+
+
+ def finalize(self, atoms, guarded, unguarded, fixpoint):
+ self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
+
+
+
+class Fixpoint(Connective):
+ pass
+
+class Mu(Fixpoint):
+ def __init__(self):
+ self._subformula = Variable(self)
+ self._var = next(gensym)
+
+
+ def __str__(self):
+ subformula = str(self._subformula)
+ if syntax == 'cool':
+ return "(μ %s . (%s))" % (self._var, subformula)
+ else:
+ return "(mu %s . (%s))" % (self._var, subformula)
+
+
+ def replace(self, what, withw):
+ assert self._subformula == what
+ self._subformula = withw
+
+
+ def finalize(self, atoms, guarded, unguarded, fixpoint):
+ if fixpoint == 'nu':
+ guarded = []
+ unguarded = []
+
+ self._subformula.finalize(atoms, guarded, unguarded + [self._var], 'mu')
+
+
+
+class Nu(Fixpoint):
+ def __init__(self):
+ self._subformula = Variable(self)
+ self._var = next(gensym)
+
+
+ def __str__(self):
+ subformula = str(self._subformula)
+ if syntax == 'cool':
+ return "(ν %s . (%s))" % (self._var, subformula)
+ else:
+ return "(nu %s . (%s))" % (self._var, subformula)
+
+
+ def replace(self, what, withw):
+ assert self._subformula == what
+ self._subformula = withw
+
+
+ def finalize(self, atoms, guarded, unguarded, fixpoint):
+ if fixpoint == 'mu':
+ guarded = []
+ unguarded = []
+
+ self._subformula.finalize(atoms, guarded, unguarded + [self._var], 'nu')
+
+
+
+class CTL(Connective):
+ pass
+
+
+
+class AG(CTL):
+ def __init__(self):
+ self._subformula = Variable(self)
+
+
+ def __str__(self):
+ subformula = str(self._subformula)
+ return "AG (%s)" % (subformula,)
+
+
+ def replace(self, what, withw):
+ assert self._subformula == what
+ self._subformula = withw
+
+
+ def finalize(self, atoms, guarded, unguarded, fixpoint):
+ self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
+
+
+
+class AF(CTL):
+ def __init__(self):
+ self._subformula = Variable(self)
+
+
+ def __str__(self):
+ subformula = str(self._subformula)
+ return "AF (%s)" % (subformula,)
+
+
+ def replace(self, what, withw):
+ assert self._subformula == what
+ self._subformula = withw
+
+
+ def finalize(self, atoms, guarded, unguarded, fixpoint):
+ self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
+
+
+
+class EG(CTL):
+ def __init__(self):
+ self._subformula = Variable(self)
+
+
+ def __str__(self):
+ subformula = str(self._subformula)
+ return "EG (%s)" % (subformula,)
+
+
+ def replace(self, what, withw):
+ assert self._subformula == what
+ self._subformula = withw
+
+
+ def finalize(self, atoms, guarded, unguarded, fixpoint):
+ self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
+
+
+
+class EF(CTL):
+ def __init__(self):
+ self._subformula = Variable(self)
+
+
+ def __str__(self):
+ subformula = str(self._subformula)
+ return "EF (%s)" % (subformula,)
+
+
+ def replace(self, what, withw):
+ assert self._subformula == what
+ self._subformula = withw
+
+
+ def finalize(self, atoms, guarded, unguarded, fixpoint):
+ self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
+
+
+
+class AU(CTL):
+ def __init__(self):
+ self._left = Variable(self)
+ self._right = Variable(self)
+
+
+ def __str__(self):
+ left = str(self._left)
+ right = str(self._right)
+ return "A((%s) U (%s))" % (left, right)
+
+
+ def replace(self, what, withw):
+ if what == self._left:
+ self._left = withw
+ else:
+ assert self._right == what
+ self._right = withw
+
+
+ def finalize(self, atoms, guarded, unguarded, fixpoint):
+ self._left.finalize(atoms, guarded, unguarded, fixpoint)
+ self._right.finalize(atoms, guarded, unguarded, fixpoint)
+
+
+
+class AR(CTL):
+ def __init__(self):
+ self._left = Variable(self)
+ self._right = Variable(self)
+
+
+ def __str__(self):
+ left = str(self._left)
+ right = str(self._right)
+ return "A((%s) R (%s))" % (left, right)
+
+
+ def replace(self, what, withw):
+ if what == self._left:
+ self._left = withw
+ else:
+ assert self._right == what
+ self._right = withw
+
+
+ def finalize(self, atoms, guarded, unguarded, fixpoint):
+ self._left.finalize(atoms, guarded, unguarded, fixpoint)
+ self._right.finalize(atoms, guarded, unguarded, fixpoint)
+
+
+
+class EU(CTL):
+ def __init__(self):
+ self._left = Variable(self)
+ self._right = Variable(self)
+
+
+ def __str__(self):
+ left = str(self._left)
+ right = str(self._right)
+ return "E((%s) U (%s))" % (left, right)
+
+
+ def replace(self, what, withw):
+ if what == self._left:
+ self._left = withw
+ else:
+ assert self._right == what
+ self._right = withw
+
+
+ def finalize(self, atoms, guarded, unguarded, fixpoint):
+ self._left.finalize(atoms, guarded, unguarded, fixpoint)
+ self._right.finalize(atoms, guarded, unguarded, fixpoint)
+
+
+
+class ER(CTL):
+ def __init__(self):
+ self._left = Variable(self)
+ self._right = Variable(self)
+
+
+ def __str__(self):
+ left = str(self._left)
+ right = str(self._right)
+ return "E((%s) R (%s))" % (left, right)
+
+
+ def replace(self, what, withw):
+ if what == self._left:
+ self._left = withw
+ else:
+ assert self._right == what
+ self._right = withw
+
+
+ def finalize(self, atoms, guarded, unguarded, fixpoint):
+ self._left.finalize(atoms, guarded, unguarded, fixpoint)
+ self._right.finalize(atoms, guarded, unguarded, fixpoint)
+
+
+
+class ATL:
+ def coalition(self):
+ if not hasattr(self, '_coalition'):
+ self._coalition = []
+ while len(self._coalition) == 0:
+ self._coalition = []
+ for i in range(1, 6):
+ if random.getrandbits(1) == 1:
+ self._coalition.append(str(i))
+
+ if syntax == 'tatl':
+ return ",".join(self._coalition)
+ else:
+ return " ".join(self._coalition)
+
+
+
+class Next(ATL):
+ def __init__(self):
+ self._subformula = Variable(self)
+
+
+ def __str__(self):
+ subformula = str(self._subformula)
+ if syntax == 'tatl':
+ return "<<%s>>X(%s)" % (self.coalition(), subformula,)
+ else:
+ return "[{%s}](%s)" % (self.coalition(), subformula,)
+
+
+ def replace(self, what, withw):
+ assert self._subformula == what
+ self._subformula = withw
+
+
+ def finalize(self, atoms, guarded, unguarded, fixpoint):
+ self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
+
+
+
+class Always(ATL):
+ def __init__(self):
+ self._subformula = Variable(self)
+
+
+ def __str__(self):
+ subformula = str(self._subformula)
+ if syntax == 'tatl':
+ return "<<%s>>G(%s)" % (self.coalition(), subformula,)
+ else:
+ return "(ν X . ((%s) & [{%s}]X))" % (subformula,self.coalition())
+
+
+ def replace(self, what, withw):
+ assert self._subformula == what
+ self._subformula = withw
+
+
+ def finalize(self, atoms, guarded, unguarded, fixpoint):
+ self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
+
+
+
+class Eventually(ATL):
+ def __init__(self):
+ self._subformula = Variable(self)
+
+
+ def __str__(self):
+ subformula = str(self._subformula)
+ if syntax == 'tatl':
+ return "<<%s>>F(%s)" % (self.coalition(), subformula,)
+ else:
+ return "(μ X . ((%s) | [{%s}]X))" % (subformula, self.coalition())
+
+
+ def replace(self, what, withw):
+ assert self._subformula == what
+ self._subformula = withw
+
+
+ def finalize(self, atoms, guarded, unguarded, fixpoint):
+ self._subformula.finalize(atoms, guarded + unguarded, [], fixpoint)
+
+
+
+class Until(ATL):
+ def __init__(self):
+ self._left = Variable(self)
+ self._right = Variable(self)
+
+
+ def __str__(self):
+ left = str(self._left)
+ right = str(self._right)
+ if syntax == 'tatl':
+ return "<<%s>>((%s) U (%s))" % (self.coalition(),left, right)
+ else:
+ return "(μ X . ((%s) | ((%s) & [{%s}]X)))" % (right,left,self.coalition())
+
+
+ def replace(self, what, withw):
+ if what == self._left:
+ self._left = withw
+ else:
+ assert self._right == what
+ self._right = withw
+
+
+ def finalize(self, atoms, guarded, unguarded, fixpoint):
+ self._left.finalize(atoms, guarded, unguarded, fixpoint)
+ self._right.finalize(atoms, guarded, unguarded, fixpoint)
+
+
+
+connectives = []
+
+
+class Variable:
+ def __init__(self, parent):
+ self._parent = parent
+ variables.append(self)
+
+
+ def __str__(self):
+ return "(undecided)"
+
+
+ def replace(self):
+ assert self._parent != None
+ replacement = random.choice(connectives)()
+ variables.remove(self)
+ self._parent.replace(self, replacement)
+
+
+ def finalize(self, atoms, guarded, unguarded, fixpoint):
+ choice = random.choice(guarded + atoms)
+ if choice in atoms:
+ choice = random.choice([choice, "~%s" % choice])
+
+ variables.remove(self)
+ self._parent.replace(self, choice)
+
+
+
+def main(args):
+ global connectives
+ if args.logic == 'afmu':
+ connectives = [And, And, Or, Or, Box, Diamond, Mu, Nu]
+ os.makedirs(os.path.join(args.destdir, 'cool'))
+ os.makedirs(os.path.join(args.destdir, 'mlsolver'))
+
+ elif args.logic == 'CTL':
+ connectives = [And, And, Or, Or, Box, Diamond, AF, AG, EF, EG, AU, EU]
+ os.makedirs(os.path.join(args.destdir, 'ctl'))
+
+ elif args.logic == 'ATL':
+ connectives = [And, And, Or, Or, Next, Always, Eventually, Until]
+ os.makedirs(os.path.join(args.destdir, 'cool'))
+ os.makedirs(os.path.join(args.destdir, 'tatl'))
+
+ for i in range(0, args.count):
+ global variables
+ global syntax
+ variables = []
+ formula = random.choice(connectives)()
+
+ for _ in range(0, args.constructors):
+ random.choice(variables).replace()
+
+ formula.finalize(list(string.ascii_lowercase[:args.atoms]), [], [], 'none')
+
+ if args.logic == 'afmu':
+ with open(os.path.join(args.destdir, 'cool', 'random.%04d.cool' % i), 'w') as f:
+ syntax = 'cool'
+ f.write(str(formula))
+
+ with open(os.path.join(args.destdir, 'mlsolver', 'random.%04d.mlsolver' % i), 'w') as f:
+ syntax = 'mlsolver'
+ f.write(str(formula))
+
+ elif args.logic == 'CTL':
+ with open(os.path.join(args.destdir, 'ctl', 'random.%04d.ctl' % i), 'w') as f:
+ syntax = 'ctl'
+ f.write(str(formula))
+
+ elif args.logic == 'ATL':
+ with open(os.path.join(args.destdir, 'cool', 'random.%04d.cool' % i), 'w') as f:
+ syntax = 'cool'
+ f.write(str(formula))
+
+ with open(os.path.join(args.destdir, 'tatl', 'random.%04d.tatl' % i), 'w') as f:
+ syntax = 'tatl'
+ f.write(str(formula))
+
+ print(args.destdir)
+
+if __name__ == '__main__':
+ parser = argparse.ArgumentParser(description="Generator for random μ-Calculus-Formulas")
+ parser.add_argument('--atoms', type=int, required=True,
+ help="Number of propositional arguments to use")
+ parser.add_argument('--constructors', type=int, required=True,
+ help="Number of connectives to build")
+ parser.add_argument('--count', type=int, required=True,
+ help="Number of formulas to generate")
+ parser.add_argument('--destdir', type=str, required=True,
+ help="Directory to place created formulas in")
+ parser.add_argument('--logic', choices=['CTL', 'ATL', 'afmu'], required=True)
+
+ args = parser.parse_args()
+
+ main(args)
diff --git a/src/.dir-locals.el b/src/.dir-locals.el
new file mode 100644
index 0000000000000000000000000000000000000000..aeb20dbe97f42350ecc56c745477924220bb7c70
--- /dev/null
+++ b/src/.dir-locals.el
@@ -0,0 +1,2 @@
+((nil
+ (indent-tabs-mode . nil)))
diff --git a/src/coalg/coalg.ml b/src/coalg/coalg.ml
index c270e63ab61f9072306f6e8f2f12b89be823d375..30f4ec3a0d94466609ec0b2834704f752422fae0 100644
--- a/src/coalg/coalg.ml
+++ b/src/coalg/coalg.ml
@@ -46,9 +46,10 @@ let _ =
let printUsage () =
print_endline "Usage: \"alc <task> <functor> [<flags>]\" where";
- print_endline " <task> in { sat print nnf prov (is »not.(sat ¬f)«) }";
+ print_endline " <task> in { sat print verify nnf prov (is »not.(sat ¬f)«) }";
print_endline " <functor> in { MultiModalK (or equivalently K)";
print_endline " MultiModalKD (or equivalently KD)";
+ print_endline " Monotone";
print_endline " CoalitionLogic (or equivalently CL)";
print_endline " Const id1 ... idn (or equivalently Constant id1 ... idn)";
print_endline " Id (or equivalently Identity)";
@@ -167,6 +168,28 @@ let choiceNNF () =
done
with End_of_file -> ()
+let choiceGraph () =
+ choiceSat ();
+ print_endline "digraph reasonerstate {";
+ CM.graphIterCores (fun core -> print_endline (CM.coreToDot core));
+ CM.graphIterStates (fun state -> print_endline (CM.stateToDot state));
+ print_endline "}"
+
+let choiceVerify () =
+ try
+ while true do
+ let input = read_line () in
+ if not (GenAndComp.isEmptyString input) then
+ let f = CoAlgFormula.importFormula input in
+ let str = CoAlgFormula.exportFormula f in
+ incr counter;
+ print_string ("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
+ flush stdout;
+ CoAlgFormula.verifyFormula f;
+ else ()
+ done
+ with End_of_file -> ()
+
let rec parseFlags arr offs : unit =
let offs = ref (offs) in
let getParam () =
@@ -198,6 +221,6 @@ let _ =
| "prov" -> choiceProvable ()
| "print" -> choicePrint ()
| "nnf" -> choiceNNF ()
+ | "verify" -> choiceVerify ()
+ | "graph" -> choiceGraph ()
| _ -> printUsage ()
-
-
diff --git a/src/debugger/debugger.ml b/src/debugger/debugger.ml
index e685a5989f0cdaaffb082dba4e9ae259c6f5794e..8e631d43dd6c5776f81789c20dd3a1c12cae764f 100644
--- a/src/debugger/debugger.ml
+++ b/src/debugger/debugger.ml
@@ -69,6 +69,12 @@ let listCores args =
let listStates args =
CM.graphIterStates (fun state -> print_endline (CM.stateToString state))
+let exportGraph args =
+ print_endline "digraph reasonerstate {";
+ CM.graphIterCores (fun core -> print_endline (CM.coreToDot core));
+ CM.graphIterStates (fun state -> print_endline (CM.stateToDot state));
+ print_endline "}"
+
let showNode = function
| (n::_) ->
let n = int_of_string n in
@@ -101,11 +107,10 @@ let _ =
Repl.bind "status" (fun _ -> printStatus ()) "Prints reasoning status" "";
Repl.bind "lscores" listCores "Lists all cores" "";
Repl.bind "lsstates" listStates "Lists all states" "";
+ Repl.bind "graphviz" exportGraph "Graphviz source of reasoner state" "";
Repl.bind "node" showNode "shows details of a node" "usage: node n";
Repl.exitBinding
];
}
in
Repl.start session
-
-
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 371895edc5dcd334811544fdd3117a0cd9a5b8c0..dcc1856aff5bb0cf56a3d25744fec5ba666f0846 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -12,7 +12,7 @@ module Str = String
(** A general exception for all kinds of errors
that can happen in the tableau procedure.
- More specific information is given in the argument.
+ More specific information is given in the argument.
*)
exception CoAlgException of string
@@ -48,7 +48,7 @@ type formula =
| MORETHAN of int * string * formula (* diamond of GML *)
| MAXEXCEPT of int * string * formula (* box of GML *)
| ATLEASTPROB of rational * formula (* = {>= 0.5} C ---> C occurs with *)
- (* probability of at least 50% *)
+ (* probability of at least 50% *)
| LESSPROBFAIL of rational * formula (* = [1/2] C = {< 1/2} ¬ C ---> C fails with *)
(* probability of less than 50% *)
| CONST of string (* constant functor with value string *)
@@ -58,6 +58,19 @@ type formula =
| NORMN of formula * formula (* \neg NORM (\neg A, \neg B) *)
| CHC of formula * formula (* Choice is self-dual *)
| FUS of bool * formula
+ | MU of string * formula
+ | NU of string * formula
+ | VAR of string
+ | AF of formula
+ | EF of formula
+ | AG of formula
+ | EG of formula
+ | AU of formula * formula
+ | EU of formula * formula
+ | AR of formula * formula
+ | ER of formula * formula
+ | AB of formula * formula
+ | EB of formula * formula
exception ConversionException of formula
@@ -80,14 +93,14 @@ let isNominal s = String.contains s '\''
*)
let rec sizeFormula f =
match f with
- | TRUE
- | FALSE
+ | TRUE
+ | FALSE
| AP _ -> 1
| NOT f1
| AT (_, f1) -> succ (sizeFormula f1)
- | OR (f1, f2)
+ | OR (f1, f2)
| AND (f1, f2)
- | EQU (f1, f2)
+ | EQU (f1, f2)
| IMP (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
| EX (_, f1)
| AX (_, f1)
@@ -106,6 +119,15 @@ let rec sizeFormula f =
| CONSTN _ -> 1
| CHC (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
| FUS (_, f1) -> succ (sizeFormula f1)
+ | MU (_, f1)
+ | NU (_, f1) -> succ (succ (sizeFormula f1))
+ | VAR _ -> 1
+ | AF _ | EF _
+ | AG _ | EG _
+ | AU _ | EU _
+ | AR _ | ER _
+ | AB _ | EB _ ->
+ raise (CoAlgException ("sizeFormula: CTL should have been removed at this point"))
(** Determines the size of a sorted formula.
@param f A sorted formula.
@@ -120,7 +142,7 @@ let rec iter func formula =
func formula;
let proc = iter func in (* proc = "process" *)
match formula with
- | TRUE | FALSE | AP _ -> ()
+ | TRUE | FALSE | AP _ | VAR _ -> ()
| CONST _
| CONSTN _ -> ()
| NOT a | AT (_,a)
@@ -135,38 +157,56 @@ let rec iter func formula =
| NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
| CHC (a,b) -> (proc a ; proc b)
| FUS (_,a) -> proc a
+ | MU (_, f) | NU (_, f) -> proc f
+ | AF f | EF f | AG f | EG f -> proc f
+ | AU (f1, f2) | EU (f1, f2)
+ | AR (f1, f2) | ER (f1, f2)
+ | AB (f1, f2) | EB (f1, f2) -> (proc f1; proc f2)
let rec convert_post func formula = (* run over all subformulas in post order *)
let c = convert_post func in (* some shorthand *)
(* replace parts of the formula *)
let formula = (match formula with
- (* 0-ary constructors *)
- | TRUE | FALSE | AP _ -> formula
- | CONST _
- | CONSTN _ -> formula
- (* unary *)
- | NOT a -> NOT (c a)
- | AT (s,a) -> AT (s,c a)
- (* binary *)
- | OR (a,b) -> OR (c a, c b)
- | AND (a,b) -> AND (c a, c b)
- | EQU (a,b) -> EQU (c a, c b)
- | IMP (a,b) -> IMP (c a, c b)
- | EX (s,a) -> EX (s,c a)
- | AX (s,a) -> AX (s,c a)
- | ENFORCES (s,a) -> ENFORCES (s,c a)
- | ALLOWS (s,a) -> ALLOWS (s,c a)
- | MIN (n,s,a) -> MIN (n,s,c a)
- | MAX (n,s,a) -> MAX (n,s,c a)
- | ATLEASTPROB (p,a) -> ATLEASTPROB (p, c a)
- | LESSPROBFAIL (p,a) -> LESSPROBFAIL (p, c a)
- | MORETHAN (n,s,a) -> MORETHAN (n,s,c a)
- | MAXEXCEPT (n,s,a) -> MAXEXCEPT (n,s,c a)
- | ID(a) -> ID (c a)
- | NORM(a, b) -> NORM(c a, c b)
- | NORMN(a, b) -> NORMN(c a, c b)
- | CHC (a,b) -> CHC (c a, c b)
- | FUS (s,a) -> FUS (s, c a)) in
+ (* 0-ary constructors *)
+ | TRUE | FALSE | AP _ | VAR _ -> formula
+ | CONST _
+ | CONSTN _ -> formula
+ (* unary *)
+ | NOT a -> NOT (c a)
+ | AT (s,a) -> AT (s,c a)
+ (* binary *)
+ | OR (a,b) -> OR (c a, c b)
+ | AND (a,b) -> AND (c a, c b)
+ | EQU (a,b) -> EQU (c a, c b)
+ | IMP (a,b) -> IMP (c a, c b)
+ | EX (s,a) -> EX (s,c a)
+ | AX (s,a) -> AX (s,c a)
+ | ENFORCES (s,a) -> ENFORCES (s,c a)
+ | ALLOWS (s,a) -> ALLOWS (s,c a)
+ | MIN (n,s,a) -> MIN (n,s,c a)
+ | MAX (n,s,a) -> MAX (n,s,c a)
+ | ATLEASTPROB (p,a) -> ATLEASTPROB (p, c a)
+ | LESSPROBFAIL (p,a) -> LESSPROBFAIL (p, c a)
+ | MORETHAN (n,s,a) -> MORETHAN (n,s,c a)
+ | MAXEXCEPT (n,s,a) -> MAXEXCEPT (n,s,c a)
+ | ID(a) -> ID (c a)
+ | NORM(a, b) -> NORM(c a, c b)
+ | NORMN(a, b) -> NORMN(c a, c b)
+ | CHC (a,b) -> CHC (c a, c b)
+ | FUS (s,a) -> FUS (s, c a)
+ | MU (n, f1) -> MU (n, c f1)
+ | NU (n, f1) -> NU (n, c f1)
+ | AF f1 -> AF (c f1)
+ | EF f1 -> EF (c f1)
+ | AG f1 -> AG (c f1)
+ | EG f1 -> EG (c f1)
+ | AU (f1, f2) -> AU (c f1, c f2)
+ | EU (f1, f2) -> EU (c f1, c f2)
+ | AR (f1, f2) -> AR (c f1, c f2)
+ | ER (f1, f2) -> ER (c f1, c f2)
+ | AB (f1, f2) -> AB (c f1, c f2)
+ | EB (f1, f2) -> EB (c f1, c f2))
+ in
func formula
let convertToK formula = (* tries to convert a formula to a pure K formula *)
@@ -200,6 +240,36 @@ let convertToGML formula = (* tries to convert a formula to a pure GML formula *
in
convert_post helper formula
+let gensym = Stream.from (fun i -> Some (Printf.sprintf "#gensym%x#" i))
+
+let convertToMu formula =
+ let name = Stream.next gensym in
+ let helper formula =
+ match formula with
+ | AF f1 ->
+ MU (name, (OR (f1, (AX ("", (VAR name))))))
+ | EF f1 ->
+ MU (name, (OR (f1, (EX ("", (VAR name))))))
+ | AG f1 ->
+ NU (name, (AND (f1, (AX ("", (VAR name))))))
+ | EG f1 ->
+ NU (name, (AND (f1, (EX ("", (VAR name))))))
+ | AU (f1, f2) ->
+ MU (name, (OR (f2, (AND (f1, (AX ("", (VAR name))))))))
+ | EU (f1, f2) ->
+ MU (name, (OR (f2, (AND (f1, (EX ("", (VAR name))))))))
+ | AR (f1, f2) ->
+ NU (name, (AND (f2, (OR (f1, (AX ("", (VAR name))))))))
+ | ER (f1, f2) ->
+ NU (name, (AND (f2, (OR (f1, (EX ("", (VAR name))))))))
+ | AB (f1, f2) ->
+ NOT (MU (name, (OR (f2, (AND ((NOT f1), (EX ("", (VAR name)))))))))
+ | EB (f1, f2) ->
+ NOT (MU (name, (OR (f2, (AND ((NOT f1), (AX ("", (VAR name)))))))))
+ | _ -> formula
+ in
+ convert_post helper formula
+
(** Appends a string representation of a formula to a string buffer.
Parentheses are ommited where possible
where the preference rules are defined as usual.
@@ -214,7 +284,7 @@ let rec exportFormula_buffer sb f =
let prio n lf =
let prionr = function
| EQU _ -> 0
- | IMP _ -> 1
+ | IMP _ -> 1
| OR _ -> 2
| AND _ -> 3
| _ -> 4
@@ -348,6 +418,67 @@ let rec exportFormula_buffer sb f =
| FUS (first, f1) ->
Buffer.add_string sb (if first then "[pi1]" else "[pi2]");
prio 4 f1
+ | MU (s, f1) ->
+ Buffer.add_string sb "μ";
+ Buffer.add_string sb s;
+ Buffer.add_string sb ".";
+ prio 4 f1
+ | NU (s, f1) ->
+ Buffer.add_string sb "ν";
+ Buffer.add_string sb s;
+ Buffer.add_string sb ".";
+ prio 4 f1
+ | VAR s ->
+ Buffer.add_string sb s
+ | AF f1 ->
+ Buffer.add_string sb "AF ";
+ prio 4 f1
+ | EF f1 ->
+ Buffer.add_string sb "EF ";
+ prio 4 f1
+ | AG f1 ->
+ Buffer.add_string sb "AG ";
+ prio 4 f1
+ | EG f1 ->
+ Buffer.add_string sb "EG ";
+ prio 4 f1
+ | AU (f1, f2) ->
+ Buffer.add_string sb "A (";
+ prio 4 f1;
+ Buffer.add_string sb " U ";
+ prio 4 f2;
+ Buffer.add_string sb ")"
+ | EU (f1, f2) ->
+ Buffer.add_string sb "E (";
+ prio 4 f1;
+ Buffer.add_string sb " U ";
+ prio 4 f2;
+ Buffer.add_string sb ")"
+ | AR (f1, f2) ->
+ Buffer.add_string sb "A (";
+ prio 4 f1;
+ Buffer.add_string sb " R ";
+ prio 4 f2;
+ Buffer.add_string sb ")"
+ | ER (f1, f2) ->
+ Buffer.add_string sb "E (";
+ prio 4 f1;
+ Buffer.add_string sb " R ";
+ prio 4 f2;
+ Buffer.add_string sb ")"
+ | AB (f1, f2) ->
+ Buffer.add_string sb "A (";
+ prio 4 f1;
+ Buffer.add_string sb " B ";
+ prio 4 f2;
+ Buffer.add_string sb ")"
+ | EB (f1, f2) ->
+ Buffer.add_string sb "E (";
+ prio 4 f1;
+ Buffer.add_string sb " B ";
+ prio 4 f2;
+ Buffer.add_string sb ")"
+
(** Converts a formula into a string representation.
Parentheses are ommited where possible
@@ -367,7 +498,7 @@ let rec exportTatlFormula_buffer sb f =
let prio n lf =
let prionr = function
| EQU _ -> 0
- | IMP _ -> 1
+ | IMP _ -> 1
| OR _ -> 2
| AND _ -> 3
| _ -> 4
@@ -433,7 +564,20 @@ let rec exportTatlFormula_buffer sb f =
| ID _
| NORM _
| NORMN _
- | FUS _ -> raise (CoAlgException ("export to tatl: Not connectives of CL"))
+ | FUS _
+ | MU _
+ | NU _
+ | VAR _
+ | AF _
+ | EF _
+ | AG _
+ | EG _
+ | AU _
+ | EU _
+ | AR _
+ | ER _
+ | AB _
+ | EB _ -> raise (CoAlgException ("export to tatl: Not connectives of CL"))
let exportTatlFormula f =
let sb = Buffer.create 128 in
@@ -505,26 +649,166 @@ let exportQueryParsable tbox (_,f) =
(* NB: True and False are the propositional constants. Lower case
true/false are regardes as atomic propositions and we emit a warning
*)
-let lexer = A.make_lexer
+let lexer = A.make_lexer
[":";";";"|-";"(";")";"=>";"<=>";"|";"&";"~";"@";"True";"False";"true";"false";"<";">";"[";"]";"{<=";"{>=";"}";"+";"[pi1]";"[pi2]"
- ;"[{";"}]";"<{";"}>";",";"/";"{<";"=";"=o";"O"
- ]
+ ;"[{";"}]";"<{";"}>";",";"/";"{<";"=";"=o";"O"
+ ;"μ";"ν";"."
+ ;"AX";"EX";"AF";"EF";"AG";"EG";"A";"E";"U";"R";"B"
+ ]
let mk_exn s = CoAlgException s
+(** Process from inside out. cons all variables seen, remove them when
+ binding fixpoint is found. Fixpoint type may only change if last
+ (inner) fixpoint didn't include any free variables.
+ *)
+let rec verifyMuAltFree formula =
+ let proc = verifyMuAltFree in
+ match formula with
+ | TRUE | FALSE | AP _ -> ("none", [])
+ | CONST _
+ | CONSTN _ -> ("none", [])
+ | AT (_,a) | NOT a
+ | EX (_,a) | AX (_,a) -> proc a
+ | OR (a,b) | AND (a,b)
+ | EQU (a,b) | IMP (a,b) ->
+ let (atype, afree) = proc a
+ and (btype, bfree) = proc b in
+ if (compare atype "μ" == 0 && compare btype "ν" == 0) ||
+ (compare atype "ν" == 0 && compare btype "μ" == 0) then
+ raise (CoAlgException ("formula not alternation-free"));
+ if compare atype "none" == 0 then
+ (btype, List.flatten [afree; bfree])
+ else
+ (atype, List.flatten [afree; bfree])
+ | 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) ->
+ let (atype, afree) = proc a
+ and (btype, bfree) = proc b in
+ if (compare atype "μ" == 0 && compare btype "ν" == 0) ||
+ (compare atype "ν" == 0 && compare btype "μ" == 0) then
+ raise (CoAlgException ("formula not alternation-free"));
+ if compare atype "none" == 0 then
+ (btype, List.flatten [afree; bfree])
+ else
+ (atype, List.flatten [afree; bfree])
+ | FUS (_,a) -> proc a
+ | MU (s, f) ->
+ let (fptype, free) = proc f in
+ (if (compare fptype "ν" == 0) then
+ raise (CoAlgException ("formula not alternation-free")));
+ let predicate x = compare x s != 0 in
+ let newfree = List.filter predicate free in
+ if newfree = [] then
+ ("none", [])
+ else
+ ("μ", newfree)
+ | NU (s, f) ->
+ let (fptype, free) = proc f in
+ (if (compare fptype "μ" == 0) then
+ raise (CoAlgException ("formula not alternation-free")));
+ let predicate x = compare x s != 0 in
+ let newfree = List.filter predicate free in
+ if newfree = [] then
+ ("none", [])
+ else
+ ("ν", newfree)
+ | VAR s -> ("none", [s])
+ | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ ->
+ raise (CoAlgException ("verifyMuAltFree: CTL should have been removed at this point"))
+
+
+(** 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
+ negations is even.
+ *)
+let rec verifyMuMonotone negations formula =
+ let proc = verifyMuMonotone negations in
+ match formula with
+ | TRUE | FALSE | AP _ -> ()
+ | CONST _
+ | CONSTN _ -> ()
+ | AT (_,a)
+ | EX (_,a) | AX (_,a) -> proc a
+ | OR (a,b) | AND (a,b)
+ | EQU (a,b) | IMP (a,b) -> (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) -> (proc a; proc b)
+ | CHC (a,b) -> (proc a ; proc b)
+ | FUS (_,a) -> proc a
+ | MU (s, f)
+ | NU (s, f) ->
+ let newNeg = (s, 0) :: negations in
+ verifyMuMonotone newNeg f
+ | VAR s ->
+ let finder (x, _) = compare x s == 0 in
+ let (_, neg) = List.find finder negations in
+ if ((neg land 1) != 0) then raise (CoAlgException ("formula not monotone"))
+ | NOT a ->
+ let increment (s, n) = (s, n+1) in
+ let newNeg = List.map increment negations in
+ verifyMuMonotone newNeg a
+ | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ ->
+ raise (CoAlgException ("verifyMuMonotone: CTL should have been removed at this point"))
+
+let rec verifyMuGuarded unguarded formula =
+ let proc = verifyMuGuarded unguarded in
+ match formula with
+ | TRUE | FALSE | AP _ -> ()
+ | CONST _
+ | CONSTN _ -> ()
+ | AT (_,a) | NOT a -> proc a
+ | EX (_,a) | AX (_,a) -> verifyMuGuarded [] a
+ | OR (a,b) | AND (a,b)
+ | EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
+ | ENFORCES (_,a) | ALLOWS (_,a)
+ | MIN (_,_,a) | MAX (_,_,a)
+ | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
+ | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> verifyMuGuarded [] a
+ | ID(a) -> verifyMuGuarded [] a
+ | NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
+ | CHC (a,b) -> (proc a ; proc b)
+ | FUS (_,a) -> proc a
+ | MU (s, f)
+ | NU (s, f) ->
+ let newUnguard = s :: unguarded in
+ verifyMuGuarded newUnguard f
+ | VAR s ->
+ let finder x = compare x s == 0 in
+ if List.exists finder unguarded then
+ raise (CoAlgException ("formula not guarded"))
+ | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ ->
+ raise (CoAlgException ("verifyMuGuarded: CTL should have been removed at this point"))
+
+let verifyFormula formula =
+ verifyMuAltFree formula;
+ verifyMuMonotone [] formula;
+ verifyMuGuarded [] formula
+
(** These functions parse a token stream to obtain a formula.
It is a standard recursive descent procedure.
@param ts A token stream.
@return The resulting (sub-)formula.
@raise CoAlgException if ts does not represent a formula.
*)
-let rec parse_formula ts =
- let f1 = parse_imp ts in
+let rec parse_formula (symtab: 'a list) ts =
+ let formula = (parse_imp symtab ts) in
+ let f1 = convertToMu formula in
match Stream.peek ts with
| None -> f1
| Some (A.Kwd "<=>") ->
Stream.junk ts;
- let f2 = parse_formula ts in
+ let f2 = parse_formula symtab ts in
EQU (f1, f2)
| _ -> f1
@@ -534,13 +818,13 @@ let rec parse_formula ts =
@return The resulting (sub-)formula.
@raise CoAlgException if ts does not represent a formula.
*)
-and parse_imp ts =
- let f1 = parse_or ts in
+and parse_imp symtab ts=
+ let f1 = parse_or symtab ts in
match Stream.peek ts with
| None -> f1
| Some (A.Kwd "=>") ->
Stream.junk ts;
- let f2 = parse_imp ts in
+ let f2 = parse_imp symtab ts in
IMP (f1, f2)
| _ -> f1
@@ -550,13 +834,13 @@ and parse_imp ts =
@return The resulting (sub-)formula.
@raise CoAlgException if ts does not represent a formula.
*)
-and parse_or ts =
- let f1 = parse_and ts in
+and parse_or symtab ts =
+ let f1 = parse_and symtab ts in
match Stream.peek ts with
| None -> f1
| Some (A.Kwd "|") ->
Stream.junk ts;
- let f2 = parse_or ts in
+ let f2 = parse_or symtab ts in
OR (f1, f2)
| _ -> f1
@@ -566,13 +850,13 @@ and parse_or ts =
@return The resulting (sub-)formula.
@raise CoAlgException if ts does not represent a formula.
*)
-and parse_and ts =
- let f1 = parse_cimp ts in
+and parse_and symtab ts =
+ let f1 = parse_cimp symtab ts in
match Stream.peek ts with
| None -> f1
| Some (A.Kwd "&") ->
Stream.junk ts;
- let f2 = parse_and ts in
+ let f2 = parse_and symtab ts in
AND (f1, f2)
| _ -> f1
@@ -582,13 +866,13 @@ and parse_and ts =
@return The resulting (sub-)formula.
@raise CoAlgException if ts does not represent a formula.
*)
-and parse_cimp ts =
- let f1 = parse_rest ts in
+and parse_cimp symtab ts =
+ let f1 = parse_rest symtab ts in
match Stream.peek ts with
| None -> f1
| Some (A.Kwd "=o") ->
Stream.junk ts;
- let f2 = parse_cimp ts in
+ let f2 = parse_cimp symtab ts in
NORM (f1, f2)
| _ -> f1
@@ -598,7 +882,7 @@ and parse_cimp ts =
@return The resulting (sub-)formula.
@raise CoAlgException if ts does not represent a formula.
*)
-and parse_rest ts =
+and parse_rest symtab ts =
let boxinternals noNo es =
let n =
if noNo then 0
@@ -652,9 +936,14 @@ and parse_rest ts =
AP "false"
| A.Kwd "True" -> TRUE
| A.Kwd "False" -> FALSE
- | A.Ident s -> AP s
+ | A.Ident s ->
+ (try
+ let finder (x, _) = compare x s == 0 in
+ let (_, symbol) = List.find finder symtab in
+ VAR symbol
+ with Not_found -> AP s)
| A.Kwd "~" ->
- let f = parse_rest ts in
+ let f = parse_rest symtab ts in
NOT f
| A.Kwd "@" ->
let s =
@@ -662,39 +951,39 @@ and parse_rest ts =
| A.Ident s when isNominal s -> s
| t -> A.printError mk_exn ~t ~ts ("nominal expected: ")
in
- let f = parse_rest ts in
+ let f = parse_rest symtab ts in
AT (s, f)
- | A.Kwd "<" ->
+ | A.Kwd "<" ->
let (_, _, s) = boxinternals true ">" in
- let f1 = parse_rest ts in
- EX (s, f1)
- | A.Kwd "[" ->
+ let f1 = parse_rest symtab ts in
+ EX (s, f1)
+ | A.Kwd "[" ->
let (_, _, s) = boxinternals true "]" in
- let f1 = parse_rest ts in
+ let f1 = parse_rest symtab ts in
AX (s, f1)
- | A.Kwd "[{" ->
+ | A.Kwd "[{" ->
let ls = agentlist "}]" in
- let f1 = parse_rest ts in
+ let f1 = parse_rest symtab ts in
ENFORCES (ls, f1)
- | A.Kwd "<{" ->
+ | A.Kwd "<{" ->
let ls = agentlist "}>" in
- let f1 = parse_rest ts in
+ let f1 = parse_rest symtab ts in
ALLOWS (ls, f1)
- | A.Kwd "{>=" ->
+ | A.Kwd "{>=" ->
let (n, denom, s) = boxinternals false "}" in
- let f1 = parse_rest ts in
+ let f1 = parse_rest symtab ts in
if (denom <> 0)
then ATLEASTPROB (rational_of_int n denom, f1)
else MIN (n, s, f1)
- | A.Kwd "{<=" ->
+ | A.Kwd "{<=" ->
let (n, denom, s) = boxinternals false "}" in
- let f1 = parse_rest ts in
+ let f1 = parse_rest symtab ts in
if (denom <> 0)
then A.printError mk_exn ~ts "Can not express {<= probability}"
else MAX (n, s, f1)
- | A.Kwd "{<" ->
+ | A.Kwd "{<" ->
let (n, denom, s) = boxinternals false "}" in
- let f1 = parse_rest ts in
+ let f1 = parse_rest symtab ts in
if (denom <> 0)
then LESSPROBFAIL (rational_of_int n denom, NOT f1)
else A.printError mk_exn ~ts "The \"Less than\" < is not implemented yet"
@@ -706,11 +995,11 @@ and parse_rest ts =
| _ -> A.printError mk_exn ~ts "constant = expects an identifier afterwards"
end
| A.Kwd "(" -> begin
- let f = parse_formula ts in
+ let f = parse_formula symtab ts in
match Stream.next ts with
| A.Kwd ")" -> f
| A.Kwd "+" -> begin
- let f2 = parse_formula ts in
+ let f2 = parse_formula symtab ts in
match Stream.next ts with
| A.Kwd ")" -> CHC (f, f2)
| t -> A.printError mk_exn ~t ~ts "\")\" expected: "
@@ -718,25 +1007,91 @@ and parse_rest ts =
| t -> A.printError mk_exn ~t ~ts "\")\" or \"+\" expected: "
end
| A.Kwd "O" ->
- let f = parse_rest ts in
+ let f = parse_rest symtab ts in
ID f
| A.Kwd "[pi1]" ->
- let f = parse_rest ts in
+ let f = parse_rest symtab ts in
FUS (true, f)
| A.Kwd "[pi2]" ->
- let f = parse_rest ts in
+ let f = parse_rest symtab ts in
FUS (false, f)
- | t -> A.printError mk_exn ~t ~ts
+ | A.Kwd "μ" ->
+ let (_, _, s) = boxinternals true "." in
+ let symbol = Stream.next gensym in
+ let newtab = (s, symbol) :: symtab in
+ let f1 = parse_rest newtab ts in
+ MU (symbol, f1)
+ | A.Kwd "ν" ->
+ let (_, _, s) = boxinternals true "." in
+ let symbol = Stream.next gensym in
+ let newtab = (s, symbol) :: symtab in
+ let f1 = parse_rest newtab ts in
+ NU (symbol, f1)
+ | A.Kwd "AF" ->
+ let f = parse_rest symtab ts in
+ AF f
+ | A.Kwd "EF" ->
+ let f = parse_rest symtab ts in
+ EF f
+ | A.Kwd "AG" ->
+ let f = parse_rest symtab ts in
+ AG f
+ | A.Kwd "EG" ->
+ let f = parse_rest symtab ts in
+ EG f
+ | A.Kwd "A" ->
+ assert (Stream.next ts = A.Kwd "(");
+ let f1 = parse_formula symtab ts in begin
+ match Stream.next ts with
+ | A.Kwd "U" ->
+ let f2 = parse_formula symtab ts in
+ assert (Stream.next ts = A.Kwd ")");
+ AU (f1, f2)
+ | A.Kwd "R" ->
+ let f2 = parse_formula symtab ts in
+ assert (Stream.next ts = A.Kwd ")");
+ AR (f1, f2)
+ | A.Kwd "B" ->
+ let f2 = parse_formula symtab ts in
+ assert (Stream.next ts = A.Kwd ")");
+ AB (f1, f2)
+ | t -> A.printError mk_exn ~t ~ts "one of \"U\" \"R\" \"B\" expected: "
+ end
+ | A.Kwd "E" ->
+ assert (Stream.next ts = A.Kwd "(");
+ let f1 = parse_formula symtab ts in begin
+ match Stream.next ts with
+ | A.Kwd "U" ->
+ let f2 = parse_formula symtab ts in
+ assert (Stream.next ts = A.Kwd ")");
+ EU (f1, f2)
+ | A.Kwd "R" ->
+ let f2 = parse_formula symtab ts in
+ assert (Stream.next ts = A.Kwd ")");
+ ER (f1, f2)
+ | A.Kwd "B" ->
+ let f2 = parse_formula symtab ts in
+ assert (Stream.next ts = A.Kwd ")");
+ EB (f1, f2)
+ | t -> A.printError mk_exn ~t ~ts "one of \"U\" \"R\" \"B\" expected: "
+ end
+ | A.Kwd "AX" ->
+ let f1 = parse_rest symtab ts in
+ AX ("", f1)
+ | A.Kwd "EX" ->
+ let f1 = parse_rest symtab ts in
+ EX ("", f1)
+ | t -> A.printError mk_exn ~t ~ts
"\"<\", \"[\", \"{>=\", \"{<=\", \"@\", \"~\", \"(\",
\"True\", \"False\", \"=\", \"=o\", \"O\" or <ident> expected: "
-
+
(** Parses a sorted formula.
@param ts A token stream.
@return A sorted formula.
@raise CoAlgException If ts does not represent a sorted formula.
*)
let parse_sortedFormula ts =
- let nr =
+ let nr =
match Stream.peek ts with
| Some (A.Int n) ->
if n >= 0 then begin
@@ -749,9 +1104,9 @@ let parse_sortedFormula ts =
n
end else
A.printError mk_exn ~ts ("<non-negative number> expected: ")
- | _ -> 0
+ | _ -> 0
in
- let f = parse_formula ts in
+ let f = parse_formula [] ts in
(nr, f)
(** Parses a list of sorted formulae separated by ";".
@@ -791,7 +1146,7 @@ let importWrapper fkt s =
@return The resulting formula.
@raise CoAlgException if s does not represent a formula.
*)
-let importFormula s = importWrapper parse_formula s
+let importFormula s = importWrapper (parse_formula []) s
(** Parses a string to obtain a sorted formula.
@param s A string representing a sorted formula.
@@ -821,7 +1176,7 @@ let importQuery s =
Stream.junk ts;
let f = parse_sortedFormula ts in
(fl, f)
- | _ ->
+ | _ ->
if List.length fl = 1 then ([], List.hd fl)
else A.printError mk_exn ~ts "\"|-\" expected: "
in
@@ -840,6 +1195,7 @@ let rec nnfNeg f =
| TRUE -> FALSE
| FALSE -> TRUE
| AP _ -> NOT f
+ | VAR _ -> f
| NOT f1 -> nnf f1
| AT (s, f1) -> AT (s, nnfNeg f1)
| OR (f1, f2) -> AND (nnfNeg f1, nnfNeg f2)
@@ -861,9 +1217,16 @@ let rec nnfNeg f =
| ID (f1) -> ID (nnfNeg f1)
| NORM(f1, f2) -> NORMN(nnfNeg f1, nnfNeg f2)
| NORMN(f1, f2) -> NORM (nnfNeg f1, nnfNeg f2)
- | CHC (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2)
+ | CHC (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2)
| FUS (first, f1) -> FUS (first, nnfNeg f1)
-
+ | MU (s, f1) -> NU(s, nnfNeg f1)
+ | NU (s, f1) -> MU(s, nnfNeg f1)
+ | AF _ | EF _
+ | AG _ | EG _
+ | AU _ | EU _
+ | AR _ | ER _
+ | AB _ | EB _ -> raise (CoAlgException ("nnfNeg: CTL should have been removed at this point"))
+
(** Converts a formula to negation normal form
by "pushing in" the negations "~".
The symbols "<=>" and "=>" are substituted by their usual definitions.
@@ -878,7 +1241,8 @@ and nnf f =
| AP _
| NOT (AP _)
| CONST _
- | CONSTN _ -> f
+ | CONSTN _
+ | VAR _ -> f
| NOT f1 -> nnfNeg f1
| AT (s, f1) ->
let ft1 = nnf f1 in
@@ -893,13 +1257,13 @@ and nnf f =
if ft1 == f1 && ft2 == f2 then f else AND (ft1, ft2)
| EQU (f1, f2) -> AND (OR (nnfNeg f1, nnf f2), OR (nnfNeg f2, nnf f1))
| IMP (f1, f2) -> OR (nnfNeg f1, nnf f2)
- | EX (s, f1) ->
+ | EX (s, f1) ->
let ft = nnf f1 in
if ft == f1 then f else EX (s, ft)
| AX (s, f1) ->
let ft = nnf f1 in
if ft == f1 then f else AX (s, ft)
- | ENFORCES (s, f1) ->
+ | ENFORCES (s, f1) ->
let ft = nnf f1 in
if ft == f1 then f else ENFORCES (s, ft)
| ALLOWS (s, f1) ->
@@ -943,7 +1307,18 @@ and nnf f =
| FUS (first, f1) ->
let ft = nnf f1 in
if ft == f1 then f else FUS (first, ft)
-
+ | MU (s, f1) ->
+ let ft = nnf f1 in
+ if ft == f1 then f else MU (s, ft)
+ | NU (s, f1) ->
+ let ft = nnf f1 in
+ if ft == f1 then f else NU (s, ft)
+ | AF _ | EF _
+ | AG _ | EG _
+ | AU _ | EU _
+ | AR _ | ER _
+ | AB _ | EB _ ->
+ raise (CoAlgException ("nnf: CTL should have been removed at this point"))
(** Simplifies a formula.
@param f A formula which must be in negation normal form.
@@ -955,7 +1330,9 @@ let rec simplify f =
| TRUE
| FALSE
| AP _
- | NOT (AP _) -> f
+ | NOT (AP _)
+ | VAR _
+ | NOT (VAR _) -> f
| AT (s, f1) ->
let ft = simplify f1 in
begin
@@ -977,7 +1354,7 @@ let rec simplify f =
| _, TRUE -> TRUE
| _, FALSE -> ft1
| _, _ ->
- if (f1 == ft1) && (f2 == ft2) then f
+ if (f1 == ft1) && (f2 == ft2) then f
else OR (ft1, ft2)
end
| AND (f1, f2) ->
@@ -990,7 +1367,7 @@ let rec simplify f =
| _, TRUE -> ft1
| _, FALSE -> FALSE
| _, _ ->
- if (f1 == ft1) && (f2 == ft2) then f
+ if (f1 == ft1) && (f2 == ft2) then f
else AND (ft1, ft2)
end
| NOT _
@@ -1082,7 +1459,7 @@ let rec simplify f =
match ft2 with
| TRUE -> TRUE
| _ ->
- if (f1 == ft1) && (f2 == ft2) then f
+ if (f1 == ft1) && (f2 == ft2) then f
else NORM (ft1, ft2)
end
| NORMN (f1, f2) ->
@@ -1092,7 +1469,7 @@ let rec simplify f =
match ft2 with
| FALSE -> FALSE
| _ ->
- if (f1 == ft1) && (f2 == ft2) then f
+ if (f1 == ft1) && (f2 == ft2) then f
else NORMN (ft1, ft2)
end
| CHC (f1, f2) ->
@@ -1103,7 +1480,7 @@ let rec simplify f =
| TRUE, TRUE -> TRUE
| FALSE, FALSE -> FALSE
| _, _ ->
- if (f1 == ft1) && (f2 == ft2) then f
+ if (f1 == ft1) && (f2 == ft2) then f
else CHC (ft1, ft2)
end
| FUS (first, f1) ->
@@ -1114,7 +1491,26 @@ let rec simplify f =
| TRUE -> TRUE
| _ -> if ft == f1 then f else FUS (first, ft)
end
-
+ | MU (s, f1) ->
+ let ft = simplify f1 in
+ begin
+ match ft with
+ | TRUE -> TRUE
+ | _ -> if ft == f1 then f else MU (s, ft)
+ end
+ | NU (s, f1) ->
+ let ft = simplify f1 in
+ begin
+ match ft with
+ | TRUE -> TRUE
+ | _ -> if ft == f1 then f else NU (s, ft)
+ end
+ | AF _ | EF _
+ | AG _ | EG _
+ | AU _ | EU _
+ | AR _ | ER _
+ | AB _ | EB _ ->
+ raise (CoAlgException ("nnf: CTL should have been removed at this point"))
(** Destructs an atomic proposition.
@param f An atomic proposition.
@@ -1405,7 +1801,7 @@ let is_fusion f =
| FUS _ -> true
| _ -> false
-
+
(** The constant True.
*)
let const_true = TRUE
@@ -1413,7 +1809,7 @@ let const_true = TRUE
(** The constant False.
*)
let const_false = FALSE
-
+
(** Constructs an atomic proposition.
@param s The name of the atomic proposition.
@return The atomic proposition with name s.
@@ -1437,7 +1833,7 @@ let const_nom s =
@return The negation of f.
*)
let const_not f = NOT f
-
+
(** Constructs an @-formula from a name and a formula.
@param s A nominal name.
@param f A formula.
@@ -1456,7 +1852,7 @@ let const_or f1 f2 = OR (f1, f2)
@param f1 The first formula (LHS).
@param f2 The second formula (LHS).
@return The formula f1 & f2.
- *)
+ *)
let const_and f1 f2 = AND (f1, f2)
(** Constructs an equivalence from two formulae.
@@ -1532,6 +1928,9 @@ let const_fusion first f1 = FUS (first, f1)
(** Hash-consed formulae, which are in negation normal form,
such that structural and physical equality coincide.
+
+ Also CTL has been replaced by the equivalent μ-Calculus
+ constructs
*)
type hcFormula = (hcFormula_node, formula) HC.hash_consed
and hcFormula_node =
@@ -1557,6 +1956,9 @@ and hcFormula_node =
| HCNORMN of hcFormula * hcFormula
| HCCHC of hcFormula * hcFormula
| HCFUS of bool * hcFormula
+ | HCMU of string * hcFormula
+ | HCNU of string * hcFormula
+ | HCVAR of string
(** Determines whether two formula nodes are structurally equal.
@param f1 The first formula node.
@@ -1580,7 +1982,7 @@ let equal_hcFormula_node f1 f2 =
| HCALLOWS (s1, f1), HCALLOWS (s2, f2) -> compare s1 s2 = 0 && f1 == f2
| HCMORETHAN (n1, s1, f1), HCMORETHAN (n2, s2, f2)
| HCMAXEXCEPT (n1, s1, f1), HCMAXEXCEPT (n2, s2, f2) ->
- n1 = n2 && compare s1 s2 = 0 && f1 == f2
+ n1 = n2 && compare s1 s2 = 0 && f1 == f2
| HCATLEASTPROB (p1, f1), HCATLEASTPROB (p2,f2) ->
p1 = p2 && f1 == f2
| HCLESSPROBFAIL (p1, f1), HCLESSPROBFAIL (p2,f2) ->
@@ -1589,6 +1991,9 @@ let equal_hcFormula_node f1 f2 =
| HCNORM (f1a, f1b), HCNORMN (f2a, f2b) -> f1a == f2a && f1b == f2b
| HCCHC (f1a, f1b), HCCHC (f2a, f2b) -> f1a == f2a && f1b == f2b
| HCFUS (first1, f1), HCFUS (first2, f2) -> first1 = first2 && f1 == f2
+ | HCMU (name1, f1), HCMU(name2, f2) -> compare name1 name2 = 0 && f1 == f2
+ | HCNU (name1, f1), HCNU(name2, f2) -> compare name1 name2 = 0 && f1 == f2
+ | HCVAR name1, HCVAR name2 -> compare name1 name2 = 0
(* The rest could be shortened to | _ -> false,
but then the compiler would not warn if the formula type is extended
and this function is not updated accordingly.*)
@@ -1613,7 +2018,10 @@ let equal_hcFormula_node f1 f2 =
| HCNORM _, _
| HCNORMN _, _
| HCCHC _, _
- | HCFUS _, _ -> false
+ | HCFUS _, _
+ | HCMU _, _
+ | HCNU _, _
+ | HCVAR _, _ -> false
(** Computes the hash value of a formula node.
@param f A formula node.
@@ -1625,7 +2033,8 @@ let hash_hcFormula_node f =
| HCTRUE -> 0
| HCFALSE -> 1
| HCAP s
- | HCNOT s -> base * Hashtbl.hash s + 1
+ | HCNOT s
+ | HCVAR s -> base * Hashtbl.hash s + 1
| HCAT (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 2
| HCOR (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 5
| HCAND (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 6
@@ -1644,6 +2053,8 @@ let hash_hcFormula_node f =
| HCNORM (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 18
| HCNORMN (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 19
| HCID (f1) -> base * f1.HC.hkey + 20
+ | HCMU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 21
+ | HCNU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 22
(** Determines the "real" formula of a formula node.
@param f A formula node.
@@ -1654,6 +2065,7 @@ let toFml_hcFormula_node f =
| HCTRUE -> TRUE
| HCFALSE -> FALSE
| HCAP s -> AP s
+ | HCVAR s -> VAR s
| HCNOT s -> NOT (AP s)
| HCAT (s, f1) -> AT (s, f1.HC.fml)
| HCOR (f1, f2) -> OR (f1.HC.fml, f2.HC.fml)
@@ -1673,6 +2085,8 @@ let toFml_hcFormula_node f =
| HCNORMN (f1, f2) -> NORMN(f1.HC.fml, f2.HC.fml)
| HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml)
| HCFUS (first, f1) -> FUS (first, f1.HC.fml)
+ | HCMU (var, f1) -> MU (var, f1.HC.fml)
+ | HCNU (var, f1) -> NU (var, f1.HC.fml)
(** Determines the negation (in negation normal form) of a formula node.
@param f A formula node.
@@ -1684,6 +2098,7 @@ let negNde_hcFormula_node f =
| HCFALSE -> HCTRUE
| HCAP s -> HCNOT s
| HCNOT s -> HCAP s
+ | HCVAR s -> f
| HCAT (s, f1) -> HCAT (s, f1.HC.neg)
| HCOR (f1, f2) -> HCAND (f1.HC.neg, f2.HC.neg)
| HCAND (f1, f2) -> HCOR (f1.HC.neg, f2.HC.neg)
@@ -1702,6 +2117,8 @@ let negNde_hcFormula_node f =
| HCNORMN (f1, f2) -> HCNORM(f1.HC.neg, f2.HC.neg)
| HCCHC (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg)
| HCFUS (first, f1) -> HCFUS (first, f1.HC.neg)
+ | HCMU (name, f1) -> HCNU (name, f1.HC.neg)
+ | HCNU (name, f1) -> HCMU (name, f1.HC.neg)
(** An instantiation of hash-consing for formulae.
*)
@@ -1727,6 +2144,7 @@ let rec hc_formula hcF f =
| TRUE -> HcFormula.hashcons hcF HCTRUE
| FALSE -> HcFormula.hashcons hcF HCFALSE
| AP s -> HcFormula.hashcons hcF (HCAP s)
+ | VAR s -> HcFormula.hashcons hcF (HCVAR s)
| NOT (AP s) -> HcFormula.hashcons hcF (HCNOT s)
| AT (s, f1) ->
let tf1 = hc_formula hcF f1 in
@@ -1788,6 +2206,139 @@ let rec hc_formula hcF f =
| FUS (first, f1) ->
let tf1 = hc_formula hcF f1 in
HcFormula.hashcons hcF (HCFUS (first, tf1))
+ | MU (var, f1) ->
+ let tf1 = hc_formula hcF f1 in
+ HcFormula.hashcons hcF (HCMU (var, tf1))
+ | NU (var, f1) ->
+ let tf1 = hc_formula hcF f1 in
+ HcFormula.hashcons hcF (HCNU (var, tf1))
+ | AF _ | EF _
+ | AG _ | EG _
+ | AU _ | EU _
+ | AR _ | ER _
+ | AB _ | EB _ ->
+ raise (CoAlgException ("nnf: CTL should have been removed at this point"))
+
+(* Replace the Variable name in f with formula formula
+ hc_replace foo φ ψ => ψ[foo |-> φ]
+ *)
+let rec hc_replace hcF name (formula: hcFormula) (f: hcFormula) =
+ let func = hc_replace hcF name formula in
+ let gennew = HcFormula.hashcons hcF in
+ match f.HC.node with
+ | HCTRUE
+ | HCFALSE
+ | HCAP _
+ | HCNOT _
+ | HCCONST _
+ | HCCONSTN _ -> f
+ | HCVAR s ->
+ if compare s name == 0
+ then formula
+ else f
+ | HCAT (s, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCAT(s, nf1))
+ | HCOR (f1, f2) ->
+ let nf1 = func f1 in
+ let nf2 = func f2 in
+ if nf1 == f1 && nf2 == f2 then f else gennew (HCOR(nf1, nf2))
+ | HCAND (f1, f2) ->
+ let nf1 = func f1 in
+ let nf2 = func f2 in
+ if nf1 == f1 && nf2 == f2 then f else gennew (HCAND(nf1, nf2))
+ | HCEX (s, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCEX(s, nf1))
+ | HCAX (s, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCAX(s, nf1))
+ | HCENFORCES (s, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCENFORCES(s, nf1))
+ | HCALLOWS (s, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCALLOWS(s, nf1))
+ | HCMORETHAN (n, s, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCMORETHAN(n, s, nf1))
+ | HCMAXEXCEPT (n, s, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCMAXEXCEPT(n, s, nf1))
+ | HCATLEASTPROB (p, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCATLEASTPROB(p, nf1))
+ | HCLESSPROBFAIL (p, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCLESSPROBFAIL(p, nf1))
+ | HCID f1 ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCID(nf1))
+ | HCNORM (f1, f2) ->
+ let nf1 = func f1 in
+ let nf2 = func f2 in
+ if nf1 == f1 && nf2 == f2 then f else gennew (HCNORM(nf1, nf2))
+ | HCNORMN (f1, f2) ->
+ let nf1 = func f1 in
+ let nf2 = func f2 in
+ if nf1 == f1 && nf2 == f2 then f else gennew (HCNORMN(nf1, nf2))
+ | HCCHC (f1, f2) ->
+ let nf1 = func f1 in
+ let nf2 = func f2 in
+ if nf1 == f1 && nf2 == f2 then f else gennew (HCCHC(nf1, nf2))
+ | HCFUS (first, f1) ->
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCFUS(first, nf1))
+ | HCMU (var, f1) ->
+ if compare var name != 0 then
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCMU(var, nf1))
+ else
+ f
+ | HCNU (var, f1) ->
+ if compare var name != 0 then
+ let nf1 = func f1 in
+ if nf1 == f1 then f else gennew (HCNU(var, nf1))
+ else
+ f
+
+let rec hc_freeIn variable (f: hcFormula) =
+ match f.HC.node with
+ | HCTRUE
+ | HCFALSE
+ | HCAP _
+ | HCNOT _
+ | HCCONST _
+ | HCCONSTN _ -> false
+ | HCVAR s ->
+ if compare variable s == 0
+ then true
+ else false
+ | HCAT (s, f1) ->
+ hc_freeIn variable f1
+ | HCOR (f1, f2)
+ | HCAND (f1, f2) ->
+ hc_freeIn variable f1 || hc_freeIn variable f2
+ | HCEX (_, f1)
+ | HCAX (_, f1)
+ | HCENFORCES (_, f1)
+ | HCALLOWS (_, f1)
+ | HCMORETHAN (_, _, f1)
+ | HCMAXEXCEPT (_, _, f1)
+ | HCATLEASTPROB (_, f1)
+ | HCLESSPROBFAIL (_, f1)
+ | HCID f1 ->
+ hc_freeIn variable f1
+ | HCNORM (f1, f2)
+ | HCNORMN (f1, f2)
+ | HCCHC (f1, f2) ->
+ hc_freeIn variable f1 || hc_freeIn variable f2
+ | HCFUS (first, f1) ->
+ hc_freeIn variable f1
+ | HCMU (var, f1)
+ | HCNU (var, f1) ->
+ (* Do we need to exclude bound variables here? *)
+ hc_freeIn variable f1
(** An instantiation of a hash table (of the standard library)
diff --git a/src/lib/CoAlgFormula.mli b/src/lib/CoAlgFormula.mli
index 3c70e1d8965589c92105af1e1bd84bef5f0b98e8..7ea6b0f8515081bc7f0cddc6218f7433ba4af04e 100644
--- a/src/lib/CoAlgFormula.mli
+++ b/src/lib/CoAlgFormula.mli
@@ -41,6 +41,19 @@ type formula =
| NORMN of formula * formula (* \neg NORM (\neg A, \neg B) *)
| CHC of formula * formula
| FUS of bool * formula
+ | MU of string * formula
+ | NU of string * formula
+ | VAR of string
+ | AF of formula
+ | EF of formula
+ | AG of formula
+ | EG of formula
+ | AU of formula * formula
+ | EU of formula * formula
+ | AR of formula * formula
+ | ER of formula * formula
+ | AB of formula * formula
+ | EB of formula * formula
exception ConversionException of formula
@@ -66,6 +79,8 @@ val importFormula : string -> formula
val importSortedFormula : string -> sortedFormula
val importQuery : string -> sortedFormula list * sortedFormula
+val verifyFormula : formula -> unit
+
val nnfNeg : formula -> formula
val nnf : formula -> formula
@@ -146,9 +161,14 @@ and hcFormula_node =
| HCNORMN of hcFormula * hcFormula
| HCCHC of hcFormula * hcFormula
| HCFUS of bool * hcFormula
+ | HCMU of string * hcFormula
+ | HCNU of string * hcFormula
+ | HCVAR of string
module HcFormula : (HashConsing.S with type nde = hcFormula_node and type fml = formula)
val hc_formula : HcFormula.t -> formula -> hcFormula
+val hc_replace : HcFormula.t -> string -> hcFormula -> hcFormula -> hcFormula
+val hc_freeIn : string -> hcFormula -> bool
module HcFHt : (Hashtbl.S with type key = hcFormula)
diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml
index d4b321b7ae10e98b1d1e2d7a9be2dff627f0e04d..fd46280ae2faeba53026db0dc5be8ff2cccccaf3 100644
--- a/src/lib/CoAlgLogics.ml
+++ b/src/lib/CoAlgLogics.ml
@@ -11,8 +11,8 @@ open Gmlmip
module S = MiscSolver
(** directly return a list of rules **)
-let mkRuleList_MultiModalK sort bs sl : rule list =
- (* arguments:
+let mkRuleList_MultiModalK sort bs defer sl : rule list =
+ (* arguments:
sort: type of formulae in bs (needed to disambiguate hashing)
sl: sorts functor arguments, e.g. type of argument formulae
bs: tableau sequent consisting of modal atoms
@@ -26,6 +26,7 @@ let mkRuleList_MultiModalK sort bs sl : rule list =
NB: propagating the whole premiss is always safe.
*)
assert (List.length sl = 1);
+ let refocusing = bsetCompare (bsetMakeRealEmpty ()) defer = 0 in
let dep f bsl = (* dependencies for formula f (f is a diamond) *)
assert (List.length bsl = 1); (* -+ *)
let bs1 = List.hd bsl in (* -+-> [bs1] := bsl *)
@@ -46,17 +47,27 @@ let mkRuleList_MultiModalK sort bs sl : rule list =
let getRules f acc =
if lfGetType sort f = ExF then (* f = ∃R.C,i.e. a diamond *)
let bs1 = bsetMake () in
- bsetAdd bs1 (lfGetDest1 sort f); (* bs1 := { C } *)
+ let defer1 = bsetMakeRealEmpty () in
+ let nextf = (lfGetDest1 sort f) in
+ bsetAdd bs1 nextf; (* bs1 := { C } *)
+ if (refocusing && (lfGetDeferral sort nextf) != (Hashtbl.hash "ε")) ||
+ ((bsetMem defer f) && (lfGetDeferral sort f) = (lfGetDeferral sort nextf))
+ then
+ bsetAdd defer1 nextf;
let (role : int) = lfGetDest3 sort f in (* role := R *)
let filterFkt f1 =
if lfGetType sort f1 = AxF && lfGetDest3 sort f1 = role then
(* if f1 = ∀R.D then bs1 = bs1 ∪ { D } *)
- bsetAdd bs1 (lfGetDest1 sort f1)
+ let nextf1 = (lfGetDest1 sort f1) in
+ bsetAdd bs1 nextf1;
+ (if (refocusing && (lfGetDeferral sort nextf1) != (Hashtbl.hash "ε")) ||
+ ((bsetMem defer f1) && (lfGetDeferral sort f1) = (lfGetDeferral sort nextf1)) then
+ bsetAdd defer1 nextf1;)
else ()
in
bsetIter filterFkt bs; (* bs1 := bs1 ∪ { D | some "∀R.D" ∈ bs } *)
let s1 = List.hd sl in (* [s1] := sl *)
- let rle = (dep f, lazylistFromList [(s1, bs1)]) in
+ let rle = (dep f, lazylistFromList [(s1, bs1, defer1)]) in
rle::acc
else acc
in
@@ -72,14 +83,14 @@ let mkRuleList_MultiModalK sort bs sl : rule list =
*)
bsetFold getRules bs []
-let mkRule_MultiModalK sort bs sl : stateExpander =
- let rules = mkRuleList_MultiModalK sort bs sl in
+let mkRule_MultiModalK sort bs defer sl : stateExpander =
+ let rules = mkRuleList_MultiModalK sort bs defer sl in
lazylistFromList rules
(* TODO: test it with:
make && ./coalg sat <<< $'<R> False \n [R] False \n [R] True'
*)
-let mkRule_MultiModalKD sort bs sl : stateExpander =
+let mkRule_MultiModalKD sort bs defer sl : stateExpander =
assert (List.length sl = 1); (* functor has just one argument *)
let s1 = List.hd sl in (* [s1] = sl *)
let roles = S.makeBS () in
@@ -114,14 +125,21 @@ let mkRule_MultiModalKD sort bs sl : stateExpander =
res
in
let succs = bsetMake () in (* succs := {D | ∀r.D ∈ bs *)
+ let defer1 = bsetMakeRealEmpty () in (* TODO: actually track deferrals *)
let f formula =
if lfGetType sort formula = AxF
&& lfGetDest3 sort formula = r
- then ignore (bsetAdd succs (lfGetDest1 sort formula))
+ then
+ let nextf1 = (lfGetDest1 sort formula) in
+ bsetAdd succs nextf1;
+ ignore (if (bsetMem defer formula) &&
+ (lfGetDeferral sort formula) = (lfGetDeferral sort nextf1)
+ then
+ bsetAdd defer1 nextf1;)
else ()
in
bsetIter f bs;
- (dep r, lazylistFromList [(s1, succs)])::acc
+ (dep r, lazylistFromList [(s1, succs, defer1)])::acc
in
(*
mkRule_MultiModalKD sort bs [s1]
@@ -132,12 +150,112 @@ let mkRule_MultiModalKD sort bs sl : stateExpander =
}
∪ mkRule_MultiModalK sort bs [s1]
*)
- let rules = mkRuleList_MultiModalK sort bs sl in
+ let rules = mkRuleList_MultiModalK sort bs defer sl in
(* extend rules from K with enforcing of successors *)
let rules = S.foldBS getRules roles rules in
lazylistFromList rules
+(** directly return a list of rules **)
+let mkRuleList_Monotone sort bs defer sl : rule list =
+ (* arguments:
+ sort: type of formulae in bs (needed to disambiguate hashing)
+ sl: sorts functor arguments, e.g. type of argument formulae
+ bs: tableau sequent consisting of modal atoms
+ (premiss, conjunctive set of formulae represented by hash values)
+ result: set R of (propagation function, rule conclusion) pairs
+ s.t. [ (premiss / conc) : (_, conc) \in R ] are all rules
+ applicable to premiss.
+ Propagation functions map unsatisfiable subsets of the
+ (union of all?) conclusion(s) to unsatisfiable subsets of
+ the premiss -- this is a hook for backjumping.
+ NB: propagating the whole premiss is always safe.
+ *)
+ assert (List.length sl = 1);
+ let refocusing = bsetCompare (bsetMakeRealEmpty ()) defer = 0 in
+ let dep f bsl = (* dependencies for formula f (f is a diamond) *)
+ assert (List.length bsl = 1); (* -+ *)
+ let bs1 = List.hd bsl in (* -+-> [bs1] := bsl *)
+ let res = bsetMake () in
+ bsetAdd res f;
+ let (role : int) = lfGetDest3 sort f in (* ♥R.? := f, ♥ ∈ {∃,∀} *)
+ let filterFkt f1 =
+ if lfGetType sort f1 = AxF && lfGetDest3 sort f1 = role
+ && bsetMem bs1 (lfGetDest1 sort f1)
+ then
+ (* if f1 = ∀R.C and C ∈ bs1 then res = res ∪ {∀R.C} *)
+ bsetAdd res f1
+ else ()
+ in
+ bsetIter filterFkt bs;
+ res
+ in
+ let getRules f acc =
+ if lfGetType sort f = ExF then (* f = ∃R.C,i.e. a diamond *)
+ let bs1base = bsetMake () in
+ let defer1base = bsetMakeRealEmpty () in
+ let nextf = (lfGetDest1 sort f) in
+ bsetAdd bs1base nextf; (* bs1 := { C } *)
+ if (refocusing && (lfGetDeferral sort nextf) != (Hashtbl.hash "ε")) ||
+ ((bsetMem defer f) && (lfGetDeferral sort f) = (lfGetDeferral sort nextf))
+ then
+ bsetAdd defer1base nextf
+ else ();
+ let (role : int) = lfGetDest3 sort f in (* role := R *)
+ let filterFkt f1 acc =
+ if lfGetType sort f1 = AxF && lfGetDest3 sort f1 = role then
+ let bs1 = bsetCopy bs1base in
+ let defer1 = bsetCopy defer1base in
+ (* if f1 = ∀R.D then bs1 = bs1 ∪ { D } *)
+ let nextf1 = (lfGetDest1 sort f1) in
+ bsetAdd bs1 nextf1;
+ if (refocusing && (lfGetDeferral sort nextf1) != (Hashtbl.hash "ε")) ||
+ ((bsetMem defer f1) && (lfGetDeferral sort f1) = (lfGetDeferral sort nextf1))
+ then
+ bsetAdd defer1 nextf1
+ else ();
+ let s1 = List.hd sl in (* [s1] := sl *)
+ let rle1 = (dep f, lazylistFromList [(s1, bs1, defer1)]) in
+ rle1::acc
+ else acc
+ in
+ let s1 = List.hd sl in (* [s1] := sl *)
+ let rle = (dep f, lazylistFromList [(s1, bs1base, defer1base)]) in
+ let fold = bsetFold filterFkt bs acc in (* bs1 := bs1 ∪ { D | some "∀R.D" ∈ bs } *)
+ rle::fold
+ else if lfGetType sort f = AxF then
+ let bs1 = bsetMake () in
+ let defer1 = bsetMakeRealEmpty () in
+ (* if f1 = ∀R.D then bs1 = bs1 ∪ { D } *)
+ let nextf1 = (lfGetDest1 sort f) in
+ bsetAdd bs1 nextf1;
+ if (refocusing && (lfGetDeferral sort nextf1) != (Hashtbl.hash "ε")) ||
+ ((bsetMem defer f) && (lfGetDeferral sort f) = (lfGetDeferral sort nextf1))
+ then
+ bsetAdd defer1 nextf1
+ else ();
+ let s1 = List.hd sl in (* [s1] := sl *)
+ let rle1 = (dep f, lazylistFromList [(s1, bs1, defer1)]) in
+ rle1::acc
+ else acc
+ in
+ (* effectively:
+ mkRule_MultiModalK sort bs [s1]
+ = { ( λ[bs1]. { ∃R.C } ∪ { ∀R.D
+ | ∀R.D ∈ bs, D ∈ bs1
+ , [(s1, {C}∪{D | "∀R.D" ∈ bs)]
+ )
+ | "∃R.C" ∈ bs
+ }
+ *)
+ bsetFold getRules bs []
+
+let mkRule_Monotone sort bs defer sl : stateExpander =
+ let rules = mkRuleList_Monotone sort bs defer sl in
+ lazylistFromList rules
+
+
+
(* CoalitionLogic: helper functions *)
(*val subset : bitset -> bitset -> bool*)
let bsetlen (a: bset) : int =
@@ -196,14 +314,19 @@ let compatible sort (a: bset) formula1 =
/ \i=1 a_i /\ b / \j=1 c_j
*)
-(* Not yet implemented: backjumping hooks.
+(* Not yet implemented: backjumping hooks.
E.g. in Rule 1, if a subset I of {a_1, ..., a_n} is unsat, then {[C_i] a_i : i \in I} is
already unsat.
*)
-let mkRule_CL sort bs sl : stateExpander =
+let mkRule_CL sort bs defer sl : stateExpander =
assert (List.length sl = 1); (* TODO: Why? *)
+ let refocusing = bsetCompare (bsetMakeRealEmpty ()) defer = 0 in
+ let deferral_tracking f nextf =
+ (refocusing && (lfGetDeferral sort nextf) != (Hashtbl.hash "ε")) ||
+ ((bsetMem defer f) && (lfGetDeferral sort f) = (lfGetDeferral sort nextf))
+ in
let s1 = List.hd sl in (* [s1] = List.hd sl *)
let boxes = bsetFilter bs (fun f -> lfGetType sort f = EnforcesF) in
let diamonds = bsetFilter bs (fun f -> lfGetType sort f = AllowsF) in
@@ -231,8 +354,10 @@ let mkRule_CL sort bs sl : stateExpander =
print_endline ("N-Cands: " ^(CoAlgMisc.bsetToString sort nCands));
print_endline ("D-Cands: " ^(CoAlgMisc.bsetToString sort dCands));
*)
- let c_j : localFormula list =
- bsetFold (fun f a -> (lfGetDest1 sort f)::a) nCands []
+ let c_j : (localFormula * bool) list =
+ bsetFold (fun f a -> let nextf = lfGetDest1 sort f in
+ (nextf, (deferral_tracking f nextf))::a)
+ nCands []
in
(* rule 2 for diamaonds where D is a proper subset of the agent set N *)
let getRule2 diamDb acc = (* diamDb = <D> b *)
@@ -245,8 +370,11 @@ let mkRule_CL sort bs sl : stateExpander =
in
let maxdisj = maxDisjoints sort (bsetFilter boxes hasAppropriateAglist) in
let createSingleRule acc coalitions =
- let a_i : localFormula list =
- bsetFold (fun f a -> (lfGetDest1 sort f)::a) coalitions []
+ let a_i : (localFormula * bool) list =
+ bsetFold (fun f a ->
+ let nextf = lfGetDest1 sort f in
+ (nextf, (deferral_tracking f nextf))::a)
+ coalitions []
in
(* now do rule 2:
coalitions /\ <d> b /\ nCands
@@ -254,9 +382,19 @@ let mkRule_CL sort bs sl : stateExpander =
a_i /\ b /\ c_j
*)
let children = bsetMakeRealEmpty () in
- List.iter (bsetAdd children) (b::c_j) ;
- List.iter (bsetAdd children) (a_i) ;
- ((fun bs1 -> bs), lazylistFromList [(s1, children)])::acc
+ let defer1 = bsetMakeRealEmpty () in
+ bsetAdd children b;
+ if deferral_tracking diamDb b
+ then bsetAdd defer1 b;
+ List.iter (fun (f, isdefer) ->
+ bsetAdd children f;
+ if isdefer then bsetAdd defer1 f)
+ c_j ;
+ List.iter (fun (f, isdefer) ->
+ bsetAdd children f;
+ if isdefer then bsetAdd defer1 f)
+ a_i ;
+ ((fun bs1 -> bs), lazylistFromList [(s1, children, defer1)])::acc
in
List.fold_left createSingleRule acc maxdisj
in
@@ -272,8 +410,10 @@ let mkRule_CL sort bs sl : stateExpander =
(* create rule 2 once for all the diamonds with a full agent set *)
let maxdisj = maxDisjoints sort boxes in
let createSingleRule acc coalitions =
- let a_i : localFormula list =
- bsetFold (fun f a -> (lfGetDest1 sort f)::a) coalitions []
+ let a_i : (localFormula * bool) list =
+ bsetFold (fun f a -> let nextf = lfGetDest1 sort f in
+ (nextf, (deferral_tracking f nextf))::a)
+ coalitions []
in
(* now do rule 2:
coalitions /\ nCands
@@ -281,9 +421,16 @@ let mkRule_CL sort bs sl : stateExpander =
a_i /\ c_j
*)
let children = bsetMakeRealEmpty () in
- List.iter (bsetAdd children) (c_j) ;
- List.iter (bsetAdd children) (a_i) ;
- ((fun bs1 -> bs), lazylistFromList [(s1, children)])::acc
+ let defer1 = bsetMakeRealEmpty () in
+ List.iter (fun (f, isdefer) ->
+ bsetAdd children f;
+ if isdefer then bsetAdd defer1 f)
+ c_j ;
+ List.iter (fun (f, isdefer) ->
+ bsetAdd children f;
+ if isdefer then bsetAdd defer1 f)
+ a_i ;
+ ((fun bs1 -> bs), lazylistFromList [(s1, children, defer1)])::acc
in
List.fold_left createSingleRule acc maxdisj
end else acc
@@ -297,8 +444,14 @@ let mkRule_CL sort bs sl : stateExpander =
a_i
*)
let a_i : bset = bsetMakeRealEmpty () in
- bsetIter (fun f -> bsetAdd a_i (lfGetDest1 sort f)) coalitions ;
- ((fun bs1 -> bs), lazylistFromList [(s1, a_i)])::acc
+ let defer1 : bset = bsetMakeRealEmpty () in
+ bsetIter (fun f ->
+ let nextf = lfGetDest1 sort f in
+ bsetAdd a_i nextf;
+ if deferral_tracking f nextf
+ then bsetAdd defer1 nextf)
+ coalitions ;
+ ((fun bs1 -> bs), lazylistFromList [(s1, a_i, defer1)])::acc
in
let rules = List.fold_left getRule1 rules disjoints in
(*
@@ -310,8 +463,9 @@ let mkRule_CL sort bs sl : stateExpander =
*)
lazylistFromList rules
-let mkRule_GML sort bs sl : stateExpander =
+let mkRule_GML sort bs defer sl : stateExpander =
assert (List.length sl = 1);
+ let defer1 = bsetMake () in (* TODO: track deferrals *)
let s1 = List.hd sl in (* [s1] = List.hd sl *)
let diamonds = bsetFilter bs (fun f -> lfGetType sort f = MoreThanF) in
let boxes = bsetFilter bs (fun f -> lfGetType sort f = MaxExceptF) in
@@ -347,7 +501,7 @@ let mkRule_GML sort bs sl : stateExpander =
in
bsetAdd res f)
conj;
- (s1,res)
+ (s1,res, defer1)
in
let rc = List.map handleConjunction rc in
((fun bs1 -> bs),lazylistFromList rc)::acc
@@ -356,8 +510,9 @@ let mkRule_GML sort bs sl : stateExpander =
let rules = S.foldBS addRule roles [] in
lazylistFromList rules
-let mkRule_PML sort bs sl : stateExpander =
+let mkRule_PML sort bs defer sl : stateExpander =
assert (List.length sl = 1);
+ let defer1 = bsetMake () in (* TODO: track deferrals *)
let s1 = List.hd sl in (* [s1] = List.hd sl *)
let diamonds = bsetFilter bs (fun f -> lfGetType sort f = AtLeastProbF) in
let boxes = bsetFilter bs (fun f -> lfGetType sort f = LessProbFailF) in
@@ -394,7 +549,7 @@ let mkRule_PML sort bs sl : stateExpander =
end
in
List.iter handleLiteral conj;
- (s1,res)
+ (s1,res, defer1)
in
let rc = List.map handleConjunction rc in
((fun bs1 -> bs),lazylistFromList rc)::acc
@@ -403,7 +558,7 @@ let mkRule_PML sort bs sl : stateExpander =
lazylistFromList rules
(* constant functor *)
-let mkRule_Const colors sort bs sl : stateExpander =
+let mkRule_Const colors sort bs defer sl : stateExpander =
assert (List.length sl = 1); (* just one (formal) argument *)
let helper (f:localFormula) (pos, neg) =
let col = lfGetDest3 sort f in
@@ -412,18 +567,24 @@ let mkRule_Const colors sort bs sl : stateExpander =
| ConstF -> ((col::pos), neg)
| _ -> (pos, neg)
in
- let (pos, neg) = bsetFold helper bs ([], []) in (* pos/neg literals *)
+ let (pos, neg) = bsetFold helper bs ([], []) in (* pos/neg literals *)
let clash = List.exists (fun l -> List.mem l pos) neg in (* =a /\ ~ = a *)
let allneg = List.length colors = List.length neg in
let twopos = List.length pos > 1 in
- let rules = if (clash || allneg || twopos)
+ let rules = if (clash || allneg || twopos)
then [((fun x -> bs), lazylistFromList [])] (* no backjumping *)
else []
- in
+ in
lazylistFromList rules
-let mkRule_Identity sort bs sl : stateExpander =
+let mkRule_Identity sort bs defer sl : stateExpander =
assert (List.length sl = 1); (* Identity has one argument *)
+ let refocusing = bsetCompare (bsetMakeRealEmpty ()) defer = 0 in
+ let deferral_tracking defer f nextf =
+ if (refocusing && (lfGetDeferral sort nextf) != (Hashtbl.hash "ε")) ||
+ ((bsetMem defer f) && (lfGetDeferral sort f) = (lfGetDeferral sort nextf))
+ then bsetAdd defer nextf
+ in
let s1 = List.hd sl in
let dep bsl = (* return arguments prefixed with identity operator *)
assert (List.length bsl = 1);
@@ -439,20 +600,31 @@ let mkRule_Identity sort bs sl : stateExpander =
res
in
let bs1 = bsetMake () in
+ let defer1 = bsetMakeRealEmpty () in
let getRule f =
- if lfGetType sort f = IdF
- then bsetAdd bs1 (lfGetDest1 sort f)
+ if lfGetType sort f = IdF
+ then
+ begin
+ deferral_tracking defer1 f (lfGetDest1 sort f);
+ bsetAdd bs1 (lfGetDest1 sort f)
+ end
else ()
in
bsetIter getRule bs;
- lazylistFromList [(dep, lazylistFromList [(s1, bs1)])]
+ lazylistFromList [(dep, lazylistFromList [(s1, bs1, defer1)])]
-let mkRule_DefaultImplication sort bs sl : stateExpander =
+let mkRule_DefaultImplication sort bs defer sl : stateExpander =
raise (CoAlgFormula.CoAlgException ("Default Implication Not yet implemented."))
-
-let mkRule_Choice sort bs sl : stateExpander =
+
+let mkRule_Choice sort bs defer sl : stateExpander =
assert (List.length sl = 2);
+ let refocusing = bsetCompare (bsetMakeRealEmpty ()) defer = 0 in
+ let deferral_tracking defer f nextf =
+ if (refocusing && (lfGetDeferral sort nextf) != (Hashtbl.hash "ε")) ||
+ ((bsetMem defer f) && (lfGetDeferral sort f) = (lfGetDeferral sort nextf))
+ then bsetAdd defer nextf
+ in
let dep bsl =
assert (List.length bsl = 2);
let bs1 = List.nth bsl 0 in
@@ -468,21 +640,32 @@ let mkRule_Choice sort bs sl : stateExpander =
res
in
let bs1 = bsetMake () in
+ let defer1 = bsetMakeRealEmpty () in
let bs2 = bsetMake () in
+ let defer2 = bsetMakeRealEmpty () in
let getRule f =
- if lfGetType sort f = ChcF then begin
- bsetAdd bs1 (lfGetDest1 sort f);
- bsetAdd bs2 (lfGetDest2 sort f)
- end else ()
+ if lfGetType sort f = ChcF then
+ begin
+ bsetAdd bs1 (lfGetDest1 sort f);
+ deferral_tracking defer1 f (lfGetDest1 sort f);
+ bsetAdd bs2 (lfGetDest2 sort f);
+ deferral_tracking defer2 f (lfGetDest2 sort f)
+ end else ()
in
bsetIter getRule bs;
let s1 = List.nth sl 0 in
let s2 = List.nth sl 1 in
- lazylistFromList [(dep, lazylistFromList [(s1, bs1); (s2, bs2)])]
+ lazylistFromList [(dep, lazylistFromList [(s1, bs1, defer1); (s2, bs2, defer2)])]
-let mkRule_Fusion sort bs sl : stateExpander =
+let mkRule_Fusion sort bs defer sl : stateExpander =
assert (List.length sl = 2);
+ let refocusing = bsetCompare (bsetMakeRealEmpty ()) defer = 0 in
+ let deferral_tracking defer f nextf =
+ if (refocusing && (lfGetDeferral sort nextf) != (Hashtbl.hash "ε")) ||
+ ((bsetMem defer f) && (lfGetDeferral sort f) = (lfGetDeferral sort nextf))
+ then bsetAdd defer nextf
+ in
let dep proj bsl =
assert (List.length bsl = 1);
let bs1 = List.hd bsl in
@@ -497,17 +680,28 @@ let mkRule_Fusion sort bs sl : stateExpander =
res
in
let bs1 = bsetMake () in
+ let defer1 = bsetMakeRealEmpty () in
let bs2 = bsetMake () in
+ let defer2 = bsetMakeRealEmpty () in
let getRule f =
if lfGetType sort f = FusF then
- if lfGetDest3 sort f = 0 then bsetAdd bs1 (lfGetDest1 sort f)
- else bsetAdd bs2 (lfGetDest1 sort f)
+ if lfGetDest3 sort f = 0 then
+ begin
+ deferral_tracking defer1 f (lfGetDest1 sort f);
+ bsetAdd bs1 (lfGetDest1 sort f)
+ end
+ else
+ begin
+ deferral_tracking defer2 f (lfGetDest1 sort f);
+ bsetAdd bs2 (lfGetDest1 sort f)
+ end
else ()
in
bsetIter getRule bs;
let s1 = List.nth sl 0 in
let s2 = List.nth sl 1 in
- lazylistFromList [(dep 0, lazylistFromList [(s1, bs1)]); (dep 1, lazylistFromList [(s2, bs2)])]
+ lazylistFromList [(dep 0, lazylistFromList [(s1, bs1, defer1)]);
+ (dep 1, lazylistFromList [(s2, bs2, defer2)])]
(* Maps a logic represented by the type "functors" to the corresponding
@@ -516,6 +710,7 @@ let mkRule_Fusion sort bs sl : stateExpander =
let getExpandingFunctionProducer = function
| MultiModalK -> mkRule_MultiModalK
| MultiModalKD -> mkRule_MultiModalKD
+ | Monotone -> mkRule_Monotone
| CoalitionLogic -> mkRule_CL
| GML -> mkRule_GML
| PML -> mkRule_PML
diff --git a/src/lib/CoAlgLogics.mli b/src/lib/CoAlgLogics.mli
index 48d0958b68bceec89898bf9788866dea0e7084bc..dd5c9ad4230fb0ae152217bd8b8c7cf9755e113d 100644
--- a/src/lib/CoAlgLogics.mli
+++ b/src/lib/CoAlgLogics.mli
@@ -6,4 +6,4 @@
open CoAlgMisc
-val getExpandingFunctionProducer : functors -> sort -> bset -> sort list -> stateExpander
+val getExpandingFunctionProducer : functors -> sort -> bset -> bset -> sort list -> stateExpander
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 00174a7c1a4c4a9518f6ab32158a486331613bbb..85d08bcabeaf8f13ceba5442f5eaa76fa0ac5440 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -21,6 +21,17 @@ module BsSet = Set.Make(
(** An instantiation of a hash table (of the standard library) for bitsets.
*)
module GHt = Hashtbl.Make(
+ struct
+ type t = S.bitset * S.bitset
+ let equal ((bs1l, bs1r) : t) (bs2l, bs2r) =
+ (S.compareBS bs1l bs2l = 0) && (S.compareBS bs1r bs2r = 0)
+ let hash ((bsl, bsr) : t) = (S.hashBS bsl) lxor (S.hashBS bsr)
+ end
+ )
+
+(** An instantiation of a hash table (of the standard library) for bitsets.
+ *)
+module GHtS = Hashtbl.Make(
struct
type t = S.bitset
let equal (bs1 : t) bs2 = S.compareBS bs1 bs2 = 0
@@ -68,6 +79,7 @@ module NHt = Hashtbl.Make(
type functors =
| MultiModalK
| MultiModalKD
+ | Monotone
| CoalitionLogic
| GML
| PML
@@ -89,6 +101,7 @@ type functorName =
let unaryfunctor2name : (functorName*string) list =
[ (NPa MultiModalK , "MultiModalK")
; (NPa MultiModalKD , "MultiModalKD")
+ ; (NPa Monotone , "Monotone")
; (NPa GML , "GML")
; (NPa PML , "PML")
; (NPa CoalitionLogic , "CoalitionLogic")
@@ -165,6 +178,8 @@ type formulaType =
| NormnF (* negation normal form of default implication *)
| ChcF (* Choice *)
| FusF (* Fusion *)
+ | MuF
+ | NuF
type localFormula = int
type bset = S.bitset
@@ -182,6 +197,7 @@ type state = { sortS : sort;
modalities (TODO: also @-formulas?).
the state is satisfiable if /\bsS is satisfiable.
*)
+ mutable deferralS : bset; (* which formulas still have deferrals *)
mutable statusS : nodeStatus;
mutable parentsS : core list; mutable childrenS : (dependencies * core list) list;
mutable constraintsS : csetSet; expandFkt : stateExpander;
@@ -191,11 +207,12 @@ and core = { (* for details, see documentation of newCore *)
sortC : sort;
mutable bsC : bset; (* a set of arbitrary formulas.
the present core is satisfiable if /\ bsC is satisfiable *)
+ mutable deferralC : bset; (* which formulas still have deferrals *)
mutable statusC : nodeStatus;
mutable parentsC : (state * int) list;
mutable childrenC : state list;
mutable constraintsC : csetSet;
- solver : Minisat.solver; (* a solver to find satisfying assignemnts for bsC.
+ mutable solver : Minisat.solver option; (* a solver to find satisfying assignemnts for bsC.
the solver returns "satisfiable" iff
there is a satisfying assignment of
bsC which is not represented by some state from the
@@ -211,7 +228,7 @@ and setState = state GHt.t array
and setCore = core GHt.t array
-and setCnstr = unit GHt.t
+and setCnstr = unit GHtS.t
(*****************************************************************************)
@@ -231,9 +248,17 @@ and nodeStatus =
| Sat
| Unsat
+(* In K, given the singleton list [bs] returns the list of all Ax'es
+ responsible for the individual members of bs being part of the core
+ as well as the Ex.
+
+ So given the state { <>φ , []ψ , []η } and the core { φ , ψ , η },
+ dependency would map { η } to { <>φ , []η } and { ψ } to { <>φ , []ψ }
+*)
and dependencies = bset list -> bset
-and rule = (dependencies * (sort * bset) lazylist)
+(* Note: sort * bset * bset is to be read as sort * formulas_in_core * deferrals_in_core *)
+and rule = (dependencies * (sort * bset * bset) lazylist)
and 'a lazyliststep =
| MultipleElements of 'a list
@@ -336,6 +361,7 @@ let queueCores1 = ref ([] : core list)
let queueCores2 = ref ([] : core list)
let queueCnstrs = ref ([] : cset list)
let doPropagation = ref false
+let doPropagationCounter = ref 0
let queueInit () =
queueStates := [];
@@ -352,7 +378,7 @@ let queueInsertState state = queueStates := state::!queueStates
(* original version: breadth-first *)
let queueInsertCore core = queueCores2 := core::!queueCores2
-(* experiment: depth first
+(* experiment: depth first
let queueInsertCore core = queueCores1 := core::!queueCores1
*)
@@ -381,10 +407,19 @@ let queueGetElement () =
let doNominalPropagation () = !doPropagation
+let setPropagationCounter count =
+ doPropagationCounter := count
+
let doSatPropagation () =
- let res = !doPropagation in
- doPropagation := false;
- res
+ if !doPropagationCounter == 0
+ then true
+ else begin
+ doPropagationCounter := !doPropagationCounter - 1;
+ false
+ end
+ (* let res = !doPropagation in *)
+ (* doPropagation := false; *)
+ (* res *)
(*****************************************************************************)
(* "Module type" and a specific implementation of the graph *)
@@ -392,14 +427,14 @@ let doSatPropagation () =
let graphStates = ref (Array.make 0 (GHt.create 0 : state GHt.t))
let graphCores = ref (Array.make 0 (GHt.create 0 : core GHt.t))
-let graphCnstrs = ref (GHt.create 0 : constrnt GHt.t)
+let graphCnstrs = ref (GHtS.create 0 : constrnt GHtS.t)
let graphRoot = ref (None : core option)
let graphInit () =
let size = Array.length !sortTable in
graphStates := Array.init size (fun _ -> GHt.create 128);
graphCores := Array.init size (fun _ -> GHt.create 128);
- graphCnstrs := GHt.create 128;
+ graphCnstrs := GHtS.create 128;
graphRoot := None
let graphIterStates fkt =
@@ -408,18 +443,18 @@ let graphIterStates fkt =
let graphIterCores fkt =
Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphCores
-let graphIterCnstrs fkt = GHt.iter fkt !graphCnstrs
+let graphIterCnstrs fkt = GHtS.iter fkt !graphCnstrs
let graphClearCnstr () =
- let newGraph = GHt.create (GHt.length !graphCnstrs) in
+ let newGraph = GHtS.create (GHtS.length !graphCnstrs) in
let copyCnstr cset cnstr =
match cnstr with
| UnsatC
- | SatC -> GHt.add newGraph cset cnstr
- | OpenC _ -> GHt.add newGraph cset (OpenC [])
- | UnexpandedC _ -> GHt.add newGraph cset (UnexpandedC [])
+ | SatC -> GHtS.add newGraph cset cnstr
+ | OpenC _ -> GHtS.add newGraph cset (OpenC [])
+ | UnexpandedC _ -> GHtS.add newGraph cset (UnexpandedC [])
in
- GHt.iter copyCnstr !graphCnstrs;
+ GHtS.iter copyCnstr !graphCnstrs;
graphCnstrs := newGraph
let graphFindState sort bs =
@@ -434,7 +469,7 @@ let graphFindCore sort bs =
let graphFindCnstr cset =
try
- Some (GHt.find !graphCnstrs cset)
+ Some (GHtS.find !graphCnstrs cset)
with Not_found -> None
let graphInsertState sort bs state =
@@ -446,17 +481,17 @@ let graphInsertCore sort bs core =
GHt.add !graphCores.(sort) bs core
let graphInsertCnstr cset cnstr =
- assert (not (GHt.mem !graphCnstrs cset));
- GHt.add !graphCnstrs cset cnstr
+ assert (not (GHtS.mem !graphCnstrs cset));
+ GHtS.add !graphCnstrs cset cnstr
let graphReplaceCnstr cset cnstr =
- GHt.replace !graphCnstrs cset cnstr
+ GHtS.replace !graphCnstrs cset cnstr
let graphSizeState () =
Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphStates
let graphSizeCore () =
Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphCores
-let graphSizeCnstr () = GHt.length !graphCnstrs
+let graphSizeCnstr () = GHtS.length !graphCnstrs
let graphAddRoot core =
if !graphRoot = None then graphRoot := Some core
@@ -493,14 +528,16 @@ let nextNodeIdx () : int =
nodeCounter := oldVal + 1;
oldVal
-let stateMake sort bs exp =
- { sortS = sort; bsS = bs; statusS = Expandable; parentsS = []; childrenS = [];
+let stateMake sort bs defer exp =
+ { sortS = sort; bsS = bs; deferralS = defer; statusS = Expandable; parentsS = []; childrenS = [];
constraintsS = cssEmpty; expandFkt = exp;
idx = nextNodeIdx()
}
let stateGetSort state = state.sortS
let stateGetBs state = state.bsS
let stateSetBs state bs = state.bsS <- bs
+let stateGetDeferral state = state.deferralS
+let stateSetDeferral state bs = state.deferralS <- bs
let stateGetStatus state = state.statusS
let stateSetStatus state status = state.statusS <- status
let stateGetParents state = state.parentsS
@@ -520,14 +557,16 @@ let stateGetIdx (state:state) = state.idx
(* "Module type" and a specific implementation of core nodes *)
(*****************************************************************************)
-let coreMake sort bs solver fht =
- { sortC = sort; bsC = bs; statusC = Expandable; parentsC = []; childrenC = [];
+let coreMake sort bs defer solver fht =
+ { sortC = sort; bsC = bs; deferralC = defer; statusC = Expandable; parentsC = []; childrenC = [];
constraintsC = cssEmpty; solver = solver; fht = fht; constraintParents = [];
idx = nextNodeIdx()
}
let coreGetSort core = core.sortC
let coreGetBs core = core.bsC
let coreSetBs core bs = core.bsC <- bs
+let coreGetDeferral core = core.deferralC
+let coreSetDeferral core bs = core.deferralC <- bs
let coreGetStatus core = core.statusC
let coreSetStatus core status = core.statusC <- status
let coreGetParents core = core.parentsC
@@ -537,6 +576,7 @@ let coreAddChild core child = core.childrenC <- child::core.childrenC
let coreGetConstraints core = core.constraintsC
let coreSetConstraints core csets = core.constraintsC <- csets
let coreGetSolver core = core.solver
+let coreDeallocateSolver core = core.solver <- None; FHt.reset core.fht
let coreGetFht core = core.fht
let coreGetIdx (core:core) = core.idx
let coreGetConstraintParents core = core.constraintParents
@@ -551,19 +591,29 @@ let coreAddConstraintParent core cset =
let setEmptyState () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128)
let setEmptyCore () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128)
-let setEmptyCnstr () = GHt.create 128
-let setAddState set state = GHt.add set.(stateGetSort state) (stateGetBs state) state
-let setAddCore set core = GHt.add set.(coreGetSort core) (coreGetBs core) core
-let setAddCnstr set cset = GHt.add set cset ()
-let setMemState set state = GHt.mem set.(stateGetSort state) (stateGetBs state)
-let setMemCore set core = GHt.mem set.(coreGetSort core) (coreGetBs core)
-let setMemCnstr set cset = GHt.mem set cset
-let setRemoveState set state = GHt.remove set.(stateGetSort state) (stateGetBs state)
-let setRemoveCore set core = GHt.remove set.(coreGetSort core) (coreGetBs core)
-let setRemoveCnstr set cset = GHt.remove set cset
+let setCopyState set = Array.init (Array.length !sortTable) (fun idx -> GHt.copy set.(idx))
+let setCopyCore set = Array.init (Array.length !sortTable) (fun idx -> GHt.copy set.(idx))
+let setEmptyCnstr () = GHtS.create 128
+let setAddState set state =
+ GHt.add set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state)) state
+let setAddCore set core =
+ GHt.add set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core)) core
+let setAddCnstr set cset = GHtS.add set cset ()
+let setMemState set state =
+ GHt.mem set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state))
+let setMemCore set core =
+ GHt.mem set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core))
+let setMemCnstr set cset = GHtS.mem set cset
+let setRemoveState set state =
+ GHt.remove set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state))
+let setRemoveCore set core =
+ GHt.remove set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core))
+let setRemoveCnstr set cset = GHtS.remove set cset
let setIterState fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set
let setIterCore fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set
-let setIterCnstr fkt set = GHt.iter (fun cset () -> fkt cset) set
+let setIterCnstr fkt set = GHtS.iter (fun cset () -> fkt cset) set
+let setLengthState seta = Array.fold_left (fun acc set -> acc + GHt.length set) 0 seta
+let setLengthCore seta = Array.fold_left (fun acc set -> acc + GHt.length set) 0 seta
(*****************************************************************************)
@@ -605,6 +655,7 @@ let bsetMake () = S.makeBS ()
let bsetAdd bs lf = S.addBSNoChk bs lf
let bsetMem bs lf = S.memBS bs lf
let bsetRem bs lf = S.remBS bs lf
+let bsetCompare bs1 bs2 = S.compareBS bs1 bs2
let bsetMakeRealEmpty () =
let res = bsetMake () in
bsetRem res !S.bstrue; (* remove bstrue which is initially in an empty bset *)
@@ -664,6 +715,7 @@ let arrayNeg = ref (Array.make 0 (Array.make 0 (-1)))
let arrayDest1 = ref (Array.make 0 (Array.make 0 (-1))) (* first subformula *)
let arrayDest2 = ref (Array.make 0 (Array.make 0 (-1))) (* second subformula *)
let arrayDest3 = ref (Array.make 0 (Array.make 0 (-1))) (* a role *)
+let arrayDeferral = ref (Array.make 0 (Array.make 0 (-1))) (* deferral at point *)
let arrayDestNum = ref (Array.make 0 (Array.make 0 (-1))) (* an integer *)
let arrayDestNum2 = ref (Array.make 0 (Array.make 0 (-1))) (* another integer *)
let arrayDestAg = ref (Array.make 0 (Array.make 0 [|0|])) (* arrays of agents *)
@@ -677,6 +729,7 @@ let lfGetType sort f = !arrayType.(sort).(f)
let lfGetDest1 sort f = !arrayDest1.(sort).(f)
let lfGetDest2 sort f = !arrayDest2.(sort).(f)
let lfGetDest3 sort f = !arrayDest3.(sort).(f)
+let lfGetDeferral sort f = !arrayDeferral.(sort).(f)
let lfGetDestNum sort f = !arrayDestNum.(sort).(f)
let lfGetDestNum2 sort f = !arrayDestNum2.(sort).(f)
let lfGetDestAg sort f = !arrayDestAg.(sort).(f)
@@ -689,6 +742,11 @@ let lfToInt lf = lf
let lfFromInt num = num
let lfGetFormula sort f = !arrayFormula.(sort).(f)
+let escapeHtml (input : string) : string =
+ List.fold_right (fun (x, y) (str : string) -> Str.global_replace (Str.regexp x) y str)
+ [("<", "<") ; (">", ">") ; ("&", "&")]
+ input
+
let bsetToString sort bset : string =
let toFormula (lf:localFormula) (lst: string list) : string list =
let formula: C.formula = lfGetFormula sort lf in
@@ -699,7 +757,7 @@ let bsetToString sort bset : string =
let csetToString sort cset = bsetToString sort cset
-let coreToString core =
+let coreToString (core:core): string =
let helper cset lst : string list =
(csetToString core.sortC cset):: lst
in
@@ -713,6 +771,8 @@ let coreToString core =
"Core "^(string_of_int core.idx)^" {\n"^
" Status: " ^ (nodeStatusToString core.statusC) ^ "\n"^
" " ^ bsetToString core.sortC core.bsC ^ "\n" ^
+ " Deferrals: \n" ^
+ " " ^ bsetToString core.sortC core.deferralC ^ "\n" ^
" Constraints: { "^(String.concat
"\n " constraints)^" }\n"^
" Children: { "^(String.concat
@@ -741,6 +801,8 @@ let stateToString (state:state): string =
"State "^(string_of_int state.idx)^" {\n"^
" Status: " ^ (nodeStatusToString state.statusS) ^ "\n"^
" " ^ bsetToString state.sortS state.bsS ^ "\n" ^
+ " Deferrals: \n" ^
+ " " ^ bsetToString state.sortS state.deferralS ^ "\n" ^
" Constraints: { "^(String.concat
"\n " constraints)^" }\n"^
" Children: { "^(String.concat
@@ -748,6 +810,60 @@ let stateToString (state:state): string =
" Parents: { "^(String.concat ", " parents)^" }\n"^
"}"
+let stateToDot (state:state): string =
+ let color = match state.statusS with
+ | Sat -> "green"
+ | Unsat -> "red"
+ | Open -> "yellow"
+ | Expandable -> "white"
+ in
+ let toFormula (lf:localFormula) (lst: string list) : string list =
+ let formula: C.formula = lfGetFormula state.sortS lf in
+ if (bsetMem state.deferralS lf)
+ then ("<B>"^(escapeHtml (C.string_of_formula formula))^"</B>") :: lst
+ else (escapeHtml (C.string_of_formula formula)) :: lst
+ in
+ let formulaList = bsetFold toFormula state.bsS [] in
+ let ownidx = (string_of_int state.idx) in
+ let parents =
+ List.map (fun (co:core) ->
+ "Node"^string_of_int co.idx^" -> Node"^ownidx^";")
+ state.parentsS
+ in
+ "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color
+ ^ ",label=<State " ^ ownidx
+ ^ "<BR/>" ^ (String.concat "<BR/>" formulaList)
+ ^ ">];\n"
+ ^ (String.concat "\n" parents)
+
+
+let coreToDot (core:core): string =
+ let color = match core.statusC with
+ | Sat -> "green"
+ | Unsat -> "red"
+ | Open -> "yellow"
+ | Expandable -> "white"
+ in
+ let toFormula (lf:localFormula) (lst: string list) : string list =
+ let formula: C.formula = lfGetFormula core.sortC lf in
+ if (bsetMem core.deferralC lf)
+ then ("<B>"^(escapeHtml (C.string_of_formula formula))^"</B>") :: lst
+ else (escapeHtml (C.string_of_formula formula)) :: lst
+ in
+ let formulaList = bsetFold toFormula core.bsC [] in
+ let ownidx = (string_of_int core.idx) in
+ let parents =
+ List.map (fun (st,_:state*int) ->
+ "Node"^string_of_int st.idx^" -> Node"^ownidx^";")
+ core.parentsC
+ in
+ "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color
+ ^ ",label=<Core " ^ ownidx
+ ^ "<BR/>" ^ (String.concat "<BR/>" formulaList)
+ ^ ">];\n"
+ ^ (String.concat "\n" parents)
+
+
let queuePrettyStatus () =
let printList (sl : int list) : string =
String.concat ", " (List.map string_of_int sl)
@@ -774,19 +890,33 @@ let atFormulaGetNominal f =
let lfToAt _ lf = lf
+(* Calculate all possible formulae. This includes all subformulae and
+ in the case of μ-Calculus the Fischer-Ladner closure.
-let rec detClosure nomTbl hcF fset atset nomset s f =
+ TODO: variable sort needs to match epected sort
+ *)
+let rec detClosure vars nomTbl hcF fset vset atset nomset s f =
+ let newvars = List.filter (fun (x) -> C.hc_freeIn x f) vars in
+ let detClosure_ = detClosure newvars in
+ let deferral = if List.length newvars > 0
+ then (List.hd newvars)
+ else "ε" in
if s < 0 || s >= Array.length fset then
let sstr = string_of_int s in
raise (C.CoAlgException ("Invalid sort (i.e. sort out of range): " ^ sstr))
else ();
- if C.HcFHt.mem fset.(s) f then ()
+ if C.HcFHt.mem vset.(s) f &&
+ (compare (C.HcFHt.find vset.(s) f) deferral = 0 ||
+ compare deferral "ε" = 0)
+ then ()
else
+ let () = C.HcFHt.add vset.(s) f deferral in
let () = C.HcFHt.add fset.(s) f () in
let (func, sortlst) = !sortTable.(s) in
match f.HC.node with
| C.HCTRUE
- | C.HCFALSE -> ()
+ | C.HCFALSE
+ | C.HCVAR _ -> ()
| C.HCAP name ->
if C.isNominal name then begin
Hashtbl.replace nomset name s;
@@ -808,37 +938,37 @@ let rec detClosure nomTbl hcF fset atset nomset s f =
| Some sort -> sort
in
let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in
- detClosure nomTbl hcF fset atset nomset s1 hcnom;
- detClosure nomTbl hcF fset atset nomset s1 f1
+ detClosure_ nomTbl hcF fset vset atset nomset s1 hcnom;
+ detClosure_ nomTbl hcF fset vset atset nomset s1 f1
| C.HCOR (f1, f2)
| C.HCAND (f1, f2) ->
- detClosure nomTbl hcF fset atset nomset s f1;
- detClosure nomTbl hcF fset atset nomset s f2
+ detClosure_ nomTbl hcF fset vset atset nomset s f1;
+ detClosure_ nomTbl hcF fset vset atset nomset s f2
| C.HCEX (_, f1)
| C.HCAX (_, f1) ->
- if (func <> MultiModalK && func <> MultiModalKD)
+ if (func <> MultiModalK && func <> MultiModalKD && func <> Monotone)
|| List.length sortlst <> 1
then raise (C.CoAlgException "Ex/Ax-formula is used in wrong sort.")
else ();
- detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1
+ detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
| C.HCENFORCES (_, f1)
| C.HCALLOWS (_, f1) ->
if func <> CoalitionLogic || List.length sortlst <> 1
then raise (C.CoAlgException "[{Agents}]-formula is used in wrong sort.")
else ();
- detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1
+ detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
| C.HCMORETHAN (_,_,f1)
| C.HCMAXEXCEPT (_,_,f1) ->
if func <> GML || List.length sortlst <> 1
then raise (C.CoAlgException "[{>=,<=}]-formula is used in wrong sort.")
else ();
- detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1
+ detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
| C.HCATLEASTPROB (_,f1)
| C.HCLESSPROBFAIL (_,f1) ->
if func <> PML || List.length sortlst <> 1
then raise (C.CoAlgException "[{>=,<}]-formula with probability is used in wrong sort.")
else ();
- detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1;
+ detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1;
(*
TODO: add ¬ f1 to the closure!
detClosure nomTbl hcF fset atset nomset (List.hd sortlst) (f1.HC.node.negNde)
@@ -861,28 +991,45 @@ let rec detClosure nomTbl hcF fset atset nomset s f =
then raise (C.CoAlgException "Identity operator applied to
formula of wrong sort.")
else ();
- detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1;
+ detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1;
| C.HCNORM (f1, f2)
| C.HCNORMN(f1, f2) ->
if func <> DefaultImplication || List.length sortlst <> 1 then
raise (C.CoAlgException "Default Implication applied to
formulae of wrong sort.")
else ();
- detClosure nomTbl hcF fset atset nomset (List.nth sortlst 0) f1;
- detClosure nomTbl hcF fset atset nomset (List.nth sortlst 1) f2
+ detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 0) f1;
+ detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 1) f2
| C.HCCHC (f1, f2) ->
if func <> Choice || List.length sortlst <> 2 then
raise (C.CoAlgException "Choice formula is used in wrong sort.")
else ();
- detClosure nomTbl hcF fset atset nomset (List.nth sortlst 0) f1;
- detClosure nomTbl hcF fset atset nomset (List.nth sortlst 1) f2
+ detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 0) f1;
+ detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 1) f2
| C.HCFUS (first, f1) ->
if func <> Fusion || List.length sortlst <> 2 then
raise (C.CoAlgException "Fusion formula is used in wrong sort.")
else ();
let s1 = List.nth sortlst (if first then 0 else 1) in
- detClosure nomTbl hcF fset atset nomset s1 f1
+ detClosure_ nomTbl hcF fset vset atset nomset s1 f1
+ (*
+ FL(μ X . φ) = {μ X . φ} ∪ FL(φ[X|->μ X . φ])
+ *)
+ | C.HCMU (name, f1) ->
+ begin
+ if C.hc_freeIn name f1
+ then
+ C.HcFHt.replace vset.(s) f name
+ else ();
+ let unfold = C.hc_replace hcF name f f1 in
+ let appendvars = List.append newvars [name] in
+ detClosure appendvars nomTbl hcF fset vset atset nomset s unfold
+ end
+ | C.HCNU (name, f1) ->
+ let unfold = C.hc_replace hcF name f f1 in
+ detClosure_ nomTbl hcF fset vset atset nomset s unfold
+
let detClosureAt hcF atset name f () =
match f.HC.node with
@@ -892,13 +1039,14 @@ let detClosureAt hcF atset name f () =
| C.HCAND _
| C.HCAT _ -> ()
| _ ->
- let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in
+ let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in
C.HcFHt.replace atset at ()
(** Initialises the arrays for a formula and its integer representation.
*)
-let initTables nomTbl hcF htF htR s f n =
+let initTables nomTbl hcF htF htR vset s f n =
!arrayFormula.(s).(n) <- f.HC.fml;
+ !arrayDeferral.(s).(n) <- Hashtbl.hash (C.HcFHt.find vset.(s) f);
let fneg = f.HC.neg in
if C.HcFHt.mem htF.(s) fneg then !arrayNeg.(s).(n) <- C.HcFHt.find htF.(s) fneg;
let (_, sortlst) = !sortTable.(s) in
@@ -928,10 +1076,10 @@ let initTables nomTbl hcF htF htR s f n =
!arrayType.(s).(n) <- AndF;
!arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) f1;
!arrayDest2.(s).(n) <- C.HcFHt.find htF.(s) f2
- | C.HCEX (role, f1) ->
+ | C.HCEX (role, f1) ->
!arrayType.(s).(n) <- ExF;
!arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
- !arrayDest3.(s).(n) <-
+ !arrayDest3.(s).(n) <-
if Hashtbl.mem htR role then Hashtbl.find htR role
else
let size = Hashtbl.length htR in
@@ -1013,11 +1161,11 @@ let initTables nomTbl hcF htF htR s f n =
| C.HCID (f1) ->
!arrayType.(s).(n) <- IdF;
!arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1
- | C.HCNORM (f1, f2) ->
+ | C.HCNORM (f1, f2) ->
!arrayType.(s).(n) <- NormF;
!arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1;
!arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2
- | C.HCNORMN (f1, f2) ->
+ | C.HCNORMN (f1, f2) ->
!arrayType.(s).(n) <- NormnF;
!arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1;
!arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2
@@ -1031,6 +1179,16 @@ let initTables nomTbl hcF htF htR s f n =
let s1 = List.nth sortlst (if first then 0 else 1) in
!arrayDest1.(s).(n) <- C.HcFHt.find htF.(s1) f1;
!arrayDest3.(s).(n) <- if first then 0 else 1
+ | C.HCMU (name, f1) ->
+ !arrayType.(s).(n) <- MuF;
+ let unfold = C.hc_replace hcF name f f1 in
+ !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) unfold
+ | C.HCNU (name, f1) ->
+ !arrayType.(s).(n) <- NuF;
+ let unfold = C.hc_replace hcF name f f1 in
+ !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) unfold
+ | C.HCVAR _ -> !arrayType.(s).(n) <- Other
+
let initTablesAt hcF htF name sort =
let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in
@@ -1043,7 +1201,7 @@ let initTablesAt hcF htF name sort =
| C.HCAND _
| C.HCAT _ -> ()
| _ ->
- let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in
+ let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in
let atn = C.HcFHt.find htF.(0) at in
FHt.add !arrayAt.(sort).(n) nom atn
in
@@ -1054,6 +1212,7 @@ let ppFormulae nomTbl tbox (s, f) =
if card <= 0 then
raise (C.CoAlgException "Number of sorts must be positive.")
else ();
+ C.verifyFormula f;
let nnfAndSimplify f = C.simplify (C.nnf f) in
let f1 = nnfAndSimplify f in
let nf1 = nnfAndSimplify (C.NOT f) in
@@ -1069,16 +1228,19 @@ let ppFormulae nomTbl tbox (s, f) =
let hctrue = C.hc_formula hcF C.TRUE in
let fset = Array.init card (fun _ -> C.HcFHt.create 128) in
+ let vset = Array.init card (fun _ -> C.HcFHt.create 128) in
let atset = C.HcFHt.create 64 in
let nomset = Hashtbl.create 16 in
for i = 0 to card-1 do
- detClosure nomTbl hcF fset atset nomset i hcfalse;
- detClosure nomTbl hcF fset atset nomset i hctrue;
+ detClosure [] nomTbl hcF fset vset atset nomset i hcfalse;
+ detClosure [] nomTbl hcF fset vset atset nomset i hctrue;
done;
- detClosure nomTbl hcF fset atset nomset s hcf;
- detClosure nomTbl hcF fset atset nomset s nhcf;
- List.iter (fun (s, f) -> detClosure nomTbl hcF fset atset nomset s f) hctbox;
- List.iter (fun (s, f) -> detClosure nomTbl hcF fset atset nomset s f) nhctbox;
+ detClosure [] nomTbl hcF fset vset atset nomset s hcf;
+ detClosure [] nomTbl hcF fset vset atset nomset s nhcf;
+ List.iter (fun (s, f) -> detClosure [] nomTbl hcF fset vset atset nomset s f)
+ hctbox;
+ List.iter (fun (s, f) -> detClosure [] nomTbl hcF fset vset atset nomset s f)
+ nhctbox;
Hashtbl.iter (fun n s -> C.HcFHt.iter (detClosureAt hcF atset n) fset.(s)) nomset;
let htF = Array.init card (fun _ -> C.HcFHt.create 128) in
@@ -1111,12 +1273,13 @@ let ppFormulae nomTbl tbox (s, f) =
arrayDest1 := Array.init card (fun _ -> Array.make !size (-1));
arrayDest2 := Array.init card (fun _ -> Array.make !size (-1));
arrayDest3 := Array.init card (fun _ -> Array.make !size (-1));
+ arrayDeferral := Array.init card (fun _-> Array.make !size(-1));
arrayNeg := Array.init card (fun _ -> Array.make !size (-1));
arrayDestNum := Array.init card (fun _ -> Array.make !size (-1));
arrayDestNum2 := Array.init card (fun _ -> Array.make !size (-1));
arrayDestAg := Array.init card (fun _ -> Array.make !size (Array.make 0 (-1)));
let htR = Hashtbl.create 128 in
- Array.iteri (fun s ht -> C.HcFHt.iter (initTables nomTbl hcF htF htR s) ht) htF;
+ Array.iteri (fun s ht -> C.HcFHt.iter (initTables nomTbl hcF htF htR vset s) ht) htF;
arrayAt := Array.init card (fun _ -> Array.init !size (fun _ -> FHt.create 8));
Hashtbl.iter (initTablesAt hcF htF) nomset;
diff --git a/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli
index b248c1803ae99d5a4f41a70706d765ed5399acaa..b93b94ea1a0798dbcabcf1447a2549b1145c1841 100644
--- a/src/lib/CoAlgMisc.mli
+++ b/src/lib/CoAlgMisc.mli
@@ -12,6 +12,7 @@
type functors =
| MultiModalK
| MultiModalKD
+ | Monotone
| CoalitionLogic
| GML
| PML
@@ -52,6 +53,8 @@ type formulaType =
| NormnF (* negation normal form of default implication *)
| ChcF
| FusF
+ | MuF
+ | NuF
type localFormula
type bset
@@ -93,7 +96,7 @@ and nodeStatus =
and dependencies = bset list -> bset
-and rule = (dependencies * (sort * bset) lazylist)
+and rule = (dependencies * (sort * bset * bset) lazylist)
and 'a lazyliststep =
| MultipleElements of 'a list
@@ -165,6 +168,7 @@ val queueInsertCnstr : cset -> unit
val queueGetElement : unit -> queueElement
val queuePrettyStatus : unit -> string
+val setPropagationCounter : int -> unit
val doNominalPropagation : unit -> bool
val doSatPropagation : unit -> bool
@@ -178,11 +182,11 @@ val graphIterStates : (state -> unit) -> unit
val graphIterCores : (core -> unit) -> unit
val graphIterCnstrs : (cset -> constrnt -> unit) -> unit
val graphClearCnstr : unit -> unit
-val graphFindState : sort -> bset -> state option
-val graphFindCore : sort -> bset -> core option
+val graphFindState : sort -> (bset * bset) -> state option
+val graphFindCore : sort -> (bset * bset) -> core option
val graphFindCnstr : cset -> constrnt option
-val graphInsertState : sort -> bset -> state -> unit
-val graphInsertCore : sort -> bset -> core -> unit
+val graphInsertState : sort -> (bset * bset) -> state -> unit
+val graphInsertCore : sort -> (bset * bset) -> core -> unit
val graphInsertCnstr : cset -> constrnt -> unit
val graphReplaceCnstr : cset -> constrnt -> unit
val graphSizeState : unit -> int
@@ -210,10 +214,12 @@ val cssIter : (cset -> unit) -> csetSet -> unit
(* "Module type" and a specific implementation of state nodes *)
(*****************************************************************************)
-val stateMake : sort -> bset -> stateExpander -> state
+val stateMake : sort -> bset -> bset -> stateExpander -> state
val stateGetSort : state -> sort
val stateGetBs : state -> bset
val stateSetBs : state -> bset -> unit
+val stateGetDeferral : state -> bset
+val stateSetDeferral : state -> bset -> unit
val stateGetStatus : state -> nodeStatus
val stateSetStatus : state -> nodeStatus -> unit
val stateGetParents : state -> core list
@@ -225,6 +231,7 @@ val stateGetConstraints : state -> csetSet
val stateSetConstraints : state -> csetSet -> unit
val stateNextRule : state -> ruleEnumeration
val stateToString : state -> string
+val stateToDot : state -> string
val stateGetIdx : state -> int
@@ -232,24 +239,28 @@ val stateGetIdx : state -> int
(* "Module type" and a specific implementation of core nodes *)
(*****************************************************************************)
-val coreMake : sort -> bset -> Minisat.solver -> fht -> core
+val coreMake : sort -> bset -> bset -> Minisat.solver option -> fht -> core
val coreGetSort : core -> sort
val coreGetBs : core -> bset
-val coreSetBs :core -> bset -> unit
+val coreSetBs : core -> bset -> unit
+val coreGetDeferral : core -> bset
+val coreSetDeferral : core -> bset -> unit
val coreGetStatus : core -> nodeStatus
val coreSetStatus : core -> nodeStatus -> unit
-val coreGetParents :core -> (state * int) list
+val coreGetParents : core -> (state * int) list
val coreAddParent : core -> state -> int -> unit
val coreGetChildren : core -> state list
val coreAddChild : core -> state -> unit
val coreGetConstraints : core -> csetSet
val coreSetConstraints : core -> csetSet -> unit
-val coreGetSolver : core -> Minisat.solver
+val coreGetSolver : core -> Minisat.solver option
+val coreDeallocateSolver : core -> unit
val coreGetFht : core -> fht
val coreGetIdx : core -> int
val coreGetConstraintParents : core -> cset list
val coreAddConstraintParent : core -> cset -> unit
val coreToString : core -> string
+val coreToDot : core -> string
(*****************************************************************************)
@@ -259,6 +270,8 @@ val coreToString : core -> string
val setEmptyState : unit -> setState
val setEmptyCore : unit -> setCore
+val setCopyState : setState -> setState
+val setCopyCore : setCore -> setCore
val setEmptyCnstr : unit -> setCnstr
val setAddState : setState -> state -> unit
val setAddCore : setCore -> core -> unit
@@ -272,6 +285,8 @@ val setRemoveCnstr : setCnstr -> cset -> unit
val setIterState : (state -> unit) -> setState -> unit
val setIterCore : (core -> unit) -> setCore -> unit
val setIterCnstr : (cset -> unit) -> setCnstr -> unit
+val setLengthState : setState -> int
+val setLengthCore : setCore -> int
(*****************************************************************************)
@@ -303,6 +318,8 @@ val bsetMake : unit -> bset (* a new bset which only contains True *)
val bsetMakeRealEmpty : unit -> bset (* a new bset without containing True *)
val bsetAdd : bset -> localFormula -> unit
val bsetMem : bset -> localFormula -> bool
+val bsetRem : bset -> int -> unit
+val bsetCompare : bset -> bset -> int
val bsetFold : (localFormula -> 'a -> 'a) -> bset -> 'a -> 'a
val bsetIter : (localFormula -> unit) -> bset -> unit
val bsetFilter : bset -> (localFormula -> bool) -> bset
@@ -331,6 +348,7 @@ val lfGetType : sort -> localFormula -> formulaType
val lfGetDest1 : sort -> localFormula -> localFormula
val lfGetDest2 : sort -> localFormula -> localFormula
val lfGetDest3 : sort -> localFormula -> int
+val lfGetDeferral : sort -> localFormula -> int
val lfGetDestNum : sort -> localFormula -> int
val lfGetDestNum2 : sort -> localFormula -> int
val lfGetDestAg : sort -> localFormula -> int array
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 034d6f28aaa58d987c006800f77557d6ed23fde7..efb1734a8702628fdb1be1267005b5adcbb0d522 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -27,11 +27,12 @@ let propSatFindSucc setCnstr cset =
if csetHasDot cset then false
else
match graphFindCnstr cset with
- | None -> raise (ReasonerError "?")
- | Some SatC -> true
- | Some (OpenC _) -> setMemCnstr setCnstr cset
- | Some (UnexpandedC _)
- | Some UnsatC -> false
+ | None -> raise (ReasonerError "?")
+ | Some SatC -> true
+ | Some (OpenC _) -> setMemCnstr setCnstr cset
+ | Some (UnexpandedC _)
+ | Some UnsatC -> false
+
let rec propSat setStates setCores setCnstr = function
| [] -> ()
@@ -112,6 +113,160 @@ let propagateSat () =
setIterCnstr (fun cset -> graphReplaceCnstr cset SatC) setCnstr
+let propagateSatMu () =
+ let setFinishingStates = setEmptyState () in
+ let setFinishingCores = setEmptyCore () in
+ let setStates = setEmptyState () in
+ let setCores = setEmptyCore () in
+ let emptySet = bsetMakeRealEmpty () in
+ let openstates = ref 0 in
+
+ (* Collect two sets of nodes. All nodes that may be satisfiable
+ * after this iteration are collected into setStates/setCores.
+ *
+ * As every cycle containing a node with empty focus or an
+ * satisfiable node should be considered satisfiable, collect these
+ * decisive nodes into setFinishingStates/setFinishingCores
+ *
+ * This also marks in trivial cases nodes as satisfiable.
+ *)
+ let stateCollector state =
+ match stateGetStatus state with
+ | Unsat -> ()
+ | Sat ->
+ setAddState setStates state;
+ setAddState setFinishingStates state
+ | Expandable -> ()
+ | Open ->
+ openstates := !openstates + 1;
+ if List.length (stateGetRules state) == 0 || (* States with no rules are satisfiable *)
+ bsetCompare (bsetMake ()) (stateGetBs state) == 0 (* KD generates nodes with just True as formula *)
+ then begin
+ setAddState setFinishingStates state;
+ stateSetStatus state Sat
+ end else begin
+ setAddState setStates state;
+ if bsetCompare (stateGetDeferral state) emptySet == 0
+ then begin
+ setAddState setFinishingStates state
+ end
+ else ()
+ end
+
+ (* As it is enough for a core to have one successfull child, we can
+ * also handle (some) expandable cores.
+ *)
+ and coreCollector core =
+ match coreGetStatus core with
+ | Unsat -> ()
+ | Sat ->
+ setAddCore setCores core;
+ setAddCore setFinishingCores core
+ | Expandable
+ | Open ->
+ setAddCore setCores core;
+ if bsetCompare (coreGetDeferral core) emptySet == 0
+ then begin
+ setAddCore setFinishingCores core
+ end
+ else ()
+ in
+ graphIterStates stateCollector;
+ graphIterCores coreCollector;
+
+ setPropagationCounter !openstates;
+
+ (* In a fixpoint the set called setStates / setCores is narrowed
+ * down.
+ *
+ * In each step only those states and cores are retained in setStates
+ * / setCores which reach one of setFinishing{States,Cores} in
+ * finitely many steps. This new set of States / Cores is collected
+ * as allowed{States,Cores} during each fixpoint iteration.
+ *
+ * Only those finishing nodes are retained that have allowed or
+ * Successfull Children.
+ *)
+ let rec fixpointstep setStates setCores =
+ let allowedStates = setEmptyState () in
+ let allowedCores = setEmptyCore () in
+
+ let rec visitParentStates (core : core) : unit =
+ if not (setMemCore allowedCores core)
+ then begin
+ setAddCore allowedCores core;
+ let verifyParent (state,_) =
+ let rules = stateGetRules state in
+ let ruleiter (dependencies, corelist) =
+ List.exists (fun (core : core) -> setMemCore allowedCores core ||
+ coreGetStatus core == Sat)
+ corelist
+ in
+ if List.for_all ruleiter rules
+ then visitParentCores state
+ in
+ List.iter verifyParent (coreGetParents core)
+ end
+
+ and visitParentCores (state : state) : unit =
+ if not (setMemState allowedStates state)
+ then begin
+ setAddState allowedStates state;
+ let verifyParent core =
+ let acceptable =
+ List.exists (fun (state : state) -> setMemState allowedStates state ||
+ stateGetStatus state == Sat)
+ (coreGetChildren core)
+ in
+ if acceptable
+ then visitParentStates core
+ in
+ List.iter verifyParent (stateGetParents state)
+ end
+ in
+
+ (* All rule applications need to still be potentially Sat for a
+ * finishing State to be a valid startingpoint for this fixpoint.
+ *)
+ let checkFinishingState (state : state) =
+ let ruleiter (dependencies, corelist) : bool =
+ List.for_all (fun (core : core) -> coreGetStatus core == Unsat ||
+ coreGetStatus core == Expandable ||
+ not (setMemCore setCores core)) corelist
+ in
+ if not (List.exists ruleiter (stateGetRules state)) then begin
+ visitParentCores state
+ end
+
+ (* There needs to be a State still potentially Sat for this core
+ * to be considered for the fixpoint
+ *)
+ and checkFinishingCore (core : core) =
+ if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat ||
+ stateGetStatus state == Expandable ||
+ not (setMemState setStates state))
+ (coreGetChildren core))
+ then begin
+ visitParentStates core
+ end
+ in
+ setIterState checkFinishingState setFinishingStates;
+ setIterCore checkFinishingCore setFinishingCores;
+
+
+ if (setLengthState setStates) = (setLengthState allowedStates) &&
+ (setLengthCore setCores) = (setLengthCore allowedCores)
+ then begin
+ setIterState (fun state -> stateSetStatus state Sat) setStates;
+ setIterCore (fun core -> coreSetStatus core Sat; if core == graphGetRoot ()
+ then raise (CoAlg_finished true)
+ else ()) setCores;
+ end else
+ fixpointstep allowedStates allowedCores
+ in
+ fixpointstep setStates setCores
+
+
(*****************************************************************************)
(* Propagation of Unsatisfiability *)
(*****************************************************************************)
@@ -132,6 +287,9 @@ let lhtMustFind lht l =
| Some f -> f
| None -> assert false
+
+(* Gets a list of Things we know are unsatisfiable and propagates this
+ information backwards *)
let rec propagateUnsat = function
| [] -> ()
| propElem::tl ->
@@ -161,7 +319,8 @@ let rec propagateUnsat = function
let prop acc core =
let turnsUnsat =
match coreGetStatus core with
- | Open -> List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core)
+ | Open -> List.for_all (fun s -> stateGetStatus s = Unsat)
+ (coreGetChildren core)
| Expandable
| Unsat
| Sat -> false
@@ -182,7 +341,7 @@ let rec propagateUnsat = function
if comesFromCnstr then coreGetBs core
else
let bs = coreGetBs core in
- let solver = coreGetSolver core in
+ let Some solver = coreGetSolver core in
let fht = coreGetFht core in
let lht = lhtInit () in
let addLits f acc =
@@ -207,6 +366,7 @@ let rec propagateUnsat = function
in
coreSetBs core mbs;
coreSetStatus core Unsat;
+ coreDeallocateSolver core;
if core == graphGetRoot () then raise (CoAlg_finished false) else ();
let prop acc (state, idx) =
let turnsUnsat =
@@ -233,7 +393,7 @@ let rec propagateUnsat = function
let prop acc node =
match node with
| State state ->
- let turnsUnsat =
+ let turnsUnsat =
match stateGetStatus state with
| Expandable
| Open -> cssForall isConstraintUnsat (stateGetConstraints state)
@@ -255,6 +415,145 @@ let rec propagateUnsat = function
in
propagateUnsat tl1
+let propagateUnsatMu () =
+ let setFinishingStates = setEmptyState () in
+ let setFinishingCores = setEmptyCore () in
+ let setStates = setEmptyState () in
+ let setCores = setEmptyCore () in
+ let emptySet = bsetMakeRealEmpty () in
+
+ (* Collect two sets of nodes. All nodes that may be unsatisfiable
+ * after this iteration are collected into setStates/setCores.
+ *
+ * Nodes reaching Points with empty focus as well as Expandable nodes
+ * (if not Unsat) can not be declared Unsat so we collect these into
+ * setFinishingStates/setFinishingCores.
+ *)
+ let stateCollector state =
+ match stateGetStatus state with
+ | Unsat -> ()
+ | Sat
+ | Expandable ->
+ setAddState setStates state;
+ setAddState setFinishingStates state
+ | Open ->
+ setAddState setStates state;
+ if [] = (stateGetRules state)
+ then begin
+ stateSetStatus state Sat;
+ setAddState setFinishingStates state
+ end
+ else ();
+ if bsetCompare (stateGetDeferral state) emptySet == 0
+ then begin
+ setAddState setFinishingStates state
+ end
+ else ()
+
+ and coreCollector core =
+ match coreGetStatus core with
+ | Unsat -> ()
+ | Expandable
+ | Sat ->
+ setAddCore setCores core;
+ setAddCore setFinishingCores core
+ | Open ->
+ setAddCore setCores core;
+ if bsetCompare (coreGetDeferral core) emptySet == 0
+ then begin
+ setAddCore setFinishingCores core
+ end
+ else ()
+ in
+ graphIterStates stateCollector;
+ graphIterCores coreCollector;
+
+ (* In a fixpoint the set called setFinishingStates/setFinishingCores
+ * is narrowed down
+ *
+ * In each iteration we start with all Nodes and remove all that can
+ * reach a finishing Node. We then remove all finishing Nodes from the
+ * respective set which are becoming Unsat and start with the next
+ * iteration until the fixpoint is reached
+ *
+ *
+ *)
+ let rec fixpointstep setPrevUnsatStates setPrevUnsatCores =
+ let setUnsatStates = setCopyState setStates in
+ let setUnsatCores = setCopyCore setCores in
+
+ let rec visitParentStates (core : core) : unit =
+ if setMemCore setUnsatCores core
+ then begin
+ setRemoveCore setUnsatCores core;
+ let verifyParent (state,_) =
+ let rules = stateGetRules state in
+ let ruleiter (dependencies, corelist) =
+ List.exists (fun (core : core) -> not (setMemCore setUnsatCores core) ||
+ coreGetStatus core == Sat)
+ corelist
+ in
+ if List.for_all ruleiter rules
+ then visitParentCores state
+ in
+ List.iter verifyParent (coreGetParents core)
+ end
+
+ and visitParentCores (state : state) : unit =
+ if setMemState setUnsatStates state
+ then begin
+ setRemoveState setUnsatStates state;
+ let verifyParent core =
+ let acceptable =
+ List.exists (fun (state : state) -> not (setMemState setUnsatStates state) ||
+ stateGetStatus state == Sat)
+ (coreGetChildren core)
+ in
+ if acceptable
+ then visitParentStates core
+ in
+ List.iter verifyParent (stateGetParents state)
+ end
+ in
+
+ (* All rule applications need to still be potentially Sat for a
+ * finishing State to be a valid startingpoint for this fixpoint.
+ *)
+ let checkFinishingState (state : state) =
+ let ruleiter (dependencies, corelist) : bool =
+ List.for_all (fun (core : core) -> coreGetStatus core == Unsat ||
+ setMemCore setPrevUnsatCores core) corelist
+ in
+ if not (List.exists ruleiter (stateGetRules state)) ||
+ stateGetStatus state == Expandable then begin
+ visitParentCores state
+ end
+
+ (* There needs to be a State still potentially Sat for this core
+ * to be considered for the fixpoint
+ *)
+ and checkFinishingCore (core : core) =
+ if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat ||
+ setMemState setPrevUnsatStates state)
+ (coreGetChildren core)) ||
+ coreGetStatus core == Expandable
+ then begin
+ visitParentStates core
+ end
+ in
+ setIterState checkFinishingState setFinishingStates;
+ setIterCore checkFinishingCore setFinishingCores;
+
+ if (setLengthState setPrevUnsatStates) = (setLengthState setUnsatStates) &&
+ (setLengthCore setPrevUnsatCores) = (setLengthCore setUnsatCores)
+ then begin
+ setIterState (fun state -> stateSetStatus state Unsat) setUnsatStates;
+ setIterCore (fun core -> propagateUnsat [UCore (core, false)]) setUnsatCores;
+ end else
+ fixpointstep setUnsatStates setUnsatCores
+ in
+ fixpointstep (setEmptyState ()) (setEmptyCore ())
+
(*****************************************************************************)
(* Propagation of Nominal Constraints *)
@@ -413,7 +712,7 @@ let getLit sort fht solver f =
in
lit
-let newCore sort bs =
+let newCore sort bs defer =
(* when creating a now core from a set of formulas bs
bs = { x_1, ...., x_n }
= "x_1 /\ .... /\ x_n"
@@ -476,13 +775,30 @@ let newCore sort bs =
assert (okay1);
let okay2 = M.add_clause solver [M.neg_lit lf; lf2] in
assert (okay2)
+ | MuF
+ | NuF ->
+ (*
+ Dest of a fixpoint is it's unfolded version. This adds just
+ an simple forward implication that could be optimised out
+ though not without nontrivial transformation of code
+
+ f = μ X . φ |---> lf
+ φ[X |-> f] |---> lf1
+
+ Then adding lf -> lf1 to minisat
+ *)
+ let f1 = lfGetDest1 sort f in
+ addClauses f1;
+ let lf1 = fhtMustFind fht f1 in
+ let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
+ assert (okay1);
| _ -> ()
(* case 2.(c)
We don't need to do anything except adding f to the fht
*)
in
bsetIter addClauses bs;
- coreMake sort bs solver fht
+ coreMake sort bs defer (Some solver) fht
let getNextState core =
(* Create a new state, which is obtained by a satisfying assignment of the
@@ -492,9 +808,16 @@ let getNextState core =
minisat calls.
*)
let bs = coreGetBs core in
+ let refocusing = bsetCompare (bsetMakeRealEmpty ()) (coreGetDeferral core) = 0 in
+ let deferralS =
+ if refocusing then
+ bsetCopy bs
+ else
+ coreGetDeferral core
+ in
let fht = coreGetFht core in
let litset = bsetFold (fun f acc -> (fhtMustFind fht f)::acc) bs [] in
- let solver = coreGetSolver core in
+ let Some solver = coreGetSolver core in
let isSat = M.invoke_solver solver litset in
(* Clearly, if the current core is unsatisfiable, no further child state can
be created *)
@@ -506,6 +829,7 @@ let getNextState core =
satisfiable.
*)
let newbs = bsetMake () in
+ let newdefer = bsetMakeRealEmpty () in
(* if newbs = { l_1, .... l_n }, i.e.
newbs = l_1 /\ ... /\ l_n
@@ -517,7 +841,7 @@ let getNextState core =
By mkExclClause, newbs is filled, and clause is built in the accumulator acc.
*)
- let rec mkExclClause f acc =
+ let rec mkExclClause deferral f acc =
(* f is a formula that is true in the current satisfying assignment *)
match lfGetType sort f with
| OrF ->
@@ -526,47 +850,65 @@ let getNextState core =
let lf1 = fhtMustFind fht f1 in
(* if the first disjunct f1 is true, then we need to add subformulas
of f1 to newbs&clause *)
- if M.literal_status solver lf1 = M.LTRUE then mkExclClause f1 acc
+ if M.literal_status solver lf1 = M.LTRUE then mkExclClause deferral f1 acc
else
(* otherwise f2 must be true *)
let f2 = lfGetDest2 sort f in
let lf2 = fhtMustFind fht f2 in
assert (M.literal_status solver lf2 = M.LTRUE);
- mkExclClause f2 acc
+ mkExclClause deferral f2 acc
| AndF ->
(* if the true f is a conjuction, then both conjunctions must be true *)
let f1 = lfGetDest1 sort f in
let lf1 = fhtMustFind fht f1 in
assert (M.literal_status solver lf1 = M.LTRUE);
- let acc1 = mkExclClause f1 acc in
+ let acc1 = mkExclClause deferral f1 acc in
let f2 = lfGetDest2 sort f in
let lf2 = fhtMustFind fht f2 in
assert (M.literal_status solver lf2 = M.LTRUE);
- mkExclClause f2 acc1
+ mkExclClause deferral f2 acc1
+ | MuF
+ | NuF ->
+ let f1 = lfGetDest1 sort f in
+ mkExclClause deferral f1 acc
| _ ->
- (* if f is a trivial formula or modality, then add it ... *)
- (* ... to newbs *)
- bsetAdd newbs f;
- (* ... and to the new clause *)
- (M.neg_lit (fhtMustFind fht f))::acc
+ (* if f is a trivial formula or modality, then add it ... *)
+ (* ... to newbs *)
+ bsetAdd newbs f;
+ let defercandidate = lfGetDeferral sort f in
+ (if (defercandidate != (Hashtbl.hash "ε") &&
+ (refocusing || deferral = defercandidate)) then
+ bsetAdd newdefer f);
+ (* ... and to the new clause *)
+ (M.neg_lit (fhtMustFind fht f))::acc
+ in
+ let init_clause f acc =
+ let deferral =
+ (* for each deferral determine which variable it belongs to *)
+ if bsetMem deferralS f then (
+ lfGetDeferral sort f)
+ else
+ (Hashtbl.hash "ε")
+ in
+ mkExclClause deferral f acc
in
- let clause = bsetFold mkExclClause bs [] in
+ let clause = bsetFold init_clause bs [] in
let okay = M.add_clause solver clause in
assert (okay);
- Some (sort, newbs)
+ Some (sort, newbs, newdefer)
-let newState sort bs =
+let newState sort bs defer =
let (func, sl) = !sortTable.(sort) in
let producer = CoAlgLogics.getExpandingFunctionProducer func in
- let exp = producer sort bs sl in
- stateMake sort bs exp
+ let exp = producer sort bs defer sl in
+ stateMake sort bs defer exp
-let insertState parent sort bs =
+let insertState parent sort bs defer =
let child =
- match graphFindState sort bs with
+ match graphFindState sort (bs, defer) with
| None ->
- let s = newState sort bs in
- graphInsertState sort bs s;
+ let s = newState sort bs defer in
+ graphInsertState sort (bs, defer) s;
queueInsertState s;
s
| Some s -> s
@@ -576,29 +918,32 @@ let insertState parent sort bs =
let expandCore core =
match getNextState core with
- | Some (sort, bs) ->
- insertState core sort bs;
+ | Some (sort, bs, defer) ->
+ insertState core sort bs defer;
queueInsertCore core
| None ->
let isUnsat = List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core) in
- if isUnsat then propagateUnsat [UCore (core, false)]
- else coreSetStatus core Open
+ if isUnsat
+ then
+ propagateUnsat [UCore (core, false)]
+ else
+ coreSetStatus core Open
-let insertCore sort bs =
- match graphFindCore sort bs with
+let insertCore sort bs defer =
+ match graphFindCore sort (bs, defer) with
| None ->
- let c = newCore sort bs in
- graphInsertCore sort bs c;
- queueInsertCore c;
- c
+ let c = newCore sort bs defer in
+ graphInsertCore sort (bs, defer) c;
+ queueInsertCore c;
+ c
| Some c -> c
let insertRule state dep chldrn =
let chldrn = listFromLazylist chldrn in
- let insert (isUns, acc) (sort, bs) =
+ let insert (isUns, acc) (sort, bs, defer) =
let bs1 = bsetAddTBox sort bs in
- let core = insertCore sort bs1 in
+ let core = insertCore sort bs1 defer in
let isUns1 = if coreGetStatus core = Unsat then isUns else false in
(isUns1, core::acc)
in
@@ -646,7 +991,7 @@ let expandCnstr cset =
in
csetIter cset mkCores;
let inCores (sort, _) bs (isUns, acc) =
- let core = insertCore sort bs in
+ let core = insertCore sort bs bs in (* TODO: think of deferral / μ stuff here *)
coreAddConstraintParent core cset;
(coreGetStatus core = Unsat || isUns, core::acc)
in
@@ -668,8 +1013,8 @@ let expandNodesLoop (recursiveAction: unit -> unit) =
if stateGetStatus state = Expandable then begin
expandState state;
if doNominalPropagation () then begin
- propagateNominals ();
- if doSatPropagation () then propagateSat ()
+ (* propagateNominals (); *)
+ if doSatPropagation () then (propagateUnsatMu (); propagateSatMu ())
end else ()
end else ();
recursiveAction ()
@@ -677,8 +1022,8 @@ let expandNodesLoop (recursiveAction: unit -> unit) =
if coreGetStatus core = Expandable then begin
expandCore core;
if doNominalPropagation () then begin
- propagateNominals ();
- if doSatPropagation () then propagateSat ()
+ (* propagateNominals (); *)
+ if doSatPropagation () then (propagateUnsatMu (); propagateSatMu ())
end else ()
end else ();
recursiveAction ()
@@ -693,14 +1038,14 @@ let runReasonerStep () =
(* if this emptied the queue *)
if queueIsEmpty () then begin
(* then check whether the nominals would add further queue elements *)
- print_endline "Propagating nominals...";
- propagateNominals ()
+ (* print_endline "Propagating nominals..."; *)
+ (* propagateNominals () *)
end else () (* else: the next step would be to expand another node *)
let rec buildGraphLoop () =
let rec expandNodesFurther () = expandNodesLoop expandNodesFurther in
expandNodesFurther (); (* expand as many queue elements as possible *)
- propagateNominals ();
+ (* propagateNominals (); *)
(* if propagating nominals added some more queue members, do all again.. *)
if queueIsEmpty () then () else buildGraphLoop ()
@@ -709,16 +1054,22 @@ let initReasoner sorts nomTable tbox sf =
let (tbox1, sf1, bs) = ppFormulae nomTable tbox sf in
let sort = fst sf in
let bs1 = bsetAddTBox sort bs in
+ let deferrals = bsetMakeRealEmpty() in
+ let markDeferral f =
+ if (Hashtbl.hash "ε") != (lfGetDeferral sort f) then (
+ bsetAdd deferrals f;)
+ in
+ bsetIter markDeferral bs;
graphInit ();
queueInit ();
- let root = insertCore sort bs1 in
+ let root = insertCore sort bs1 deferrals in
graphAddRoot root
let isRootSat () =
match coreGetStatus (graphGetRoot ()) with
| Expandable -> None
| Unsat -> Some false
- | Sat
+ | Sat -> Some true
| Open -> if (queueIsEmpty()) then Some true else None
let reasonerFinished () =
@@ -727,7 +1078,7 @@ let reasonerFinished () =
| Unsat
| Sat -> true
| Open -> queueIsEmpty ()
-
+
(** A graph-tableau-based decision procedure framework for coalgebraic logics.
@param verbose An optional switch which determines
@@ -748,6 +1099,7 @@ let isSat ?(verbose = false) sorts nomTable tbox sf =
let sat =
try
buildGraphLoop ();
+ propagateUnsatMu ();
(* get whether the root is satisfiable *)
(* we know that the reasoner finished, so the value is there, *)
(* i.e. isRootSat() will give a "Some x" and not "None" *)
@@ -775,4 +1127,3 @@ let isSat ?(verbose = false) sorts nomTable tbox sf =
print_newline ()
else ();
sat
-
diff --git a/src/lib/HashConsing.ml b/src/lib/HashConsing.ml
index a7e88dee447e90c162e6de2702c93d99704522c0..6b75c0b9ee40f79c227f74b8b2096b6dce97dd83 100644
--- a/src/lib/HashConsing.ml
+++ b/src/lib/HashConsing.ml
@@ -208,11 +208,18 @@ module Make(H : HashedTyped) : (S with type nde = H.nde and type fml = H.fml) =
let ndeN = H.negNde nde in
let hkeyN = realhash ndeN in
let fmlN = H.toFml ndeN in
- let ndN = { node = ndeN; hkey = hkeyN; tag = osize + 1; fml = fmlN; neg = nd } in
- nd.neg <- ndN;
let idxN = hkeyN mod ds in
- data.(idxN) <- ndN :: data.(idxN);
- hc.size <- osize + 2;
+ let bucketN = data.(idxN) in
+ try begin
+ find ndeN bucketN;
+ hc.size <- succ osize;
+ end
+ with Not_found ->
+ let ndN = { node = ndeN; hkey = hkeyN; tag = osize + 1; fml = fmlN; neg = nd } in
+ nd.neg <- ndN;
+ let idxN = hkeyN mod ds in
+ data.(idxN) <- ndN :: data.(idxN);
+ hc.size <- osize + 2
else hc.size <- succ osize;
if hc.size > ds lsl 1 then resize hc else ();
nd
diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml
index a6f312d2580134c3a6ee94093b830dc8f5032ee5..0fdc0fbb1594b836848c50b46d51a3df0075de48 100644
--- a/src/testsuite/cool-testsuite.ml
+++ b/src/testsuite/cool-testsuite.ml
@@ -37,15 +37,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))"
- ; 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"
+ ; 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"
]