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

[Peter Gjøl Jensen]

Added checks for
GCD + liveness
GCD + deadlock in query

Engine ouputs error message and exits if any of above.

[lp:~verifydtapn-contributers/verifydtapn/NoLivenessGCD]

295. By Peter Gjøl Jensen on 2014-02-17

added missing checks

[Mathias Grund Sørensen (mathias.grund)]

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)

[lp:~verifydtapn-contributers/verifydtapn/NoLivenessGCD]

296. By Peter Gjøl Jensen on 2014-02-17

refactored; improved code quality of GCD checks

297. By Peter Gjøl Jensen on 2014-02-17

readded deadlock + liveness check

[Jiri Srba (srba)]

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

[Peter Gjøl Jensen (peter-gjoel)]

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.

[Peter Gjøl Jensen (peter-gjoel)]

> 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.

[Jiri Srba (srba)]

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

[lp:~verifydtapn-contributers/verifydtapn/NoLivenessGCD]

298. By Peter Gjøl Jensen on 2014-02-17

added missing check

[Peter Gjøl Jensen (peter-gjoel)]

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

[Jiri Srba (srba)]

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

review: Needs Fixing

[lp:~verifydtapn-contributers/verifydtapn/NoLivenessGCD]

299. By Peter Gjøl Jensen on 2014-02-17

changed error text

[Peter Gjøl Jensen (peter-gjoel)]

Should be as requested now.

[Jiri Srba (srba)]

review: Approve

=== modified file 'src/DiscreteVerification/DiscreteVerification.cpp'
--- src/DiscreteVerification/DiscreteVerification.cpp	2013-12-05 13:23:21 +0000
+++ src/DiscreteVerification/DiscreteVerification.cpp	2014-02-17 21:34:43 +0000
@@ -89,10 +89,26 @@
             	}
 
             	delete strategy;
+                return 0;
+            }
+            
+            
+            // asume that we dont reach here except if we are doing normal verification
+            AST::BoolResult containsDeadlock;
+            DeadlockVisitor deadlockVisitor = DeadlockVisitor();
+            deadlockVisitor.visit(*query, containsDeadlock);
+            if(containsDeadlock.value && options.getDisableGCDLowerGuards() == false){
+                        cout << "Lowering constants by greatest common divisor is unsound for queries containing the deadlock proposition" << endl;
+                        exit(1);
+            }
+            if((query->getQuantifier() == EG || query->getQuantifier() == AF) && options.getDisableGCDLowerGuards() == false){
+                        cout << "Lowering constants by greatest common divisor is unsound for EG and AF queries" << endl;
+                        exit(1);
+            }
+            
+            
+            if (options.getVerificationType() == VerificationOptions::DISCRETE) {
 
-            }
-            else if (options.getVerificationType() == VerificationOptions::DISCRETE) {
-                
                 if (options.getMemoryOptimization() == VerificationOptions::PTRIE) {
                     //TODO fix initialization
                     WaitingList<EncodingPointer<MetaData> >* strategy = getWaitingList<EncodingPointer<MetaData> > (query, options);
@@ -132,12 +148,8 @@
                     }
                     delete strategy;
                 }
-            } else if (options.getVerificationType() == VerificationOptions::TIMEDART) {
+            } else if (options.getVerificationType() == VerificationOptions::TIMEDART) {              
                 if (query->getQuantifier() == EG || query->getQuantifier() == AF) {
-                    AST::BoolResult containsDeadlock;
-                    DeadlockVisitor deadlockVisitor = DeadlockVisitor();
-                    deadlockVisitor.visit(*query, containsDeadlock);
-
                     if (containsDeadlock.value) {
                         std::cout << "The combination of TimeDarts, Deadlock proposition and EG or AF queries is currently not supported" << endl;
                         exit(1);