ExecutionLog
|
`- Expected Cost
   |
   +- [f]
   |    0
   |
   +- [Program]
   |    i :~ {1 : 0}
   |    0:While(5  1 + i)
   |        1:If(0  i   i  0) Then
   |            i :~ {1 : 1 + i}
   |          Else
   |            2:If(1  i   i  1) Then
   |                Choice
   |                  1/5: i :~ {1 : 1}
   |                  4/5: i :~ {1 : 1 + i}
   |              Else
   |                3:If(2  i   i  2) Then
   |                    Choice
   |                      2/5: i :~ {1 : 2}
   |                      3/5: i :~ {1 : 1 + i}
   |                  Else
   |                    4:If(3  i   i  3) Then
   |                        Choice
   |                          3/5: i :~ {1 : 3}
   |                          2/5: i :~ {1 : 1 + i}
   |                      Else
   |                        Choice
   |                          4/5: i :~ {1 : 4}
   |                          1/5: i :~ {1 : 1 + i}
   |        Tick(1)
   |
   +- While.step
   |  |
   |  +- [Problem]
   |  |    0:While(5  1 + i)
   |  |        1:If(0  i   i  0) Then
   |  |            i :~ {1 : 1 + i}
   |  |          Else
   |  |            2:If(1  i   i  1) Then
   |  |                Choice
   |  |                  1/5: i :~ {1 : 1}
   |  |                  4/5: i :~ {1 : 1 + i}
   |  |              Else
   |  |                3:If(2  i   i  2) Then
   |  |                    Choice
   |  |                      2/5: i :~ {1 : 2}
   |  |                      3/5: i :~ {1 : 1 + i}
   |  |                  Else
   |  |                    4:If(3  i   i  3) Then
   |  |                        Choice
   |  |                          3/5: i :~ {1 : 3}
   |  |                          2/5: i :~ {1 : 1 + i}
   |  |                      Else
   |  |                        Choice
   |  |                          4/5: i :~ {1 : 4}
   |  |                          1/5: i :~ {1 : 1 + i}
   |  |        Tick(1)
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- Expected Cost Body
   |  |  |
   |  |  `- [1 | ]
   |  |
   |  +- linear-template
   |  |  |
   |  |  `- 1 + [5 + -i | 5 + -i  0]
   |  |
   |  +- [Norms]
   |  |    [[1 | ],[5 + -i | 5 + -i  0]]
   |  |
   |  +- [Invariant]
   |  |    5  1 + i ==> [1 | ] + h([1 | ],ite(0  i   i  0,[4 + -i | 4 + -i  0],ite(1  i   i  1,4/5 + 4/5[4 + -i | 4 + -i  0],ite(2  i   i  2,6/5 + 3/5[4 + -i | 4 + -i  0],ite(3  i   i  3,6/5 + 2/5[4 + -i | 4 + -i  0],4/5 + 1/5[4 + -i | 4 + -i  0])))))  h([1 | ],[5 + -i | 5 + -i  0])
   |  |    1 + i  6 ==> 0  h([1 | ],[5 + -i | 5 + -i  0])
   |  |
   |  `- 5[5 + -i | 5 + -i  0]
   |
   `- 25

[Success] 25
Degree: 0