Commit dc81ed33 authored by Christian Müller's avatar Christian Müller

add typedcausal

parent 099e00ea
Workflow
forall a:T1
(O(a)) -> R += (a)
forallmay a:T1,b:T2
True -> S += (b, a)
forallmay a:T2,b:T3
True -> S += (b, a)
Declassify
O(x): True
Target
S(a1:T3, a2:T2)
Causality
ca:T1, cb:T2
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment