will62794
action labels and traces do not include action parameters
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.
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.
