search

informalsystems / quint

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
Apache License 2.0
817 stars 31 forks source link

Misleading docs: --mbt flag missing #1526

Closed vitorguidi closed 3 weeks ago

vitorguidi commented 3 weeks ago

I am following the bank example and docs instruct me to run:

quint run bank.qnt --invariant=no_negatives --mbt

However this is not recognized:

image

I managed to see what transitions led to the failed states by doing, instead:

quint run bank.qnt --invariant=no_negatives --verbosity=3
image

Is mbt deprecated? If so, maybe change it like this?

bugarela commented 3 weeks ago

Hi Vitor! Any chance you have an old version of Quint installed? You can check it with quint --version. Newest version is 0.22.1

vitorguidi commented 3 weeks ago

Oh, my bad. I am running 0.18.3, this is what got shipped with homebrew. Closing!