Re: [tlaplus] Checking that a specific path is always possible to take

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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

> On Oct 28, 2025, at 2:41 PM, Dylan Zueck <dzueck@xxxxxxx> wrote:
> 
> 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

-- 
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 visit https://groups.google.com/d/msgid/tlaplus/CD51BDE0-08DA-4062-90E3-84C303CE3DBA%40lemmster.de.