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

3
4
5
6
forallmay x,s O(s) -> Q += (x,s)
loop {
	forall x,y,s R(y,s) -> S += (x,y,s)
	forall x,s Q(x,s) -> R += (x,s)
Christian Müller's avatar
Christian Müller committed
7
8
9
10
11
}

Target

S(x,y,s)