Unable to verify UPPAAL properties

Question

I am verifying a very small model. But I receive the memory exhaust message. I changed the model several times but having same problem. I thought that problem would be due to using a user defined function or using the select option to get the random number. Then I changed the model and didn't call the function nor used the Selection option but still.... I am wondering either it's UPPAAL's issue or in my model. There is no error other than memory exhaust. Once the value of "r1" and "r2" are changed after that ctl property doesn't work. CTL works for all values of r1 and r2 before the increment.

Answer 1

The model increments several variables (r1, r2 and cntr): if there is no upper bound for them (and it seems there is not, but I cannot see all the functions), then the state space is going to be huge (all values multiplied times the number of locations, times clock zones) and thus exhaust all the memory.

Either make those variables bounded (do not allow increments passed some value), or declare them as meta (don't do it if you do not understand the consequences).