[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Problem with instance substitutions
Many thanks for such a quick and clear reply. That has helped a lot. The code now works and I have to understand it clearly enough to teach it.
I have another question. not sure if this is the correct thread to ask it on but here goes.
The below (taken from practical TLA+) works
EXTENDS TLC, Sequences
open = FALSE,
locked = FALSE;
\* lock: \* undo the comment to add the label => deadlock
locked := FALSE;
\* unlock: \* undo the comment to add the label => deadlock
locked := TRUE;
\* pingo: \* needed when the above labels added
print("locked = " \o ToString(locked) \o " open = " \o ToString(open));
end algorithm *)
but if you add the commented out labels it deadlocks. I can see why by looking at the generated TLA+. I did not realise that adding labels could have an effect other than just changing atomicity.
1) ) is there any way, other than thinking about the generated TLA+, to describe the behaviour of the labels. (no problem if the only way to understand PlusCal labels is to understand TLA+ labels as I plan to teach both together)
2) are there commands other than ether .. or that labels will change the behaviour (other that the change in atomicity)
again many thanks in advance. david streader