Commit 8c862890 authored by Christian Müller's avatar Christian Müller

fix

parent e998e442
......@@ -126,7 +126,7 @@ trait NondetChoice[T <: NondetChoice[T, B], B <: Block] extends Block {
}
}
trait TSBlock extends Block
sealed trait TSBlock extends Block
case class SimpleTSBlock(steps: List[SetStmt]) extends SimpleBlock[SimpleTSBlock, SetStmt] with TSBlock {
override def toString: String = steps.mkString("{", "\n ", "}")
......
......@@ -21,7 +21,7 @@ object Workflow {
val EMPTY = Workflow(Signature.EMPTY, List())
}
// TODO: make causals a set
// TODO: make causals a set;
case class NISpec(w: Workflow, declass: Map[String, (List[Var], Formula)], axioms: Formula, target: Fun, causals:List[Var]) extends Spec with LazyLogging {
override def toString: String = {
s"NISpec\nWorkflow:\n$w\nDeclass:$declass\nTarget:$target"
......@@ -102,7 +102,7 @@ object NISpec {
}
trait WFBlock extends Block
sealed trait WFBlock extends Block
trait SimpleWFBlock[T <: SimpleWFBlock[T]] extends SimpleBlock[SimpleWFBlock[T], Statement[_]] with WFBlock {
def agents: List[Var]
......
......@@ -27,12 +27,6 @@ object WFGraphEncoding extends GraphBuilder with LazyLogging {
def toBlock(e:WorkflowGraph#EdgeT):SimpleWFBlock[_] = e.label
def toNumber(n:WorkflowGraph#NodeT):Int = n.toOuter
// type TSGraph = Graph[Int, LDiEdge]
// def toBlock(e:TSGraph#EdgeT):SimpleTSBlock = e
// def toNumber(n:TSGraph#NodeT):Int = n.toOuter
def toGraph(w:Workflow): WorkflowGraph = {
def makeid() = ForallWFBlock(List(), List())
toGraph(w.steps, makeid)
......
......@@ -40,7 +40,7 @@ object InvariantChecker extends LazyLogging {
type Node = graph.NodeT
type Edge = graph.EdgeT
val untouched = WFGraphEncoding.untouchedMap(graph, spec.ts.sig, properties)
val untouched = TSGraphEncoding.untouchedMap(graph, spec.ts.sig, properties)
@tailrec
def checkInvariantRec(labellist: List[Map[Int, Formula]], provenlist: List[Set[Edge]]): (Boolean, List[Map[Int, Formula]], List[Set[Edge]]) = {
......
......@@ -30,7 +30,7 @@ class InferenceTests extends FlatSpec {
assert(checkSafeStubborn(name, _ => inv))
}
"Invariant Inference" should "fail prove unsafe stuff safe" in {
"Invariant Inference" should "fail to prove unsafe stuff safe" in {
val name = "tests/conference_linear_small_unsafe"
val xt = Var("xt","X")
val yt = Var("yt","X")
......@@ -40,6 +40,12 @@ class InferenceTests extends FlatSpec {
assert(!checkSafeStubborn(name, _ => inv))
}
// type TSGraph = Graph[Int, LDiEdge]
// def toBlock(e:TSGraph#EdgeT):SimpleTSBlock = e
// def toNumber(n:TSGraph#NodeT):Int = n.toOuter
it should "prove safe causal stuff safe" in {
val name = "tests/conference_linear_small_withB"
val xt = Var("xt","X")
......
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