Enabled outside temporal mode with effects

[bugarela]

Hello

In our current language specification, we state that the enabled operator is only available in temporal mode. I believe we should allow it (or a renamed version of it such as condition) in state mode as well. Here's why and how.

Why

Looking at the tic-tac-toe spec from this tutorial:

MoveX ==
    /\ nextTurn = "X" \* Only enabled on X's turn
    /\ ~Won("O") \* And X has not won
    \* This specifies the spots X will move on X's turn
    /\ \/ /\ BoardEmpty
          /\ StartInCorner
       \/ /\ ~BoardEmpty \* If it's not the start
          /\ \/ /\ CanWin
                /\ Win
             \/ /\ ~CanWin
                /\  \/ /\ CanBlockWin
                       /\ BlockWin
                    \/ /\ ~CanBlockWin
                       /\ \/ /\ CanTakeCenter
                             /\ TakeCenter
                          \/ /\ ~CanTakeCenter
                             /\ \/ /\ CanSetupWin
                                   /\ SetupWin
                                \/ /\ ~CanSetupWin
                                   /\ MoveToEmpty("X") \* No more strategies. Pick spot
    /\ nextTurn' = "O" \* The future state of next turn is O

It has a bunch of pairs of definitions (i.e. CanWin and Win, CanBlockWin and BlockWin) that represent the same action, but one of them encapsulates only the condition part.

While writing this spec in Quint, my intuition was to do something like:

action MoveX = {
  & nextTurn == "X"
  & not(Won("O"))
  & if (BoardEmpty) StartInCorner else
    if (enabled(Win)) Win else
    if (enabled(Block)) Block else
    if (enabled(TakeCenter)) TakeCenter else
    if (enabled(SetupWin)) SetupWin else
    MoveToEmpty("X")
  & nextTurn <- "O"
}

and therefore not have to define any of the Can* operators.

How

I believe the main reason we are not using enabled in this context is some implementation difficulty, so here's how I envision it. First of all, enabled (or whatever name we choose) should have effect signature (Read[r1] & Update[u1]) => Read[r1] - meaning it swallows any updates and the result effect is either Pure (if r1 = {}) or Read[vars]. The implementation for swallowing updates is a simple expression replacement:

guess -> exists
assign -> true
andAction -> andExpr
orAction -> orExpr

Note

We are discussing the simulator/interpreter for Quint and I believe this is very useful for interactive simulation (it's how I did it in my thesis).

WDYT @konnov @shonfeder @Kukovec @p-offtermatt @rodrigo7491 @thpani ?

[konnov]

enabled is a tricky operator as it kind of looks into the future. I think in your example it is relatively safe to use it, but in general you could write something like this:

action A = not(enabled(B)) & x <- x + 1
action B = not(enabled(A)) & x <- x - 1

In TLA+, it is not technically possible, as names have to be defined before they are used, but even there one can probably write some strange things.

[bugarela]

I don't think this is a problem of looking into the future (since in my definition, it is only looking at the current state, hence the state mode), but a problem of cyclical reference we will have to avoid anyway. This is a similar problem:

action A = B
action B = A

Can you think of an example where enabled is a problem with no cyclical references? I'm asking because I'm trying and I can't.

[konnov]

I vaguely remember that it was possible to specify a FIFO channel in epistemic logic, which would not have a single implementation. ENABLED is not exactly about epistemic logic, but it has the same smell. I would have to think a bit more.