Show net after structural reductions
Affects | Status | Importance | Assigned to | Milestone | |
---|---|---|---|---|---|
TAPAAL |
Fix Committed
|
Wishlist
|
Thomas Pedersen |
Bug Description
This is relevant only for the CTL query dialog that allows the option for structural reductions. The Verification Result shows the number of applications of reduction rules. Would be nice to have a button next to the statistics of how many reductions rules were used that would say "Open the reduced net". By clicking this, a new tab should open that would display the reduced net. The net needs to be first composed into a single net (this happens automatically in GUI before the engine is called). The engine should be in this case called with a special switch --write-reduced <filename>
so that the engine outputs the reduced net in to a file. This file should be then opened in a separate tab.
Related branches
- Jiri Srba: Approve
- Thomas Pedersen (community): Needs Resubmitting
- Kenneth Yrke Jørgensen: Approve (code)
-
Diff: 1488 lines (+515/-113)43 files modifiedsrc/dk/aau/cs/TCTL/AritmeticOperator.java (+5/-1)
src/dk/aau/cs/TCTL/TCTLAFNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLAGNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLAUNode.java (+7/-1)
src/dk/aau/cs/TCTL/TCTLAXNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLAbstractProperty.java (+2/-0)
src/dk/aau/cs/TCTL/TCTLAndListNode.java (+8/-1)
src/dk/aau/cs/TCTL/TCTLAtomicPropositionNode.java (+32/-1)
src/dk/aau/cs/TCTL/TCTLConstNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLDeadlockNode.java (+5/-1)
src/dk/aau/cs/TCTL/TCTLEFNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLEGNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLEUNode.java (+7/-1)
src/dk/aau/cs/TCTL/TCTLEXNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLFalseNode.java (+5/-1)
src/dk/aau/cs/TCTL/TCTLNotNode.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLOrListNode.java (+8/-1)
src/dk/aau/cs/TCTL/TCTLPathPlaceHolder.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLPathToStateConverter.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLPlaceNode.java (+11/-1)
src/dk/aau/cs/TCTL/TCTLPlusListNode.java (+8/-1)
src/dk/aau/cs/TCTL/TCTLStatePlaceHolder.java (+5/-1)
src/dk/aau/cs/TCTL/TCTLStateToPathConverter.java (+6/-1)
src/dk/aau/cs/TCTL/TCTLTermListNode.java (+8/-1)
src/dk/aau/cs/TCTL/TCTLTransitionNode.java (+7/-1)
src/dk/aau/cs/TCTL/TCTLTrueNode.java (+5/-1)
src/dk/aau/cs/verification/VerificationResult.java (+5/-0)
src/dk/aau/cs/verification/VerifyTAPN/VerifyPN.java (+3/-2)
src/dk/aau/cs/verification/VerifyTAPN/VerifyPNOptions.java (+21/-11)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java (+1/-1)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNDiscreteVerification.java (+1/-1)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNExporter.java (+63/-16)
src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java (+5/-4)
src/net/tapaal/TAPAAL.java (+1/-1)
src/pipe/dataLayer/TAPNQuery.java (+10/-0)
src/pipe/gui/Export.java (+2/-2)
src/pipe/gui/KBoundAnalyzer.java (+1/-1)
src/pipe/gui/RunVerification.java (+54/-16)
src/pipe/gui/RunVerificationBase.java (+17/-5)
src/pipe/gui/Verifier.java (+65/-16)
src/pipe/gui/widgets/QueryDialog.java (+73/-8)
src/pipe/gui/widgets/QueryPane.java (+1/-1)
src/pipe/gui/widgets/WorkflowDialog.java (+3/-3)
Changed in tapaal: | |
assignee: | nobody → Thomas Pedersen (tpede16) |
Changed in tapaal: | |
status: | New → In Progress |
Changed in tapaal: | |
status: | In Progress → Fix Committed |