Re: mixing apples and oranges

If you want to work with the union of the sets Apples and Oranges of
incomparable elements, my favorite approach is to define

Fruit == [type : {"apple"}, value : Apples] \cup [type : {"orange"}, value : Oranges]

To define an operator Op that takes a fruit as an argument and whose
value doesn't depend on the type of fruit, you can just write:

Op(F) == some _expression_ mentioning only F.value.

If the value of Op(F) depends on the type of fruit F, then you can
define it by:

Op(F) == CASE F.type = "apple" -> ...
[] F.type = "orange" -> ...

Leslie

On Friday, September 14, 2018 at 6:41:32 AM UTC-7, Sebastian Hunt wrote:

I'm developing a spec which involves measurements which may fail or, if they succeed, take a numeric value. My first attempt was:

BPvalue == (MIN_BP..MAX_BP)
BPmeasurement == {"failed"} \cup BPvalue

But TLC didn't like this and complained about being unable to compare strings with non-strings.

I've currently arrived at this approach:

BPmeasurement == {<<"failed">>} \cup {"measured"} \X BPvalue

This works, but is there a better way?

Part of the system state is a variable bpTarget taking values in [min: BPvalue, max: BPvalue]. I define an inRange operator for checking if a measurement is in range. My first attempt was:

inRange(m, r) == \E v : m = <<"measured",v>> /\ r.min <= v /\ v <= r.max

Using this in the spec results in an error when running TLC. There is an error trace but the box above the trace which would usually contain a description of the error (eg violated invariant) is empty, so a bit mysterious. Is this empty box a bug?

My guess is that the error is caused by the unbounded \E v, hence my second attempt:

inRange(S, m, r) == \E v \in S : m = <<"measured",v>> /\ r.min <= v /\ v <= r.max

then I pass BPvalue as the first parameter (I could hardwire BPvalue into the definition but I was trying for something generic).

This works but, again, is there a better way?

Seb