TAPAAL

Merge lp:~yrke/tapaal/fix1976496 into lp:tapaal

  1. fix1976496
  2. Merge into trunk
Proposed by Kenneth Yrke Jørgensen
Status: Needs review
Proposed branch: lp:~yrke/tapaal/fix1976496
Merge into: lp:tapaal
Diff against target: 98 lines (+14/-13)
3 files modified
src/pipe/gui/RunKBoundAnalysis.java (+2/-3)
src/pipe/gui/RunVerification.java (+10/-7)
src/pipe/gui/RunVerificationBase.java (+2/-3)
To merge this branch: bzr merge lp:~yrke/tapaal/fix1976496
Reviewer Review Type Date Requested Status
TAPAAL Reviewers Pending
Review via email: mp+423763@code.launchpad.net
To post a comment you must log in.

Unmerged revisions

1170. By Kenneth Yrke Jørgensen

Fix bug #1976496, dont show duscrete time warning for untimed games (or timed models that are untimed)

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
=== modified file 'src/pipe/gui/RunKBoundAnalysis.java'
--- src/pipe/gui/RunKBoundAnalysis.java 2021-09-23 11:36:16 +0000
+++ src/pipe/gui/RunKBoundAnalysis.java 2022-06-01 12:45:16 +0000
@@ -4,6 +4,7 @@
4import javax.swing.JSpinner;4import javax.swing.JSpinner;
55
6import dk.aau.cs.Messenger;6import dk.aau.cs.Messenger;
7import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
7import dk.aau.cs.verification.VerifyTAPN.VerifyPN;8import dk.aau.cs.verification.VerifyTAPN.VerifyPN;
8import net.tapaal.resourcemanager.ResourceManager;9import net.tapaal.resourcemanager.ResourceManager;
9import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace;10import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace;
@@ -11,8 +12,6 @@
11import dk.aau.cs.verification.ModelChecker;12import dk.aau.cs.verification.ModelChecker;
12import dk.aau.cs.verification.VerificationResult;13import dk.aau.cs.verification.VerificationResult;
1314
14import java.util.ArrayList;
15
16public class RunKBoundAnalysis extends RunVerificationBase {15public class RunKBoundAnalysis extends RunVerificationBase {
1716
18 private final JSpinner spinner;17 private final JSpinner spinner;
@@ -25,7 +24,7 @@
25 }24 }
2625
27 @Override26 @Override
28 protected boolean showResult(VerificationResult<TAPNNetworkTrace> result) {27 protected boolean showResult(VerificationResult<TAPNNetworkTrace> result, TimedArcPetriNetNetwork model) {
29 if(result != null && !result.error()) {28 if(result != null && !result.error()) {
30 if (!result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) {29 if (!result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) {
31 JOptionPane.showMessageDialog(CreateGui.getApp(),30 JOptionPane.showMessageDialog(CreateGui.getApp(),
3231
=== modified file 'src/pipe/gui/RunVerification.java'
--- src/pipe/gui/RunVerification.java 2021-10-13 18:51:36 +0000
+++ src/pipe/gui/RunVerification.java 2022-06-01 12:45:16 +0000
@@ -19,6 +19,7 @@
19import javax.swing.table.TableModel;19import javax.swing.table.TableModel;
20import javax.swing.table.TableRowSorter;20import javax.swing.table.TableRowSorter;
21import dk.aau.cs.gui.TabContent;21import dk.aau.cs.gui.TabContent;
22import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
22import dk.aau.cs.verification.*;23import dk.aau.cs.verification.*;
23import dk.aau.cs.Messenger;24import dk.aau.cs.Messenger;
24import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace;25import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace;
@@ -45,7 +46,7 @@
45 }46 }
4647
47 @Override48 @Override
48 protected boolean showResult(VerificationResult<TAPNNetworkTrace> result) {49 protected boolean showResult(VerificationResult<TAPNNetworkTrace> result, TimedArcPetriNetNetwork model) {
49 if (reduceNetOnly) {50 if (reduceNetOnly) {
50 //If the engine is only called to produce a reduced net, it will fail, but no error message should be shown51 //If the engine is only called to produce a reduced net, it will fail, but no error message should be shown
51 if (result != null && result.stats().transitionsCount() == 0 && result.stats().placeBoundCount() == 0) {52 if (result != null && result.stats().transitionsCount() == 0 && result.stats().placeBoundCount() == 0) {
@@ -415,12 +416,14 @@
415 (queryResult.queryType() == QueryType.EG && !queryResult.isQuerySatisfied()) || 416 (queryResult.queryType() == QueryType.EG && !queryResult.isQuerySatisfied()) ||
416 (queryResult.queryType() == QueryType.AF && queryResult.isQuerySatisfied())) 417 (queryResult.queryType() == QueryType.AF && queryResult.isQuerySatisfied()))
417 && modelChecker.useDiscreteSemantics()){418 && modelChecker.useDiscreteSemantics()){
418 gbc = new GridBagConstraints();419 if (!model.isUntimed()) {
419 gbc.gridx = 0;420 gbc = new GridBagConstraints();
420 gbc.gridy = 11;421 gbc.gridx = 0;
421 gbc.gridwidth = 2;422 gbc.gridy = 11;
422 gbc.anchor = GridBagConstraints.WEST;423 gbc.gridwidth = 2;
423 panel.add(new JLabel("<html><font color=red>The verification answer is guaranteed for<br/>the discrete semantics only (integer delays).</font></html>"), gbc);424 gbc.anchor = GridBagConstraints.WEST;
425 panel.add(new JLabel("<html><font color=red>The verification answer is guaranteed for<br/>the discrete semantics only (integer delays).</font></html>"), gbc);
426 }
424 }427 }
425 428
426 return panel;429 return panel;
427430
=== modified file 'src/pipe/gui/RunVerificationBase.java'
--- src/pipe/gui/RunVerificationBase.java 2021-09-24 09:34:48 +0000
+++ src/pipe/gui/RunVerificationBase.java 2022-06-01 12:45:16 +0000
@@ -1,6 +1,5 @@
1package pipe.gui;1package pipe.gui;
22
3import java.io.File;
4import java.util.concurrent.ExecutionException;3import java.util.concurrent.ExecutionException;
54
6import javax.swing.*;5import javax.swing.*;
@@ -220,7 +219,7 @@
220 }219 }
221 firePropertyChange("state", StateValue.PENDING, StateValue.DONE);220 firePropertyChange("state", StateValue.PENDING, StateValue.DONE);
222221
223 if (showResult(result) && spinner != null) {222 if (showResult(result, model) && spinner != null) {
224 options = new VerifyPNOptions(options.extraTokens(), pipe.dataLayer.TAPNQuery.TraceOption.NONE, SearchOption.BFS, false, ModelReduction.BOUNDPRESERVING, false, false, 1, pipe.dataLayer.TAPNQuery.QueryCategory.Default, pipe.dataLayer.TAPNQuery.AlgorithmOption.CERTAIN_ZERO, false, pipe.dataLayer.TAPNQuery.QueryReductionTime.NoTime, false, null, false, false);223 options = new VerifyPNOptions(options.extraTokens(), pipe.dataLayer.TAPNQuery.TraceOption.NONE, SearchOption.BFS, false, ModelReduction.BOUNDPRESERVING, false, false, 1, pipe.dataLayer.TAPNQuery.QueryCategory.Default, pipe.dataLayer.TAPNQuery.AlgorithmOption.CERTAIN_ZERO, false, pipe.dataLayer.TAPNQuery.QueryReductionTime.NoTime, false, null, false, false);
225 KBoundAnalyzer optimizer = new KBoundAnalyzer(model, options.extraTokens(), modelChecker, new MessengerImpl(), spinner);224 KBoundAnalyzer optimizer = new KBoundAnalyzer(model, options.extraTokens(), modelChecker, new MessengerImpl(), spinner);
226 optimizer.analyze((VerifyTAPNOptions) options, true);225 optimizer.analyze((VerifyTAPNOptions) options, true);
@@ -242,5 +241,5 @@
242 });241 });
243 }242 }
244243
245 protected abstract boolean showResult(VerificationResult<TAPNNetworkTrace> result);244 protected abstract boolean showResult(VerificationResult<TAPNNetworkTrace> result, TimedArcPetriNetNetwork model);
246}245}

Subscribers

People subscribed via source and target branches