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

[Peter Gjøl Jensen]

Trailing delays removed and if we print delay for ever, any previous delay is removed.

The fix removes trailing delays from traces which leads to wrong reporting of "delay forever" (see bug).

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

312. By Jiri Srba on 2014-07-05

fixes a problem with wrong delay detection in case of a deadlock

[Jiri Srba (srba)]

I fixed a small issue. However, if e.g. EG ends with delay for ever, it will report something like

...
delay 7
delay for ever

and the delay 7 is redundant and should be replaced just with delay for ever.

review: Needs Fixing

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

313. By Peter Gjøl Jensen on 2014-07-07

fixed by altering trace before output, rather than adding more special cases

[Jiri Srba (srba)]

Tested and seems to work just fine. Mathias and Jakob, what do you think?

review: Approve

=== modified file 'src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp'
--- src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp	2014-05-09 16:05:31 +0000
+++ src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp	2014-07-07 19:00:30 +0000
@@ -51,7 +51,11 @@
 				marking->incrementAge();
 				marking->setGeneratedBy(NULL);
                                 if(addToPW(marking, &next_marking)){
-                                        return true;
+                                    // 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-04-06 11:00:59 +0000
+++ src/DiscreteVerification/VerificationTypes/TimeDartVerification.cpp	2014-07-07 19:00:30 +0000
@@ -199,11 +199,18 @@
                 if(diff > tapn.getMaxConstant()) {
                     diff = (tapn.getMaxConstant() + 1) - trace->start;
                 }
+                
+                // find the lowest delay at which the query is satisfied
+                while(diff && base->canDeadlock(tapn, trace->start + diff - 1))
+                {
+                    --diff;
+                }
 
                 while (diff) {  // while there is some delay in trace
                         NonStrictMarkingBase* mc = new NonStrictMarkingBase(*base);
                         mc->incrementAge(trace->start + diff);
-                        mc->setGeneratedBy(NULL);       // NULL indicates that it is a delay transition
+                        mc->setGeneratedBy(NULL);       // NULL indicates that it is a delay transition 
+                        
                         if (last != NULL) {
                             last->setParent(mc);        // set the parent of the last marking
                         }

=== modified file 'src/DiscreteVerification/VerificationTypes/Verification.hpp'
--- src/DiscreteVerification/VerificationTypes/Verification.hpp	2014-06-11 15:18:23 +0000
+++ src/DiscreteVerification/VerificationTypes/Verification.hpp	2014-07-07 19:00:30 +0000
@@ -8,6 +8,8 @@
 #include "../../Core/TAPNParser/util.hpp"
 #include "../DeadlockVisitor.hpp"
 
+
+
 namespace VerifyTAPN {
     namespace DiscreteVerification {
         template<typename T>
@@ -27,6 +29,7 @@
                 std::cout << "Error generating trace" << std::endl;
             }
 
+            void removeLastIfDelay(rapidxml::xml_node<>&);
             void printHumanTrace(T* m, std::stack<T*>& stack, AST::Quantifier query);
             void printXMLTrace(T* m, std::stack<T*>& stack, AST::Query* query, TAPN::TimedArcPetriNet& tapn);
             rapidxml::xml_node<>* createTransitionNode(T* old, T* current, rapidxml::xml_document<>& doc);
@@ -125,6 +128,19 @@
         }
 
         template<typename T>
+        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();
+                }
+            }
+        }
+        
+        template<typename T>
         void Verification<T>::printXMLTrace(T* m, std::stack<T*>& stack, AST::Query* query, TAPN::TimedArcPetriNet& tapn) {
             using namespace rapidxml;
             std::cerr << "Trace: " << std::endl;
@@ -170,6 +186,8 @@
                         if(delayloop)
                             continue;
                         if ((!foundLoop) && stack.empty() && old->getNumberOfChildren() > 0) {
+                            // remove delay before delay forever
+                            removeLastIfDelay(*root);
                             xml_node<>* node = doc.allocate_node(node_element, "delay", doc.allocate_string("forever"));
                             root->append_node(node);
                             delayedForever = true;
@@ -247,13 +265,17 @@
 				node = doc.allocate_node(node_element, "deadlock");
 			} else {
 				// if not it is delay forever
-				node = doc.allocate_node(node_element, "delay", doc.allocate_string("forever"));				
+                            
+                                // remove delay before delay forever
+                                removeLastIfDelay(*root);
+				node = doc.allocate_node(node_element, "delay", doc.allocate_string("forever"));
+                                
 			}
                         root->append_node(node);
                     }
                 }
             }
-
+            
             std::cerr << doc;
         }