`quint test` doesn't support `--mbt`

[bugarela]

Originally reported by @erickpintor (migrated from Notion)

Currently, mbt::actionTaken and mbt::nondetPicks are only available for quint run. Users attempting to do MBT with Quint Connect are forced to manually track nondeterminism in their test cases. Ideally, Quint would track calls to then(..) and attempt to determine which action is being called. For example:

run myTest =
  init
    .then(action1)
    .then(action2)

The run above should generate a trace with 3 steps where the mbt::actionTaken variable matches the 3 actions invoked by the test. Moreover, it’s not unusual for actions called in test cases to be parameterized:

run myTest =
  init
    .then(action1("foo"))
    .then(action2("bar"))

In those cases, it’d be useful for the action arguments to end up in the set of nondeterministic picks so that MBT can leverage them. Ideally, this feature should also be implemented for quint run.

[fkberthold]

It would be profoundly useful to have this available using quint test. In my own use case there are model states that are useful for the model, but not reasonably testable. Having a separate model just for test is begging for the two to get out of sync.