Consider supporting dynamic run steps

[bugarela]

In the run mode, we make some restrictions such as reps requiring a pure argument for number of repetitions, while we could be more permissive since these are just tests that aren't translated to Apalache at all. We should consider the pros and cons of support this.

[p-offtermatt]

Thank you for looking into this! For me as a user, I am happy to use the "scheduler" solution Igor suggested. However, I do think that solution is more work in simple cases like just iterating over a list with reps, and it might be nice to have this. However, I think it mostly depends on how much implementation work it is, and I personally wouldn't prioritize this highly on my feature wishlist.

since these are just tests that aren't translated to Apalache at all.

This worries me a bit - which operators are not translated to Apalache? I didn't see any indication of this in the language docs. I am indeed using .then in the actions of a spec, and this makes me unsure whether it's meant to be usable there

[bugarela]

This worries me a bit - which operators are not translated to Apalache? I didn't see any indication of this in the language docs. I am indeed using .then in the actions of a spec, and this makes me unsure whether it's meant to be usable there

The operators in run mode are not meant to be translated to apalache, as there are no such a thing as a run in TLA+. You can check them here: https://github.com/informalsystems/quint/blob/main/doc/lang.md#runs.

Sorry that this is not clear. We also want the effect checker to prevent usages of the run-level operator inside actions, but this was never prioritized.

For then specifically, it is equivalent to TLA's \cdot, which I personally think is useful. However, neither the Apalache devs (my team) and the TLC devs agree, so \cdot is unsupported in both model checkers. IIRC, @konnov said he doesn't see anything preventing the implementation of that, so perhaps one day we'll have it. For now, I recommend rewriting those actions without then or any other run operators, specially if you plan on using Apalache.

[konnov]

We could translate run to TLA+ by simply introducing a designated action for every step. However, that would require us introducing an additional state variable. For instance:

run test =
  init
   .then(A)
   .then(B)

would become:

VARIABLE stepNo

testInit ==
  stepNo = 0 /\ init

testNext ==
  CASE step = 0 -> A /\ stepNo' = 1
    [] step = 1 -> B /\ stepNo' = 2

This is not implemented, even though we could have implemented something like this. In particular, it is not clear, what the users would get from it by running Apalache.

As for \cdot, it is the only operator that allowed one to collapse two steps into one. I think I know the reason for not ever implementing it. If it was implemented, people would immediately start to translate their imperative code into TLA+ without thinking.

[josef-widder]

I was hitting the limitations of reps requiring a pure argument when I was trying to define a "domain-specific language" for consensus runs, where I use parameterized runs to define individual rounds, and then combine these runs with .then.

Since I would like to combine rounds (and parts of rounds), it would make sense to have some flexibility on the boundaries between sub runs, e.g., perhaps I don't want to think too much about what messages a process has in its inbuffer after a run before applying the next run r. So it might be convenient in run r to just deliver all of the messages in the in-buffer (where delivery is one step per message). So using the size of the inbuffer in reps seemed appealing at first sight.

I think for now I will get around the limitations. As I have the set of validators as const and consequently as values, I can do a lot of parameterization (defining runs of different lengths) even with pure arguments. For more dynamic systems, one might really hit a limit eventually. But one can still generate a lot of useful traces with the current limitations.

So I guess that this is not a high priority, but as soon as people starting to understand how powerful runs are to generate traces, eventually more people might want that feature.

[josef-widder]

I think I have changed my opinion on this subject a bit. What happened is that in a project, I changed the protocol logic a bit, which effectively resulted in tests failing because I required every process at some points to do an additional step. As a result I needed to update all the concerned runs and tests, that is, figuring out where the tests hit a deadlock first, add additional steps there, and see whether there is another deadlock later, and repeat (I will write a separate issue on better user experience for writing tests, soon).

But what I would have prefered doing is having a way to tell quint to let everyone take steps (just calling the same action) until a certain condition is met (e.g., all the in-buffers are empty, and everyone has a specific value in its variable).

I think the ability to do that, will allow us to write tests (perhaps they are not really tests anymore but objects that we can use as we use tests in CI today) that require less maintenance if small changes in the protocol happen. In particular, in distributed systems, adding steps that result in stuttering doesn't seem to be uncommon, and not having to rewrite tests all the time seems to have big potential for saving time.

Effectively, what I am asking for is the feature to define a scheduler, that is, some way to decide on the next step, depending on the current state. Now, a fully-fledged scheduler syntactically might look totally different from a run: For instance, I might want to write a run that goes through 3 rounds of consensus. In a standard run, it is clear that syntactically, the steps of round 1 are at the top of the run, and the steps of round 3 they are at the bottom. I think this structure is super useful when using runs for onboarding and documentation. However, if a scheduler is a function of a state to the next step taken, this structure might go away, as we write functions differently from how we write runs and it might be less suitable for documentation purposes.

So I guess we should think about an extension of runs, perhaps call them "scenarios", that are more or less runs, but have some concepts that allow some sort scheduling, while maintaining the overall structure. The initial point of the discussion in this issue (having the argument of reps depending on the state; instead of being it pure) might be just one example. Perhaps we could also have a construct "repeat until" whose exit condition depends on the state.

I think that such "scenarios" would be a great extensions to runs, that could reduce the maintenance cost of executable specs in the long run. So it would be great to prioritize at least some initial steps into this direction.