university.spec 292 Bytes
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2
Workflow

3
forall p:Prof,s:Student,g:Grade
Christian Müller's avatar
Christian Müller committed
4 5 6 7 8 9 10 11
    (O(p,s,g)) -> Grading += (p,s,g)
forallmay p:Prof,t:TA
    True -> Talk1 += (t, p)
forallmay t:TA,s:Student
    True -> Talk2 += (s, t)

Declassify

12
O(p:Prof,s:Student,g:Grade): False
Christian Müller's avatar
Christian Müller committed
13 14 15 16 17 18 19 20

Target

Talk2(as:Student, at:TA)

Causality

cta:TA, cp:Prof