TransitionSystem.scala 3.69 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43
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]
Christian Müller's avatar
stuff  
Christian Müller committed
44
  def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple): This
45 46 47 48 49 50 51

  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("(", ",", ")") + ";"
Christian Müller's avatar
stuff  
Christian Müller committed
52
  override def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple) = Add(guard, fun, tuple)
53 54 55 56
}
case class Remove(guard: Formula, fun: String, tuple: List[Var]) extends Statement {
  type This = Remove
  override def toString: String = guard + " → " + fun + " -= " + tuple.mkString("(", ",", ")") + ";"
Christian Müller's avatar
stuff  
Christian Müller committed
57 58
  override def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple) = Remove(guard, fun, tuple)

59 60 61 62
}
case class SetStmt(guard:Formula, fun:String, tuple: List[Var]) extends Statement {
  type This = SetStmt
  override def toString: String = guard + " → " + fun + " := " + tuple.mkString("(", ",", ")") + ";"
Christian Müller's avatar
stuff  
Christian Müller committed
63
  override def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple) = SetStmt(guard, fun, tuple)
64 65 66 67 68 69 70 71 72 73 74 75 76
}

trait Block

trait SimpleBlock extends Block {
  type SType <: Statement

  def steps: List[SType]

  def updating:Set[String] = {
      steps.map(_.fun).toSet
  }

Christian Müller's avatar
stuff  
Christian Müller committed
77
  def update(steps:List[SType]):this.type
78 79 80 81 82
}

trait TSBlock extends Block

trait Loop extends Block {
Christian Müller's avatar
stuff  
Christian Müller committed
83 84 85 86
  type B <: Block

  def steps:List[B]
  def update(steps:List[B] = steps):this.type
87 88 89 90 91 92 93
  override def toString: String = {
    // indentation
    "loop {\n" + Utils.indentLines(steps.mkString("\n") + "\n}\n")
  }
}

trait NondetChoice extends Block {
Christian Müller's avatar
stuff  
Christian Müller committed
94 95 96 97 98 99
  type B <: Block

  def left: List[B]
  def right: List[B]
  def update(left:List[B] = left, right:List[B] = right):this.type

100 101 102 103 104 105 106 107 108
  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 SType = SetStmt
  override def toString: String = steps.mkString("{", "\n  ", "}")
Christian Müller's avatar
stuff  
Christian Müller committed
109
  override def update(newsteps: List[SetStmt]) = SimpleTSBlock(newsteps)
110 111
}

Christian Müller's avatar
stuff  
Christian Müller committed
112 113 114 115 116 117 118 119 120 121 122 123
case class TSLoop(steps:List[TSBlock]) extends Loop with TSBlock {
  type B = TSBlock
  override def update(steps:List[TSBlock] = steps):TSLoop = {
    TSLoop(steps)
  }
}
case class TSNondetChoice(left:List[TSBlock], right:List[TSBlock]) extends NondetChoice with TSBlock {
  type B = TSBlock
  override def update(left:List[TSBlock] = left, right:List[TSBlock] = right):TSNondetChoice = {
    TSNondetChoice(left, right)
  }
}