[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Autoincrement



Thank you very much for the quick response Leslie, I really appreciate it!  And thank you a lot for all the work you are doing with TLA+ and the Toolbox!
Yuri

On Tuesday, October 23, 2012 11:45:03 AM UTC-7, Leslie Lamport wrote:
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...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus?hl=en.