Merge lp:~verifydtapn-contributers/verifydtapn/NoLivenessGCD into lp:verifydtapn

Proposed by Peter Gjøl Jensen
Status: Merged
Approved by: Jiri Srba
Approved revision: 299
Merged at revision: 294
Proposed branch: lp:~verifydtapn-contributers/verifydtapn/NoLivenessGCD
Merge into: lp:verifydtapn
Diff against target: 47 lines (+20/-8)
1 file modified
src/DiscreteVerification/DiscreteVerification.cpp (+20/-8)
To merge this branch: bzr merge lp:~verifydtapn-contributers/verifydtapn/NoLivenessGCD
Reviewer Review Type Date Requested Status
Jiri Srba Approve
Mathias Grund Sørensen code Approve
Jakob Taankvist Pending
Review via email: mp+206810@code.launchpad.net

Description of the change

Added checks for
GCD + liveness
GCD + deadlock in query

Engine ouputs error message and exits if any of above.

To post a comment you must log in.
295. By Peter Gjøl Jensen

added missing checks

Revision history for this message
Mathias Grund Sørensen (mathias.grund) wrote :

Appears to be a lot of checks for the same thing; must be possible to make the test just once?

Also, if this is easier, you could consider storing the string in a variable rather than copy-paste.

I'll approve as this is only for improved readability.

review: Approve (code)
296. By Peter Gjøl Jensen

refactored; improved code quality of GCD checks

297. By Peter Gjøl Jensen

readded deadlock + liveness check

Revision history for this message
Jiri Srba (srba) wrote :

Why did this error message was removed?

 "The combination of TimeDarts, Deadlock proposition and EG or AF queries is currently not supported"

review: Needs Information
Revision history for this message
Peter Gjøl Jensen (peter-gjoel) wrote :

I agree, I moved the checks to one single check.
I did not move the strings to constants as this is (currently) not the convention inside the engine.

Revision history for this message
Peter Gjøl Jensen (peter-gjoel) wrote :

> Why did this error message was removed?
>
> "The combination of TimeDarts, Deadlock proposition and EG or AF queries is
> currently not supported"

I was to fast on the push, it has been re-added.

Revision history for this message
Jiri Srba (srba) wrote :

Should not the if condition that at the same time the query contains deadlocks?

 if(query->getQuantifier() == EG || query->getQuantifier() == AF){
21 + cout << "Lowering constants by greatest common divisor gives wrong answer for EG and AF queries" << endl;
22 + exit(1);
23 + }

review: Needs Information
298. By Peter Gjøl Jensen

added missing check

Revision history for this message
Peter Gjøl Jensen (peter-gjoel) wrote :

Line 16
if(containsDeadlock.value && options.getDisableGCDLowerGuards() == false)

does the check if we have deadlocks and do GCD lowering

Line 20
 if((query->getQuantifier() == EG || query->getQuantifier() == AF) && options.getDisableGCDLowerGuards() == false)

checks if liveness and and GCD

Revision history for this message
Jiri Srba (srba) wrote :

OK, gives sense to me now. Can you replace "gives wrong answer" with "is unsound"?
There are two occurences.

review: Needs Fixing
299. By Peter Gjøl Jensen

changed error text

Revision history for this message
Peter Gjøl Jensen (peter-gjoel) wrote :

Should be as requested now.

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/DiscreteVerification/DiscreteVerification.cpp'
2--- src/DiscreteVerification/DiscreteVerification.cpp 2013-12-05 13:23:21 +0000
3+++ src/DiscreteVerification/DiscreteVerification.cpp 2014-02-17 21:34:43 +0000
4@@ -89,10 +89,26 @@
5 }
6
7 delete strategy;
8+ return 0;
9+ }
10+
11+
12+ // asume that we dont reach here except if we are doing normal verification
13+ AST::BoolResult containsDeadlock;
14+ DeadlockVisitor deadlockVisitor = DeadlockVisitor();
15+ deadlockVisitor.visit(*query, containsDeadlock);
16+ if(containsDeadlock.value && options.getDisableGCDLowerGuards() == false){
17+ cout << "Lowering constants by greatest common divisor is unsound for queries containing the deadlock proposition" << endl;
18+ exit(1);
19+ }
20+ if((query->getQuantifier() == EG || query->getQuantifier() == AF) && options.getDisableGCDLowerGuards() == false){
21+ cout << "Lowering constants by greatest common divisor is unsound for EG and AF queries" << endl;
22+ exit(1);
23+ }
24+
25+
26+ if (options.getVerificationType() == VerificationOptions::DISCRETE) {
27
28- }
29- else if (options.getVerificationType() == VerificationOptions::DISCRETE) {
30-
31 if (options.getMemoryOptimization() == VerificationOptions::PTRIE) {
32 //TODO fix initialization
33 WaitingList<EncodingPointer<MetaData> >* strategy = getWaitingList<EncodingPointer<MetaData> > (query, options);
34@@ -132,12 +148,8 @@
35 }
36 delete strategy;
37 }
38- } else if (options.getVerificationType() == VerificationOptions::TIMEDART) {
39+ } else if (options.getVerificationType() == VerificationOptions::TIMEDART) {
40 if (query->getQuantifier() == EG || query->getQuantifier() == AF) {
41- AST::BoolResult containsDeadlock;
42- DeadlockVisitor deadlockVisitor = DeadlockVisitor();
43- deadlockVisitor.visit(*query, containsDeadlock);
44-
45 if (containsDeadlock.value) {
46 std::cout << "The combination of TimeDarts, Deadlock proposition and EG or AF queries is currently not supported" << endl;
47 exit(1);

Subscribers

People subscribed via source and target branches