I hope someone here can give me your advice or knowledge.
I have already read about train-gate example in Uppaal and in Spin. I also tried to use Uppaal for verifying my plans, and the results were great. However. I would like to expand my plan a little bit. Therefore, I tried to use Spin to verify some properties which are not relevant to the time.
My question is: May I understand that if I remove the relative time (clock), Uppaal can handle the same Spin. if no, can you give me an example or property to demonstrate?
Any information or advice is helpful to me. Sincerely thank you so much for reading.
UPPAAL assumes dense time semantics, which means that queries like "next state" make no sense. It also assumes synchronous time therefore its algorithms have fewer assumptions it can exploit, thus verification might be slower for untimed models.