[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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.



On Friday, November 15, 2019 at 8:14:10 PM UTC-5, Leslie Lamport wrote:
Read my paper Proving Possibility Properties.


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


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 ==


    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.


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2ff3eadf-a9c5-47d8-9909-db30737d91e3%40googlegroups.com.