Operation view show non-deterministically assigned variables
Description
Environment
Attachments
- 06 Nov 2018, 02:39 PM
- 13 Oct 2017, 10:02 AM
- 13 Oct 2017, 10:02 AM
Gliffy Diagrams
Activity
dgelessus November 21, 2019 at 12:46 PM
Can't reproduce this with the current version of the UI - the non-deterministic variables are displayed correctly for the test machine from the comment above.
Michael Leuschel November 6, 2018 at 2:39 PM
I have just tried the above example (NonDetChoicesOpViewTest.mch) and I do not see the values of the non-deterministically assigned variables in the operations view?
dgelessus June 12, 2018 at 1:13 PM
Now implemented in kernel (c4b89fd) and UI (3b0bad2).
Michael Leuschel June 12, 2018 at 11:04 AM
What is the status of this issue?
Here is another example one can use to test the UI:
MACHINE NonDetChoicesOpViewTest
// check that non-deterministic assignments are shown in the operations/event view
SETS
ID={aa,bb,cc}
CONSTANTS iv
PROPERTIES
iv:ID
VARIABLES xx,yy
INVARIANT
xx:ID & yy:ID
INITIALISATION xx :: ID || yy :: (ID \ {iv})
OPERATIONS
ChooseByChoice = CHOICE xx := aa OR xx:= bb END;
ChooseNonDet1 = BEGIN xx :: ID{xx} END;
ChooseNonDet2 = BEGIN xx :: ID{xx} || yy :: (ID{iv}) END;
ChooseNonDet3 = BEGIN xx,yy : (xx /= yy) END;
ChooseNonDet4 = SELECT xx /= yy THEN xx := yy ELSE yy := aa END;
ChooseNonDet5 = ANY v WHERE v:ID \ {xx} THEN xx := v END
END
dgelessus October 18, 2017 at 7:46 AM
This is an issue in the kernel, not the UI. The Login transitions have an empty params list:
> animations.currentTrace.getNextTransitions(true)[0]
Login
> animations.currentTrace.getNextTransitions(true)[0].params
[]Details
Details
Assignee
Reporter
Priority
Major
It would be nice to improve the pretty printing of operations in the Operations View.
In Tcl/Tk ProB uses the Prolog predicate:
translate_event_with_target_id
where the Operation is pretty printed with knowledge of the target state id.
This allows to show non-deterministically assigned variables, see attached screenshots for a model in prob_examples/public_examples/TLA/Login/.