| Summary: | Analysis for channel bounds violation ignores guard | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Timothy Bourke <tbourke> |
| Component: | GUI | Assignee: | Alexandre David <adavid> |
| Status: | RESOLVED DUPLICATE | ||
| Severity: | minor | ||
| Priority: | P2 | ||
| Version: | 4.0.6 | ||
| Hardware: | All | ||
| OS: | All | ||
| Architecture: | |||
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.