TAR wrong GUI reporting
Bug #1958791 reported by
Jiri Srba
This bug affects 1 person
Affects | Status | Importance | Assigned to | Milestone | |
---|---|---|---|---|---|
TAPAAL |
Fix Committed
|
Undecided
|
Kenneth Yrke Jørgensen |
Bug Description
Open referendum-colored (untimed) and verify the second query "tie vote".
It returns true. Now turn on TAR (trace abstraction refinement) in advanced
query dialog. Verify again and it returns true but writes "The query was resolved
using state equations" which is wrong but it should instead write "The query
was resolved using trace abstraction refinement."
Related branches
lp:~tapaal-contributor/tapaal/cpn-solvedBy
- Jiri Srba: Approve
-
Diff: 375 lines (+33/-55)9 files modifiedsrc/dk/aau/cs/approximation/ApproximationWorker.java (+22/-22)
src/dk/aau/cs/verification/QueryResult.java (+0/-9)
src/dk/aau/cs/verification/UPPAAL/UppaalIconSelector.java (+1/-1)
src/dk/aau/cs/verification/VerificationResult.java (+0/-4)
src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java (+1/-2)
src/dk/aau/cs/verification/VerifyTAPN/VerifyPNCTLOutputParser.java (+0/-1)
src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOutputParser.java (+0/-1)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOutputParser.java (+1/-5)
src/net/tapaal/gui/petrinet/verification/RunVerification.java (+8/-10)
Changed in tapaal: | |
status: | In Progress → Fix Committed |
To post a comment you must log in.
The same problem is in ERK (untime, nongame CPN model). Verify the property using "siphon-trap" option which kicks in but it instead of siphon-trap returns that it was the state-equations that solved the query. Here the problem is that the GUI does not really print the reason why the query was solved (it only does so in the MCC keywords but we should not rely on this information).