add university

7541cf42 · Christian Müller · 9c28ba33 · 7541cf42
Commit 7541cf42 authored May 18, 2017 by Christian Müller
Hide whitespace changes
Inline Side-by-side

Showing with 20 additions and 0 deletions

examples/university.spec examples/university.spec +20 -0

No files found.
--- a/examples/university.spec
+++ b/examples/university.spec
+Workflow
+
+forallmay p:Prof,s:Student,g:Grade
+    (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
+
+O(p:Prof,s:Student,g:Grade): True
+
+Target
+
+Talk2(as:Student, at:TA)
+
+Causality
+
+cta:TA, cp:Prof