Preprocessing

Found invariant 1 ≤ X₃ ∧ 1 ≤ X₀+X₃ ∧ X₀ ≤ X₃ ∧ 0 ≤ X₀ for location h

Found invariant X₃ ≤ X₀ ∧ 0 ≤ X₀ for location j

Found invariant X₃ ≤ X₀ ∧ 1 ≤ X₁ ∧ 1 ≤ X₀+X₁ ∧ 0 ≤ X₀ for location k

Found invariant 0 ≤ X₀ for location g

Probabilistic Analysis

Probabilistic Program after Preprocessing

Start: f
Program_Vars: X₀, X₁, X₂, X₃, X₄
Temp_Vars:
Locations: f, g, h, j, k
Transitions:
g₂:f(X₀,X₁,X₂,X₃,X₄) -{0}> t₃:g(0,X₁,X₂,X₃,X₄) :|:
g₄:g(X₀,X₁,X₂,X₃,X₄) -{0}> t₅:h(X₀+UNIFORM(0, 1),X₁+3⋅X₄,X₂,X₃,X₄) :|: 1+X₀ ≤ X₃ ∧ 0 ≤ 1 ∧ 0 ≤ X₀
g₆:h(X₀,X₁,X₂,X₃,X₄) -{0}> t₇:g(X₀,X₁+Binomial (3, 1/2),X₂,X₃,X₄) :|: 0 ≤ 1 ∧ 1 ≤ X₀+X₃ ∧ 1 ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₃
g₈:g(X₀,X₁,X₂,X₃,X₄) -{0}> t₉:j(X₀,X₁,X₂,X₃,X₄) :|: X₃ ≤ X₀ ∧ 0 ≤ X₀
g₁₀:j(X₀,X₁,X₂,X₃,X₄) -{0}> t₁₁:k(X₀,X₁,X₂,X₃,X₄) :|: 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀
g₁₂:k(X₀,X₁,X₂,X₃,X₄) → t₁₃:k(X₀,X₁,X₂-1,X₃,X₄) :|: 1 ≤ X₂ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀
g₁₄:k(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₁₅:j(X₀,1+X₁,X₂,X₃,X₄) :+: [3/4]:t₁₆:j(X₀,X₁-1,X₂,X₃,X₄) :|: X₂ ≤ 0 ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ 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₈: 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}
g₁₀: inf {Infinity}
g₁₂: inf {Infinity}
g₁₄: inf {Infinity}

Sizebounds

(g₂,g), X₀: 0 {O(1)}
(g₂,g), X₁: X₁ {O(n)}
(g₂,g), X₂: X₂ {O(n)}
(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]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₂: 1 {O(1)}
g₄: inf {Infinity}
g₆: 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}
g₁₀: inf {Infinity}
g₁₂: inf {Infinity}
g₁₄: inf {Infinity}

Sizebounds

(g₂,g), X₀: 0 {O(1)}
(g₂,g), X₁: X₁ {O(n)}
(g₂,g), X₂: X₂ {O(n)}
(g₂,g), X₃: X₃ {O(n)}
(g₂,g), X₄: X₄ {O(n)}
(g₄,h), X₂: X₂ {O(n)}
(g₄,h), X₃: X₃ {O(n)}
(g₄,h), X₄: X₄ {O(n)}
(g₆,g), X₂: X₂ {O(n)}
(g₆,g), X₃: X₃ {O(n)}
(g₆,g), X₄: X₄ {O(n)}
(g₈,j), X₂: 2⋅X₂ {O(n)}
(g₈,j), X₃: 2⋅X₃ {O(n)}
(g₈,j), X₄: 2⋅X₄ {O(n)}

Run probabilistic analysis on SCC: [g; h]

Plrf for transition g₄:g(X₀,X₁,X₂,X₃,X₄) -{0}> t₅:h(X₀+UNIFORM(0, 1),X₁+3⋅X₄,X₂,X₃,X₄) :|: 1+X₀ ≤ X₃ ∧ 0 ≤ 1 ∧ 0 ≤ X₀:

new bound:

2⋅X₃ {O(n)}

PLRF:

• g: 2⋅X₃-2⋅X₀
• h: 2⋅X₃-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)

Plrf for transition g₆:h(X₀,X₁,X₂,X₃,X₄) -{0}> t₇:g(X₀,X₁+Binomial (3, 1/2),X₂,X₃,X₄) :|: 0 ≤ 1 ∧ 1 ≤ X₀+X₃ ∧ 1 ≤ X₃ ∧ 0 ≤ X₀ ∧ X₀ ≤ X₃:

new bound:

2⋅X₃ {O(n)}

PLRF:

• g: 2⋅X₃-2⋅X₀
• h: 1+2⋅X₃-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: [j; k]

MPRF for transition t₁₃: k(X₀,X₁,X₂,X₃,X₄) → k(X₀,X₁,X₂-1,X₃,X₄) :|: 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀ ∧ 1 ≤ X₂ of depth 1:

new bound:

2⋅X₂ {O(n)}

MPRF:

• j: [X₂]
• k: [X₂]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:inf {Infinity}
g₂: 1 {O(1)}
g₄: 2⋅X₃ {O(n)}
g₆: 2⋅X₃ {O(n)}
g₈: 1 {O(1)}
g₁₀: inf {Infinity}
g₁₂: 2⋅X₂ {O(n)}
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}
g₁₄: inf {Infinity}

Sizebounds

(g₂,g), X₀: 0 {O(1)}
(g₂,g), X₁: X₁ {O(n)}
(g₂,g), X₂: X₂ {O(n)}
(g₂,g), X₃: X₃ {O(n)}
(g₂,g), X₄: X₄ {O(n)}
(g₄,h), X₀: X₃ {O(n)}
(g₄,h), X₁: 12⋅X₃⋅X₄+3⋅X₃+X₁ {O(n^2)}
(g₄,h), X₂: X₂ {O(n)}
(g₄,h), X₃: X₃ {O(n)}
(g₄,h), X₄: X₄ {O(n)}
(g₆,g), X₀: X₃ {O(n)}
(g₆,g), X₁: 12⋅X₃⋅X₄+3⋅X₃+X₁ {O(n^2)}
(g₆,g), X₂: X₂ {O(n)}
(g₆,g), X₃: X₃ {O(n)}
(g₆,g), X₄: X₄ {O(n)}
(g₈,j), X₀: X₃ {O(n)}
(g₈,j), X₁: 12⋅X₃⋅X₄+2⋅X₁+3⋅X₃ {O(n^2)}
(g₈,j), X₂: 2⋅X₂ {O(n)}
(g₈,j), X₃: 2⋅X₃ {O(n)}
(g₈,j), X₄: 2⋅X₄ {O(n)}
(g₁₀,k), X₂: 2⋅X₂ {O(n)}
(g₁₀,k), X₃: 2⋅X₃ {O(n)}
(g₁₀,k), X₄: 2⋅X₄ {O(n)}
(g₁₂,k), X₂: 2⋅X₂ {O(n)}
(g₁₂,k), X₃: 2⋅X₃ {O(n)}
(g₁₂,k), X₄: 2⋅X₄ {O(n)}
(g₁₄,j), X₂: 4⋅X₂ {O(n)}
(g₁₄,j), X₃: 4⋅X₃ {O(n)}
(g₁₄,j), X₄: 4⋅X₄ {O(n)}

Run probabilistic analysis on SCC: [j; k]

Plrf for transition g₁₀:j(X₀,X₁,X₂,X₃,X₄) -{0}> t₁₁:k(X₀,X₁,X₂,X₃,X₄) :|: 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀:

new bound:

24⋅X₃⋅X₄+4⋅X₁+6⋅X₃+1 {O(n^2)}

PLRF:

• j: 1+2⋅X₁
• k: 2⋅X₁

Use expected size bounds for entry point (g₈:g→[t₉:1:j],j)
Use classical time bound for entry point (g₈:g→[t₉:1:j],j)

Plrf for transition g₁₄:k(X₀,X₁,X₂,X₃,X₄) → [1/4]:t₁₅:j(X₀,1+X₁,X₂,X₃,X₄) :+: [3/4]:t₁₆:j(X₀,X₁-1,X₂,X₃,X₄) :|: X₂ ≤ 0 ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₁ ∧ 0 ≤ X₀ ∧ X₃ ≤ X₀:

new bound:

24⋅X₃⋅X₄+4⋅X₁+6⋅X₃ {O(n^2)}

PLRF:

• j: 2⋅X₁
• k: 2⋅X₁

Use expected size bounds for entry point (g₈:g→[t₉:1:j],j)
Use classical time bound for entry point (g₈:g→[t₉:1:j],j)

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:48⋅X₃⋅X₄+16⋅X₃+2⋅X₂+8⋅X₁+3 {O(n^2)}
g₂: 1 {O(1)}
g₄: 2⋅X₃ {O(n)}
g₆: 2⋅X₃ {O(n)}
g₈: 1 {O(1)}
g₁₀: 24⋅X₃⋅X₄+4⋅X₁+6⋅X₃+1 {O(n^2)}
g₁₂: 2⋅X₂ {O(n)}
g₁₄: 24⋅X₃⋅X₄+4⋅X₁+6⋅X₃ {O(n^2)}

Costbounds

Overall costbound: 48⋅X₃⋅X₄+12⋅X₃+2⋅X₂+8⋅X₁ {O(n^2)}
g₂: 0 {O(1)}
g₄: 0 {O(1)}
g₆: 0 {O(1)}
g₈: 0 {O(1)}
g₁₀: 0 {O(1)}
g₁₂: 2⋅X₂ {O(n)}
g₁₄: 48⋅X₃⋅X₄+12⋅X₃+8⋅X₁ {O(n^2)}

Sizebounds

(g₂,g), X₀: 0 {O(1)}
(g₂,g), X₁: X₁ {O(n)}
(g₂,g), X₂: X₂ {O(n)}
(g₂,g), X₃: X₃ {O(n)}
(g₂,g), X₄: X₄ {O(n)}
(g₄,h), X₀: X₃ {O(n)}
(g₄,h), X₁: 12⋅X₃⋅X₄+3⋅X₃+X₁ {O(n^2)}
(g₄,h), X₂: X₂ {O(n)}
(g₄,h), X₃: X₃ {O(n)}
(g₄,h), X₄: X₄ {O(n)}
(g₆,g), X₀: X₃ {O(n)}
(g₆,g), X₁: 12⋅X₃⋅X₄+3⋅X₃+X₁ {O(n^2)}
(g₆,g), X₂: X₂ {O(n)}
(g₆,g), X₃: X₃ {O(n)}
(g₆,g), X₄: X₄ {O(n)}
(g₈,j), X₀: X₃ {O(n)}
(g₈,j), X₁: 12⋅X₃⋅X₄+2⋅X₁+3⋅X₃ {O(n^2)}
(g₈,j), X₂: 2⋅X₂ {O(n)}
(g₈,j), X₃: 2⋅X₃ {O(n)}
(g₈,j), X₄: 2⋅X₄ {O(n)}
(g₁₀,k), X₀: X₃ {O(n)}
(g₁₀,k), X₁: 18⋅X₃⋅X₄+3⋅X₁+9/2⋅X₃ {O(n^2)}
(g₁₀,k), X₂: 2⋅X₂ {O(n)}
(g₁₀,k), X₃: 2⋅X₃ {O(n)}
(g₁₀,k), X₄: 2⋅X₄ {O(n)}
(g₁₂,k), X₀: X₃ {O(n)}
(g₁₂,k), X₁: 18⋅X₃⋅X₄+3⋅X₁+9/2⋅X₃ {O(n^2)}
(g₁₂,k), X₂: 2⋅X₂ {O(n)}
(g₁₂,k), X₃: 2⋅X₃ {O(n)}
(g₁₂,k), X₄: 2⋅X₄ {O(n)}
(g₁₄,j), X₀: X₃ {O(n)}
(g₁₄,j), X₁: 18⋅X₃⋅X₄+3⋅X₁+9/2⋅X₃ {O(n^2)}
(g₁₄,j), X₂: 4⋅X₂ {O(n)}
(g₁₄,j), X₃: 4⋅X₃ {O(n)}
(g₁₄,j), X₄: 4⋅X₄ {O(n)}