causal1.spec 288 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
Workflow

forallmay a
    True -> T1 += (a)
forallmay a
    ¬ T1(a) -> T2 += (a)
forallmay a
    (¬ T1(a) ∧ ¬ T2(a)) -> T3 += (a)

forall a
    (O(a) ∧ T1(a)) -> R += (a)
forallmay a,b
    (T1(a) ∧ T2(b)) -> S += (b, a)

Declassify

Christian Müller's avatar
Christian Müller committed
17
O(x): T1(x)
Christian Müller's avatar
Christian Müller committed
18 19 20 21 22 23 24 25

Target

S(a1, a2)

Causality

ca