Discrete inclusion provides wrong answer
Affects | Status | Importance | Assigned to | Milestone | |
---|---|---|---|---|---|
TAPAAL |
Fix Released
|
Critical
|
Jiri Srba | ||
VerifyTAPN |
Won't Fix
|
Critical
|
Unassigned |
Bug Description
Open the attached net verification-
(even if the query is upward closed). This was a problem already at 2.0.0, so this has nothing to do
with the relaxation of the upward closed queries. The problem is in the engine and I attach also the
exported files 1.xml 1.q that show the problem:
./verifytapn64 -k 4 -f 1 ~/1.xml ~/1.q
is NOT satisfied, and
./verifytapn64 -k 4 -f 0 ~/1.xml ~/1.q
is satisfied (the same for 32 version of the engine).
The reason seems the place on the receiver side where there is the token in the initial marking.
If this is not including in the inclusion places, all is fine. The same is, of course, if in the query we
ask about equality to 1 for this place.
Related branches
- Kenneth Yrke Jørgensen: Approve (code)
- Jiri Srba: Approve
-
Diff: 252 lines (+60/-12)10 files modifiedsrc/dk/aau/cs/io/ResourceManager.java (+5/-0)
src/dk/aau/cs/verification/IconSelector.java (+2/-1)
src/dk/aau/cs/verification/QueryResult.java (+7/-1)
src/dk/aau/cs/verification/UPPAAL/VerifytaOutputParser.java (+5/-2)
src/dk/aau/cs/verification/VerificationResult.java (+9/-0)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java (+6/-5)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java (+2/-2)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOutputParser.java (+4/-1)
src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java (+8/-0)
src/pipe/dataLayer/TAPNQuery.java (+12/-0)
Changed in tapaal: | |
importance: | Undecided → Critical |
milestone: | none → 2.1 |
Changed in verifytapn: | |
status: | New → Won't Fix |
Changed in tapaal: | |
status: | New → In Progress |
Changed in tapaal: | |
status: | In Progress → Fix Committed |
Changed in tapaal: | |
status: | Fix Committed → Fix Released |
One more information, the problem is here with DFS and CoverMost search, for BFS it returns the correct answer.