conference_linear_small.spec 337 Bytes
Newer Older
Christian Müller's avatar
Christian Müller committed
1
2
3
4
Workflow

forallmay x:X,p:P
	True -> Conf += (x,p)
Christian Müller's avatar
withB    
Christian Müller committed
5
6
forallmay x:x,p:P
    ¬Conf(x,p) -> Assign += (x,p)
Christian Müller's avatar
Christian Müller committed
7
forall x:X,p:P,r:R
Christian Müller's avatar
withB    
Christian Müller committed
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
withB    
Christian Müller committed
10
	(Assign(x,p) ∧ Assign(y,p)) -> Comm += (x,y,p)
Christian Müller's avatar
Christian Müller committed
11
12
13
14
15
16
17
18
19
20
21
22

Declassify

O(x:X,p:P,r:R): ¬ Conf(xt:X,p:P)

Target

Comm(xt:X, yt:X, pt:P)

Causality

a:X