Your spec seems fine, assuming that there are several counters and not just the single one Id. If Id were the only one, there's no need for NextId to have a parameter; you could define it simply to equal Id' = Id + 1.I would probably eliminate the definition of NextId and simply write Id' = Id + 1 in the definition of NextAction, but that's just a matter of taste.Leslie LamportOn Tue, Oct 23, 2012 at 10:36 AM, Y2i <yur...@xxxxxxxxx> wrote:
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,
Yuri
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...@googlegroups.com .
Visit this group at http://groups.google.com/group/tlaplus?hl=en .