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?
Thank you in advance,
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
To unsubscribe from this group, send email to tlaplus+u...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus?hl=en.