TAPAAL

Merge lp:~tapaal-contributor/tapaal/boundedness-check-1944588 into lp:tapaal

  1. boundedness-check-1944588
  2. Merge into trunk
Proposed by Lena Ernstsen
Status: Merged
Approved by: Jiri Srba
Approved revision: 1145
Merged at revision: 1145
Proposed branch: lp:~tapaal-contributor/tapaal/boundedness-check-1944588
Merge into: lp:tapaal
Diff against target: 77 lines (+14/-7)
3 files modified
src/pipe/gui/KBoundAnalyzer.java (+3/-3)
src/pipe/gui/RunKBoundAnalysis.java (+10/-3)
src/pipe/gui/RunVerificationBase.java (+1/-1)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/boundedness-check-1944588
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Review via email: mp+409056@code.launchpad.net

Description of the change

Checks whether the boundedness check dialog is shown

To post a comment you must log in.
Revision history for this message
Jiri Srba (srba) wrote :

Tested and works.

review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/pipe/gui/KBoundAnalyzer.java'
2--- src/pipe/gui/KBoundAnalyzer.java 2021-08-25 10:07:04 +0000
3+++ src/pipe/gui/KBoundAnalyzer.java 2021-09-23 11:50:31 +0000
4@@ -45,10 +45,10 @@
5 }
6
7 public void analyze() {
8- analyze(verificationOptions());
9+ analyze(verificationOptions(), false);
10 }
11
12- public void analyze(VerifyTAPNOptions options) {
13+ public void analyze(VerifyTAPNOptions options, boolean resultShown) {
14 TAPNQuery query;
15 if (modelChecker instanceof VerifyPN) {
16 query = getPNBoundednessQuery();
17@@ -56,7 +56,7 @@
18 query = getBoundednessQuery();
19 }
20
21- RunKBoundAnalysis analyzer = new RunKBoundAnalysis(modelChecker, messenger, spinner);
22+ RunKBoundAnalysis analyzer = new RunKBoundAnalysis(modelChecker, messenger, spinner, resultShown);
23 RunningVerificationDialog dialog = new RunningVerificationDialog(CreateGui.getApp(), analyzer);
24
25 analyzer.execute(options, tapnNetwork, query, null);
26
27=== modified file 'src/pipe/gui/RunKBoundAnalysis.java'
28--- src/pipe/gui/RunKBoundAnalysis.java 2021-08-25 10:21:40 +0000
29+++ src/pipe/gui/RunKBoundAnalysis.java 2021-09-23 11:50:31 +0000
30@@ -16,10 +16,12 @@
31 public class RunKBoundAnalysis extends RunVerificationBase {
32
33 private final JSpinner spinner;
34+ private boolean resultShown;
35
36- public RunKBoundAnalysis(ModelChecker modelChecker, Messenger messenger,JSpinner spinner) {
37+ public RunKBoundAnalysis(ModelChecker modelChecker, Messenger messenger,JSpinner spinner, boolean resultShown) {
38 super(modelChecker, messenger, spinner);
39 this.spinner = spinner;
40+ this.resultShown = resultShown;
41 }
42
43 @Override
44@@ -30,13 +32,18 @@
45 getAnswerNotBoundedString(), "Analysis Result",
46 JOptionPane.INFORMATION_MESSAGE);
47 } else {
48- if (modelChecker instanceof VerifyPN && !result.getRawOutput().contains("max tokens:")) {
49+ if (modelChecker instanceof VerifyPN && !resultShown) {
50 Object[] options = {"Ok", "Minimize extra tokens"};
51 int answer = JOptionPane.showOptionDialog(CreateGui.getApp(),
52 getPNAnswerBoundedString(), "Analysis Result,",
53 JOptionPane.OK_CANCEL_OPTION, JOptionPane.INFORMATION_MESSAGE,
54 ResourceManager.satisfiedIcon(), options, JOptionPane.OK_OPTION);
55- return answer != JOptionPane.OK_OPTION;
56+
57+ if (answer != JOptionPane.OK_OPTION && result.getRawOutput().contains("max tokens:")) {
58+ spinner.setValue(result.getQueryResult().boundednessAnalysis().usedTokens() - result.getQueryResult().boundednessAnalysis().tokensInNet());
59+ } else {
60+ return answer != JOptionPane.OK_OPTION;
61+ }
62 } else if (modelChecker instanceof VerifyPN) {
63 spinner.setValue(result.getQueryResult().boundednessAnalysis().usedTokens() - result.getQueryResult().boundednessAnalysis().tokensInNet());
64 } else {
65
66=== modified file 'src/pipe/gui/RunVerificationBase.java'
67--- src/pipe/gui/RunVerificationBase.java 2021-08-25 10:11:18 +0000
68+++ src/pipe/gui/RunVerificationBase.java 2021-09-23 11:50:31 +0000
69@@ -221,7 +221,7 @@
70 if (showResult(result) && spinner != null) {
71 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);
72 KBoundAnalyzer optimizer = new KBoundAnalyzer(model, options.extraTokens(), modelChecker, new MessengerImpl(), spinner);
73- optimizer.analyze((VerifyTAPNOptions) options);
74+ optimizer.analyze((VerifyTAPNOptions) options, true);
75 }
76 } else {
77 modelChecker.kill();

Subscribers

People subscribed via source and target branches