sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Refactored state valuations. They now store values for transient jani variables and do not store values for constants (solving Github issue #73)

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
3a86cc4391
commit
adfdf8c572
9 changed files with 433 additions and 51 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 23
      src/storm/builder/ExplicitModelBuilder.cpp
  2. 5
      src/storm/builder/ExplicitModelBuilder.h
  3. 90
      src/storm/generator/JaniNextStateGenerator.cpp
  4. 10
      src/storm/generator/JaniNextStateGenerator.h
  5. 29
      src/storm/generator/NextStateGenerator.cpp
  6. 9
      src/storm/generator/NextStateGenerator.h
  7. 2
      src/storm/storage/Scheduler.cpp
  8. 217
      src/storm/storage/sparse/StateValuations.cpp
  9. 99
      src/storm/storage/sparse/StateValuations.h

23
src/storm/builder/ExplicitModelBuilder.cpp
View File

@ -105,7 +105,7 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType, typename StateType>
void ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianStates) {
void ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianStates, boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder) {
// Create markovian states bit vector, if required.
if (generator->getModelType() == storm::generator::ModelType::MA) {
@ -154,6 +154,9 @@ namespace storm {
}
generator->load(currentState);
if (stateValuationsBuilder) {
generator->addStateValuation(currentIndex, stateValuationsBuilder.get());
}
storm::generator::StateBehavior<ValueType, StateType> behavior = generator->expand(stateToIdCallback);
// If there is no behavior, we might have to introduce a self-loop.
@ -188,7 +191,7 @@ namespace storm {
++currentRow;
++currentRowGroup;
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating sparse matrix from probabilistic program: found deadlock state (" << generator->toValuation(currentState).toString(true) << "). For fixing these, please provide the appropriate option.");
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating sparse matrix from probabilistic program: found deadlock state (" << generator->stateToString(currentState) << "). For fixing these, please provide the appropriate option.");
}
} else {
// Add the state rewards to the corresponding reward models.
@ -314,7 +317,13 @@ namespace storm {
ChoiceInformationBuilder choiceInformationBuilder;
boost::optional<storm::storage::BitVector> markovianStates;
buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates);
// If we need to build state valuations, initialize them now.
boost::optional<storm::storage::sparse::StateValuationsBuilder> stateValuationsBuilder;
if (generator->getOptions().isBuildStateValuationsSet()) {
stateValuationsBuilder = generator->initializeStateValuationsBuilder();
}
buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates, stateValuationsBuilder);
// Initialize the model components with the obtained information.
storm::storage::sparse::ModelComponents<ValueType, RewardModelType> modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getCurrentRowGroupCount()), buildStateLabeling(), std::unordered_map<std::string, RewardModelType>(), !generator->isDiscreteTimeModel(), std::move(markovianStates));
@ -327,12 +336,8 @@ namespace storm {
modelComponents.choiceLabeling = choiceInformationBuilder.buildChoiceLabeling(modelComponents.transitionMatrix.getRowCount());
// If requested, build the state valuations and choice origins
if (generator->getOptions().isBuildStateValuationsSet()) {
std::vector<storm::expressions::SimpleValuation> valuations(modelComponents.transitionMatrix.getRowGroupCount());
for (auto const& bitVectorIndexPair : stateStorage.stateToId) {
valuations[bitVectorIndexPair.second] = generator->toValuation(bitVectorIndexPair.first);
}
modelComponents.stateValuations = storm::storage::sparse::StateValuations(std::move(valuations));
if (stateValuationsBuilder) {
modelComponents.stateValuations = stateValuationsBuilder->build(modelComponents.transitionMatrix.getRowGroupCount());
}
if (generator->getOptions().isBuildChoiceOriginsSet()) {
auto originData = choiceInformationBuilder.buildDataOfChoiceOrigins(modelComponents.transitionMatrix.getRowCount());

5
src/storm/builder/ExplicitModelBuilder.h
View File

@ -107,9 +107,10 @@ namespace storm {
* @param transitionMatrixBuilder The builder of the transition matrix.
* @param rewardModelBuilders The builders for the selected reward models.
* @param choiceInformationBuilder The builder for the requested information of the choices
* @param markovianChoices is set to a bit vector storing whether a choice is markovian (is only set if the model type requires this information).
* @param markovianChoices is set to a bit vector storing whether a choice is Markovian (is only set if the model type requires this information).
* @param stateValuationsBuilder if not boost::none, we insert valuations for the corresponding states
*/
void buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianChoices);
void buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, ChoiceInformationBuilder& choiceInformationBuilder, boost::optional<storm::storage::BitVector>& markovianChoices, boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder);
/*!
* Explores the state space of the given program and returns the components of the model as a result.

90
src/storm/generator/JaniNextStateGenerator.cpp
View File

@ -394,7 +394,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
void JaniNextStateGenerator<ValueType, StateType>::applyTransientUpdate(TransientVariableValuation<ValueType>& transientValuation, storm::jani::detail::ConstAssignments const& transientAssignments, storm::expressions::ExpressionEvaluator<ValueType> const& expressionEvaluator) {
void JaniNextStateGenerator<ValueType, StateType>::applyTransientUpdate(TransientVariableValuation<ValueType>& transientValuation, storm::jani::detail::ConstAssignments const& transientAssignments, storm::expressions::ExpressionEvaluator<ValueType> const& expressionEvaluator) const {
auto assignmentIt = transientAssignments.begin();
auto assignmentIte = transientAssignments.end();
@ -457,15 +457,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
StateBehavior<ValueType, StateType> JaniNextStateGenerator<ValueType, StateType>::expand(StateToIdCallback const& stateToIdCallback) {
// Prepare the result, in case we return early.
StateBehavior<ValueType, StateType> result;
// Retrieve the locations from the state.
std::vector<uint64_t> locations = getLocations(*this->state);
// First, construct the state rewards, as we may return early if there are no choices later and we already
// need the state rewards then.
TransientVariableValuation<ValueType> JaniNextStateGenerator<ValueType, StateType>::getTransientVariableValuationAtLocations(std::vector<uint64_t> const& locations) const {
uint64_t automatonIndex = 0;
TransientVariableValuation<ValueType> transientVariableValuation;
for (auto const& automatonRef : this->parallelAutomata) {
@ -476,6 +468,84 @@ namespace storm {
applyTransientUpdate(transientVariableValuation, location.getAssignments().getTransientAssignments(), *this->evaluator);
++automatonIndex;
}
return transientVariableValuation;
}
template<typename ValueType, typename StateType>
storm::storage::sparse::StateValuationsBuilder JaniNextStateGenerator<ValueType, StateType>::initializeStateValuationsBuilder() const {
auto result = NextStateGenerator<ValueType, StateType>::initializeStateValuationsBuilder();
// Also add information for transient variables
for (auto const& varInfo : transientVariableInformation.booleanVariableInformation) {
result.addVariable(varInfo.variable);
}
for (auto const& varInfo : transientVariableInformation.integerVariableInformation) {
result.addVariable(varInfo.variable);
}
for (auto const& varInfo : transientVariableInformation.rationalVariableInformation) {
result.addVariable(varInfo.variable);
}
return result;
}
template<typename ValueType, typename StateType>
void JaniNextStateGenerator<ValueType, StateType>::addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const {
std::vector<bool> booleanValues;
booleanValues.reserve(this->variableInformation.booleanVariables.size() + transientVariableInformation.booleanVariableInformation.size());
std::vector<int64_t> integerValues;
integerValues.reserve(this->variableInformation.locationVariables.size() + this->variableInformation.integerVariables.size() + transientVariableInformation.integerVariableInformation.size());
std::vector<storm::RationalNumber> rationalValues;
rationalValues.reserve(transientVariableInformation.rationalVariableInformation.size());
// Add values for non-transient variables
extractVariableValues(*this->state, this->variableInformation, integerValues, booleanValues, integerValues);
// Add values for transient variables
auto transientVariableValuation = getTransientVariableValuationAtLocations(getLocations(*this->state));
{
auto varIt = transientVariableValuation.booleanValues.begin();
for (auto const& varInfo : transientVariableInformation.booleanVariableInformation) {
if (varIt->first->variable == varInfo.variable) {
booleanValues.push_back(varIt->second);
} else {
booleanValues.push_back(varInfo.defaultValue);
}
}
}
{
auto varIt = transientVariableValuation.integerValues.begin();
for (auto const& varInfo : transientVariableInformation.integerVariableInformation) {
if (varIt->first->variable == varInfo.variable) {
integerValues.push_back(varIt->second);
} else {
integerValues.push_back(varInfo.defaultValue);
}
}
}
{
auto varIt = transientVariableValuation.rationalValues.begin();
for (auto const& varInfo : transientVariableInformation.rationalVariableInformation) {
if (varIt->first->variable == varInfo.variable) {
rationalValues.push_back(storm::utility::convertNumber<storm::RationalNumber>(varIt->second));
} else {
rationalValues.push_back(storm::utility::convertNumber<storm::RationalNumber>(varInfo.defaultValue));
}
}
}
valuationsBuilder.addState(currentStateIndex, std::move(booleanValues), std::move(integerValues), std::move(rationalValues));
}
template<typename ValueType, typename StateType>
StateBehavior<ValueType, StateType> JaniNextStateGenerator<ValueType, StateType>::expand(StateToIdCallback const& stateToIdCallback) {
// Prepare the result, in case we return early.
StateBehavior<ValueType, StateType> result;
// Retrieve the locations from the state.
std::vector<uint64_t> locations = getLocations(*this->state);
// First, construct the state rewards, as we may return early if there are no choices later and we already
// need the state rewards then.
auto transientVariableValuation = getTransientVariableValuationAtLocations(locations);
transientVariableValuation.setInEvaluator(*this->evaluator, this->getOptions().isExplorationChecksSet());
result.addStateRewards(evaluateRewardExpressions());
this->transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator);

10
src/storm/generator/JaniNextStateGenerator.h
View File

@ -50,8 +50,14 @@ namespace storm {
virtual bool isPartiallyObservable() const override;
virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override;
/// Initializes a builder for state valuations by adding the appropriate variables.
virtual storm::storage::sparse::StateValuationsBuilder initializeStateValuationsBuilder() const override;
virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) override;
/// Adds the valuation for the currently loaded state to the given builder
virtual void addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const override;
virtual std::size_t getNumberOfRewardModels() const override;
virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const override;
@ -102,7 +108,7 @@ namespace storm {
* @params assignmentLevel The assignmentLevel that is to be considered for the update.
* @return The resulting state.
*/
void applyTransientUpdate(TransientVariableValuation<ValueType>& transientValuation, storm::jani::detail::ConstAssignments const& transientAssignments, storm::expressions::ExpressionEvaluator<ValueType> const& expressionEvaluator);
void applyTransientUpdate(TransientVariableValuation<ValueType>& transientValuation, storm::jani::detail::ConstAssignments const& transientAssignments, storm::expressions::ExpressionEvaluator<ValueType> const& expressionEvaluator) const;
/**
* Required method to overload, but currently throws an error as POMDPs are not yet specified in JANI.
@ -113,6 +119,8 @@ namespace storm {
*/
virtual storm::storage::BitVector evaluateObservationLabels(CompressedState const& state) const override;
TransientVariableValuation<ValueType> getTransientVariableValuationAtLocations(std::vector<uint64_t> const& locations) const;
/*!
* Retrieves all choices possible from the given state.
*

29
src/storm/generator/NextStateGenerator.cpp
View File

@ -47,6 +47,21 @@ namespace storm {
return variableInformation.getTotalBitOffset(true);
}
template<typename ValueType, typename StateType>
storm::storage::sparse::StateValuationsBuilder NextStateGenerator<ValueType, StateType>::initializeStateValuationsBuilder() const {
storm::storage::sparse::StateValuationsBuilder result;
for (auto const& v : variableInformation.locationVariables) {
result.addVariable(v.variable);
}
for (auto const& v : variableInformation.booleanVariables) {
result.addVariable(v.variable);
}
for (auto const& v : variableInformation.integerVariables) {
result.addVariable(v.variable);
}
return result;
}
template<typename ValueType, typename StateType>
void NextStateGenerator<ValueType, StateType>::load(CompressedState const& state) {
// Since almost all subsequent operations are based on the evaluator, we load the state into it now.
@ -64,6 +79,16 @@ namespace storm {
return evaluator->asBool(expression);
}
template<typename ValueType, typename StateType>
void NextStateGenerator<ValueType, StateType>::addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const {
std::vector<bool> booleanValues;
booleanValues.reserve(variableInformation.booleanVariables.size());
std::vector<int64_t> integerValues;
integerValues.reserve(variableInformation.locationVariables.size() + variableInformation.integerVariables.size());
extractVariableValues(*this->state, variableInformation, integerValues, booleanValues, integerValues);
valuationsBuilder.addState(currentStateIndex, std::move(booleanValues), std::move(integerValues));
}
template<typename ValueType, typename StateType>
storm::models::sparse::StateLabeling NextStateGenerator<ValueType, StateType>::label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions) {
@ -168,8 +193,8 @@ namespace storm {
}
template<typename ValueType, typename StateType>
storm::expressions::SimpleValuation NextStateGenerator<ValueType, StateType>::toValuation(CompressedState const& state) const {
return unpackStateIntoValuation(state, variableInformation, *expressionManager);
std::string NextStateGenerator<ValueType, StateType>::stateToString(CompressedState const& state) const {
return toString(state, variableInformation);
}
template<typename ValueType, typename StateType>

9
src/storm/generator/NextStateGenerator.h
View File

@ -10,6 +10,7 @@
#include "storm/storage/sparse/StateStorage.h"
#include "storm/storage/expressions/ExpressionEvaluator.h"
#include "storm/storage/sparse/ChoiceOrigins.h"
#include "storm/storage/sparse/StateValuations.h"
#include "storm/builder/BuilderOptions.h"
#include "storm/builder/RewardModelInformation.h"
@ -54,14 +55,20 @@ namespace storm {
virtual bool isPartiallyObservable() const = 0;
virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) = 0;
/// Initializes a builder for state valuations by adding the appropriate variables.
virtual storm::storage::sparse::StateValuationsBuilder initializeStateValuationsBuilder() const;
void load(CompressedState const& state);
virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) = 0;
bool satisfies(storm::expressions::Expression const& expression) const;
/// Adds the valuation for the currently loaded state to the given builder
virtual void addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const;
virtual std::size_t getNumberOfRewardModels() const = 0;
virtual storm::builder::RewardModelInformation getRewardModelInformation(uint64_t const& index) const = 0;
storm::expressions::SimpleValuation toValuation(CompressedState const& state) const;
std::string stateToString(CompressedState const& state) const;
uint32_t observabilityClass(CompressedState const& state) const;

2
src/storm/storage/Scheduler.cpp
View File

@ -241,7 +241,7 @@ namespace storm {
}
storm::json<storm::RationalNumber> stateChoicesJson;
if (model && model->hasStateValuations()) {
stateChoicesJson["s"] = model->getStateValuations().getStateValuation(state).toJson();
stateChoicesJson["s"] = model->getStateValuations()[state].toJson(model->getStateValuations());
} else {
stateChoicesJson["s"] = state;
}

217
src/storm/storage/sparse/StateValuations.cpp
View File

@ -1,24 +1,184 @@
#include "storm/storage/sparse/StateValuations.h"
#include "storm/storage/BitVector.h"
#include "storm/utility/vector.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidTypeException.h"
namespace storm {
namespace storage {
namespace sparse {
StateValuations::StateValuations(std::vector<storm::expressions::SimpleValuation> const& valuations) : valuations(valuations) {
// Intentionally left empty.
StateValuation::StateValuation(std::vector<bool>&& booleanValues, std::vector<int64_t>&& integerValues, std::vector<storm::RationalNumber>&& rationalValues) : booleanValues(std::move(booleanValues)), integerValues(std::move(integerValues)), rationalValues(std::move(rationalValues)) {
// Intentionally left empty
}
StateValuations::StateValuations(std::vector<storm::expressions::SimpleValuation>&& valuations) : valuations(std::move(valuations)) {
// Intentionally left empty.
bool StateValuation::getBooleanValue(StateValuations const& valuations, storm::expressions::Variable const& booleanVariable) const {
STORM_LOG_ASSERT(assertValuations(valuations), "Invalid state valuations");
STORM_LOG_ASSERT(valuations.variableToIndexMap.count(booleanVariable) > 0, "Variable " << booleanVariable.getName() << " is not part of this valuation.");
return booleanValues[valuations.variableToIndexMap.at(booleanVariable)];
}
int64_t const& StateValuation::getIntegerValue(StateValuations const& valuations, storm::expressions::Variable const& integerVariable) const {
STORM_LOG_ASSERT(assertValuations(valuations), "Invalid state valuations");
STORM_LOG_ASSERT(valuations.variableToIndexMap.count(integerVariable) > 0, "Variable " << integerVariable.getName() << " is not part of this valuation.");
return integerValues[valuations.variableToIndexMap.at(integerVariable)];
}
storm::RationalNumber const& StateValuation::getRationalValue(StateValuations const& valuations, storm::expressions::Variable const& rationalVariable) const {
STORM_LOG_ASSERT(assertValuations(valuations), "Invalid state valuations");
STORM_LOG_ASSERT(valuations.variableToIndexMap.count(rationalVariable) > 0, "Variable " << rationalVariable.getName() << " is not part of this valuation.");
return rationalValues[valuations.variableToIndexMap.at(rationalVariable)];
}
bool StateValuation::isEmpty() const {
return booleanValues.empty() && integerValues.empty() && rationalValues.empty();
}
std::string StateValuation::toString(StateValuations const& valuations, bool pretty, boost::optional<std::set<storm::expressions::Variable>> const& selectedVariables) const {
STORM_LOG_ASSERT(assertValuations(valuations), "Invalid state valuations");
typename std::map<storm::expressions::Variable, uint64_t>::const_iterator mapIt = valuations.variableToIndexMap.begin();
typename std::set<storm::expressions::Variable>::const_iterator setIt;
if (selectedVariables) {
setIt = selectedVariables->begin();
}
std::vector<std::string> assignments;
while (mapIt != valuations.variableToIndexMap.end() && (!selectedVariables || setIt != selectedVariables->end())) {
// Move Map iterator to next relevant position
if (selectedVariables) {
while (mapIt->first != *setIt) {
++mapIt;
STORM_LOG_ASSERT(mapIt != valuations.variableToIndexMap.end(), "Valuation does not consider selected variable " << setIt->getName() << ".");
}
}
auto const& variable = mapIt->first;
std::stringstream stream;
if (pretty) {
if (variable.hasBooleanType() && !booleanValues[mapIt->second]) {
stream << "!";
}
stream << variable.getName();
if (variable.hasIntegerType()) {
stream << "=" << integerValues[mapIt->second];
} else if (variable.hasRationalType()) {
stream << "=" << rationalValues[mapIt->second];
} else {
STORM_LOG_THROW(variable.hasBooleanType(), storm::exceptions::InvalidTypeException, "Unexpected variable type.");
}
} else {
if (variable.hasBooleanType()) {
stream << std::boolalpha << booleanValues[mapIt->second] << std::noboolalpha;
} else if (variable.hasIntegerType()) {
stream << integerValues[mapIt->second];
} else if (variable.hasRationalType()) {
stream << rationalValues[mapIt->second];
}
}
assignments.push_back(stream.str());
// Go to next position
if (selectedVariables) {
++setIt;
} else {
++mapIt;
}
}
if (pretty) {
return "[" + boost::join(assignments, "\t& ") + "]";
} else {
return "[" + boost::join(assignments, "\t") + "]";
}
}
typename StateValuation::Json StateValuation::toJson(StateValuations const& valuations, boost::optional<std::set<storm::expressions::Variable>> const& selectedVariables) const {
STORM_LOG_ASSERT(assertValuations(valuations), "Invalid state valuations");
typename std::map<storm::expressions::Variable, uint64_t>::const_iterator mapIt = valuations.variableToIndexMap.begin();
typename std::set<storm::expressions::Variable>::const_iterator setIt;
if (selectedVariables) {
setIt = selectedVariables->begin();
}
Json result;
while (mapIt != valuations.variableToIndexMap.end() && (!selectedVariables || setIt != selectedVariables->end())) {
// Move Map iterator to next relevant position
if (selectedVariables) {
while (mapIt->first != *setIt) {
++mapIt;
STORM_LOG_ASSERT(mapIt != valuations.variableToIndexMap.end(), "Valuation does not consider selected variable " << setIt->getName() << ".");
}
}
auto const& variable = mapIt->first;
if (variable.hasBooleanType()) {
result[variable.getName()] = bool(booleanValues[mapIt->second]);
} else if (variable.hasIntegerType()) {
result[variable.getName()] = integerValues[mapIt->second];
} else if (variable.hasRationalType()) {
result[variable.getName()] = rationalValues[mapIt->second];
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type.");
}
// Go to next position
if (selectedVariables) {
++setIt;
} else {
++mapIt;
}
}
return result;
}
bool StateValuation::assertValuations(StateValuations const& valuations) const {
storm::storage::BitVector foundBooleanValues(booleanValues.size(), false);
storm::storage::BitVector foundIntegerValues(integerValues.size(), false);
storm::storage::BitVector foundRationalValues(rationalValues.size(), false);
for (auto const& varIndex : valuations.variableToIndexMap) {
storm::storage::BitVector* bv;
if (varIndex.first.hasBooleanType()) {
bv = &foundBooleanValues;
} else if (varIndex.first.hasIntegerType()) {
bv = &foundIntegerValues;
} else if (varIndex.first.hasRationalType()) {
bv = &foundRationalValues;
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type.");
}
if (varIndex.second < bv->size()) {
if (bv->get(varIndex.second)) {
STORM_LOG_ERROR("Multiple variables refer to the same value index");
return false;
}
bv->set(varIndex.second, true);
} else {
STORM_LOG_ERROR("Valuation does not provide a value for all variables");
return false;
}
}
if (!(foundBooleanValues.full() && foundIntegerValues.full() && foundRationalValues.full())) {
STORM_LOG_ERROR("Valuation has too many entries.");
}
return true;
}
StateValuations::StateValuations(std::map<storm::expressions::Variable, uint64_t> const& variableToIndexMap, std::vector<StateValuation>&& valuations) : variableToIndexMap(variableToIndexMap), valuations(valuations) {
// Intentionally left empty
}
std::string StateValuations::getStateInfo(state_type const& state) const {
return getStateValuation(state).toString();
STORM_LOG_ASSERT(state < getNumberOfStates(), "Invalid state index.");
return (*this)[state].toString(*this);
}
StateValuation& StateValuations::operator[](storm::storage::sparse::state_type const& state) {
STORM_LOG_ASSERT(state < getNumberOfStates(), "Invalid state index.");
return valuations[state];
}
storm::expressions::SimpleValuation const& StateValuations::getStateValuation(storm::storage::sparse::state_type const& state) const {
StateValuation const& StateValuations::operator[](storm::storage::sparse::state_type const& state) const {
STORM_LOG_ASSERT(state < getNumberOfStates(), "Invalid state index.");
return valuations[state];
}
@ -27,11 +187,11 @@ namespace storm {
}
StateValuations StateValuations::selectStates(storm::storage::BitVector const& selectedStates) const {
return StateValuations(storm::utility::vector::filterVector(valuations, selectedStates));
return StateValuations(variableToIndexMap, storm::utility::vector::filterVector(valuations, selectedStates));
}
StateValuations StateValuations::selectStates(std::vector<storm::storage::sparse::state_type> const& selectedStates) const {
std::vector<storm::expressions::SimpleValuation> selectedValuations;
std::vector<StateValuation> selectedValuations;
selectedValuations.reserve(selectedStates.size());
for (auto const& selectedState : selectedStates){
if (selectedState < valuations.size()) {
@ -40,7 +200,44 @@ namespace storm {
selectedValuations.emplace_back();
}
}
return StateValuations(std::move(selectedValuations));
return StateValuations(variableToIndexMap, std::move(selectedValuations));
}
StateValuationsBuilder::StateValuationsBuilder() : booleanVarCount(0), integerVarCount(0), rationalVarCount(0) {
// Intentionally left empty.
}
void StateValuationsBuilder::addVariable(storm::expressions::Variable const& variable) {
STORM_LOG_ASSERT(currentStateValuations.valuations.empty(), "Tried to add a variable, although a state has already been added before.");
STORM_LOG_ASSERT(currentStateValuations.variableToIndexMap.count(variable) == 0, "Variable " << variable.getName() << " already added.");
if (variable.hasBooleanType()) {
currentStateValuations.variableToIndexMap[variable] = booleanVarCount++;
}
if (variable.hasIntegerType()) {
currentStateValuations.variableToIndexMap[variable] = integerVarCount++;
}
if (variable.hasRationalType()) {
currentStateValuations.variableToIndexMap[variable] = rationalVarCount++;
}
}
void StateValuationsBuilder::addState(storm::storage::sparse::state_type const& state, std::vector<bool>&& booleanValues, std::vector<int64_t>&& integerValues, std::vector<storm::RationalNumber>&& rationalValues) {
if (state > currentStateValuations.valuations.size()) {
currentStateValuations.valuations.resize(state);
}
if (state == currentStateValuations.valuations.size()) {
currentStateValuations.valuations.emplace_back(std::move(booleanValues), std::move(integerValues), std::move(rationalValues));
} else {
STORM_LOG_ASSERT(currentStateValuations[state].isEmpty(), "Adding a valuation to the same state multiple times.");
currentStateValuations[state] = StateValuation(std::move(booleanValues), std::move(integerValues), std::move(rationalValues));
}
}
StateValuations StateValuationsBuilder::build(std::size_t totalStateCount) {
return std::move(currentStateValuations);
booleanVarCount = 0;
integerVarCount = 0;
rationalVarCount = 0;
}
}
}

99
src/storm/storage/sparse/StateValuations.h
View File

@ -1,35 +1,77 @@
#ifndef STORM_STORAGE_SPARSE_STATEVALUATIONS_H_
#define STORM_STORAGE_SPARSE_STATEVALUATIONS_H_
#pragma once
#include <cstdint>
#include <string>
#include "storm/storage/sparse/StateType.h"
#include "storm/storage/BitVector.h"
#include "storm/storage/expressions/SimpleValuation.h"
#include "storm/storage/expressions/Variable.h"
#include "storm/models/sparse/StateAnnotation.h"
#include "storm/adapters/JsonAdapter.h"
namespace storm {
namespace storage {
namespace sparse {
// A structure holding information about the reachable state space that can be retrieved from the outside.
class StateValuations : public storm::models::sparse::StateAnnotation {
class StateValuations;
class StateValuationsBuilder;
class StateValuation {
public:
typedef storm::json<storm::RationalNumber> Json;
StateValuation() = default;
StateValuation(std::vector<bool>&& booleanValues, std::vector<int64_t>&& integerValues, std::vector<storm::RationalNumber>&& rationalValues);
bool getBooleanValue(StateValuations const& valuations, storm::expressions::Variable const& booleanVariable) const;
int64_t const& getIntegerValue(StateValuations const& valuations, storm::expressions::Variable const& integerVariable) const;
storm::RationalNumber const& getRationalValue(StateValuations const& valuations, storm::expressions::Variable const& rationalVariable) const;
// Returns true, if this valuation does not contain any value.
bool isEmpty() const;
/*!
* Constructs a state information object for the given number of states.
* Returns a string representation of the valuation.
*
* @param selectedVariables If given, only the informations for the variables in this set are processed.
* @return The string representation.
*/
StateValuations(std::vector<storm::expressions::SimpleValuation> const& valuations);
StateValuations(std::vector<storm::expressions::SimpleValuation>&& valuations);
std::string toString(StateValuations const& valuations, bool pretty = true, boost::optional<std::set<storm::expressions::Variable>> const& selectedVariables = boost::none) const;
virtual ~StateValuations() = default;
/*!
* Returns a JSON representation of this valuation
* @param selectedVariables If given, only the informations for the variables in this set are processed.
* @return
*/
Json toJson(StateValuations const& valuations, boost::optional<std::set<storm::expressions::Variable>> const& selectedVariables = boost::none) const;
private:
// Asserts whether the variable and value counts for each type match.
bool assertValuations(StateValuations const& valuations) const;
std::vector<bool> booleanValues;
std::vector<int64_t> integerValues;
std::vector<storm::RationalNumber> rationalValues;
};
// A structure holding information about the reachable state space that can be retrieved from the outside.
class StateValuations : public storm::models::sparse::StateAnnotation {
public:
friend class StateValuation;
friend class StateValuationsBuilder;
StateValuations() = default;
virtual ~StateValuations() = default;
virtual std::string getStateInfo(storm::storage::sparse::state_type const& state) const override;
storm::expressions::SimpleValuation const& getStateValuation(storm::storage::sparse::state_type const& state) const;
/*!
* Returns the valuation at the specific state
*/
StateValuation& operator[](storm::storage::sparse::state_type const& state);
StateValuation const& operator[](storm::storage::sparse::state_type const& state) const;
// Returns the number of states that this object describes.
// Returns the (current) number of states that this object describes.
uint_fast64_t getNumberOfStates() const;
/*
@ -45,14 +87,41 @@ namespace storm {
private:
StateValuations(std::map<storm::expressions::Variable, uint64_t> const& variableToIndexMap, std::vector<StateValuation>&& valuations);
std::map<storm::expressions::Variable, uint64_t> variableToIndexMap;
// A mapping from state indices to their variable valuations.
std::vector<storm::expressions::SimpleValuation> valuations;
std::vector<StateValuation> valuations;
};
class StateValuationsBuilder {
public:
StateValuationsBuilder();
/*! Adds a new variable to keep track of for the state valuations.
*! All variables need to be added before adding new states.
*/
void addVariable(storm::expressions::Variable const& variable);
/*!
* Adds a new state.
* The variable values have to be given in the same order as the variables have been added.
* The number of given variable values for each type needs to match the number of added variables.
* After calling this method, no more variables should be added.
*/
void addState(storm::storage::sparse::state_type const& state, std::vector<bool>&& booleanValues = {}, std::vector<int64_t>&& integerValues = {}, std::vector<storm::RationalNumber>&& rationalValues = {});
/*!
* Creates the finalized state valuations object.
*/
StateValuations build(std::size_t totalStateCount);
private:
StateValuations currentStateValuations;
uint64_t booleanVarCount;
uint64_t integerVarCount;
uint64_t rationalVarCount;
};
}
}
}
#endif /* STORM_STORAGE_SPARSE_STATEVALUATIONS_H_ */
Write Preview
Loading…
Cancel
Save