Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

action labels and traces do not include action parameters #56

Open
jskri opened this issue Jan 6, 2025 · 1 comment
Open

action labels and traces do not include action parameters #56

jskri opened this issue Jan 6, 2025 · 1 comment

Comments

@jskri
Copy link

jskri commented Jan 6, 2025

Consider the following spec:

---------------------- MODULE Test -------------------------
EXTENDS Naturals
VARIABLES count
Init == count = 0
Incr(N) == count' = count + N
Next == Incr(1) \/ Incr(2)
Spec == Init /\ [][Next]_count
============================================================

Then the action tab features two buttons with the same label "Incr", making them difficult to distinguish.
I would expect the labels to be respectively "Incr(1)" and "Incr(2)".
This also affects the trace tab.

@will62794
Copy link
Owner

will62794 commented Jan 7, 2025

Eventually the interface should handle this case better, but I just pushed a small change that may help you work around the confusion in the current tool.

The change allows you to optionally view the full set of next state choices directly (i.e. showing the set of changed variables for each), which hopefully helps to disambiguate between actions that aren't parsed as distinct, as you noted in the case above.

You can find the example spec from above running here, where you should be able to see the new "Show full next states" toggle button to enable this feature.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants