TransitionSystem.scala 5.5 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
case class Signature(as: Set[Fun], constas: Set[Fun], bs: Set[Fun], preds: Set[Fun], constants: Set[Var]) {
Christian Müller's avatar
Christian Müller committed
9 10 11

  lazy val allpredicates: Set[Fun] = as ++ bs ++ constas ++ preds

12 13 14 15
  override def toString: String =
  {
    def mkString(set:Set[Fun]) = set.map(_.toTypedString).mkString(",")
    val inner =
16
      s"""EmptyPredicates:${mkString(preds)}
17 18 19 20 21 22 23 24 25
        |AxiomPredicates:${mkString(constas)}
        |As:${mkString(as)}
        |Bs:${mkString(bs)}
        |Constants:${constants.map(_.withType).mkString(",")}
      """.stripMargin
    s"Signature:\n${Utils.indentLines(inner)}"
  }

}
26 27 28 29 30
object Signature {
  val EMPTY = Signature(Set(), Set(), Set(), Set(), Set())
}

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

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

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

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

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

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

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

trait Block

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

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

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

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

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

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

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

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

124 125 126 127 128 129
  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
Christian Müller committed
130 131 132 133
sealed trait TSBlock extends Block {
  // TODO: maybe move this to general blocks?
  def mapStatements(f:SetStmt => SetStmt):TSBlock
}
134 135

case class SimpleTSBlock(steps: List[SetStmt]) extends SimpleBlock[SimpleTSBlock, SetStmt] with TSBlock {
136
  override def toString: String = steps.mkString("{", "\n  ", "}")
137 138
  def toTypedString: String = steps.map(_.toTypedString).mkString("{", "\n  ", "}")
  override def update(newsteps: List[SetStmt]): SimpleTSBlock = copy(newsteps)
Christian Müller's avatar
Christian Müller committed
139 140

  override def mapStatements(f: SetStmt => SetStmt): TSBlock = update(steps.map(f))
141 142
}

143
case class TSLoop(steps:List[TSBlock]) extends Loop[TSLoop, TSBlock] with TSBlock {
Christian Müller's avatar
stuff  
Christian Müller committed
144
  type B = TSBlock
145
  override def update(steps:List[TSBlock] = steps):TSLoop = copy(steps)
Christian Müller's avatar
Christian Müller committed
146 147

  override def mapStatements(f: SetStmt => SetStmt): TSBlock = update(steps.map(_.mapStatements(f)))
Christian Müller's avatar
stuff  
Christian Müller committed
148
}
149
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
150
  type B = TSBlock
151
  override def update(left:List[TSBlock] = left, right:List[TSBlock] = right):TSNondetChoice = copy(left, right)
Christian Müller's avatar
Christian Müller committed
152 153

  override def mapStatements(f: SetStmt => SetStmt): B = update(left.map(_.mapStatements(f)), right.map(_.mapStatements(f)))
Christian Müller's avatar
stuff  
Christian Müller committed
154
}