typedcausal3.spec

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)

Declassify

O(x:T1): True

Target

U(a1:T4, a2:T3)

Causality

ca:T1, cb:T2, cc:T3