I am new to model checking, I am using UPPAAL and I can’t find how to query what I want to query:
I have this model:
I am trying to see if there is a course of actions that could lead to an impossibility to reach the goal place.
Is there an UPPAAL query that could allow me to do that? Or is this not the right tool? Am I misunderstanding something fundamental in model checking.
I have considered the deadlock
property but it only detects when stuck in one and only one place. I have tried A<> Process.goal
but it seems like the model checker is satisfied with just never going there?