typedcausal5.spec 363 Bytes
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
Workflow

forall a:T1
    (O(a)) -> R += (a)
forallmay a:T1,b:T2
    True -> S += (b, a)
forallmay a:T2,b:T3
    True -> T += (b, a)
forallmay a:T3,b:T4
    True -> U += (b, a)
forallmay a:T4,b:T5
    True -> V += (b, a)
forallmay a:T5,b:T6
    True -> W += (b, a)

Declassify

18
O(x:T1): True
Christian Müller's avatar
Christian Müller committed
19 20 21

Target

Christian Müller's avatar
Christian Müller committed
22
W(a1:T6, a2:T5)
Christian Müller's avatar
Christian Müller committed
23 24 25 26

Causality

ca:T1, cb:T2, cc:T3, cd:T4, ce:T5