/\ pc(p) = a
/\ x’ = t(p) + 1
/\ t’ = (t EXCEPT p |-> x )
/\ pc’ = (pc EXCEPT p |-> done)
This to me seems wrong since t is only changed when that process is about to be set to done and hence is never accessed. So as far as i can see this will only ever set x' to one of the initial values of t (+1) - so will always end at one since t is initialized to zero for all processes.
I am fairly new to TLA and a little terrified to question this so i apologize in advance if i am wasting peoples time - but all my efforts to make sense of this have failed.
In some ways this is a bit of a weird example since the temporary variable was introduced to illustrate issues of concurrency - and when you compose the steps it becomes irrelevant- naturally.
Thanks for any help!
Dave Hughes