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₁

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₁

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₁

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)}