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

Autoincrement



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