From 923f779a09ff01db8ef5b6aa4986bfbc91817b05 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Mon, 17 Aug 2020 21:09:38 -0700
Subject: [PATCH] explicit-state-lookup, for finding states in a model based on
the variable assignment
---
src/storm/api/builder.h | 33 ++++++++++++++++------
src/storm/builder/ExplicitModelBuilder.cpp | 18 ++++++++++--
src/storm/builder/ExplicitModelBuilder.h | 23 ++++++++++++++-
src/storm/generator/CompressedState.cpp | 30 ++++++++++++++++++++
src/storm/generator/CompressedState.h | 5 ++++
src/storm/generator/NextStateGenerator.cpp | 5 ++++
src/storm/generator/NextStateGenerator.h | 2 +-
src/storm/generator/VariableInformation.h | 6 +++-
src/storm/storage/sparse/StateStorage.h | 6 ++--
9 files changed, 110 insertions(+), 18 deletions(-)
diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h
index 0760ae9f1..fbe838c5d 100644
--- a/src/storm/api/builder.h
+++ b/src/storm/api/builder.h
@@ -77,6 +77,26 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "CUDD does not support rational functions.");
}
+ /**
+ * Initializes an explict model builder; an object/algorithm that is used to build sparse models
+ * @tparam ValueType Type of the probabilities in the sparse model
+ * @param model SymbolicModelDescription of the model
+ * @param options Builder options
+ * @return A builder
+ */
+ template<typename ValueType>
+ storm::builder::ExplicitModelBuilder<ValueType> makeExplicitModelBuilder(storm::storage::SymbolicModelDescription const& model, storm::builder::BuilderOptions const& options) {
+ std::shared_ptr<storm::generator::NextStateGenerator<ValueType, uint32_t>> generator;
+ if (model.isPrismProgram()) {
+ generator = std::make_shared<storm::generator::PrismNextStateGenerator<ValueType, uint32_t>>(model.asPrismProgram(), options);
+ } else if (model.isJaniModel()) {
+ generator = std::make_shared<storm::generator::JaniNextStateGenerator<ValueType, uint32_t>>(model.asJaniModel(), options);
+ } else {
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot build sparse model from this symbolic model description.");
+ }
+ return storm::builder::ExplicitModelBuilder<ValueType>(generator);
+ }
+
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::storage::SymbolicModelDescription const& model, storm::builder::BuilderOptions const& options, bool jit = false, bool doctor = false) {
if (jit) {
@@ -92,19 +112,14 @@ namespace storm {
return builder.build();
} else {
- std::shared_ptr<storm::generator::NextStateGenerator<ValueType, uint32_t>> generator;
- if (model.isPrismProgram()) {
- generator = std::make_shared<storm::generator::PrismNextStateGenerator<ValueType, uint32_t>>(model.asPrismProgram(), options);
- } else if (model.isJaniModel()) {
- generator = std::make_shared<storm::generator::JaniNextStateGenerator<ValueType, uint32_t>>(model.asJaniModel(), options);
- } else {
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot build sparse model from this symbolic model description.");
- }
- storm::builder::ExplicitModelBuilder<ValueType> builder(generator);
+ storm::builder::ExplicitModelBuilder<ValueType> builder = makeExplicitModelBuilder<ValueType>(model, options);
return builder.build();
}
}
+
+
+
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool jit = false, bool doctor = false) {
storm::builder::BuilderOptions options(formulas, model);
diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp
index b4be0dd6a..9f5c7d298 100644
--- a/src/storm/builder/ExplicitModelBuilder.cpp
+++ b/src/storm/builder/ExplicitModelBuilder.cpp
@@ -8,6 +8,7 @@
#include "storm/exceptions/AbortException.h"
#include "storm/exceptions/WrongFormatException.h"
+#include "storm/exceptions/IllegalArgumentException.h"
#include "storm/generator/PrismNextStateGenerator.h"
#include "storm/generator/JaniNextStateGenerator.h"
@@ -36,7 +37,14 @@
namespace storm {
namespace builder {
-
+
+ template<typename StateType>
+ StateType ExplicitStateLookup<StateType>::lookup(std::map<storm::expressions::Variable, storm::expressions::Expression> const& stateDescription) const {
+ auto cs = storm::generator::createCompressedState(this->varInfo, stateDescription, true);
+ STORM_LOG_THROW(stateToId.contains(cs), storm::exceptions::IllegalArgumentException, "State unknown.");
+ return this->stateToId.getValue(cs);
+ }
+
template <typename ValueType, typename RewardModelType, typename StateType>
ExplicitModelBuilder<ValueType, RewardModelType, StateType>::Options::Options() : explorationOrder(storm::settings::getModule<storm::settings::modules::BuildSettings>().getExplorationOrder()) {
// Intentionally left empty.
@@ -103,7 +111,12 @@ namespace storm {
return actualIndex;
}
-
+
+ template <typename ValueType, typename RewardModelType, typename StateType>
+ ExplicitStateLookup<StateType> ExplicitModelBuilder<ValueType, RewardModelType, StateType>::exportExplicitStateLookup() const {
+ return ExplicitStateLookup<StateType>(this->generator->getVariableInformation(), this->stateStorage.stateToId);
+ }
+
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, boost::optional<storm::storage::sparse::StateValuationsBuilder>& stateValuationsBuilder) {
@@ -419,6 +432,7 @@ namespace storm {
// Explicitly instantiate the class.
template class ExplicitModelBuilder<double, storm::models::sparse::StandardRewardModel<double>, uint32_t>;
+ template class ExplicitStateLookup<uint32_t>;
#ifdef STORM_HAVE_CARL
template class ExplicitModelBuilder<RationalNumber, storm::models::sparse::StandardRewardModel<RationalNumber>, uint32_t>;
diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h
index 4a94ad724..132345075 100644
--- a/src/storm/builder/ExplicitModelBuilder.h
+++ b/src/storm/builder/ExplicitModelBuilder.h
@@ -44,6 +44,21 @@ namespace storm {
// Forward-declare classes.
template <typename ValueType> class RewardModelBuilder;
class ChoiceInformationBuilder;
+
+ template<typename StateType>
+ class ExplicitStateLookup {
+ public:
+ ExplicitStateLookup(VariableInformation const& varInfo,
+ storm::storage::BitVectorHashMap<StateType> const& stateToId ) : varInfo(varInfo), stateToId(stateToId) {
+ // intentionally left empty.
+ }
+
+ StateType lookup(std::map<storm::expressions::Variable, storm::expressions::Expression> const& stateDescription) const;
+
+ private:
+ VariableInformation varInfo;
+ storm::storage::BitVectorHashMap<StateType> stateToId;
+ };
template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>
class ExplicitModelBuilder {
@@ -88,7 +103,13 @@ namespace storm {
* information (if requested).
*/
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> build();
-
+
+ /*!
+ * Export a wrapper that contains (a copy of) the internal information that maps states to ids.
+ * This wrapper can be helpful to find states in later stages.
+ * @return
+ */
+ ExplicitStateLookup<StateType> exportExplicitStateLookup() const;
private:
/*!
* Retrieves the state id of the given state. If the state has not been encountered yet, it will be added to
diff --git a/src/storm/generator/CompressedState.cpp b/src/storm/generator/CompressedState.cpp
index 546b8e4bc..8fddc848e 100644
--- a/src/storm/generator/CompressedState.cpp
+++ b/src/storm/generator/CompressedState.cpp
@@ -2,6 +2,9 @@
#include <boost/algorithm/string/join.hpp>
+#include "storm/exceptions/InvalidArgumentException.h"
+#include "storm/exceptions/NotImplementedException.h"
+
#include "storm/generator/VariableInformation.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/storage/expressions/SimpleValuation.h"
@@ -134,6 +137,33 @@ namespace storm {
return result;
}
+ CompressedState createCompressedState(VariableInformation const& varInfo, std::map<storm::expressions::Variable, storm::expressions::Expression> const& stateDescription, bool checkOutOfBounds) {
+ CompressedState result(varInfo.getTotalBitOffset(true));
+ auto boolItEnd = varInfo.booleanVariables.end();
+
+ for (auto boolIt = varInfo.booleanVariables.begin(); boolIt != boolItEnd; ++boolIt) {
+ STORM_LOG_THROW(stateDescription.count(boolIt->variable) > 0,storm::exceptions::InvalidArgumentException, "Assignment for Boolean variable " << boolIt->getName() << " missing." );
+ result.set(boolIt->bitOffset, stateDescription.at(boolIt->variable).evaluateAsBool());
+ }
+
+ // Iterate over all integer assignments and carry them out.
+ auto integerItEnd = varInfo.integerVariables.end();
+ for (auto integerIt = varInfo.integerVariables.begin(); integerIt != integerItEnd; ++integerIt) {
+ STORM_LOG_THROW(stateDescription.count(integerIt->variable) > 0,storm::exceptions::InvalidArgumentException, "Assignment for Integer variable " << integerIt->getName() << " missing." );
+
+ int64_t assignedValue = stateDescription.at(integerIt->variable).evaluateAsInt();
+ if (checkOutOfBounds) {
+ STORM_LOG_THROW(assignedValue >= integerIt->lowerBound, storm::exceptions::InvalidArgumentException, "The assignment leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << integerIt->getName() << "'.");
+ STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::InvalidArgumentException, "The assignment leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << integerIt->getName() << "'.");
+ }
+ result.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
+ STORM_LOG_ASSERT(static_cast<int_fast64_t>(result.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << result.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ").");
+ }
+
+ STORM_LOG_THROW(varInfo.locationVariables.size() == 0, storm::exceptions::NotImplementedException, "Support for JANI is not implemented");
+ return result;
+ }
+
#ifdef STORM_HAVE_CARL
template void unpackStateIntoEvaluator<storm::RationalNumber>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<storm::RationalNumber>& evaluator);
template void unpackStateIntoEvaluator<storm::RationalFunction>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<storm::RationalFunction>& evaluator);
diff --git a/src/storm/generator/CompressedState.h b/src/storm/generator/CompressedState.h
index 8768929ee..7a6446ecb 100644
--- a/src/storm/generator/CompressedState.h
+++ b/src/storm/generator/CompressedState.h
@@ -2,6 +2,7 @@
#define STORM_GENERATOR_COMPRESSEDSTATE_H_
#include "storm/storage/BitVector.h"
+#include <map>
#include <unordered_map>
namespace storm {
@@ -10,12 +11,15 @@ namespace storm {
class ExpressionManager;
class SimpleValuation;
+ class Variable;
+ class Expression;
}
namespace generator {
typedef storm::storage::BitVector CompressedState;
struct VariableInformation;
+
/*!
* Unpacks the compressed state into the evaluator.
@@ -75,6 +79,7 @@ namespace storm {
*/
CompressedState createOutOfBoundsState(VariableInformation const& varInfo, bool roundTo64Bit = true);
+ CompressedState createCompressedState(VariableInformation const& varInfo, std::map<storm::expressions::Variable, storm::expressions::Expression> const& stateDescription, bool checkOutOfBounds);
}
}
diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp
index e83c9338d..eb681382b 100644
--- a/src/storm/generator/NextStateGenerator.cpp
+++ b/src/storm/generator/NextStateGenerator.cpp
@@ -78,6 +78,11 @@ namespace storm {
}
return evaluator->asBool(expression);
}
+
+ template<typename ValueType, typename StateType>
+ VariableInformation const& NextStateGenerator<ValueType, StateType>::getVariableInformation() const {
+ return variableInformation;
+ }
template<typename ValueType, typename StateType>
void NextStateGenerator<ValueType, StateType>::addStateValuation(storm::storage::sparse::state_type const& currentStateIndex, storm::storage::sparse::StateValuationsBuilder& valuationsBuilder) const {
diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h
index c329f34d6..b782ad908 100644
--- a/src/storm/generator/NextStateGenerator.h
+++ b/src/storm/generator/NextStateGenerator.h
@@ -76,8 +76,8 @@ namespace storm {
NextStateGeneratorOptions const& getOptions() const;
+ VariableInformation const& getVariableInformation() const;
-
virtual std::shared_ptr<storm::storage::sparse::ChoiceOrigins> generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const;
/*!
diff --git a/src/storm/generator/VariableInformation.h b/src/storm/generator/VariableInformation.h
index ffa02f5ac..b7be52200 100644
--- a/src/storm/generator/VariableInformation.h
+++ b/src/storm/generator/VariableInformation.h
@@ -24,7 +24,9 @@ namespace storm {
// A structure storing information about the boolean variables of the model.
struct BooleanVariableInformation {
BooleanVariableInformation(storm::expressions::Variable const& variable, uint_fast64_t bitOffset, bool global, bool observable);
-
+
+ std::string const& getName() const { return variable.getName(); }
+
// The boolean variable.
storm::expressions::Variable variable;
@@ -43,6 +45,8 @@ namespace storm {
IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth, bool global = false, bool observable = true, bool forceOutOfBoundsCheck = false);
+ std::string const& getName() const { return variable.getName(); }
+
// The integer variable.
storm::expressions::Variable variable;
diff --git a/src/storm/storage/sparse/StateStorage.h b/src/storm/storage/sparse/StateStorage.h
index 65b592cb5..8c637c5d4 100644
--- a/src/storm/storage/sparse/StateStorage.h
+++ b/src/storm/storage/sparse/StateStorage.h
@@ -1,5 +1,4 @@
-#ifndef STORM_STORAGE_SPARSE_STATESTORAGE_H_
-#define STORM_STORAGE_SPARSE_STATESTORAGE_H_
+#pragma once
#include <cstdint>
@@ -28,11 +27,10 @@ namespace storm {
uint64_t bitsPerState;
// Get the number of states that were found in the exploration so far.
- uint_fast64_t getNumberOfStates() const;
+ uint64_t getNumberOfStates() const;
};
}
}
}
-#endif /* STORM_STORAGE_SPARSE_STATESTORAGE_H_ */