Commit 9840f81e authored by Christian Müller's avatar Christian Müller

add types!

parent 18857293
p cnf 35 44
7 0
-7 8 0
-7 9 0
-8 -1 -2 0
-9 10 0
-9 11 0
-10 -1 -3 0
-11 12 0
-11 13 0
-12 -4 -1 0
-13 14 0
-13 15 0
-14 -4 -5 0
-15 16 0
-15 17 0
-16 -4 -2 0
-17 18 0
-17 19 0
-18 -4 -3 0
-19 20 0
-19 21 0
-20 -1 -5 0
-21 22 0
-21 23 0
-22 -2 -3 0
-23 24 0
-23 25 0
-24 -6 -5 0
-25 26 0
-25 27 0
-26 -6 -3 0
-27 28 0
-27 29 0
-28 -5 -3 0
-29 30 0
-29 31 0
-30 -6 -2 0
-31 32 0
-31 33 0
-32 -5 -2 0
-33 34 0
-33 35 0
-34 -6 -1 0
-35 -6 -4 0
p cnf 3 2
3 0
-3 -1 -2 0
Workflow
forallmay x,p
forallmay x:A,p:P
True -> Conf += (x,p)
forallmay x,p
forallmay x:A,p:P
!Conf(x,p) -> Ass += (x,p)
forallmay x,p,r
forallmay x:A,p:P,r:R
(Ass(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
loop {
forall xa,xb,p,r (A(xa,p) ∧ Review(xb,p,r)) -> Read += (xa,xb,p,r)
forallmay x,p,r (A(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
forall xa:A,xb:A,p:P,r:R (A(xa,p) ∧ Review(xb,p,r)) -> Read += (xa,xb,p,r)
forallmay x:A,p:P,r:R (A(x,p) ∧ O(x,p,r)) -> Review += (x,p,r)
}
Target
Read(xa, xb, p, r)
Read(xa:A, xb:A, p:P, r:R)
Workflow
forall x,s
forall x:A,s:S
O(s) -> R += (x,s)
Target
R(x,s)
\ No newline at end of file
R(x:A,s:S)
......@@ -37,9 +37,10 @@ object Main extends App with LazyLogging {
val (agents, res) = LTL.eliminateExistentials(prop)
logger.info(s"Using universe $agents")
if (agents.length > MAXAGENTS) {
logger.error(s"Universe of size ${agents.size} is too large. Aborting.")
logger.info(s"Using universe ${agents.map(_.withType())}")
if (agents.groupBy(_.typ).exists(_._2.size > MAXAGENTS)) {
logger.error(s"Universe has more than $MAXAGENTS agents for a single type. Aborting.")
return
}
......
......@@ -120,7 +120,7 @@ object WorkflowParser extends RegexParsers with LazyLogging {
def OR = repsep(SIMPLETERM, "∨") ^^ { case ts => Or.make(ts) }
def NEG = ("¬" | "!") ~ SIMPLETERM ^^ { case _ ~ t => Neg(t) }
def TUPLE = "(" ~> repsep(VAR, ",") <~ ")"
def TUPLE = "(" ~> repsep(TYPEDVAR, ",") <~ ")"
def FUN = VAR ~ TUPLE ^^ { case f ~ tup => Fun(f.name, tup) }
def SIMPLETERM = (tt | ff | FUN )
......
......@@ -48,11 +48,11 @@ case class Remove(guard: Term, fun: String, tuple: List[Var]) extends Statement
case class ForallBlock(agents: List[Var], steps: List[Statement]) extends SimpleBlock {
val may = false
override def toString() = "forall " + agents.mkString(",") + steps.mkString("\n ", ";\n ", "")
override def toString() = "forall " + agents.map(_.withType).mkString(",") + steps.mkString("\n ", ";\n ", "")
}
case class ForallMayBlock(agents: List[Var], pred: String, steps: List[Statement]) extends SimpleBlock {
val may = true
override def toString() = "forall " + agents.mkString(",") + " may (" + pred + ")" + steps.mkString("\n ", ";\n ", "")
override def toString() = "forall " + agents.map(_.withType).mkString(",") + " may (" + pred + ")" + steps.mkString("\n ", ";\n ", "")
}
case class Loop(steps: List[Block]) extends Block {
......
......@@ -47,6 +47,7 @@ object FOLTL {
}
case class Var(name: String, typ:String = Var.DEFAULT_TYPE) extends Term {
override def toString() = s"$name"
def withType() = s"$name:$typ"
}
object Fun {
......@@ -66,7 +67,7 @@ object FOLTL {
override def toString() = {
// show types only in quantifiers
qname + " " + vars.map(v => s"${v.name}:${v.typ}").mkString(",") + ". " + t.bracketed()
qname + " " + vars.map(_.withType()).mkString(",") + ". " + t.bracketed()
}
}
......
......@@ -27,6 +27,8 @@ object Causal {
}
val max = outputs.map(_.params.length).max
// TODO: Add correct types
val vexist = (for (num <- 1 until max) yield { Var(s"causalce$num") }) toList
val agents = agent :: vexist
......
......@@ -8,14 +8,17 @@ import de.tum.workflows.foltl.FOLTL._
object LTL extends LazyLogging {
// Computes all possible tuples of size i
def comb[T](i: Int, agents:List[T]):List[List[T]] = {
i match {
case 0 => List(List())
case i => {
val subres = comb(i - 1, agents)
for (a <- agents; s <- subres) yield {
s :+ a
def comb[T](types:List[String], universe:Map[String, List[T]]):List[List[T]] = {
types match {
case List() => List(List())
case t :: ts => {
val subres = comb(ts, universe)
if (!universe.isDefinedAt(t)) {
logger.error(s"No variable for type ${t} in the universe.")
}
for (a <- universe(t); s <- subres) yield {
a :: s
}
}
}
......@@ -48,15 +51,17 @@ object LTL extends LazyLogging {
// TODO: does not work for nested foralls
def eliminateUniversals(t: Term, agents: List[Var]) = {
if (agents.isEmpty) {
logger.error("Agent list should never be empty")
}
val universe = agents.groupBy(_.typ)
t.everywhere({
case Forall(tup, term) => {
val repl = comb(tup.size, agents)
val terms = for (r <- repl) yield {
val mapping = tup.zip(r) toMap
val replacements = comb(tup.map(_.typ), universe)
val terms = for (repl <- replacements) yield {
val mapping = tup.zip(repl) toMap
term.everywhere({
// do replacement
......
......@@ -25,10 +25,30 @@ class LTLSpec extends FlatSpec {
val f3 = Forall(List("x","y"), Fun("f", List("x", "y")))
val r = """
(f(x,x) ∧ f(y,x) ∧ f(x,y) ∧ f(y,y))
(f(x,x) ∧ f(x,y) ∧ f(y,x) ∧ f(y,y))
"""
LTL.eliminateUniversals(f3, List("x", "y")) should be(WorkflowParser.parseTerm(r).get)
}
it should "generate the correct types" in {
val x = Var("x", "agent")
val p = Var("p","paper")
val f = Globally(Forall(List(x, p), Fun("f", List(x, p))))
LTL.eliminateUniversals(f, List(x, p)) should be (
Globally(Fun("f", List(x,p)))
)
val x2 = Var("x2", "agent")
val f2 = Forall(List(x, p), Fun("f", List(x, p)))
val r2 = And(Fun("f", List(x,p)), Fun("f", List(x2, p)))
LTL.eliminateUniversals(f2, List(x, p, x2)) should be(r2)
val f3 = Forall(List(x, x2, p), Fun("f", List(x, x2, p)))
val r3 = And.make(Fun("f", List(x,x,p)), Fun("f", List(x, x2, p)), Fun("f", List(x2,x,p)), Fun("f", List(x2,x2,p)))
LTL.eliminateUniversals(f3, List(x, x2, p)) should be(r3)
}
"Existential elimination" should "work" in {
val test = Exists("a", And(Globally(Exists("b", True)), Exists("c", Forall("d", Exists("e", False)))))
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment