Hi Ben!
Thanks for your report Steffen. Nice to see such comparisons even when a bit apples & oranges. Will you be implementing those "additional verification and normalization steps" ? It seems they have an exponential or power impact on times.
I certainly will. Meanwhile, I have some more precise numbers. As it turns out, it is indeed the additional steps (nobuild) that causes the impact. I also added the (nobuild) times from another tool, the probabilistic model checker Storm.
input Prism Storm XP PP size parse nobuild nobuild parse parse 230kB 0.1s 10s 6s 9s 2s 544kB 0.2s 90s 20s 20s 5s 1.1MB 0.4s 392s 46s 34s 8s 1.4MB 0.8s 1091s 85s 47s 12s 2.2MB 63s 16s 2.9MB 81s 20s 3.8MB 107s 25s 4.4MB 123s 30s Best, Steffen
