Preprocessing
Found invariant 0 ≤ X₁ ∧ X₀ ≤ X₁ ∧ X₀ ≤ 0 for location h
Found invariant 0 ≤ X₁ for location g
Found invariant 0 ≤ X₁ ∧ X₀ ≤ X₁ ∧ X₀ ≤ 0 for location i
Probabilistic Analysis
Probabilistic Program after Preprocessing
Start: f
Program_Vars: X₀, X₁
Temp_Vars:
Locations: f, g, h, i
Transitions:
g₀:f(X₀,X₁) -{0}> t₁:g(X₀,X₁) :|: 0 ≤ X₁
g₂:g(X₀,X₁) -{9}> [9/10]:t₃:h(1+X₀,X₁) :+: [1/10]:t₄:h(X₀,X₁) :|: 1+X₀ ≤ 0 ∧ 0 ≤ X₁
g₅:h(X₀,X₁) -{0}> t₆:i(X₀,X₁) :|: X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
g₇:h(X₀,X₁) -{0}> t₈:g(X₀,X₁) :|: X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
g₉:i(X₀,X₁) -{5}> [1/2]:t₁₀:i(X₀,X₁-100) :+: [1/2]:t₁₁:i(X₀,X₁-90) :|: 100 ≤ X₁ ∧ X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
g₁₂:i(X₀,X₁) -{0}> t₁₃:g(X₀,1000+X₁) :|: X₁ ≤ 99 ∧ X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
τ = 0 ≤ X₁
{0}
h
h
g->h
p = 9/10
t₃ ∈ g₂
η (X₀) = 1+X₀
τ = 0 ≤ X₁ ∧ 1+X₀ ≤ 0
{9}
g->h
p = 1/10
t₄ ∈ g₂
τ = 0 ≤ X₁ ∧ 1+X₀ ≤ 0
{9}
h->g
p = 1
t₈ ∈ g₇
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
{0}
i
i
h->i
p = 1
t₆ ∈ g₅
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
{0}
i->g
p = 1
t₁₃ ∈ g₁₂
η (X₁) = 1000+X₁
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ X₁ ≤ 99
{0}
i->i
p = 1/2
t₁₀ ∈ g₉
η (X₁) = X₁-100
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ 100 ≤ X₁
{5}
i->i
p = 1/2
t₁₁ ∈ g₉
η (X₁) = X₁-90
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ 100 ≤ X₁
{5}
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₅: inf {Infinity}
g₇: inf {Infinity}
g₉: inf {Infinity}
g₁₂: inf {Infinity}
Costbounds
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: 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; h; i]
MPRF for transition t₃: g(X₀,X₁) -{9}> h(1+X₀,X₁) :|: 0 ≤ X₁ ∧ 1+X₀ ≤ 0 of depth 1:
new bound:
X₀ {O(n)}
MPRF:
• g: [-X₀]
• h: [-X₀]
• i: [-X₀]
Show Graph
G
f
f
g
g
f->g
t₁
τ = 0 ≤ X₁
{0}
h
h
g->h
t₃
η (X₀) = 1+X₀
τ = 0 ≤ X₁ ∧ 1+X₀ ≤ 0
{9}
g->h
t₄
τ = 0 ≤ X₁ ∧ 1+X₀ ≤ 0
{9}
h->g
t₈
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
{0}
i
i
h->i
t₆
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
{0}
i->g
t₁₃
η (X₁) = 1000+X₁
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ X₁ ≤ 99
{0}
i->i
t₁₀
η (X₁) = X₁-100
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ 100 ≤ X₁
{5}
i->i
t₁₁
η (X₁) = X₁-90
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ 100 ≤ X₁
{5}
Classical Approximation after Lifting Classical Results
All Bounds
Timebounds
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: inf {Infinity}
g₅: inf {Infinity}
g₇: inf {Infinity}
g₉: inf {Infinity}
g₁₂: inf {Infinity}
Costbounds
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: 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₂,h), X₀: 2⋅X₀ {O(n)}
(g₂,h), X₁: 2⋅X₁+2200 {O(n)}
(g₅,i), X₀: X₀ {O(n)}
(g₅,i), X₁: 2⋅X₁+2200 {O(n)}
(g₇,g), X₀: X₀ {O(n)}
(g₇,g), X₁: X₁+1100 {O(n)}
(g₉,i), X₀: 2⋅X₀ {O(n)}
(g₉,i), X₁: 4⋅X₁+4400 {O(n)}
(g₁₂,g), X₀: X₀ {O(n)}
(g₁₂,g), X₁: 1100 {O(1)}
Run probabilistic analysis on SCC: [g; h; i]
Plrf for transition g₂:g(X₀,X₁) -{9}> [9/10]:t₃:h(1+X₀,X₁) :+: [1/10]:t₄:h(X₀,X₁) :|: 1+X₀ ≤ 0 ∧ 0 ≤ X₁:
new bound:
10/9⋅X₀ {O(n)}
PLRF:
• g: -10/9⋅X₀
• h: -10/9⋅X₀
• i: -10/9⋅X₀
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
τ = 0 ≤ X₁
{0}
h
h
g->h
p = 9/10
t₃ ∈ g₂
η (X₀) = 1+X₀
τ = 0 ≤ X₁ ∧ 1+X₀ ≤ 0
{9}
g->h
p = 1/10
t₄ ∈ g₂
τ = 0 ≤ X₁ ∧ 1+X₀ ≤ 0
{9}
h->g
p = 1
t₈ ∈ g₇
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
{0}
i
i
h->i
p = 1
t₆ ∈ g₅
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
{0}
i->g
p = 1
t₁₃ ∈ g₁₂
η (X₁) = 1000+X₁
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ X₁ ≤ 99
{0}
i->i
p = 1/2
t₁₀ ∈ g₉
η (X₁) = X₁-100
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ 100 ≤ X₁
{5}
i->i
p = 1/2
t₁₁ ∈ g₉
η (X₁) = X₁-90
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ 100 ≤ X₁
{5}
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)
Plrf for transition g₅:h(X₀,X₁) -{0}> t₆:i(X₀,X₁) :|: X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁:
new bound:
10/9⋅X₀ {O(n)}
PLRF:
• g: -10/9⋅X₀
• h: 1-10/9⋅X₀
• i: -10/9⋅X₀
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
τ = 0 ≤ X₁
{0}
h
h
g->h
p = 9/10
t₃ ∈ g₂
η (X₀) = 1+X₀
τ = 0 ≤ X₁ ∧ 1+X₀ ≤ 0
{9}
g->h
p = 1/10
t₄ ∈ g₂
τ = 0 ≤ X₁ ∧ 1+X₀ ≤ 0
{9}
h->g
p = 1
t₈ ∈ g₇
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
{0}
i
i
h->i
p = 1
t₆ ∈ g₅
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
{0}
i->g
p = 1
t₁₃ ∈ g₁₂
η (X₁) = 1000+X₁
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ X₁ ≤ 99
{0}
i->i
p = 1/2
t₁₀ ∈ g₉
η (X₁) = X₁-100
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ 100 ≤ X₁
{5}
i->i
p = 1/2
t₁₁ ∈ g₉
η (X₁) = X₁-90
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ 100 ≤ X₁
{5}
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)
Plrf for transition g₇:h(X₀,X₁) -{0}> t₈:g(X₀,X₁) :|: X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁:
new bound:
10/9⋅X₀ {O(n)}
PLRF:
• g: -10/9⋅X₀
• h: 1-10/9⋅X₀
• i: -10/9⋅X₀
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
τ = 0 ≤ X₁
{0}
h
h
g->h
p = 9/10
t₃ ∈ g₂
η (X₀) = 1+X₀
τ = 0 ≤ X₁ ∧ 1+X₀ ≤ 0
{9}
g->h
p = 1/10
t₄ ∈ g₂
τ = 0 ≤ X₁ ∧ 1+X₀ ≤ 0
{9}
h->g
p = 1
t₈ ∈ g₇
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
{0}
i
i
h->i
p = 1
t₆ ∈ g₅
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
{0}
i->g
p = 1
t₁₃ ∈ g₁₂
η (X₁) = 1000+X₁
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ X₁ ≤ 99
{0}
i->i
p = 1/2
t₁₀ ∈ g₉
η (X₁) = X₁-100
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ 100 ≤ X₁
{5}
i->i
p = 1/2
t₁₁ ∈ g₉
η (X₁) = X₁-90
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ 100 ≤ X₁
{5}
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)
Plrf for transition g₉:i(X₀,X₁) -{5}> [1/2]:t₁₀:i(X₀,X₁-100) :+: [1/2]:t₁₁:i(X₀,X₁-90) :|: 100 ≤ X₁ ∧ X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁:
new bound:
1/95⋅X₁+2000/171⋅X₀ {O(n)}
PLRF:
• g: 1/95⋅X₁-2000/171⋅X₀
• h: 200/19+1/95⋅X₁-2000/171⋅X₀
• i: 200/19+1/95⋅X₁-2000/171⋅X₀
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
τ = 0 ≤ X₁
{0}
h
h
g->h
p = 9/10
t₃ ∈ g₂
η (X₀) = 1+X₀
τ = 0 ≤ X₁ ∧ 1+X₀ ≤ 0
{9}
g->h
p = 1/10
t₄ ∈ g₂
τ = 0 ≤ X₁ ∧ 1+X₀ ≤ 0
{9}
h->g
p = 1
t₈ ∈ g₇
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
{0}
i
i
h->i
p = 1
t₆ ∈ g₅
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
{0}
i->g
p = 1
t₁₃ ∈ g₁₂
η (X₁) = 1000+X₁
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ X₁ ≤ 99
{0}
i->i
p = 1/2
t₁₀ ∈ g₉
η (X₁) = X₁-100
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ 100 ≤ X₁
{5}
i->i
p = 1/2
t₁₁ ∈ g₉
η (X₁) = X₁-90
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ 100 ≤ X₁
{5}
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)
Plrf for transition g₁₂:i(X₀,X₁) -{0}> t₁₃:g(X₀,1000+X₁) :|: X₁ ≤ 99 ∧ X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁:
new bound:
10/9⋅X₀ {O(n)}
PLRF:
• g: -10/9⋅X₀
• h: 1-10/9⋅X₀
• i: 1-10/9⋅X₀
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
τ = 0 ≤ X₁
{0}
h
h
g->h
p = 9/10
t₃ ∈ g₂
η (X₀) = 1+X₀
τ = 0 ≤ X₁ ∧ 1+X₀ ≤ 0
{9}
g->h
p = 1/10
t₄ ∈ g₂
τ = 0 ≤ X₁ ∧ 1+X₀ ≤ 0
{9}
h->g
p = 1
t₈ ∈ g₇
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
{0}
i
i
h->i
p = 1
t₆ ∈ g₅
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁
{0}
i->g
p = 1
t₁₃ ∈ g₁₂
η (X₁) = 1000+X₁
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ X₁ ≤ 99
{0}
i->i
p = 1/2
t₁₀ ∈ g₉
η (X₁) = X₁-100
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ 100 ≤ X₁
{5}
i->i
p = 1/2
t₁₁ ∈ g₉
η (X₁) = X₁-90
τ = X₀ ≤ 0 ∧ X₀ ≤ X₁ ∧ 0 ≤ X₁ ∧ 100 ≤ X₁
{5}
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)
Results of Probabilistic Analysis
All Bounds
Timebounds
Overall timebound:1/95⋅X₁+920/57⋅X₀+1 {O(n)}
g₀: 1 {O(1)}
g₂: 10/9⋅X₀ {O(n)}
g₅: 10/9⋅X₀ {O(n)}
g₇: 10/9⋅X₀ {O(n)}
g₉: 1/95⋅X₁+2000/171⋅X₀ {O(n)}
g₁₂: 10/9⋅X₀ {O(n)}
Costbounds
Overall costbound: 2/19⋅X₁+23420/171⋅X₀ {O(n)}
g₀: 0 {O(1)}
g₂: 20⋅X₀ {O(n)}
g₅: 0 {O(1)}
g₇: 0 {O(1)}
g₉: 2/19⋅X₁+20000/171⋅X₀ {O(n)}
g₁₂: 0 {O(1)}
Sizebounds
(g₀,g), X₀: X₀ {O(n)}
(g₀,g), X₁: X₁ {O(n)}
(g₂,h), X₀: X₀ {O(n)}
(g₂,h), X₁: 2⋅X₁+2200 {O(n)}
(g₅,i), X₀: X₀ {O(n)}
(g₅,i), X₁: 2⋅X₁+2200 {O(n)}
(g₇,g), X₀: X₀ {O(n)}
(g₇,g), X₁: X₁+1100 {O(n)}
(g₉,i), X₀: X₀ {O(n)}
(g₉,i), X₁: 4⋅X₁+4400 {O(n)}
(g₁₂,g), X₀: X₀ {O(n)}
(g₁₂,g), X₁: 1100 {O(1)}