diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index b7dc1a380..c669a295c 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -19,22 +19,48 @@ template class AbstractDeterministicModel: public AbstractModel { public: + /*! Constructs an abstract determinstic model from the given parameters. + * @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), backwardTransitions(nullptr) { } + /*! + * Destructor. + */ virtual ~AbstractDeterministicModel() { // Intentionally left empty. } + /*! + * Copy Constructor. + */ AbstractDeterministicModel(AbstractDeterministicModel const& other) : AbstractModel(other), backwardTransitions(nullptr) { if (other.backwardTransitions != nullptr) { backwardTransitions = new storm::models::GraphTransitions(*other.backwardTransitions); } } + /*! + * Retrieves the size of the internal representation of the model in memory. + * @return the size of the internal representation of the model in memory + * measured in bytes. + */ + virtual uint_fast64_t getSizeInMemory() const { + uint_fast64_t result = AbstractModel::getSizeInMemory(); + if (backwardTransitions != nullptr) { + result += backwardTransitions->getSizeInMemory(); + } + return result; + } + /*! * Retrieves a reference to the backwards transition relation. * @return A reference to the backwards transition relation. diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 42aa13eb8..0f830b6fc 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -4,6 +4,7 @@ #include "src/models/AtomicPropositionsLabeling.h" #include "src/storage/BitVector.h" #include "src/storage/SparseMatrix.h" +#include "src/utility/CommandLine.h" #include #include @@ -49,7 +50,7 @@ class AbstractModel: public std::enable_shared_from_this> { } /*! - * Destructors. + * Destructor. */ virtual ~AbstractModel() { // Intentionally left empty. @@ -82,7 +83,7 @@ class AbstractModel: public std::enable_shared_from_this> { * * @return Type of the model. */ - virtual ModelType getType() = 0; + virtual ModelType getType() const = 0; /*! * Returns the state space size of the model. @@ -178,6 +179,39 @@ class AbstractModel: public std::enable_shared_from_this> { return transitionRewardMatrix != nullptr; } + /*! + * Retrieves the size of the internal representation of the model in memory. + * @return the size of the internal representation of the model in memory + * 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); + } + if (transitionRewardMatrix != nullptr) { + result += transitionRewardMatrix->getSizeInMemory(); + } + return result; + } + + /*! + * Prints information about the model to the specified stream. + * @param out The stream the information is to be printed to. + */ + void printModelInformationToStream(std::ostream& out) const { + out << "-------------------------------------------------------------- " + << std::endl; + out << "Model type: \t\t" << this->getType() << std::endl; + out << "States: \t\t" << this->getNumberOfStates() << std::endl; + out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl; + this->getStateLabeling()->printAtomicPropositionsInformationToStream(out); + out << "Size in memory: \t" + << (this->getSizeInMemory())/1024 << " kbytes" << std::endl; + out << "-------------------------------------------------------------- " + << std::endl; + } + private: /*! A matrix representing the likelihoods of moving between states. */ std::shared_ptr> transitionMatrix; diff --git a/src/models/AbstractNonDeterministicModel.h b/src/models/AbstractNonDeterministicModel.h index 153ca059c..257644093 100644 --- a/src/models/AbstractNonDeterministicModel.h +++ b/src/models/AbstractNonDeterministicModel.h @@ -19,7 +19,15 @@ template class AbstractNonDeterministicModel: public AbstractModel { public: - AbstractNonDeterministicModel(std::shared_ptr> transitionMatrix, + /*! Constructs an abstract non-determinstic model from the given parameters. + * @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 choiceIndices A mapping from states to rows in the transition matrix. + * @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> choiceIndices, std::shared_ptr> stateRewardVector, @@ -28,13 +36,28 @@ class AbstractNonDeterministicModel: public AbstractModel { choiceIndices(choiceIndices) { } + /*! + * Destructor. + */ virtual ~AbstractNonDeterministicModel() { // Intentionally left empty. } + /*! + * Copy Constructor. + */ AbstractNonDeterministicModel(AbstractNonDeterministicModel const& other) : AbstractModel(other), choiceIndices(other.choiceIndices) { + // Intentionally left empty. + } + /*! + * Retrieves the size of the internal representation of the model in memory. + * @return the size of the internal representation of the model in memory + * measured in bytes. + */ + virtual uint_fast64_t getSizeInMemory() const { + return AbstractModel::getSizeInMemory() + choiceIndices->size() * sizeof(uint_fast64_t); } private: diff --git a/src/models/Ctmc.h b/src/models/Ctmc.h index 3c4a36a75..0b8eff5fd 100644 --- a/src/models/Ctmc.h +++ b/src/models/Ctmc.h @@ -8,17 +8,12 @@ #ifndef STORM_MODELS_CTMC_H_ #define STORM_MODELS_CTMC_H_ -#include -#include #include -#include +#include +#include "AbstractDeterministicModel.h" #include "AtomicPropositionsLabeling.h" -#include "GraphTransitions.h" #include "src/storage/SparseMatrix.h" -#include "src/exceptions/InvalidArgumentException.h" - -#include "AbstractDeterministicModel.h" namespace storm { @@ -57,26 +52,7 @@ public: // Intentionally left empty. } - /*! - * Prints information about the model to the specified stream. - * @param out The stream the information is to be printed to. - */ - void printModelInformationToStream(std::ostream& out) const { - out << "-------------------------------------------------------------- " - << std::endl; - out << "Model type: \t\tCTMC" << std::endl; - out << "States: \t\t" << this->getNumberOfStates() << std::endl; - out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl; - this->getStateLabeling()->printAtomicPropositionsInformationToStream(out); - out << "Size in memory: \t" - << (this->getTransitionMatrix()->getSizeInMemory() + - this->stateLabeling()->getSizeInMemory() + - sizeof(*this))/1024 << " kbytes" << std::endl; - out << "-------------------------------------------------------------- " - << std::endl; - } - - storm::models::ModelType getType() { + storm::models::ModelType getType() const { return CTMC; } }; diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h index 37b73d748..3e1f8f5b8 100644 --- a/src/models/Ctmdp.h +++ b/src/models/Ctmdp.h @@ -8,19 +8,13 @@ #ifndef STORM_MODELS_CTMDP_H_ #define STORM_MODELS_CTMDP_H_ -#include -#include #include -#include +#include #include "AtomicPropositionsLabeling.h" -#include "GraphTransitions.h" +#include "AbstractNonDeterministicModel.h" #include "src/storage/SparseMatrix.h" -#include "src/exceptions/InvalidArgumentException.h" -#include "src/utility/CommandLine.h" #include "src/utility/Settings.h" -#include "src/models/AbstractNonDeterministicModel.h" -#include "src/parser/NonDeterministicSparseTransitionParser.h" namespace storm { @@ -74,27 +68,8 @@ public: ~Ctmdp() { // Intentionally left empty. } - - /*! - * Prints information about the model to the specified stream. - * @param out The stream the information is to be printed to. - */ - void printModelInformationToStream(std::ostream& out) const { - storm::utility::printSeparationLine(out); - out << std::endl; - out << "Model type: \t\tCTMDP" << std::endl; - out << "States: \t\t" << this->getNumberOfStates() << std::endl; - out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl; - this->getStateLabeling()->printAtomicPropositionsInformationToStream(out); - out << "Size in memory: \t" - << (this->getTransitionMatrix()->getSizeInMemory() + - this->getStateLabeling()->getSizeInMemory() + - sizeof(*this))/1024 << " kbytes" << std::endl; - out << std::endl; - storm::utility::printSeparationLine(out); - } - - storm::models::ModelType getType() { + + storm::models::ModelType getType() const { return CTMDP; } diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 42e6279d3..eefcc2ab5 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -13,13 +13,11 @@ #include #include +#include "AbstractDeterministicModel.h" #include "AtomicPropositionsLabeling.h" -#include "GraphTransitions.h" #include "src/storage/SparseMatrix.h" #include "src/exceptions/InvalidArgumentException.h" -#include "src/utility/CommandLine.h" #include "src/utility/Settings.h" -#include "src/models/AbstractDeterministicModel.h" namespace storm { @@ -75,27 +73,8 @@ public: ~Dtmc() { // Intentionally left empty. } - - /*! - * Prints information about the model to the specified stream. - * @param out The stream the information is to be printed to. - */ - void printModelInformationToStream(std::ostream& out) const { - storm::utility::printSeparationLine(out); - out << std::endl; - out << "Model type: \t\tDTMC" << std::endl; - out << "States: \t\t" << this->getNumberOfStates() << std::endl; - out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl; - this->getStateLabeling()->printAtomicPropositionsInformationToStream(out); - out << "Size in memory: \t" - << (this->getTransitionMatrix()->getSizeInMemory() + - this->getStateLabeling()->getSizeInMemory() + - sizeof(*this))/1024 << " kbytes" << std::endl; - out << std::endl; - storm::utility::printSeparationLine(out); - } - storm::models::ModelType getType() { + storm::models::ModelType getType() const { return DTMC; } diff --git a/src/models/GraphTransitions.h b/src/models/GraphTransitions.h index 1cf152666..561165501 100644 --- a/src/models/GraphTransitions.h +++ b/src/models/GraphTransitions.h @@ -61,6 +61,16 @@ public: } } + /*! + * Retrieves the size of the internal representation of the graph transitions in memory. + * @return the size of the internal representation of the graph transitions in memory + * measured in bytes. + */ + virtual uint_fast64_t getSizeInMemory() const { + uint_fast64_t result = sizeof(this) + (numberOfStates + numberOfNonZeroTransitions + 1) * sizeof(uint_fast64_t); + return result; + } + /*! * Returns an iterator to the successors of the given state. * @param state The state for which to get the successor iterator. diff --git a/src/models/Mdp.h b/src/models/Mdp.h index 357fa1433..dc92dfda6 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -14,13 +14,9 @@ #include #include "AtomicPropositionsLabeling.h" -#include "GraphTransitions.h" #include "src/storage/SparseMatrix.h" -#include "src/exceptions/InvalidArgumentException.h" -#include "src/utility/CommandLine.h" #include "src/utility/Settings.h" #include "src/models/AbstractNonDeterministicModel.h" -#include "src/parser/NonDeterministicSparseTransitionParser.h" namespace storm { @@ -75,26 +71,7 @@ public: // Intentionally left empty. } - /*! - * Prints information about the model to the specified stream. - * @param out The stream the information is to be printed to. - */ - void printModelInformationToStream(std::ostream& out) const { - storm::utility::printSeparationLine(out); - out << std::endl; - out << "Model type: \t\tMDP" << std::endl; - out << "States: \t\t" << this->getNumberOfStates() << std::endl; - out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl; - this->getStateLabeling()->printAtomicPropositionsInformationToStream(out); - out << "Size in memory: \t" - << (this->getTransitionMatrix()->getSizeInMemory() + - this->getStateLabeling()->getSizeInMemory() + - sizeof(*this))/1024 << " kbytes" << std::endl; - out << std::endl; - storm::utility::printSeparationLine(out); - } - - storm::models::ModelType getType() { + storm::models::ModelType getType() const { return MDP; }