TransitionSystem.scala 4.94 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 15 16 17 18 19 20 21 22 23
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)}"
  }

}
24 25 26 27 28 29
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
30 31 32 33 34

  def isSane() = {

    // check that the steps fit the signature
    val uses = ParserUtils.allpredicates(steps)
35
    val sanesteps = ParserUtils.checkSig(sig, uses)
Christian Müller's avatar
Christian Müller committed
36

37
    sanesteps
Christian Müller's avatar
Christian Müller committed
38
  }
39 40 41 42 43 44 45 46 47 48 49
}
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 = {
Christian Müller's avatar
Christian Müller committed
50
    s"InvSpec\nTransition System:\n$ts\n\nAxioms:\n$axioms\n\nInvariant:$inv\n"
51 52
  }
  def addAxiom(k:Formula) = {
Christian Müller's avatar
Christian Müller committed
53
      copy(axioms = And.make(axioms, k))
54
  }
Christian Müller's avatar
Christian Müller committed
55 56 57
//  def addInv(k:Formula) = {
//    InvariantSpec(ts, axioms, And.make(inv, k))
//  }
58 59 60 61
  def isSane: Boolean = {
    // TODO: add sanity checking for axioms and invariant signatures
    ts.isSane()
  }
62 63 64 65 66
}
object InvariantSpec {
  val EMPTY = InvariantSpec(TransitionSystem.EMPTY, True, True)
}

67
abstract class Statement[T <: Statement[T]] {
68 69 70
  def guard: Formula
  def fun: String
  def tuple: List[Var]
71 72
  def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple): Statement[T]
  def toTypedString: String
73 74 75 76

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

77
case class Add(guard: Formula, fun: String, tuple: List[Var]) extends Statement[Add] {
78
  override def toString: String = guard + " → " + fun + " += " + tuple.mkString("(", ",", ")") + ";"
79 80
  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)
81
}
82
case class Remove(guard: Formula, fun: String, tuple: List[Var]) extends Statement[Remove] {
83
  override def toString: String = guard + " → " + fun + " -= " + tuple.mkString("(", ",", ")") + ";"
84 85
  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)
Christian Müller's avatar
stuff  
Christian Müller committed
86

87
}
88
case class SetStmt(guard:Formula, fun:String, tuple: List[Var]) extends Statement[SetStmt] {
89
  override def toString: String = guard + " → " + fun + " := " + tuple.mkString("(", ",", ")") + ";"
90 91
  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)
92 93 94 95
}

trait Block

96
trait SimpleBlock[B <: SimpleBlock[B, S], S <: Statement[_]] extends Block {
97

98
  def steps: List[S]
99 100 101 102 103

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

104
  def update(steps:List[S]):SimpleBlock[B, S]
105 106
}

107
trait Loop[T <: Loop[T, B], B <: Block] extends Block {
Christian Müller's avatar
stuff  
Christian Müller committed
108 109

  def steps:List[B]
110
  def update(steps:List[B] = steps):Loop[T, B]
111 112 113 114 115 116
  override def toString: String = {
    // indentation
    "loop {\n" + Utils.indentLines(steps.mkString("\n") + "\n}\n")
  }
}

117
trait NondetChoice[T <: NondetChoice[T, B], B <: Block] extends Block {
Christian Müller's avatar
stuff  
Christian Müller committed
118 119 120

  def left: List[B]
  def right: List[B]
121
  def update(left:List[B] = left, right:List[B] = right):NondetChoice[T, B]
Christian Müller's avatar
stuff  
Christian Müller committed
122

123 124 125 126 127 128
  override def toString: String = {
    "choose {\n" + Utils.indentLines(left.mkString("\n")) +
      "\n} or {\n" + Utils.indentLines(right.mkString("\n")) + "\n}\n"
  }
}

Christian Müller's avatar
fix  
Christian Müller committed
129
sealed trait TSBlock extends Block
130 131

case class SimpleTSBlock(steps: List[SetStmt]) extends SimpleBlock[SimpleTSBlock, SetStmt] with TSBlock {
132
  override def toString: String = steps.mkString("{", "\n  ", "}")
133 134
  def toTypedString: String = steps.map(_.toTypedString).mkString("{", "\n  ", "}")
  override def update(newsteps: List[SetStmt]): SimpleTSBlock = copy(newsteps)
135 136
}

137
case class TSLoop(steps:List[TSBlock]) extends Loop[TSLoop, TSBlock] with TSBlock {
Christian Müller's avatar
stuff  
Christian Müller committed
138
  type B = TSBlock
139
  override def update(steps:List[TSBlock] = steps):TSLoop = copy(steps)
Christian Müller's avatar
stuff  
Christian Müller committed
140
}
141
case class TSNondetChoice(left:List[TSBlock], right:List[TSBlock]) extends NondetChoice[TSNondetChoice, TSBlock] with TSBlock {
Christian Müller's avatar
stuff  
Christian Müller committed
142
  type B = TSBlock
143
  override def update(left:List[TSBlock] = left, right:List[TSBlock] = right):TSNondetChoice = copy(left, right)
Christian Müller's avatar
stuff  
Christian Müller committed
144
}