Re: [tlaplus] Autoincrement

[TLA Plus <tlapl...@xxxxxxxxx>]

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 Lamport

On 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...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus?hl=en.