I wanted to ask for an advice on how to model values that should auto-increment when the next value is used, similar to auto-increment of database IDs when a new record is inserted.
My current thinking is:
VARIABLES Id, ...
Init == Id = 0 /\ ...
NextId(x) == x' = x + 1
SomeAction == NextId(Id) /\ use_id_here
Is this too complicated? May be there is a simpler way to model this?