Preprocessing

Eliminate variables [X₀] that do not contribute to the problem

Probabilistic Analysis

Probabilistic Program after Preprocessing

Start: f
Program_Vars:
Temp_Vars:
Locations: f, g, h, i, j, k, l, m
Transitions:
g₀:f(X₀) -{0}> [1/3]:t₁:g(0) :+: [2/3]:t₂:h(X₀) :|:
g₃:g(X₀) -{3}> t₄:i(X₀) :|:
g₅:h(X₀) -{0}> [1/2]:t₆:j(1) :+: [1/2]:t₇:k(1) :|:
g₈:j(X₀) -{5}> t₉:l(X₀) :|:
g₁₀:k(X₀) -{7}> t₁₁:m(X₀) :|:

Run classical analysis on SCC: [f]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:6 {O(1)}
g₀: 2 {O(1)}
g₃: 1 {O(1)}
g₅: 1 {O(1)}
g₈: 1 {O(1)}
g₁₀: 1 {O(1)}

Costbounds

Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₃: inf {Infinity}
g₅: inf {Infinity}
g₈: inf {Infinity}
g₁₀: inf {Infinity}

Sizebounds

Run probabilistic analysis on SCC: [f]

Run classical analysis on SCC: [g]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:6 {O(1)}
g₀: 2 {O(1)}
g₃: 1 {O(1)}
g₅: 1 {O(1)}
g₈: 1 {O(1)}
g₁₀: 1 {O(1)}

Costbounds

Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₃: inf {Infinity}
g₅: inf {Infinity}
g₈: inf {Infinity}
g₁₀: inf {Infinity}

Sizebounds

Run probabilistic analysis on SCC: [g]

Run classical analysis on SCC: [i]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:6 {O(1)}
g₀: 2 {O(1)}
g₃: 1 {O(1)}
g₅: 1 {O(1)}
g₈: 1 {O(1)}
g₁₀: 1 {O(1)}

Costbounds

Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₃: inf {Infinity}
g₅: inf {Infinity}
g₈: inf {Infinity}
g₁₀: inf {Infinity}

Sizebounds

Run probabilistic analysis on SCC: [i]

Run classical analysis on SCC: [h]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:7 {O(1)}
g₀: 2 {O(1)}
g₃: 1 {O(1)}
g₅: 2 {O(1)}
g₈: 1 {O(1)}
g₁₀: 1 {O(1)}

Costbounds

Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₃: inf {Infinity}
g₅: inf {Infinity}
g₈: inf {Infinity}
g₁₀: inf {Infinity}

Sizebounds

Run probabilistic analysis on SCC: [h]

Run classical analysis on SCC: [j]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:7 {O(1)}
g₀: 2 {O(1)}
g₃: 1 {O(1)}
g₅: 2 {O(1)}
g₈: 1 {O(1)}
g₁₀: 1 {O(1)}

Costbounds

Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₃: inf {Infinity}
g₅: inf {Infinity}
g₈: inf {Infinity}
g₁₀: inf {Infinity}

Sizebounds

Run probabilistic analysis on SCC: [j]

Run classical analysis on SCC: [l]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:7 {O(1)}
g₀: 2 {O(1)}
g₃: 1 {O(1)}
g₅: 2 {O(1)}
g₈: 1 {O(1)}
g₁₀: 1 {O(1)}

Costbounds

Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₃: inf {Infinity}
g₅: inf {Infinity}
g₈: inf {Infinity}
g₁₀: inf {Infinity}

Sizebounds

Run probabilistic analysis on SCC: [l]

Run classical analysis on SCC: [k]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:7 {O(1)}
g₀: 2 {O(1)}
g₃: 1 {O(1)}
g₅: 2 {O(1)}
g₈: 1 {O(1)}
g₁₀: 1 {O(1)}

Costbounds

Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₃: inf {Infinity}
g₅: inf {Infinity}
g₈: inf {Infinity}
g₁₀: inf {Infinity}

Sizebounds

Run probabilistic analysis on SCC: [k]

Run classical analysis on SCC: [m]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:7 {O(1)}
g₀: 2 {O(1)}
g₃: 1 {O(1)}
g₅: 2 {O(1)}
g₈: 1 {O(1)}
g₁₀: 1 {O(1)}

Costbounds

Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₃: inf {Infinity}
g₅: inf {Infinity}
g₈: inf {Infinity}
g₁₀: inf {Infinity}

Sizebounds

Run probabilistic analysis on SCC: [m]

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:7 {O(1)}
g₀: 2 {O(1)}
g₃: 1 {O(1)}
g₅: 2 {O(1)}
g₈: 1 {O(1)}
g₁₀: 1 {O(1)}

Costbounds

Overall costbound: 15 {O(1)}
g₀: 0 {O(1)}
g₃: 3 {O(1)}
g₅: 0 {O(1)}
g₈: 5 {O(1)}
g₁₀: 7 {O(1)}

Sizebounds