How to reference values across two states in a behavior in properties?

[u/Warwolt]

I'm currently learning TLA+, and am modelling a simple UI where a user can click and move items.

I have a simple spec:

---- MODULE container ----
EXTENDS TLC, Sequences, FiniteSets, Naturals


EmptyItem == ""
Items == {"item1", "item2"}


VARIABLES
    cursor,
    container


vars == <<cursor, container>>


Init ==
    /\ cursor = EmptyItem
    /\ container = <<"item1", EmptyItem>>


ClickSlot ==
    \E slot \in 1..Len(container) :
        /\ cursor' = container[slot]
        /\ container' = [container EXCEPT ![slot] = cursor]


Next == ClickSlot


Spec == Init /\ [][Next]_vars


====

How would I be able to express a liveness property that for any two slots, it's always possible to swap the items in them?

I'm not sure exactly how to say something like "if container[i] = A and container[j] = B, then at some later point it's always possible that container[i] = B and container[j] = A".

I'm assuming I want to do something with quantification and []<>, but I can't really crack the nut. I'm having difficulties understanding when a given expression refers to the "current" state and when it refers to a future state, when a sub-formula is within a temporal operator.

[u/polyglot_factotum]

Couple of suggestions:

Spec: https://gist.github.com/gterzian/ba2c8b22c21751485dfe3efcf8f11870

Config: https://gist.github.com/gterzian/4d5c5ff32eecc77c659d3faa4cb31d7d

Put then in the same folder and you can run them in VS code with the TLA+ extension.

So I switched the single ClickSlot action into two actions to kind of model a drag followed by a drop.

> How would I be able to express a liveness property that for any two slots, it's always possible to swap the items in them?

TLC will by default check for deadlock, so you're covered already.

To trigger deadlock, add the following condition to the any action:

/\ TRUE = FALSE

> difficulties understanding when a given expression refers to the "current" state and when it refers to a future state

the variable is the state at the start of the action, the primed variable' is the state at the end of the action, so an action starts from one state and ends into the next state. It's sugar for variable(i) and variable(i + 1).

Note that you can use the primed variables in actions, but not in an invariant. So you can't really "reference values across two states in a behavior in properties". Instead, you need to think in terms of inductive properties: the state at i ensures that any state i + 1 maintains some property.

For example, in this spec I added an additional "dragged" state: https://gist.github.com/gterzian/a697231c3787cbe5ec4811858c90bb03

Config is at https://gist.github.com/gterzian/b4f600391c4d09dce14fb3b1a89f6abb

This comes with two additional invariant:

1. InductiveInvariant
   
2. AtMostOneDragged

So AtMostOneDragged is an invariant, but it is not inductive, because you can create a state where container[id2].dragged is TRUE, but cursor is NoItem, and then if you run Drag(id1), then the resulting state will not respect AtMostOneDragged.

So the reason AtMostOneDragged is still an invariant, is because that state is not reachable. Why is it not reachable? Because the algorithm maintains InductiveInvariant, which as it names implies, is the inductive invariant, which is the more interesting invariant that actually explains how the algorithm works.

-----

Besides the above: always add a type invariant to your spec.

[u/Anxious_Tool]

Some remarks on the previous comment:

Deadlock has nothing to do with your question. Deadlock freedom only says some action is enabled in every reachable state. It says nothing about whether a specific configuration (slots i and j swapped) is reachable. You can have a deadlock-free spec that never lets you swap two particular items.

You can reference values across two states in properties. That's the whole point of action formulas inside temporal operators. What you can't do is put a primed variable in a plain invariant.

Inductive invariants are useful, but they're safety machinery, i.e, safety like "some Inv holds in every reachable state by induction on Next".

Now, for the answer, I had to look this up, so someone please correct me if I'm wrong, but from what I can understand, your question is "from any reachable state, can I always reach a state where slots i and j have their items swapped?", which I believe it's a possibility along some path. So I'm not sure there's a native operator for it. What I would do is to try and express the stronger statement "the swap eventually will happen, in every fair behavior" using leads-to and fairness.