TransitionSystem.scala 5.03 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
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 =
13
      s"""EmptyPredicates:${mkString(preds)}
14 15 16 17 18 19 20 21 22
        |AxiomPredicates:${mkString(constas)}
        |As:${mkString(as)}
        |Bs:${mkString(bs)}
        |Constants:${constants.map(_.withType).mkString(",")}
      """.stripMargin
    s"Signature:\n${Utils.indentLines(inner)}"
  }

}
23 24 25 26 27
object Signature {
  val EMPTY = Signature(Set(), Set(), Set(), Set(), Set())
}

case class TransitionSystem(sig: Signature, steps: List[TSBlock]) {
28
  override def toString: String = s"$sig\nTransition System\n${Utils.indentLines(steps.mkString("\n"))}"
Christian Müller's avatar
Christian Müller committed
29

30
  def isSane: Boolean = {
Christian Müller's avatar
Christian Müller committed
31 32
    // check that the steps fit the signature
    val uses = ParserUtils.allpredicates(steps)
33
    val sanesteps = ParserUtils.checkSig(sig, uses)
Christian Müller's avatar
Christian Müller committed
34

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

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

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

75
case class Add(guard: Formula, fun: String, tuple: List[Var]) extends Statement[Add] {
76
  override def toString: String = guard + " → " + fun + " += " + tuple.mkString("(", ",", ")") + ";"
77 78
  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)
79
}
80
case class Remove(guard: Formula, fun: String, tuple: List[Var]) extends Statement[Remove] {
81
  override def toString: String = guard + " → " + fun + " -= " + tuple.mkString("(", ",", ")") + ";"
82 83
  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
84

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

trait Block

94
trait SimpleBlock[B <: SimpleBlock[B, S], S <: Statement[_]] extends Block {
95

96
  def steps: List[S]
97 98 99 100 101

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

102
  def update(steps:List[S]):SimpleBlock[B, S]
103 104
}

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

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

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

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

121 122 123 124 125 126
  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
127
sealed trait TSBlock extends Block
128 129

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

135
case class TSLoop(steps:List[TSBlock]) extends Loop[TSLoop, TSBlock] with TSBlock {
Christian Müller's avatar
stuff  
Christian Müller committed
136
  type B = TSBlock
137
  override def update(steps:List[TSBlock] = steps):TSLoop = copy(steps)
Christian Müller's avatar
stuff  
Christian Müller committed
138
}
139
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
140
  type B = TSBlock
141
  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
142
}