|Summary:||Invalid assigns are silently ignored in the verification.|
|Product:||UPPAAL||Reporter:||Ulrik Nyman <ulrik>|
|Component:||Engine||Assignee:||Gerd Behrmann <behrmann>|
Description Ulrik Nyman 2003-09-10 15:35:44 CEST
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.
Comment 1 Gerd Behrmann 2003-09-11 09:08:38 CEST
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.
Comment 2 Gerd Behrmann 2003-09-11 09:40:04 CEST
Oops, i didn't want to close it already :-)
Comment 3 Gerd Behrmann 2003-09-11 09:41:24 CEST
Well, for this bug I wanted to postpone it.
Comment 4 Gerd Behrmann 2005-06-29 21:45:20 CEST
We should do something about this. Reopening it.
Comment 5 Gerd Behrmann 2006-01-19 13:34:51 CET
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.
Comment 6 Mark Pavlidis 2006-06-07 23:24:43 CEST
(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.
Comment 7 Gerd Behrmann 2006-06-08 10:35:47 CEST
Comment 8 Gerd Behrmann 2006-06-13 09:17:45 CEST
The problem is limitted to the increment operator. The problem is fixed on the trunk in rev. 2106.