STORM vs PRISM Probability Difference
The following table quantifies the difference (albeit small one) between Storm and Prism on some small tests.
| Model | STORM | PRISM | Difference |
|---|---|---|---|
| Toy 1 (Combined) | 0.8521736966 | 0.852173648263556 | 4.83364440695411E-08 |
| Toy 1 (Separate) | 0.8521736966 | 0.852173648263556 | 4.83364440695411E-08 |
| Toy 2 (Combined) 2 | 0.8521736966 | 0.852173648263556 | 4.83364440695411E-08 |
| Toy 2 (Combined) 3 | 0.02001270818 | 0.020012706722445 | 1.45755505234768E-09 |
| Toy 2 (Combined) 4 | 0.6263694968 | 0.626369457942353 | 3.88576472110103E-08 |
| Toy 2 (Combined) 1 | 0.6953953213 | 0.69539527920791 | 4.20920902577393E-08 |
| Toy 2 (Separate) | 0.6953953213 | 0.69539527920791 | 4.20920902577393E-08 |
| Jackson 5 N 4 | None (OOM Error) | None (OOM Error) | |
| Jackson 5 N 5 | None (OOM Error) | None (OOM Error) | |
| Tandem c2047 | 0.4989665901 | 0.498966574855377 | 1.52446226753256E-08 |
| Tandem c4095 | 0.4992677454 | 0.499267709080004 | 3.63199963993033E-08 |
The Jackson models did not finish for either model checker, and ended with OOM errors.