Checking that a specific path is always possible to take

[Dylan Zueck]

I am trying to model a system where at any point some interrupt function could be triggered. Since it could happen at any time, I want to ensure that the model reflects this behavior by proving that at every point, the function corresponding to the interrupt could possibly be true.

As an example model:

Variables x

DoSomething == x' = (x + 1) % 10

Interrupt == x <= 10 /\ x' = 5

Init == x = 0

Next == DoSomething \/ Interrupt

I already ensure that the interrupt does not see any partial state, so there is no need to account for partial states from the DoSomething path. What I want to show is that at all points the Interrupt path is possible for the model checker to evaluate to TRUE (and thus it could happen at any point). 

In my real model, the Interrupt path only consists of constraints on next state variables (i.e. x'), however I am comprehensive to assume that this means it can always be true. 

Thanks

[Andrew Helwer]

It sounds like the property you want is [](ENABLED Interrupt). This is similar to deadlock checking, which is the property [](ENABLED Next).

Andrew

--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/a30b7ea3-dc7e-4835-9472-0a48a28aa577n%40googlegroups.com.

[Markus Kuppe]

Interrupt cannot occur at any time in your example specification because you restricted Interrupt to only happen when x is less than or equal to 10.

Markus