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

add transition system parsing

parent 8e7f3d1f
package de.tum.niwo
import scalax.collection.Graph
import scalax.collection.GraphPredef._
import scalax.collection.GraphEdge._
import scalax.collection.edge.LDiEdge
import scalax.collection.edge.Implicits._
import blocks._
import de.tum.niwo.foltl.{FOLTL, Properties}
import de.tum.niwo.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.niwo.toz3.InvProperties
import scalax.collection.GraphTraversal.{BreadthFirst, DepthFirst}
import scalax.collection.GraphTraversal.BreadthFirst
object Encoding extends LazyLogging {
......@@ -26,19 +22,22 @@ object Encoding extends LazyLogging {
def nodeVar(n: Any) = Fun("n" + n, List())
def choiceVar(n: Any) = "choice" + n
def makeblock(b: WFBlock, n1: Int, n2: Int, makeNode: (() => Int), makeId: (() => WFBlock)): (List[LDiEdge[Int]]) = {
def toBlock(e:WorkflowGraph#EdgeT):SimpleWFBlock[_] = e
def toNumber(n:WorkflowGraph#NodeT):Int = n.toOuter
def makeblock[BL <: Block](b: BL, n1: Int, n2: Int, makeNode: () => Int, makeId: () => BL): List[LDiEdge[Int]] = {
b match {
// single edge
case b: SimpleWFBlock => {
case b: SimpleBlock[_, _] => {
List((n1 ~+> n2)(b))
}
case Loop(steps) => {
case l:Loop[_, _] => {
// add empty statement if loop ends with loop
val adjsteps = steps.last match {
case _: Loop => steps :+ makeId()
case _: WFBlock => steps
val adjsteps = l.steps.last match {
case _: Loop[_, _] => l.steps :+ makeId()
case _ => l.steps
}
// looping with n-1 nodes around n1
val newnodes = n1 +: (0 until adjsteps.size - 1).toList.map(_ => makeNode()) :+ n1
......@@ -51,7 +50,9 @@ object Encoding extends LazyLogging {
edges.flatten :+ (n1 ~+> n2)(makeId())
}
case NondetChoice(l1, l2) => {
case nd:NondetChoice[_, _] => {
val l1 = nd.left
val l2 = nd.right
// make sure that at least one of the two branches has one node, so they will never build 2 edges between the same node
val newl1 = if (l1.length == l2.length && l1.length == 1) {
l1 :+ makeId()
......@@ -72,6 +73,8 @@ object Encoding extends LazyLogging {
}
}
def toGraph(w: Workflow): WorkflowGraph = {
var n1 = 0
......@@ -83,7 +86,7 @@ object Encoding extends LazyLogging {
def makeid() = ForallWFBlock(List(), List())
val edges = (for ((step, i) <- w.steps.zipWithIndex) yield {
if (i == 0 && step.isInstanceOf[Loop]) {
if (i == 0 && step.isInstanceOf[Loop[_, _]]) {
logger.info("Found loop in the initial step")
val n = n1
val n2 = newnode()
......@@ -109,114 +112,17 @@ object Encoding extends LazyLogging {
Graph.from(nodes, edges)
}
def encodeGraph(g: WorkflowGraph) = {
val allnodes = for (n <- g.nodes.toList) yield {
val list = n.outgoing.toList.map(e => nodeVar(e.to))
Implies(nodeVar(n), Next(Or.make(list: _*)))
}
Globally(And.make(allnodes))
}
def encodeSanity(g: WorkflowGraph) = {
val negs = for (n <- g.nodes.toList; n2 <- g.nodes.toList if n < n2) yield {
Neg(And(nodeVar(n), nodeVar(n2)))
}
val nodes = for (n <- g.nodes.toList if !(n == 0)) yield {
Neg(nodeVar(n))
}
And.make(nodeVar(0), And.make(nodes), Globally(And.make(negs)))
}
def encodeStmt(s: Statement, pred: Option[Formula], bind: List[Var]): (Formula, String) = {
// var guard = s.guard
// for (p <- pred) { // if pred defined
// guard = And(guard, p)
// }
val list = List(s.guard) ++ pred.toList
val guard = And.make(list)
// omitted variables
val omitted = (bind toSet) -- (s.tuple toSet)
val t = s match {
case Add(_, f, tup) if omitted.isEmpty => Or(Fun(f, tup), guard)
case Add(_, f, tup) => Or(Fun(f, tup), Exists(omitted toList, guard))
case Remove(_, f, tup) if omitted.isEmpty => And(Fun(f, tup), Neg(guard))
case Remove(_, f, tup) => And(Fun(f, tup), Exists(omitted toList, Neg(guard)))
}
(Forall(s.tuple, Equiv(Next(Fun(s.fun, s.tuple)), t)), s.fun)
}
def encodeStaying(target: Fun) = {
Forall(target.params, Equiv(Next(target), target))
}
def encodeSem(sig: Signature, g: Graph[Int, LDiEdge]) = {
val impls = for (e <- g.edges.toList) yield {
val choice = e.pred.map(n => Fun(n, e.agents))
val bound = e.agents
val res = for (s <- e.steps) yield {
encodeStmt(s, choice, e.agents)
}
val updates = res.map(_._2)
val staying = for (f <- sig.preds if !updates.contains(f.name)) yield {
encodeStaying(f)
}
val terms = res.map(_._1) ++ staying
Implies(And(nodeVar(e.from), Next(nodeVar(e.to))), And.make(terms))
}
Globally(And.make(impls))
}
def encodeInitial(sig: Signature, g: Graph[Int, LDiEdge]) = {
val empties = for (f <- sig.preds toList) yield {
Forall(f.params, Neg(f))
}
And.make(empties)
}
def sanecfg(g: Graph[Int, LDiEdge]) = {
And(encodeGraph(g), encodeSanity(g))
}
def exec(sig: Signature, g: Graph[Int, LDiEdge]) = {
And(encodeInitial(sig, g), encodeSem(sig, g))
}
def nodepredicates(g: Graph[Int, LDiEdge]) = {
// toSet because the initial set is mutable
g.nodes map nodeVar toSet
}
// def toFOLTL(w: Workflow) = {
// val g = toGraph(w)
// logger.info("Graph of w:\n" + g)
//
// val cfg = encodeGraph(g)
// logger.info(s"cfg(w): $cfg")
// val sanity = encodeSanity(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")
//
// And.make(List(cfg, sanity, sem, init))
// }
val MAXINVLENGTH = 800
def toDot(g: WorkflowGraph, elaboration:Option[(InvProperties, NISpec)] = None)(labels:Map[Int, String], edges:Set[g.EdgeT]) = {
val root = DotRootGraph(
directed = true,
id = Some("Invariant Labelling"))
id = Some("Invariant Labelling")
)
def edgeTransformer(innerEdge: WorkflowGraph#EdgeT): Option[(DotGraph, DotEdgeStmt)] = innerEdge.edge match {
case LDiEdge(source, target, label) => label match {
case label: SimpleWFBlock => {
case label: SimpleWFBlock[_] => {
val green = edges.exists(_ == innerEdge)
val color = List(DotAttr("color", if (green) "green" else "red"))
......
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
import de.tum.niwo.parser.{TransitionSystemParser, WorkflowParser}
object ExampleWorkflows extends LazyLogging {
val FOLDER = new File("examples")
val ENDING = ".spec"
object Examples extends LazyLogging {
private val BASE = new File("examples/").toPath
private val WFFOLDERS = List("tests/", "omitting/", "nonomitting/")
private val TSFOLDERS = List("tstests/")
private val ENDING = ".spec"
def listExamples(prefix:String, folder:File):Map[String,File] = {
val sublists = (for (f <- folder.listFiles if f.isDirectory()) yield {
listExamples(s"$prefix${f.getName}/", f)
}) flatten
def listExamples(folder:File):Map[String,File] = {
val sublists = (for (f <- folder.listFiles if f.isDirectory) yield {
listExamples(f)
}).flatten
val here = (for (f <- folder.listFiles() if f.isFile() && f.getName.endsWith(ENDING)) yield {
prefix + f.getName.replace(ENDING, "") -> f
}) toList
val here = (for (f <- folder.listFiles() if f.isFile && f.getName.endsWith(ENDING)) yield {
val name = BASE.relativize(f.toPath).toString.stripSuffix(ENDING)
name -> f
}).toList
(sublists toMap) ++ here
sublists.toMap ++ here
}
def parseExample(s:String):Option[NISpec] = {
if (!examples.contains(s)) {
def parseExampleWF(s:String):Option[NISpec] = {
if (!wfexamples.contains(s)) {
logger.error(s"$s not contained in list of examples")
None
} else {
val f = examples(s)
val f = wfexamples(s)
val source = Source.fromFile(f).mkString
val spec = WorkflowParser.parseSpec(source)
if (!spec.successful) {
......@@ -49,8 +51,8 @@ object ExampleWorkflows extends LazyLogging {
}
}
def parsedExamples(prefix:String, folder:File):Map[String, NISpec] = {
val map = for ((name, f) <- examples) yield {
def parsedWFExamples():Map[String, NISpec] = {
val map = for ((name, f) <- wfexamples) yield {
val s = Source.fromFile(f).mkString
val spec = WorkflowParser.parseSpec(s)
......@@ -70,10 +72,59 @@ object ExampleWorkflows extends LazyLogging {
}
// filter out all empty specs and those that are not sane
for ((k, v) <- map if (v.isDefined)) yield {
for ((k, v) <- map if v.isDefined) yield {
(k, v.get)
}
}
def parseExampleTS(s:String):Option[InvariantSpec] = {
if (!tsexamples.contains(s)) {
logger.error(s"$s not contained in list of examples")
None
} else {
val f = tsexamples(s)
val source = Source.fromFile(f).mkString
val spec = TransitionSystemParser.parseSpec(source)
if (!spec.successful) {
logger.error(s"Parsing of $f unsuccessful: $spec")
None
} else {
if (!spec.get.isSane) {
logger.error(s"Sanity check of $f failed. Skipping file.")
None
} else {
Some(spec.get)
}
}
}
}
def parsedTSExamples():Map[String, InvariantSpec] = {
val map = for ((name, f) <- tsexamples) yield {
val s = Source.fromFile(f).mkString
logger.info(s"Parsing file $f")
val spec = TransitionSystemParser.parseSpec(s)
if (!spec.successful) {
logger.error(s"Parsing of $f unsuccessful: $spec")
name -> None
} else {
if (!spec.get.isSane) {
logger.error(s"Sanity check of $f failed. Skipping file.")
name -> None
} else {
name -> Some(spec.get)
}
}
}
// filter out all empty specs and those that are not sane
for ((k, v) <- map if v.isDefined) yield {
(k, v.get)
}
}
val examples = listExamples("", FOLDER)
val wfexamples: Map[String, File] = WFFOLDERS.flatMap(wffolder => listExamples(new File(BASE.toFile, wffolder))).toMap
val tsexamples: Map[String, File] = TSFOLDERS.flatMap(tsfolder => listExamples(new File(BASE.toFile, tsfolder))).toMap
}
......@@ -4,7 +4,7 @@ import de.tum.niwo.foltl.FOLTL._
import scalax.collection.edge.LBase.LEdgeImplicits
import de.tum.niwo.blocks.SimpleWFBlock
object Implicits extends LEdgeImplicits[SimpleWFBlock] {
object Implicits extends LEdgeImplicits[SimpleWFBlock[_ <: SimpleWFBlock[_]]] {
implicit def toList[A](v: A): List[A] = List(v)
// Logic
......
......@@ -22,7 +22,7 @@ object InvariantInspector extends App with LazyLogging {
def inspect(name: String) {
logger.info(s"Generating $name")
val optspec = ExampleWorkflows.parseExample(name)
val optspec = Examples.parseExampleWF(name)
if (!optspec.isDefined) {
logger.error(s"Not a valid spec: $name")
......
......@@ -35,7 +35,7 @@ object MainInvariants extends App with LazyLogging {
def generateExample(name: String) {
logger.info(s"Generating $name")
val spec = ExampleWorkflows.parseExample(name)
val spec = Examples.parseExampleWF(name)
if (spec.isEmpty) {
logger.error(s"Not a valid spec: $name")
......@@ -47,7 +47,7 @@ object MainInvariants extends App with LazyLogging {
def generateAllExamples() {
clear()
// Fill results alphabetically
for (k <- ExampleWorkflows.examples.keys.toList.sorted) {
for (k <- Examples.wfexamples.keys.toList.sorted) {
generateExample(k)
}
}
......
......@@ -43,7 +43,7 @@ object MainInvariantsInference extends App with LazyLogging {
def generateExample(name: String, target: Int) {
logger.info(s"Generating $name")
val spec = ExampleWorkflows.parseExample(name)
val spec = Examples.parseExampleWF(name)
if (spec.isEmpty) {
logger.error(s"Not a valid spec: $name")
......
......@@ -139,7 +139,7 @@ object MainInvariantsInterpolation extends App with LazyLogging {
def generateExample(name: String, target: Int) {
logger.info(s"Generating $name")
val spec = ExampleWorkflows.parseExample(name)
val spec = Examples.parseExampleWF(name)
if (spec.isEmpty) {
logger.error(s"Not a valid spec: $name")
......
......@@ -91,7 +91,7 @@ object MainLTL extends App with LazyLogging {
def generateExample(name: String) {
logger.info(s"Generating $name")
val spec = ExampleWorkflows.parseExample(name)
val spec = Examples.parseExampleWF(name)
if (spec.isEmpty) {
logger.error(s"Not a valid spec: $name")
......@@ -103,7 +103,7 @@ object MainLTL extends App with LazyLogging {
def generateAllExamples() {
clear()
// Fill results alphabetically
for (k <- ExampleWorkflows.examples.keys.toList.sorted) {
for (k <- Examples.wfexamples.keys.toList.sorted) {
generateExample(k)
}
}
......
......@@ -9,13 +9,13 @@ import de.tum.niwo.toz3.{InvProperties, Z3BSFO}
object Preconditions extends LazyLogging {
private def elaborateSteps(b: SimpleWFBlock, spec: NISpec, properties: InvProperties): List[SimpleWFBlock] = {
private def elaborateSteps(b: SimpleWFBlock[_], spec: NISpec, properties: InvProperties):List[SimpleWFBlock[_]] = {
val guardfix = if (!b.isoracly && b.pred.isDefined) {
// is "normal" may block
val choice = Fun(b.pred.get, b.agents)
for (s <- b.steps) yield {
val fixed = for (s <- b.steps) yield {
val first = s.tuple.head
val inner = if (first.typ == spec.target.params.head.typ) {
if (properties.stubborn) {
......@@ -28,16 +28,18 @@ object Preconditions extends LazyLogging {
choice
}
val newguard = And(s.guard, inner)
s.updateGuard(newguard)
s.update(guard = newguard)
}
fixed
} else {
b.steps
}
val newb = b.update(guardfix)
// FIXME: wät? why do I have to cast this? this should be an inference error
val newb:Any = b.update(guardfix)
// for causality, add informedness updates
if (properties.stubborn) {
val list = if (properties.stubborn) {
List(newb)
} else {
val newsteps = for (
......@@ -51,10 +53,11 @@ object Preconditions extends LazyLogging {
}
newb :: newsteps
}
list.asInstanceOf[List[SimpleWFBlock[_]]]
}
// For oracly blocks, remove O from guard and add to ForallMay choice predicate
private def elaborateOraclyBlock(b: SimpleWFBlock, spec: NISpec) = {
private def elaborateOraclyBlock(b: SimpleWFBlock[_], spec: NISpec) = {
if (b.isoracly) {
val stmt = b.steps.head // can only be one
......@@ -93,7 +96,7 @@ object Preconditions extends LazyLogging {
} else b
}
def subst(f: Formula, updates: List[(String, (List[FOLTL.Var], FOLTL.Formula))], b: SimpleWFBlock): 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) => {
......@@ -116,7 +119,7 @@ object Preconditions extends LazyLogging {
})
}
def getUpdate(s:Statement, spec:NISpec, properties:InvProperties): Formula = {
def getUpdate(s:Statement[_], spec:NISpec, properties:InvProperties): Formula = {
val frees = s.guard.freeVars -- s.tuple.toSet -- spec.constants
......@@ -131,12 +134,12 @@ object Preconditions extends LazyLogging {
form
}
def elaborate(block: SimpleWFBlock, spec:NISpec, properties:InvProperties): List[SimpleWFBlock] = {
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: SimpleWFBlock, spec: NISpec, properties: InvProperties): Formula = {
def weakestPrecondition(post: Formula, outerb: SimpleWFBlock[_], spec: NISpec, properties: InvProperties): Formula = {
// TODO: Make 2-trace elaboration optional
......@@ -149,7 +152,7 @@ object Preconditions extends LazyLogging {
precond
}
private def weakestPreconditionSingle(f: Formula, b:SimpleWFBlock, 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 +177,7 @@ object Preconditions extends LazyLogging {
removed
}
def abstractedPrecondition(f: Formula, b: SimpleWFBlock, 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
......
......@@ -7,7 +7,6 @@ import java.io.PrintWriter
import de.tum.niwo.toz3.{InvProperties, InvariantChecker, Z3BSFO}
import com.typesafe.scalalogging.LazyLogging
import de.tum.niwo.MainInvariantsInference.logger
object Utils extends LazyLogging {
......@@ -20,15 +19,15 @@ object Utils extends LazyLogging {
def collectChoices(w: WFBlock): List[Fun] = {
w match {
case Loop(steps) => steps.flatMap(collectChoices)
case l:WFLoop => l.steps.flatMap(collectChoices)
case nd:WFNondetChoice => nd.left.flatMap(collectChoices) ++ nd.right.flatMap(collectChoices)
case ForallMayWFBlock(agents, pred, _) => List(Fun(pred, agents))
case b: ForallWFBlock => List()
case NondetChoice(l, r) => l.flatMap(collectChoices) ++ r.flatMap(collectChoices)
case _: ForallWFBlock => List()
}
}
def allchoices(w: Workflow) = {
w.steps flatMap collectChoices toSet
w.steps.flatMap(collectChoices).toSet
}
def indentLines(s: String) = {
......@@ -81,7 +80,7 @@ object Utils extends LazyLogging {
if (!res) {
val headinv = labelling.last(graph.nodes.head)
val satq = And(spec.always, Neg(headinv))
val satq = And(spec.axioms, Neg(headinv))
logger.info(s"Initial state violating the invariant: ${Z3BSFO.debugmodelBS(satq)}")
}
......@@ -122,7 +121,7 @@ ${inv.pretty.lines.map(s => " " + s).mkString("\n")}
}
def check(name:String, desc:String, inv:Formula, properties:InvProperties):Boolean = {
val spec = ExampleWorkflows.parseExample(name).get
val spec = Examples.parseExampleWF(name).get
check(name, desc, inv, spec, properties)
}
}
\ No newline at end of file
......@@ -5,7 +5,22 @@ import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.Properties
import de.tum.niwo.parser.ParserUtils
case class Signature(as: Set[Fun], constas: Set[Fun], bs: Set[Fun], preds: Set[Fun], constants: Set[Var])
case class Signature(as: Set[Fun], constas: Set[Fun], bs: Set[Fun], preds: Set[Fun], constants: Set[Var]) {
override def toString: String =
{
def mkString(set:Set[Fun]) = set.map(_.toTypedString).mkString(",")
val inner =
s"""
|EmptyPredicates:${mkString(preds)}
|AxiomPredicates:${mkString(constas)}
|As:${mkString(as)}
|Bs:${mkString(bs)}
|Constants:${constants.map(_.withType).mkString(",")}
""".stripMargin
s"Signature:\n${Utils.indentLines(inner)}"
}
}
object Signature {
val EMPTY = Signature(Set(), Set(), Set(), Set(), Set())
}
......@@ -17,9 +32,9 @@ case class TransitionSystem(sig: Signature, steps: List[TSBlock]) {
// check that the steps fit the signature
val uses = ParserUtils.allpredicates(steps)
val sanesteps = ParserUtils.checkSig(uses)
val sanesteps = ParserUtils.checkSig(sig, uses)
true
sanesteps
}
}
object TransitionSystem {
......@@ -40,67 +55,70 @@ case class InvariantSpec(ts:TransitionSystem, axioms:Formula, inv:Formula) exten
def addInv(k:Formula) = {
InvariantSpec(ts, axioms, And.make(inv, k))
}
def isSane: Boolean = {
// TODO: add sanity checking for axioms and invariant signatures
ts.isSane()
}
}
object InvariantSpec {
val EMPTY = InvariantSpec(TransitionSystem.EMPTY, True, True)
}
abstract class Statement {
abstract class Statement[T <: Statement[T]] {
def guard: Formula
def fun: String
def tuple: List[Var]
def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple): this.type
def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple): Statement[T]
def toTypedString: String
lazy val freeVars: Set[Var] = guard.freeVars ++ tuple
}
case class Add(guard: Formula, fun: String, tuple: List[Var]) extends Statement {
case class Add(guard: Formula, fun: String, tuple: List[Var]) extends Statement[Add] {
override def toString: String = guard + " → " + fun + " += " + tuple.mkString("(", ",", ")") + ";"
override def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple) = Add(guard, fun, tuple)
def toTypedString: String = guard.toTypedString + " → " + fun + " += " + tuple.map(_.withType).mkString("(", ",", ")") + ";"
override def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple) = copy(guard, fun, tuple)
}
case class Remove(guard: Formula, fun: String, tuple: List[Var]) extends Statement {
case class Remove(guard: Formula, fun: String, tuple: List[Var]) extends Statement[Remove] {
override def toString: String = guard + " → " + fun + " -= " + tuple.mkString("(", ",", ")") + ";"
override def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple) = Remove(guard, fun, tuple)
def toTypedString: String = guard.toTypedString + " → " + fun + " -= " + tuple.map(_.withType).mkString("(", ",", ")") + ";"
override def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple) = copy(guard, fun, tuple)
}
case class SetStmt(guard:Formula, fun:String, tuple: List[Var]) extends Statement {
case class SetStmt(guard:Formula, fun:String, tuple: List[Var]) extends Statement[SetStmt] {
override def toString: String = guard + " → " + fun + " := " + tuple.mkString("(", ",", ")") + ";"
override def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple) = SetStmt(guard, fun, tuple)
def toTypedString: String = guard.toTypedString + " → " + fun + " := " + tuple.map(_.withType).mkString("(", ",", ")") + ";"
override def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple) = copy(guard, fun, tuple)
}
trait Block
trait SimpleBlock extends Block {
type SType <: Statement
trait SimpleBlock[B <: SimpleBlock[B, S], S <: Statement[_]] extends Block {
def steps: List[SType]
def steps: List[S]
def updating:Set[String] = {
steps.map(_.fun).toSet
}
def update(steps:List[SType]):this.type
def update(steps:List[S]):SimpleBlock[B, S]
}
trait TSBlock extends Block
trait Loop extends Block {
type B <: Block
trait Loop[T <: Loop[T, B], B <: Block] extends Block {
def steps:List[B]
def update(steps:List[B] = steps):this.type
def update(steps:List[B] = steps):Loop[T, B]
override def toString: String = {
// indentation
"loop {\n" + Utils.indentLines(steps.mkString("\n") + "\n}\n")
}
}
trait NondetChoice extends Block {
type B <: Block