TAPAAL

Merge lp:~tapaal-contributor/tapaal/wrongVerificationAnswers-bug1031666 into lp:tapaal

  1. wrongVerificationAnswers-bug1031666
  2. Merge into trunk
Proposed by Jiri Srba
Status: Merged
Approved by: Jiri Srba
Approved revision: 727
Merged at revision: 726
Proposed branch: lp:~tapaal-contributor/tapaal/wrongVerificationAnswers-bug1031666
Merge into: lp:tapaal
Diff against target: 62 lines (+8/-7)
3 files modified
src/dk/aau/cs/verification/QueryResult.java (+2/-2)
src/dk/aau/cs/verification/UPPAAL/UppaalIconSelector.java (+4/-3)
src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java (+2/-2)
To merge this branch: bzr merge lp:~tapaal-contributor/tapaal/wrongVerificationAnswers-bug1031666
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Kenneth Yrke Jørgensen Approve
Review via email: mp+117610@code.launchpad.net

Commit message

Fixes wrong GUI interpretation of verification answer for EG and AF queries.
Fixes bug #1031666.

Description of the change

Fixes wrong GUI interpretation of verification answer for EG and AF queries.
Fixes bug #1031666.

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
Revision history for this message
Jiri Srba (srba) :
review: Needs Fixing
lp:~tapaal-contributor/tapaal/wrongVerificationAnswers-bug1031666 updated
727. By Jiri Srba

fixes a problem for IconSelector for UPPAAL model.

Revision history for this message
Jiri Srba (srba) :
review: Approve

Preview Diff

[H/L] Next/Prev Comment, [J/K] Next/Prev File, [N/P] Next/Prev Hunk
=== modified file 'src/dk/aau/cs/verification/QueryResult.java'
--- src/dk/aau/cs/verification/QueryResult.java 2012-08-01 08:57:31 +0000
+++ src/dk/aau/cs/verification/QueryResult.java 2012-08-01 11:11:21 +0000
@@ -36,8 +36,8 @@
36 36
37 private boolean shouldAddExplanation() {37 private boolean shouldAddExplanation() {
38 return (queryType.equals(QueryType.EF) && !isQuerySatisfied()) 38 return (queryType.equals(QueryType.EF) && !isQuerySatisfied())
39 || (queryType.equals(QueryType.EG) && !isQuerySatisfied()) 39 || (queryType.equals(QueryType.EG)) // && !isQuerySatisfied())
40 || (queryType.equals(QueryType.AF) && isQuerySatisfied())40 || (queryType.equals(QueryType.AF)) // && isQuerySatisfied())
41 || (queryType.equals(QueryType.AG) && isQuerySatisfied());41 || (queryType.equals(QueryType.AG) && isQuerySatisfied());
42 }42 }
43 43
4444
=== modified file 'src/dk/aau/cs/verification/UPPAAL/UppaalIconSelector.java'
--- src/dk/aau/cs/verification/UPPAAL/UppaalIconSelector.java 2011-05-22 13:00:57 +0000
+++ src/dk/aau/cs/verification/UPPAAL/UppaalIconSelector.java 2012-08-01 11:11:21 +0000
@@ -12,18 +12,19 @@
12 public ImageIcon getIconFor(QueryResult result){12 public ImageIcon getIconFor(QueryResult result){
13 switch(result.queryType())13 switch(result.queryType())
14 {14 {
15 case AF:
16 case EF:15 case EF:
17 if(result.isQuerySatisfied()) return satisfiedIcon;16 if(result.isQuerySatisfied()) return satisfiedIcon;
18 break;17 break;
19 case EG:
20 case AG:18 case AG:
21 if(!result.isQuerySatisfied()) return notSatisfiedIcon;19 if(!result.isQuerySatisfied()) return notSatisfiedIcon;
22 break;20 break;
21 case AF: return inconclusiveIcon;
22 case EG: return inconclusiveIcon;
23 default:23 default:
24 return null;24 return null;
25 }25 }
26
27 return inconclusiveIcon;
26 28
27 return inconclusiveIcon;
28 }29 }
29}30}
3031
=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java'
--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java 2012-07-11 13:36:33 +0000
+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java 2012-08-01 11:11:21 +0000
@@ -24,14 +24,14 @@
24 else if(result.isQuerySatisfied() && result.boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) return satisfiedIcon;24 else if(result.isQuerySatisfied() && result.boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) return satisfiedIcon;
25 break;25 break;
26 case AF:26 case AF:
27 if(!result.isQuerySatisfied()){27 if(!result.isQuerySatisfied() && result.boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)){
28 return notSatisfiedIcon;28 return notSatisfiedIcon;
29 } else if(result.isQuerySatisfied() && result.boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)){29 } else if(result.isQuerySatisfied() && result.boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)){
30 return satisfiedIcon;30 return satisfiedIcon;
31 }31 }
32 break;32 break;
33 case EG:33 case EG:
34 if(result.isQuerySatisfied()) return satisfiedIcon;34 if(result.isQuerySatisfied() && result.boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) return satisfiedIcon;
35 else if(!result.isQuerySatisfied() && result.boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) return notSatisfiedIcon;35 else if(!result.isQuerySatisfied() && result.boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) return notSatisfiedIcon;
36 break;36 break;
37 default:37 default:

Subscribers

People subscribed via source and target branches