From 7ce969b312688e8f852ac568351990f6b22afd74 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 23 Feb 2016 17:59:00 +0100 Subject: [PATCH] started working on more flexible model generation using next-state-generators Former-commit-id: 805940f1790292223f9216cc9dd146af12d3d6c8 --- src/CMakeLists.txt | 4 + src/builder/ExplicitPrismModelBuilder.cpp | 39 +---- src/builder/ExplicitPrismModelBuilder.h | 54 ------- src/generator/Choice.cpp | 111 ++++++++++++++ src/generator/Choice.h | 158 ++++++++++++++++++++ src/generator/NextStateGenerator.h | 27 ++++ src/generator/PrismNextStateGenerator.cpp | 22 +++ src/generator/PrismNextStateGenerator.h | 32 ++++ src/generator/prism/VariableInformation.cpp | 44 ++++++ src/generator/prism/VariableInformation.h | 73 +++++++++ src/storage/Distribution.cpp | 52 +++---- src/storage/Distribution.h | 12 +- 12 files changed, 504 insertions(+), 124 deletions(-) create mode 100644 src/generator/Choice.cpp create mode 100644 src/generator/Choice.h create mode 100644 src/generator/NextStateGenerator.h create mode 100644 src/generator/PrismNextStateGenerator.cpp create mode 100644 src/generator/PrismNextStateGenerator.h create mode 100644 src/generator/prism/VariableInformation.cpp create mode 100644 src/generator/prism/VariableInformation.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5b06a498d..0a5832d87 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -11,6 +11,8 @@ file(GLOB_RECURSE STORM_SOURCES_CLI ${PROJECT_SOURCE_DIR}/src/cli/*.cpp) file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm.cpp) file(GLOB_RECURSE STORM_ADAPTERS_FILES ${PROJECT_SOURCE_DIR}/src/adapters/*.h ${PROJECT_SOURCE_DIR}/src/adapters/*.cpp) file(GLOB_RECURSE STORM_BUILDER_FILES ${PROJECT_SOURCE_DIR}/src/builder/*.h ${PROJECT_SOURCE_DIR}/src/builder/*.cpp) +file(GLOB STORM_GENERATOR_FILES ${PROJECT_SOURCE_DIR}/src/generator/*.h ${PROJECT_SOURCE_DIR}/src/generator/*.cpp) +file(GLOB_RECURSE STORM_GENERATOR_PRISM_FILES ${PROJECT_SOURCE_DIR}/src/generator/prism/*.h ${PROJECT_SOURCE_DIR}/src/generator/prism/*.cpp) file(GLOB_RECURSE STORM_CLI_FILES ${PROJECT_SOURCE_DIR}/src/cli/*.h ${PROJECT_SOURCE_DIR}/src/cli/*.cpp) file(GLOB_RECURSE STORM_EXCEPTIONS_FILES ${PROJECT_SOURCE_DIR}/src/exceptions/*.h ${PROJECT_SOURCE_DIR}/src/exceptions/*.cpp) file(GLOB_RECURSE STORM_LOGIC_FILES ${PROJECT_SOURCE_DIR}/src/logic/*.h ${PROJECT_SOURCE_DIR}/src/logic/*.cpp) @@ -57,6 +59,8 @@ set(STORM_MAIN_HEADERS ${STORM_HEADERS_CLI}) source_group(main FILES ${STORM_MAIN_FILE}) source_group(adapters FILES ${STORM_ADAPTERS_FILES}) source_group(builder FILES ${STORM_BUILDER_FILES}) +source_group(generator FILES ${STORM_GENERATOR_FILES}) +source_group(generator\\prism FILES ${STORM_GENERATOR_PRISM_FILES}) source_group(cli FILES ${STORM_CLI_FILES}) source_group(exceptions FILES ${STORM_EXCEPTIONS_FILES}) source_group(logic FILES ${STORM_LOGIC_FILES}) diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index d7c2f6293..19b115c6e 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -75,44 +75,7 @@ namespace storm { ExplicitPrismModelBuilder::InternalStateInformation::InternalStateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), bitsPerState(bitsPerState), reachableStates() { // Intentionally left empty. } - - template - ExplicitPrismModelBuilder::VariableInformation::BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset) : variable(variable), initialValue(initialValue), bitOffset(bitOffset) { - // Intentionally left empty. - } - - template - ExplicitPrismModelBuilder::VariableInformation::IntegerVariableInformation::IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : variable(variable), initialValue(initialValue), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth) { - // Intentionally left empty. - } - - template - ExplicitPrismModelBuilder::VariableInformation::VariableInformation(storm::expressions::ExpressionManager const& manager) : manager(manager) { - // Intentionally left empty. - } - - template - uint_fast64_t ExplicitPrismModelBuilder::VariableInformation::getBitOffset(storm::expressions::Variable const& variable) const { - auto const& booleanIndex = booleanVariableToIndexMap.find(variable); - if (booleanIndex != booleanVariableToIndexMap.end()) { - return booleanVariables[booleanIndex->second].bitOffset; - } - auto const& integerIndex = integerVariableToIndexMap.find(variable); - if (integerIndex != integerVariableToIndexMap.end()) { - return integerVariables[integerIndex->second].bitOffset; - } - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit index of unknown variable."); - } - - template - uint_fast64_t ExplicitPrismModelBuilder::VariableInformation::getBitWidth(storm::expressions::Variable const& variable) const { - auto const& integerIndex = integerVariableToIndexMap.find(variable); - if (integerIndex != integerVariableToIndexMap.end()) { - return integerVariables[integerIndex->second].bitWidth; - } - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit width of unknown variable."); - } - + template ExplicitPrismModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() { // Intentionally left empty. diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h index ccb0622e7..9bd62ad2b 100644 --- a/src/builder/ExplicitPrismModelBuilder.h +++ b/src/builder/ExplicitPrismModelBuilder.h @@ -74,60 +74,6 @@ namespace storm { } }; - // A structure storing information about the used variables of the program. - struct VariableInformation { - VariableInformation(storm::expressions::ExpressionManager const& manager); - - struct BooleanVariableInformation { - BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset); - - // The boolean variable. - storm::expressions::Variable variable; - - // Its initial value. - bool initialValue; - - // Its bit offset in the compressed state. - uint_fast64_t bitOffset; - }; - - struct IntegerVariableInformation { - IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth); - - // The integer variable. - storm::expressions::Variable variable; - - // Its initial value. - int_fast64_t initialValue; - - // The lower bound of its range. - int_fast64_t lowerBound; - - // The upper bound of its range. - int_fast64_t upperBound; - - // Its bit offset in the compressed state. - uint_fast64_t bitOffset; - - // Its bit width in the compressed state. - uint_fast64_t bitWidth; - }; - - // Provide methods to access the bit offset and width of variables in the compressed state. - uint_fast64_t getBitOffset(storm::expressions::Variable const& variable) const; - uint_fast64_t getBitWidth(storm::expressions::Variable const& variable) const; - - // The known boolean variables. - boost::container::flat_map booleanVariableToIndexMap; - std::vector booleanVariables; - - // The known integer variables. - boost::container::flat_map integerVariableToIndexMap; - std::vector integerVariables; - - storm::expressions::ExpressionManager const& manager; - }; - // A structure holding the individual components of a model. struct ModelComponents { ModelComponents(); diff --git a/src/generator/Choice.cpp b/src/generator/Choice.cpp new file mode 100644 index 000000000..3b6609ebd --- /dev/null +++ b/src/generator/Choice.cpp @@ -0,0 +1,111 @@ +#include "src/generator/Choice.h" + +#include "src/utility/constants.h" + +namespace storm { + namespace generator { + + template + Choice::Choice(uint_fast64_t actionIndex, bool markovian) : markovian(markovian), actionIndex(actionIndex), distribution(), totalMass(storm::utility::zero()), choiceReward(storm::utility::zero()) { + // Intentionally left empty. + } + + template + typename storm::storage::Distribution::iterator Choice::begin() { + return distribution.begin(); + } + + template + typename storm::storage::Distribution::const_iterator Choice::begin() const { + return distribution.cbegin(); + } + + template + typename storm::storage::Distribution::iterator Choice::end() { + return distribution.end(); + } + + template + typename storm::storage::Distribution::const_iterator Choice::end() const { + return distribution.cend(); + } + + template + void Choice::addChoiceLabel(uint_fast64_t label) { + if (!choiceLabels) { + choiceLabels = LabelSet(); + } + choiceLabels->insert(label); + } + + template + void Choice::addChoiceLabels(LabelSet const& labelSet) { + if (!choiceLabels) { + choiceLabels = LabelSet(); + } + choiceLabels->insert(labelSet.begin(), labelSet.end()); + } + + template + boost::container::flat_set const& Choice::getChoiceLabels() const { + return *choiceLabels; + } + + template + uint_fast64_t Choice::getActionIndex() const { + return actionIndex; + } + + template + ValueType Choice::getTotalMass() const { + return totalMass; + } + + template + ValueType& Choice::getOrAddEntry(StateType const& state) { + auto stateProbabilityPair = distribution.find(state); + + if (stateProbabilityPair == distribution.end()) { + distribution[state] = ValueType(); + } + return distribution.at(state); + } + + template + ValueType const& Choice::getOrAddEntry(StateType const& state) const { + auto stateProbabilityPair = distribution.find(state); + + if (stateProbabilityPair == distribution.end()) { + distribution[state] = ValueType(); + } + return distribution.at(state); + } + + template + void Choice::addProbability(StateType const& state, ValueType const& value) { + totalMass += value; + distribution[state] += value; + } + + template + void Choice::addChoiceReward(ValueType const& value) { + choiceReward += value; + } + + template + std::size_t Choice::size() const { + return distribution.size(); + } + + template + std::ostream& operator<<(std::ostream& out, Choice const& choice) { + out << "<"; + for (auto const& stateProbabilityPair : choice) { + out << stateProbabilityPair.first << " : " << stateProbabilityPair.second << ", "; + } + out << ">"; + return out; + } + + } +} \ No newline at end of file diff --git a/src/generator/Choice.h b/src/generator/Choice.h new file mode 100644 index 000000000..07eb6efbe --- /dev/null +++ b/src/generator/Choice.h @@ -0,0 +1,158 @@ +#ifndef STORM_GENERATOR_CHOICE_H_ +#define STORM_GENERATOR_CHOICE_H_ + +#include +#include + +#include +#include + +#include "src/storage/Distribution.h" + +namespace storm { + namespace generator { + + // A structure holding information about a particular choice. + template + struct Choice { + public: + typedef boost::container::flat_set LabelSet; + + Choice(uint_fast64_t actionIndex = 0, bool markovian = false); + + Choice(Choice const& other) = default; + Choice& operator=(Choice const& other) = default; + Choice(Choice&& other) = default; + Choice& operator=(Choice&& other) = default; + + /*! + * Returns an iterator to the distribution associated with this choice. + * + * @return An iterator to the first element of the distribution. + */ + typename storm::storage::Distribution::iterator begin(); + + /*! + * Returns an iterator to the distribution associated with this choice. + * + * @return An iterator to the first element of the distribution. + */ + typename storm::storage::Distribution::const_iterator begin() const; + + /*! + * Returns an iterator past the end of the distribution associated with this choice. + * + * @return An iterator past the end of the distribution. + */ + typename storm::storage::Distribution::iterator end(); + + /*! + * Returns an iterator past the end of the distribution associated with this choice. + * + * @return An iterator past the end of the distribution. + */ + typename storm::storage::Distribution::const_iterator end() const; + + /*! + * Inserts the contents of this object to the given output stream. + * + * @param out The stream in which to insert the contents. + */ + template + friend std::ostream& operator<<(std::ostream& out, Choice const& choice); + + /*! + * Adds the given label to the labels associated with this choice. + * + * @param label The label to associate with this choice. + */ + void addChoiceLabel(uint_fast64_t label); + + /*! + * Adds the given label set to the labels associated with this choice. + * + * @param labelSet The label set to associate with this choice. + */ + void addChoiceLabels(LabelSet const& labelSet); + + /*! + * Retrieves the set of labels associated with this choice. + * + * @return The set of labels associated with this choice. + */ + LabelSet const& getChoiceLabels() const; + + /*! + * Retrieves the index of the action of this choice. + * + * @return The index of the action of this choice. + */ + uint_fast64_t getActionIndex() const; + + /*! + * Retrieves the total mass of this choice. + * + * @return The total mass. + */ + ValueType getTotalMass() const; + + /*! + * Retrieves the entry in the choice that is associated with the given state and creates one if none exists, + * yet. + * + * @param state The state for which to add the entry. + * @return A reference to the entry that is associated with the given state. + */ + ValueType& getOrAddEntry(StateType const& state); + + /*! + * Retrieves the entry in the choice that is associated with the given state and creates one if none exists, + * yet. + * + * @param state The state for which to add the entry. + * @return A reference to the entry that is associated with the given state. + */ + ValueType const& getOrAddEntry(StateType const& state) const; + + /*! + * Adds the given probability value to the given state in the underlying distribution. + */ + void addProbability(StateType const& state, ValueType const& value); + + /*! + * Adds the given value to the reward associated with this choice. + */ + void addChoiceReward(ValueType const& value); + + /*! + * Retrieves the size of the distribution associated with this choice. + */ + std::size_t size() const; + + private: + // A flag indicating whether this choice is Markovian or not. + bool markovian; + + // The action index associated with this choice. + uint_fast64_t actionIndex; + + // The distribution that is associated with the choice. + storm::storage::Distribution distribution; + + // The total probability mass (or rates) of this choice. + ValueType totalMass; + + // The reward value associated with this choice. + ValueType choiceReward; + + // The labels that are associated with this choice. + boost::optional choiceLabels; + }; + + template + std::ostream& operator<<(std::ostream& out, Choice const& choice); + + } +} + +#endif /* STORM_GENERATOR_CHOICE_H_ */ \ No newline at end of file diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h new file mode 100644 index 000000000..1fdc38cfb --- /dev/null +++ b/src/generator/NextStateGenerator.h @@ -0,0 +1,27 @@ +#ifndef STORM_GENERATOR_NEXTSTATEGENERATOR_H_ +#define STORM_GENERATOR_NEXTSTATEGENERATOR_H_ + +#include +#include + +#include "src/storage/sparse/StateType.h" +#include "src/storage/BitVector.h" + +#include "src/generator/Choice.h" + +namespace storm { + namespace generator { + template + class NextStateGenerator { + public: + typedef storm::storage::BitVector InternalStateType; + typedef StateType (*StateToIdCallback)(InternalStateType const&); + + virtual std::vector getInitialStates(StateToIdCallback stateToIdCallback) = 0; + virtual std::vector> expand(StateType const& state, StateToIdCallback stateToIdCallback) = 0; + virtual ValueType getStateReward(StateType const& state) = 0; + }; + } +} + +#endif \ No newline at end of file diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp new file mode 100644 index 000000000..0acf4d8dd --- /dev/null +++ b/src/generator/PrismNextStateGenerator.cpp @@ -0,0 +1,22 @@ +#include "src/generator/PrismNextStateGenerator.h" + +namespace storm { + namespace generator { + + template + PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program) : program(program) { + // Intentionally left empty. + } + + template + std::vector> PrismNextStateGenerator::expand(StateType const& state, typename NextStateGenerator::StateToIdCallback stateToIdCallback) { + // TODO + } + + template + ValueType PrismNextStateGenerator::getStateReward(StateType const& state) { + // TODO + } + + } +} \ No newline at end of file diff --git a/src/generator/PrismNextStateGenerator.h b/src/generator/PrismNextStateGenerator.h new file mode 100644 index 000000000..1330d4420 --- /dev/null +++ b/src/generator/PrismNextStateGenerator.h @@ -0,0 +1,32 @@ +#ifndef STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_ +#define STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_ + +#include "src/generator/NextStateGenerator.h" + +#include "src/storage/prism/Program.h" + +namespace storm { + namespace generator { + + template + class PrismNextStateGenerator : public NextStateGenerator { + public: + typedef typename NextStateGenerator::StateToIdCallback StateToIdCallback; + + PrismNextStateGenerator(storm::prism::Program const& program); + + virtual std::vector getInitialStates(StateToIdCallback stateToIdCallback) = 0; + virtual std::vector> expand(StateType const& state, StateToIdCallback stateToIdCallback) override; + virtual ValueType getStateReward(StateType const& state) override; + + private: + // The program used for the generation of next states. + storm::prism::Program program; + + + }; + + } +} + +#endif /* STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_ */ \ No newline at end of file diff --git a/src/generator/prism/VariableInformation.cpp b/src/generator/prism/VariableInformation.cpp new file mode 100644 index 000000000..f648eda1b --- /dev/null +++ b/src/generator/prism/VariableInformation.cpp @@ -0,0 +1,44 @@ +#include "src/generator/prism/VariableInformation.h" + +#include "src/utility/macros.h" +#include "src/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace generator { + namespace prism { + + BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset) : variable(variable), initialValue(initialValue), bitOffset(bitOffset) { + // Intentionally left empty. + } + + IntegerVariableInformation::IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : variable(variable), initialValue(initialValue), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth) { + // Intentionally left empty. + } + + VariableInformation::VariableInformation(storm::expressions::ExpressionManager const& manager) : manager(manager) { + // Intentionally left empty. + } + + uint_fast64_t VariableInformation::getBitOffset(storm::expressions::Variable const& variable) const { + auto const& booleanIndex = booleanVariableToIndexMap.find(variable); + if (booleanIndex != booleanVariableToIndexMap.end()) { + return booleanVariables[booleanIndex->second].bitOffset; + } + auto const& integerIndex = integerVariableToIndexMap.find(variable); + if (integerIndex != integerVariableToIndexMap.end()) { + return integerVariables[integerIndex->second].bitOffset; + } + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit index of unknown variable."); + } + + uint_fast64_t VariableInformation::getBitWidth(storm::expressions::Variable const& variable) const { + auto const& integerIndex = integerVariableToIndexMap.find(variable); + if (integerIndex != integerVariableToIndexMap.end()) { + return integerVariables[integerIndex->second].bitWidth; + } + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit width of unknown variable."); + } + + } + } +} \ No newline at end of file diff --git a/src/generator/prism/VariableInformation.h b/src/generator/prism/VariableInformation.h new file mode 100644 index 000000000..56ac7bda2 --- /dev/null +++ b/src/generator/prism/VariableInformation.h @@ -0,0 +1,73 @@ +#ifndef STORM_GENERATOR_PRISM_VARIABLEINFORMATION_H_ +#define STORM_GENERATOR_PRISM_VARIABLEINFORMATION_H_ + +#include +#include + +#include "src/storage/expressions/Variable.h" + +namespace storm { + namespace generator { + namespace prism { + + // A structure storing information about the boolean variables of the program. + struct BooleanVariableInformation { + BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset); + + // The boolean variable. + storm::expressions::Variable variable; + + // Its initial value. + bool initialValue; + + // Its bit offset in the compressed state. + uint_fast64_t bitOffset; + }; + + // A structure storing information about the integer variables of the program. + struct IntegerVariableInformation { + IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth); + + // The integer variable. + storm::expressions::Variable variable; + + // Its initial value. + int_fast64_t initialValue; + + // The lower bound of its range. + int_fast64_t lowerBound; + + // The upper bound of its range. + int_fast64_t upperBound; + + // Its bit offset in the compressed state. + uint_fast64_t bitOffset; + + // Its bit width in the compressed state. + uint_fast64_t bitWidth; + }; + + // A structure storing information about the used variables of the program. + struct VariableInformation { + VariableInformation(storm::expressions::ExpressionManager const& manager); + + // Provide methods to access the bit offset and width of variables in the compressed state. + uint_fast64_t getBitOffset(storm::expressions::Variable const& variable) const; + uint_fast64_t getBitWidth(storm::expressions::Variable const& variable) const; + + // The known boolean variables. + boost::container::flat_map booleanVariableToIndexMap; + std::vector booleanVariables; + + // The known integer variables. + boost::container::flat_map integerVariableToIndexMap; + std::vector integerVariables; + + storm::expressions::ExpressionManager const& manager; + }; + + } + } +} + +#endif /* STORM_GENERATOR_PRISM_VARIABLEINFORMATION_H_ */ \ No newline at end of file diff --git a/src/storage/Distribution.cpp b/src/storage/Distribution.cpp index 50d794d01..516227277 100644 --- a/src/storage/Distribution.cpp +++ b/src/storage/Distribution.cpp @@ -14,13 +14,13 @@ namespace storm { namespace storage { - template - Distribution::Distribution() { + template + Distribution::Distribution() { // Intentionally left empty. } - template - bool Distribution::equals(Distribution const& other, storm::utility::ConstantsComparator const& comparator) const { + template + bool Distribution::equals(Distribution const& other, storm::utility::ConstantsComparator const& comparator) const { // We need to check equality by ourselves, because we need to account for epsilon differences. if (this->distribution.size() != other.distribution.size()) { return false; @@ -42,8 +42,8 @@ namespace storm { return true; } - template - void Distribution::addProbability(storm::storage::sparse::state_type const& state, ValueType const& probability) { + template + void Distribution::addProbability(StateType const& state, ValueType const& probability) { auto it = this->distribution.find(state); if (it == this->distribution.end()) { this->distribution.emplace_hint(it, state, probability); @@ -52,8 +52,8 @@ namespace storm { } } - template - void Distribution::removeProbability(storm::storage::sparse::state_type const& state, ValueType const& probability, storm::utility::ConstantsComparator const& comparator) { + template + void Distribution::removeProbability(StateType const& state, ValueType const& probability, storm::utility::ConstantsComparator const& comparator) { auto it = this->distribution.find(state); STORM_LOG_ASSERT(it != this->distribution.end(), "Cannot remove probability, because the state is not in the support of the distribution."); it->second -= probability; @@ -62,34 +62,34 @@ namespace storm { } } - template - void Distribution::shiftProbability(storm::storage::sparse::state_type const& fromState, storm::storage::sparse::state_type const& toState, ValueType const& probability, storm::utility::ConstantsComparator const& comparator) { + template + void Distribution::shiftProbability(StateType const& fromState, StateType const& toState, ValueType const& probability, storm::utility::ConstantsComparator const& comparator) { removeProbability(fromState, probability, comparator); addProbability(toState, probability); } - template - typename Distribution::iterator Distribution::begin() { + template + typename Distribution::iterator Distribution::begin() { return this->distribution.begin(); } - template - typename Distribution::const_iterator Distribution::begin() const { + template + typename Distribution::const_iterator Distribution::begin() const { return this->distribution.begin(); } - template - typename Distribution::iterator Distribution::end() { + template + typename Distribution::iterator Distribution::end() { return this->distribution.end(); } - template - typename Distribution::const_iterator Distribution::end() const { + template + typename Distribution::const_iterator Distribution::end() const { return this->distribution.end(); } - template - void Distribution::scale(storm::storage::sparse::state_type const& state) { + template + void Distribution::scale(StateType const& state) { auto probabilityIterator = this->distribution.find(state); if (probabilityIterator != this->distribution.end()) { ValueType scaleValue = storm::utility::one() / probabilityIterator->second; @@ -101,13 +101,13 @@ namespace storm { } } - template - std::size_t Distribution::size() const { + template + std::size_t Distribution::size() const { return this->distribution.size(); } - template - std::ostream& operator<<(std::ostream& out, Distribution const& distribution) { + template + std::ostream& operator<<(std::ostream& out, Distribution const& distribution) { out << "{"; for (auto const& entry : distribution) { out << "[" << entry.second << ": " << entry.first << "], "; @@ -117,8 +117,8 @@ namespace storm { return out; } - template - bool Distribution::less(Distribution const& other, storm::utility::ConstantsComparator const& comparator) const { + template + bool Distribution::less(Distribution const& other, storm::utility::ConstantsComparator const& comparator) const { if (this->size() != other.size()) { return this->size() < other.size(); } diff --git a/src/storage/Distribution.h b/src/storage/Distribution.h index 9d3276941..39e6eb6f9 100644 --- a/src/storage/Distribution.h +++ b/src/storage/Distribution.h @@ -17,10 +17,10 @@ namespace storm { namespace storage { - template + template class Distribution { public: - typedef boost::container::flat_map container_type; + typedef boost::container::flat_map container_type; typedef typename container_type::iterator iterator; typedef typename container_type::const_iterator const_iterator; @@ -51,7 +51,7 @@ namespace storm { * @param state The state to which to assign the probability. * @param probability The probability to assign. */ - void addProbability(storm::storage::sparse::state_type const& state, ValueType const& probability); + void addProbability(StateType const& state, ValueType const& probability); /*! * Removes the given probability mass of going to the given state. @@ -61,7 +61,7 @@ namespace storm { * @param comparator A comparator that is used to determine if the remaining probability is zero. If so, the * entry is removed. */ - void removeProbability(storm::storage::sparse::state_type const& state, ValueType const& probability, storm::utility::ConstantsComparator const& comparator = storm::utility::ConstantsComparator()); + void removeProbability(StateType const& state, ValueType const& probability, storm::utility::ConstantsComparator const& comparator = storm::utility::ConstantsComparator()); /*! * Removes the probability mass from one state and adds it to another. @@ -72,7 +72,7 @@ namespace storm { * @param comparator A comparator that is used to determine if the remaining probability is zero. If so, the * entry is removed. */ - void shiftProbability(storm::storage::sparse::state_type const& fromState, storm::storage::sparse::state_type const& toState, ValueType const& probability, storm::utility::ConstantsComparator const& comparator = storm::utility::ConstantsComparator()); + void shiftProbability(StateType const& fromState, StateType const& toState, ValueType const& probability, storm::utility::ConstantsComparator const& comparator = storm::utility::ConstantsComparator()); /*! * Retrieves an iterator to the elements in this distribution. @@ -109,7 +109,7 @@ namespace storm { * * @param state The state whose associated probability is used to scale the distribution. */ - void scale(storm::storage::sparse::state_type const& state); + void scale(StateType const& state); /*! * Retrieves the size of the distribution, i.e. the size of the support set.