From 9987dadf738779b0caf880385b0c013bea5bccf3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Christian=20M=C3=BCller?= Date: Wed, 20 Feb 2019 12:43:24 +0100 Subject: [PATCH] withB --- examples/tests/conference_linear_small.spec | 6 +++-- .../tests/conference_linear_small_withB.spec | 22 +++++++++++++++++++ .../workflows/MainInvariantsInference.scala | 4 ++-- 3 files changed, 28 insertions(+), 4 deletions(-) create mode 100644 examples/tests/conference_linear_small_withB.spec diff --git a/examples/tests/conference_linear_small.spec b/examples/tests/conference_linear_small.spec index c5b0564..916dad0 100644 --- a/examples/tests/conference_linear_small.spec +++ b/examples/tests/conference_linear_small.spec @@ -2,10 +2,12 @@ Workflow forallmay x:X,p:P True -> Conf += (x,p) +forallmay x:x,p:P + ¬Conf(x,p) -> Assign += (x,p) forall x:X,p:P,r:R - (¬ Conf(x,p) ∧ O(x,p,r)) -> Read += (x,p,r) + (Assign(x,p) ∧ O(x,p,r)) -> Read += (x,p,r) forallmay y:X,x:X,p:P - (¬ Conf(x,p) ∧ ¬ Conf(y,p)) -> Comm += (x,y,p) + (Assign(x,p) ∧ Assign(y,p)) -> Comm += (x,y,p) Declassify diff --git a/examples/tests/conference_linear_small_withB.spec b/examples/tests/conference_linear_small_withB.spec new file mode 100644 index 0000000..e27bb5a --- /dev/null +++ b/examples/tests/conference_linear_small_withB.spec @@ -0,0 +1,22 @@ +Workflow + +forallmay x:X,p:P + True -> Conf += (x,p) +forall x:x,p:P + B(x,p) -> Assign += (x,p) +forall x:X,p:P,r:R + (Assign(x,p) ∧ O(x,p,r)) -> Read += (x,p,r) +forallmay y:X,x:X,p:P + (Assign(x,p) ∧ Assign(y,p)) -> Comm += (x,y,p) + +Declassify + +O(x:X,p:P,r:R): ¬ Conf(xt:X,p:P) + +Target + +Comm(xt:X, yt:X, pt:P) + +Causality + +a:X diff --git a/src/main/scala/de/tum/workflows/MainInvariantsInference.scala b/src/main/scala/de/tum/workflows/MainInvariantsInference.scala index be9562b..1a39de9 100644 --- a/src/main/scala/de/tum/workflows/MainInvariantsInference.scala +++ b/src/main/scala/de/tum/workflows/MainInvariantsInference.scala @@ -36,7 +36,7 @@ object MainInvariantsInference extends App with LazyLogging { val inv = invariant(spec) // val (res, graph, labels, t) = InvariantChecker.checkInvariantFPHeadLabel(spec, inv, props) - val res = Utils.check("tests/conference_linear_small", "elimB", inv, props) + val res = Utils.check(name, "elimB", inv, props) } @@ -62,7 +62,7 @@ object MainInvariantsInference extends App with LazyLogging { // clear() // generateExample("nonomitting/conference") - generateExample("tests/conference_linear_small", 1) + generateExample("tests/conference_linear_small_withB", 1) // generateExample("nonomitting/conference_linear", 2) // generateExample("tests/loopexampleNoOracle") // generateAllExamples() -- 2.24.1