Sorry, I edited a bunch and the point was that the ordering can matter due to references to the new value on the rhs or due to a loop. So
a' = a + b + 1 and b' = a + b + 1
should be
a' = a + b' + 1 and b' = a' + b + 1
Or alternatively they can have non-primed right hand sides but occur in a loop and you have the same problem even though the rhs's are at-free. A syntactic constraint won't work unless it includes "and also no loops in at-mentioning blocks" which... well, yeah, we know how to reason about NFAs :)
Sorry again, trying to make too many points with a single example
Could you not tackle this problem by not allowing this mingling of 'next' and 'current' variables? You would only allow a next variable to be a computation of current variables. Not sure to what extent this would limit the application of the paradigm, though.
You can allow mingling as long as you don't produce an evaluation loop. The existence of evaluation loops can be detected by the compiler (Metron does this already).
Author here, you are both correct and not correct - in your example the two equations represent an impossible constraint (there's an evaluation loop), thus a program (or TLA proof) containing those two statements would be invalid.
a' = a + b + 1 and b' = a + b + 1
should be
a' = a + b' + 1 and b' = a' + b + 1
Or alternatively they can have non-primed right hand sides but occur in a loop and you have the same problem even though the rhs's are at-free. A syntactic constraint won't work unless it includes "and also no loops in at-mentioning blocks" which... well, yeah, we know how to reason about NFAs :)
Sorry again, trying to make too many points with a single example