Commit 791bb3d5 authored by Christian Müller's avatar Christian Müller

build, tests

parent b39ef875
...@@ -4,8 +4,9 @@ version := "0.1" ...@@ -4,8 +4,9 @@ version := "0.1"
scalaVersion := "2.12.8" scalaVersion := "2.12.8"
javaOptions += "-Xmx1G" javaOptions += "-Xmx4096m"
javaOptions += "-Xms256m" javaOptions += "-Xms2048m"
// EclipseKeys.withBundledScalaContainers := false // EclipseKeys.withBundledScalaContainers := false
......
...@@ -12,8 +12,6 @@ forallmay x:A,p:P,r:R ...@@ -12,8 +12,6 @@ forallmay x:A,p:P,r:R
(Assign(x,p)) → Review += (x,p,r) (Assign(x,p)) → Review += (x,p,r)
forall xa:A,xb:A,p:P,r:R forall xa:A,xb:A,p:P,r:R
(Assign(xa,p) ∧ Review(xb,p,r)) → Read += (xa,p,r) (Assign(xa,p) ∧ Review(xb,p,r)) → Read += (xa,p,r)
forallmay x:A,p:P,r:R
(Assign(x,p)) → Review += (x,p,r)
Declassify Declassify
......
...@@ -13,11 +13,11 @@ loop { ...@@ -13,11 +13,11 @@ loop {
Declassify Declassify
Oracle(x:A,p:P,r:R): ¬ Conf(xat:A,p:P) Oracle(x:A,p:P,r:R): ¬ Conf(xt:A,p:P)
Target Target
Read(xat:A, p:P, rt:R) Read(xt:A, pt:P, rt:R)
Causality Causality
......
package de.tum.niwo.tests.papertests package de.tum.niwo.tests.papertests
import de.tum.niwo.foltl.FOLTL.{Forall, Var} import de.tum.niwo.blocks.NISpec
import de.tum.niwo.foltl.FOLTL
import de.tum.niwo.foltl.FOLTL.{And, Forall, Fun, Neg, Var}
import de.tum.niwo.invariants.InvariantGenerator.genEq import de.tum.niwo.invariants.InvariantGenerator.genEq
import de.tum.niwo.{Examples, Utils} import de.tum.niwo.{Examples, Utils}
import de.tum.niwo.invariants.{InvProperties, InvariantGenerator} import de.tum.niwo.invariants.{InvProperties, InvariantGenerator}
import de.tum.niwo.tests.TestUtils.checkSafe import de.tum.niwo.tests.TestUtils.{checkSafe, checkSafeCausalElim}
import org.scalatest.FlatSpec import org.scalatest.FlatSpec
class CCSSubmissionTest extends FlatSpec { class CCSSubmissionTest extends FlatSpec {
...@@ -98,6 +100,18 @@ class CCSSubmissionTest extends FlatSpec { ...@@ -98,6 +100,18 @@ class CCSSubmissionTest extends FlatSpec {
))) )))
} }
// single choice
it should "prove unrolled causal conference with single choice" in {
val name = "omitting/conference_unrolled_withB"
val inv = InvariantGenerator.invariantNoninterSingleBS _
assert(checkSafe(name, "", inv, InvProperties(
stubborn = false,
eliminateA = false,
eliminateB = true,
approxElim = false
)))
}
it should "prove stubborn omitting/conference_linear_fixed" in { it should "prove stubborn omitting/conference_linear_fixed" in {
val name = "omitting/conference_linear_fixed" val name = "omitting/conference_linear_fixed"
val inv = InvariantGenerator.invariantNoninterSingleBS _ val inv = InvariantGenerator.invariantNoninterSingleBS _
...@@ -115,4 +129,23 @@ class CCSSubmissionTest extends FlatSpec { ...@@ -115,4 +129,23 @@ class CCSSubmissionTest extends FlatSpec {
approxElim = false approxElim = false
))) )))
} }
it should "prove causal omitting/conference_fixed for a given invariant" in {
val name = "omitting/conference_withB"
// val inv = InvariantGenerator.invariantNoninterSingleBS _
val xat = Var("xat","A")
val pt = Var("pt","P")
val rt = Var("rt","R")
// val rt = Var("rt","R")
val inv = (spec:NISpec) => And.make(InvariantGenerator.invariantAllEqual(spec), Forall(List(xat), Neg(Fun("informed", Some("t1"), List(xat)))))
// val inv = InvariantGenerator.invariantNoninterSingleBS _
assert(checkSafe(name, "", inv, InvProperties(
stubborn = false,
approxElim = false,
eliminateA = true
)))
}
} }
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