From 8f5e5d7dd2aa2acc23b703e7b9bd6abcc93c7eb9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Christian=20M=C3=BCller?= <christian.mueller@in.tum.de>
Date: Fri, 15 Sep 2017 10:55:20 +0100
Subject: [PATCH] fixed linear from atva

---
 examples/omitting/conference_linear_safe.spec | 24 +++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 examples/omitting/conference_linear_safe.spec

diff --git a/examples/omitting/conference_linear_safe.spec b/examples/omitting/conference_linear_safe.spec
new file mode 100644
index 0000000..d8b3600
--- /dev/null
+++ b/examples/omitting/conference_linear_safe.spec
@@ -0,0 +1,24 @@
+Workflow
+
+forallmay x:X,p:P
+	True -> Conf += (x,p)
+forallmay x:X,p:P
+	!Conf(x,p) -> Assign += (x,p)
+forall x:X,y:X,p:P,q:P
+	(Conf(x,p) ∧ ¬ Conf(y,p) ∧ Assign(x,p) ∧ Assign(y,q)) -> Assign -= (y,q)
+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
-- 
GitLab