Bug 48 - Invalid assigns are silently ignored in the verification.
Summary: Invalid assigns are silently ignored in the verification.
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 3.5.7
Hardware: All All
: P2 normal
Assignee: Gerd Behrmann
URL: http://www.cs.auc.dk/~ulrikl/uppaal/n...
Depends on:
Blocks:
 
Reported: 2003-09-10 15:35 CEST by Ulrik Nyman
Modified: 2006-06-13 09:17 CEST (History)
1 user (show)

See Also:
Architecture:


Attachments

Note You need to log in before you can comment on or make changes to this bug.
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
Confirmed.
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.