Re: mixing apples and oranges

Thank you, that works very well, I doubt it would have occurred to me.

It's not yet second nature to me that it's necessary in this context to write (for example)

IF F.type = "apple" THEN F.value = a ELSE FALSE

rather than

F.type = "apple" /\ F.value = a

But I do see why.

Seb

On Friday, 14 September 2018 14:41:32 UTC+1, 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