UPPAAL verification does not work
Bug #331012 reported by
Jiri Srba
| Affects | Status | Importance | Assigned to | Milestone | |
|---|---|---|---|---|---|
| TAPAAL |
Fix Released
|
Medium
|
Kenneth Yrke Jørgensen | ||
Bug Description
Consider the following attached net and ask the query, exists a path exists a marking such
that
P1==2
leave all other options in the query dialog in default.
Clearly, this marking is achievable and UPPAAL says yes, but it gives the following ouput trace:
TRACE:
0.5
T0
0.5
T1
TRACE END
which clearly does not place two token in P1 but only one!!! This is a serious problem!
Revision history for this message
| Jiri Srba (srba) wrote | #1 |
| Changed in tapn: | |
| importance: | Undecided → Critical |
| milestone: | none → version1 |
Revision history for this message
| Kenneth Yrke Jørgensen (yrke) wrote | #2 |
| Changed in tapn: | |
| assignee: | nobody → yrke |
| importance: | Critical → Medium |
| status: | New → Fix Committed |
| Changed in tapn: | |
| status: | Fix Committed → Fix Released |
To post a comment you must log in.
This was not relay a bug but a feature just a feature we realy finished. The code properly need a look at again at some time.
I have committed a smarll fix that solves the problem for now.