TransitionSystem.scala 3.8 KB
Newer Older
1 2 3 4 5
package de.tum.niwo.blocks;

import de.tum.niwo.Utils
import de.tum.niwo.foltl.FOLTL._
import de.tum.niwo.foltl.Properties
Christian Müller's avatar
Christian Müller committed
6
import de.tum.niwo.parser.ParserUtils
7 8 9 10 11 12 13 14

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")
Christian Müller's avatar
Christian Müller committed
15 16 17 18 19 20 21 22 23

  def isSane() = {

    // check that the steps fit the signature
    val uses = ParserUtils.allpredicates(steps)
    val sanesteps = ParserUtils.checkSig(uses)

    true
  }
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
}
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 {
  def guard: Formula
  def fun: String
  def tuple: List[Var]
Christian Müller's avatar
Christian Müller committed
52
  def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple): this.type
53 54 55 56 57 58

  lazy val freeVars: Set[Var] = guard.freeVars ++ tuple
}

case class Add(guard: Formula, fun: String, tuple: List[Var]) extends Statement {
  override def toString: String = guard + " → " + fun + " += " + tuple.mkString("(", ",", ")") + ";"
Christian Müller's avatar
stuff  
Christian Müller committed
59
  override def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple) = Add(guard, fun, tuple)
60 61 62
}
case class Remove(guard: Formula, fun: String, tuple: List[Var]) extends Statement {
  override def toString: String = guard + " → " + fun + " -= " + tuple.mkString("(", ",", ")") + ";"
Christian Müller's avatar
stuff  
Christian Müller committed
63 64
  override def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple) = Remove(guard, fun, tuple)

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

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
82
  def update(steps:List[SType]):this.type
83 84 85 86 87
}

trait TSBlock extends Block

trait Loop extends Block {
Christian Müller's avatar
stuff  
Christian Müller committed
88 89 90 91
  type B <: Block

  def steps:List[B]
  def update(steps:List[B] = steps):this.type
92 93 94 95 96 97 98
  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
99 100 101 102 103 104
  type B <: Block

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

105 106 107 108 109 110 111 112 113
  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
114
  override def update(newsteps: List[SetStmt]) = SimpleTSBlock(newsteps)
115 116
}

Christian Müller's avatar
stuff  
Christian Müller committed
117 118 119 120 121 122 123 124 125 126 127 128
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)
  }
}