Expected Cost | +- [f] | 0 | +- [Program] | 0:While(n ≥ 1 + d) | 1:If(x ≥ 1) Then | 2:If(y ≥ 1) Then | Choice | 1/4: x :~ {1 : 2 + x} | d :~ {1 : 2 + d} | 3/4: Choice | 1/3: y :~ {1 : 2 + y} | d :~ {1 : 2 + d} | 2/3: Choice | 1/2: x :~ {1 : -1 + x} | d :~ {1 : -1 + d} | 1/2: y :~ {1 : -1 + y} | d :~ {1 : -1 + d} | Else | 3:If(0 ≥ 1 + y) Then | Choice | 1/4: x :~ {1 : 2 + x} | d :~ {1 : 2 + d} | 3/4: Choice | 1/3: y :~ {1 : 1 + y} | d :~ {1 : -1 + d} | 2/3: Choice | 1/2: x :~ {1 : -1 + x} | d :~ {1 : -1 + d} | 1/2: y :~ {1 : -2 + y} | d :~ {1 : 2 + d} | Else | Choice | 1/4: x :~ {1 : 2 + x} | d :~ {1 : 2 + d} | 3/4: Choice | 1/3: y :~ {1 : 1 + y} | d :~ {1 : 1 + d} | 2/3: Choice | 1/2: x :~ {1 : -1 + x} | d :~ {1 : -1 + d} | 1/2: y :~ {1 : -1 + y} | d :~ {1 : 1 + d} | Else | 4:If(0 ≥ 1 + x) Then | 5:If(y ≥ 1) Then | Choice | 1/4: x :~ {1 : 1 + x} | d :~ {1 : -1 + d} | 3/4: Choice | 1/3: y :~ {1 : 2 + y} | d :~ {1 : 2 + d} | 2/3: Choice | 1/2: x :~ {1 : -2 + x} | d :~ {1 : 2 + d} | 1/2: y :~ {1 : -1 + y} | d :~ {1 : -1 + d} | Else | 6:If(0 ≥ 1 + y) Then | Choice | 1/4: x :~ {1 : 1 + x} | d :~ {1 : -1 + d} | 3/4: Choice | 1/3: y :~ {1 : 1 + y} | d :~ {1 : -1 + d} | 2/3: Choice | 1/2: x :~ {1 : -2 + x} | d :~ {1 : 2 + d} | 1/2: y :~ {1 : -2 + y} | d :~ {1 : 2 + d} | Else | Choice | 1/4: x :~ {1 : 1 + x} | d :~ {1 : -1 + d} | 3/4: Choice | 1/3: y :~ {1 : 1 + y} | d :~ {1 : 1 + d} | 2/3: Choice | 1/2: x :~ {1 : -2 + x} | d :~ {1 : 2 + d} | 1/2: y :~ {1 : -1 + y} | d :~ {1 : 1 + d} | Else | 7:If(y ≥ 1) Then | Choice | 1/4: x :~ {1 : 1 + x} | d :~ {1 : 1 + d} | 3/4: Choice | 1/3: y :~ {1 : 2 + y} | d :~ {1 : 2 + d} | 2/3: Choice | 1/2: x :~ {1 : -1 + x} | d :~ {1 : 1 + d} | 1/2: y :~ {1 : -1 + y} | d :~ {1 : -1 + d} | Else | 8:If(0 ≥ 1 + y) Then | Choice | 1/4: x :~ {1 : 1 + x} | d :~ {1 : 1 + d} | 3/4: Choice | 1/3: y :~ {1 : 1 + y} | d :~ {1 : -1 + d} | 2/3: Choice | 1/2: x :~ {1 : -1 + x} | d :~ {1 : 1 + d} | 1/2: y :~ {1 : -2 + y} | d :~ {1 : 2 + d} | Else | Choice | 1/4: x :~ {1 : 1 + x} | d :~ {1 : 1 + d} | 3/4: Choice | 1/3: y :~ {1 : 1 + y} | d :~ {1 : 1 + d} | 2/3: Choice | 1/2: x :~ {1 : -1 + x} | d :~ {1 : 1 + d} | 1/2: y :~ {1 : -1 + y} | d :~ {1 : 1 + d} | Tick(1) | +- While.step | | | +- [Problem] | | 0:While(n ≥ 1 + d) | | 1:If(x ≥ 1) Then | | 2:If(y ≥ 1) Then | | Choice | | 1/4: x :~ {1 : 2 + x} | | d :~ {1 : 2 + d} | | 3/4: Choice | | 1/3: y :~ {1 : 2 + y} | | d :~ {1 : 2 + d} | | 2/3: Choice | | 1/2: x :~ {1 : -1 + x} | | d :~ {1 : -1 + d} | | 1/2: y :~ {1 : -1 + y} | | d :~ {1 : -1 + d} | | Else | | 3:If(0 ≥ 1 + y) Then | | Choice | | 1/4: x :~ {1 : 2 + x} | | d :~ {1 : 2 + d} | | 3/4: Choice | | 1/3: y :~ {1 : 1 + y} | | d :~ {1 : -1 + d} | | 2/3: Choice | | 1/2: x :~ {1 : -1 + x} | | d :~ {1 : -1 + d} | | 1/2: y :~ {1 : -2 + y} | | d :~ {1 : 2 + d} | | Else | | Choice | | 1/4: x :~ {1 : 2 + x} | | d :~ {1 : 2 + d} | | 3/4: Choice | | 1/3: y :~ {1 : 1 + y} | | d :~ {1 : 1 + d} | | 2/3: Choice | | 1/2: x :~ {1 : -1 + x} | | d :~ {1 : -1 + d} | | 1/2: y :~ {1 : -1 + y} | | d :~ {1 : 1 + d} | | Else | | 4:If(0 ≥ 1 + x) Then | | 5:If(y ≥ 1) Then | | Choice | | 1/4: x :~ {1 : 1 + x} | | d :~ {1 : -1 + d} | | 3/4: Choice | | 1/3: y :~ {1 : 2 + y} | | d :~ {1 : 2 + d} | | 2/3: Choice | | 1/2: x :~ {1 : -2 + x} | | d :~ {1 : 2 + d} | | 1/2: y :~ {1 : -1 + y} | | d :~ {1 : -1 + d} | | Else | | 6:If(0 ≥ 1 + y) Then | | Choice | | 1/4: x :~ {1 : 1 + x} | | d :~ {1 : -1 + d} | | 3/4: Choice | | 1/3: y :~ {1 : 1 + y} | | d :~ {1 : -1 + d} | | 2/3: Choice | | 1/2: x :~ {1 : -2 + x} | | d :~ {1 : 2 + d} | | 1/2: y :~ {1 : -2 + y} | | d :~ {1 : 2 + d} | | Else | | Choice | | 1/4: x :~ {1 : 1 + x} | | d :~ {1 : -1 + d} | | 3/4: Choice | | 1/3: y :~ {1 : 1 + y} | | d :~ {1 : 1 + d} | | 2/3: Choice | | 1/2: x :~ {1 : -2 + x} | | d :~ {1 : 2 + d} | | 1/2: y :~ {1 : -1 + y} | | d :~ {1 : 1 + d} | | Else | | 7:If(y ≥ 1) Then | | Choice | | 1/4: x :~ {1 : 1 + x} | | d :~ {1 : 1 + d} | | 3/4: Choice | | 1/3: y :~ {1 : 2 + y} | | d :~ {1 : 2 + d} | | 2/3: Choice | | 1/2: x :~ {1 : -1 + x} | | d :~ {1 : 1 + d} | | 1/2: y :~ {1 : -1 + y} | | d :~ {1 : -1 + d} | | Else | | 8:If(0 ≥ 1 + y) Then | | Choice | | 1/4: x :~ {1 : 1 + x} | | d :~ {1 : 1 + d} | | 3/4: Choice | | 1/3: y :~ {1 : 1 + y} | | d :~ {1 : -1 + d} | | 2/3: Choice | | 1/2: x :~ {1 : -1 + x} | | d :~ {1 : 1 + d} | | 1/2: y :~ {1 : -2 + y} | | d :~ {1 : 2 + d} | | Else | | Choice | | 1/4: x :~ {1 : 1 + x} | | d :~ {1 : 1 + d} | | 3/4: Choice | | 1/3: y :~ {1 : 1 + y} | | d :~ {1 : 1 + d} | | 2/3: Choice | | 1/2: x :~ {1 : -1 + x} | | d :~ {1 : 1 + d} | | 1/2: y :~ {1 : -1 + y} | | d :~ {1 : 1 + d} | | Tick(1) | | | +- [f] | | 0 | | | +- Expected Cost Body | | | | | `- [1 | ⊤] | | | +- shift-avg-template | | | | | `- 1 + [1 + -d + n | 1 + -d + n ≥ 0] | | | +- [Norms] | | [[1 | ⊤],[1 + -d + n | 1 + -d + n ≥ 0]] | | | +- [Invariant] | | n ≥ 1 + d ==> [1 | ⊤] + h([1 | ⊤],ite(x ≥ 1,ite(y ≥ 1,1/4·[-1 + -d + n | -1 + -d + n ≥ 0] + 1/4·[-1 + -d + n | -1 + -d + n ≥ 0] + 1/2·[2 + -d + n | 2 + -d + n ≥ 0],ite(0 ≥ 1 + y,1/4·[-1 + -d + n | -1 + -d + n ≥ 0] + 1/4·[2 + -d + n | 2 + -d + n ≥ 0] + 1/4·[2 + -d + n | 2 + -d + n ≥ 0] + 1/4·[-1 + -d + n | -1 + -d + n ≥ 0],1/4·[-1 + -d + n | -1 + -d + n ≥ 0] + 1/4·[-d + n | -d + n ≥ 0] + 1/4·[2 + -d + n | 2 + -d + n ≥ 0] + 1/4·[-d + n | -d + n ≥ 0])),ite(0 ≥ 1 + x,ite(y ≥ 1,1/4·[2 + -d + n | 2 + -d + n ≥ 0] + 1/4·[-1 + -d + n | -1 + -d + n ≥ 0] + 1/4·[-1 + -d + n | -1 + -d + n ≥ 0] + 1/4·[2 + -d + n | 2 + -d + n ≥ 0],ite(0 ≥ 1 + y,1/4·[2 + -d + n | 2 + -d + n ≥ 0] + 1/4·[2 + -d + n | 2 + -d + n ≥ 0] + 1/2·[-1 + -d + n | -1 + -d + n ≥ 0],1/4·[2 + -d + n | 2 + -d + n ≥ 0] + 1/4·[-d + n | -d + n ≥ 0] + 1/4·[-1 + -d + n | -1 + -d + n ≥ 0] + 1/4·[-d + n | -d + n ≥ 0])),ite(y ≥ 1,1/4·[-d + n | -d + n ≥ 0] + 1/4·[-1 + -d + n | -1 + -d + n ≥ 0] + 1/4·[-d + n | -d + n ≥ 0] + 1/4·[2 + -d + n | 2 + -d + n ≥ 0],ite(0 ≥ 1 + y,1/4·[-d + n | -d + n ≥ 0] + 1/4·[2 + -d + n | 2 + -d + n ≥ 0] + 1/4·[-d + n | -d + n ≥ 0] + 1/4·[-1 + -d + n | -1 + -d + n ≥ 0],[-d + n | -d + n ≥ 0]))))) ≼ h([1 | ⊤],[1 + -d + n | 1 + -d + n ≥ 0]) | | 1 + d ≥ 1 + n ==> 0 ≼ h([1 | ⊤],[1 + -d + n | 1 + -d + n ≥ 0]) | | | `- 2·[1 + -d + n | 1 + -d + n ≥ 0] | `- 2·[1 + -d + n | 1 + -d + n ≥ 0]