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

[Mathias Grund Sørensen]

[Jakob Taankvist (jakob-taankvist)]

It's very nice we do the check in the "static part" instead of in the cut function.

review: Approve

[Jiri Srba (srba)]

review: Approve

=== modified file 'src/Core/ArgsParser.cpp'
--- src/Core/ArgsParser.cpp	2012-07-09 13:19:22 +0000
+++ src/Core/ArgsParser.cpp	2012-07-12 15:51:27 +0000
@@ -14,6 +14,7 @@
 	static const std::string MAX_CONSTANT_OPTION = "global-max-constants";
 	static const std::string XML_TRACE_OPTION = "xml-trace";
 	static const std::string LEGACY = "legacy";
+	static const std::string KEEP_DEAD = "keep-dead-tokens";
 
 	std::ostream& operator<<(std::ostream& out, const Switch& flag)
 	{
@@ -138,7 +139,7 @@
 		parsers.push_back(boost::make_shared<SwitchWithArg>("k", KBOUND_OPTION, "Max tokens to use during exploration.",0));
 		parsers.push_back(boost::make_shared<SwitchWithArg>("o", SEARCH_OPTION, "Specify the desired search strategy.\n - 0: Breadth-First Search\n - 1: Depth-First Search\n - 2: Random Search\n - 3: Heuristic Search",3));
 		parsers.push_back(boost::make_shared<SwitchWithArg>("t", TRACE_OPTION, "Specify the desired trace option.\n - 0: none\n - 1: some",0));
-
+		parsers.push_back(boost::make_shared<Switch>("d",KEEP_DEAD, "Do not discard dead tokens\n(used for boundedness checking)"));
 		parsers.push_back(boost::make_shared<Switch>("g",MAX_CONSTANT_OPTION, "Use global maximum constant for \nextrapolation (as opposed to local \nconstants)."));
 		parsers.push_back(boost::make_shared<Switch>("s",LEGACY, "Legacy option (no effect)."));
 
@@ -316,9 +317,12 @@
 		assert(map.find(MAX_CONSTANT_OPTION) != map.end());
 		bool max_constant = boost::lexical_cast<bool>(map.find(MAX_CONSTANT_OPTION)->second);
 
+		assert(map.find(KEEP_DEAD) != map.end());
+		bool keep_dead = boost::lexical_cast<bool>(map.find(KEEP_DEAD)->second);
+
 		assert(map.find(XML_TRACE_OPTION) != map.end());
 		bool xml_trace = boost::lexical_cast<bool>(map.find(XML_TRACE_OPTION)->second);
 
-		return VerificationOptions(modelFile, queryFile, search, kbound, trace, xml_trace, max_constant);
+		return VerificationOptions(modelFile, queryFile, search, kbound, trace, xml_trace, max_constant, keep_dead);
 	}
 }

=== modified file 'src/Core/TAPN/TimedArcPetriNet.cpp'
--- src/Core/TAPN/TimedArcPetriNet.cpp	2012-07-02 06:33:02 +0000
+++ src/Core/TAPN/TimedArcPetriNet.cpp	2012-07-12 15:51:27 +0000
@@ -206,7 +206,7 @@
 			}
 		}
 
-		void TimedArcPetriNet::updatePlaceTypes(const AST::Query* query){
+		void TimedArcPetriNet::updatePlaceTypes(const AST::Query* query, VerificationOptions options){
 			std::vector< int > placeNumbers;
 			boost::any context = placeNumbers;
 			DiscreteVerification::PlaceVisitor visitor;
@@ -214,9 +214,14 @@
 			placeNumbers = boost::any_cast< std::vector< int > >(context);
 
 			for(TimedPlace::Vector::const_iterator iter = places.begin(); iter != places.end(); ++iter){
+				if(options.GetKeepDeadTokens() && (*iter)->GetType() == Dead){
+					(*iter)->SetType(Std);
+					continue;
+				}
 				for(std::vector<int>::const_iterator id_iter = placeNumbers.begin(); id_iter != placeNumbers.end(); id_iter++){
 					if((*id_iter) == (*iter)->GetIndex() && (*iter)->GetType() == Dead){
 						(*iter)->SetType(Std);
+						break;
 					}
 				}
 			}

=== modified file 'src/Core/TAPN/TimedArcPetriNet.hpp'
--- src/Core/TAPN/TimedArcPetriNet.hpp	2012-07-02 06:33:02 +0000
+++ src/Core/TAPN/TimedArcPetriNet.hpp	2012-07-12 15:51:27 +0000
@@ -14,6 +14,7 @@
 #include "Pairing.hpp"
 #include "../QueryParser/AST.hpp"
 #include "../../DiscreteVerification/PlaceVisitor.hpp"
+#include "../VerificationOptions.hpp"
 
 namespace VerifyTAPN {
 
@@ -52,7 +53,7 @@
 			inline const bool IsPlaceUntimed(int index) const { return places[index]->IsUntimed(); }
 			bool IsNonStrict() const;
 			void calculateCausality(TimedPlace& p, std::vector< TimedPlace* >* result) const;
-			void updatePlaceTypes(const AST::Query* query);
+			void updatePlaceTypes(const AST::Query* query, VerificationOptions options);
 		public: // modifiers
 			void Initialize(bool useGlobalMaxConstant);
 			void removeOrphantedTransitions();

=== modified file 'src/Core/VerificationOptions.hpp'
--- src/Core/VerificationOptions.hpp	2012-07-02 06:33:02 +0000
+++ src/Core/VerificationOptions.hpp	2012-07-12 15:51:27 +0000
@@ -19,14 +19,16 @@
 				unsigned int k_bound,
 				Trace trace,
 				bool xml_trace,
-				bool useGlobalMaxConstants
+				bool useGlobalMaxConstants,
+				bool keepDeadTokens
 			) :	inputFile(inputFile),
 				queryFile(queryFile),
 				searchType(searchType),
 				k_bound(k_bound),
 				trace(trace),
 				xml_trace(xml_trace),
-				useGlobalMaxConstants(useGlobalMaxConstants)
+				useGlobalMaxConstants(useGlobalMaxConstants),
+				keepDeadTokens(keepDeadTokens)
 			{ };
 
 		public: // inspectors
@@ -37,6 +39,7 @@
 			inline const bool XmlTrace() const { return xml_trace; };
 			inline const bool GetGlobalMaxConstantsEnabled() const { return useGlobalMaxConstants; }
 			inline const SearchType GetSearchType() const { return searchType; }
+			inline const bool GetKeepDeadTokens() const { return keepDeadTokens; };
 			inline Factory GetFactory() const { return DEFAULT; };
 			inline void SetFactory(Factory f) { factory = f; };
 		private:
@@ -47,6 +50,7 @@
 			Trace trace;
 			bool xml_trace;
 			bool useGlobalMaxConstants;
+			bool keepDeadTokens;
 			Factory factory;
 	};
 

=== modified file 'src/main.cpp'
--- src/main.cpp	2012-07-02 06:49:56 +0000
+++ src/main.cpp	2012-07-12 15:51:27 +0000
@@ -47,7 +47,7 @@
 		tapn->removeOrphantedTransitions();
 	}
 
-	tapn->updatePlaceTypes(query);
+	tapn->updatePlaceTypes(query, options);
 
 	return DiscreteVerification::DiscreteVerification::run(tapn, initialPlacement, query, options);
 }