Preprocessing
Found invariant X₁ ≤ X₂ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ for location h
Found invariant X₀ ≤ 1 ∧ 0 ≤ X₀ for location g
Probabilistic Analysis
Probabilistic Program after Preprocessing
Start: f
Program_Vars: X₀, X₁, X₂
Temp_Vars:
Locations: f, g, h
Transitions:
g₀:f(X₀,X₁,X₂) → t₁:g(1,X₁,X₂) :|:
g₂:g(X₀,X₁,X₂) → t₃:h(X₀,X₂,X₂) :|: 1 ≤ X₀ ∧ X₀ ≤ 1 ∧ 0 ≤ X₀
g₄:h(X₀,X₁,X₂) → t₅:h(X₀,X₁-X₀,X₂) :|: 1 ≤ X₁ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ X₂
g₆:h(X₀,X₁,X₂) → [1/2]:t₇:g(1,X₁,X₂) :+: [1/2]:t₈:g(0,X₁,X₂) :|: X₁ ≤ 0 ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ X₂
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
η (X₀) = 1
h
h
g->h
p = 1
t₃ ∈ g₂
η (X₁) = X₂
τ = X₀ ≤ 1 ∧ 0 ≤ X₀ ∧ 1 ≤ X₀
h->g
p = 1/2
t₇ ∈ g₆
η (X₀) = 1
τ = X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ X₂ ∧ X₁ ≤ 0
h->g
p = 1/2
t₈ ∈ g₆
η (X₀) = 0
τ = X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ X₂ ∧ X₁ ≤ 0
h->h
p = 1
t₅ ∈ g₄
η (X₁) = X₁-X₀
τ = X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ X₂ ∧ 1 ≤ 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₄: inf {Infinity}
g₆: inf {Infinity}
Costbounds
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₄: inf {Infinity}
g₆: inf {Infinity}
Sizebounds
(g₀,g), X₀: 1 {O(1)}
(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]
MPRF for transition t₈: h(X₀,X₁,X₂) → g(Temp_Int₅₅,X₁,X₂) :|: X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ X₂ ∧ X₁ ≤ 0 ∧ X₁ ≤ X₂ ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ Temp_Int₅₅ ≤ 0 ∧ 0 ≤ Temp_Int₅₅ ∧ X₁ ≤ 0 of depth 1:
new bound:
1 {O(1)}
MPRF:
• g: [X₀]
• h: [1]
Show Graph
G
f
f
g
g
f->g
t₁
η (X₀) = 1
h
h
g->h
t₃
η (X₁) = X₂
τ = X₀ ≤ 1 ∧ 0 ≤ X₀ ∧ 1 ≤ X₀
h->g
t₇
η (X₀) = 1
τ = X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ X₂ ∧ X₁ ≤ 0
h->g
t₈
η (X₀) = 0
τ = X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ X₂ ∧ X₁ ≤ 0
h->h
t₅
η (X₁) = X₁-X₀
τ = X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ X₂ ∧ 1 ≤ X₁
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}
Costbounds
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₄: inf {Infinity}
g₆: inf {Infinity}
Sizebounds
(g₀,g), X₀: 1 {O(1)}
(g₀,g), X₁: X₁ {O(n)}
(g₀,g), X₂: X₂ {O(n)}
(g₂,h), X₀: 1 {O(1)}
(g₂,h), X₁: 2⋅X₂ {O(n)}
(g₂,h), X₂: X₂ {O(n)}
(g₄,h), X₀: 1 {O(1)}
(g₄,h), X₁: 2⋅X₂ {O(n)}
(g₄,h), X₂: X₂ {O(n)}
(g₆,g), X₀: 1 {O(1)}
(g₆,g), X₁: 8⋅X₂ {O(n)}
(g₆,g), X₂: 3⋅X₂ {O(n)}
Run probabilistic analysis on SCC: [g; h]
Plrf for transition g₂:g(X₀,X₁,X₂) → t₃:h(X₀,X₂,X₂) :|: 1 ≤ X₀ ∧ X₀ ≤ 1 ∧ 0 ≤ X₀:
new bound:
3 {O(1)}
PLRF:
• g: 1+2⋅X₀
• h: 2⋅X₀
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
η (X₀) = 1
h
h
g->h
p = 1
t₃ ∈ g₂
η (X₁) = X₂
τ = X₀ ≤ 1 ∧ 0 ≤ X₀ ∧ 1 ≤ X₀
h->g
p = 1/2
t₇ ∈ g₆
η (X₀) = 1
τ = X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ X₂ ∧ X₁ ≤ 0
h->g
p = 1/2
t₈ ∈ g₆
η (X₀) = 0
τ = X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ X₂ ∧ X₁ ≤ 0
h->h
p = 1
t₅ ∈ g₄
η (X₁) = X₁-X₀
τ = X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ X₂ ∧ 1 ≤ X₁
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₁,X₂) → [1/2]:t₇:g(1,X₁,X₂) :+: [1/2]:t₈:g(0,X₁,X₂) :|: X₁ ≤ 0 ∧ X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ X₂:
new bound:
2 {O(1)}
PLRF:
• g: 2⋅X₀
• h: 2
Show Graph
G
f
f
g
g
f->g
p = 1
t₁ ∈ g₀
η (X₀) = 1
h
h
g->h
p = 1
t₃ ∈ g₂
η (X₁) = X₂
τ = X₀ ≤ 1 ∧ 0 ≤ X₀ ∧ 1 ≤ X₀
h->g
p = 1/2
t₇ ∈ g₆
η (X₀) = 1
τ = X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ X₂ ∧ X₁ ≤ 0
h->g
p = 1/2
t₈ ∈ g₆
η (X₀) = 0
τ = X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ X₂ ∧ X₁ ≤ 0
h->h
p = 1
t₅ ∈ g₄
η (X₁) = X₁-X₀
τ = X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ X₂ ∧ 1 ≤ X₁
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)
Computed expected time bound for g₄:h→[t₅:1:h] with MPRF
Obtained bound 3⋅X₂ {O(n)}
MPRF for transition t₅: h(X₀,X₁,X₂) → h(X₀,X₁-X₀,X₂) :|: X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ X₂ ∧ 1 ≤ X₁ of depth 1:
new bound:
3⋅X₂ {O(n)}
MPRF:
• g: [X₂]
• h: [X₁]
Show Graph
G
f
f
g
g
f->g
t₁
η (X₀) = 1
h
h
g->h
t₃
η (X₁) = X₂
τ = X₀ ≤ 1 ∧ 0 ≤ X₀ ∧ 1 ≤ X₀
h->g
t₇
η (X₀) = 1
τ = X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ X₂ ∧ X₁ ≤ 0
h->g
t₈
η (X₀) = 0
τ = X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ X₂ ∧ X₁ ≤ 0
h->h
t₅
η (X₁) = X₁-X₀
τ = X₀ ≤ 1 ∧ 1 ≤ X₀ ∧ X₁ ≤ X₂ ∧ 1 ≤ X₁
Use classical time bound for t₁∈g₀: f→1:g
Use expected size bounds for t₁∈g₀: f→1:g
Use expected time bound for t₇∈g₆: h→1/2:g
Use classical size bounds for t₇∈g₆: h→1/2:g
Results of Probabilistic Analysis
All Bounds
Timebounds
Overall timebound:3⋅X₂+6 {O(n)}
g₀: 1 {O(1)}
g₂: 3 {O(1)}
g₄: 3⋅X₂ {O(n)}
g₆: 2 {O(1)}
Costbounds
Overall costbound: 3⋅X₂+8 {O(n)}
g₀: 1 {O(1)}
g₂: 3 {O(1)}
g₄: 3⋅X₂ {O(n)}
g₆: 4 {O(1)}
Sizebounds
(g₀,g), X₀: 1 {O(1)}
(g₀,g), X₁: X₁ {O(n)}
(g₀,g), X₂: X₂ {O(n)}
(g₂,h), X₀: 1 {O(1)}
(g₂,h), X₁: 2⋅X₂ {O(n)}
(g₂,h), X₂: X₂ {O(n)}
(g₄,h), X₀: 1 {O(1)}
(g₄,h), X₁: 2⋅X₂ {O(n)}
(g₄,h), X₂: X₂ {O(n)}
(g₆,g), X₀: 1 {O(1)}
(g₆,g), X₁: 8⋅X₂ {O(n)}
(g₆,g), X₂: X₂ {O(n)}