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

Re: mixing apples and oranges

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.