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
1=== modified file 'src/pipe/gui/RunKBoundAnalysis.java'
2--- src/pipe/gui/RunKBoundAnalysis.java 2021-09-23 11:36:16 +0000
3+++ src/pipe/gui/RunKBoundAnalysis.java 2022-06-01 12:45:16 +0000
4@@ -4,6 +4,7 @@
5 import javax.swing.JSpinner;
6
7 import dk.aau.cs.Messenger;
8+import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
9 import dk.aau.cs.verification.VerifyTAPN.VerifyPN;
10 import net.tapaal.resourcemanager.ResourceManager;
11 import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace;
12@@ -11,8 +12,6 @@
13 import dk.aau.cs.verification.ModelChecker;
14 import dk.aau.cs.verification.VerificationResult;
15
16-import java.util.ArrayList;
17-
18 public class RunKBoundAnalysis extends RunVerificationBase {
19
20 private final JSpinner spinner;
21@@ -25,7 +24,7 @@
22 }
23
24 @Override
25- protected boolean showResult(VerificationResult<TAPNNetworkTrace> result) {
26+ protected boolean showResult(VerificationResult<TAPNNetworkTrace> result, TimedArcPetriNetNetwork model) {
27 if(result != null && !result.error()) {
28 if (!result.getQueryResult().boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) {
29 JOptionPane.showMessageDialog(CreateGui.getApp(),
30
31=== modified file 'src/pipe/gui/RunVerification.java'
32--- src/pipe/gui/RunVerification.java 2021-10-13 18:51:36 +0000
33+++ src/pipe/gui/RunVerification.java 2022-06-01 12:45:16 +0000
34@@ -19,6 +19,7 @@
35 import javax.swing.table.TableModel;
36 import javax.swing.table.TableRowSorter;
37 import dk.aau.cs.gui.TabContent;
38+import dk.aau.cs.model.tapn.TimedArcPetriNetNetwork;
39 import dk.aau.cs.verification.*;
40 import dk.aau.cs.Messenger;
41 import dk.aau.cs.model.tapn.simulation.TAPNNetworkTrace;
42@@ -45,7 +46,7 @@
43 }
44
45 @Override
46- protected boolean showResult(VerificationResult<TAPNNetworkTrace> result) {
47+ protected boolean showResult(VerificationResult<TAPNNetworkTrace> result, TimedArcPetriNetNetwork model) {
48 if (reduceNetOnly) {
49 //If the engine is only called to produce a reduced net, it will fail, but no error message should be shown
50 if (result != null && result.stats().transitionsCount() == 0 && result.stats().placeBoundCount() == 0) {
51@@ -415,12 +416,14 @@
52 (queryResult.queryType() == QueryType.EG && !queryResult.isQuerySatisfied()) ||
53 (queryResult.queryType() == QueryType.AF && queryResult.isQuerySatisfied()))
54 && modelChecker.useDiscreteSemantics()){
55- gbc = new GridBagConstraints();
56- gbc.gridx = 0;
57- gbc.gridy = 11;
58- gbc.gridwidth = 2;
59- gbc.anchor = GridBagConstraints.WEST;
60- panel.add(new JLabel("<html><font color=red>The verification answer is guaranteed for<br/>the discrete semantics only (integer delays).</font></html>"), gbc);
61+ if (!model.isUntimed()) {
62+ gbc = new GridBagConstraints();
63+ gbc.gridx = 0;
64+ gbc.gridy = 11;
65+ gbc.gridwidth = 2;
66+ gbc.anchor = GridBagConstraints.WEST;
67+ panel.add(new JLabel("<html><font color=red>The verification answer is guaranteed for<br/>the discrete semantics only (integer delays).</font></html>"), gbc);
68+ }
69 }
70
71 return panel;
72
73=== modified file 'src/pipe/gui/RunVerificationBase.java'
74--- src/pipe/gui/RunVerificationBase.java 2021-09-24 09:34:48 +0000
75+++ src/pipe/gui/RunVerificationBase.java 2022-06-01 12:45:16 +0000
76@@ -1,6 +1,5 @@
77 package pipe.gui;
78
79-import java.io.File;
80 import java.util.concurrent.ExecutionException;
81
82 import javax.swing.*;
83@@ -220,7 +219,7 @@
84 }
85 firePropertyChange("state", StateValue.PENDING, StateValue.DONE);
86
87- if (showResult(result) && spinner != null) {
88+ if (showResult(result, model) && spinner != null) {
89 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);
90 KBoundAnalyzer optimizer = new KBoundAnalyzer(model, options.extraTokens(), modelChecker, new MessengerImpl(), spinner);
91 optimizer.analyze((VerifyTAPNOptions) options, true);
92@@ -242,5 +241,5 @@
93 });
94 }
95
96- protected abstract boolean showResult(VerificationResult<TAPNNetworkTrace> result);
97+ protected abstract boolean showResult(VerificationResult<TAPNNetworkTrace> result, TimedArcPetriNetNetwork model);
98 }

Subscribers

People subscribed via source and target branches