causal2.spec 357 Bytes
Newer Older
1
2
Workflow

Christian Müller's avatar
Christian Müller committed
3
forallmay a
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
    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)
forallmay a,b
    (T2(a) ∧ T3(b)) -> S += (b, a)

Declassify

O(x): F (T1(x) ∨ T2(x))

Target

S(a1, a2)

Causality

ca, cb