causal3.spec 496 Bytes
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2
IGNORE

3 4
Workflow

Christian Müller's avatar
Christian Müller committed
5
forallmay a
6 7 8 9 10
    True -> T1 += (a)
forallmay a
    ¬ T1(a) -> T2 += (a)
forallmay a
    (¬ T1(a) ∧ ¬ T2(a)) -> T3 += (a)
11 12
forallmay a
    (¬ T1(a) ∧ ¬ T2(a) ∧ ¬ T3(a)) -> T4 += (a)
13 14 15 16 17 18

forall a
    (O(a) ∧ T1(a)) -> R += (a)
forallmay a,b
    (T1(a) ∧ T2(b)) -> S += (b, a)
forallmay a,b
19 20 21
    (T2(a) ∧ T3(b)) -> T += (b, a)
forallmay a,b
    (T3(a) ∧ T4(b)) -> U += (b, a)
22 23 24

Declassify

Christian Müller's avatar
Christian Müller committed
25
O(x): F (T1(x) ∨ T2(x) ∨ T3(x))
26 27 28

Target

29
U(a1, a2)
30 31 32

Causality

33
ca, cb, cc