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

Re: [tlaplus] Re: mixing apples and oranges

Thank you, that also works well (and is a direct fix for my original attempt, where I tried to use a string for NoValue). As you say, it is simpler for this example. And I see now in the toolbox docs that TLC has specific support for this idiom.

On Sat, Sep 15, 2018 at 12:55 AM, Ron Pressler <ron.pr...@xxxxxxxxx> wrote:
While Leslie's suggestion is a great way to mix apples and oranges in general, your motivating example was of a special case, where a specific "null" value is required (if you know a language like Haskell, you can compare these two scenarios to an Either type vs a Maybe type, where the latter is asymmetric in the sense that you can have any number of apples but only one orange). In that case, a simpler approach may be to define:

BPvalue == (MIN_BP..MAX_BP) 
NoValue == CHOOSE x : x \notin BPvalue
BPmeasurement == {NoValue} \cup BPvalue

From a theoretical point of view, it is then possible to know that NoValue is not equal to any BPvalue. In practice, when using TLC, you then override NoValue with a "model value" which is comparable with any value and equal to nothing but itself.

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@googlegroups.com.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.