the constants and ranges should also be range-checked, for example expressions like the following are asking for trouble but accepted: const int x = 1000000000000000000; int[0,5000000000000000000000000] x = 1000000000000000000; (strange how this goes through scanner, does it expect 64bit integers?) typechecker should also issue errors on meaningless expressions like "x=-1" where x is a clock and "-1" is arbitrary constant expression evaluating to negative value. Currently this is not checked and shows up only during simulation/verification. typechecker could also issue a warning if the estimated range of non-const expression contains negative values in the clock assignment -- that would encourage better style of declaring explicit ranges, but may become annoyance, so this is debatable.
now I've found a case where range checker is too restrictive when dealing with clocks: Declarations: typedef int[0, 10000000] time_t; const int MULT = 4; const int CYCLE = 250*1000/MULT; const int CYCLELIMIT = 12*MULT; time_t counter=1; clock global; then put expression "global<=counter*CYCLE" into invariant or guard. For MULT=4 Uppaal says "clock constraint is out of range", but it is fine with MULT=1 or MULT=2.
please ignore my last comment: my fault, the issue can be fixed by the following declaration: int[0, CYCLELIMIT] counter=1;
the fix for this bug seems to depend on the fix for bug 488. *** This bug has been marked as a duplicate of bug 488 ***
Actually it's not a duplicate of bug 488. It's similar but not the same. The lexer was not able to recognize INT_MIN due to overflow on positive integers even though it should have done it. This comes from the rule (unary not) natural. There's a special case for that now. The real overflow issue has been fixed in the same revision but it's a different fix.