From ad39b23c1c87ae0f30c549632b002196388e7939 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 2 Jun 2020 14:17:46 +0200 Subject: [PATCH] StateValuations: Added class to conveniently iterate over the variable-value assignments of a given state --- src/storm/storage/sparse/StateValuations.cpp | 140 ++++++++++++------- src/storm/storage/sparse/StateValuations.h | 37 ++++- 2 files changed, 127 insertions(+), 50 deletions(-) diff --git a/src/storm/storage/sparse/StateValuations.cpp b/src/storm/storage/sparse/StateValuations.cpp index 0dbe726bf..541e56b90 100644 --- a/src/storm/storage/sparse/StateValuations.cpp +++ b/src/storm/storage/sparse/StateValuations.cpp @@ -19,6 +19,61 @@ namespace storm { STORM_LOG_ASSERT(assertValuation(valuations[stateIndex]), "Invalid state valuations"); return valuations[stateIndex]; } + + StateValuations::StateValueIterator::StateValueIterator(typename std::map::const_iterator variableIt, StateValuation const* valuation) : variableIt(variableIt), valuation(valuation) { + // Intentionally left empty. + } + + storm::expressions::Variable const& StateValuations::StateValueIterator::getVariable() const { return variableIt->first; } + bool StateValuations::StateValueIterator::isBoolean() const { return getVariable().hasBooleanType(); } + bool StateValuations::StateValueIterator::isInteger() const { return getVariable().hasIntegerType(); } + bool StateValuations::StateValueIterator::isRational() const { return getVariable().hasRationalType(); } + + bool StateValuations::StateValueIterator::getBooleanValue() const { + STORM_LOG_ASSERT(isBoolean(), "Variable has no boolean type."); + return valuation->booleanValues[variableIt->second]; + } + + int64_t StateValuations::StateValueIterator::getIntegerValue() const { + STORM_LOG_ASSERT(isInteger(), "Variable has no integer type."); + return valuation->integerValues[variableIt->second]; + } + + storm::RationalNumber StateValuations::StateValueIterator::getRationalValue() const { + STORM_LOG_ASSERT(isRational(), "Variable has no rational type."); + return valuation->rationalValues[variableIt->second]; + } + + bool StateValuations::StateValueIterator::operator==(StateValueIterator const& other) { + STORM_LOG_ASSERT(valuation == valuation, "Comparing iterators for different states"); + return variableIt == other.variableIt; + } + bool StateValuations::StateValueIterator::operator!=(StateValueIterator const& other) { + STORM_LOG_ASSERT(valuation == valuation, "Comparing iterators for different states"); + return variableIt != other.variableIt; + } + + typename StateValuations::StateValueIterator& StateValuations::StateValueIterator::operator++() { + ++variableIt; + return *this; + } + + typename StateValuations::StateValueIterator& StateValuations::StateValueIterator::operator--() { + --variableIt; + return *this; + } + + StateValuations::StateValueIteratorRange::StateValueIteratorRange(std::map const& variableMap, StateValuation const* valuation) : variableMap(variableMap), valuation(valuation) { + // Intentionally left empty. + } + + StateValuations::StateValueIterator StateValuations::StateValueIteratorRange::begin() const { + return StateValueIterator(variableMap.cbegin(), valuation); + } + + StateValuations::StateValueIterator StateValuations::StateValueIteratorRange::end() const { + return StateValueIterator(variableMap.cend(), valuation); + } bool StateValuations::getBooleanValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& booleanVariable) const { auto const& valuation = getValuation(stateIndex); @@ -44,55 +99,48 @@ namespace storm { } std::string StateValuations::toString(storm::storage::sparse::state_type const& stateIndex, bool pretty, boost::optional> const& selectedVariables) const { - auto const& valuation = getValuation(stateIndex); - typename std::map::const_iterator mapIt = variableToIndexMap.begin(); + auto const& valueAssignment = at(stateIndex); typename std::set::const_iterator setIt; if (selectedVariables) { setIt = selectedVariables->begin(); } std::vector assignments; - while (mapIt != variableToIndexMap.end() && (!selectedVariables || setIt != selectedVariables->end())) { - - // Move Map iterator to next relevant position - if (selectedVariables) { - while (mapIt->first != *setIt) { - ++mapIt; - STORM_LOG_ASSERT(mapIt != variableToIndexMap.end(), "Valuation does not consider selected variable " << setIt->getName() << "."); - } + for (auto valIt = valueAssignment.begin(); valIt != valueAssignment.end(); ++valIt) { + if (selectedVariables && (*setIt != valIt.getVariable())) { + continue; } - - auto const& variable = mapIt->first; + std::stringstream stream; if (pretty) { - if (variable.hasBooleanType() && !valuation.booleanValues[mapIt->second]) { + if (valIt.isBoolean() && !valIt.getBooleanValue()) { stream << "!"; } - stream << variable.getName(); - if (variable.hasIntegerType()) { - stream << "=" << valuation.integerValues[mapIt->second]; - } else if (variable.hasRationalType()) { - stream << "=" << valuation.rationalValues[mapIt->second]; + stream << valIt.getVariable().getName(); + if (valIt.isInteger()) { + stream << "=" << valIt.getIntegerValue(); + } else if (valIt.isRational()) { + stream << "=" << valIt.getRationalValue(); } else { - STORM_LOG_THROW(variable.hasBooleanType(), storm::exceptions::InvalidTypeException, "Unexpected variable type."); + STORM_LOG_THROW(valIt.isBoolean(), storm::exceptions::InvalidTypeException, "Unexpected variable type."); } } else { - if (variable.hasBooleanType()) { - stream << std::boolalpha << valuation.booleanValues[mapIt->second] << std::noboolalpha; - } else if (variable.hasIntegerType()) { - stream << valuation.integerValues[mapIt->second]; - } else if (variable.hasRationalType()) { - stream << valuation.rationalValues[mapIt->second]; + if (valIt.isBoolean()) { + stream << std::boolalpha << valIt.getBooleanValue() << std::noboolalpha; + } else if (valIt.isInteger()) { + stream << valIt.getIntegerValue(); + } else if (valIt.isRational()) { + stream << valIt.getRationalValue(); } } assignments.push_back(stream.str()); - // Go to next position if (selectedVariables) { + // Go to next selected position ++setIt; - } else { - ++mapIt; } } + STORM_LOG_ASSERT(!selectedVariables || setIt == selectedVariables->end(), "Valuation does not consider selected variable " << setIt->getName() << "."); + if (pretty) { return "[" + boost::join(assignments, "\t& ") + "]"; } else { @@ -101,38 +149,29 @@ namespace storm { } typename StateValuations::Json StateValuations::toJson(storm::storage::sparse::state_type const& stateIndex, boost::optional> const& selectedVariables) const { - auto const& valuation = getValuation(stateIndex); - typename std::map::const_iterator mapIt = variableToIndexMap.begin(); + auto const& valueAssignment = at(stateIndex); typename std::set::const_iterator setIt; if (selectedVariables) { setIt = selectedVariables->begin(); } Json result; - while (mapIt != variableToIndexMap.end() && (!selectedVariables || setIt != selectedVariables->end())) { - // Move Map iterator to next relevant position - if (selectedVariables) { - while (mapIt->first != *setIt) { - ++mapIt; - STORM_LOG_ASSERT(mapIt != variableToIndexMap.end(), "Valuation does not consider selected variable " << setIt->getName() << "."); - } + for (auto valIt = valueAssignment.begin(); valIt != valueAssignment.end(); ++valIt) { + if (selectedVariables && (*setIt != valIt.getVariable())) { + continue; } - auto const& variable = mapIt->first; - if (variable.hasBooleanType()) { - result[variable.getName()] = bool(valuation.booleanValues[mapIt->second]); - } else if (variable.hasIntegerType()) { - result[variable.getName()] = valuation.integerValues[mapIt->second]; - } else if (variable.hasRationalType()) { - result[variable.getName()] = valuation.rationalValues[mapIt->second]; + if (valIt.isBoolean()) { + result[valIt.getVariable().getName()] = valIt.getBooleanValue(); + } else if (valIt.isInteger()) { + result[valIt.getVariable().getName()] = valIt.getIntegerValue(); } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type."); + STORM_LOG_ASSERT(valIt.isRational(), "Unexpected variable type."); + result[valIt.getVariable().getName()] = valIt.getRationalValue(); } - // Go to next position if (selectedVariables) { + // Go to next selected position ++setIt; - } else { - ++mapIt; } } return result; @@ -179,6 +218,11 @@ namespace storm { return this->toString(state); } + typename StateValuations::StateValueIteratorRange StateValuations::at(state_type const& state) const { + STORM_LOG_ASSERT(state < getNumberOfStates(), "Invalid state index."); + return StateValueIteratorRange({variableToIndexMap, &(valuations[state])}); + } + uint_fast64_t StateValuations::getNumberOfStates() const { return valuations.size(); } diff --git a/src/storm/storage/sparse/StateValuations.h b/src/storm/storage/sparse/StateValuations.h index 8626f89c0..07027d52b 100644 --- a/src/storm/storage/sparse/StateValuations.h +++ b/src/storm/storage/sparse/StateValuations.h @@ -2,6 +2,7 @@ #include #include +#include #include "storm/storage/sparse/StateType.h" #include "storm/storage/BitVector.h" @@ -34,11 +35,43 @@ namespace storm { std::vector rationalValues; }; - - StateValuations() = default; + class StateValueIterator { + public: + StateValueIterator(typename std::map::const_iterator variableIt, StateValuation const* valuation); + bool operator==(StateValueIterator const& other); + bool operator!=(StateValueIterator const& other); + StateValueIterator& operator++(); + StateValueIterator& operator--(); + + storm::expressions::Variable const& getVariable() const; + bool isBoolean() const; + bool isInteger() const; + bool isRational() const; + + // These shall only be called if the variable has the correct type + bool getBooleanValue() const; + int64_t getIntegerValue() const; + storm::RationalNumber getRationalValue() const; + + private: + typename std::map::const_iterator variableIt; + StateValuation const* const valuation; + }; + + class StateValueIteratorRange { + public: + StateValueIteratorRange(std::map const& variableMap, StateValuation const* valuation); + StateValueIterator begin() const; + StateValueIterator end() const; + private: + std::map const& variableMap; + StateValuation const* const valuation; + }; + StateValuations() = default; virtual ~StateValuations() = default; virtual std::string getStateInfo(storm::storage::sparse::state_type const& state) const override; + StateValueIteratorRange at(storm::storage::sparse::state_type const& state) const; bool getBooleanValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& booleanVariable) const; int64_t const& getIntegerValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& integerVariable) const;