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

[Peter Gjøl Jensen]

The fix contains a minor change to the structure of the trace-generation. This will only affect livenes queries ending in delay forever or deadlocks.

The fix contains a minor change to the structure of the trace-generation. This will only affect livenes queries ending in delay forever or deadlocks.

Please verify that this fix does not break any other traces.

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

323. By Peter Gjøl Jensen on 2014-08-11

should fix delay forever/deadlock prefference

324. By Peter Gjøl Jensen on 2014-08-11

fixed raised assert

[Jiri Srba (srba)]

I thoroughly tested it now and it seems work correctly. In particular I like the simplification
of the code when detecting deadlock vs. delay-for-ever.

review: Approve

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

Code looks good and changes seem reasonable.

review: Approve (code)

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

Code looks good and changes seem reasonable.

review: Approve (code)

=== modified file 'src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp'
--- src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp	2014-07-14 09:54:33 +0000
+++ src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp	2014-08-11 19:51:42 +0000
@@ -51,10 +51,6 @@
 				marking->incrementAge();
 				marking->setGeneratedBy(NULL);
                                 if(addToPW(marking, &next_marking)){
-                                    // this can only occur when there is a deadlock detected by cut
-                                    // pop last marking as it is not a part of the trace
-                                    // ie. we detect the situation 1 delay later.
-                                    trace.pop();
                                     return true;
                                 }
                                 endOfMaxRun = false;

=== modified file 'src/DiscreteVerification/VerificationTypes/TimeDartVerification.cpp'
--- src/DiscreteVerification/VerificationTypes/TimeDartVerification.cpp	2014-07-14 09:54:33 +0000
+++ src/DiscreteVerification/VerificationTypes/TimeDartVerification.cpp	2014-08-11 19:51:42 +0000
@@ -213,6 +213,7 @@
                         
                         if (last != NULL) {
                             last->setParent(mc);        // set the parent of the last marking
+                            mc->setNumberOfChildren(1);
                         }
 
                         last = mc;
@@ -256,6 +257,7 @@
                         mc->setGeneratedBy(NULL);       // NULL indicates that it is a delay transition
                         if (last != NULL){
                             last->setParent(mc);          // set the parent of the last marking
+                            mc->setNumberOfChildren(1);
                         }
                         if(!l->getParent()){
                             l->setParent(mc);
@@ -268,9 +270,11 @@
                 }
                 if(last != NULL){
                     last->setParent(m);
+                    m->setNumberOfChildren(1);
                 }
                 if(!l->getParent()) {
                     l->setParent(m);
+                    m->setNumberOfChildren(1);
                 }
                 m->cut(placeStats);
                 last = m;
@@ -279,6 +283,10 @@
                 upper = trace->upper;
                 trace = (TraceDart*) trace->parent;
             }
+            
+            if(!deadlock){
+                l->setNumberOfChildren(1);
+            }
 
             printXMLTrace(l, traceStack, query, tapn);
         }

=== modified file 'src/DiscreteVerification/VerificationTypes/Verification.hpp'
--- src/DiscreteVerification/VerificationTypes/Verification.hpp	2014-07-14 09:54:33 +0000
+++ src/DiscreteVerification/VerificationTypes/Verification.hpp	2014-08-11 19:51:42 +0000
@@ -151,11 +151,13 @@
         void Verification<T>::removeLastIfDelay(rapidxml::xml_node<>& root)
         {
             using namespace rapidxml;
-            xml_node<>* node = root.last_node();
-            if(node){
-                char* name = node->name();
-                if(strcmp(name, "delay") == 0){
-                    root.remove_last_node();
+            if(root.first_node()){ // if there is a node in the trace
+                xml_node<>* node = root.last_node();
+                if(node){
+                    char* name = node->name();
+                    if(strcmp(name, "delay") == 0){
+                        root.remove_last_node();
+                    }
                 }
             }
         }
@@ -262,7 +264,7 @@
                             break;
                         } 
                         temp = (T*)temp->getParent();
-                    } while(temp && temp->getParent() && temp->getParent() != top);
+                    } while(temp && temp->getParent());
                     if(foundLoop){
                         root->append_node(doc.allocate_node(node_element, "loop"));
                     }
@@ -275,24 +277,19 @@
             //Trace ended, goto * or deadlock
             if (query->getQuantifier() == AST::EG || query->getQuantifier() == AST::AF) {
                 if (!foundLoop && !delayedForever) {
-                    if (m->getNumberOfChildren() > 0) {
-                        root->append_node(doc.allocate_node(node_element, "deadlock"));
+                    xml_node<>* node;
+                    if(m->canDeadlock(tapn, 0, false)){
+                            // check if deadlock
+                            node = doc.allocate_node(node_element, "deadlock");
                     } else {
-                        
-			xml_node<>* node;
-			if(m->canDeadlock(tapn, 0, false)){
-				// check if deadlock
-				node = doc.allocate_node(node_element, "deadlock");
-			} else {
-				// if not it is delay forever
-                            
-                                // remove delay before delay forever
-                                removeLastIfDelay(*root);
-				node = doc.allocate_node(node_element, "delay", doc.allocate_string("forever"));
-                                
-			}
-                        root->append_node(node);
+                            // if not it is delay forever
+
+                            // remove delay before delay forever
+                            removeLastIfDelay(*root);
+                            node = doc.allocate_node(node_element, "delay", doc.allocate_string("forever"));
+
                     }
+                    root->append_node(node);
                 }
             }