Commit 79a55c21 authored by Christian Müller's avatar Christian Müller

remove old code

parent a0582bfa
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)
}
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
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
}
}
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
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
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
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