TLC won't let me use:
\A <<x,y>> \in AllRouters, s \in Sides :
LET q == grid[x, y][s].in
IN \/ q = <<>>
\/ Head(q).header # <<x,y>>
However, this ugly alternative works:
...
IN IF q = <<>> THEN TRUE ELSE Head(q).header # <<x,y>>
Could TLC's evaluation of disjunctions be improved to avoid the problem? Or is there a non-ugly alternative that I'm missing?
(Note: I'm using the command-line tools, TLC2 Version 2.03 of 20 July 2011.)
MC