Verificiation results explanation
Bug #1879129 reported by
Jiri Srba
This bug affects 1 person
Affects | Status | Importance | Assigned to | Milestone | |
---|---|---|---|---|---|
TAPAAL |
Fix Released
|
Wishlist
|
Thomas Pedersen |
Bug Description
The "Verification result" dialog shows a button called explanation.
I would suggest to remove the button and instead show the explanation for
Discovered/
Test it both for timed and untimed nets.
Related branches
lp:~tapaal-contributor/tapaal/verification-result-explanation-to-tooltip-1879129
- Jiri Srba: Approve
- Thomas Pedersen (community): Needs Resubmitting
- Kenneth Yrke Jørgensen: Approve (code)
-
Diff: 297 lines (+66/-93)7 files modifiedsrc/dk/aau/cs/verification/ModelChecker.java (+2/-1)
src/dk/aau/cs/verification/UPPAAL/Verifyta.java (+7/-5)
src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java (+14/-21)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java (+9/-15)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java (+7/-13)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOutputParser.java (+1/-1)
src/pipe/gui/RunVerification.java (+26/-37)
Changed in tapaal: | |
assignee: | nobody → Thomas Pedersen (tpede16) |
Changed in tapaal: | |
status: | New → In Progress |
Changed in tapaal: | |
status: | In Progress → Fix Committed |
Changed in tapaal: | |
status: | Fix Committed → Fix Released |
To post a comment you must log in.
I can see in the code that there is a specific verification result explanation for when a CTL query is solved without using state equations. However, I am having trouble creating a CTL query, which is not solved by state equations, to test it.
Is there some option to disable state equations I am missing? Otherwise, how do I go about creating a CTL query which cannot be solved by state equations?