This problem relates to bug #47. When a transition has an assignment between integers with non overlapping ranges the verification simply treats this as if this transition cannot be taken. Such invalid assignments, whether only runtime out of range or non overlapping ranges, should at least generate a warning.
The command line tool (verifyta) actually does produce a warning for this (and for out of range array lookups and for divide by zero exceptions). You are right that the GUI should report this. Will mark it as an enhancement and postpone it to 3.5 work.
Oops, i didn't want to close it already :-)
Well, for this bug I wanted to postpone it.
We should do something about this. Reopening it.
Invalid assignments and other exceptions now cancel the verification. The GUI does not yet produce a proper error message, however the GUI reports the result as MAYBE indicating that something is wrong. I resolve this bug as fixed. There are other bugs already that describe enhancements to the communication protocol to provide better error messags overall.
(In reply to comment #5) > Invalid assignments and other exceptions now cancel the verification. The GUI > does not yet produce a > proper error message, however the GUI reports the result as MAYBE indicating > that something is wrong. In the OS X build for the 3.6 betas and 4.0.0 (GUI and verifyta), the above does not occur. The out of range assignment does not produce and error, or change the value of the variable, and the simulation and verification both continue. I have an example at http://mark.pavlidis.org/code/uppaal/auto_loop_bound.[xml,q] It models a pathological loop where both the loop counter and loop bound both get incremented, thus and infinite loop. Instead of identifying that termintation will not occur, or stopping at the out of range assignment, the simulation continues without incrementing the loop bound (that is at the end of the range) then successfully exits the loop when the counter catches up. I have not verified this on other platforms.
Confirmed.
The problem is limitted to the increment operator. The problem is fixed on the trunk in rev. 2106.