diff --git a/src/adapters/EigenAdapter.h b/src/adapters/EigenAdapter.h index b258c6aa2..68f2ba588 100644 --- a/src/adapters/EigenAdapter.h +++ b/src/adapters/EigenAdapter.h @@ -14,6 +14,8 @@ #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" +#include "src/utility/OsDetection.h" + extern log4cplus::Logger logger; namespace storm { @@ -36,7 +38,10 @@ public: result->resizeNonZeros(static_cast(realNonZeros)); //result->reserve(realNonZeros); - +#ifdef WINDOWS +# pragma warning(push) +# pragma warning(disable: 4244) // possible loss of data +#endif // Copy Row Indications std::copy(matrix.rowIndications.begin(), matrix.rowIndications.end(), (result->outerIndexPtr())); // Copy Columns Indications @@ -44,6 +49,10 @@ public: // And do the same thing with the actual values. std::copy(matrix.valueStorage.begin(), matrix.valueStorage.end(), (result->valuePtr())); +#ifdef WINDOWS +# pragma warning(pop) +#endif + LOG4CPLUS_DEBUG(logger, "Done converting matrix to Eigen format."); return result; diff --git a/src/adapters/ExplicitModelAdapter.cpp b/src/adapters/ExplicitModelAdapter.cpp index 54c885b11..af5dfe848 100644 --- a/src/adapters/ExplicitModelAdapter.cpp +++ b/src/adapters/ExplicitModelAdapter.cpp @@ -28,7 +28,7 @@ namespace adapters { ExplicitModelAdapter::ExplicitModelAdapter(storm::ir::Program program) : program(program), booleanVariables(), integerVariables(), booleanVariableToIndexMap(), integerVariableToIndexMap(), - allStates(), stateToIndexMap(), numberOfTransitions(0), numberOfChoices(0), transitionRewards(nullptr), transitionMap() { + allStates(), stateToIndexMap(), numberOfTransitions(0), numberOfChoices(0), transitionMap() { // Get variables from program. this->initializeVariables(); storm::settings::Settings* s = storm::settings::instance(); @@ -50,12 +50,12 @@ namespace adapters { this->buildTransitionMap(); // Compute labeling. - std::shared_ptr stateLabeling = this->getStateLabeling(this->program.getLabels()); + storm::models::AtomicPropositionsLabeling stateLabeling = this->getStateLabeling(this->program.getLabels()); // Compute state rewards. - std::shared_ptr> stateRewards = nullptr; + boost::optional> stateRewards; if ((this->rewardModel != nullptr) && this->rewardModel->hasStateRewards()) { - stateRewards = this->getStateRewards(this->rewardModel->getStateRewards()); + stateRewards.reset(this->getStateRewards(this->rewardModel->getStateRewards())); } // Build and return actual model. @@ -63,19 +63,19 @@ namespace adapters { { case storm::ir::Program::DTMC: { - std::shared_ptr> matrix = this->buildDeterministicMatrix(); + storm::storage::SparseMatrix matrix = this->buildDeterministicMatrix(); return std::shared_ptr>(new storm::models::Dtmc(matrix, stateLabeling, stateRewards, this->transitionRewards)); break; } case storm::ir::Program::CTMC: { - std::shared_ptr> matrix = this->buildDeterministicMatrix(); + storm::storage::SparseMatrix matrix = this->buildDeterministicMatrix(); return std::shared_ptr>(new storm::models::Ctmc(matrix, stateLabeling, stateRewards, this->transitionRewards)); break; } case storm::ir::Program::MDP: { - std::shared_ptr> matrix = this->buildNondeterministicMatrix(); + storm::storage::SparseMatrix matrix = this->buildNondeterministicMatrix(); return std::shared_ptr>(new storm::models::Mdp(matrix, stateLabeling, this->choiceIndices, stateRewards, this->transitionRewards)); break; } @@ -88,8 +88,6 @@ namespace adapters { throw storm::exceptions::WrongFormatException() << "Error while creating model from probabilistic program: We can't handle this model type."; break; } - - return std::shared_ptr>(nullptr); } void ExplicitModelAdapter::setValue(StateType* const state, uint_fast64_t const index, bool const value) { @@ -107,31 +105,31 @@ namespace adapters { return ss.str(); } - std::shared_ptr> ExplicitModelAdapter::getStateRewards(std::vector const& rewards) { - std::shared_ptr> results(new std::vector(this->allStates.size())); + std::vector ExplicitModelAdapter::getStateRewards(std::vector const & rewards) { + std::vector results(this->allStates.size()); for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { - (*results)[index] = 0; + results[index] = 0; for (auto reward: rewards) { // Add this reward to the state if the state is included in the state reward. if (reward.getStatePredicate()->getValueAsBool(this->allStates[index]) == true) { - (*results)[index] += reward.getRewardValue()->getValueAsDouble(this->allStates[index]); + results[index] += reward.getRewardValue()->getValueAsDouble(this->allStates[index]); } } } return results; } - std::shared_ptr ExplicitModelAdapter::getStateLabeling(std::map> labels) { - std::shared_ptr results(new storm::models::AtomicPropositionsLabeling(this->allStates.size(), labels.size())); + storm::models::AtomicPropositionsLabeling ExplicitModelAdapter::getStateLabeling(std::map> labels) { + storm::models::AtomicPropositionsLabeling results(this->allStates.size(), labels.size()); // Initialize labeling. for (auto it: labels) { - results->addAtomicProposition(it.first); + results.addAtomicProposition(it.first); } for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { for (auto label: labels) { // Add label to state, if guard is true. if (label.second->getValueAsBool(this->allStates[index])) { - results->addAtomicPropositionToState(label.first, index); + results.addAtomicPropositionToState(label.first, index); } } } @@ -434,7 +432,7 @@ namespace adapters { * @param intermediate Intermediate representation of transition mapping. * @return result matrix. */ - std::shared_ptr> ExplicitModelAdapter::buildDeterministicMatrix() { + storm::storage::SparseMatrix ExplicitModelAdapter::buildDeterministicMatrix() { // ***** ATTENTION ***** // this->numberOfTransitions is meaningless, as we combine all choices into one for each state. // Hence, we compute the correct number of transitions now. @@ -452,11 +450,11 @@ namespace adapters { LOG4CPLUS_INFO(logger, "Building deterministic transition matrix: " << allStates.size() << " x " << allStates.size() << " with " << numberOfTransitions << " transitions."); // Now build matrix. - std::shared_ptr> result(new storm::storage::SparseMatrix(allStates.size())); - result->initialize(numberOfTransitions); + storm::storage::SparseMatrix result(allStates.size()); + result.initialize(numberOfTransitions); if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { - this->transitionRewards = std::shared_ptr>(new storm::storage::SparseMatrix(allStates.size())); - this->transitionRewards->initialize(numberOfTransitions); + this->transitionRewards.reset(storm::storage::SparseMatrix(allStates.size())); + this->transitionRewards.get().initialize(numberOfTransitions); } for (uint_fast64_t state = 0; state < this->allStates.size(); state++) { if (transitionMap[state].size() > 1) { @@ -480,14 +478,14 @@ namespace adapters { // Scale probabilities by number of choices. double factor = 1.0 / transitionMap[state].size(); for (auto it : map) { - result->addNextValue(state, it.first, it.second * factor); + result.addNextValue(state, it.first, it.second * factor); if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { - this->transitionRewards->addNextValue(state, it.first, rewardMap[it.first] * factor); + this->transitionRewards.get().addNextValue(state, it.first, rewardMap[it.first] * factor); } } } - result->finalize(); + result.finalize(); return result; } @@ -497,23 +495,23 @@ namespace adapters { * @param choices Overall number of choices for all nodes. * @return result matrix. */ - std::shared_ptr> ExplicitModelAdapter::buildNondeterministicMatrix() { + storm::storage::SparseMatrix ExplicitModelAdapter::buildNondeterministicMatrix() { LOG4CPLUS_INFO(logger, "Building nondeterministic transition matrix: " << this->numberOfChoices << " x " << allStates.size() << " with " << this->numberOfTransitions << " transitions."); - std::shared_ptr> result(new storm::storage::SparseMatrix(this->numberOfChoices, allStates.size())); - result->initialize(this->numberOfTransitions); + storm::storage::SparseMatrix result(this->numberOfChoices, allStates.size()); + result.initialize(this->numberOfTransitions); if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { - this->transitionRewards = std::shared_ptr>(new storm::storage::SparseMatrix(this->numberOfChoices, allStates.size())); - this->transitionRewards->initialize(this->numberOfTransitions); + this->transitionRewards.reset(storm::storage::SparseMatrix(this->numberOfChoices, allStates.size())); + this->transitionRewards.get().initialize(this->numberOfTransitions); } - this->choiceIndices = std::shared_ptr>(new std::vector()); - this->choiceIndices->reserve(allStates.size()); + this->choiceIndices.clear(); + this->choiceIndices.reserve(allStates.size()); // Build matrix. uint_fast64_t nextRow = 0; for (uint_fast64_t state = 0; state < this->allStates.size(); state++) { - this->choiceIndices->push_back(transitionMap[state].size()); + this->choiceIndices.push_back(transitionMap[state].size()); for (auto choice : transitionMap[state]) { for (auto it : choice.second) { - result->addNextValue(nextRow, it.first, it.second); + result.addNextValue(nextRow, it.first, it.second); if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { double rewardValue = 0; for (auto reward : this->rewardModel->getTransitionRewards()) { @@ -521,13 +519,13 @@ namespace adapters { rewardValue = reward.getRewardValue()->getValueAsDouble(this->allStates[state]); } } - this->transitionRewards->addNextValue(nextRow, it.first, rewardValue); + this->transitionRewards.get().addNextValue(nextRow, it.first, rewardValue); } } nextRow++; } } - result->finalize(); + result.finalize(); return result; } @@ -572,7 +570,8 @@ namespace adapters { stateToIndexMap.clear(); this->numberOfTransitions = 0; this->numberOfChoices = 0; - this->transitionRewards = nullptr; + this->choiceIndices.clear(); + this->transitionRewards.reset(); this->transitionMap.clear(); } diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index a69d7382c..c1f083968 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -121,14 +121,14 @@ private: * @param rewards List of state reward models. * @return Reward for every state. */ - std::shared_ptr> getStateRewards(std::vector const & rewards); + std::vector getStateRewards(std::vector const & rewards); /*! * Determines the labels for every reachable state, based on a list of available labels. * @param labels Mapping from label names to boolean expressions. * @returns The resulting labeling. */ - std::shared_ptr getStateLabeling(std::map> labels); + storm::models::AtomicPropositionsLabeling getStateLabeling(std::map> labels); /*! * Retrieves all active command labeled by some label, ordered by modules. @@ -181,7 +181,7 @@ private: * @param intermediate Intermediate representation of transition mapping. * @return result matrix. */ - std::shared_ptr> buildDeterministicMatrix(); + storm::storage::SparseMatrix buildDeterministicMatrix(); /*! * Create matrix from intermediate mapping, assuming it is a mdp model. @@ -189,7 +189,7 @@ private: * @param choices Overall number of choices for all nodes. * @return result matrix. */ - std::shared_ptr> buildNondeterministicMatrix(); + storm::storage::SparseMatrix buildNondeterministicMatrix(); /*! * Generate internal transition map from given model. @@ -225,9 +225,9 @@ private: // Number of choices. (Is number of rows in matrix of nondeterministic model.) uint_fast64_t numberOfChoices; // Number of choices for each state. - std::shared_ptr> choiceIndices; + std::vector choiceIndices; // Rewards for transitions. - std::shared_ptr> transitionRewards; + boost::optional> transitionRewards; /*! * Maps a source node to a list of probability distributions over target nodes. diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index e48046aa7..7c70e59df 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -409,6 +409,7 @@ public: storm::utility::vector::setVectorValues(*result, maybeStates, storm::utility::constGetOne()); } else { // In this case we have to compute the reward values for the remaining states. + uint_fast64_t maybeStatesSetBitCount = maybeStates.getNumberOfSetBits(); // Now we can eliminate the rows and columns from the original transition probability matrix. storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates); diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index 921f6cbfb..5882fa4f3 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -20,28 +20,28 @@ class AbstractDeterministicModel: public AbstractModel { public: /*! Constructs an abstract determinstic model from the given parameters. + * All values are copied. * @param transitionMatrix The matrix representing the transitions in the model. * @param stateLabeling The labeling that assigns a set of atomic * propositions to each state. * @param stateRewardVector The reward values associated with the states. * @param transitionRewardMatrix The reward values associated with the transitions of the model. */ - AbstractDeterministicModel(std::shared_ptr> transitionMatrix, - std::shared_ptr stateLabeling, - std::shared_ptr> stateRewardVector, std::shared_ptr> transitionRewardMatrix) - : AbstractModel(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix) { + AbstractDeterministicModel(storm::storage::SparseMatrix const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, + boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix) + : AbstractModel(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix) { } /*! Constructs an abstract determinstic model from the given parameters. - * All values are copied. + * Moves all references. * @param transitionMatrix The matrix representing the transitions in the model. * @param stateLabeling The labeling that assigns a set of atomic * propositions to each state. * @param stateRewardVector The reward values associated with the states. * @param transitionRewardMatrix The reward values associated with the transitions of the model. */ - AbstractDeterministicModel(storm::storage::SparseMatrix const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, - boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix) + AbstractDeterministicModel(storm::storage::SparseMatrix&& transitionMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, + boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix) : AbstractModel(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix) { } @@ -66,7 +66,7 @@ class AbstractDeterministicModel: public AbstractModel { * @return An iterator to the successors of the given state. */ virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) const { - return this->transitionMatrix->constColumnIteratorBegin(state); + return this->transitionMatrix.constColumnIteratorBegin(state); } /*! @@ -76,7 +76,7 @@ class AbstractDeterministicModel: public AbstractModel { * @return An iterator pointing to the element past the successors of the given state. */ virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const { - return this->transitionMatrix->constColumnIteratorEnd(state); + return this->transitionMatrix.constColumnIteratorEnd(state); } virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override { diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 65c993ad4..2bec382c8 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -35,19 +35,16 @@ template class AbstractModel: public std::enable_shared_from_this> { public: - /*! Constructs an abstract model from the given transition matrix and - * the given labeling of the states. - * @param transitionMatrix The matrix representing the transitions in the model. - * @param stateLabeling The labeling that assigns a set of atomic - * propositions to each state. - * @param stateRewardVector The reward values associated with the states. - * @param transitionRewardMatrix The reward values associated with the transitions of the model. + /*! Move Constructor for an abstract model from the given transition matrix and + * the given labeling of the states. Creates copies of all given references. + * @param other The Source Abstract Model */ - AbstractModel(std::shared_ptr> transitionMatrix, - std::shared_ptr stateLabeling, - std::shared_ptr> stateRewardVector, std::shared_ptr> transitionRewardMatrix) - : transitionMatrix(transitionMatrix), stateLabeling(stateLabeling), stateRewardVector(stateRewardVector), transitionRewardMatrix(transitionRewardMatrix) { - // Intentionally left empty. + AbstractModel(AbstractModel&& other) { + this->transitionMatrix = std::move(other.transitionMatrix); + this->stateLabeling = std::move(other.stateLabeling); + + this->stateRewardVector = std::move(other.stateRewardVector); + this->transitionRewardMatrix = std::move(other.transitionRewardMatrix); } /*! Constructs an abstract model from the given transition matrix and @@ -59,22 +56,34 @@ class AbstractModel: public std::enable_shared_from_this> { * @param transitionRewardMatrix The reward values associated with the transitions of the model. */ AbstractModel(storm::storage::SparseMatrix const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, - boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix) { - this->transitionMatrix.reset(new storm::storage::SparseMatrix(transitionMatrix)); - this->stateLabeling.reset(new storm::models::AtomicPropositionsLabeling(stateLabeling)); + boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix) + : transitionMatrix(transitionMatrix), stateLabeling(stateLabeling) { - this->stateRewardVector = nullptr; - this->transitionRewardMatrix = nullptr; - if (optionalStateRewardVector) { // Boost::Optional - this->stateRewardVector.reset(new std::vector(optionalStateRewardVector.get())); + this->stateRewardVector.reset(optionalStateRewardVector.get()); } - if (optionalTransitionRewardMatrix) { // Boost::Optional - this->transitionRewardMatrix.reset(new storm::storage::SparseMatrix(optionalTransitionRewardMatrix.get())); + this->transitionRewardMatrix.reset(optionalTransitionRewardMatrix.get()); } } + /*! Constructs an abstract model from the given transition matrix and + * the given labeling of the states. Moves all given references. + * @param transitionMatrix The matrix representing the transitions in the model. + * @param stateLabeling The labeling that assigns a set of atomic + * propositions to each state. + * @param stateRewardVector The reward values associated with the states. + * @param transitionRewardMatrix The reward values associated with the transitions of the model. + */ + AbstractModel(storm::storage::SparseMatrix&& transitionMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, + boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix) { + this->transitionMatrix = std::move(transitionMatrix); + this->stateLabeling = std::move(stateLabeling); + + this->stateRewardVector = std::move(optionalStateRewardVector); + this->transitionRewardMatrix = std::move(optionalTransitionRewardMatrix); + } + /*! * Destructor. */ @@ -254,7 +263,7 @@ class AbstractModel: public std::enable_shared_from_this> { * correspond to a state labeled with the given atomic proposition. */ storm::storage::BitVector const& getLabeledStates(std::string const& ap) const { - return stateLabeling->getLabeledStates(ap); + return stateLabeling.getLabeledStates(ap); } /*! @@ -263,7 +272,7 @@ class AbstractModel: public std::enable_shared_from_this> { * @return True if the given atomic proposition is valid in this model. */ bool hasAtomicProposition(std::string const& atomicProposition) const { - return stateLabeling->containsAtomicProposition(atomicProposition); + return stateLabeling.containsAtomicProposition(atomicProposition); } /*! @@ -273,7 +282,7 @@ class AbstractModel: public std::enable_shared_from_this> { * function. */ storm::storage::SparseMatrix const& getTransitionMatrix() const { - return *transitionMatrix; + return transitionMatrix; } /*! @@ -281,7 +290,7 @@ class AbstractModel: public std::enable_shared_from_this> { * @return A pointer to the matrix representing the transition rewards. */ storm::storage::SparseMatrix const& getTransitionRewardMatrix() const { - return *transitionRewardMatrix; + return transitionRewardMatrix.get(); } /*! @@ -289,7 +298,7 @@ class AbstractModel: public std::enable_shared_from_this> { * @return A pointer to the vector representing the state rewards. */ std::vector const& getStateRewardVector() const { - return *stateRewardVector; + return stateRewardVector.get(); } /*! @@ -299,7 +308,7 @@ class AbstractModel: public std::enable_shared_from_this> { * @return The set of labels with which the given state is labeled. */ std::set getLabelsForState(uint_fast64_t state) const { - return stateLabeling->getPropositionsForState(state); + return stateLabeling.getPropositionsForState(state); } /*! @@ -307,7 +316,7 @@ class AbstractModel: public std::enable_shared_from_this> { * @return The state labeling associated with this model. */ storm::models::AtomicPropositionsLabeling const& getStateLabeling() const { - return *stateLabeling; + return stateLabeling; } /*! @@ -315,7 +324,7 @@ class AbstractModel: public std::enable_shared_from_this> { * @return True if this model has a state reward model. */ bool hasStateRewards() const { - return stateRewardVector != nullptr; + return stateRewardVector; } /*! @@ -323,7 +332,7 @@ class AbstractModel: public std::enable_shared_from_this> { * @return True if this model has a transition reward model. */ bool hasTransitionRewards() const { - return transitionRewardMatrix != nullptr; + return transitionRewardMatrix; } /*! @@ -332,12 +341,12 @@ class AbstractModel: public std::enable_shared_from_this> { * measured in bytes. */ virtual uint_fast64_t getSizeInMemory() const { - uint_fast64_t result = transitionMatrix->getSizeInMemory() + stateLabeling->getSizeInMemory(); - if (stateRewardVector != nullptr) { - result += stateRewardVector->size() * sizeof(T); + uint_fast64_t result = transitionMatrix.getSizeInMemory() + stateLabeling.getSizeInMemory(); + if (stateRewardVector) { + result += getStateRewardVector().size() * sizeof(T); } - if (transitionRewardMatrix != nullptr) { - result += transitionRewardMatrix->getSizeInMemory(); + if (hasTransitionRewards()) { + result += getTransitionRewardMatrix().getSizeInMemory(); } return result; } @@ -430,17 +439,17 @@ protected: } /*! A matrix representing the likelihoods of moving between states. */ - std::shared_ptr> transitionMatrix; + storm::storage::SparseMatrix transitionMatrix; private: /*! The labeling of the states of the model. */ - std::shared_ptr stateLabeling; + storm::models::AtomicPropositionsLabeling stateLabeling; /*! The state-based rewards of the model. */ - std::shared_ptr> stateRewardVector; + boost::optional> stateRewardVector; /*! The transition-based rewards of the model. */ - std::shared_ptr> transitionRewardMatrix; + boost::optional> transitionRewardMatrix; }; } // namespace models diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index 8f1924716..763b87128 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -19,6 +19,7 @@ class AbstractNondeterministicModel: public AbstractModel { public: /*! Constructs an abstract non-determinstic model from the given parameters. + * All values are copied. * @param transitionMatrix The matrix representing the transitions in the model. * @param stateLabeling The labeling that assigns a set of atomic * propositions to each state. @@ -26,17 +27,18 @@ class AbstractNondeterministicModel: public AbstractModel { * @param stateRewardVector The reward values associated with the states. * @param transitionRewardMatrix The reward values associated with the transitions of the model. */ - AbstractNondeterministicModel(std::shared_ptr> transitionMatrix, - std::shared_ptr stateLabeling, - std::shared_ptr> nondeterministicChoiceIndices, - std::shared_ptr> stateRewardVector, - std::shared_ptr> transitionRewardMatrix) - : AbstractModel(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix), - nondeterministicChoiceIndices(nondeterministicChoiceIndices) { + AbstractNondeterministicModel( + storm::storage::SparseMatrix const& transitionMatrix, + storm::models::AtomicPropositionsLabeling const& stateLabeling, + std::vector const& nondeterministicChoiceIndices, + boost::optional> const& optionalStateRewardVector, + boost::optional> const& optionalTransitionRewardMatrix) + : AbstractModel(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix) { + this->nondeterministicChoiceIndices = nondeterministicChoiceIndices; } /*! Constructs an abstract non-determinstic model from the given parameters. - * All values are copied. + * All values are moved. * @param transitionMatrix The matrix representing the transitions in the model. * @param stateLabeling The labeling that assigns a set of atomic * propositions to each state. @@ -45,13 +47,13 @@ class AbstractNondeterministicModel: public AbstractModel { * @param transitionRewardMatrix The reward values associated with the transitions of the model. */ AbstractNondeterministicModel( - storm::storage::SparseMatrix const& transitionMatrix, - storm::models::AtomicPropositionsLabeling const& stateLabeling, - std::vector const& nondeterministicChoiceIndices, - boost::optional> const& optionalStateRewardVector, - boost::optional> const& optionalTransitionRewardMatrix) + storm::storage::SparseMatrix&& transitionMatrix, + storm::models::AtomicPropositionsLabeling&& stateLabeling, + std::vector&& nondeterministicChoiceIndices, + boost::optional>&& optionalStateRewardVector, + boost::optional>&& optionalTransitionRewardMatrix) : AbstractModel(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix) { - this->nondeterministicChoiceIndices.reset(new std::vector(nondeterministicChoiceIndices)); + this->nondeterministicChoiceIndices = std::move(nondeterministicChoiceIndices); } /*! @@ -69,12 +71,20 @@ class AbstractNondeterministicModel: public AbstractModel { // Intentionally left empty. } + /*! + * Move Constructor. + */ + AbstractNondeterministicModel(AbstractNondeterministicModel&& other) : AbstractModel(other), + nondeterministicChoiceIndices(std::move(other.nondeterministicChoiceIndices)) { + // Intentionally left empty. + } + /*! * Returns the number of choices for all states of the MDP. * @return The number of choices for all states of the MDP. */ uint_fast64_t getNumberOfChoices() const { - return this->transitionMatrix->getRowCount(); + return this->transitionMatrix.getRowCount(); } /*! @@ -83,7 +93,7 @@ class AbstractNondeterministicModel: public AbstractModel { * measured in bytes. */ virtual uint_fast64_t getSizeInMemory() const { - return AbstractModel::getSizeInMemory() + nondeterministicChoiceIndices->size() * sizeof(uint_fast64_t); + return AbstractModel::getSizeInMemory() + nondeterministicChoiceIndices.size() * sizeof(uint_fast64_t); } /*! @@ -93,7 +103,7 @@ class AbstractNondeterministicModel: public AbstractModel { * of a certain state. */ std::vector const& getNondeterministicChoiceIndices() const { - return *nondeterministicChoiceIndices; + return nondeterministicChoiceIndices; } /*! @@ -103,7 +113,7 @@ class AbstractNondeterministicModel: public AbstractModel { * @return An iterator to the successors of the given state. */ virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) const { - return this->transitionMatrix->constColumnIteratorBegin((*nondeterministicChoiceIndices)[state]); + return this->transitionMatrix.constColumnIteratorBegin(nondeterministicChoiceIndices[state]); } /*! @@ -113,7 +123,7 @@ class AbstractNondeterministicModel: public AbstractModel { * @return An iterator pointing to the element past the successors of the given state. */ virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const { - return this->transitionMatrix->constColumnIteratorEnd((*nondeterministicChoiceIndices)[state + 1] - 1); + return this->transitionMatrix.constColumnIteratorEnd(nondeterministicChoiceIndices[state + 1] - 1); } virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override { @@ -187,7 +197,7 @@ class AbstractNondeterministicModel: public AbstractModel { private: /*! A vector of indices mapping states to the choices (rows) in the transition matrix. */ - std::shared_ptr> nondeterministicChoiceIndices; + std::vector nondeterministicChoiceIndices; }; } // namespace models diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h index 07deef78b..ced1cd235 100644 --- a/src/models/AtomicPropositionsLabeling.h +++ b/src/models/AtomicPropositionsLabeling.h @@ -57,6 +57,20 @@ public: // Intentionally left empty. } + /*! + * Move Constructor that performs a move copy on the given atomic proposition labeling. + * + * @param atomicPropositionsLabeling The atomic propositions labeling to copy. + */ + AtomicPropositionsLabeling(AtomicPropositionsLabeling&& atomicPropositionsLabeling) + : stateCount(atomicPropositionsLabeling.stateCount), + apCountMax(atomicPropositionsLabeling.apCountMax), + apsCurrent(atomicPropositionsLabeling.apsCurrent), + nameToLabelingMap(std::move(atomicPropositionsLabeling.nameToLabelingMap)), + singleLabelings(std::move(atomicPropositionsLabeling.singleLabelings)) { + // Intentionally left empty. + } + /*! * (Empty) destructor. */ diff --git a/src/models/Ctmc.h b/src/models/Ctmc.h index 9a51d8732..bd1ef5c42 100644 --- a/src/models/Ctmc.h +++ b/src/models/Ctmc.h @@ -27,7 +27,6 @@ template class Ctmc : public storm::models::AbstractDeterministicModel { public: - //! Constructor /*! * Constructs a CTMC object from the given transition rate matrix and * the given labeling of the states. @@ -36,11 +35,9 @@ public: * @param stateLabeling The labeling that assigns a set of atomic * propositions to each state. */ - Ctmc(std::shared_ptr> rateMatrix, - std::shared_ptr stateLabeling, - std::shared_ptr> stateRewardVector = nullptr, - std::shared_ptr> transitionRewardMatrix = nullptr) - : AbstractDeterministicModel(rateMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix) { + Ctmc(storm::storage::SparseMatrix const& rateMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, + boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix) + : AbstractDeterministicModel(rateMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix) { } /*! @@ -51,8 +48,8 @@ public: * @param stateLabeling The labeling that assigns a set of atomic * propositions to each state. */ - Ctmc(storm::storage::SparseMatrix const& rateMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, - boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix) + Ctmc(storm::storage::SparseMatrix&& rateMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, + boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix) : AbstractDeterministicModel(rateMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix) { } @@ -61,7 +58,15 @@ public: * Copy Constructor. Performs a deep copy of the given CTMC. * @param ctmc A reference to the CTMC that is to be copied. */ - Ctmc(const Ctmc &ctmc) : AbstractDeterministicModel(ctmc) { + Ctmc(Ctmc const & ctmc) : AbstractDeterministicModel(ctmc) { + // Intentionally left empty. + } + + /*! + * Move Constructor. Performs a move on the given CTMC. + * @param ctmc A reference to the CTMC that is to be moved from. + */ + Ctmc(Ctmc&& ctmc) : AbstractDeterministicModel(ctmc) { // Intentionally left empty. } diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h index abfcb0485..70b6dcbe8 100644 --- a/src/models/Ctmdp.h +++ b/src/models/Ctmdp.h @@ -28,21 +28,21 @@ template class Ctmdp : public storm::models::AbstractNondeterministicModel { public: - //! Constructor /*! * Constructs a CTMDP object from the given transition probability matrix and * the given labeling of the states. + * All values are copied. * @param probabilityMatrix The transition probability relation of the * CTMDP given by a matrix. * @param stateLabeling The labeling that assigns a set of atomic * propositions to each state. */ - Ctmdp(std::shared_ptr> probabilityMatrix, - std::shared_ptr stateLabeling, - std::shared_ptr> choiceIndices, - std::shared_ptr> stateRewardVector = nullptr, - std::shared_ptr> transitionRewardMatrix = nullptr) - : AbstractNondeterministicModel(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) { + Ctmdp(storm::storage::SparseMatrix const& probabilityMatrix, + storm::models::AtomicPropositionsLabeling const& stateLabeling, + std::vector const& nondeterministicChoiceIndices, + boost::optional> const& optionalStateRewardVector, + boost::optional> const& optionalTransitionRewardMatrix) + : AbstractNondeterministicModel(probabilityMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; @@ -52,17 +52,17 @@ public: /*! * Constructs a CTMDP object from the given transition probability matrix and * the given labeling of the states. - * All values are copied. + * All values are moved. * @param probabilityMatrix The transition probability relation of the * CTMDP given by a matrix. * @param stateLabeling The labeling that assigns a set of atomic * propositions to each state. */ - Ctmdp(storm::storage::SparseMatrix const& probabilityMatrix, - storm::models::AtomicPropositionsLabeling const& stateLabeling, - std::vector const& nondeterministicChoiceIndices, - boost::optional> const& optionalStateRewardVector, - boost::optional> const& optionalTransitionRewardMatrix) + Ctmdp(storm::storage::SparseMatrix&& probabilityMatrix, + storm::models::AtomicPropositionsLabeling&& stateLabeling, + std::vector&& nondeterministicChoiceIndices, + boost::optional>&& optionalStateRewardVector, + boost::optional>&& optionalTransitionRewardMatrix) : AbstractNondeterministicModel(probabilityMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); @@ -70,12 +70,22 @@ public: } } - //! Copy Constructor /*! * Copy Constructor. Performs a deep copy of the given CTMDP. * @param ctmdp A reference to the CTMDP that is to be copied. */ - Ctmdp(const Ctmdp &ctmdp) : AbstractNondeterministicModel(ctmdp) { + Ctmdp(Ctmdp const & ctmdp) : AbstractNondeterministicModel(ctmdp) { + if (!this->checkValidityOfProbabilityMatrix()) { + LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); + throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; + } + } + + /*! + * Move Constructor. Performs a move on the given CTMDP. + * @param ctmdp A reference to the CTMDP that is to be moved. + */ + Ctmdp(Ctmdp&& ctmdp) : AbstractNondeterministicModel(ctmdp) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index c2c652e0b..07dc213d8 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -31,20 +31,19 @@ template class Dtmc : public storm::models::AbstractDeterministicModel { public: - //! Constructor /*! * Constructs a DTMC object from the given transition probability matrix and * the given labeling of the states. - * @param probabilityMatrix The transition probability function of the - * DTMC given by a matrix. + * All values are copied. + * @param probabilityMatrix The matrix representing the transitions in the model. * @param stateLabeling The labeling that assigns a set of atomic * propositions to each state. + * @param stateRewardVector The reward values associated with the states. + * @param transitionRewardMatrix The reward values associated with the transitions of the model. */ - Dtmc(std::shared_ptr> probabilityMatrix, - std::shared_ptr stateLabeling, - std::shared_ptr> stateRewardVector = nullptr, - std::shared_ptr> transitionRewardMatrix = nullptr) - : AbstractDeterministicModel(probabilityMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix) { + Dtmc(storm::storage::SparseMatrix const& probabilityMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, + boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix) + : AbstractDeterministicModel(probabilityMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; @@ -60,15 +59,15 @@ public: /*! * Constructs a DTMC object from the given transition probability matrix and * the given labeling of the states. - * All values are copied. + * All values are moved. * @param probabilityMatrix The matrix representing the transitions in the model. * @param stateLabeling The labeling that assigns a set of atomic * propositions to each state. * @param stateRewardVector The reward values associated with the states. * @param transitionRewardMatrix The reward values associated with the transitions of the model. */ - Dtmc(storm::storage::SparseMatrix const& probabilityMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, - boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix) + Dtmc(storm::storage::SparseMatrix&& probabilityMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, + boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix) : AbstractDeterministicModel(probabilityMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); @@ -82,12 +81,19 @@ public: } } - //! Copy Constructor /*! * Copy Constructor. Performs a deep copy of the given DTMC. * @param dtmc A reference to the DTMC that is to be copied. */ - Dtmc(Dtmc const& dtmc) : AbstractDeterministicModel(dtmc) { + Dtmc(Dtmc const & dtmc) : AbstractDeterministicModel(dtmc) { + // Intentionally left empty. + } + + /*! + * Move Constructor. Performs a move on the given DTMC. + * @param dtmc A reference to the DTMC that is to be moved. + */ + Dtmc(Dtmc&& dtmc) : AbstractDeterministicModel(dtmc) { // Intentionally left empty. } diff --git a/src/models/Mdp.h b/src/models/Mdp.h index 6817c458a..e826db108 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -30,21 +30,21 @@ template class Mdp : public storm::models::AbstractNondeterministicModel { public: - //! Constructor /*! * Constructs a MDP object from the given transition probability matrix and * the given labeling of the states. + * All values are copied. * @param probabilityMatrix The transition probability relation of the * MDP given by a matrix. * @param stateLabeling The labeling that assigns a set of atomic * propositions to each state. */ - Mdp(std::shared_ptr> probabilityMatrix, - std::shared_ptr stateLabeling, - std::shared_ptr> choiceIndices, - std::shared_ptr> stateRewardVector = nullptr, - std::shared_ptr> transitionRewardMatrix = nullptr) - : AbstractNondeterministicModel(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) { + Mdp(storm::storage::SparseMatrix const& transitionMatrix, + storm::models::AtomicPropositionsLabeling const& stateLabeling, + std::vector const& nondeterministicChoiceIndices, + boost::optional> const& optionalStateRewardVector, + boost::optional> const& optionalTransitionRewardMatrix) + : AbstractNondeterministicModel(transitionMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; @@ -54,17 +54,17 @@ public: /*! * Constructs a MDP object from the given transition probability matrix and * the given labeling of the states. - * All values are copied. + * All values are moved. * @param probabilityMatrix The transition probability relation of the * MDP given by a matrix. * @param stateLabeling The labeling that assigns a set of atomic * propositions to each state. */ - Mdp(storm::storage::SparseMatrix const& transitionMatrix, - storm::models::AtomicPropositionsLabeling const& stateLabeling, - std::vector const& nondeterministicChoiceIndices, - boost::optional> const& optionalStateRewardVector, - boost::optional> const& optionalTransitionRewardMatrix) + Mdp(storm::storage::SparseMatrix&& transitionMatrix, + storm::models::AtomicPropositionsLabeling&& stateLabeling, + std::vector&& nondeterministicChoiceIndices, + boost::optional>&& optionalStateRewardVector, + boost::optional>&& optionalTransitionRewardMatrix) : AbstractNondeterministicModel(transitionMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); @@ -72,12 +72,22 @@ public: } } - //! Copy Constructor /*! * Copy Constructor. Performs a deep copy of the given MDP. * @param mdp A reference to the MDP that is to be copied. */ - Mdp(const Mdp &mdp) : AbstractNondeterministicModel(mdp) { + Mdp(Mdp const & mdp) : AbstractNondeterministicModel(mdp) { + if (!this->checkValidityOfProbabilityMatrix()) { + LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); + throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; + } + } + + /*! + * Move Constructor. Performs a move on the given MDP. + * @param mdp A reference to the MDP that is to be moved. + */ + Mdp(Mdp&& mdp) : AbstractNondeterministicModel(mdp) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index eb5cca456..3c768c60a 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -224,6 +224,25 @@ public: internalStatus(MatrixStatus::UnInitialized), currentSize(0), lastRow(0) { // Intentionally left empty. } + + /*! + * Move Constructor. + * + * @param other The Matrix from which to move the content + */ + SparseMatrix(SparseMatrix&& other) + : rowCount(other.rowCount), colCount(other.colCount), nonZeroEntryCount(other.nonZeroEntryCount), + internalStatus(other.internalStatus), currentSize(other.currentSize), lastRow(other.lastRow), + valueStorage(std::move(other.valueStorage)), columnIndications(std::move(other.columnIndications)), + rowIndications(std::move(other.rowIndications)) { + // Now update the source matrix + other.rowCount = 0; + other.colCount = 0; + other.nonZeroEntryCount = 0; + other.internalStatus = MatrixStatus::Error; + other.currentSize = 0; + other.lastRow = 0; + } /*! * Constructs a sparse matrix object with the given (moved) contents.