How do you list possible next steps?

56 views
Skip to first unread message

Andreas Källberg

unread,
Apr 15, 2020, 10:53:34 AM4/15/20
to tlaplus
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

unread,
Apr 15, 2020, 12:21:12 PM4/15/20
to tla...@googlegroups.com
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

unread,
Apr 15, 2020, 1:08:32 PM4/15/20
to tla...@googlegroups.com
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

unread,
Apr 18, 2020, 12:47:09 PM4/18/20
to tla...@googlegroups.com
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

unread,
Apr 19, 2020, 7:04:15 PM4/19/20
to tla...@googlegroups.com
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/
Reply all
Reply to author
Forward
0 new messages