TAPAAL

Wrong verification answer

Bug #1031666 reported by Jiri Srba
6
This bug affects 1 person
Affects Status Importance Assigned to Milestone
TAPAAL
Fix Released
Critical
Jiri Srba
2.1
Fix Released
Critical
Jiri Srba
TAPAAL 2.1.2

Bug Description

This bug affects both 2.1 and trunk.

Open producer-consumer example and open the avoid garbage query.
Change the number of extra tokens to 0 and verify the query.

It says that it is satisfied (and returns an empty trace) while it should say
that it is not satisfied for this number of extra tokens (and that the answer is inconclusive).

Related branches

lp:~tapaal-contributor/tapaal/wrongVerificationAnswers-bug1031666
Jiri Srba: Approve
Kenneth Yrke Jørgensen: Approve
Diff: 62 lines (+8/-7)
3 files modified
src/dk/aau/cs/verification/QueryResult.java (+2/-2)
src/dk/aau/cs/verification/UPPAAL/UppaalIconSelector.java (+4/-3)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java (+2/-2)
lp:~tapaal-contributor/tapaal/wrongVerificationAnswers-bug1031666-for-2.1
Jiri Srba: Approve
Kenneth Yrke Jørgensen: Pending requested
Diff: 35 lines (+4/-4)
2 files modified
src/dk/aau/cs/verification/QueryResult.java (+2/-2)
src/dk/aau/cs/verification/UPPAAL/UppaalIconSelector.java (+2/-2)
Jiri Srba (srba)
Changed in tapaal:
milestone: none → 2.2
Revision history for this message
Jiri Srba (srba) wrote :

In fact the answer IS correct (the EG query is satisfied because there is a deadlock right from the start).

When UPPAAL engine is used, we should just add "The answer is conclusive only if the net is bounded for the number of extra tokens. Run the boundedness check in the query dialog."

However, when using the discrete engine, the answer is "The property is NOT satisfied" but add more tokens and try again ...
This is wrong, it should have found the deadlock (as there are no extra tokens).

Revision history for this message
Jiri Srba (srba) wrote :

The behaviour should now be correct.

If the net is unbounded, then for EG and AF neither the positive nor the negative answer is conclusive.
(If there are not enough tokens we might get some extra deadlocks).

It should now work ok. There is still an issues with verifydtapn, a separate bug report will be done.

Changed in tapaal:
assignee: nobody → Jiri Srba (srba)
status: New → In Progress
TAPAAL Janitor (tapaal)
Changed in tapaal:
status: In Progress → Fix Committed
Kenneth Yrke Jørgensen (yrke)
Changed in tapaal:
milestone: 2.2 → none
status: Fix Committed → Fix Released
To post a comment you must log in.
This report contains Public information  
Everyone can see this information.
Subscribing...

Other bug subscribers

Remote bug watches

Bug watches keep track of this bug in other bug trackers.