TransitionSystem.scala 4.94 KB
Newer Older
Christian Müller's avatar
Christian Müller committed
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
Christian Müller's avatar
Christian Müller committed
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)}"
  }

}
Christian Müller's avatar
Christian Müller committed
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
  }
Christian Müller's avatar
Christian Müller committed
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"
Christian Müller's avatar
Christian Müller committed
51
52
  }
  def addAxiom(k:Formula) = {
Christian Müller's avatar
Christian Müller committed
53
      copy(axioms = And.make(axioms, k))
Christian Müller's avatar
Christian Müller committed
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()
  }
Christian Müller's avatar
Christian Müller committed
62
63
64
65
66
}
object InvariantSpec {
  val EMPTY = InvariantSpec(TransitionSystem.EMPTY, True, True)
}

67
abstract class Statement[T <: Statement[T]] {
Christian Müller's avatar
Christian Müller committed
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
Christian Müller's avatar
Christian Müller committed
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] {
Christian Müller's avatar
Christian Müller committed
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)
Christian Müller's avatar
Christian Müller committed
81
}
82
case class Remove(guard: Formula, fun: String, tuple: List[Var]) extends Statement[Remove] {
Christian Müller's avatar
Christian Müller committed
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

Christian Müller's avatar
Christian Müller committed
87
}
88
case class SetStmt(guard:Formula, fun:String, tuple: List[Var]) extends Statement[SetStmt] {
Christian Müller's avatar
Christian Müller committed
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)
Christian Müller's avatar
Christian Müller committed
92
93
94
95
}

trait Block

96
trait SimpleBlock[B <: SimpleBlock[B, S], S <: Statement[_]] extends Block {
Christian Müller's avatar
Christian Müller committed
97

98
  def steps: List[S]
Christian Müller's avatar
Christian Müller committed
99
100
101
102
103

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

104
  def update(steps:List[S]):SimpleBlock[B, S]
Christian Müller's avatar
Christian Müller committed
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]
Christian Müller's avatar
Christian Müller committed
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

Christian Müller's avatar
Christian Müller committed
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 {
Christian Müller's avatar
Christian Müller committed
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)
Christian Müller's avatar
Christian Müller committed
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
}