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₁+Binomial (4, 1/2)) :|: 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₁
Show Graph
G
f
f
g
g
f->g
p = 1
t₂ ∈ g₁
τ = 10 ≤ X₁
{0}
g->g
p = 1
t₄ ∈ g₃
η (X₁) = X₁+Binomial (4, 1/2)
τ = 0 ≤ 1 ∧ 10 ≤ X₁ ∧ 3+X₁ ≤ X₀
{3}
h
h
g->h
p = 1
t₆ ∈ g₅
τ = 10 ≤ X₁ ∧ X₀ ≤ 2+X₁
{0}
h->h
p = 2/3
t₈ ∈ g₇
η (X₁) = X₁-10
τ = 0 ≤ X₁ ∧ 10 ≤ X₁
h->h
p = 1/3
t₉ ∈ g₇
τ = 0 ≤ X₁ ∧ 10 ≤ 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]
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)}
(g₃,g), X₀: X₀ {O(n)}
(g₅,h), X₀: 2⋅X₀ {O(n)}
Run probabilistic analysis on SCC: [g]
Plrf for transition g₃:g(X₀,X₁) -{3}> t₄:g(X₀,X₁+Binomial (4, 1/2)) :|: 3+X₁ ≤ X₀ ∧ 0 ≤ 1 ∧ 10 ≤ X₁:
new bound:
1/2⋅X₀+1/2⋅X₁+1/2 {O(n)}
PLRF:
• g: 1/2+1/2⋅X₀-1/2⋅X₁
Show Graph
G
f
f
g
g
f->g
p = 1
t₂ ∈ g₁
τ = 10 ≤ X₁
{0}
g->g
p = 1
t₄ ∈ g₃
η (X₁) = X₁+Binomial (4, 1/2)
τ = 0 ≤ 1 ∧ 10 ≤ X₁ ∧ 3+X₁ ≤ X₀
{3}
h
h
g->h
p = 1
t₆ ∈ g₅
τ = 10 ≤ X₁ ∧ X₀ ≤ 2+X₁
{0}
h->h
p = 2/3
t₈ ∈ g₇
η (X₁) = X₁-10
τ = 0 ≤ X₁ ∧ 10 ≤ X₁
h->h
p = 1/3
t₉ ∈ g₇
τ = 0 ≤ X₁ ∧ 10 ≤ X₁
Use expected size bounds for entry point (g₁:f→[t₂:1:g],g)
Use expected size bounds for entry point (g₁:f→[t₂:1:g],g)
Use classical time bound for entry point (g₁:f→[t₂:1:g],g)
Run classical analysis on SCC: [h]
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₁: 1 {O(1)}
g₃: 1/2⋅X₀+1/2⋅X₁+1/2 {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₁: 2⋅X₁+X₀+1 {O(n)}
(g₅,h), X₀: 2⋅X₀ {O(n)}
(g₅,h), X₁: 3⋅X₁+X₀+1 {O(n)}
(g₇,h), X₀: 4⋅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/20⋅X₀+9/20⋅X₁+33/20 {O(n)}
PLRF:
• h: 3/2+3/20⋅X₁
Show Graph
G
f
f
g
g
f->g
p = 1
t₂ ∈ g₁
τ = 10 ≤ X₁
{0}
g->g
p = 1
t₄ ∈ g₃
η (X₁) = X₁+Binomial (4, 1/2)
τ = 0 ≤ 1 ∧ 10 ≤ X₁ ∧ 3+X₁ ≤ X₀
{3}
h
h
g->h
p = 1
t₆ ∈ g₅
τ = 10 ≤ X₁ ∧ X₀ ≤ 2+X₁
{0}
h->h
p = 2/3
t₈ ∈ g₇
η (X₁) = X₁-10
τ = 0 ≤ X₁ ∧ 10 ≤ X₁
h->h
p = 1/3
t₉ ∈ g₇
τ = 0 ≤ X₁ ∧ 10 ≤ 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:13/20⋅X₀+19/20⋅X₁+83/20 {O(n)}
g₁: 1 {O(1)}
g₃: 1/2⋅X₀+1/2⋅X₁+1/2 {O(n)}
g₅: 1 {O(1)}
g₇: 3/20⋅X₀+9/20⋅X₁+33/20 {O(n)}
Costbounds
Overall costbound: 12/5⋅X₁+9/5⋅X₀+24/5 {O(n)}
g₁: 0 {O(1)}
g₃: 3/2⋅X₀+3/2⋅X₁+3/2 {O(n)}
g₅: 0 {O(1)}
g₇: 3/10⋅X₀+9/10⋅X₁+33/10 {O(n)}
Sizebounds
(g₁,g), X₀: X₀ {O(n)}
(g₁,g), X₁: X₁ {O(n)}
(g₃,g), X₀: X₀ {O(n)}
(g₃,g), X₁: 2⋅X₁+X₀+1 {O(n)}
(g₅,h), X₀: 2⋅X₀ {O(n)}
(g₅,h), X₁: 3⋅X₁+X₀+1 {O(n)}
(g₇,h), X₀: 4⋅X₀ {O(n)}
(g₇,h), X₁: 3⋅X₁+X₀+1 {O(n)}