|If you intend your specification to be used with TLC, you have to use bounded choice (CHOOSE x \in S : ...), contrary to your goal of not specifying the kinds of these values.|
My suggestion would be to declare constant parameters and assume they are distinct, like so:
ASSUME x # y /\ x # z /\ y # z
For a TLC model, you can instantiate these constants by model values, which are always distinct.
On 26 Jul 2020, at 21:39, mmynsted <code@xxxxxxxxxxxxxxxxxx> wrote:
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/9540F26C-5956-4912-8DD1-C62EA719B7AC%40gmail.com.