CHOOSE behavior: evaluates to FALSE if no element of a set can be chosen

[craft095]

Description

Not sure if it is a bug or a feature request. Anyway, consider: CHOOSE t \in {FALSE} : FALSE Is it possible to report an error in such a case (like TLC does)? Right now it just evaluates to FALSE.

Input specification

---- MODULE M0 ----
VARIABLE
    \* @type: Bool;
    x

Init == x = TRUE
Next == x' = x
Spec == Init /\ [][Next]_x

Inv == ~(CHOOSE t \in {} : FALSE)
====

The command line parameters used to run the tool

java -jar apalache-pkg-0.20.2-full.jar check --inv=Inv M0.tla

Expected behavior

Apalache throws an error

System information

• Apalache version [apalache-mc version]: 0.20.2
• OS [e.g. Ubuntu Linux or Mac OS, and the current version]: Ubuntu Linux
• JDK version [e.g. OpenJDK 0.8.0]: openjdk "14.0.2"

[konnov]

This is related to #95. Unfortunately, we still have not found any good automatic solution to this problem. Many languages work around this problem by using the option type, which forces the user to manually resolve the out-of-bounds case. It is relatively easy to emulate this behavior in TLA+ by hand: Introduce a failure flag in the state and set it to true, whenever one of the partial operators is applied outside of the domain. It is hard to automatically preprocess a specification this way, as it would require us to place UNCHANGED on the branches that do not lead to a failure.

[Kukovec]

I'd just like to elaborate on @konnov 's answer above. This behavior of CHOOSE is consistent with the TLA+ semantics. The book, (p295) states that: "[CHOOSE x \in S: p] is equal to some arbitrary value v in S such that p, with v substituted for x , is true - if such a v exists. If no such v exists, the choose expression has a completely arbitrary value."

Ultimately, this approach lends itself well to Apalache's symbolic encoding, as the case where p = FALSE results in v being totally unconstrained. What you're asking for - throwing exceptions - goes against this approach, because there's no such thing as partial evaluation of a formula. In order to throw an exception, one needs to know a state in which p evaluates to FALSE (in the general case, where p is not constant), which is a) reachable and b) distinguishable by at least one invariant (that is, depending on the value selected by CHOOSE, that invariant may be made either TRUE or FALSE). Therefore, detecting whether a p = FALSE (or, similarly, whether a function is accessed outside of its domain) is essentially equivalent to the entire model-checking process. Trying to add these checks for every CHOOSE or function access anywhere in the specification would require so many constraints, the solver would end up spending more time on bookkeeping, than actually solving the formulas.

Ultimately, if you have a specification where CHOOSE is used with a predicate that can be FALSE, it likely has to be rewritten either way. One can either ensure that the expression is guarded appropriately, add invariants, asserting that the CHOOSE predicates have witnesses, or implement auxiliary TLA flag-variables, that toggle whenever a CHOOSE predicate is FALSE.

Someone has to decide what happens in an ELSE branch of:

\* safe CHOOSE
IF \E x \in S: p
THEN 
  LET v == CHOOSE x \in S: p
  IN ...
ELSE ???

and we leave it up to the specification authors to describe the system behavior in those cases.

For reference, some standard ways to handle this would be:

\* guard
Action == 
  /\ \E x \in S: p
  /\ LET v == CHOOSE x \in S: p IN ...

or

\* invariant
Action == LET v == CHOOSE x \in S: p IN ...

Inv == ActionCanHappen => \E x \in S: p 

or

\* flag
VARIABLE
  \* @type: Bool;
  flag

Action == 
  /\ LET v == CHOOSE x \in S: p IN ...
  /\ flag' = (\E x \in S: p)

More than anything, this entire issue is a cautionary tale about using CHOOSE, and there's some DOs and DON'Ts discussed here.

[craft095]

@konnov @Kukovec Thanks for your explanation! I believed that such a behavior (when exception is thrown) would be helpful in capturing specification errors (which may happen). It is so difficult to do, then perhaps it is not worth efforts (given the workarounds you described)

[konnov]

Thanks! We also find this issue important and we keep thinking about it. However, this behavior of TLC is a side effect. It's hard to deal with side effects in symbolic encodings. I believe TLAPS has the same issue.

[konnov]

There is another issue that makes it hard to report out-of-bounds access. I just tried to introduce unconditional error reporting for seemingly wrong expressions such as seq123[4] applied to a sequence seq123 = <<1, 2, 3>>. Unfortunately, it breaks perfectly correct TLA+ specs. For instance:

VARIABLES
  \* @type: Seq(Int);
  seq,
  \* @type: Bool;
  ok

IsOk(seq) ==
  4 \notin DOMAIN seq \/ seq[4] > 0

Init ==
  /\ seq = <<>>
  /\ ok = IsOk(seq)

Next ==
  \E x \in Int:
    /\ seq' = Append(seq, x)
    /\ ok' = isOk(seq')

TLC evaluates expressions over concrete states and it does implement lazy semantics for \/ and /\. As a result, it does not complain about seq[4] > 0.

Apalache encodes eager semantics for all formulas (modulo optimizations for constant values). It should be possible to implement this kind of semantics, e.g., by preprocessing a specification. However, this error propagation would taint virtually every expression of the specification.

Would it help you, if Apalache had a special mode for checking for out of bounds errors? For instance, we could report on the location of the problematic expression, but it would be harder to report the concrete values that caused the error.