diff --git a/src/Core/ArgsParser.cpp b/src/Core/ArgsParser.cpp index 904045b..59cfabf 100644 --- a/src/Core/ArgsParser.cpp +++ b/src/Core/ArgsParser.cpp @@ -3,7 +3,6 @@ #include #include "boost/algorithm/string.hpp" #include "boost/lexical_cast.hpp" -#include "boost/make_shared.hpp" #include #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("k", KBOUND_OPTION, "Max tokens to use during exploration.",0)); - parsers.push_back(boost::make_shared("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("t", TRACE_OPTION, "Specify the desired trace option.\n - 0: none\n - 1: some",0)); + parsers.push_back(std::make_shared("k", KBOUND_OPTION, "Max tokens to use during exploration.",0)); + parsers.push_back(std::make_shared("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("t", TRACE_OPTION, "Specify the desired trace option.\n - 0: none\n - 1: some",0)); - parsers.push_back(boost::make_shared("g",MAX_CONSTANT_OPTION, "Use global maximum constant for \nextrapolation (as opposed to local \nconstants).")); - parsers.push_back(boost::make_shared("u",UNTIMED_PLACES_OPTION, "Disables the untimed place optimization.")); - parsers.push_back(boost::make_shared("s",SYMMETRY_OPTION, "Disables symmetry reduction.")); + parsers.push_back(std::make_shared("g",MAX_CONSTANT_OPTION, "Use global maximum constant for \nextrapolation (as opposed to local \nconstants).")); + parsers.push_back(std::make_shared("u",UNTIMED_PLACES_OPTION, "Disables the untimed place optimization.")); + parsers.push_back(std::make_shared("s",SYMMETRY_OPTION, "Disables symmetry reduction.")); - parsers.push_back(boost::make_shared("x",XML_TRACE_OPTION, "Output trace in xml format for TAPAAL.")); + parsers.push_back(std::make_shared("x",XML_TRACE_OPTION, "Output trace in xml format for TAPAAL.")); - parsers.push_back(boost::make_shared("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("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("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("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 diff --git a/src/Core/ArgsParser.hpp b/src/Core/ArgsParser.hpp index 96120ce..9f9f2b4 100644 --- a/src/Core/ArgsParser.hpp +++ b/src/Core/ArgsParser.hpp @@ -1,13 +1,14 @@ #ifndef ARGSPARSER_HPP_ #define ARGSPARSER_HPP_ +#include "VerificationOptions.hpp" +#include "boost/lexical_cast.hpp" + #include #include #include #include -#include "boost/smart_ptr.hpp" -#include "VerificationOptions.hpp" -#include "boost/lexical_cast.hpp" +#include namespace VerifyTAPN { @@ -65,7 +66,7 @@ namespace VerifyTAPN }; class ArgsParser { - typedef std::vector< boost::shared_ptr > parser_vec; + typedef std::vector< std::shared_ptr > parser_vec; public: ArgsParser() : parsers() { Initialize(); }; virtual ~ArgsParser() {}; diff --git a/src/Core/QueryParser/ToStringVisitor.hpp b/src/Core/QueryParser/ToStringVisitor.hpp index 60f356f..461882d 100644 --- a/src/Core/QueryParser/ToStringVisitor.hpp +++ b/src/Core/QueryParser/ToStringVisitor.hpp @@ -13,7 +13,7 @@ namespace VerifyTAPN class ToStringVisitor : public Visitor { public: - ToStringVisitor(const boost::shared_ptr& tapn) : tapn(tapn) { }; + ToStringVisitor(const std::shared_ptr& 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; + const std::shared_ptr tapn; }; } } diff --git a/src/Core/SymbolicMarking/DBMMarking.cpp b/src/Core/SymbolicMarking/DBMMarking.cpp index d656335..945fd5b 100644 --- a/src/Core/SymbolicMarking/DBMMarking.cpp +++ b/src/Core/SymbolicMarking/DBMMarking.cpp @@ -4,7 +4,7 @@ namespace VerifyTAPN { - boost::shared_ptr DBMMarking::tapn; + std::shared_ptr DBMMarking::tapn; // Add a token in each output place of placesOfTokensToAdd // and add placesOfTokensToAdd.size() clocks to the DBM. diff --git a/src/Core/SymbolicMarking/DBMMarking.hpp b/src/Core/SymbolicMarking/DBMMarking.hpp index bf13772..5fac43f 100644 --- a/src/Core/SymbolicMarking/DBMMarking.hpp +++ b/src/Core/SymbolicMarking/DBMMarking.hpp @@ -15,7 +15,7 @@ namespace VerifyTAPN { friend class UppaalDBMMarkingFactory; friend class DiscreteInclusionMarkingFactory; public: - static boost::shared_ptr tapn; + static std::shared_ptr 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()); }; diff --git a/src/Core/SymbolicMarking/DiscreteInclusionMarkingFactory.hpp b/src/Core/SymbolicMarking/DiscreteInclusionMarkingFactory.hpp index a5bef1d..36d9d5d 100644 --- a/src/Core/SymbolicMarking/DiscreteInclusionMarkingFactory.hpp +++ b/src/Core/SymbolicMarking/DiscreteInclusionMarkingFactory.hpp @@ -13,7 +13,7 @@ namespace VerifyTAPN { class DiscreteInclusionMarkingFactory : public UppaalDBMMarkingFactory { public: - DiscreteInclusionMarkingFactory(const boost::shared_ptr& tapn, const VerificationOptions& options) + DiscreteInclusionMarkingFactory(const std::shared_ptr& 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; + std::shared_ptr tapn; std::vector inc_places; bool empty_inc; }; diff --git a/src/Core/SymbolicMarking/UppaalDBMMarkingFactory.hpp b/src/Core/SymbolicMarking/UppaalDBMMarkingFactory.hpp index aaddf2d..9287c8a 100644 --- a/src/Core/SymbolicMarking/UppaalDBMMarkingFactory.hpp +++ b/src/Core/SymbolicMarking/UppaalDBMMarkingFactory.hpp @@ -11,7 +11,7 @@ namespace VerifyTAPN { protected: static id_type nextId; public: - UppaalDBMMarkingFactory(const boost::shared_ptr& tapn) + UppaalDBMMarkingFactory(const std::shared_ptr& tapn) { DBMMarking::tapn = tapn; }; diff --git a/src/Core/TAPN/InhibitorArc.hpp b/src/Core/TAPN/InhibitorArc.hpp index 1d1b6e4..e0cf0db 100644 --- a/src/Core/TAPN/InhibitorArc.hpp +++ b/src/Core/TAPN/InhibitorArc.hpp @@ -1,9 +1,10 @@ #ifndef INHIBITORARC_HPP_ #define INHIBITORARC_HPP_ -#include #include "TimeInterval.hpp" -#include "boost/smart_ptr.hpp" + +#include +#include namespace VerifyTAPN { namespace TAPN { @@ -12,10 +13,10 @@ namespace VerifyTAPN { class InhibitorArc { public: // typedefs - typedef std::vector< boost::shared_ptr > Vector; - typedef std::vector< boost::weak_ptr > WeakPtrVector; + typedef std::vector< std::shared_ptr > Vector; + typedef std::vector< InhibitorArc* > NakedPtrVector; public: - InhibitorArc(const boost::shared_ptr& place, const boost::shared_ptr& transition) : place(place), transition(transition) { }; + InhibitorArc(const std::shared_ptr& place, const std::shared_ptr& 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 place; - const boost::shared_ptr transition; + const std::shared_ptr place; + const std::shared_ptr transition; }; inline std::ostream& operator<<(std::ostream& out, const InhibitorArc& arc) diff --git a/src/Core/TAPN/OutputArc.hpp b/src/Core/TAPN/OutputArc.hpp index 1272aa8..3843f78 100644 --- a/src/Core/TAPN/OutputArc.hpp +++ b/src/Core/TAPN/OutputArc.hpp @@ -2,7 +2,7 @@ #define VERIFYTAPN_TAPN_OUTPUTARC_HPP_ #include -#include "boost/smart_ptr.hpp" +#include namespace VerifyTAPN { namespace TAPN { @@ -12,10 +12,10 @@ namespace VerifyTAPN { class OutputArc { public: // typedefs - typedef std::vector< boost::shared_ptr > Vector; - typedef std::vector< boost::weak_ptr > WeakPtrVector; + typedef std::vector< std::shared_ptr > Vector; + typedef std::vector< OutputArc* > NakedPtrVector; public: - OutputArc(const boost::shared_ptr& transition, const boost::shared_ptr& place) + OutputArc(const std::shared_ptr& transition, const std::shared_ptr& 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 transition; - const boost::shared_ptr place; + const std::shared_ptr transition; + const std::shared_ptr place; }; inline std::ostream& operator<<(std::ostream& out, const OutputArc& arc) diff --git a/src/Core/TAPN/Pairing.cpp b/src/Core/TAPN/Pairing.cpp index 065ab8f..e94fb81 100644 --- a/src/Core/TAPN/Pairing.cpp +++ b/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,8 +19,8 @@ using namespace TAPN; { if(i < preset.size() && i < postset.size()) { - boost::shared_ptr tiaPtr = preset[i].lock(); - boost::shared_ptr oaPtr = postset[i].lock(); + TimedInputArc* tiaPtr = preset[i]; + OutputArc* oaPtr = postset[i]; inputPlace = tapn.GetPlaceIndex(tiaPtr->InputPlace()); outputPlace = tapn.GetPlaceIndex(oaPtr->OutputPlace()); @@ -28,14 +28,14 @@ using namespace TAPN; Add(inputPlace, outputPlace); } else if(i < preset.size() && i >= postset.size()){ - boost::shared_ptr 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 oaPtr = postset[i].lock(); + OutputArc* oaPtr = postset[i]; outputPlace = tapn.GetPlaceIndex(oaPtr->OutputPlace()); diff --git a/src/Core/TAPN/TimedArcPetriNet.cpp b/src/Core/TAPN/TimedArcPetriNet.cpp index 39099c3..6563416 100644 --- a/src/Core/TAPN/TimedArcPetriNet.cpp +++ b/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& arc = *iter; + const std::shared_ptr& 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& arc = *iter; + const std::shared_ptr& 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& arc = *iter; + const std::shared_ptr& 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& arc = *iter; + const std::shared_ptr& arc = *iter; arc->InputTransition().AddToPostset(arc); } @@ -115,7 +115,7 @@ namespace VerifyTAPN { { if((*arcIter)->InputPlace() == **iter) { - boost::shared_ptr ia = *arcIter; + std::shared_ptr ia = *arcIter; const TAPN::TimeInterval& interval = ia->Interval(); const int lowerBound = interval.GetLowerBound(); diff --git a/src/Core/TAPN/TimedArcPetriNet.hpp b/src/Core/TAPN/TimedArcPetriNet.hpp index 2464ab7..b1f5ec5 100644 --- a/src/Core/TAPN/TimedArcPetriNet.hpp +++ b/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" diff --git a/src/Core/TAPN/TimedInputArc.hpp b/src/Core/TAPN/TimedInputArc.hpp index dbe41e3..0489fe7 100644 --- a/src/Core/TAPN/TimedInputArc.hpp +++ b/src/Core/TAPN/TimedInputArc.hpp @@ -1,9 +1,10 @@ #ifndef VERIFYTAPN_TAPN_TIMEDINPUTARC_HPP_ #define VERIFYTAPN_TAPN_TIMEDINPUTARC_HPP_ -#include #include "TimeInterval.hpp" -#include "boost/smart_ptr.hpp" + +#include +#include namespace VerifyTAPN { namespace TAPN { @@ -13,11 +14,11 @@ namespace VerifyTAPN { class TimedInputArc { public: // typedefs - typedef std::vector< boost::shared_ptr > Vector; - typedef std::vector< boost::weak_ptr > WeakPtrVector; + typedef std::vector< std::shared_ptr > Vector; + typedef std::vector< TimedInputArc* > NakedPtrVector; public: - TimedInputArc(const boost::shared_ptr& place, const boost::shared_ptr& transition) : interval(), place(place), transition(transition) { }; - TimedInputArc(const boost::shared_ptr& place, const boost::shared_ptr& transition, const TimeInterval& interval) : interval(interval), place(place), transition(transition) { }; + TimedInputArc(const std::shared_ptr& place, const std::shared_ptr& transition) : interval(), place(place), transition(transition) { }; + TimedInputArc(const std::shared_ptr& place, const std::shared_ptr& 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 place; - const boost::shared_ptr transition; + const std::shared_ptr place; + const std::shared_ptr transition; }; inline std::ostream& operator<<(std::ostream& out, const TimedInputArc& arc) diff --git a/src/Core/TAPN/TimedPlace.hpp b/src/Core/TAPN/TimedPlace.hpp index 6e869a8..d82d058 100644 --- a/src/Core/TAPN/TimedPlace.hpp +++ b/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 > Vector; + typedef std::vector< std::shared_ptr > Vector; public: // construction / destruction TimedPlace(const std::string& name, const std::string& id, const TimeInvariant timeInvariant) diff --git a/src/Core/TAPN/TimedTransition.cpp b/src/Core/TAPN/TimedTransition.cpp index 834e78d..31dd9ab 100644 --- a/src/Core/TAPN/TimedTransition.cpp +++ b/src/Core/TAPN/TimedTransition.cpp @@ -7,35 +7,35 @@ namespace VerifyTAPN { out << GetName() << "(" << index << ")"; } - void TimedTransition::AddToPreset(const boost::shared_ptr& arc) + void TimedTransition::AddToPreset(const std::shared_ptr& arc) { if(arc) { - preset.push_back(arc); + preset.push_back(arc.get()); } } - void TimedTransition::AddTransportArcGoingThrough(const boost::shared_ptr& arc) + void TimedTransition::AddTransportArcGoingThrough(const std::shared_ptr& arc) { if(arc) { - transportArcs.push_back(arc); + transportArcs.push_back(arc.get()); } } - void TimedTransition::AddIncomingInhibitorArc(const boost::shared_ptr& arc) + void TimedTransition::AddIncomingInhibitorArc(const std::shared_ptr& arc) { if(arc) { - inhibitorArcs.push_back(arc); + inhibitorArcs.push_back(arc.get()); } } - void TimedTransition::AddToPostset(const boost::shared_ptr& arc) + void TimedTransition::AddToPostset(const std::shared_ptr& arc) { if(arc) { - postset.push_back(arc); + postset.push_back(arc.get()); } } } diff --git a/src/Core/TAPN/TimedTransition.hpp b/src/Core/TAPN/TimedTransition.hpp index f18ba31..a2a6026 100644 --- a/src/Core/TAPN/TimedTransition.hpp +++ b/src/Core/TAPN/TimedTransition.hpp @@ -1,13 +1,15 @@ #ifndef VERIFYTAPN_TAPN_TIMEDTRANSITION_HPP_ #define VERIFYTAPN_TAPN_TIMEDTRANSITION_HPP_ -#include -#include #include "TimedInputArc.hpp" #include "TransportArc.hpp" #include "InhibitorArc.hpp" #include "OutputArc.hpp" -#include "boost/shared_ptr.hpp" + +#include +#include +#include + namespace VerifyTAPN { @@ -19,28 +21,28 @@ class SymMarking; class TimedTransition { public: // typedefs - typedef std::vector< boost::shared_ptr > Vector; + typedef std::vector< std::shared_ptr > Vector; public: TimedTransition(const std::string& name, const std::string& id) : name(name), id(id), preset(), postset(), transportArcs(), index(-1) { }; TimedTransition() : name("*EMPTY*"), id("-1"), preset(), postset(), transportArcs(), index(-1) { }; virtual ~TimedTransition() { /* empty */ } public: // modifiers - void AddToPreset(const boost::shared_ptr& arc); - void AddToPostset(const boost::shared_ptr& arc); - void AddTransportArcGoingThrough(const boost::shared_ptr& arc); - void AddIncomingInhibitorArc(const boost::shared_ptr& arc); + void AddToPreset(const std::shared_ptr& arc); + void AddToPostset(const std::shared_ptr& arc); + void AddTransportArcGoingThrough(const std::shared_ptr& arc); + void AddIncomingInhibitorArc(const std::shared_ptr& arc); inline void SetIndex(int i) { index = i; }; public: // inspectors inline const std::string& GetName() const { return name; }; inline const std::string& GetId() const { return id; }; void Print(std::ostream&) const; - inline const TimedInputArc::WeakPtrVector& GetPreset() const { return preset; } - inline const TransportArc::WeakPtrVector& GetTransportArcs() const { return transportArcs; } - inline const InhibitorArc::WeakPtrVector& GetInhibitorArcs() const { return inhibitorArcs; } + inline const TimedInputArc::NakedPtrVector& GetPreset() const { return preset; } + inline const TransportArc::NakedPtrVector& GetTransportArcs() const { return transportArcs; } + inline const InhibitorArc::NakedPtrVector& GetInhibitorArcs() const { return inhibitorArcs; } inline const unsigned int GetPresetSize() const { return NumberOfInputArcs() + NumberOfTransportArcs(); } - inline const OutputArc::WeakPtrVector& GetPostset() const { return postset; } + inline const OutputArc::NakedPtrVector& GetPostset() const { return postset; } inline const unsigned int GetPostsetSize() const { return postset.size() + transportArcs.size(); } inline unsigned int NumberOfInputArcs() const { return preset.size(); }; inline unsigned int NumberOfTransportArcs() const { return transportArcs.size(); }; @@ -51,10 +53,10 @@ class SymMarking; private: // data std::string name; std::string id; - TimedInputArc::WeakPtrVector preset; - OutputArc::WeakPtrVector postset; - TransportArc::WeakPtrVector transportArcs; - InhibitorArc::WeakPtrVector inhibitorArcs; + TimedInputArc::NakedPtrVector preset; + OutputArc::NakedPtrVector postset; + TransportArc::NakedPtrVector transportArcs; + InhibitorArc::NakedPtrVector inhibitorArcs; unsigned int index; }; diff --git a/src/Core/TAPN/TransportArc.hpp b/src/Core/TAPN/TransportArc.hpp index 281a93e..95349b3 100644 --- a/src/Core/TAPN/TransportArc.hpp +++ b/src/Core/TAPN/TransportArc.hpp @@ -1,9 +1,10 @@ #ifndef TRANSPORTARC_HPP_ #define TRANSPORTARC_HPP_ -#include #include "TimeInterval.hpp" -#include "boost/smart_ptr.hpp" + +#include +#include namespace VerifyTAPN { @@ -15,13 +16,13 @@ namespace VerifyTAPN class TransportArc { public: - typedef std::vector< boost::shared_ptr > Vector; - typedef std::vector< boost::weak_ptr > WeakPtrVector; + typedef std::vector< std::shared_ptr > Vector; + typedef std::vector< TransportArc* > NakedPtrVector; public: TransportArc( - const boost::shared_ptr& source, - const boost::shared_ptr& transition, - const boost::shared_ptr& destination, + const std::shared_ptr& source, + const std::shared_ptr& transition, + const std::shared_ptr& destination, const TAPN::TimeInterval& interval ) : interval(interval), source(source), transition(transition), destination(destination) {}; @@ -36,9 +37,9 @@ namespace VerifyTAPN void Print(std::ostream& out) const; private: const TAPN::TimeInterval interval; - const boost::shared_ptr source; - const boost::shared_ptr transition; - const boost::shared_ptr destination; + const std::shared_ptr source; + const std::shared_ptr transition; + const std::shared_ptr destination; }; inline std::ostream& operator<<(std::ostream& out, const TransportArc& arc) diff --git a/src/Core/TAPNParser/TAPNXmlParser.cpp b/src/Core/TAPNParser/TAPNXmlParser.cpp index 808cfd5..f5330b0 100644 --- a/src/Core/TAPNParser/TAPNXmlParser.cpp +++ b/src/Core/TAPNParser/TAPNXmlParser.cpp @@ -1,6 +1,9 @@ #include "TAPNXmlParser.hpp" + #include #include +#include + #include "boost/bind.hpp" #include "boost/algorithm/string.hpp" #include "boost/lexical_cast.hpp" @@ -11,7 +14,7 @@ namespace VerifyTAPN { using namespace rapidxml; - boost::shared_ptr TAPNXmlParser::Parse(const std::string & filename) const + std::shared_ptr TAPNXmlParser::Parse(const std::string & filename) const { const std::string contents = VerifyTAPN::ReadFile(filename); std::vector charArray(contents.begin(), contents.end()); @@ -43,14 +46,14 @@ namespace VerifyTAPN { return ParseInitialMarking(*root, tapn); } - boost::shared_ptr TAPNXmlParser::ParseTAPN(const xml_node<>& root) const + std::shared_ptr TAPNXmlParser::ParseTAPN(const xml_node<>& root) const { TimedPlace::Vector places = ParsePlaces(root); TimedTransition::Vector transitions = ParseTransitions(root); TAPNXmlParser::ArcCollections arcs = ParseArcs(root, places, transitions); - boost::shared_ptr tapn = boost::make_shared(places, transitions, arcs.inputArcs, arcs.outputArcs, arcs.transportArcs, arcs.inhibitorArcs); + std::shared_ptr tapn = std::make_shared(places, transitions, arcs.inputArcs, arcs.outputArcs, arcs.transportArcs, arcs.inhibitorArcs); return tapn; } @@ -61,7 +64,7 @@ namespace VerifyTAPN { xml_node<>* placeNode = root.first_node("place"); while(placeNode != NULL){ - boost::shared_ptr place = ParsePlace(*placeNode); + std::shared_ptr place = ParsePlace(*placeNode); places.push_back(place); placeNode = placeNode->next_sibling("place"); } @@ -69,14 +72,14 @@ namespace VerifyTAPN { return places; } - boost::shared_ptr TAPNXmlParser::ParsePlace(const xml_node<>& placeNode) const + std::shared_ptr TAPNXmlParser::ParsePlace(const xml_node<>& placeNode) const { std::string id(placeNode.first_attribute("id")->value()); std::string name(placeNode.first_attribute("name")->value()); std::string invariantNode = placeNode.first_attribute("invariant")->value(); TimeInvariant timeInvariant = TimeInvariant::CreateFor(invariantNode); - return boost::make_shared(name, id, timeInvariant); + return std::make_shared(name, id, timeInvariant); } TimedTransition::Vector TAPNXmlParser::ParseTransitions(const xml_node<>& root) const @@ -85,7 +88,7 @@ namespace VerifyTAPN { xml_node<>* transitionNode = root.first_node("transition"); while(transitionNode != NULL){ - boost::shared_ptr transition = ParseTransition(*transitionNode); + std::shared_ptr transition = ParseTransition(*transitionNode); transitions.push_back(transition); transitionNode = transitionNode->next_sibling("transition"); } @@ -93,11 +96,11 @@ namespace VerifyTAPN { return transitions; } - boost::shared_ptr TAPNXmlParser::ParseTransition(const xml_node<>& transitionNode) const + std::shared_ptr TAPNXmlParser::ParseTransition(const xml_node<>& transitionNode) const { std::string id(transitionNode.first_attribute("id")->value()); std::string name(transitionNode.first_attribute("name")->value()); - return boost::make_shared(name, id); + return std::make_shared(name, id); } TAPNXmlParser::ArcCollections TAPNXmlParser::ParseArcs(const xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const @@ -157,7 +160,7 @@ namespace VerifyTAPN { return outputArcs; } - boost::shared_ptr TAPNXmlParser::ParseInputArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const + std::shared_ptr TAPNXmlParser::ParseInputArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const { std::string source = arcNode.first_attribute("source")->value(); std::string target = arcNode.first_attribute("target")->value(); @@ -166,10 +169,10 @@ namespace VerifyTAPN { TimedPlace::Vector::const_iterator place = find_if(places.begin(), places.end(), boost::bind(boost::mem_fn(&TimedPlace::GetId), _1) == source); TimedTransition::Vector::const_iterator transition = find_if(transitions.begin(), transitions.end(), boost::bind(boost::mem_fn(&TimedTransition::GetId), _1) == target); - return boost::make_shared(*place, *transition, TimeInterval::CreateFor(interval)); + return std::make_shared(*place, *transition, TimeInterval::CreateFor(interval)); } - boost::shared_ptr TAPNXmlParser::ParseTransportArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const + std::shared_ptr TAPNXmlParser::ParseTransportArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const { std::string sourceName = arcNode.first_attribute("source")->value(); std::string transitionName = arcNode.first_attribute("transition")->value(); @@ -179,10 +182,10 @@ namespace VerifyTAPN { TimedPlace::Vector::const_iterator source = find_if(places.begin(), places.end(), boost::bind(boost::mem_fn(&TimedPlace::GetId), _1) == sourceName); TimedTransition::Vector::const_iterator transition = find_if(transitions.begin(), transitions.end(), boost::bind(boost::mem_fn(&TimedTransition::GetId), _1) == transitionName); TimedPlace::Vector::const_iterator target = find_if(places.begin(), places.end(), boost::bind(boost::mem_fn(&TimedPlace::GetId), _1) == targetName); - return boost::make_shared(*source, *transition, *target, TimeInterval::CreateFor(interval)); + return std::make_shared(*source, *transition, *target, TimeInterval::CreateFor(interval)); } - boost::shared_ptr TAPNXmlParser::ParseInhibitorArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const + std::shared_ptr TAPNXmlParser::ParseInhibitorArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const { std::string source = arcNode.first_attribute("source")->value(); std::string target = arcNode.first_attribute("target")->value(); @@ -190,10 +193,10 @@ namespace VerifyTAPN { TimedPlace::Vector::const_iterator place = find_if(places.begin(), places.end(), boost::bind(boost::mem_fn(&TimedPlace::GetId), _1) == source); TimedTransition::Vector::const_iterator transition = find_if(transitions.begin(), transitions.end(), boost::bind(boost::mem_fn(&TimedTransition::GetId), _1) == target); - return boost::make_shared(*place, *transition); + return std::make_shared(*place, *transition); } - boost::shared_ptr TAPNXmlParser::ParseOutputArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const + std::shared_ptr TAPNXmlParser::ParseOutputArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const { std::string source = arcNode.first_attribute("source")->value(); std::string target = arcNode.first_attribute("target")->value(); @@ -201,7 +204,7 @@ namespace VerifyTAPN { TimedTransition::Vector::const_iterator transition = find_if(transitions.begin(), transitions.end(), boost::bind(boost::mem_fn(&TimedTransition::GetId), _1) == source); TimedPlace::Vector::const_iterator place = find_if(places.begin(), places.end(), boost::bind(boost::mem_fn(&TimedPlace::GetId), _1) == target); - return boost::make_shared(*transition, *place); + return std::make_shared(*transition, *place); } diff --git a/src/Core/TAPNParser/TAPNXmlParser.hpp b/src/Core/TAPNParser/TAPNXmlParser.hpp index b734472..96d5289 100644 --- a/src/Core/TAPNParser/TAPNXmlParser.hpp +++ b/src/Core/TAPNParser/TAPNXmlParser.hpp @@ -3,7 +3,6 @@ #include "../TAPN/TAPN.hpp" -#include #include namespace VerifyTAPN { @@ -28,26 +27,26 @@ namespace VerifyTAPN { virtual ~TAPNXmlParser() { /* empty */ }; public: - boost::shared_ptr Parse(const std::string & filename) const; + std::shared_ptr Parse(const std::string & filename) const; std::vector ParseMarking(const std::string & filename, const TimedArcPetriNet& tapn) const; private: - boost::shared_ptr ParseTAPN(const rapidxml::xml_node<> & root) const; + std::shared_ptr ParseTAPN(const rapidxml::xml_node<> & root) const; TimedPlace::Vector ParsePlaces(const rapidxml::xml_node<>& root) const; - boost::shared_ptr ParsePlace(const rapidxml::xml_node<>& placeNode) const; + std::shared_ptr ParsePlace(const rapidxml::xml_node<>& placeNode) const; TimedTransition::Vector ParseTransitions(const rapidxml::xml_node<>& root) const; - boost::shared_ptr ParseTransition(const rapidxml::xml_node<>& transitionNode) const; + std::shared_ptr ParseTransition(const rapidxml::xml_node<>& transitionNode) const; ArcCollections ParseArcs(const rapidxml::xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const; TransportArc::Vector ParseTransportArcs(const rapidxml::xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const; InhibitorArc::Vector ParseInhibitorArcs(const rapidxml::xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const; TimedInputArc::Vector ParseInputArcs(const rapidxml::xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const; OutputArc::Vector ParseOutputArcs(const rapidxml::xml_node<>& root, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const; - boost::shared_ptr ParseInputArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const; - boost::shared_ptr ParseInhibitorArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const; - boost::shared_ptr ParseTransportArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const; - boost::shared_ptr ParseOutputArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const; + std::shared_ptr ParseInputArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const; + std::shared_ptr ParseInhibitorArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const; + std::shared_ptr ParseTransportArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const; + std::shared_ptr ParseOutputArc(const rapidxml::xml_node<>& arcNode, const TimedPlace::Vector& places, const TimedTransition::Vector& transitions) const; std::vector ParseInitialMarking(const rapidxml::xml_node<>& root, const TimedArcPetriNet& tapn) const; }; } diff --git a/src/ReachabilityChecker/SuccessorGenerator.cpp b/src/ReachabilityChecker/SuccessorGenerator.cpp index ba361e0..3cb50bd 100644 --- a/src/ReachabilityChecker/SuccessorGenerator.cpp +++ b/src/ReachabilityChecker/SuccessorGenerator.cpp @@ -2,6 +2,7 @@ #include "../Core/TAPN/TimedInputArc.hpp" #include "../Core/TAPN/Pairing.hpp" #include "../Core/SymbolicMarking/SymbolicMarking.hpp" + #include #include @@ -36,7 +37,7 @@ namespace VerifyTAPN { assert(nTokensFromCurrInputPlace <= static_cast(options.GetKBound())); arcsArray[currInputArcIdx] = arcsArray[currInputArcIdx] + 1; - tokenIndices->insert_element(currInputArcIdx,nTokensFromCurrInputPlace, i); + tokenIndices[toIndex(currInputArcIdx, nTokensFromCurrInputPlace)] = i; nTokensFromCurrInputPlace++; } } @@ -50,12 +51,10 @@ namespace VerifyTAPN { { unsigned int currInputArcIdx = 0; - for(TAPN::TimedTransition::Vector::const_iterator iter = transitions.begin(); iter != transitions.end(); ++iter) + for(auto& trans : transitions) { - const TAPN::TransportArc::WeakPtrVector& transportArcs = (*iter)->GetTransportArcs(); - for(TAPN::TransportArc::WeakPtrVector::const_iterator presetIter = transportArcs.begin(); presetIter != transportArcs.end(); ++presetIter) + for(auto* ta : trans->GetTransportArcs()) { - boost::shared_ptr ta = (*presetIter).lock(); const TAPN::TimeInterval& ti = ta->Interval(); int currInputPlaceIndex = tapn.GetPlaceIndex(ta->Source()); @@ -63,10 +62,8 @@ namespace VerifyTAPN { currInputArcIdx++; } - const TAPN::TimedInputArc::WeakPtrVector& preset = (*iter)->GetPreset(); - for(TAPN::TimedInputArc::WeakPtrVector::const_iterator presetIter = preset.begin(); presetIter != preset.end(); ++presetIter) + for(auto* ia : trans->GetPreset()) { - boost::shared_ptr ia = (*presetIter).lock(); const TAPN::TimeInterval& ti = ia->Interval(); int currInputPlaceIndex = tapn.GetPlaceIndex(ia->InputPlace()); @@ -103,7 +100,7 @@ namespace VerifyTAPN { // Generate next permutation of input tokens int j = presetSize - 1; - if (j<0) { break; } + if (j<0) { break; } while(true) { @@ -134,10 +131,8 @@ namespace VerifyTAPN { // along with the size of the preset of the transition bool SuccessorGenerator::IsTransitionEnabled(const TAPN::TimedTransition& transition, const SymbolicMarking* marking, unsigned int currTransitionIndex, unsigned int presetSize) const { - const TAPN::InhibitorArc::WeakPtrVector& inhibitorArcs = transition.GetInhibitorArcs(); - for(TAPN::InhibitorArc::WeakPtrVector::const_iterator iter = inhibitorArcs.begin(); iter != inhibitorArcs.end(); ++iter) + for(auto* ia : transition.GetInhibitorArcs()) { - boost::shared_ptr ia = iter->lock(); int sourcePlaceIndex = ia->InputPlace().GetIndex(); for(unsigned int i = 0; i < marking->NumberOfTokens(); i++) @@ -162,16 +157,16 @@ namespace VerifyTAPN { bool trace = options.GetTrace() != NONE; const Pairing& pairing = tapn.GetPairing(transition); - const TAPN::TimedInputArc::WeakPtrVector& preset = transition.GetPreset(); + const TAPN::TimedInputArc::NakedPtrVector& preset = transition.GetPreset(); std::set tokensToRemove; // sets are sorted internally in ascending order. THIS MUST BE THE CASE OR THE CODE WONT WORK! SymbolicMarking* next = factory.Clone(*marking); for(unsigned int i = 0; i < transition.NumberOfTransportArcs(); ++i) { - boost::shared_ptr ta = transition.GetTransportArcs()[i].lock(); + TAPN::TransportArc* ta = transition.GetTransportArcs()[i]; const TAPN::TimeInterval& ti = ta->Interval(); - int tokenIndex = tokenIndices->at_element(currentTransitionIndex+i, currentPermutationindices[i]); + int tokenIndex = tokenIndices[toIndex(currentTransitionIndex+i, currentPermutationindices[i])]; int outputPlaceIndex = tapn.GetPlaceIndex(ta->Destination()); // constrain dbm with the guard of the input arc @@ -190,7 +185,7 @@ namespace VerifyTAPN { // move all tokens that are currently in the net for(unsigned int i = 0; i < transition.NumberOfInputArcs(); ++i) { - boost::shared_ptr inputArc = preset[i].lock(); + auto* inputArc = preset[i]; int inputPlace = tapn.GetPlaceIndex(inputArc->InputPlace()); const TAPN::TimeInterval& ti = inputArc->Interval(); const std::list& outputPlaces = pairing.GetOutputPlacesFor(inputPlace); @@ -198,11 +193,10 @@ namespace VerifyTAPN { // only BOTTOM is allowed to have more than 1 associated output place assert(outputPlaces.size() <= 1); - for(std::list::const_iterator opIter = outputPlaces.begin(); opIter != outputPlaces.end(); ++opIter) + for(auto outputPlaceIndex : outputPlaces) { // change placement - int tokenIndex = tokenIndices->at_element(currentTransitionIndex+offset+i, currentPermutationindices[offset+i]); - int outputPlaceIndex = *opIter; + int tokenIndex = tokenIndices[toIndex(currentTransitionIndex+offset+i, currentPermutationindices[offset+i])]; // constrain dbm with the guard of the input arc next->Constrain(tokenIndex, ti); @@ -222,7 +216,7 @@ namespace VerifyTAPN { // reset clocks of moved tokens for (unsigned int i = transition.NumberOfTransportArcs(); i < presetSize; ++i) { - int tokenIndex = tokenIndices->at_element(currentTransitionIndex+i, currentPermutationindices[i]); + int tokenIndex = tokenIndices[toIndex(currentTransitionIndex+i, currentPermutationindices[i])]; next->Reset(tokenIndex); } @@ -278,14 +272,14 @@ namespace VerifyTAPN { // handle transport arcs for(unsigned int i = 0; i < transition.NumberOfTransportArcs(); i++) { - int tokenIndex = tokenIndices->at_element(currentTransitionIndex+i, currentPermutationindices[i]); - boost::shared_ptr ia = transition.GetTransportArcs()[i].lock(); + int tokenIndex = tokenIndices[toIndex(currentTransitionIndex+i, currentPermutationindices[i])]; + TAPN::TransportArc* ia = transition.GetTransportArcs()[i]; const TAPN::TimeInterval& ti = ia->Interval(); int indexAfterFiring = tokenIndex; - for(std::set::iterator iter = tokensToRemove.begin(); iter != tokensToRemove.end(); ++iter) + for(auto to_remove : tokensToRemove) { - if(*iter < tokenIndex) indexAfterFiring--; - assert(*iter != tokenIndex); + if(to_remove < tokenIndex) indexAfterFiring--; + assert(to_remove != tokenIndex); } assert(tokenIndex < static_cast(marking->NumberOfTokens())); assert(indexAfterFiring < static_cast(next->NumberOfTokens())); @@ -297,8 +291,8 @@ namespace VerifyTAPN { // handle normal arcs for(unsigned int i = 0; i < transition.NumberOfInputArcs(); ++i) { - int tokenIndex = tokenIndices->at_element(currentTransitionIndex+offset+i, currentPermutationindices[offset+i]); - boost::shared_ptr ia = preset[i].lock(); + int tokenIndex = tokenIndices[toIndex(currentTransitionIndex+offset+i, currentPermutationindices[offset+i])]; + TAPN::TimedInputArc* ia = preset[i]; const TAPN::TimeInterval& ti = ia->Interval(); int indexAfterFiring = tokenIndex; for(std::set::iterator iter = tokensToRemove.begin(); iter != tokensToRemove.end(); ++iter) @@ -372,46 +366,6 @@ namespace VerifyTAPN { mapping.Swap(table); } -// void SuccessorGenerator::InvertMapping(std::vector& mapping) const -// { -// std::vector inverted(mapping.size(),-1); -// unsigned int count = 0; -// for(unsigned int i = 0; i < mapping.size(); ++i) -// { -// int index = mapping[i]; -// if(index >= 0) -// { -// inverted[index] = i; -// count++; -// } -// } -// inverted.resize(count); -// mapping.swap(inverted); -// } - - - void SuccessorGenerator::Print(std::ostream& out) const - { - out << "\nArcs Array:\n"; - out << "------------------\n"; - - for(unsigned int i = 0; i < nInputArcs; i++) - { - out << i << ": " << arcsArray[i] << "\n"; - } - - out << "\nTransitions Array:\n"; - out << "------------------\n"; - for(int j =0;j< numberOfTransitions;j++){ - out << j << ": " << transitionStatistics[j] << "\n"; - } - - out << "\n\nToken Indices:\n"; - out << "----------------------\n"; - - out << *tokenIndices << "\n"; - } - void SuccessorGenerator::PrintTransitionStatistics(std::ostream& out) const { out << std::endl << "TRANSITION STATISTICS"; for (int i=0;i -#include -#include -#include namespace VerifyTAPN { class SymbolicMarking; @@ -17,29 +14,25 @@ namespace VerifyTAPN { class SuccessorGenerator { public: SuccessorGenerator(const TAPN::TimedArcPetriNet & tapn, const MarkingFactory & factory, const VerificationOptions & options, unsigned int tokensInInitialMarking) - :tapn(tapn), factory(factory), arcsArray(), nInputArcs(tapn.GetNumberOfConsumingArcs()), transitionStatistics(), numberOfTransitions(tapn.GetNumberOfTransitions()), options(options), tokenIndices(), maxUsedTokens(tokensInInitialMarking) + :tapn(tapn), factory(factory), arcsArray(tapn.GetNumberOfConsumingArcs()), + nInputArcs(tapn.GetNumberOfConsumingArcs()), + transitionStatistics(tapn.GetNumberOfTransitions()), + numberOfTransitions(tapn.GetNumberOfTransitions()), + options(options), + tokenIndices(nInputArcs * options.GetKBound()), + maxUsedTokens(tokensInInitialMarking) { - arcsArray = new unsigned [nInputArcs]; - transitionStatistics = new unsigned [numberOfTransitions]; - tokenIndices = new boost::numeric::ublas::matrix(nInputArcs, options.GetKBound()); ClearTransitionsArray(); } ; virtual ~SuccessorGenerator() - { - delete [] arcsArray; - delete tokenIndices; - delete [] transitionStatistics; - } + {} ; public: void GenerateDiscreteTransitionsSuccessors(const SymbolicMarking & marking, std::vector & succ); - public: - void Print(std::ostream & out) const; void PrintTransitionStatistics(std::ostream & out) const; - public: inline void ClearAll() { ClearArcsArray(); @@ -48,16 +41,16 @@ namespace VerifyTAPN { inline void ClearArcsArray() { - memset(arcsArray, 0, nInputArcs * sizeof (arcsArray[0])); + std::fill(arcsArray.begin(), arcsArray.end(), 0); } inline void ClearTransitionsArray() { - memset(transitionStatistics, 0, numberOfTransitions * sizeof (transitionStatistics[0])); + std::fill(transitionStatistics.begin(), transitionStatistics.end(), 0); } inline void ClearTokenIndices() { - tokenIndices->clear(); + std::fill(tokenIndices.begin(), tokenIndices.end(), 0); } unsigned int MaxUsedTokens() const @@ -74,22 +67,23 @@ namespace VerifyTAPN { void MakeIdentity(IndirectionTable& mapping, unsigned int size) const; void UpdateTraceMapping(IndirectionTable& mapping, unsigned int tokenToRemove) const; + uint64_t toIndex(int currInputArcIdx, int nTokensFromCurrInputPlace) { + return currInputArcIdx*options.GetKBound() + nTokensFromCurrInputPlace; + } + int getIndicy(int currInputArcIdx, uint32_t nTokensFromCurrInputPlace) { + return tokenIndices[toIndex(currInputArcIdx, nTokensFromCurrInputPlace)]; + } private: const TAPN::TimedArcPetriNet& tapn; const MarkingFactory& factory; - unsigned int* arcsArray; + std::vector arcsArray; unsigned int nInputArcs; - unsigned int* transitionStatistics; + std::vector transitionStatistics; const int numberOfTransitions; const VerificationOptions& options; - boost::numeric::ublas::matrix* tokenIndices; + std::vector tokenIndices; unsigned int maxUsedTokens; }; - inline std::ostream& operator<<(std::ostream& out, const VerifyTAPN::SuccessorGenerator& succGen) - { - succGen.Print( out ); - return out; - } } #endif /* SUCCESSORGENERATOR_HPP_ */ diff --git a/src/main.cpp b/src/main.cpp index fc304fb..96d3258 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -1,5 +1,4 @@ #include -#include "boost/smart_ptr.hpp" #include "Core/TAPNParser/TAPNXmlParser.hpp" #include "Core/VerificationOptions.hpp" #include "Core/ArgsParser.hpp" @@ -25,7 +24,7 @@ using namespace VerifyTAPN; using namespace VerifyTAPN::TAPN; using namespace boost; -MarkingFactory* CreateFactory(const VerificationOptions& options, const boost::shared_ptr& tapn) +MarkingFactory* CreateFactory(const VerificationOptions& options, const std::shared_ptr& tapn) { switch(options.GetFactory()) { @@ -37,7 +36,7 @@ MarkingFactory* CreateFactory(const VerificationOptions& options, const boost::s }; } -SearchStrategy* CreateSearchStrategy(const boost::shared_ptr& tapn, SymbolicMarking* initialMarking, AST::Query* query, const VerificationOptions& options, MarkingFactory* factory) +SearchStrategy* CreateSearchStrategy(const std::shared_ptr& tapn, SymbolicMarking* initialMarking, AST::Query* query, const VerificationOptions& options, MarkingFactory* factory) { SearchStrategy* strategy; @@ -98,7 +97,7 @@ int main(int argc, char* argv[]) VerificationOptions options = parser.Parse(argc, argv); TAPNXmlParser modelParser; - boost::shared_ptr tapn; + std::shared_ptr tapn; try{ tapn = modelParser.Parse(options.GetInputFile());