Commit a6dfb491 authored by Christian Müller's avatar Christian Müller

stuff

parent 32501d18
......@@ -34,7 +34,7 @@ object Preconditions extends LazyLogging {
b.steps
}
val newb = b.updateSteps(guardfix)
val newb = b.update(guardfix)
// for causality, add informedness updates
if (properties.stubborn) {
......
......@@ -41,7 +41,7 @@ abstract class Statement {
def guard: Formula
def fun: String
def tuple: List[Var]
def updateGuard(newguard: Formula): This
def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple): This
lazy val freeVars: Set[Var] = guard.freeVars ++ tuple
}
......@@ -49,23 +49,23 @@ abstract class Statement {
case class Add(guard: Formula, fun: String, tuple: List[Var]) extends Statement {
type This = Add
override def toString: String = guard + " → " + fun + " += " + tuple.mkString("(", ",", ")") + ";"
override def updateGuard(newguard: Formula) = Add(newguard, fun, tuple)
override def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple) = Add(guard, fun, tuple)
}
case class Remove(guard: Formula, fun: String, tuple: List[Var]) extends Statement {
type This = Remove
override def toString: String = guard + " → " + fun + " -= " + tuple.mkString("(", ",", ")") + ";"
override def updateGuard(newguard: Formula) = Remove(newguard, fun, tuple)
override def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple) = Remove(guard, fun, tuple)
}
case class SetStmt(guard:Formula, fun:String, tuple: List[Var]) extends Statement {
type This = SetStmt
override def toString: String = guard + " → " + fun + " := " + tuple.mkString("(", ",", ")") + ";"
override def updateGuard(newguard: Formula) = SetStmt(newguard, fun, tuple)
override def update(guard: Formula = guard, fun: String = fun, tuple: List[Var] = tuple) = SetStmt(guard, fun, tuple)
}
trait Block
trait SimpleBlock extends Block {
type This >: this.type <: SimpleBlock
type SType <: Statement
def steps: List[SType]
......@@ -74,13 +74,16 @@ trait SimpleBlock extends Block {
steps.map(_.fun).toSet
}
def updateSteps(s:List[SType]):This
def update(steps:List[SType]):this.type
}
trait TSBlock extends Block
trait Loop extends Block {
def steps:List[Block]
type B <: Block
def steps:List[B]
def update(steps:List[B] = steps):this.type
override def toString: String = {
// indentation
"loop {\n" + Utils.indentLines(steps.mkString("\n") + "\n}\n")
......@@ -88,8 +91,12 @@ trait Loop extends Block {
}
trait NondetChoice extends Block {
def left: List[Block]
def right: List[Block]
type B <: Block
def left: List[B]
def right: List[B]
def update(left:List[B] = left, right:List[B] = right):this.type
override def toString: String = {
"choose {\n" + Utils.indentLines(left.mkString("\n")) +
"\n} or {\n" + Utils.indentLines(right.mkString("\n")) + "\n}\n"
......@@ -97,11 +104,20 @@ trait NondetChoice extends Block {
}
case class SimpleTSBlock(steps: List[SetStmt]) extends SimpleBlock with TSBlock {
type This = TSBlock
type SType = SetStmt
override def toString: String = steps.mkString("{", "\n ", "}")
override def updateSteps(newsteps: List[SetStmt]) = SimpleTSBlock(newsteps)
override def update(newsteps: List[SetStmt]) = SimpleTSBlock(newsteps)
}
case class TSLoop(steps:List[TSBlock]) extends Loop with TSBlock
case class TSNondetChoice(left:List[TSBlock], right:List[TSBlock]) extends NondetChoice with TSBlock
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)
}
}
......@@ -94,7 +94,7 @@ case class NISpec(w: Workflow, declass: Map[String, (List[Var], Formula)], axiom
}
def addKnowledge(k:Formula) = {
NISpec(w, declass, And.make(always, k), target, causals)
NISpec(w, declass, And.make(axioms, k), target, causals)
}
}
object NISpec {
......@@ -104,7 +104,7 @@ object NISpec {
trait WFBlock extends Block
abstract sealed class SimpleWFBlock extends SimpleBlock with WFBlock {
trait SimpleWFBlock extends SimpleBlock with WFBlock {
def agents: List[Var]
def may: Boolean
def pred: Option[String]
......@@ -134,19 +134,29 @@ abstract sealed class SimpleWFBlock extends SimpleBlock with WFBlock {
}
case class ForallWFBlock(agents: List[Var], steps: List[Statement]) extends SimpleWFBlock {
type This = ForallWFBlock
type SType = Statement
val may = false
override def pred():Option[String] = None
override def pred:None.type = None
override def toString: String = "forall " + agents.map(_.withType).mkString(",") + steps.mkString("\n ", "\n ", "")
override def updateSteps(newsteps: List[Statement]) = ForallWFBlock(agents, newsteps)
override def update(newsteps: List[Statement]) = ForallWFBlock(agents, newsteps)
}
case class ForallMayWFBlock(agents: List[Var], choice: String, steps: List[Statement]) extends SimpleWFBlock {
type This = ForallMayWFBlock
type SType = Statement
val may = true
override def pred:Some[String] = Some(choice)
override def toString: String = "forall " + agents.map(_.withType).mkString(",") + " may (" + pred + ")" + steps.mkString("\n ", "\n ", "")
override def updateSteps(newsteps: List[Statement]) = ForallMayWFBlock(agents, choice, newsteps)
override def update(newsteps: List[Statement]) = ForallMayWFBlock(agents, choice, newsteps)
}
case class WFLoop(steps:List[WFBlock]) extends Loop with WFBlock
case class WFNondetChoice(left:List[WFBlock], right:List[WFBlock]) extends NondetChoice with WFBlock
case class WFLoop(steps:List[WFBlock]) extends Loop with WFBlock {
type B = WFBlock
override def update(steps:List[WFBlock] = steps):WFLoop = {
WFLoop(steps)
}
}
case class WFNondetChoice(left:List[WFBlock], right:List[WFBlock]) extends NondetChoice with WFBlock {
type B = WFBlock
override def update(left:List[WFBlock] = left, right:List[WFBlock] = right):WFNondetChoice = {
WFNondetChoice(left, right)
}
}
......@@ -91,11 +91,43 @@ trait ParserUtils extends LazyLogging {
typedpreds.map(v => v.name -> v.params.map(_.typ)).toMap
}
def inferTypeFromSig(sig:Signature, block:TSBlock): TSBlock = {
???
def mapStatements(block:Block, pf:T => T) = {
block match {
case sim:SimpleBlock => {
val newsteps = sim.steps.map(pf(_))
sim.update(newsteps)
}
case l:Loop => {
val newsteps = l.steps.map(inferTypeFromSig(sig, _))
l.update(newsteps)
}
case c:NondetChoice => {
val left = c.left.map(inferTypeFromSig(sig, _))
val right = c.right.map(inferTypeFromSig(sig, _))
c.update(left, right)
}
}
}
def inferTypeFromSig(sig:Signature, stmt:Statement): Statement = {
def inferTypeFromSig[B <: Block](sig:Signature, block:B): B = {
block match {
case sim:SimpleBlock => {
val newsteps = sim.steps.map(inferTypeFromSig(sig, _))
sim.update(newsteps)
}
case l:Loop => {
val newsteps = l.steps.map(inferTypeFromSig(sig, _))
l.update(newsteps)
}
case c:NondetChoice => {
val left = c.left.map(inferTypeFromSig(sig, _))
val right = c.right.map(inferTypeFromSig(sig, _))
c.update(left, right)
}
}
}
def inferTypeFromSig[T <: Statement](sig:Signature, stmt:T): T = {
val map = predtypeMap(sig.preds ++ sig.as ++ sig.constas ++ sig.bs)
......@@ -107,10 +139,6 @@ trait ParserUtils extends LazyLogging {
}
val newtup = addTypes(stmt.tuple, map(stmt.fun))
stmt match {
case s:Add => Add(newguard, stmt.fun, newtup)
case s:Remove => Remove(newguard, stmt.fun, newtup)
case s:SetStmt => SetStmt(newguard, stmt.fun, newtup)
}
stmt.update(guard = newguard, tuple = newtup)
}
}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment