Remove boost & Fixing CMake

src/Core/ArgsParser.cpp

@@ -3,7 +3,6 @@
 #include <sstream>
 #include "boost/algorithm/string.hpp"
 #include "boost/lexical_cast.hpp"
-#include "boost/make_shared.hpp"
 #include <iomanip>
 #include "boost/tokenizer.hpp"
 
@@ -132,18 +131,18 @@ namespace VerifyTAPN {
 		// NOTE: The Help() function only splits and indents descriptions based on newlines.
 		//       Each line in the description is assumed to fit within the remaining width
 		//       of the console, so keep descriptions short, or implement manual word-wrapping :).
-		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: Maximum Cover 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(std::make_shared<SwitchWithArg>("k", KBOUND_OPTION, "Max tokens to use during exploration.",0));
+		parsers.push_back(std::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: Maximum Cover Search",3));
+		parsers.push_back(std::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>("g",MAX_CONSTANT_OPTION, "Use global maximum constant for \nextrapolation (as opposed to local \nconstants)."));
-		parsers.push_back(boost::make_shared<Switch>("u",UNTIMED_PLACES_OPTION, "Disables the untimed place optimization."));
-		parsers.push_back(boost::make_shared<Switch>("s",SYMMETRY_OPTION, "Disables symmetry reduction."));
+		parsers.push_back(std::make_shared<Switch>("g",MAX_CONSTANT_OPTION, "Use global maximum constant for \nextrapolation (as opposed to local \nconstants)."));
+		parsers.push_back(std::make_shared<Switch>("u",UNTIMED_PLACES_OPTION, "Disables the untimed place optimization."));
+		parsers.push_back(std::make_shared<Switch>("s",SYMMETRY_OPTION, "Disables symmetry reduction."));
 
-		parsers.push_back(boost::make_shared<Switch>("x",XML_TRACE_OPTION, "Output trace in xml format for TAPAAL."));
+		parsers.push_back(std::make_shared<Switch>("x",XML_TRACE_OPTION, "Output trace in xml format for TAPAAL."));
 
-		parsers.push_back(boost::make_shared<SwitchWithArg>("f", FACTORY_OPTION, "Specify the desired marking factory.\n - 0: Default\n - 1: Discrete-inclusion\n - 2: Old factory",0));
-		parsers.push_back(boost::make_shared<SwitchWithStringArg>("i", INCLUSION_PLACES, "Specify a list of places to consider \nfor discrete inclusion. No spaces after\nthe commas!\nSpecial values: *ALL*, *NONE*", "*ALL*"));
+		parsers.push_back(std::make_shared<SwitchWithArg>("f", FACTORY_OPTION, "Specify the desired marking factory.\n - 0: Default\n - 1: Discrete-inclusion\n - 2: Old factory",0));
+		parsers.push_back(std::make_shared<SwitchWithStringArg>("i", INCLUSION_PLACES, "Specify a list of places to consider \nfor discrete inclusion. No spaces after\nthe commas!\nSpecial values: *ALL*, *NONE*", "*ALL*"));
 	};
 
 	void ArgsParser::Help() const

src/Core/ArgsParser.hpp

@@ -1,13 +1,14 @@
 #ifndef ARGSPARSER_HPP_
 #define ARGSPARSER_HPP_
 
+#include "VerificationOptions.hpp"
+#include "boost/lexical_cast.hpp"
+
 #include <vector>
 #include <map>
 #include <string>
 #include <iosfwd>
-#include "boost/smart_ptr.hpp"
-#include "VerificationOptions.hpp"
-#include "boost/lexical_cast.hpp"
+#include <memory>
 
 namespace VerifyTAPN
 {
@@ -65,7 +66,7 @@ namespace VerifyTAPN
 	};
 
 	class ArgsParser {
-		typedef std::vector< boost::shared_ptr<Switch> > parser_vec;
+		typedef std::vector< std::shared_ptr<Switch> > parser_vec;
 	public:
 		ArgsParser() : parsers() { Initialize(); };
 		virtual ~ArgsParser() {};

src/Core/QueryParser/ToStringVisitor.hpp

@@ -13,7 +13,7 @@ namespace VerifyTAPN
 		class ToStringVisitor : public Visitor
 		{
 		public:
-			ToStringVisitor(const boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn) : tapn(tapn) { };
+			ToStringVisitor(const std::shared_ptr<TAPN::TimedArcPetriNet>& tapn) : tapn(tapn) { };
 			virtual ~ToStringVisitor() {}
 			virtual void Visit(const NotExpression& expr, boost::any& context);
 			virtual void Visit(const OrExpression& expr, boost::any& context);
@@ -30,7 +30,7 @@ namespace VerifyTAPN
 
 			void Print(const Query& query) { boost::any any; query.Accept(*this, any); };
 		private:
-			const boost::shared_ptr<TAPN::TimedArcPetriNet> tapn;
+			const std::shared_ptr<TAPN::TimedArcPetriNet> tapn;
 		};
 	}
 }

src/Core/SymbolicMarking/DBMMarking.cpp

@@ -4,7 +4,7 @@
 
 namespace VerifyTAPN
 {
-	boost::shared_ptr<TAPN::TimedArcPetriNet> DBMMarking::tapn;
+	std::shared_ptr<TAPN::TimedArcPetriNet> DBMMarking::tapn;
 
 	// Add a token in each output place of placesOfTokensToAdd
 	// and add placesOfTokensToAdd.size() clocks to the DBM.

src/Core/SymbolicMarking/DBMMarking.hpp

@@ -15,7 +15,7 @@ namespace VerifyTAPN {
 		friend class UppaalDBMMarkingFactory;
 		friend class DiscreteInclusionMarkingFactory;
 	public:
-		static boost::shared_ptr<TAPN::TimedArcPetriNet> tapn;
+		static std::shared_ptr<TAPN::TimedArcPetriNet> tapn;
 	public:
 		DBMMarking(const DiscretePart& dp, const dbm::dbm_t& dbm) : DiscreteMarking(dp), dbm(dbm), mapping() { InitMapping(); assert(IsConsistent()); };
 		DBMMarking(const DiscretePart& dp, const TokenMapping& mapping, const dbm::dbm_t& dbm) : DiscreteMarking(dp), dbm(dbm), mapping(mapping) { assert(IsConsistent()); };

src/Core/SymbolicMarking/DiscreteInclusionMarkingFactory.hpp

@@ -13,7 +13,7 @@ namespace VerifyTAPN {
 
 class DiscreteInclusionMarkingFactory : public UppaalDBMMarkingFactory {
 public:
-	DiscreteInclusionMarkingFactory(const boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn, const VerificationOptions& options)
+	DiscreteInclusionMarkingFactory(const std::shared_ptr<TAPN::TimedArcPetriNet>& tapn, const VerificationOptions& options)
 		: UppaalDBMMarkingFactory(tapn), tapn(tapn), inc_places(tapn->NumberOfPlaces(), false), empty_inc(options.GetFactory() == DEFAULT) { MarkPlacesForInclusion(options.GetIncPlaces()); };
 	virtual ~DiscreteInclusionMarkingFactory() {};
 
@@ -310,7 +310,7 @@ class DiscreteInclusionMarkingFactory : public UppaalDBMMarkingFactory {
 		}
 	};
 private:
-	boost::shared_ptr<TAPN::TimedArcPetriNet> tapn;
+	std::shared_ptr<TAPN::TimedArcPetriNet> tapn;
 	std::vector<bool> inc_places;
 	bool empty_inc;
 };

src/Core/SymbolicMarking/UppaalDBMMarkingFactory.hpp

@@ -11,7 +11,7 @@ namespace VerifyTAPN {
 	protected:
 		static id_type nextId;
 	public:
-		UppaalDBMMarkingFactory(const boost::shared_ptr<TAPN::TimedArcPetriNet>& tapn)
+		UppaalDBMMarkingFactory(const std::shared_ptr<TAPN::TimedArcPetriNet>& tapn)
 		{
 			DBMMarking::tapn = tapn;
 		};

src/Core/TAPN/InhibitorArc.hpp

@@ -1,9 +1,10 @@
 #ifndef INHIBITORARC_HPP_
 #define INHIBITORARC_HPP_
 
-#include <vector>
 #include "TimeInterval.hpp"
-#include "boost/smart_ptr.hpp"
+
+#include <vector>
+#include <memory>
 
 namespace VerifyTAPN {
 	namespace TAPN {
@@ -12,10 +13,10 @@ namespace VerifyTAPN {
 
 		class InhibitorArc {
 			public: // typedefs
-				typedef std::vector< boost::shared_ptr<InhibitorArc> > Vector;
-				typedef std::vector< boost::weak_ptr<InhibitorArc> > WeakPtrVector;
+				typedef std::vector< std::shared_ptr<InhibitorArc> > Vector;
+				typedef std::vector< InhibitorArc* > NakedPtrVector;
 			public:
-				InhibitorArc(const boost::shared_ptr<TimedPlace>& place, const boost::shared_ptr<TimedTransition>& transition) : place(place), transition(transition) { };
+				InhibitorArc(const std::shared_ptr<TimedPlace>& place, const std::shared_ptr<TimedTransition>& transition) : place(place), transition(transition) { };
 				virtual ~InhibitorArc() { /* empty */ }
 
 			public: // modifiers
@@ -25,8 +26,8 @@ namespace VerifyTAPN {
 			public: // Inspectors
 				void Print(std::ostream& out) const;
 			private:
-				const boost::shared_ptr<TimedPlace> place;
-				const boost::shared_ptr<TimedTransition> transition;
+				const std::shared_ptr<TimedPlace> place;
+				const std::shared_ptr<TimedTransition> transition;
 		};
 
 		inline std::ostream& operator<<(std::ostream& out, const InhibitorArc& arc)

src/Core/TAPN/OutputArc.hpp

@@ -2,7 +2,7 @@
 #define VERIFYTAPN_TAPN_OUTPUTARC_HPP_
 
 #include <vector>
-#include "boost/smart_ptr.hpp"
+#include <memory>
 
 namespace VerifyTAPN {
 	namespace TAPN {
@@ -12,10 +12,10 @@ namespace VerifyTAPN {
 		class OutputArc
 		{
 		public: // typedefs
-			typedef std::vector< boost::shared_ptr<OutputArc> > Vector;
-			typedef std::vector< boost::weak_ptr<OutputArc> > WeakPtrVector;
+			typedef std::vector< std::shared_ptr<OutputArc> > Vector;
+			typedef std::vector< OutputArc* > NakedPtrVector;
 		public:
-			OutputArc(const boost::shared_ptr<TimedTransition>& transition, const boost::shared_ptr<TimedPlace>& place)
+			OutputArc(const std::shared_ptr<TimedTransition>& transition, const std::shared_ptr<TimedPlace>& place)
 				: transition(transition), place(place) { };
 			virtual ~OutputArc() { /* empty */ }
 
@@ -26,8 +26,8 @@ namespace VerifyTAPN {
 		public: // inspectors
 			void Print(std::ostream& out) const;
 		private:
-			const boost::shared_ptr<TimedTransition> transition;
-			const boost::shared_ptr<TimedPlace> place;
+			const std::shared_ptr<TimedTransition> transition;
+			const std::shared_ptr<TimedPlace> place;
 		};
 
 		inline std::ostream& operator<<(std::ostream& out, const OutputArc& arc)

src/Core/TAPN/Pairing.cpp

@@ -7,8 +7,8 @@ namespace VerifyTAPN {
 using namespace TAPN;
 
 	void Pairing::GeneratePairingFor(const TimedArcPetriNet& tapn, const TAPN::TimedTransition& t) {
-		TimedInputArc::WeakPtrVector preset = t.GetPreset();
-		OutputArc::WeakPtrVector postset = t.GetPostset();
+		TimedInputArc::NakedPtrVector preset = t.GetPreset();
+		OutputArc::NakedPtrVector postset = t.GetPostset();
 
 		unsigned int sizeOfPairing = preset.size() >= postset.size() ? preset.size() : postset.size();
 
@@ -19,23 +19,23 @@ using namespace TAPN;
 		{
 			if(i < preset.size() && i < postset.size())
 			{
-				boost::shared_ptr<TimedInputArc> tiaPtr = preset[i].lock();
-				boost::shared_ptr<OutputArc> oaPtr = postset[i].lock();
+				TimedInputArc* tiaPtr = preset[i];
+				OutputArc* oaPtr = postset[i];
 
 				inputPlace = tapn.GetPlaceIndex(tiaPtr->InputPlace());
 				outputPlace = tapn.GetPlaceIndex(oaPtr->OutputPlace());
 
 				Add(inputPlace, outputPlace);
 			}
 			else if(i < preset.size() && i >= postset.size()){
-				boost::shared_ptr<TimedInputArc> tiaPtr = preset[i].lock();
+				TimedInputArc* tiaPtr = preset[i];
 
 				inputPlace = tapn.GetPlaceIndex(tiaPtr->InputPlace());
 				Add(inputPlace, TimedPlace::BottomIndex());
 			}
 			else if(i >= preset.size() && i < postset.size())
 			{
-				boost::shared_ptr<OutputArc> oaPtr = postset[i].lock();
+				OutputArc* oaPtr = postset[i];
 
 				outputPlace = tapn.GetPlaceIndex(oaPtr->OutputPlace());
 

src/Core/TAPN/TimedArcPetriNet.cpp

@@ -25,27 +25,27 @@ namespace VerifyTAPN {
 
 			for(TimedInputArc::Vector::const_iterator iter = inputArcs.begin(); iter != inputArcs.end(); ++iter)
 			{
-				const boost::shared_ptr<TimedInputArc>& arc = *iter;
+				const std::shared_ptr<TimedInputArc>& arc = *iter;
 				arc->OutputTransition().AddToPreset(arc);
 				UpdateMaxConstant(arc->Interval());
 			}
 
 			for(TransportArc::Vector::const_iterator iter = transportArcs.begin(); iter != transportArcs.end(); ++iter)
 			{
-				const boost::shared_ptr<TransportArc>& arc = *iter;
+				const std::shared_ptr<TransportArc>& arc = *iter;
 				arc->Transition().AddTransportArcGoingThrough(arc);
 				UpdateMaxConstant(arc->Interval());
 			}
 
 			for(InhibitorArc::Vector::const_iterator iter = inhibitorArcs.begin(); iter != inhibitorArcs.end(); ++iter) {
-				const boost::shared_ptr<InhibitorArc>& arc = *iter;
+				const std::shared_ptr<InhibitorArc>& arc = *iter;
 				arc->OutputTransition().AddIncomingInhibitorArc(arc);
 				arc->InputPlace().SetHasInhibitorArcs(true);
 			}
 
 			for(OutputArc::Vector::const_iterator iter = outputArcs.begin(); iter != outputArcs.end(); ++iter)
 			{
-				const boost::shared_ptr<OutputArc>& arc = *iter;
+				const std::shared_ptr<OutputArc>& arc = *iter;
 				arc->InputTransition().AddToPostset(arc);
 			}
 
@@ -115,7 +115,7 @@ namespace VerifyTAPN {
 				{
 					if((*arcIter)->InputPlace() == **iter)
 					{
-						boost::shared_ptr<TimedInputArc> ia = *arcIter;
+						std::shared_ptr<TimedInputArc> ia = *arcIter;
 						const TAPN::TimeInterval& interval = ia->Interval();
 
 						const int lowerBound = interval.GetLowerBound();

src/Core/TAPN/TimedArcPetriNet.hpp

@@ -8,7 +8,6 @@
 #include "TransportArc.hpp"
 #include "InhibitorArc.hpp"
 #include "OutputArc.hpp"
-#include "boost/make_shared.hpp"
 #include "google/sparse_hash_map"
 #include "boost/functional/hash.hpp"
 #include "Pairing.hpp"

src/Core/TAPN/TimedInputArc.hpp

@@ -1,9 +1,10 @@
 #ifndef VERIFYTAPN_TAPN_TIMEDINPUTARC_HPP_
 #define VERIFYTAPN_TAPN_TIMEDINPUTARC_HPP_
 
-#include <vector>
 #include "TimeInterval.hpp"
-#include "boost/smart_ptr.hpp"
+
+#include <vector>
+#include <memory>
 
 namespace VerifyTAPN {
 	namespace TAPN {
@@ -13,11 +14,11 @@ namespace VerifyTAPN {
 		class TimedInputArc
 		{
 		public: // typedefs
-			typedef std::vector< boost::shared_ptr<TimedInputArc> > Vector;
-			typedef std::vector< boost::weak_ptr<TimedInputArc> > WeakPtrVector;
+			typedef std::vector< std::shared_ptr<TimedInputArc> > Vector;
+			typedef std::vector< TimedInputArc* > NakedPtrVector;
 		public:
-			TimedInputArc(const boost::shared_ptr<TimedPlace>& place, const boost::shared_ptr<TimedTransition>& transition) : interval(), place(place), transition(transition) { };
-			TimedInputArc(const boost::shared_ptr<TimedPlace>& place, const boost::shared_ptr<TimedTransition>& transition, const TimeInterval& interval) : interval(interval), place(place), transition(transition) { };
+			TimedInputArc(const std::shared_ptr<TimedPlace>& place, const std::shared_ptr<TimedTransition>& transition) : interval(), place(place), transition(transition) { };
+			TimedInputArc(const std::shared_ptr<TimedPlace>& place, const std::shared_ptr<TimedTransition>& transition, const TimeInterval& interval) : interval(interval), place(place), transition(transition) { };
 			virtual ~TimedInputArc() { /* empty */}
 
 		public: // modifiers
@@ -29,8 +30,8 @@ namespace VerifyTAPN {
 			void Print(std::ostream& out) const;
 		private:
 			const TimeInterval interval;
-			const boost::shared_ptr<TimedPlace> place;
-			const boost::shared_ptr<TimedTransition> transition;
+			const std::shared_ptr<TimedPlace> place;
+			const std::shared_ptr<TimedTransition> transition;
 		};
 
 		inline std::ostream& operator<<(std::ostream& out, const TimedInputArc& arc)

src/Core/TAPN/TimedPlace.hpp

@@ -8,7 +8,6 @@
 #include "TimeInvariant.hpp"
 #include "TimedInputArc.hpp"
 #include "OutputArc.hpp"
-#include "boost/shared_ptr.hpp"
 
 namespace VerifyTAPN{
 	namespace TAPN{
@@ -26,7 +25,7 @@ namespace VerifyTAPN{
 			static const std::string BOTTOM_NAME;
 
 		public: // typedefs
-			typedef std::vector< boost::shared_ptr<TimedPlace> > Vector;
+			typedef std::vector< std::shared_ptr<TimedPlace> > Vector;
 
 		public: // construction / destruction
 			TimedPlace(const std::string& name, const std::string& id, const TimeInvariant timeInvariant)

src/Core/TAPN/TimedTransition.cpp

@@ -7,35 +7,35 @@ namespace VerifyTAPN {
 			out << GetName() << "(" << index << ")";
 		}
 
-		void TimedTransition::AddToPreset(const boost::shared_ptr<TimedInputArc>& arc)
+		void TimedTransition::AddToPreset(const std::shared_ptr<TimedInputArc>& arc)
 		{
 			if(arc)
 			{
-				preset.push_back(arc);
+				preset.push_back(arc.get());
 			}
 		}
 
-		void TimedTransition::AddTransportArcGoingThrough(const boost::shared_ptr<TransportArc>& arc)
+		void TimedTransition::AddTransportArcGoingThrough(const std::shared_ptr<TransportArc>& arc)
 		{
 			if(arc)
 			{
-				transportArcs.push_back(arc);
+				transportArcs.push_back(arc.get());
 			}
 		}
 
-		void TimedTransition::AddIncomingInhibitorArc(const boost::shared_ptr<InhibitorArc>& arc)
+		void TimedTransition::AddIncomingInhibitorArc(const std::shared_ptr<InhibitorArc>& arc)
 		{
 			if(arc)
 			{
-				inhibitorArcs.push_back(arc);
+				inhibitorArcs.push_back(arc.get());
 			}
 		}
 
-		void TimedTransition::AddToPostset(const boost::shared_ptr<OutputArc>& arc)
+		void TimedTransition::AddToPostset(const std::shared_ptr<OutputArc>& arc)
 		{
 			if(arc)
 			{
-				postset.push_back(arc);
+				postset.push_back(arc.get());
 			}
 		}
 	}