Merge lp:~tapaal-contributor/tapaal/show-reduced-net-1879130 into lp:tapaal
Status: | Merged | ||||
---|---|---|---|---|---|
Approved by: | Jiri Srba on 2020-12-18 | ||||
Approved revision: | 1080 | ||||
Merged at revision: | 1117 | ||||
Proposed branch: | lp:~tapaal-contributor/tapaal/show-reduced-net-1879130 | ||||
Merge into: | lp:tapaal | ||||
Diff against target: |
1488 lines (+515/-113) 43 files modified
src/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) |
||||
To merge this branch: | bzr merge lp:~tapaal-contributor/tapaal/show-reduced-net-1879130 | ||||
Related bugs: |
|
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
Jiri Srba | 2020-09-18 | Approve on 2020-12-18 | |
Thomas Pedersen (community) | Resubmit on 2020-12-17 | ||
Kenneth Yrke Jørgensen | code | Approve on 2020-11-09 | |
Review via email:
|
Commit message
Add button for opening the reduced net, obtained after applying the structural reduction rules.
Added the place and transition positions to the saved net file, for the engine to preserve these positions in the reduced net.
This code is dependent on https:/
- 1070. By Thomas Pedersen <email address hidden> on 2020-10-15
-
Add option to open reduced net from the query dialog panel
Thomas Pedersen (tpede16) wrote : | # |
Added the open reduced net button to the query dialog.
The button will close the dialog and run minimal verification before opening the reduced net.
Jiri Srba (srba) wrote : | # |
The reduction gives error when called for timed net. The reduction show option should be available only if the lens says that the new is untimed and non-game.
- 1071. By Thomas Pedersen <email address hidden> on 2020-10-31
-
Make button to open reduced net in query dialog only appear for untimed non-game nets
Thomas Pedersen (tpede16) wrote : | # |
Made the button to open the reduced net from the query dialog only appear if the lens is untimed and non-game
- 1072. By Thomas Pedersen <email address hidden> on 2020-10-31
-
Added the query to the reduced net
- 1073. By Thomas Pedersen <email address hidden> on 2020-11-06
-
Fix query translation for reduced nets
- 1074. By Thomas Pedersen <email address hidden> on 2020-11-06
-
Merge with trunk
- 1075. By Thomas Pedersen <email address hidden> on 2020-11-06
-
Ensure that a new tab is only opened when a reduced net is created
Thomas Pedersen (tpede16) wrote : | # |
Transferred the query that produced the reduced net to the tab for the reduced net and ensured that a new tab is only created when there is a reduced net to display.
Kenneth Yrke Jørgensen (yrke) wrote : | # |
approved, you might consider implementing the changes in the AST as a visitor insted of directly on the AST.
Jiri Srba (srba) wrote : | # |
Open the alternating bit components example - untime it and verify the query. An exception is raised - works correctly in 3.7.1.
- 1076. By Thomas Pedersen <email address hidden> on 2020-11-11
-
Fix getting positional information from multiple components
Thomas Pedersen (tpede16) wrote : | # |
Fixed getting positions from multiple templates and stopped entering simulation mode after verification if the reduced net is opened.
Jiri Srba (srba) wrote : | # |
If you run verification and no reduction rules were applicable, the verification answer still offers "Open reduced net" but when you click nothing happens. If no reduction rules are applicable, then the button show not be enabled.
Jiri Srba (srba) wrote : | # |
Also, open intro net, untime it and change the query so that Target=2. Now try to show the reduced net - it never opens as the state equations kick in - they should be disabled when you want to see the reduced net.
Thomas Pedersen (tpede16) wrote : | # |
Removed the button for opening the reduced net, when no reduction rules are applied.
Disabled query reduction completely when the reduced net is opened from the query dialog. This is dependent on the changes made to verifypn allowing -s OverApprox -q 0 (https:/
Jiri Srba (srba) wrote : | # |
Still needs fixing - open intro example and unselect all verification options (Reductions, Siphon etc). They try to open the reduced net, an error appers.
- 1079. By Thomas Pedersen <email address hidden> on 2020-12-16
-
Disable open reduced net button when query reductions are disabled
Jiri Srba (srba) wrote : | # |
Needs to be merged with trunk - there are a few merge conflicts
- 1080. By Thomas Pedersen <email address hidden> on 2020-12-17
-
Merge with trunk
Thomas Pedersen (tpede16) wrote : | # |
Disable the button for opening the reduced net from the query dialog, when structural reductions are disabled and merged with trunk
The button should also appear in the query dialog next two "Merge net components".