From d43318afd83337f119deb0f3ea61db725b07f89d Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 13 Nov 2013 14:05:48 +0100 Subject: [PATCH] Added first version of MarkovAutomaton class. Former-commit-id: c211dd9bf4342e4d8e760f8acbd99f8513d1b305 --- src/models/MarkovAutomaton.h | 83 ++++++++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) create mode 100644 src/models/MarkovAutomaton.h diff --git a/src/models/MarkovAutomaton.h b/src/models/MarkovAutomaton.h new file mode 100644 index 000000000..5bd50749c --- /dev/null +++ b/src/models/MarkovAutomaton.h @@ -0,0 +1,83 @@ +/* + * MarkovAutomaton.h + * + * Created on: 07.11.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_MODELS_MA_H_ +#define STORM_MODELS_MA_H_ + +#include "AbstractNondeterministicModel.h" +#include "AtomicPropositionsLabeling.h" +#include "src/storage/SparseMatrix.h" +#include "src/exceptions/InvalidArgumentException.h" +#include "src/settings/Settings.h" +#include "src/utility/vector.h" + +namespace storm { + namespace models { + + template + class MarkovAutomaton : public storm::models::AbstractNondeterministicModel { + + public: + MarkovAutomaton(storm::storage::SparseMatrix const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, + std::vector&& nondeterministicChoiceIndices, + storm::storage::BitVector const& markovianChoices, std::vector const& exitRates, + boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, + boost::optional>> const& optionalChoiceLabeling) + : AbstractNondeterministicModel(transitionMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling), + markovianChoices(markovianChoices), exitRates(exitRates) { + if (this->hasTransitionRewards()) { + if (!this->getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix())) { + LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); + throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions."; + } + } + } + + MarkovAutomaton(storm::storage::SparseMatrix&& transitionMatrix, + storm::models::AtomicPropositionsLabeling&& stateLabeling, + std::vector&& nondeterministicChoiceIndices, + storm::storage::BitVector const& markovianChoices, std::vector const& exitRates, + boost::optional>&& optionalStateRewardVector, + boost::optional>&& optionalTransitionRewardMatrix, + boost::optional>>&& optionalChoiceLabeling) + // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class + : AbstractNondeterministicModel(std::move(transitionMatrix), std::move(stateLabeling), std::move(nondeterministicChoiceIndices), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), + std::move(optionalChoiceLabeling)), markovianChoices(std::move(markovianChoices)), exitRates(std::move(exitRates)) { + if (this->hasTransitionRewards()) { + if (!this->getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix())) { + LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); + throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions."; + } + } + } + + MarkovAutomaton(MarkovAutomaton const & markovAutomaton) : AbstractNondeterministicModel(markovAutomaton) { + // Intentionally left empty. + } + + MarkovAutomaton(MarkovAutomaton&& markovAutomaton) : AbstractNondeterministicModel(std::move(markovAutomaton)) { + // Intentionally left empty. + } + + ~MarkovAutomaton() { + // Intentionally left empty. + } + + storm::models::ModelType getType() const { + return MA; + } + + private: + + std::vector exitRates; + storm::storage::BitVector markovianChoices; + + }; + } +} + +#endif /* STORM_MODELS_MA_H_ */