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
Transitions:
g₁:f(X₀) → t₂:g(X₀+UNIFORM(1, 15)) :|: 0 ≤ 1
g₃:g(X₀) → t₄:h((X₀)²) :|:

Run classical analysis on SCC: [f]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:2 {O(1)}
g₁: 1 {O(1)}
g₃: 1 {O(1)}

Costbounds

Overall costbound: 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:2 {O(1)}
g₁: 1 {O(1)}
g₃: 1 {O(1)}

Costbounds

Overall costbound: inf {Infinity}
g₁: inf {Infinity}
g₃: inf {Infinity}

Sizebounds

Run probabilistic analysis on SCC: [g]

Run classical analysis on SCC: [h]

Classical Approximation after Lifting Classical Results

All Bounds
Timebounds

Overall timebound:2 {O(1)}
g₁: 1 {O(1)}
g₃: 1 {O(1)}

Costbounds

Overall costbound: inf {Infinity}
g₁: inf {Infinity}
g₃: inf {Infinity}

Sizebounds

Run probabilistic analysis on SCC: [h]

Results of Probabilistic Analysis

All Bounds

Timebounds

Overall timebound:2 {O(1)}
g₁: 1 {O(1)}
g₃: 1 {O(1)}

Costbounds

Overall costbound: 2 {O(1)}
g₁: 1 {O(1)}
g₃: 1 {O(1)}

Sizebounds