| Benchmark Name | Num Vars | If-then-else Statements |
Infinite state-space |
Circular Dependency |
Symbolic Constants |
Continuous State-Space |
Defective Variables |
Non-polynomial Updates |
|
|---|---|---|---|---|---|---|---|---|---|
 |
|
|
|
|
|
|
|||
| 2D Robotic Arm | 9 |
|
|
|
|
|
|
|
|
| Bees Model | 5 |
|
|
|
|
|
|
|
|
| Binomial (Parametric) | 1 |
|
|
|
|
|
|
|
|
| Coupon Collector (2 Coupons) | 5 |
|
|
|
|
|
|
|
|
| Coupon Collector (3 Coupons) | 6 |
|
|
|
|
|
|
|
|
| Coupon Collector (4 Coupons) | 7 |
|
|
|
|
|
|
|
|
| DBN Component Health | 3 |
|
|
|
|
|
|
|
|
| DBN Umbrella | 2 |
|
|
|
|
|
|
|
|
| Duelling Cowboys | 4 |
|
|
|
|
|
|
|
|
| Eighths | 3 |
|
|
|
|
|
|
|
|
| Fibonacci Trace | 3 |
|
|
|
|
|
|
|
|
| Fifths | 2 |
|
|
|
|
|
|
|
|
| Five Hundreds | 3 |
|
|
|
|
|
|
|
|
| Gambler Ruin Momentum | 4 |
|
|
|
|
|
|
|
|
| Hawk Dove Symbolic | 5 |
|
|
|
|
|
|
|
|
| Hermann-3 | 7 |
|
|
|
|
|
|
|
|
| Hermann-5 | 10 |
|
|
|
|
|
|
|
|
| Hermann-7 | 16 |
|
|
|
|
|
|
|
|
| Knuth-Yao Algorithm | 8 |
|
|
|
|
|
|
|
|
| Las Vegas Search | 3 |
|
|
|
|
|
|
|
|
| Martingale-Bet | 4 |
|
|
|
|
|
|
|
|
| Nagata | 3 |
|
|
|
|
|
|
|
|
| Nonlinear Markov Model 1 | 3 |
|
|
|
|
|
|
|
|
| Nonlinear Markov Model 2 | 3 |
|
|
|
|
|
|
|
|
| PI Approximation | 4 |
|
|
|
|
|
|
|
|
| Product Dep Var | 4 |
|
|
|
|
|
|
|
|
| Random Walk 1D | 1 |
|
|
|
|
|
|
|
|
| Random Walk 2D | 3 |
|
|
|
|
|
|
|
|
| Randomized Response | 7 |
|
|
|
|
|
|
|
|
| Retransmission Protocol | 4 |
|
|
|
|
|
|
|
|
| Rimless | 9 |
|
|
|
|
|
|
|
|
| Rock Paper Scissors | 7 |
|
|
|
|
|
|
|
|
| Square | 2 |
|
|
|
|
|
|
|
|
| Square and Cube | 3 |
|
|
|
|
|
|
|
|
| Stuttering A | 6 |
|
|
|
|
|
|
|
|
| Stuttering B | 6 |
|
|
|
|
|
|
|
|
| Stuttering C | 6 |
|
|
|
|
|
|
|
|
| Stuttering D | 6 |
|
|
|
|
|
|
|
|
| Stuttering P | 4 |
|
|
|
|
|
|
|
|
| sum_rnd_series | 2 |
|
|
|
|
|
|
|
|
| Taylor Rule | 9 |
|
|
|
|
|
|
|
|
| Turning Vehicle | 6 |
|
|
|
|
|
|
|
|
| Variable Swap | 4 |
|
|
|
|
|
|
|
|