notebook.spec 210 Bytes
Newer Older
1 2 3 4 5 6 7
Workflow

loop {
	choose {
		forallmay x:User, i:Info
			Written(i, x) → Read += (x, i)
	} {
Christian Müller's avatar
pics  
Christian Müller committed
8 9
		forallmay x:User, i:Info
			True → Written += (i, x)
10 11 12 13 14 15 16
	}
}

Target

Read(u:User, info:Info)

Christian Müller's avatar
Christian Müller committed
17 18 19
Causality

ac:User