Preprocessing
Found invariant 0 ≤ X₁ for location h
Found invariant 10 ≤ X₁ for location g
Probabilistic Analysis
Probabilistic Program after Preprocessing
Start: f
Program_Vars: X₀, X₁
Temp_Vars:
Locations: f, g, h
Transitions:
g₁:f(X₀,X₁) -{0}> t₂:g(X₀,X₁) :|: 10 ≤ X₁
g₃:g(X₀,X₁) -{3}> t₄:g(X₀,X₁+UNIFORM(1, 3)) :|: 3+X₁ ≤ X₀ ∧ 0 ≤ 1 ∧ 10 ≤ X₁
g₅:g(X₀,X₁) -{0}> t₆:h(X₀,X₁) :|: X₀ ≤ 2+X₁ ∧ 10 ≤ X₁
g₇:h(X₀,X₁) → [2/3]:t₈:h(X₀,X₁-10) :+: [1/3]:t₉:h(X₀,X₁) :|: 10 ≤ X₁ ∧ 0 ≤ X₁
Run classical analysis on SCC: [f]
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₁: 1 {O(1)}
g₃: inf {Infinity}
g₅: 1 {O(1)}
g₇: inf {Infinity}
Costbounds
Overall costbound: inf {Infinity}
g₁: inf {Infinity}
g₃: inf {Infinity}
g₅: inf {Infinity}
g₇: inf {Infinity}
Sizebounds
(g₁,g), X₀: X₀ {O(n)}
(g₁,g), X₁: X₁ {O(n)}
Run probabilistic analysis on SCC: [f]
Run classical analysis on SCC: [g]
MPRF for transition t₄: g(X₀,X₁) -{3}> g(X₀,Temp_Int₄₃) :|: 0 ≤ 1 ∧ 10 ≤ X₁ ∧ 1+X₁ ≤ Temp_Int₄₃ ∧ 1 ≤ Temp_Int₂ ∧ Temp_Int₂ ≤ 3 ∧ Temp_Int₄₃ ≤ 3+X₁ ∧ 10 ≤ X₁ ∧ 3+X₁ ≤ X₀ ∧ Temp_Int₂+X₁ ≤ Temp_Int₁ ∧ Temp_Int₁ ≤ Temp_Int₂+X₁ ∧ Temp_Int₁ ≤ Temp_Int₂+X₁ ∧ Temp_Int₂+X₁ ≤ Temp_Int₁ ∧ 1 ≤ Temp_Int₂ ∧ Temp_Int₂ ≤ 3 ∧ 3+X₁ ≤ X₀ of depth 1:
new bound:
X₀+X₁ {O(n)}
MPRF:
• g: [X₀-X₁]
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₁: 1 {O(1)}
g₃: X₀+X₁ {O(n)}
g₅: 1 {O(1)}
g₇: inf {Infinity}
Costbounds
Overall costbound: inf {Infinity}
g₁: inf {Infinity}
g₃: inf {Infinity}
g₅: inf {Infinity}
g₇: inf {Infinity}
Sizebounds
(g₁,g), X₀: X₀ {O(n)}
(g₁,g), X₁: X₁ {O(n)}
(g₃,g), X₀: X₀ {O(n)}
(g₃,g), X₁: 3⋅X₀+4⋅X₁ {O(n)}
(g₅,h), X₀: 2⋅X₀ {O(n)}
(g₅,h), X₁: 3⋅X₀+5⋅X₁ {O(n)}
Run probabilistic analysis on SCC: [g]
Run classical analysis on SCC: [h]
MPRF for transition t₈: h(X₀,X₁) → h(X₀,X₁-10) :|: 0 ≤ X₁ ∧ 10 ≤ X₁ of depth 1:
new bound:
3⋅X₀+5⋅X₁+1 {O(n)}
MPRF:
• h: [1+X₁]
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₁: 1 {O(1)}
g₃: X₀+X₁ {O(n)}
g₅: 1 {O(1)}
g₇: inf {Infinity}
Costbounds
Overall costbound: inf {Infinity}
g₁: inf {Infinity}
g₃: inf {Infinity}
g₅: inf {Infinity}
g₇: inf {Infinity}
Sizebounds
(g₁,g), X₀: X₀ {O(n)}
(g₁,g), X₁: X₁ {O(n)}
(g₃,g), X₀: X₀ {O(n)}
(g₃,g), X₁: 3⋅X₀+4⋅X₁ {O(n)}
(g₅,h), X₀: 2⋅X₀ {O(n)}
(g₅,h), X₁: 3⋅X₀+5⋅X₁ {O(n)}
(g₇,h), X₀: 4⋅X₀ {O(n)}
(g₇,h), X₁: 10⋅X₁+6⋅X₀ {O(n)}
Run probabilistic analysis on SCC: [h]
Plrf for transition g₇:h(X₀,X₁) → [2/3]:t₈:h(X₀,X₁-10) :+: [1/3]:t₉:h(X₀,X₁) :|: 10 ≤ X₁ ∧ 0 ≤ X₁:
new bound:
3/4⋅X₁+9/20⋅X₀+3/2 {O(n)}
PLRF:
• h: 3/2+3/20⋅X₁
Use expected size bounds for entry point (g₅:g→[t₆:1:h],h)
Use classical time bound for entry point (g₅:g→[t₆:1:h],h)
Results of Probabilistic Analysis
All Bounds
Timebounds
Overall timebound:29/20⋅X₀+7/4⋅X₁+7/2 {O(n)}
g₁: 1 {O(1)}
g₃: X₀+X₁ {O(n)}
g₅: 1 {O(1)}
g₇: 3/4⋅X₁+9/20⋅X₀+3/2 {O(n)}
Costbounds
Overall costbound: 39/10⋅X₀+9/2⋅X₁+3 {O(n)}
g₁: 0 {O(1)}
g₃: 3⋅X₀+3⋅X₁ {O(n)}
g₅: 0 {O(1)}
g₇: 3/2⋅X₁+9/10⋅X₀+3 {O(n)}
Sizebounds
(g₁,g), X₀: X₀ {O(n)}
(g₁,g), X₁: X₁ {O(n)}
(g₃,g), X₀: X₀ {O(n)}
(g₃,g), X₁: 3⋅X₀+4⋅X₁ {O(n)}
(g₅,h), X₀: 2⋅X₀ {O(n)}
(g₅,h), X₁: 3⋅X₀+5⋅X₁ {O(n)}
(g₇,h), X₀: 4⋅X₀ {O(n)}
(g₇,h), X₁: 3⋅X₀+5⋅X₁ {O(n)}