Expected Cost
|
+- [f]
|    0
|
+- [Program]
|    flag_ab :~ {1 : 1}
|    flag_ac :~ {1 : 1}
|    flag_bc :~ {1 : 1}
|    Choice
|      1/3: flag_ac :~ {1 : 0}
|           flag_bc :~ {1 : 0}
|           Choice
|             1/2: flag_ab :~ {1 : 0}
|             1/2: Choice
|                    1/2: flag_ac :~ {1 : 0}
|                         flag_bc :~ {1 : 0}
|                    1/2: flag_ab :~ {1 : 0}
|                         flag_ac :~ {1 : 0}
|      2/3: Skip
|    Tick(1)
|    0:If(1 ≥ flag_ab ∧  flag_ab ≥ 1) Then
|        1:While(flag_ab ≥ 1)
|            Choice
|              1/3: flag_ab :~ {1 : 0}
|              2/3: Choice
|                     1/2: flag_ab :~ {1 : 0}
|                     1/2: flag_ab :~ {1 : 1}
|            Tick(1)
|      Else
|        Skip
|    2:If(1 ≥ flag_ac ∧  flag_ac ≥ 1) Then
|        3:While(flag_ac ≥ 1)
|            Choice
|              1/3: flag_ac :~ {1 : 0}
|              2/3: flag_ac :~ {1 : 0}
|            Tick(1)
|      Else
|        Skip
|    4:If(1 ≥ flag_bc ∧  flag_bc ≥ 1) Then
|        5:While(flag_bc ≥ 1)
|            Choice
|              1/2: flag_bc :~ {1 : 0}
|              1/2: flag_bc :~ {1 : 0}
|            Tick(1)
|      Else
|        Skip
|
+- Expected Cost
|  |
|  +- [f]
|  |    0
|  |
|  +- [Program]
|  |    0:If(1 ≥ flag_ab ∧  flag_ab ≥ 1) Then
|  |        1:While(flag_ab ≥ 1)
|  |            Choice
|  |              1/3: flag_ab :~ {1 : 0}
|  |              2/3: Choice
|  |                     1/2: flag_ab :~ {1 : 0}
|  |                     1/2: flag_ab :~ {1 : 1}
|  |            Tick(1)
|  |      Else
|  |        Skip
|  |
|  +- While.step
|  |  |
|  |  +- [Problem]
|  |  |    1:While(flag_ab ≥ 1)
|  |  |        Choice
|  |  |          1/3: flag_ab :~ {1 : 0}
|  |  |          2/3: Choice
|  |  |                 1/2: flag_ab :~ {1 : 0}
|  |  |                 1/2: flag_ab :~ {1 : 1}
|  |  |        Tick(1)
|  |  |
|  |  +- [f]
|  |  |    0
|  |  |
|  |  +- Expected Cost Body
|  |  |  |
|  |  |  `- [1 | ⊤]
|  |  |
|  |  +- linear-template
|  |  |  |
|  |  |  `- 1 + [flag_ab | flag_ab ≥ 0]
|  |  |
|  |  +- [Norms]
|  |  |    [[1 | ⊤],[flag_ab | flag_ab ≥ 0]]
|  |  |
|  |  +- [Invariant]
|  |  |    flag_ab ≥ 1 ==> [1 | ⊤] + h([1 | ⊤],1/3) ≼ h([1 | ⊤],[flag_ab | flag_ab ≥ 0])
|  |  |    1 ≥ 1 + flag_ab ==> 0 ≼ h([1 | ⊤],[flag_ab | flag_ab ≥ 0])
|  |  |
|  |  `- 3/2·[flag_ab | flag_ab ≥ 0]
|  |
|  `- [1 ≥ flag_ab ∧  flag_ab ≥ 1] · 3/2·[flag_ab | flag_ab ≥ 0]
|
+- Expected Cost
|  |
|  +- [f]
|  |    0
|  |
|  +- [Program]
|  |    2:If(1 ≥ flag_ac ∧  flag_ac ≥ 1) Then
|  |        3:While(flag_ac ≥ 1)
|  |            Choice
|  |              1/3: flag_ac :~ {1 : 0}
|  |              2/3: flag_ac :~ {1 : 0}
|  |            Tick(1)
|  |      Else
|  |        Skip
|  |    4:If(1 ≥ flag_bc ∧  flag_bc ≥ 1) Then
|  |        5:While(flag_bc ≥ 1)
|  |            Choice
|  |              1/2: flag_bc :~ {1 : 0}
|  |              1/2: flag_bc :~ {1 : 0}
|  |            Tick(1)
|  |      Else
|  |        Skip
|  |
|  +- Expected Cost
|  |  |
|  |  +- [f]
|  |  |    0
|  |  |
|  |  +- [Program]
|  |  |    2:If(1 ≥ flag_ac ∧  flag_ac ≥ 1) Then
|  |  |        3:While(flag_ac ≥ 1)
|  |  |            Choice
|  |  |              1/3: flag_ac :~ {1 : 0}
|  |  |              2/3: flag_ac :~ {1 : 0}
|  |  |            Tick(1)
|  |  |      Else
|  |  |        Skip
|  |  |
|  |  +- While.step
|  |  |  |
|  |  |  +- [Problem]
|  |  |  |    3:While(flag_ac ≥ 1)
|  |  |  |        Choice
|  |  |  |          1/3: flag_ac :~ {1 : 0}
|  |  |  |          2/3: flag_ac :~ {1 : 0}
|  |  |  |        Tick(1)
|  |  |  |
|  |  |  +- [f]
|  |  |  |    0
|  |  |  |
|  |  |  +- Expected Cost Body
|  |  |  |  |
|  |  |  |  `- [1 | ⊤]
|  |  |  |
|  |  |  +- linear-template
|  |  |  |  |
|  |  |  |  `- 1 + [flag_ac | flag_ac ≥ 0]
|  |  |  |
|  |  |  +- [Norms]
|  |  |  |    [[1 | ⊤],[flag_ac | flag_ac ≥ 0]]
|  |  |  |
|  |  |  +- [Invariant]
|  |  |  |    flag_ac ≥ 1 ==> [1 | ⊤] + h([1 | ⊤],0) ≼ h([1 | ⊤],[flag_ac | flag_ac ≥ 0])
|  |  |  |    1 ≥ 1 + flag_ac ==> 0 ≼ h([1 | ⊤],[flag_ac | flag_ac ≥ 0])
|  |  |  |
|  |  |  `- [flag_ac | flag_ac ≥ 0]
|  |  |
|  |  `- [1 ≥ flag_ac ∧  flag_ac ≥ 1] · [flag_ac | flag_ac ≥ 0]
|  |
|  +- Expected Cost
|  |  |
|  |  +- [f]
|  |  |    0
|  |  |
|  |  +- [Program]
|  |  |    4:If(1 ≥ flag_bc ∧  flag_bc ≥ 1) Then
|  |  |        5:While(flag_bc ≥ 1)
|  |  |            Choice
|  |  |              1/2: flag_bc :~ {1 : 0}
|  |  |              1/2: flag_bc :~ {1 : 0}
|  |  |            Tick(1)
|  |  |      Else
|  |  |        Skip
|  |  |
|  |  +- While.step
|  |  |  |
|  |  |  +- [Problem]
|  |  |  |    5:While(flag_bc ≥ 1)
|  |  |  |        Choice
|  |  |  |          1/2: flag_bc :~ {1 : 0}
|  |  |  |          1/2: flag_bc :~ {1 : 0}
|  |  |  |        Tick(1)
|  |  |  |
|  |  |  +- [f]
|  |  |  |    0
|  |  |  |
|  |  |  +- Expected Cost Body
|  |  |  |  |
|  |  |  |  `- [1 | ⊤]
|  |  |  |
|  |  |  +- linear-template
|  |  |  |  |
|  |  |  |  `- 1 + [flag_bc | flag_bc ≥ 0]
|  |  |  |
|  |  |  +- [Norms]
|  |  |  |    [[1 | ⊤],[flag_bc | flag_bc ≥ 0]]
|  |  |  |
|  |  |  +- [Invariant]
|  |  |  |    flag_bc ≥ 1 ==> [1 | ⊤] + h([1 | ⊤],0) ≼ h([1 | ⊤],[flag_bc | flag_bc ≥ 0])
|  |  |  |    1 ≥ 1 + flag_bc ==> 0 ≼ h([1 | ⊤],[flag_bc | flag_bc ≥ 0])
|  |  |  |
|  |  |  `- [flag_bc | flag_bc ≥ 0]
|  |  |
|  |  `- [1 ≥ flag_bc ∧  flag_bc ≥ 1] · [flag_bc | flag_bc ≥ 0]
|  |
|  +- Expected Cost
|  |  |
|  |  +- [f]
|  |  |    [1 ≥ flag_bc ∧  flag_bc ≥ 1] · [flag_bc | flag_bc ≥ 0]
|  |  |
|  |  +- [Program]
|  |  |    2:If(1 ≥ flag_ac ∧  flag_ac ≥ 1) Then
|  |  |        3:While(flag_ac ≥ 1)
|  |  |            Choice
|  |  |              1/3: flag_ac :~ {1 : 0}
|  |  |              2/3: flag_ac :~ {1 : 0}
|  |  |            Tick(1)
|  |  |      Else
|  |  |        Skip
|  |  |
|  |  `- [1 ≥ flag_bc ∧  flag_bc ≥ 1] · [flag_bc | flag_bc ≥ 0]
|  |
|  `- [1 ≥ flag_ac ∧  flag_ac ≥ 1] · [flag_ac | flag_ac ≥ 0] + [1 ≥ flag_bc ∧  flag_bc ≥ 1] · [flag_bc | flag_bc ≥ 0]
|
+- Expected Cost
|  |
|  +- [f]
|  |    [1 ≥ flag_ac ∧  flag_ac ≥ 1] · [flag_ac | flag_ac ≥ 0] + [1 ≥ flag_bc ∧  flag_bc ≥ 1] · [flag_bc | flag_bc ≥ 0]
|  |
|  +- [Program]
|  |    0:If(1 ≥ flag_ab ∧  flag_ab ≥ 1) Then
|  |        1:While(flag_ab ≥ 1)
|  |            Choice
|  |              1/3: flag_ab :~ {1 : 0}
|  |              2/3: Choice
|  |                     1/2: flag_ab :~ {1 : 0}
|  |                     1/2: flag_ab :~ {1 : 1}
|  |            Tick(1)
|  |      Else
|  |        Skip
|  |
|  `- [1 ≥ flag_ac ∧  flag_ac ≥ 1] · [flag_ac | flag_ac ≥ 0] + [1 ≥ flag_bc ∧  flag_bc ≥ 1] · [flag_bc | flag_bc ≥ 0]
|
`- 83/24