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

[tlaplus] Re: Variables with values unspecified but distinct from each other

If your spec contains a definition of the form

  x == CHOOSE b : b \notin S

then when you create a model for it, the Toolbox will add to the model the appropriate
incantation to substitute for x a model value named "x".  You could therefore write

   x == CHOOSE a : a \notin {}
   y == CHOOSE a : a \notin {x}
   z == CHOOSE a : a \notin {x,y}

and you won't have to do any instantiation of constants.


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c14403e0-1e14-4a45-8d3a-b8815c478781o%40googlegroups.com.