initial looping version

.gitignore

+*.class
+*.log
+
+# sbt specific
+.cache
+.cache-main
+.cache-tests
+.history
+.lib/
+dist/*
+target/
+lib_managed/
+src_managed/
+project/boot/
+project/plugins/project/
+
+# Scala-IDE specific
+.scala_dependencies
+.worksheet
+
+# Eclipse
+build
+.classpath
+.settings/

.project

+<projectDescription>
+  <name>LoopingWorkflows</name>
+  <buildSpec>
+    <buildCommand>
+      <name>org.scala-ide.sdt.core.scalabuilder</name>
+    </buildCommand>
+  </buildSpec>
+  <natures>
+    <nature>org.scala-ide.sdt.core.scalanature</nature>
+    <nature>org.eclipse.jdt.core.javanature</nature>
+  </natures>
+  <linkedResources> </linkedResources>
+</projectDescription>
\ No newline at end of file

build.sbt

+name := "LoopingWorkflows"
+
+version := "0.1"
+
+scalaVersion := "2.11.8"
+
+libraryDependencies ++= Seq(
+	"com.typesafe.scala-logging" %% "scala-logging" % "3.5.0",
+	"ch.qos.logback" % "logback-classic" % "1.1.7",
+	"org.scalactic" %% "scalactic" % "3.0.1",
+	"org.scalatest" %% "scalatest" % "3.0.1" % "test",
+	"org.scala-graph" %% "graph-core" % "1.11.4"
+)
+

project/plugins.sbt

+addSbtPlugin("com.artima.supersafe" % "sbtplugin" % "1.1.0")

scala/de/tum/workflows/Implicits.scala

+package de.tum.workflows
+
+import pqltl.PQLTL._
+
+object Implicits {
+  implicit def toList[A](v: A): List[A] = List(v)
+
+  // Logic
+  implicit def nameToVar(name: String) = Var(name)
+}

scala/de/tum/workflows/Main.scala

+package de.tum.workflows
+
+import pqltl.PQLTL._
+import blocks.WorkFlow._
+import Implicits._
+
+object Main extends App {
+  
+//  val post = Historically(Forall(List("x", "p"), Neg(And(Fun("Conf", List("x", "p")), Fun("Know", List("x", "p"))))))
+//
+//  val workflow = Workflow(List(
+//      ForallMayBlock(List("a1", "p1"), Add(True, "Conf", List("a1", "p1"))),
+//      ForallMayBlock(List("a2", "b2", "p2"), Add(Fun("Conf", List("b2", "p2")), "Know", List("a2", "p2")))
+//  ))
+  
+//  println(Neg(post).simplify())
+//  println(workflow)
+}
\ No newline at end of file

scala/de/tum/workflows/blocks/Precondition.scala

+package de.tum.workflows.blocks
+
+import de.tum.workflows.pqltl.PQLTL._
+import de.tum.workflows.blocks.WorkFlow._
+import com.typesafe.scalalogging.LazyLogging
+
+object Precondition extends LazyLogging {
+  
+  // Generates new name everytime
+  def auxname = "Aux"
+  
+  def apply(w: Workflow, t: Term): Term = {
+    val simp = t.simplify()
+    val result = foldblocks(simp, w.steps)
+    val notemporals = result.removeTemporals()
+    notemporals.simplify()
+  }
+  
+  def foldblocks(t: Term, steps: List[Block]): Term = {
+
+    steps.zipWithIndex.foldRight(t)((b, t) => b match {
+
+      case (ForallBlock(agents, stmts),_)    => foldstmts(t, stmts)
+      case (ForallMayBlock(agents, stmts), i) => foldmaystmts(t, auxname + i, stmts)
+
+    })
+  }
+
+  def foldstmts(t: Term, steps: List[Statement]): Term = {
+
+    // No aux calls
+    steps.foldRight(t)(wp(xs => True) _).simplify()
+
+  }
+
+  def foldmaystmts(t: Term, auxname:String, steps: List[Statement]): Term = {
+    
+    steps.foldRight(t)(wp(xs => Fun(auxname, None, xs)) _).simplify()
+
+  }
+  
+  def wp(mkaux: List[Var] => Term)(step:Statement, t:Term): Term = {
+    
+    // Resolve temporals
+    val unwrapped = t.everywhere({
+      case Since(u, v) => Or(v, And(u, Since(u,v)))
+      case Once(t) => Or(t, Once(t))
+      case Historically(t) => And(t, Historically(t))
+    })
+    
+    val simp = unwrapped.simplify()
+    
+    val replaced = (step match {
+      
+      case Add(guard, fun, tuple) => simp.everywhere({
+        // Ignore temporals
+        case _:TemporalTerm => t
+        case Fun(name, Some(ind), xs) if fun == name =>
+          Or(
+            Fun(name, Some(ind), xs),
+            Exists((guard.freeVars() -- xs).toList, And(guard.annotate(ind), mkaux(xs).annotate(ind)))
+          )
+        case Fun(name, None, xs) => {
+          println("FAIL") 
+          False
+        }
+      })
+      
+      case Remove(guard, fun, tuple) => simp.everywhere({
+        // Ignore temporals
+        case _:TemporalTerm => t
+        case Fun(name, Some(ind), xs) if fun == name =>
+          And(
+            Fun(name, Some(ind), xs),
+            Forall((guard.freeVars() -- xs).toList, Or(Neg(guard.annotate(ind)), Neg(mkaux(xs).annotate(ind))))
+          )
+        case Fun(name, None, xs) => {
+          println("FAIL") 
+          False
+        }
+      })
+    })
+    
+    val pre = replaced.simplify()
+    
+    // Unwrap prev
+    val result = pre.everywhere({
+      case Previously(t) => t
+    })
+    
+    logger.debug(s"Precondition of $t under $step is $result")
+    
+    result
+  }
+
+}

scala/de/tum/workflows/blocks/Workflow.scala

+package de.tum.workflows.blocks
+
+import de.tum.workflows.pqltl.PQLTL._
+
+object WorkFlow {
+  case class Workflow(steps: List[Block]) {
+    override def toString() = steps.mkString("\n")
+  }
+
+  abstract sealed class Block
+
+  abstract class Statement
+  case class Add(guard: Term, fun: String, tuple: List[Var]) extends Statement {
+    override def toString() = guard + " → " + fun + " += " + tuple.mkString("(", ",", ")")
+  }
+  case class Remove(guard: Term, fun: String, tuple: List[Var]) extends Statement {
+    override def toString() = guard + " → " + fun + " -= " + tuple.mkString("(", ",", ")")
+  }
+
+  case class ForallBlock(agents: List[Var], steps: List[Statement]) extends Block {
+    override def toString() = "forall " + agents.mkString(",") + steps.mkString("\n  ", ";\n  ", "")
+  }
+  case class ForallMayBlock(agents: List[Var], steps: List[Statement]) extends Block {
+    override def toString() = "forall " + agents.mkString(",") + " may" + steps.mkString("\n  ", ";\n  ", "")
+  }
+}
\ No newline at end of file

scala/de/tum/workflows/pqltl/PQLTL.scala

+package de.tum.workflows.pqltl
+
+object PQLTL {
+  abstract class Term {
+    def simplify() = TermFunctions.simplify(this)
+    def freeVars() = TermFunctions.freeVars(this)
+    def removeTemporals() = TermFunctions.removeTemporals(this)
+    def everywhere(trans: PartialFunction[Term, Term]) = TermFunctions.everywhere(trans, this)
+    def assumeEmpty(name: String) = TermFunctions.assumeEmpty(this, name)
+    def annotate(name:String) = TermFunctions.annotate(this, name)
+    
+    def bracketed():String = this match {
+      case _:BinOp => "(" + this + ")"
+      case _ => this.toString()
+    }
+  }
+
+  case object True extends Term
+  case object False extends Term
+
+  case class Var(name: String) extends Term {
+    override def toString() = name
+  }
+  
+  object Fun {
+    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("(", ",", ")")
+  }
+
+  trait Quantifier extends Term {
+    def qmake: (List[Var], Term) => Quantifier
+    def qname: String
+    def vars: List[Var]
+    def t: Term
+    
+    override def toString() = {
+      qname + " " + vars.mkString(",") + ". " + t.bracketed()
+    }
+  }
+  
+  object Quantifier {
+    def unapply(q: Quantifier) = Some((q.qmake, q.vars, q.t))
+  }
+
+  case class Exists(vars: List[Var], t: Term) extends Quantifier {
+    val qname = "∃"
+    val qmake = Exists.apply _
+  }
+  case class Forall(vars: List[Var], t: Term) extends Quantifier {
+    val qname = "∀"
+    val qmake = Forall.apply _
+  }
+
+  trait TemporalTerm extends Term
+
+  case class Previously(t:Term) extends TemporalTerm {
+    override def toString() = {
+      "Prev " + t.bracketed()
+    }
+  }
+  case class Historically(t: Term) extends TemporalTerm {
+    override def toString() = {
+      "A " + t.bracketed()
+    }
+  }
+  case class Since(t1: Term, t2: Term) extends TemporalTerm {
+    override def toString() = {
+      t1.bracketed() + " S " + t2.bracketed()
+    }
+  }
+  case class Once(t: Term) extends TemporalTerm
+
+  trait BinOp extends Term {
+    def make:(Term, Term) => BinOp
+    def opname: String
+    def t1: Term
+    def t2: Term 
+    
+    override def toString() = {
+      (t1, t2) match {
+        case (t1: BinOp, t2:BinOp) if (opname == t1.opname == t2.opname) => t1 + " " + opname + " " + t2
+        case (t1: BinOp, _) if (opname == t1.opname) => t1 + " " + opname + " " + t2.bracketed()
+        case (_, t2:BinOp) if (opname == t2.opname) => t1.bracketed() + " " + opname + " " + t2
+        case _ => t1.bracketed() + " " + opname + " " + t2.bracketed()
+      }
+    }
+  }
+  
+  object BinOp {
+    def unapply(binop: BinOp) = {
+      Some((binop.make, binop.t1, binop.t2))
+    }
+  }
+
+  case class Or(t1: Term, t2: Term) extends BinOp {
+    val opname = "∨"
+    val make = Or.apply _
+  }
+  case class And(t1: Term, t2: Term) extends BinOp {
+    val opname = "∧"
+    val make = And.apply _
+  }
+  case class Eq(t1: Term, t2:Term) extends BinOp {
+    val opname = "↔"
+    val make = Eq.apply _
+  }
+
+  trait UnOp extends Term {
+    def opname: String
+    def t: Term
+    
+    override def toString() = opname + t.bracketed
+  }
+
+  case class Neg(t: Term) extends UnOp {
+    val opname = "¬"
+  }
+
+}
\ No newline at end of file

scala/de/tum/workflows/pqltl/PQLTLTermfunctions.scala

+package de.tum.workflows.pqltl
+
+import PQLTL._
+
+object TermFunctions {
+
+  def freeVars(t: Term) = {
+    def free(t: Term, bound: Set[Var]): Set[Var] = {
+      t match {
+        // Extractors
+        // Exists, Forall
+        case Quantifier(_, ps, t)  => free(t, bound ++ ps)
+        case Since(t1, t2)         => free(t1, bound) ++ free(t2, bound)
+        case Once(t1)              => free(t1, bound)
+        case Historically(t1)      => free(t1, bound)
+        // And, Or, Eq
+        case BinOp(_, t1, t2)      => free(t1, bound) ++ free(t2, bound)
+        case Neg(t1)               => free(t1, bound)
+
+        case Fun(_, Some(ind), ps) => (ps.toSet -- bound) + Var(ind)
+        case Fun(_, _, ps)         => (ps.toSet -- bound)
+        case v: Var if !bound(v)   => Set(v)
+        case x                     => Set()
+      }
+    }
+
+    free(t, Set())
+  }
+
+  def simplify(t: Term): Term = {
+    val simp: PartialFunction[Term, Term] = {
+      // Push negation inward
+      case Neg(Or(t1, t2))                        => And(Neg(t1), Neg(t2))
+      case Neg(And(t1, t2))                       => Or(Neg(t1), Neg(t2))
+      case Neg(Historically(t))                   => Once(Neg(t))
+      case Neg(Once(t))                           => Historically(Neg(t))
+      case Neg(Previously(t))                     => Previously(Neg(t))
+      case Neg(Forall(vars, t))                   => Exists(vars, Neg(t))
+      case Neg(Exists(vars, t))                   => Forall(vars, Neg(t))
+
+      // Simple laws
+      case Neg(True)                              => False
+      case Neg(False)                             => True
+      case Or(True, t)                            => True
+      case Or(t, True)                            => True
+      case Or(False, t)                           => t
+      case Or(t, False)                           => t
+      case And(False, t)                          => False
+      case And(t, False)                          => False
+      case And(True, t)                           => t
+      case And(t, True)                           => t
+
+      case Eq(False, False)                       => True
+
+      case Neg(Neg(t))                            => t
+      // TODO: Since
+
+      // Remove quantifiers if empty
+      case Quantifier(qmake, xs, t) if xs.isEmpty => t
+      case Quantifier(qmake, xs, True)            => True
+      case Quantifier(qmake, xs, False)           => False
+
+      // Remove variables from quantifiers if not used in the body
+      //      case Quantifier(qmake, xs, t) if !(xs.toSet -- t.freeVars()).isEmpty =>
+      //        qmake((xs.toSet.intersect(t.freeVars())).toList, t)
+      //
+      //      // Split off binops from quantifiers
+      //      case Quantifier(qmake, xs, BinOp(make, t1, t2)) if (t1.freeVars().intersect(xs.toSet)).isEmpty =>
+      //        make(t1, qmake(xs, t2))
+      //      case Quantifier(qmake, xs, BinOp(make, t1, t2)) if (t2.freeVars().intersect(xs.toSet)).isEmpty =>
+      //        make(qmake(xs, t1), t2)
+    }
+
+    val t1 = everywhere(simp, t)
+    if (t == t1) t1 else simplify(t1)
+  }
+
+  def everywhere(trans: PartialFunction[Term, Term], t: Term): Term = {
+    if (trans.isDefinedAt(t))
+      trans(t)
+    else
+      t match {
+        // Extractors
+        case Quantifier(make, ps, t) => make(ps, everywhere(trans, t))
+        case Since(t1, t2)           => Since(everywhere(trans, t1), everywhere(trans, t2))
+        case Once(t1)                => Once(everywhere(trans, t1))
+        case Historically(t1)        => Historically(everywhere(trans, t1))
+        case Previously(t1)          => Previously(everywhere(trans, t1))
+        case BinOp(make, t1, t2)     => make(everywhere(trans, t1), everywhere(trans, t2))
+        case Neg(t1)                 => Neg(everywhere(trans, t1))
+
+        case x                       => x
+      }
+  }
+
+  def removeTemporals(t: Term): Term = {
+    t.everywhere({
+      case Historically(u) => u
+      case Since(u, v)     => v
+      case Once(u)         => u
+      case _: TemporalTerm => False
+
+    })
+  }
+
+  def assumeEmpty(t: Term, name: String) = {
+    t.everywhere({
+      case Fun(f, _, _) if f == name => False
+    })
+  }
+
+  def annotate(t: Term, name: String) = {
+    t.everywhere({
+      case Fun(f, None, xs) => Fun(f, Some(name), xs)
+    })
+  }
+}
\ No newline at end of file

src/main/scala/de/tum/workflows/Implicits.scala

+package de.tum.workflows
+
+import de.tum.workflows.foltl.FOLTL._
+
+object Implicits {
+  implicit def toList[A](v: A): List[A] = List(v)
+
+  // Logic
+  implicit def nameToVar(name: String) = Var(name)
+  
+  implicit def nameToVarList(name: String) = List(Var(name))
+}

src/main/scala/de/tum/workflows/Main.scala

+package de.tum.workflows
+
+import foltl.FOLTL._
+import blocks.WorkFlow._
+import Implicits._
+
+object Main extends App {
+
+  val w = Workflow(List(
+      ForallMayBlock(List("x","s"),
+          Add(Fun("O","s"),"Q", List("x","s"))
+      ),
+      Loop(List(
+          ForallMayBlock(List("x","y","s"),
+              Add(Fun("R", List("y","s")), "S", List("x","y","s"))
+          ),
+          ForallBlock(List("x","s"),
+              Add(Fun("Q",List("x","s")), "R", List("x","s"))
+          )
+      ))
+  ))
+  println(w)
+  
+  val res = Encoding.toFOLTL(w)
+}
\ No newline at end of file

src/main/scala/de/tum/workflows/WorkflowEncoding.scala

+package de.tum.workflows
+
+import scalax.collection.Graph // or scalax.collection.mutable.Graph
+import scalax.collection.GraphPredef._
+import scalax.collection.GraphEdge._
+import scalax.collection.edge.LDiEdge     // labeled directed edge
+import scalax.collection.edge.Implicits._ // shortcuts
+
+import blocks.WorkFlow._
+import de.tum.workflows.foltl.FOLTL
+import de.tum.workflows.foltl.FOLTL._
+import de.tum.workflows.foltl.TermFunctions._
+
+import scalax.collection.edge.LBase.LEdgeImplicits
+object BlockImplicit extends LEdgeImplicits[SimpleBlock]; import BlockImplicit._
+
+
+object Encoding {
+
+  // Naming
+  // TODO: make sure there are no clashes
+  def nodeVar(n: Any) = Var("n" + n)
+  def choiceVar(n: Any) = "choice" + n
+  
+  def makeblock(b: Block, n1: Int, n2:Int, makeNode: (() => Int), makeId: (() => Block)):(List[LDiEdge[Int]]) = {
+    
+    b match {
+      case Loop(steps) => {
+        // add empty statement if loop ends with loop
+        val adjsteps = steps.last match {
+          case _:Loop => steps :+ makeId()
+          case _:Block => steps
+        }
+        // looping with n-1 nodes around n1
+        val newnodes = n1 +: (0 until adjsteps.size -1).toList.map(_ => makeNode()) :+ n1
+
+        // n1 -> n2, n2 -> n3, ...
+        val edgenodes = newnodes.sliding(2).toList
+        val edges = for ((step,List(start, end)) <- adjsteps.zip(edgenodes)) yield {
+          makeblock(step, start, end, makeNode, makeId)
+        }
+        edges.flatten :+ (n1 ~+> n2)(makeId())
+      }
+      // single edge
+      case b:Block => {
+        List((n1 ~+> n2)(b))
+      }
+    }
+  }
+  
+  def toGraph(w: Workflow) = {
+    
+    var n1 = 0;
+    def newnode() = {
+      n1 = n1 + 1
+      n1
+    }
+    def makeid() = ForallBlock(List(), List())
+    
+    val edges = (for ((step,i) <- w.steps.zipWithIndex) yield {
+      if (i == w.steps.size - 1) {
+        val n = n1
+        val n2 = newnode()
+        val edges = makeblock(step, n, n2, newnode, makeid)
+        edges :+ (n2 ~+> n2)(makeid())
+      } else {
+        makeblock(step, n1, newnode(), newnode, makeid)
+      }
+    }).flatten
+    var nodes = (0 until n1).toList
+    
+    
+    
+    Graph.from(nodes, edges)
+  }
+  
+  def encodeGraph(g:Graph[Int, LDiEdge]) = {
+    val allnodes = for (n <- g.nodes.toList) yield {
+        // TODO: better syntax
+        val list = n.outgoing.toList.map(e => nodeVar(e.to))
+        Implies(nodeVar(n), Next(BinOp.makeL(Or.apply, list)))
+    }
+    Globally(BinOp.makeL(And.apply, allnodes))
+  }
+  
+  def encodeSanity(g: Graph[Int, LDiEdge]) = {
+    val negs = for (n <- g.nodes.toList; n2 <- g.nodes.toList if n < n2) yield {
+      Neg(And(nodeVar(n), nodeVar(n2)))
+    }
+    Globally(BinOp.makeL(And.apply, negs))
+  }
+