by ahelwer on 9/18/24, 4:57 PM with 2 comments
by bugarela on 9/18/24, 7:47 PM
Quint also has the concept of a run, where users can guide the "searcher" to a specific set of executions, so it works really well as a BF/DF* searcher, which is it's focus (it doesn't support refinement or proofs, at least for now).
So yeah, if you are curious for a language that supersedes TLA+, you should definitely give Quint a try :)
* BF through model checking, DF through bounded random simulation