Verification: Improve performance of model checking

crestdsl / CREST

Continuous REactive SysTems DSL

https://crestdsl.github.io

MIT License

18 stars 2 forks source link

Verification: Improve performance of model checking #12

Open stklik opened 5 years ago

stklik commented 5 years ago

The continuous model checking creates lots of formulas that are repeatedly calculated. A cache can reduce the number of explorations through the statespace.

Also: call simplify from within the model checker, not just before.