Parsing error on action with binary boolean operator

[hvanz]

When an action is defined using the binary disjunction operator (x or y), the parser gives en error. When it is defined using the list operator (any { ... }), it works as expected. It is the same with conjunction.

This is a minimal working example:

module disjunctionBug {
    var x: bool
    action a = x' = x
    action step = a or a // this fails
    // action step = any { a, a } // this is ok
}

which outputs the following error:

Expected [x] and [] to be the same
Trying to unify entities ['x'] and []
Trying to unify Read[v2] & Temporal[v3] and Read['x'] & Update['x']
Trying to unify (Read[v2] & Temporal[v3], Read[v4] & Temporal[v5]) => Read[v2, v4] & Temporal[v3, v5] and (Read['x'] & Update['x'], Read['x'] & Update['x']) => e1
Trying to infer effect for operator application in or(a, a)
quint(QNT000)

[shonfeder]

Thanks for the report! This is indeed a syntax error, but it would help if we had better error messages to explain the problem.

Any/all are not interchangeable with or/and: they have different effects, the latter being pure, and not able to effect state updates.

I’m not sure if there may be an ambiguity in the grammar too tho: while actions are intended to update states, and you can’t update a state inside and/or, an action that only consists of a pure Boolean expression should be valid as long as there is no remaining state needing updates, and in this case it should be legal to use and/or at the top-level of the action. I wonder what @konnov thinks of this.

A separate question is whether and/or should be separate operators from any/all. I was not in favor this at the time, but I think we are pretty well committed to this course ;)

[shonfeder]

We may also need to improve
The documentation around this fairly subtle point. Currently afaik it is only discussed in https://github.com/informalsystems/quint/blob/main/doc/lang.md#block-disjunctions

[hvanz]

Thanks for the explanation @shonfeder! I should had carefully read the documentation first, though I still think it's not very intuitive this distinction. For example, it's possible to use any instead of or in the condition of an if expression. Originally I wanted to write an action in a single line and to avoid the brackets, so I thought the binary operator is more elegant.

[konnov]

This is indeed a syntax error, but it would help if we had better error messages to explain the problem.

Just to make it clear, this is not a syntax error. The error is produced by the effect checker, and this is expected.

[konnov]

I should had carefully read the documentation first, though I still think it's not very intuitive this distinction. For example, it's possible to use any instead of or in the condition of an if expression. Originally I wanted to write an action in a single line and to avoid the brackets, so I thought the binary operator is more elegant.

The effects checker is sometimes imprecise. Maybe @bugarela has a better idea of what is going on in this concrete case.

At the logic level, all is the same thing as and. They are both translated to /\ of TLA+. However, engineers are confused by that, so we have all for actions and and for non-actions.

[bugarela]

In the current implementation, any can always be used to replace or, but not the other way around. We discussed (a while ago) that a linter should suggest that or should be used instead of any when the parameters are not updating the state, since using a more general operator is not an error, just a bad practice (i.e. using let when you can be using const in typescript).

That's why you won't see the tools complaining about using any instead of or (i.e. in if conditions).

[bugarela]

Similar to #643 and related to #502