TransitionSystem.scala 3.19 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 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107
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