mixing apples and oranges

[Sebastian Hunt]

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

[Leslie Lamport]

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

[Sebastian Hunt]

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

[Ron Pressler]

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.

[Seb Hunt]

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.

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