UPPAAL: What cause clock to stop running

Question

I am currently running my UPPAAL simulator. My simulator stops running the code after a certain point. This point varies depending on the declaration i provide. But i would like to know generally when does the clock stop running? Is there something that triggers this?

Answer 1

I'm not sure if I interpret your question correctly, if I could read your model I may give you some precise advice.

Trying to guess what the problem is, I can say there are times when the Uppaal simulator takes infinitely many discrete steps (transitions) without increasing any of the clock variables.

The feeling is that "the clock is stopped", while the rest of the simulation is going on. In this case, the time is not actually stopped: Uppaal, among all possible paths, it is just exploring the one where clock does not evolve. If the simulator (or the model checker) can take infinitely many transitions without increasing the clock variables, that is an example of "Zeno path".

It is a responsibility of the person who writes the model to avoid the possibility of taking zeno paths.

If you are not sure your model is free of Zeno paths, you can use known methods for verifying that a Timed Automaton has no zeno paths (in Uppaal).

Another possibility is that the simulator stop running at all saying that there is a deadlock. In this case the problem is not that the clock stopped running, but that you arrived at a situation where all possible transitions are disabled (maybe because all possible guards are never enabled, or because all the possible target states of your enabled transitions have some time invariants that are false)