Problem description
In my experience it can be hard to get the most from Apalache for model-based testing because for large specs the number of steps it can check can be quite limited. In my experience a very large non trivial model can be limited to as few as 2/3 steps when checking invariants, and medium/large models are often limited to 5-7 steps. 8+ steps only be achieved in some cases or with very small/trivial models.
Apalache has many advantages for MBT such as being able to handle unbounded Integers, and being able to use View and Trace invariants to check and generate traces for very interesting behaviors. These features far surpass what TLC offers. Therefore it is unfortunate to be limited in the steps (where TLC is usually not as limited).
As an example please consider these versions of a spec written for MBT of the staking module: Apalache and TLC. The spec is large, and I wrote it over a period time. Early on, when the spec was smaller, I experimented and was achieving better results with TLC so after that I wrote a lot of the spec with TLC in mind. But still, in the Apalache version I tried to the extent possible to avoid anti patterns (there are no recursive operators, @@ chains, or CHOOSE, and I use Nat instead of small sets of Ints). There are admittedly a lot of uses of Fold due to computing sums over sets, but I'm not sure what I could do to remove those.
The TLC version of the model can be checked up to 10+ steps quite easily whereas Apalache cannot really get past 3 steps (or 2 if checking an invariant). This rules out using Apalache as testing any meaningful behavior will require several actions.
Of course, the small scope hypothesis is a thing, and there are many many instances where 5-7 steps is sufficient to test meaningful behavior, but still, being able to consistently get there, or check 8+ steps more often would be great.
I would like to add, the example I gave is concrete and fresh in memory but I have noticed this as a trend when using Apalache. I think @andrey-kuprianov has had similar experiences.
The solution I'd like
N/A
Alternatives I've considered
N/A
Additional context
I spoke @gabrielamafra about the phenomena of the step limitation being a bigger problem than the state explosion and I'm happy that Apalache is discussing this.
Problem description
In my experience it can be hard to get the most from Apalache for model-based testing because for large specs the number of steps it can check can be quite limited. In my experience a very large non trivial model can be limited to as few as 2/3 steps when checking invariants, and medium/large models are often limited to 5-7 steps. 8+ steps only be achieved in some cases or with very small/trivial models.
Apalache has many advantages for MBT such as being able to handle unbounded Integers, and being able to use View and Trace invariants to check and generate traces for very interesting behaviors. These features far surpass what TLC offers. Therefore it is unfortunate to be limited in the steps (where TLC is usually not as limited).
As an example please consider these versions of a spec written for MBT of the staking module: Apalache and TLC. The spec is large, and I wrote it over a period time. Early on, when the spec was smaller, I experimented and was achieving better results with TLC so after that I wrote a lot of the spec with TLC in mind. But still, in the Apalache version I tried to the extent possible to avoid anti patterns (there are no recursive operators, @@ chains, or CHOOSE, and I use Nat instead of small sets of Ints). There are admittedly a lot of uses of
Folddue to computing sums over sets, but I'm not sure what I could do to remove those.The TLC version of the model can be checked up to 10+ steps quite easily whereas Apalache cannot really get past 3 steps (or 2 if checking an invariant). This rules out using Apalache as testing any meaningful behavior will require several actions.
Of course, the small scope hypothesis is a thing, and there are many many instances where 5-7 steps is sufficient to test meaningful behavior, but still, being able to consistently get there, or check 8+ steps more often would be great.
I would like to add, the example I gave is concrete and fresh in memory but I have noticed this as a trend when using Apalache. I think @andrey-kuprianov has had similar experiences.
The solution I'd like
N/A
Alternatives I've considered
N/A
Additional context
I spoke @gabrielamafra about the phenomena of the step limitation being a bigger problem than the state explosion and I'm happy that Apalache is discussing this.