A simple UPPAAL model but can't get result due to the range of an integer variable

Question

This uppaal model showing in the image is part of a top system. It's used to check the condition var==1 hold for at least 10 time units. The range of the integer variable var is [0, 20000].

I use query E<>condition.hold to get the trace, but can't get result within minutes. If I change the range of var to [0, 1000], uppaal return result within seconds.

The question is:

1. Do I use uppaal in a right way?
2. Is uppaal suitable for this kind of model-checking? or any other options?

Thanks for any help

Answer 1

Due to the problem domain that we deal with, the model need to support integer and float data type. And now I understood that Uppaal treat clock as symbolic representation but other variables as concrete value, so maybe it's not possible to meet our requirement. And I am going to try nuxmv, which seems OK because SMT solver is used. I'm not sure whether nuxmv is suitable for timed automata modeling. Have a try.