A ternary type for actions?

[konnov]

This is a very rough idea that needs some thinking. We have always had problems with Assert in Apalache, because it is kind of Boolean, but it also should report an error somehow, which is very hard to do in symbolic execution.

Started as a comment: #552 (comment)

We could let actions to have three kinds of results: Executed, NotExecuted, and Fail. Executed is exactly like true in the current system, and NotExecuted and Fail represent false together. NotExecuted would mean that the action is disabled in a state, while Fail would mean that the action was not disabled, but it is not well-defined in a state. The most immediate example of this would be assert.

Moreover, as we have seen, it would help us to explain actions to people, as our first users are surprised to see Boolean results.

If we want to try this approach, we would have to understand how ternary results combine via any and all. I did a quick search. There are paper on three-valued logics, e.g., this paper. That probably needs further search.

/cc @shonfeder, @bugarela, @Kukovec, @thpani

[p-offtermatt]

This is interesting to me - I did get a vague feeling of this three-valued logic being appropriate when writing my actions.
Could Fail be used to have a more native way to distinguish between system errors and successful action executions?

Right now, the suggested pattern seems to be to have a Result record, which is essentially an option, either a newState or an error. This is usually fine when we want to execute actions only when there is no error. However, I think this pattern becomes confusing when one wants to actually let the system execute error-ing actions to e.g. check that a system under test returns the same errors that the model does. Then, I think we get exactly this ternary logic: either the action is disabled, or it is enabled and returns a new state, or it is enabled and returns an error.

From reading the initial post, I think Fail is meant to be something slightly different, more to guard against bugs in the model that would be caught by carefully placed asserts, but it reminded me of these "expected errors". I wonder if these are completely orthogonal or related.