Verifytapn in CPN verification
Bug #1959498 reported by
Jiri Srba
This bug affects 1 person
| Affects | Status | Importance | Assigned to | Milestone | |
|---|---|---|---|---|---|
| TAPAAL |
Fix Committed
|
Medium
|
Kenneth Yrke Jørgensen | ||
Bug Description
In cpn branch, open the alternating-
It returns NPE (wrong engine - verifytapn in this case) but in principle this should work
that we unfold using verifydtapn and then verify using verifytapn.
Related branches
lp:~tapaal-contributor/tapaal/cpn-tapn
- Jiri Srba: Approve
-
Diff: 1231 lines (+467/-282)15 files modifiedsrc/dk/aau/cs/verification/QueryResult.java (+37/-0)
src/dk/aau/cs/verification/VerificationResult.java (+30/-15)
src/dk/aau/cs/verification/VerifyTAPN/VerifyDTAPN.java (+30/-24)
src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java (+50/-51)
src/dk/aau/cs/verification/VerifyTAPN/VerifyPNCTLOutputParser.java (+9/-1)
src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOutputParser.java (+9/-1)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java (+93/-22)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java (+1/-1)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOptions.java (+38/-6)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOutputParser.java (+21/-0)
src/net/tapaal/gui/petrinet/dialog/QueryDialog.java (+12/-12)
src/net/tapaal/gui/petrinet/verification/RunVerification.java (+120/-135)
src/net/tapaal/gui/petrinet/verification/RunVerificationBase.java (+13/-12)
src/net/tapaal/gui/petrinet/verification/Verifier.java (+3/-1)
src/net/tapaal/gui/petrinet/verification/VerifyTAPNEngineOptions.java (+1/-1)
Revision history for this message
| Kenneth Yrke Jørgensen (yrke) wrote | #2 |
Revision history for this message
| Kenneth Yrke Jørgensen (yrke) wrote | #3 |
| Changed in tapaal: | |
| status: | New → In Progress |
| importance: | Undecided → High |
| assignee: | nobody → Kenneth Yrke Jørgensen (yrke) |
| importance: | High → Medium |
| Changed in tapaal: | |
| status: | In Progress → Fix Committed |
To post a comment you must log in.
It seem it keeps the verifytapn engine when converting to colored.
I guess in principiel we could support unfolding and the verification, but It will be yet an other special case to handle