Commit 9c28ba33 authored by Christian Müller's avatar Christian Müller

add typedcausal

parent 888faf32
IGNORE
Workflow
forallmay a
......
IGNORE
Workflow
forallmay a
......
IGNORE
Workflow
forallmay a
......
Workflow
forall a:T1
(O(a)) -> R += (a)
forallmay a:T1,b:T2
True -> S += (b, a)
forallmay a:T2,b:T3
True -> T += (b, a)
forallmay a:T3,b:T4
True -> U += (b, a)
Declassify
O(x): True
Target
T(a1:T4, a2:T3)
Causality
ca:T1, cb:T2, cc:T3
Workflow
forall a:T1
(O(a)) -> R += (a)
forallmay a:T1,b:T2
True -> S += (b, a)
forallmay a:T2,b:T3
True -> T += (b, a)
forallmay a:T3,b:T4
True -> U += (b, a)
forallmay a:T4,b:T5
True -> V += (b, a)
forallmay a:T5,b:T6
True -> W += (b, a)
Declassify
O(x): True
Target
T(a1:T5, a2:T5)
Causality
ca:T1, cb:T2, cc:T3, cd:T4, ce:T5
Workflow
forallmay i:A True -> R += (i)
forallmay i:A,j:B (R(i)) -> S += (i,j)
forallmay i:A,j:B,k:C (S(i,j)) -> T += (i,j,k)
forallmay i:A,j:B,k:C,l:D (T(i,j,k)) -> U += (i,j,k,l)
forallmay i:A,j:B,k:C,l:D,m:E (U(i,j,k,l)) -> V += (i,j,k,l,m)
forallmay i:A,j:B,k:C,l:D,m:E,n:F (V(i,j,k,l,m)) -> W += (i,j,k,l,m,n)
forallmay i:A,j:B,k:C,l:D,m:E,n:F,o:G (W(i,j,k,l,m,n)) -> X += (i,j,k,l,m,n,o)
forallmay i:A,j:B,k:C,l:D,m:E,n:F,o:G,p:H (X(i,j,k,l,m,n,o)) -> Y += (i,j,k,l,m,n,o,p)
forallmay i:A,j:B,k:C,l:D,m:E,n:F,o:G,p:H,q:I (Y(i,j,k,l,m,n,o,p)) -> Z += (i,j,k,l,m,n,o,p,q)
forallmay i:A,j:B,k:C,l:D,m:E,n:F,o:G,p:H,q:I,r:J (Z(i,j,k,l,m,n,o,p,q)) -> A += (i,j,k,l,m,n,o,p,q,r)
Target
A(u:A,v:B,w:C,x:D,y:E,z:F,aa:G,ab:H,ac:I,ad:J)
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