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
=== modified file 'src/dk/aau/cs/io/ResourceManager.java'
--- src/dk/aau/cs/io/ResourceManager.java 2011-06-23 12:10:48 +0000
+++ src/dk/aau/cs/io/ResourceManager.java 2012-03-11 17:12:23 +0000
@@ -12,6 +12,7 @@
12 private static ImageIcon satisfiedIcon = loadIcon("satisfied.png");12 private static ImageIcon satisfiedIcon = loadIcon("satisfied.png");
13 private static ImageIcon notSatisfiedIcon = loadIcon("notsatisfied.png");13 private static ImageIcon notSatisfiedIcon = loadIcon("notsatisfied.png");
14 private static ImageIcon inconclusiveIcon = loadIcon("maybe1.png");14 private static ImageIcon inconclusiveIcon = loadIcon("maybe1.png");
15 private static ImageIcon rerunIcon = loadIcon("maybe.png");
15 private static ImageIcon infoIcon = loadIcon("info.png");16 private static ImageIcon infoIcon = loadIcon("info.png");
16 private static ImageIcon appIcon = loadIcon("tapaal-2.0.png");17 private static ImageIcon appIcon = loadIcon("tapaal-2.0.png");
17 18
@@ -38,6 +39,10 @@
38 return inconclusiveIcon;39 return inconclusiveIcon;
39 }40 }
40 41
42 public static ImageIcon rerunIcon(){
43 return rerunIcon;
44 }
45
41 public static ImageIcon infoIcon(){46 public static ImageIcon infoIcon(){
42 return infoIcon;47 return infoIcon;
43 }48 }
4449
=== modified file 'src/dk/aau/cs/verification/IconSelector.java'
--- src/dk/aau/cs/verification/IconSelector.java 2011-06-11 14:03:45 +0000
+++ src/dk/aau/cs/verification/IconSelector.java 2012-03-11 17:12:23 +0000
@@ -8,6 +8,7 @@
8 protected static ImageIcon satisfiedIcon = ResourceManager.satisfiedIcon();8 protected static ImageIcon satisfiedIcon = ResourceManager.satisfiedIcon();
9 protected static ImageIcon notSatisfiedIcon = ResourceManager.notSatisfiedIcon();9 protected static ImageIcon notSatisfiedIcon = ResourceManager.notSatisfiedIcon();
10 protected static ImageIcon inconclusiveIcon = ResourceManager.inconclusiveIcon();10 protected static ImageIcon inconclusiveIcon = ResourceManager.inconclusiveIcon();
1111 protected static ImageIcon rerunIcon = ResourceManager.rerunIcon();
12
12 public abstract ImageIcon getIconFor(QueryResult result);13 public abstract ImageIcon getIconFor(QueryResult result);
13}14}
14\ No newline at end of file15\ No newline at end of file
1516
=== modified file 'src/dk/aau/cs/verification/QueryResult.java'
--- src/dk/aau/cs/verification/QueryResult.java 2011-05-22 13:00:57 +0000
+++ src/dk/aau/cs/verification/QueryResult.java 2012-03-11 17:12:23 +0000
@@ -4,19 +4,25 @@
44
5public class QueryResult {5public class QueryResult {
6 private boolean satisfied = false;6 private boolean satisfied = false;
7 private boolean discreteInclusion = false;
7 protected QueryType queryType;8 protected QueryType queryType;
8 private BoundednessAnalysisResult boundednessAnalysis;9 private BoundednessAnalysisResult boundednessAnalysis;
910
10 public QueryResult(boolean satisfied, BoundednessAnalysisResult boundednessAnalysis, QueryType queryType){11 public QueryResult(boolean satisfied, BoundednessAnalysisResult boundednessAnalysis, QueryType queryType, boolean discreteInclusion){
11 this.satisfied = satisfied;12 this.satisfied = satisfied;
12 this.boundednessAnalysis = boundednessAnalysis;13 this.boundednessAnalysis = boundednessAnalysis;
13 this.queryType = queryType;14 this.queryType = queryType;
15 this.discreteInclusion = discreteInclusion;
14 }16 }
15 17
16 public boolean isQuerySatisfied() {18 public boolean isQuerySatisfied() {
17 return satisfied;19 return satisfied;
18 }20 }
19 21
22 public boolean isDiscreteIncludion() {
23 return discreteInclusion;
24 }
25
20 @Override26 @Override
21 public String toString() {27 public String toString() {
22 StringBuffer buffer = new StringBuffer( "Property is ");28 StringBuffer buffer = new StringBuffer( "Property is ");
2329
=== modified file 'src/dk/aau/cs/verification/UPPAAL/VerifytaOutputParser.java'
--- src/dk/aau/cs/verification/UPPAAL/VerifytaOutputParser.java 2011-05-22 13:00:57 +0000
+++ src/dk/aau/cs/verification/UPPAAL/VerifytaOutputParser.java 2012-03-11 17:12:23 +0000
@@ -7,7 +7,9 @@
7public class VerifytaOutputParser {7public class VerifytaOutputParser {
8 private static final String PROPERTY_IS_NOT_SATISFIED_STRING = "Property is NOT satisfied";8 private static final String PROPERTY_IS_NOT_SATISFIED_STRING = "Property is NOT satisfied";
9 private static final String PROPERTY_IS_SATISFIED_STRING = "Property is satisfied";9 private static final String PROPERTY_IS_SATISFIED_STRING = "Property is satisfied";
10 private static final String DISCRETE_INCLUSION = "discrete inclusion";
10 private boolean error = false;11 private boolean error = false;
12 private boolean discreteInclusion = false;
11 private QueryType queryType;13 private QueryType queryType;
1214
13 public VerifytaOutputParser(QueryType queryType){15 public VerifytaOutputParser(QueryType queryType){
@@ -23,10 +25,11 @@
23 try {25 try {
24 for (int i = 0; i < lines.length; i++) {26 for (int i = 0; i < lines.length; i++) {
25 String line = lines[i];27 String line = lines[i];
28 if (line.contains(DISCRETE_INCLUSION)) { discreteInclusion = true;}
26 if (line.contains(PROPERTY_IS_SATISFIED_STRING)) {29 if (line.contains(PROPERTY_IS_SATISFIED_STRING)) {
27 return new QueryResult(true, new InconclusiveBoundednessAnalysisResult(), queryType);30 return new QueryResult(true, new InconclusiveBoundednessAnalysisResult(), queryType, discreteInclusion);
28 } else if (line.contains(PROPERTY_IS_NOT_SATISFIED_STRING)) {31 } else if (line.contains(PROPERTY_IS_NOT_SATISFIED_STRING)) {
29 return new QueryResult(false, new InconclusiveBoundednessAnalysisResult(), queryType);32 return new QueryResult(false, new InconclusiveBoundednessAnalysisResult(), queryType, discreteInclusion);
30 }33 }
31 }34 }
32 } catch (Exception e) {35 } catch (Exception e) {
3336
=== modified file 'src/dk/aau/cs/verification/VerificationResult.java'
--- src/dk/aau/cs/verification/VerificationResult.java 2011-09-23 21:23:31 +0000
+++ src/dk/aau/cs/verification/VerificationResult.java 2012-03-11 17:12:23 +0000
@@ -60,7 +60,16 @@
60 return stats.toString();60 return stats.toString();
61 }61 }
6262
63 public boolean isBounded() {
64 return queryResult.boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded);
65 }
66
63 public String getResultString() {67 public String getResultString() {
68 if (queryResult.isDiscreteIncludion() && !queryResult.boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded) &&
69 ((!queryResult.isQuerySatisfied() && queryResult.queryType.equals(QueryType.EF)
70 ||
71 (queryResult.isQuerySatisfied() && queryResult.queryType.equals(QueryType.AG)))))
72 {return "Verification is inconclusive.\nDisable discrete inclusion or add extra tokens and try again."; }
64 return queryResult.toString();73 return queryResult.toString();
65 }74 }
66}75}
6776
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java 2012-02-23 15:48:30 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPN.java 2012-03-11 17:12:23 +0000
@@ -134,7 +134,7 @@
134 134
135 File file = new File(getPath());135 File file = new File(getPath());
136 if(!file.canExecute()){136 if(!file.canExecute()){
137 messenger.displayErrorMessage("The program can not be verified as being verifytapn.\n"137 messenger.displayErrorMessage("The engine verifytapn is not executable.\n"
138 + "The verifytapn path will be reset. Please try again, "138 + "The verifytapn path will be reset. Please try again, "
139 + "to manually set the verifytapn path.", "Verifytapn Error");139 + "to manually set the verifytapn path.", "Verifytapn Error");
140 resetVerifytapn();140 resetVerifytapn();
@@ -349,10 +349,11 @@
349 return true;349 return true;
350 }350 }
351 351
352 private boolean isQueryUpwardClosed(TAPNQuery query) {352 // JS: this is not used any more
353 UpwardsClosedVisitor visitor = new UpwardsClosedVisitor();353 //private boolean isQueryUpwardClosed(TAPNQuery query) {
354 return visitor.isUpwardClosed(query.getProperty());354 // UpwardsClosedVisitor visitor = new UpwardsClosedVisitor();
355 }355 // return visitor.isUpwardClosed(query.getProperty());
356 //}
356357
357 public static void reset() {358 public static void reset() {
358 verifytapnpath = "";359 verifytapnpath = "";
359360
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java 2011-05-22 13:00:57 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java 2012-03-11 17:12:23 +0000
@@ -27,7 +27,7 @@
27 return null;27 return null;
28 }28 }
29 29
30 return inconclusiveIcon;30 if (result.isDiscreteIncludion()) {return rerunIcon;}
31 else { return inconclusiveIcon;}
31 }32 }
32
33}33}
3434
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOutputParser.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOutputParser.java 2011-10-08 17:27:08 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNOutputParser.java 2012-03-11 17:12:23 +0000
@@ -12,6 +12,7 @@
12public class VerifyTAPNOutputParser {12public class VerifyTAPNOutputParser {
13 private static final String Query_IS_NOT_SATISFIED_STRING = "Query is NOT satisfied";13 private static final String Query_IS_NOT_SATISFIED_STRING = "Query is NOT satisfied";
14 private static final String Query_IS_SATISFIED_STRING = "Query is satisfied";14 private static final String Query_IS_SATISFIED_STRING = "Query is satisfied";
15 private static final String DISCRETE_INCLUSION = "discrete inclusion";
1516
16 private static final Pattern discoveredPattern = Pattern.compile("\\s*discovered markings:\\s*(\\d+)\\s*");17 private static final Pattern discoveredPattern = Pattern.compile("\\s*discovered markings:\\s*(\\d+)\\s*");
17 private static final Pattern exploredPattern = Pattern.compile("\\s*explored markings:\\s*(\\d+)\\s*");18 private static final Pattern exploredPattern = Pattern.compile("\\s*explored markings:\\s*(\\d+)\\s*");
@@ -34,10 +35,12 @@
34 boolean result = false;35 boolean result = false;
35 int maxUsedTokens = 0;36 int maxUsedTokens = 0;
36 boolean foundResult = false;37 boolean foundResult = false;
38 boolean discreteInclusion = false;
37 String[] lines = output.split(System.getProperty("line.separator"));39 String[] lines = output.split(System.getProperty("line.separator"));
38 try {40 try {
39 for (int i = 0; i < lines.length; i++) {41 for (int i = 0; i < lines.length; i++) {
40 String line = lines[i];42 String line = lines[i];
43 if (line.contains(DISCRETE_INCLUSION)) { discreteInclusion = true; }
41 if (line.contains(Query_IS_SATISFIED_STRING)) {44 if (line.contains(Query_IS_SATISFIED_STRING)) {
42 result = true;45 result = true;
43 foundResult = true;46 foundResult = true;
@@ -72,7 +75,7 @@
72 if(!foundResult) return null;75 if(!foundResult) return null;
73 76
74 BoundednessAnalysisResult boundedAnalysis = new BoundednessAnalysisResult(totalTokens, maxUsedTokens, extraTokens);77 BoundednessAnalysisResult boundedAnalysis = new BoundednessAnalysisResult(totalTokens, maxUsedTokens, extraTokens);
75 return new Tuple<QueryResult, Stats>(new QueryResult(result, boundedAnalysis, queryType), new Stats(discovered, explored, stored));78 return new Tuple<QueryResult, Stats>(new QueryResult(result, boundedAnalysis, queryType, discreteInclusion), new Stats(discovered, explored, stored));
76 } catch (Exception e) {79 } catch (Exception e) {
77 e.printStackTrace();80 e.printStackTrace();
78 }81 }
7982
=== modified file 'src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java'
--- src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java 2012-03-01 08:40:30 +0000
+++ src/dk/aau/cs/verification/batchProcessing/BatchProcessingWorker.java 2012-03-11 17:12:23 +0000
@@ -28,9 +28,12 @@
28import dk.aau.cs.util.Tuple;28import dk.aau.cs.util.Tuple;
29import dk.aau.cs.util.UnsupportedModelException;29import dk.aau.cs.util.UnsupportedModelException;
30import dk.aau.cs.util.UnsupportedQueryException;30import dk.aau.cs.util.UnsupportedQueryException;
31import dk.aau.cs.verification.Boundedness;
31import dk.aau.cs.verification.ModelChecker;32import dk.aau.cs.verification.ModelChecker;
32import dk.aau.cs.verification.NameMapping;33import dk.aau.cs.verification.NameMapping;
33import dk.aau.cs.verification.NullStats;34import dk.aau.cs.verification.NullStats;
35import dk.aau.cs.verification.QueryResult;
36import dk.aau.cs.verification.QueryType;
34import dk.aau.cs.verification.Stats;37import dk.aau.cs.verification.Stats;
35import dk.aau.cs.verification.TAPNComposer;38import dk.aau.cs.verification.TAPNComposer;
36import dk.aau.cs.verification.VerificationOptions;39import dk.aau.cs.verification.VerificationOptions;
@@ -226,6 +229,11 @@
226 timeoutCurrentVerification = false;229 timeoutCurrentVerification = false;
227 } else if(!verificationResult.error()) {230 } else if(!verificationResult.error()) {
228 String queryResult = verificationResult.getQueryResult().isQuerySatisfied() ? "Satisfied" : "Not Satisfied";231 String queryResult = verificationResult.getQueryResult().isQuerySatisfied() ? "Satisfied" : "Not Satisfied";
232 if (query.discreteInclusion() && !verificationResult.isBounded() &&
233 ((query.queryType().equals(QueryType.EF) && !verificationResult.getQueryResult().isQuerySatisfied())
234 ||
235 (query.queryType().equals(QueryType.AG) && verificationResult.getQueryResult().isQuerySatisfied())))
236 {queryResult = "Inconclusive answer";}
229 publishResult(file.getName(), query, queryResult, verificationResult.verificationTime(), verificationResult.stats());237 publishResult(file.getName(), query, queryResult, verificationResult.verificationTime(), verificationResult.stats());
230 } else {238 } else {
231 publishResult(file.getName(), query, "Error during verification", verificationResult.verificationTime(), new NullStats());239 publishResult(file.getName(), query, "Error during verification", verificationResult.verificationTime(), new NullStats());
232240
=== modified file 'src/pipe/dataLayer/TAPNQuery.java'
--- src/pipe/dataLayer/TAPNQuery.java 2011-09-23 21:23:31 +0000
+++ src/pipe/dataLayer/TAPNQuery.java 2012-03-11 17:12:23 +0000
@@ -1,8 +1,12 @@
1package pipe.dataLayer;1package pipe.dataLayer;
22
3import pipe.gui.widgets.InclusionPlaces;3import pipe.gui.widgets.InclusionPlaces;
4import dk.aau.cs.TCTL.TCTLAFNode;
4import dk.aau.cs.TCTL.TCTLAbstractProperty;5import dk.aau.cs.TCTL.TCTLAbstractProperty;
6import dk.aau.cs.TCTL.TCTLEFNode;
7import dk.aau.cs.TCTL.TCTLEGNode;
5import dk.aau.cs.translations.ReductionOption;8import dk.aau.cs.translations.ReductionOption;
9import dk.aau.cs.verification.QueryType;
610
7public class TAPNQuery {11public class TAPNQuery {
8 public enum TraceOption {12 public enum TraceOption {
@@ -225,4 +229,12 @@
225 229
226 return copy;230 return copy;
227 }231 }
232
233 public QueryType queryType(){
234 if(property instanceof TCTLEFNode) return QueryType.EF;
235 else if(property instanceof TCTLEGNode) return QueryType.EG;
236 else if(property instanceof TCTLAFNode) return QueryType.AF;
237 else return QueryType.AG;
238 }
239
228}240}

Subscribers

People subscribed via source and target branches