Re: Problem with instance substitutions

[davidis...@xxxxxxxxx]

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
(*--algorithm door
variables
   open = FALSE,
   locked = FALSE;   
   begin
     Event:
      either
     \* lock: \* undo the comment to add the label => deadlock
       await locked;
       locked := FALSE;
      or 
    \*  unlock: \* undo the comment to add the label => deadlock
        await ~locked;
        locked := TRUE;   
      end either;
   \*   pingo:  \* needed when the above labels added
      print("locked = " \o ToString(locked) \o " open = " \o ToString(open));
      goto Event;   
 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