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
1=== modified file 'src/dk/aau/cs/verification/QueryResult.java'
2--- src/dk/aau/cs/verification/QueryResult.java 2012-08-01 08:57:31 +0000
3+++ src/dk/aau/cs/verification/QueryResult.java 2012-08-01 11:11:21 +0000
4@@ -36,8 +36,8 @@
5
6 private boolean shouldAddExplanation() {
7 return (queryType.equals(QueryType.EF) && !isQuerySatisfied())
8- || (queryType.equals(QueryType.EG) && !isQuerySatisfied())
9- || (queryType.equals(QueryType.AF) && isQuerySatisfied())
10+ || (queryType.equals(QueryType.EG)) // && !isQuerySatisfied())
11+ || (queryType.equals(QueryType.AF)) // && isQuerySatisfied())
12 || (queryType.equals(QueryType.AG) && isQuerySatisfied());
13 }
14
15
16=== modified file 'src/dk/aau/cs/verification/UPPAAL/UppaalIconSelector.java'
17--- src/dk/aau/cs/verification/UPPAAL/UppaalIconSelector.java 2011-05-22 13:00:57 +0000
18+++ src/dk/aau/cs/verification/UPPAAL/UppaalIconSelector.java 2012-08-01 11:11:21 +0000
19@@ -12,18 +12,19 @@
20 public ImageIcon getIconFor(QueryResult result){
21 switch(result.queryType())
22 {
23- case AF:
24 case EF:
25 if(result.isQuerySatisfied()) return satisfiedIcon;
26 break;
27- case EG:
28 case AG:
29 if(!result.isQuerySatisfied()) return notSatisfiedIcon;
30 break;
31+ case AF: return inconclusiveIcon;
32+ case EG: return inconclusiveIcon;
33 default:
34 return null;
35 }
36+
37+ return inconclusiveIcon;
38
39- return inconclusiveIcon;
40 }
41 }
42
43=== modified file 'src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java'
44--- src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java 2012-07-11 13:36:33 +0000
45+++ src/dk/aau/cs/verification/VerifyTAPN/VerifyTAPNIconSelector.java 2012-08-01 11:11:21 +0000
46@@ -24,14 +24,14 @@
47 else if(result.isQuerySatisfied() && result.boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) return satisfiedIcon;
48 break;
49 case AF:
50- if(!result.isQuerySatisfied()){
51+ if(!result.isQuerySatisfied() && result.boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)){
52 return notSatisfiedIcon;
53 } else if(result.isQuerySatisfied() && result.boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)){
54 return satisfiedIcon;
55 }
56 break;
57 case EG:
58- if(result.isQuerySatisfied()) return satisfiedIcon;
59+ if(result.isQuerySatisfied() && result.boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) return satisfiedIcon;
60 else if(!result.isQuerySatisfied() && result.boundednessAnalysis().boundednessResult().equals(Boundedness.Bounded)) return notSatisfiedIcon;
61 break;
62 default:

Subscribers

People subscribed via source and target branches