Commit d3643fe9 authored by Christian Müller's avatar Christian Müller

workflow to LTL

parent 56228e9d
G ((n0 → X n1) ∧ (n1 → X (n3 ∨ n2)) ∧ (n2 → X n2) ∧ (n3 → X n1)) ∧ G (¬(n0 ∧ n1) ∧ ¬(n0 ∧ n2) ∧ ¬(n0 ∧ n3) ∧ ¬(n1 ∧ n2) ∧ ¬(n1 ∧ n3) ∧ ¬(n2 ∧ n3)) ∧ ((n0 ∧ X n1) → ((X Q_a_a ↔ (Q_a_a ∨ (O_a ∧ choice0_a_a))) ∧ (X O_a ↔ O_a) ∧ (X R_a_a ↔ R_a_a) ∧ (X S_a_a_a ↔ S_a_a_a))) ∧ ((n1 ∧ X n3) → ((X S_a_a_a ↔ (S_a_a_a ∨ (R_a_a ∧ choice1_a_a_a))) ∧ (X O_a ↔ O_a) ∧ (X Q_a_a ↔ Q_a_a) ∧ (X R_a_a ↔ R_a_a))) ∧ ((n1 ∧ X n2) → ((X O_a ↔ O_a) ∧ (X Q_a_a ↔ Q_a_a) ∧ (X R_a_a ↔ R_a_a) ∧ (X S_a_a_a ↔ S_a_a_a))) ∧ ((n2 ∧ X n2) → ((X O_a ↔ O_a) ∧ (X Q_a_a ↔ Q_a_a) ∧ (X R_a_a ↔ R_a_a) ∧ (X S_a_a_a ↔ S_a_a_a))) ∧ ((n3 ∧ X n1) → ((X R_a_a ↔ (R_a_a ∨ Q_a_a)) ∧ (X O_a ↔ O_a) ∧ (X Q_a_a ↔ Q_a_a) ∧ (X S_a_a_a ↔ S_a_a_a))) ∧ (n0 ∧ ¬n1 ∧ ¬n2 ∧ ¬n3 ∧ ¬Q_a_a ∧ ¬R_a_a ∧ ¬S_a_a_a)
......@@ -3,15 +3,25 @@ package de.tum.workflows
import foltl.FOLTL._
import blocks.WorkFlow._
import Implicits._
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.ltl.LTL
object Main extends App {
object Main extends App with LazyLogging {
val w = Workflow(List(
val w = Workflow(
Signature(Map(
// first one is oracle
("O" -> List("s")),
("Q" -> List("x","s")),
("R" -> List("y","s")),
("S" -> List("x","y","s"))
)),
List(
ForallMayBlock(List("x","s"),
Add(Fun("O","s"),"Q", List("x","s"))
),
Loop(List(
ForallMayBlock(List("x","y","s"),
ForallBlock(List("x","y","s"),
Add(Fun("R", List("y","s")), "S", List("x","y","s"))
),
ForallBlock(List("x","s"),
......@@ -19,7 +29,13 @@ object Main extends App {
)
))
))
println(w)
logger.info(s"Workflow:\n$w")
val res = Encoding.toFOLTL(w)
// agent list
val res2 = LTL.eliminateUniversals(res, List("a"))
val res3 = LTL.eliminatePredicates(res2)
logger.info(res3.toString())
}
\ No newline at end of file
package de.tum.workflows
object Utils {
def mkString[T](string: Iterable[T], start: String, mid: String, end:String) = {
if (string.isEmpty) "" else string.mkString(start, mid, end)
}
}
\ No newline at end of file
......@@ -11,15 +11,19 @@ import de.tum.workflows.foltl.FOLTL
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.TermFunctions._
import com.typesafe.scalalogging._
import scalax.collection.edge.LBase.LEdgeImplicits
object BlockImplicit extends LEdgeImplicits[SimpleBlock]; import BlockImplicit._
object Encoding {
object Encoding extends LazyLogging {
val ORACLE = "O"
// Naming
// TODO: make sure there are no clashes
def nodeVar(n: Any) = Var("n" + n)
def nodeVar(n: Any) = Fun("n" + n, List())
def choiceVar(n: Any) = "choice" + n
def makeblock(b: Block, n1: Int, n2:Int, makeNode: (() => Int), makeId: (() => Block)):(List[LDiEdge[Int]]) = {
......@@ -91,7 +95,6 @@ object Encoding {
}
def encodeStmt(s: Statement, pred: Option[Term]):(Term, String) = {
var guard = s.guard
for (p <- pred) { // if pred defined
guard = And(guard, p)
......@@ -104,42 +107,53 @@ object Encoding {
(Forall(s.tuple, Eq(Next(Fun(s.fun, s.tuple)), t)), s.fun)
}
def encodeSem(g: Graph[Int, LDiEdge]) = {
// TODO: this is still wrong - should be EVERY relation
// all relations that are updated
// val updated = for (e <- g.edges.toList; s <- e.steps) yield {
// // e has a block that is not a loop
// s.fun
// }
def encodeStaying(sig: Signature, u:String) = {
val tup = sig.preds(u)
Forall(tup, Eq(Next(Fun(u, tup)), Fun(u, tup)))
}
def encodeSem(sig: Signature, g: Graph[Int, LDiEdge]) = {
val impls = for (e <- g.edges.toList) yield {
val choice = if (e.may) Some(Fun(choiceVar(e.from), e.label.agents)) else None
// TODO: choicevar breaks as soon as we change the graph structure
val choice = if (e.may) Some(Fun(choiceVar(e.from), e.agents)) else None
val res = for (s <- e.steps) yield {
encodeStmt(s, choice)
}
// TODO fix this
// val updates = res.map(_._2)
// val staying:List[Term] = for (u <- updated if !updates.contains(u)) yield {
//
// }
val terms = res.map(_._1)
val updates = res.map(_._2)
val staying = for (u <- sig.preds.map(_._1) if !updates.contains(u)) yield {
encodeStaying(sig, u)
}
val terms = res.map(_._1) ++ staying
Implies(And(nodeVar(e.from), Next(nodeVar(e.to))), BinOp.makeL(And.apply, terms))
}
BinOp.makeL(And.apply, impls)
}
def encodeInitial(sig: Signature, g: Graph[Int, LDiEdge]) = {
val empties = for ((p, tup) <- sig.preds if !(p == ORACLE)) yield {
Forall(tup, Neg(Fun(p, tup)))
}
val nodes = for (n <- g.nodes.toList if !(n == 0)) yield {
Neg(nodeVar(n))
}
BinOp.makeL(And.apply, nodeVar(0) +: (nodes ++ empties))
}
def toFOLTL(w: Workflow) = {
val g = toGraph(w)
println("Graph of w: " + g)
logger.info("Graph of w:\n" + g)
val cfg = encodeGraph(g)
println("cfg(w): " + cfg)
logger.info(s"cfg(w): $cfg")
val sanity = encodeSanity(g)
println("sanity(w): " + sanity)
// val encodesem = encodeSem(g)
logger.info(s"sanity(w): $sanity")
val sem = encodeSem(w.sig, g)
logger.info(s"sem(w): $sem")
val init = encodeInitial(w.sig, g)
logger.info(s"init(w): $init")
BinOp.makeL(And.apply, List(cfg, sanity, sem, init))
}
}
\ No newline at end of file
......@@ -3,7 +3,9 @@ package de.tum.workflows.blocks
import de.tum.workflows.foltl.FOLTL._
object WorkFlow {
case class Workflow(steps: List[Block]) {
case class Signature(preds: Map[String, List[Var]])
case class Workflow(sig: Signature, steps: List[Block]) {
override def toString() = steps.mkString("\n")
}
......
package de.tum.workflows.foltl
import de.tum.workflows.Utils
//import de.tum.workflows.foltl.TermFunctions._
object FOLTL {
......@@ -27,7 +28,7 @@ object FOLTL {
def apply(name: String, params: List[Var]):Fun = Fun(name, None, params)
}
case class Fun(name: String, ind:Option[String], params: List[Var]) extends Term {
override def toString() = name + ind.mkString("(",",",")") + params.mkString("(", ",", ")")
override def toString() = name + Utils.mkString(ind, "(", "", ")") + params.mkString("(", ",", ")")
}
trait Quantifier extends Term {
......
......@@ -26,26 +26,6 @@ object TermFunctions {
}
free(t, Set())
}
// def relations(t: Term) {
// def rels(t: Term, s: Set[String]):Set[String] = {
// t match {
// // Extractors
// // Exists, Forall
// case Quantifier(_, ps, t) => rels(t, s)
// case Until(t1, t2) => rels(t1, s) ++ rels(t2, s)
// case Next(t1) => rels(t1, s)
// case Globally(t1) => rels(t1, s)
// case Finally(t1) => rels(t1, s)
// // And, Or, Eq, Implies
// case BinOp(_, t1, t2) => rels(t1, s) ++ rels(t2, s)
// case Neg(t1) => rels(t1, s)
// case Fun(s, _, _) => Set(s)
// case x => Set()
// }
// }
// rels(t, Set())
// }
def simplify(t: Term): Term = {
val simp: PartialFunction[Term, Term] = {
......
package de.tum.workflows.ltl
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Utils
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
}
}
}
}
// agents need to be distince names in t
def eliminateUniversals(t: Term, agents: List[Var]) = {
if (agents.isEmpty) {
logger.error("Agent list should never be empty")
}
t.everywhere({
case Forall(tup, term) => {
val repl = comb(tup.size, agents)
val terms = for (r <- repl) yield {
var newterm = term
for ((x,a) <- tup.zip(r)) {
newterm = newterm.everywhere({
// do replacement
case Fun(f, id, tup) => Fun(f, id, tup.map(v => if (x == v) a else v))
})
}
newterm
}
BinOp.makeL(And.apply, terms)
}
})
}
def eliminatePredicates(t: Term) = {
t.everywhere({
case Fun(f, ind, tup) => {
val pi = if (ind.isDefined) "_" + ind.get else ""
Var(f + pi + Utils.mkString(tup, "_", "_", ""))
}
})
}
}
\ No newline at end of file
object Test extends App {
val agents = List("a", "b", "c")
println(agents.combinations(2).toList)
}
\ No newline at end of file
package de.tum.workflows.ltl.tests
import org.scalatest._
import org.scalatest.Matchers._
import org.scalatest.Inspectors._
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.ltl.LTL
import de.tum.workflows.Implicits._
class LTLSpec extends FlatSpec {
"A FOLTL formula" should "simplify double negation" in {
Neg(Neg(True)).simplify() should be (True)
}
"The universal replacement" should "work" in {
val f = Globally(Forall(List("x", "y"), Fun("f", List("x", "y"))))
LTL.eliminateUniversals(f, List("a")) should be (Globally(Fun("f", List("a", "a"))))
val f2 = Exists("x", Forall(List("y"), Fun("f", List("x", "y"))))
LTL.eliminateUniversals(f2, List("a")) should be (Exists("x", Fun("f", List("x", "a"))))
}
}
\ No newline at end of file
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