How do you list possible next steps?

[Andreas Källberg]

I have a model with an `Init` and `Next` formula.
While going through an error trace, I would like to see a list of all possible next steps it could transition to.

I assume that I could add some expression based on `Next`, that will provide a set of all solutions for `var'`,

but I have no idea of how to express that?

Thanks,
Andreas

[Stephan Merz]

You could evaluate predicates ENABLED A for all actions A when analyzing the error trace in order to understand which actions are enabled at each of the states. This won't show actual successor states, though.

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1efaa45d-f714-4e4d-8fb6-a7ca95d5badb%40googlegroups.com.

[Markus Kuppe]

Hi Andreas,

I shared a trick how to interactively explore a state space at
http://tla.msr-inria.inria.fr/kuppe/ExploreInteractively.gif

I can write a howto if this is what you are looking for.

Markus

[Andreas Källberg]

Den ons 15 apr. 2020 kl 19:08 skrev Markus Kuppe <tlaplus-go...@lemmster.de>:

I shared a trick how to interactively explore a state space at
http://tla.msr-inria.inria.fr/kuppe/ExploreInteractively.gif

I can write a howto if this is what you are looking for.

 Yes, that would be very nice!

[Markus Kuppe]

On 18.04.20 09:46, Andreas Källberg wrote:
> Den ons 15 apr. 2020 kl 19:08 skrev Markus Kuppe
>

> I shared a trick how to interactively explore a state space at
> http://tla.msr-inria.inria.fr/kuppe/ExploreInteractively.gif
>
> I can write a howto if this is what you are looking for.
>
>
>  Yes, that would be very nice!

Hi Andreas,

I recorded a screencast [1] that shows how to print all possible
next-states at each step of an error trace. The trick does not work
with the Toolbox but uses a recent nightly release of TLC [2]. I
summarized the high-level steps in a comment under the screencast.

Hope this helps,
Markus

[1] https://asciinema.org/a/321778
[2] http://nightly.tlapl.us/