Commit 32501d18 authored by Christian Müller's avatar Christian Müller

add ts parsing first steps

parent ce65cda4
Signature
EmptyPredicates
R(a:T,b:T), S(a:T, b:T)
AxiomPredicates
I(b:T)
As
A(b:T)
Bs
B(b:T)
Constants
ca:T, cb:T
Transition System
loop {
sim {
R(a,b) := A(a,b)
S(c,d) := R(a,b)
}
S(a,b) := False
}
Invariant
True
Axioms
True
Manifest-Version: 1.0
Main-Class: de.tum.workflows.LTLCLI
Main-Class: de.tum.niwo.LTLCLI
package de.tum.workflows
package de.tum.niwo
import scalax.collection.Graph
import scalax.collection.GraphPredef._
......@@ -6,15 +6,15 @@ import scalax.collection.GraphEdge._
import scalax.collection.edge.LDiEdge
import scalax.collection.edge.Implicits._
import blocks._
import de.tum.workflows.foltl.{FOLTL, Properties}
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.FormulaFunctions._
import de.tum.niwo.foltl.{FOLTL, Properties}
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.FormulaFunctions._
import com.typesafe.scalalogging._
import scalax.collection.edge.LBase.LEdgeImplicits
import scalax.collection.io.dot._
import implicits._
import Implicits._
import de.tum.workflows.toz3.InvProperties
import de.tum.niwo.toz3.InvProperties
import scalax.collection.GraphTraversal.{BreadthFirst, DepthFirst}
object Encoding extends LazyLogging {
......@@ -26,11 +26,11 @@ object Encoding extends LazyLogging {
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]]) = {
def makeblock(b: WFBlock, n1: Int, n2: Int, makeNode: (() => Int), makeId: (() => WFBlock)): (List[LDiEdge[Int]]) = {
b match {
// single edge
case b: SimpleBlock => {
case b: SimpleWFBlock => {
List((n1 ~+> n2)(b))
}
......@@ -38,7 +38,7 @@ object Encoding extends LazyLogging {
// add empty statement if loop ends with loop
val adjsteps = steps.last match {
case _: Loop => steps :+ makeId()
case _: Block => steps
case _: WFBlock => steps
}
// looping with n-1 nodes around n1
val newnodes = n1 +: (0 until adjsteps.size - 1).toList.map(_ => makeNode()) :+ n1
......@@ -80,7 +80,7 @@ object Encoding extends LazyLogging {
n1 = n1 + 1
n1
}
def makeid() = ForallBlock(List(), List())
def makeid() = ForallWFBlock(List(), List())
val edges = (for ((step, i) <- w.steps.zipWithIndex) yield {
if (i == 0 && step.isInstanceOf[Loop]) {
......@@ -216,7 +216,7 @@ object Encoding extends LazyLogging {
def edgeTransformer(innerEdge: WorkflowGraph#EdgeT): Option[(DotGraph, DotEdgeStmt)] = innerEdge.edge match {
case LDiEdge(source, target, label) => label match {
case label: SimpleBlock => {
case label: SimpleWFBlock => {
val green = edges.exists(_ == innerEdge)
val color = List(DotAttr("color", if (green) "green" else "red"))
......
package de.tum.workflows
package de.tum.niwo
import foltl.FOLTL._
import blocks._
import Implicits._
import java.io.File
import java.io.FilenameFilter
import scala.io.Source
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.parser.WorkflowParser
object ExampleWorkflows extends LazyLogging {
......
package de.tum.workflows
package de.tum.niwo
import de.tum.workflows.foltl.FOLTL._
import de.tum.niwo.foltl.FOLTL._
import scalax.collection.edge.LBase.LEdgeImplicits
import de.tum.workflows.blocks.SimpleBlock
import de.tum.niwo.blocks.SimpleWFBlock
object Implicits extends LEdgeImplicits[SimpleBlock] {
object Implicits extends LEdgeImplicits[SimpleWFBlock] {
implicit def toList[A](v: A): List[A] = List(v)
// Logic
......
package de.tum.workflows
package de.tum.niwo
import scala.io.Source
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Utils._
import de.tum.workflows.blocks.NISpec
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.toz3.InvariantGenerator
import de.tum.workflows.toz3.InvProperties
import de.tum.niwo.Utils._
import de.tum.niwo.blocks.NISpec
import de.tum.niwo.toz3.InvariantChecker
import de.tum.niwo.toz3.InvariantGenerator
import de.tum.niwo.toz3.InvProperties
import java.io.File
import de.tum.niwo.parser.WorkflowParser
object InvariantCLI extends App with LazyLogging {
lazy val usage = """
......
package de.tum.workflows
package de.tum.niwo
import foltl.FOLTL._
import blocks.Workflow._
import Implicits._
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.foltl.FOTransformers
import de.tum.workflows.Utils._
import de.tum.workflows.foltl.Stubborn
import de.tum.workflows.foltl.Properties
import de.tum.niwo.foltl.FOTransformers
import de.tum.niwo.Utils._
import de.tum.niwo.foltl.Stubborn
import de.tum.niwo.foltl.Properties
import java.io.PrintWriter
import java.io.File
import de.tum.workflows.blocks.Workflow
import de.tum.workflows.blocks.NISpec
import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.toz3.InvariantGenerator
import de.tum.workflows.toz3.InvProperties
import de.tum.workflows.toz3.Z3QFree
import de.tum.niwo.blocks.Workflow
import de.tum.niwo.blocks.NISpec
import de.tum.niwo.foltl.FormulaFunctions
import de.tum.niwo.toz3.InvariantChecker
import de.tum.niwo.toz3.InvariantGenerator
import de.tum.niwo.toz3.InvProperties
import de.tum.niwo.toz3.Z3QFree
object InvariantInspector extends App with LazyLogging {
......
package de.tum.workflows
package de.tum.niwo
import scala.io.Source
import com.typesafe.scalalogging.LazyLogging
import java.io.File
import de.tum.niwo.parser.WorkflowParser
object LTLCLI extends App with LazyLogging {
lazy val usage = """
......
package de.tum.workflows
package de.tum.niwo
import foltl.FOLTL._
import blocks.Workflow._
import Implicits._
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Utils._
import de.tum.niwo.Utils._
import java.io.PrintWriter
import java.io.File
import de.tum.workflows.blocks.Workflow
import de.tum.workflows.blocks.NISpec
import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.toz3.InvariantChecker
import de.tum.workflows.toz3.InvariantGenerator
import de.tum.niwo.blocks.Workflow
import de.tum.niwo.blocks.NISpec
import de.tum.niwo.foltl.FormulaFunctions
import de.tum.niwo.toz3.InvariantChecker
import de.tum.niwo.toz3.InvariantGenerator
object MainInvariants extends App with LazyLogging {
......
package de.tum.workflows
package de.tum.niwo
import com.typesafe.scalalogging.LazyLogging
import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Utils._
import de.tum.workflows.blocks.{SimpleBlock, NISpec}
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.FOTransformers
import de.tum.workflows.synth.Model
import de.tum.workflows.toz3._
import de.tum.workflows.foltl.Properties
import de.tum.niwo.Utils._
import de.tum.niwo.blocks.{SimpleWFBlock, NISpec}
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.FOTransformers
import de.tum.niwo.synth.Model
import de.tum.niwo.toz3._
import de.tum.niwo.foltl.Properties
// Labelled Edge to Block
import Implicits._
......
package de.tum.workflows
package de.tum.niwo
import com.microsoft.z3.Status
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Utils._
import de.tum.workflows.blocks.{SimpleBlock, NISpec}
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.FOTransformers
import de.tum.workflows.synth.Model
import de.tum.workflows.toz3._
import de.tum.workflows.foltl.Properties
import de.tum.niwo.Utils._
import de.tum.niwo.blocks.{SimpleWFBlock, NISpec}
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.FOTransformers
import de.tum.niwo.synth.Model
import de.tum.niwo.toz3._
import de.tum.niwo.foltl.Properties
// Labelled Edge to Block
import Implicits._
......
package de.tum.workflows
package de.tum.niwo
import foltl.FOLTL._
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.foltl.FOTransformers
import de.tum.workflows.Utils._
import de.tum.workflows.foltl.Properties
import de.tum.workflows.blocks.NISpec
import de.tum.workflows.foltl.FormulaFunctions
import de.tum.workflows.foltl.FOTransformers
import de.tum.workflows.owltransformer.OwlTransformer
import de.tum.niwo.foltl.FOTransformers
import de.tum.niwo.Utils._
import de.tum.niwo.foltl.Properties
import de.tum.niwo.blocks.NISpec
import de.tum.niwo.foltl.FormulaFunctions
import de.tum.niwo.foltl.FOTransformers
import de.tum.niwo.owltransformer.OwlTransformer
import owl.ltl.algorithms.LanguageAnalysis
import owl.ltl.rewriter.SimplifierFactory
......
package de.tum.workflows
package de.tum.niwo
import com.typesafe.scalalogging._
import blocks._
import de.tum.workflows.foltl.{FOLTL, FOTransformers, FormulaFunctions, Properties}
import de.tum.workflows.foltl.FOLTL._
import de.tum.workflows.foltl.Properties._
import de.tum.workflows.toz3.{InvProperties, Z3BSFO}
import de.tum.niwo.foltl.{FOLTL, FOTransformers, FormulaFunctions, Properties}
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.Properties._
import de.tum.niwo.toz3.{InvProperties, Z3BSFO}
object Preconditions extends LazyLogging {
private def elaborateSteps(b: SimpleBlock, spec: NISpec, properties: InvProperties): List[SimpleBlock] = {
private def elaborateSteps(b: SimpleWFBlock, spec: NISpec, properties: InvProperties): List[SimpleWFBlock] = {
val guardfix = if (!b.isoracly && b.pred.isDefined) {
// is "normal" may block
......@@ -47,14 +47,14 @@ object Preconditions extends LazyLogging {
val fun = Fun(stmt.fun, stmt.tuple)
// TODO
val guard = Neg(Equiv(fun.in(T1), fun.in(T2)))
ForallBlock(stmt.tuple, List(Add(guard, INFNAME, List(stmt.tuple.head))))
ForallWFBlock(stmt.tuple, List(Add(guard, INFNAME, List(stmt.tuple.head))))
}
newb :: newsteps
}
}
// For oracly blocks, remove O from guard and add to ForallMay choice predicate
private def elaborateOraclyBlock(b: SimpleBlock, spec: NISpec) = {
private def elaborateOraclyBlock(b: SimpleWFBlock, spec: NISpec) = {
if (b.isoracly) {
val stmt = b.steps.head // can only be one
......@@ -89,11 +89,11 @@ object Preconditions extends LazyLogging {
case Add(guard, fun, tuple) => Add(fixguard(guard, choice).simplify, fun, tuple)
case Remove(guard, fun, tuple) => Remove(fixguard(guard, choice).simplify, fun, tuple)
}
ForallMayBlock(b.agents, name, List(newstmt))
ForallMayWFBlock(b.agents, name, List(newstmt))
} else b
}
def subst(f: Formula, updates: List[(String, (List[FOLTL.Var], FOLTL.Formula))], b: SimpleBlock): Formula = {
def subst(f: Formula, updates: List[(String, (List[FOLTL.Var], FOLTL.Formula))], b: SimpleWFBlock): Formula = {
// TODO: should this contain f.freeVars?
val boundvars = f.boundVars
updates.foldRight(f)((update, f) => {
......@@ -131,12 +131,12 @@ object Preconditions extends LazyLogging {
form
}
def elaborate(block: SimpleBlock, spec:NISpec, properties:InvProperties): List[SimpleBlock] = {
def elaborate(block: SimpleWFBlock, spec:NISpec, properties:InvProperties): List[SimpleWFBlock] = {
val stepOne = elaborateSteps(block, spec, properties)
stepOne map { b => elaborateOraclyBlock(b, spec) }
}
def weakestPrecondition(post: Formula, outerb: SimpleBlock, spec: NISpec, properties: InvProperties): Formula = {
def weakestPrecondition(post: Formula, outerb: SimpleWFBlock, spec: NISpec, properties: InvProperties): Formula = {
// TODO: Make 2-trace elaboration optional
......@@ -149,7 +149,7 @@ object Preconditions extends LazyLogging {
precond
}
private def weakestPreconditionSingle(f: Formula, b:SimpleBlock, spec: NISpec, properties: InvProperties) = {
private def weakestPreconditionSingle(f: Formula, b:SimpleWFBlock, spec: NISpec, properties: InvProperties) = {
val updates = for (s <- b.steps) yield {
s.fun -> (s.tuple, {
......@@ -174,7 +174,7 @@ object Preconditions extends LazyLogging {
removed
}
def abstractedPrecondition(f: Formula, b: SimpleBlock, spec: NISpec, properties: InvProperties, untouched: Set[String]): Formula = {
def abstractedPrecondition(f: Formula, b: SimpleWFBlock, spec: NISpec, properties: InvProperties, untouched: Set[String]): Formula = {
val precond = weakestPrecondition(f, b, spec, properties)
// Assume untouched predicates empty
......
package de.tum.workflows
package de.tum.niwo
import de.tum.workflows.blocks._
import de.tum.workflows.foltl.FOLTL._
import de.tum.niwo.blocks._
import de.tum.niwo.foltl.FOLTL._
import java.io.File
import java.io.PrintWriter
import de.tum.workflows.toz3.{InvProperties, InvariantChecker, Z3BSFO}
import de.tum.niwo.toz3.{InvProperties, InvariantChecker, Z3BSFO}
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.MainInvariantsInference.logger
import de.tum.niwo.MainInvariantsInference.logger
object Utils extends LazyLogging {
......@@ -18,11 +18,11 @@ object Utils extends LazyLogging {
if (string.isEmpty) "" else string.mkString(start, mid, end)
}
def collectChoices(w: Block): List[Fun] = {
def collectChoices(w: WFBlock): List[Fun] = {
w match {
case Loop(steps) => steps.flatMap(collectChoices)
case ForallMayBlock(agents, pred, _) => List(Fun(pred, agents))
case b: ForallBlock => List()
case ForallMayWFBlock(agents, pred, _) => List(Fun(pred, agents))
case b: ForallWFBlock => List()
case NondetChoice(l, r) => l.flatMap(collectChoices) ++ r.flatMap(collectChoices)
}
}
......
package de.tum.niwo.blocks;
import de.tum.niwo.Utils
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.Properties
case class Signature(as: Set[Fun], constas: Set[Fun], bs: Set[Fun], preds: Set[Fun], constants: Set[Var])
object Signature {
val EMPTY = Signature(Set(), Set(), Set(), Set(), Set())
}
case class TransitionSystem(sig: Signature, steps: List[TSBlock]) {
override def toString: String = steps.mkString("\n")
}
object TransitionSystem {
val EMPTY = TransitionSystem(Signature.EMPTY, List())
}
trait Spec {
def axioms: Formula
}
case class InvariantSpec(ts:TransitionSystem, axioms:Formula, inv:Formula) extends Spec {
override def toString: String = {
s"InvSpec\nTransition System:\n$ts\n\nAxioms:\n$axioms\n\nInvariant:$inv"
}
def addAxiom(k:Formula) = {
InvariantSpec(ts, And.make(axioms, k), inv)
}
def addInv(k:Formula) = {
InvariantSpec(ts, axioms, And.make(inv, k))
}
}
object InvariantSpec {
val EMPTY = InvariantSpec(TransitionSystem.EMPTY, True, True)
}
abstract class Statement {
type This >: this.type <: Statement
def guard: Formula
def fun: String
def tuple: List[Var]
def updateGuard(newguard: Formula): This
lazy val freeVars: Set[Var] = guard.freeVars ++ tuple
}
case class Add(guard: Formula, fun: String, tuple: List[Var]) extends Statement {
type This = Add
override def toString: String = guard + " → " + fun + " += " + tuple.mkString("(", ",", ")") + ";"
override def updateGuard(newguard: Formula) = Add(newguard, fun, tuple)
}
case class Remove(guard: Formula, fun: String, tuple: List[Var]) extends Statement {
type This = Remove
override def toString: String = guard + " → " + fun + " -= " + tuple.mkString("(", ",", ")") + ";"
override def updateGuard(newguard: Formula) = Remove(newguard, fun, tuple)
}
case class SetStmt(guard:Formula, fun:String, tuple: List[Var]) extends Statement {
type This = SetStmt
override def toString: String = guard + " → " + fun + " := " + tuple.mkString("(", ",", ")") + ";"
override def updateGuard(newguard: Formula) = SetStmt(newguard, fun, tuple)
}
trait Block
trait SimpleBlock extends Block {
type This >: this.type <: SimpleBlock
type SType <: Statement
def steps: List[SType]
def updating:Set[String] = {
steps.map(_.fun).toSet
}
def updateSteps(s:List[SType]):This
}
trait TSBlock extends Block
trait Loop extends Block {
def steps:List[Block]
override def toString: String = {
// indentation
"loop {\n" + Utils.indentLines(steps.mkString("\n") + "\n}\n")
}
}
trait NondetChoice extends Block {
def left: List[Block]
def right: List[Block]
override def toString: String = {
"choose {\n" + Utils.indentLines(left.mkString("\n")) +
"\n} or {\n" + Utils.indentLines(right.mkString("\n")) + "\n}\n"
}
}
case class SimpleTSBlock(steps: List[SetStmt]) extends SimpleBlock with TSBlock {
type This = TSBlock
type SType = SetStmt
override def toString: String = steps.mkString("{", "\n ", "}")
override def updateSteps(newsteps: List[SetStmt]) = SimpleTSBlock(newsteps)
}
case class TSLoop(steps:List[TSBlock]) extends Loop with TSBlock
case class TSNondetChoice(left:List[TSBlock], right:List[TSBlock]) extends NondetChoice with TSBlock
package de.tum.workflows.blocks
package de.tum.niwo.blocks
import de.tum.workflows.foltl.FOLTL._
import de.tum.niwo.foltl.FOLTL._
import com.typesafe.scalalogging.LazyLogging
import de.tum.workflows.Utils
import de.tum.workflows.foltl.Properties
import de.tum.niwo.Utils
import de.tum.niwo.foltl.Properties
case class Signature(as: Set[Fun], constas: Set[Fun], bs: Set[Fun], preds: Set[Fun])
object Signature {
val EMPTY = Signature(Set(), Set(), Set(), Set())
}
case class Workflow(sig: Signature, steps: List[Block]) {
override def toString(): String = steps.mkString("\n")
case class Workflow(sig: Signature, steps: List[WFBlock]) {
override def toString: String = steps.mkString("\n")
lazy val isomitting: Boolean = {
steps.exists(_.isomitting)
def omitting(b:Block):Boolean = { b match {
case l: WFLoop => l.steps.exists(omitting)
case c: WFNondetChoice => c.left.exists(omitting) || c.right.exists(omitting)
case s: SimpleWFBlock => s.steps.exists(stmt => s.agents.exists(a => !stmt.tuple.contains(a)))
}
}
steps.exists(omitting)
}
}
object Workflow {
val EMPTY = Workflow(Signature.EMPTY, List())
}
trait Spec {
def w: Workflow
}
case class NISpec(w: Workflow, declass: Map[String, (List[Var], Formula)], always: Formula, target: Fun, causals:List[Var]) extends Spec with LazyLogging {
case class NISpec(w: Workflow, declass: Map[String, (List[Var], Formula)], axioms: Formula, target: Fun, causals:List[Var]) extends Spec with LazyLogging {
override def toString: String = {
s"NISpec\nWorkflow:\n$w\nDeclass:$declass\nTarget:$target"
}
......@@ -72,7 +70,7 @@ case class NISpec(w: Workflow, declass: Map[String, (List[Var], Formula)], alway
// check same relation only updated once per block
def isSane(steps:List[Block]):Boolean = {
val sanes = steps map {
case b: SimpleBlock => {
case b: SimpleWFBlock => {
// all predicates should only appear at most once
val pred = w.sig.preds.find(p => b.steps.count(s => s.fun == p.name) > 1)
pred.foreach(p =>
......@@ -85,11 +83,12 @@ case class NISpec(w: Workflow, declass: Map[String, (List[Var], Formula)], alway
if (!saneoracly) { logger.warn(s"Oracles used wrongly in $b") }
pred.isEmpty && saneoracly
}
case Loop(steps) => isSane(steps)
case NondetChoice(left, right) => isSane(left) && isSane(right)
case WFLoop(blocks) => isSane(blocks)
case WFNondetChoice(left, right) => isSane(left) && isSane(right)
}
sanes reduce (_ && _)
}
sane &&= isSane(w.steps)
sane
}
......@@ -102,24 +101,24 @@ object NISpec {
val EMPTY = NISpec(Workflow.EMPTY, Map(), True, Fun("NOTHING", List()), List())
}
abstract sealed class Block {
def isomitting: Boolean
}
abstract sealed class SimpleBlock extends Block {
type This >: this.type <: SimpleBlock
trait WFBlock extends Block
abstract sealed class SimpleWFBlock extends SimpleBlock with WFBlock {
def agents: List[Var]
def steps: List[Statement]
def may: Boolean
def pred: Option[String]
def updateSteps(s:List[Statement]):This
override def isomitting: Boolean = {
// a simple block is omitting, if there exists a statement where not all agents appear in the tuple
steps.exists(s => agents.exists(a => !s.tuple.contains(a)))
override def updating:Set[String] = {
// This works because of the way the untouchedmap is computed.
// As soon as that changes, fix here.
if (isoracly) {
super.updating + Properties.INFNAME
} else {
super.updating
}
}
def isoracly: Boolean = {
// before transformation
val before = steps.exists(s => {
......@@ -132,70 +131,22 @@ abstract sealed class SimpleBlock extends Block {
before || after
}
def updating:Set[String] = {
// This works because of the way the untouchedmap is computed.
// As soon as that changes, fix here.
if (isoracly) {
steps.map(_.fun).toSet + Properties.INFNAME
} else {
steps.map(_.fun).toSet
}
}
}
abstract class Statement {
type This >: this.type <: Statement
def guard: Formula
def fun: String
def tuple: List[Var]
def updateGuard(newguard: Formula): This
lazy val freeVars: Set[Var] = guard.freeVars ++ tuple
}
case class Add(guard: Formula, fun: String, tuple: List[Var]) extends Statement {
type This = Add
override def toString(): String = guard + " → " + fun + " += " + tuple.mkString("(", ",", ")") + ";"
override def updateGuard(newguard: Formula) = Add(newguard, fun, tuple)
}
case class Remove(guard: Formula, fun: String, tuple: List[Var]) extends Statement {
type This = Remove
override def toString(): String = guard + " → " + fun + " -= " + tuple.mkString("(", ",", ")") + ";"
override def updateGuard(newguard: Formula) = Remove(newguard, fun, tuple)
}
case class ForallBlock(agents: List[Var], steps: List[Statement]) extends SimpleBlock {
type This = ForallBlock