conference_linear.spec 334 Bytes
Newer Older
1
2
Workflow

Christian Müller's avatar
Christian Müller committed
3
forallmay x:X,p:P
4
	True -> Conf += (x,p)
Christian Müller's avatar
Christian Müller committed
5
forallmay x:X,p:P
Christian Müller's avatar
Christian Müller committed
6
	!Conf(x,p) -> Assign += (x,p)
Christian Müller's avatar
Christian Müller committed
7
forall x:X,p:P,r:R
8
	(Assign(x,p) ∧ O(x,p,r)) -> Read += (x,p,r)
Christian Müller's avatar
Christian Müller committed
9
forallmay y:X,x:X,p:P 
Christian Müller's avatar
Christian Müller committed
10
	(Assign(x,p) ∧ Assign(y,p)) -> Comm += (x,y,p)
11

Christian Müller's avatar
Christian Müller committed
12
13
Declassify

Christian Müller's avatar
Christian Müller committed
14
O(x:X,p:P,r:R): ¬ Conf(xt:X,p:P)
Christian Müller's avatar
Christian Müller committed
15

16
17
Target

Christian Müller's avatar
Christian Müller committed
18
Comm(xt:X, yt:X, pt:P)
19
20
21
22

Causality

a:X