[tlaplus] Re: Checking that all expected values of a variable are seen

H and Leslie,

Thank you very much for the prompt responses! I will take some time to digest this material.

-Tom

On Friday, November 15, 2019 at 8:14:10 PM UTC-5, Leslie Lamport wrote:

Read my paper Proving Possibility Properties.

Leslie

On Friday, November 15, 2019 at 1:45:30 PM UTC-8, tlabonte@... wrote:

Hi,

I am new to TLA+ and am trying to figure out if there's a way to write a check that guarantees that the spec is defined such that a variable is able to take on all expected values. (In other words, in the set of all states defined by the spec, the variable of interest is seen to take on all expected values.) This would be used to determine if all states of a hardware state machine are reachable.

The complication is that the (simplified) hardware state machine is defined to have an outer cycle, but also a smaller inner cycle, and can run indefinitely (no terminal state). The hardware state machine states and arcs look like:

            a <-> b -> c -> (back to a)

Here is the TLA code demonstrating this:

---------------------------- MODULE CycleExample ----------------------------

MachineStates == { "a", "b", "c" }

VARIABLES MachineState

TypeOK == MachineState \in MachineStates

Init == MachineState = "a"

Next ==

CASE

    MachineState = "a" -> MachineState' = "b" []

    MachineState = "b" -> MachineState' \in {"a", "c"} []

    MachineState = "c" -> MachineState' = "a" []

    OTHER -> MachineState' = "error"



Spec == Init /\ [][Next]_MachineState /\ WF_MachineState(Next)

AllSMStatesVisited ==

<>(\A x \in MachineStates : (MachineState = x))

=============================================================================

I've attempted to write the temporal property, AllSMStatesVisited, to perform this check, but it fails because a valid behavior is for the state machine to cycle between a and b infinitely and never visit c. From what I understand, invariants must be true in every state of the specification and temporal properties must be true for all steps in the specification. Given that, I see no way to write a check that will do what I want.

I understand that I can use TLC to show that a state is reachable by counterexample, but in a large specification, this is not practical. I'm really looking for a way to write a self-contained module that contains the specification and all checks to guarantee that it functions as intended.

Is it possible to achieve this with TLA+ and TLC?

Thank you in advance.

-Tom