TAPAAL

Merge lp:~tapaal-contributor/tapaal/bug-948502-discrete-incl-wrong-answer into lp:tapaal

  1. bug-948502-discrete-incl-wrong-answer
  2. Merge into trunk
Proposed by Jiri Srba
Status: Merged
Approved by: Jiri Srba
Approved revision: 683
Merged at revision: 683
Proposed branch: lp:~tapaal-contributor/tapaal/bug-948502-discrete-incl-wrong-answer
Merge into: lp:tapaal
Diff against target: 252 lines (+60/-12)
10 files modified
src/dk/aau/cs/io/ResourceManager.java (+5/-0)
src/dk/aau/cs/verification/IconSelector.java (+2/-1)
src/dk/aau/cs/verification/QueryResult.java (+7/-1)
src/dk/aau/cs/verification/UPPAAL/VerifytaOutputParser.java (+5/-2)
src/dk/aau/cs/verification/VerificationResult.java (+9/-0)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java (+6/-5)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java (+2/-2)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOutputParser.java (+4/-1)
src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java (+8/-0)
src/pipe/dataLayer/TAPNQuery.java (+12/-0)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/bug-948502-discrete-incl-wrong-answer
Reviewer Review Type Date Requested Status
Kenneth Yrke Jørgensen code Approve
Jiri Srba Approve
Review via email: mp+96924@code.launchpad.net

Commit message

Fixes Bug #948502 but answering "Inconclusive verification result" for the cases where discrete inclusion is used for
unbounded nets on queries that do not have any trace.

Description of the change

Fixes a wrong verification answer of discrete inclusion for unbounded nets.
It should now behave as follows:

1. unsatisfeid EF query for unbounded net with discrete inclusion is reported as "Inconclusive answer"

2. satisfied AG query for unbounded net with discrete inclusion is also reported as "Inconclusive answer"

This was fixed both in the standard query dialog and batch processing.

To post a comment you must log in.
Revision history for this message
Jiri Srba (srba) :
review: Approve
Revision history for this message
Kenneth Yrke Jørgensen (yrke) :
review: Approve (code)

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
1=== modified file 'src/dk/aau/cs/io/ResourceManager.java'
2--- src/dk/aau/cs/io/ResourceManager.java 2011-06-23 12:10:48 +0000
3+++ src/dk/aau/cs/io/ResourceManager.java 2012-03-11 17:12:23 +0000
4@@ -12,6 +12,7 @@
5 private static ImageIcon satisfiedIcon = loadIcon("satisfied.png");
6 private static ImageIcon notSatisfiedIcon = loadIcon("notsatisfied.png");
7 private static ImageIcon inconclusiveIcon = loadIcon("maybe1.png");
8+ private static ImageIcon rerunIcon = loadIcon("maybe.png");
9 private static ImageIcon infoIcon = loadIcon("info.png");
10 private static ImageIcon appIcon = loadIcon("tapaal-2.0.png");
11
12@@ -38,6 +39,10 @@
13 return inconclusiveIcon;
14 }
15
16+ public static ImageIcon rerunIcon(){
17+ return rerunIcon;
18+ }
19+
20 public static ImageIcon infoIcon(){
21 return infoIcon;
22 }
23
24=== modified file 'src/dk/aau/cs/verification/IconSelector.java'
25--- src/dk/aau/cs/verification/IconSelector.java 2011-06-11 14:03:45 +0000
26+++ src/dk/aau/cs/verification/IconSelector.java 2012-03-11 17:12:23 +0000
27@@ -8,6 +8,7 @@
28 protected static ImageIcon satisfiedIcon = ResourceManager.satisfiedIcon();
29 protected static ImageIcon notSatisfiedIcon = ResourceManager.notSatisfiedIcon();
30 protected static ImageIcon inconclusiveIcon = ResourceManager.inconclusiveIcon();
31-
32+ protected static ImageIcon rerunIcon = ResourceManager.rerunIcon();
33+
34 public abstract ImageIcon getIconFor(QueryResult result);
35 }
36\ No newline at end of file
37
38=== modified file 'src/dk/aau/cs/verification/QueryResult.java'
39--- src/dk/aau/cs/verification/QueryResult.java 2011-05-22 13:00:57 +0000
40+++ src/dk/aau/cs/verification/QueryResult.java 2012-03-11 17:12:23 +0000
41@@ -4,19 +4,25 @@
42
43 public class QueryResult {
44 private boolean satisfied = false;
45+ private boolean discreteInclusion = false;
46 protected QueryType queryType;
47 private BoundednessAnalysisResult boundednessAnalysis;
48
49- public QueryResult(boolean satisfied, BoundednessAnalysisResult boundednessAnalysis, QueryType queryType){
50+ public QueryResult(boolean satisfied, BoundednessAnalysisResult boundednessAnalysis, QueryType queryType, boolean discreteInclusion){
51 this.satisfied = satisfied;
52 this.boundednessAnalysis = boundednessAnalysis;
53 this.queryType = queryType;
54+ this.discreteInclusion = discreteInclusion;
55 }
56
57 public boolean isQuerySatisfied() {
58 return satisfied;
59 }
60
61+ public boolean isDiscreteIncludion() {
62+ return discreteInclusion;
63+ }
64+
65 @Override
66 public String toString() {
67 StringBuffer buffer = new StringBuffer( "Property is ");
68
69=== modified file 'src/dk/aau/cs/verification/UPPAAL/VerifytaOutputParser.java'
70--- src/dk/aau/cs/verification/UPPAAL/VerifytaOutputParser.java 2011-05-22 13:00:57 +0000
71+++ src/dk/aau/cs/verification/UPPAAL/VerifytaOutputParser.java 2012-03-11 17:12:23 +0000
72@@ -7,7 +7,9 @@
73 public class VerifytaOutputParser {
74 private static final String PROPERTY_IS_NOT_SATISFIED_STRING = "Property is NOT satisfied";
75 private static final String PROPERTY_IS_SATISFIED_STRING = "Property is satisfied";
76+ private static final String DISCRETE_INCLUSION = "discrete inclusion";
77 private boolean error = false;
78+ private boolean discreteInclusion = false;
79 private QueryType queryType;
80
81 public VerifytaOutputParser(QueryType queryType){
82@@ -23,10 +25,11 @@
83 try {
84 for (int i = 0; i < lines.length; i++) {
85 String line = lines[i];
86+ if (line.contains(DISCRETE_INCLUSION)) { discreteInclusion = true;}
87 if (line.contains(PROPERTY_IS_SATISFIED_STRING)) {
88- return new QueryResult(true, new InconclusiveBoundednessAnalysisResult(), queryType);
89+ return new QueryResult(true, new InconclusiveBoundednessAnalysisResult(), queryType, discreteInclusion);
90 } else if (line.contains(PROPERTY_IS_NOT_SATISFIED_STRING)) {
91- return new QueryResult(false, new InconclusiveBoundednessAnalysisResult(), queryType);
92+ return new QueryResult(false, new InconclusiveBoundednessAnalysisResult(), queryType, discreteInclusion);
93 }
94 }
95 } catch (Exception e) {
96
97=== modified file 'src/dk/aau/cs/verification/VerificationResult.java'
98--- src/dk/aau/cs/verification/VerificationResult.java 2011-09-23 21:23:31 +0000
99+++ src/dk/aau/cs/verification/VerificationResult.java 2012-03-11 17:12:23 +0000
100@@ -60,7 +60,16 @@
101 return stats.toString();
102 }
103
104+ public boolean isBounded() {
105+ return queryResult.boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded);
106+ }
107+
108 public String getResultString() {
109+ if (queryResult.isDiscreteIncludion() && !queryResult.boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded) &&
110+ ((!queryResult.isQuerySatisfied() && queryResult.queryType.equals(QueryType.EF)
111+ ||
112+ (queryResult.isQuerySatisfied() && queryResult.queryType.equals(QueryType.AG)))))
113+ {return "Verification is inconclusive.\nDisable discrete inclusion or add extra tokens and try again."; }
114 return queryResult.toString();
115 }
116 }
117
118=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java'
119--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java 2012-02-23 15:48:30 +0000
120+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java 2012-03-11 17:12:23 +0000
121@@ -134,7 +134,7 @@
122
123 File file = new File(getPath());
124 if(!file.canExecute()){
125- messenger.displayErrorMessage("The program can not be verified as being verifytapn.\n"
126+ messenger.displayErrorMessage("The engine verifytapn is not executable.\n"
127 + "The verifytapn path will be reset. Please try again, "
128 + "to manually set the verifytapn path.", "Verifytapn Error");
129 resetVerifytapn();
130@@ -349,10 +349,11 @@
131 return true;
132 }
133
134- private boolean isQueryUpwardClosed(TAPNQuery query) {
135- UpwardsClosedVisitor visitor = new UpwardsClosedVisitor();
136- return visitor.isUpwardClosed(query.getProperty());
137- }
138+ // JS: this is not used any more
139+ //private boolean isQueryUpwardClosed(TAPNQuery query) {
140+ // UpwardsClosedVisitor visitor = new UpwardsClosedVisitor();
141+ // return visitor.isUpwardClosed(query.getProperty());
142+ //}
143
144 public static void reset() {
145 verifytapnpath = "";
146
147=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java'
148--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java 2011-05-22 13:00:57 +0000
149+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java 2012-03-11 17:12:23 +0000
150@@ -27,7 +27,7 @@
151 return null;
152 }
153
154- return inconclusiveIcon;
155+ if (result.isDiscreteIncludion()) {return rerunIcon;}
156+ else { return inconclusiveIcon;}
157 }
158-
159 }
160
161=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOutputParser.java'
162--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOutputParser.java 2011-10-08 17:27:08 +0000
163+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOutputParser.java 2012-03-11 17:12:23 +0000
164@@ -12,6 +12,7 @@
165 public class VerifyTAPNOutputParser {
166 private static final String Query_IS_NOT_SATISFIED_STRING = "Query is NOT satisfied";
167 private static final String Query_IS_SATISFIED_STRING = "Query is satisfied";
168+ private static final String DISCRETE_INCLUSION = "discrete inclusion";
169
170 private static final Pattern discoveredPattern = Pattern.compile("\\s*discovered markings:\\s*(\\d+)\\s*");
171 private static final Pattern exploredPattern = Pattern.compile("\\s*explored markings:\\s*(\\d+)\\s*");
172@@ -34,10 +35,12 @@
173 boolean result = false;
174 int maxUsedTokens = 0;
175 boolean foundResult = false;
176+ boolean discreteInclusion = false;
177 String[] lines = output.split(System.getProperty("line.separator"));
178 try {
179 for (int i = 0; i < lines.length; i++) {
180 String line = lines[i];
181+ if (line.contains(DISCRETE_INCLUSION)) { discreteInclusion = true; }
182 if (line.contains(Query_IS_SATISFIED_STRING)) {
183 result = true;
184 foundResult = true;
185@@ -72,7 +75,7 @@
186 if(!foundResult) return null;
187
188 BoundednessAnalysisResult boundedAnalysis = new BoundednessAnalysisResult(totalTokens, maxUsedTokens, extraTokens);
189- return new Tuple<QueryResult, Stats>(new QueryResult(result, boundedAnalysis, queryType), new Stats(discovered, explored, stored));
190+ return new Tuple<QueryResult, Stats>(new QueryResult(result, boundedAnalysis, queryType, discreteInclusion), new Stats(discovered, explored, stored));
191 } catch (Exception e) {
192 e.printStackTrace();
193 }
194
195=== modified file 'src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java'
196--- src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java 2012-03-01 08:40:30 +0000
197+++ src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java 2012-03-11 17:12:23 +0000
198@@ -28,9 +28,12 @@
199 import dk.aau.cs.util.Tuple;
200 import dk.aau.cs.util.UnsupportedModelException;
201 import dk.aau.cs.util.UnsupportedQueryException;
202+import dk.aau.cs.verification.Boundedness;
203 import dk.aau.cs.verification.ModelChecker;
204 import dk.aau.cs.verification.NameMapping;
205 import dk.aau.cs.verification.NullStats;
206+import dk.aau.cs.verification.QueryResult;
207+import dk.aau.cs.verification.QueryType;
208 import dk.aau.cs.verification.Stats;
209 import dk.aau.cs.verification.TAPNComposer;
210 import dk.aau.cs.verification.VerificationOptions;
211@@ -226,6 +229,11 @@
212 timeoutCurrentVerification = false;
213 } else if(!verificationResult.error()) {
214 String queryResult = verificationResult.getQueryResult().isQuerySatisfied() ? "Satisfied" : "Not Satisfied";
215+ if (query.discreteInclusion() && !verificationResult.isBounded() &&
216+ ((query.queryType().equals(QueryType.EF) && !verificationResult.getQueryResult().isQuerySatisfied())
217+ ||
218+ (query.queryType().equals(QueryType.AG) && verificationResult.getQueryResult().isQuerySatisfied())))
219+ {queryResult = "Inconclusive answer";}
220 publishResult(file.getName(), query, queryResult, verificationResult.verificationTime(), verificationResult.stats());
221 } else {
222 publishResult(file.getName(), query, "Error during verification", verificationResult.verificationTime(), new NullStats());
223
224=== modified file 'src/pipe/dataLayer/TAPNQuery.java'
225--- src/pipe/dataLayer/TAPNQuery.java 2011-09-23 21:23:31 +0000
226+++ src/pipe/dataLayer/TAPNQuery.java 2012-03-11 17:12:23 +0000
227@@ -1,8 +1,12 @@
228 package pipe.dataLayer;
229
230 import pipe.gui.widgets.InclusionPlaces;
231+import dk.aau.cs.TCTL.TCTLAFNode;
232 import dk.aau.cs.TCTL.TCTLAbstractProperty;
233+import dk.aau.cs.TCTL.TCTLEFNode;
234+import dk.aau.cs.TCTL.TCTLEGNode;
235 import dk.aau.cs.translations.ReductionOption;
236+import dk.aau.cs.verification.QueryType;
237
238 public class TAPNQuery {
239 public enum TraceOption {
240@@ -225,4 +229,12 @@
241
242 return copy;
243 }
244+
245+ public QueryType queryType(){
246+ if(property instanceof TCTLEFNode) return QueryType.EF;
247+ else if(property instanceof TCTLEGNode) return QueryType.EG;
248+ else if(property instanceof TCTLAFNode) return QueryType.AF;
249+ else return QueryType.AG;
250+ }
251+
252 }

Subscribers

People subscribed via source and target branches