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

[Peter Gjøl Jensen]

Implementation of urgent transitions for the pointwise engine.
The only major change is the return-type of the successor-generator which now returns "Query Satisfied", "Query Unsatisfied" and "Urgent Enabled" to be able to allow/disallow the aging of a marking when needed.

[Jiri Srba (srba)]

review: Approve

[Jakob Taankvist (jakob-taankvist)]

review: Approve

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

review: Approve

=== modified file 'src/Core/ArgsParser.hpp'
--- src/Core/ArgsParser.hpp	2013-05-14 19:30:32 +0000
+++ src/Core/ArgsParser.hpp	2013-07-21 08:22:24 +0000
@@ -80,7 +80,7 @@
 	class ArgsParser {
 		typedef std::vector< boost::shared_ptr<Switch> > parser_vec;
 	public:
-		ArgsParser() : parsers(), version(2,0,1) { initialize(); };
+		ArgsParser() : parsers(), version(2,2,0) { initialize(); };
 		virtual ~ArgsParser() {};
 
 		VerificationOptions parse(int argc, char* argv[]) const;

=== modified file 'src/Core/TAPN/TimedTransition.cpp'
--- src/Core/TAPN/TimedTransition.cpp	2013-05-08 15:10:14 +0000
+++ src/Core/TAPN/TimedTransition.cpp	2013-07-21 08:22:24 +0000
@@ -1,17 +1,28 @@
 #include "TimedTransition.hpp"
+#include "TimedPlace.hpp"
 
 namespace VerifyTAPN {
 	namespace TAPN {
 		void TimedTransition::print(std::ostream& out) const
 		{
-			out << getName() << "(" << index << ")";
+			out << getName();
+                        if(this->urgent)
+                            out << " urgent ";
+                        out << "(" << index << ")";
 		}
 
 		void TimedTransition::addToPreset(const boost::shared_ptr<TimedInputArc>& arc)
 		{
 			if(arc)
 			{
-				preset.push_back(arc);
+                                if(this->urgent){   // all urgency in discrete time must have untimed 
+                                                    //inputarcs to not break semantics
+                                    if(!arc.get()->getInterval().isZeroInfinity()){
+                                        std::cout << "Urgent transitions must have untimed input arcs" << std::endl;
+                                        exit(1);
+                                    }
+                                }
+                                preset.push_back(arc);
 			}
 		}
 
@@ -19,6 +30,17 @@
 		{
 			if(arc)
 			{
+                            if(this->urgent){   // all urgency in discrete time must have untimed 
+                                                //inputarcs to not break semantics
+                                if(!arc.get()->getInterval().isZeroInfinity()){
+                                    std::cout << "Urgent transitions must have untimed transportarcs" << std::endl;
+                                    exit(1);
+                                } else if(arc.get()->getDestination().getInvariant() != TimeInvariant::LS_INF){
+                                    // urgency breaks if we have invariant at destination
+                                    std::cout << "Transportarcs going through an urgent transition cannot have invariants at destination-places." << std::endl;
+                                    exit(1);                                    
+                                }
+                            }
 				transportArcs.push_back(arc);
 			}
 		}

=== modified file 'src/Core/TAPN/TimedTransition.hpp'
--- src/Core/TAPN/TimedTransition.hpp	2013-05-08 15:10:14 +0000
+++ src/Core/TAPN/TimedTransition.hpp	2013-07-21 08:22:24 +0000
@@ -21,8 +21,8 @@
 		public: // typedefs
 			typedef std::vector< boost::shared_ptr<TimedTransition> > Vector;
 		public:
-			TimedTransition(const std::string& name, const std::string& id) : name(name), id(id), preset(), postset(), transportArcs(), index(-1), untimedPostset(true) { };
-			TimedTransition() : name("*EMPTY*"), id("-1"), preset(), postset(), transportArcs(), index(-1), untimedPostset(true) { };
+			TimedTransition(const std::string& name, const std::string& id, bool urgent) : name(name), id(id), preset(), postset(), transportArcs(), index(-1), untimedPostset(true), urgent(urgent) { };
+			TimedTransition() : name("*EMPTY*"), id("-1"), preset(), postset(), transportArcs(), index(-1), untimedPostset(true),urgent(false) { };
 			virtual ~TimedTransition() { /* empty */ }
 
 		public: // modifiers
@@ -49,6 +49,9 @@
 			inline unsigned int getIndex() const { return index; }
 			inline const bool hasUntimedPostset() const { return untimedPostset; }
 			inline void setUntimedPostset(bool untimed){ untimedPostset = untimed; }
+                        inline const bool isUrgent() const {
+                            return urgent;
+                        }
 
 		private: // data
 			std::string name;
@@ -59,6 +62,7 @@
 			InhibitorArc::WeakPtrVector inhibitorArcs;
 			unsigned int index;
 			bool untimedPostset;
+                        bool urgent;
 		};
 
 		inline std::ostream& operator<<(std::ostream& out, const TimedTransition& transition)

=== modified file 'src/Core/TAPNParser/TAPNXmlParser.cpp'
--- src/Core/TAPNParser/TAPNXmlParser.cpp	2013-05-08 15:23:45 +0000
+++ src/Core/TAPNParser/TAPNXmlParser.cpp	2013-07-21 08:22:24 +0000
@@ -95,7 +95,15 @@
 {
 	std::string id(transitionNode.first_attribute("id")->value());
 	std::string name(transitionNode.first_attribute("name")->value());
-	return boost::make_shared<TimedTransition>(name, id);
+        xml_attribute<char>* urgenatt = transitionNode.first_attribute("urgent");
+        bool urgent = false;
+        if(urgenatt != NULL){
+            std::string urgentStr = urgenatt->value();
+            if(urgentStr.compare("true") == 0){
+                urgent = true;
+            }
+        }
+	return boost::make_shared<TimedTransition>(name, id,urgent );
 }
 
 TAPNXmlParser::ArcCollections TAPNXmlParser::parseArcs(const xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const

=== modified file 'src/DiscreteVerification/SuccessorGenerator.hpp'
--- src/DiscreteVerification/SuccessorGenerator.hpp	2013-05-08 15:10:14 +0000
+++ src/DiscreteVerification/SuccessorGenerator.hpp	2013-07-21 08:22:24 +0000
@@ -132,6 +132,8 @@
             }
         };
 
+        enum Result {QUERY_SATISFIED, QUERY_UNSATISFIED, URGENT_ENABLED};
+        
         template<typename T>
         class SuccessorGenerator {
             typedef google::sparse_hash_map<const void*, TokenList> ArcHashMap;
@@ -139,10 +141,13 @@
             typedef typename boost::ptr_vector< ArcAndTokenWithType > ArcAndTokensVector;
 
         public:
+            
             SuccessorGenerator(TAPN::TimedArcPetriNet& tapn, Verification<T>& verifier);
             ~SuccessorGenerator();
-            bool generateAndInsertSuccessors(const T& marking);
+            
+            Result generateAndInsertSuccessors(const T& marking);
             void printTransitionStatistics(std::ostream & out) const;
+
             inline bool doSuccessorsExist();
             
         private:
@@ -165,7 +170,7 @@
                     const TimedTransition& transition,
                     int bound = std::numeric_limits<int>().max(),
                     bool isInhib = false
-                    ) const;
+                    );
 
             inline void clearTransitionsArray() {
                 memset(transitionStatistics, 0, numberoftransitions * sizeof (transitionStatistics[0]));
@@ -175,6 +180,7 @@
             unsigned int* transitionStatistics;
             Verification<T>& verifier;
             bool succesorsExist;
+            bool urgentEnabled;
         };
 
         template<typename T>
@@ -200,11 +206,12 @@
         }
         
         template<typename T>
-        bool SuccessorGenerator<T>::generateAndInsertSuccessors(const T& marking) {
+        Result SuccessorGenerator<T>::generateAndInsertSuccessors(const T& marking) {
             succesorsExist = false;
-            
+            urgentEnabled = false;
             ArcHashMap enabledArcs(tapn.getInhibitorArcs().size() + tapn.getInputArcs().size() + tapn.getTransportArcs().size());
             std::vector<unsigned int> enabledTransitionArcs(tapn.getTransitions().size(), 0);
+
             std::vector<const TAPN::TimedTransition* > enabledTransitions;
 
             for (PlaceList::const_iterator iter = marking.getPlaceList().begin(); iter < marking.getPlaceList().end(); iter++) {
@@ -230,7 +237,16 @@
             }
 
             enabledTransitions.insert(enabledTransitions.end(), allwaysEnabled.begin(), allwaysEnabled.end());
-            return generateMarkings(marking, enabledTransitions, enabledArcs);
+            if(generateMarkings(marking, enabledTransitions, enabledArcs)){
+                return QUERY_SATISFIED;
+            } else {
+                if(urgentEnabled){
+                    return URGENT_ENABLED;
+                } else{
+                    return QUERY_UNSATISFIED;
+                }
+            }
+
         }
 
         template<typename T>
@@ -244,7 +260,7 @@
                 const TimedTransition& transition,
                 int bound,
                 bool isInhib
-                ) const {
+                ) {
             bool arcIsEnabled = false;
             for (TokenList::const_iterator token_iter = place.tokens.begin(); token_iter != place.tokens.end(); token_iter++) {
                 if (interval.getLowerBound() <= token_iter->getAge() && token_iter->getAge() <= interval.getUpperBound() && token_iter->getAge() <= bound) {
@@ -310,6 +326,11 @@
                 }
             }
 
+            // only here the weights have been properly checked.
+            if(transition.isUrgent()){
+                this->urgentEnabled = true;
+            }
+            
             // Write statistics
             transitionStatistics[transition.getIndex()]++;
 

=== modified file 'src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp'
--- src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp	2013-05-08 13:49:42 +0000
+++ src/DiscreteVerification/VerificationTypes/LivenessSearch.cpp	2013-07-21 08:22:24 +0000
@@ -37,8 +37,16 @@
 			trace.push(&next_marking);
 			validChildren = 0;
 
-
-			if(isDelayPossible(next_marking)){
+                        bool noDelay = false;
+                        Result res = successorGenerator.generateAndInsertSuccessors(next_marking);
+                        if (res == QUERY_SATISFIED) {
+                            return true;
+                        } else if (res == URGENT_ENABLED) {
+                            noDelay = true;
+                        }
+                        
+                        
+			if(!noDelay && isDelayPossible(next_marking)){
 				NonStrictMarking* marking = new NonStrictMarking(next_marking);
 				marking->incrementAge();
 				marking->setGeneratedBy(NULL);
@@ -47,9 +55,6 @@
                                 }
                                 endOfMaxRun = false;
 			}
-                        if(successorGenerator.generateAndInsertSuccessors(next_marking)){
-                                return true;
-                        }
                         // if no delay is possible, and no transition-based succecors are possible, we have reached a max run
                         endOfMaxRun = endOfMaxRun && (!successorGenerator.doSuccessorsExist());
 

=== modified file 'src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp'
--- src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp	2013-05-08 13:49:42 +0000
+++ src/DiscreteVerification/VerificationTypes/ReachabilitySearch.cpp	2013-07-21 08:22:24 +0000
@@ -32,8 +32,16 @@
 		trace.push(&next_marking);
 		validChildren = 0;
 
+                bool noDelay = false;
+                Result res = successorGenerator.generateAndInsertSuccessors(next_marking);
+                if(res == QUERY_SATISFIED){
+                    return true;
+                }  else if (res == URGENT_ENABLED) {
+                    noDelay = true;
+                }
+
 		// Generate next markings
-		if(isDelayPossible(next_marking)){
+		if(!noDelay && isDelayPossible(next_marking)){
 			NonStrictMarking* marking = new NonStrictMarking(next_marking);
 			marking->incrementAge();
 			marking->setGeneratedBy(NULL);
@@ -41,11 +49,8 @@
                             return true;
                         }
 		}
-                if(successorGenerator.generateAndInsertSuccessors(next_marking)){
-                    return true;
-                }  
-
                 deleteMarking(&next_marking);
+
 	}
 
 	return false;

=== modified file 'src/DiscreteVerification/VerificationTypes/TimeDartVerification.hpp'
--- src/DiscreteVerification/VerificationTypes/TimeDartVerification.hpp	2013-05-08 15:10:14 +0000
+++ src/DiscreteVerification/VerificationTypes/TimeDartVerification.hpp	2013-07-21 08:22:24 +0000
@@ -28,6 +28,10 @@
                     if ((*iter)->getPreset().size() + (*iter)->getTransportArcs().size() == 0) {
                         allwaysEnabled.push_back(iter->get());
                     }
+                    if((*iter)->isUrgent()){    // no implementation for urgency in timedart engine yet
+                        cout << "The TimeDart engine cannot handle urgent transitions" << endl;
+                        exit(1);
+                    }
                 }
             }