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