Closed rmascarenhas closed 5 years ago
In other words, the same label name could be reused across processes/procedures (and the PlusCal to TLA+ translator is responsible for making sure labels are unique).
Make sure the atomicity inference pass works well with that fact. /cc @mrordinaire
The current code still works well because each label has a unique UID.
In other words, the same label name could be reused across processes/procedures (and the PlusCal to TLA+ translator is responsible for making sure labels are unique).
Make sure the atomicity inference pass works well with that fact. /cc @mrordinaire