This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 442 - Analysis for channel bounds violation ignores guard
Summary: Analysis for channel bounds violation ignores guard
Status: RESOLVED DUPLICATE of bug 438
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: GUI (show other bugs)
Version: 4.0.6
Hardware: All All
: P2 minor
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2008-05-13 01:56 CEST by Timothy Bourke
Modified: 2008-09-12 17:17 CEST (History)
0 users

See Also:
Architecture:


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Description Timothy Bourke 2008-05-13 01:56:41 CEST
Global declaration:
     chan c[3];

Template with a self-loop:
     i : int[0,5]
     i < 3
     c[i]!

Gives the unnecessary error:
  The successors of this state are not well defined. This is most likely due
  to range error, index error or division by zero in a guard, synchronisation,
  update or invariant in one or more outgoing edges.

While ordinarily there would be no need to create such transitions, we have found that they can sometimes occur while automatically transforming Uppaal models. In any case, the guard prevents the suggested bounds violation.
Comment 1 Alexandre David 2008-09-12 17:17:02 CEST

*** This bug has been marked as a duplicate of bug 438 ***