Hi Tom, Unfortunately, there’s no easy way to check this property in TLA+. It’s a consequence of "Sometimes" is Sometimes "Not Never"; there are certain properties that branching time logics can express that linear time logics cannot. That said, it’s possible to work around this. We can show a state is reachable via counterexample. We can also instantiate the spec in a larger “controller” spec. The controller has an auxiliary variable that tracks which states the machine reached. We also add an additional Reset action, which returns the machine to its initial state without changing the aux variable. This is then equivalent to simulating multiple different behaviors of the machine, to see if any combination of them reach all of the states. VARIABLES MachineState, seen_states vars == <<MachineState, seen_states>> Machine == INSTANCE CycleExample WITH MachineState <- MachineState Init == /\ Machine!Init /\ seen_states = {MachineState} Reset == /\ MachineState' = "a" Next == /\ seen_states' = seen_states \union {MachineState} /\ \/ Reset \/ Machine!Next Spec == Init /\ [][Next]_vars AllStatesNotVisited == seen_states /= Machine!MachineStates If AllStatesNotVisited is violated then we know that some combination of executions reach all possible states. H From: tlaplus@xxxxxxxxxxxxxxxx <tlaplus@xxxxxxxxxxxxxxxx> On Behalf Of tlabonte@xxxxxxxxx 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 -- 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/00d001d59c0c%24451d8200%24cf588600%24%40gmail.com. |