Browse Source

Merge branch 'master' into almostsurepomdp

tempestpy_adaptions
Sebastian Junges 5 years ago
parent
commit
1a2a4c1a8e
  1. 5
      CHANGELOG.md
  2. 23
      src/storm/builder/ExplicitModelBuilder.cpp
  3. 5
      src/storm/builder/ExplicitModelBuilder.h
  4. 37
      src/storm/generator/CompressedState.cpp
  5. 16
      src/storm/generator/CompressedState.h
  6. 90
      src/storm/generator/JaniNextStateGenerator.cpp
  7. 10
      src/storm/generator/JaniNextStateGenerator.h
  8. 29
      src/storm/generator/NextStateGenerator.cpp
  9. 9
      src/storm/generator/NextStateGenerator.h
  10. 6
      src/storm/generator/TransientVariableInformation.cpp
  11. 6
      src/storm/generator/TransientVariableInformation.h
  12. 2
      src/storm/settings/modules/CoreSettings.cpp
  13. 2
      src/storm/storage/Scheduler.cpp
  14. 220
      src/storm/storage/sparse/StateValuations.cpp
  15. 93
      src/storm/storage/sparse/StateValuations.h

5
CHANGELOG.md

@ -8,10 +8,11 @@ The releases of major and minor versions contain an overview of changes since th
Version 1.5.x
-------------
## Version 1.5.x (Under development)
- Scheduler export: Properly handle models with end components. Added export in .json format.
- Changed default Dd library from `cudd` to `sylvan`. The Dd library can be changed back to `cudd` using the command line switch `--ddlib`.
- Scheduler export: Properly handle models with end components. Added export in `.json` format.
- CMake: Search for Gurobi prefers new versions
- CMake: We no longer ship xerces-c. If xerces-c is not found on the system, storm-gspn will not be able to parse xml-based GSPN formats
- `Eigen' library: The source code of Eigen is no longer included but downloaded from an external repository instead. Incremented Eigen version to 3.3.7 which fixes a compilation issue with recent XCode Versions.
- Eigen library: The source code of Eigen is no longer included but downloaded from an external repository instead. Incremented Eigen version to 3.3.7 which fixes a compilation issue with recent XCode versions.
- Tests: Enabled tests for permissive schedulers
- `storm-counterexamples`: fix when computing multiple counterexamples in debug mode
- `storm-dft`: Renamed setting `--show-dft-stats` to `dft-statistics` and added approximation information to statistics.

23
src/storm/builder/ExplicitModelBuilder.cpp

@ -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

@ -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.

37
src/storm/generator/CompressedState.cpp

@ -1,5 +1,7 @@
#include "storm/generator/CompressedState.h"
#include <boost/algorithm/string/join.hpp>
#include "storm/generator/VariableInformation.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/storage/expressions/SimpleValuation.h"
@ -43,6 +45,41 @@ namespace storm {
return result;
}
void extractVariableValues(CompressedState const& state, VariableInformation const& variableInformation, std::vector<int64_t>& locationValues, std::vector<bool>& booleanValues, std::vector<int64_t>& integerValues) {
for (auto const& locationVariable : variableInformation.locationVariables) {
if (locationVariable.bitWidth != 0) {
locationValues.push_back(state.getAsInt(locationVariable.bitOffset, locationVariable.bitWidth));
} else {
locationValues.push_back(0);
}
}
for (auto const& booleanVariable : variableInformation.booleanVariables) {
booleanValues.push_back(state.get(booleanVariable.bitOffset));
}
for (auto const& integerVariable : variableInformation.integerVariables) {
integerValues.push_back(state.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound);
}
}
std::string toString(CompressedState const& state, VariableInformation const& variableInformation) {
std::vector<std::string> assignments;
for (auto const& locationVariable : variableInformation.locationVariables) {
assignments.push_back(locationVariable.variable.getName() + "=");
assignments.back() += std::to_string(locationVariable.bitWidth == 0 ? 0 : state.getAsInt(locationVariable.bitOffset, locationVariable.bitWidth));
}
for (auto const& booleanVariable : variableInformation.booleanVariables) {
if (!state.get(booleanVariable.bitOffset)) {
assignments.push_back("!" + booleanVariable.variable.getName());
} else {
assignments.push_back(booleanVariable.variable.getName());
}
}
for (auto const& integerVariable : variableInformation.integerVariables) {
assignments.push_back(integerVariable.variable.getName() + "=" + std::to_string(state.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound));
}
return boost::join(assignments, " & ");
}
storm::storage::BitVector computeObservabilityMask(VariableInformation const& variableInformation) {
storm::storage::BitVector result(variableInformation.getTotalBitOffset(true));
for (auto const& locationVariable : variableInformation.locationVariables) {

16
src/storm/generator/CompressedState.h

@ -37,6 +37,22 @@ namespace storm {
*/
storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager);
/*!
* Appends the values of the given variables in the given state to the corresponding result vectors.
* locationValues are inserted before integerValues (relevant if both, locationValues and integerValues actually refer to the same vector)
* @param state The state
* @param variableInformation The variables
* @param locationValues
* @param booleanValues
* @param integerValues
*/
void extractVariableValues(CompressedState const& state, VariableInformation const& variableInformation, std::vector<int64_t>& locationValues, std::vector<bool>& booleanValues, std::vector<int64_t>& integerValues);
/*!
* Returns a (human readable) string representation of the variable valuation encoded by the given state
*/
std::string toString(CompressedState const& state, VariableInformation const& variableInformation);
/*!
*
* @param variableInformation

90
src/storm/generator/JaniNextStateGenerator.cpp

@ -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

@ -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

@ -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

@ -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;

6
src/storm/generator/TransientVariableInformation.cpp

@ -97,21 +97,21 @@ namespace storm {
}
template <typename ValueType>
TransientVariableData<bool> const& TransientVariableInformation<ValueType>::getBooleanArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t arrayIndex) {
TransientVariableData<bool> const& TransientVariableInformation<ValueType>::getBooleanArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t arrayIndex) const {
std::vector<uint64_t> const& indices = arrayVariableToElementInformations.at(arrayVariable);
STORM_LOG_THROW(arrayIndex < indices.size(), storm::exceptions::WrongFormatException, "Array access at array " << arrayVariable.getName() << " evaluates to array index " << arrayIndex << " which is out of bounds as the array size is " << indices.size() << ".");
return booleanVariableInformation[indices[arrayIndex]];
}
template <typename ValueType>
TransientVariableData<int64_t> const& TransientVariableInformation<ValueType>::getIntegerArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t arrayIndex) {
TransientVariableData<int64_t> const& TransientVariableInformation<ValueType>::getIntegerArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t arrayIndex) const {
std::vector<uint64_t> const& indices = arrayVariableToElementInformations.at(arrayVariable);
STORM_LOG_THROW(arrayIndex < indices.size(), storm::exceptions::WrongFormatException, "Array access at array " << arrayVariable.getName() << " evaluates to array index " << arrayIndex << " which is out of bounds as the array size is " << indices.size() << ".");
return integerVariableInformation[indices[arrayIndex]];
}
template <typename ValueType>
TransientVariableData<ValueType> const& TransientVariableInformation<ValueType>::getRationalArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t arrayIndex) {
TransientVariableData<ValueType> const& TransientVariableInformation<ValueType>::getRationalArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t arrayIndex) const {
std::vector<uint64_t> const& indices = arrayVariableToElementInformations.at(arrayVariable);
STORM_LOG_THROW(arrayIndex < indices.size(), storm::exceptions::WrongFormatException, "Array access at array " << arrayVariable.getName() << " evaluates to array index " << arrayIndex << " which is out of bounds as the array size is " << indices.size() << ".");
return rationalVariableInformation[indices[arrayIndex]];

6
src/storm/generator/TransientVariableInformation.h

@ -93,9 +93,9 @@ namespace storm {
TransientVariableInformation() = default;
void registerArrayVariableReplacements(storm::jani::ArrayEliminatorData const& arrayEliminatorData);
TransientVariableData<bool> const& getBooleanArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t index);
TransientVariableData<int64_t> const& getIntegerArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t index);
TransientVariableData<ValueType> const& getRationalArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t index);
TransientVariableData<bool> const& getBooleanArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t index) const;
TransientVariableData<int64_t> const& getIntegerArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t index) const;
TransientVariableData<ValueType> const& getRationalArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t index) const;
void setDefaultValuesInEvaluator(storm::expressions::ExpressionEvaluator<ValueType>& evaluator) const;

2
src/storm/settings/modules/CoreSettings.cpp

@ -46,7 +46,7 @@ namespace storm {
std::vector<std::string> ddLibraries = {"cudd", "sylvan"};
this->addOption(storm::settings::OptionBuilder(moduleName, ddLibraryOptionName, false, "Sets which library is preferred for decision-diagram operations.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the library to prefer.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(ddLibraries)).setDefaultValueString("cudd").build()).build());
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the library to prefer.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(ddLibraries)).setDefaultValueString("sylvan").build()).build());
std::vector<std::string> lpSolvers = {"gurobi", "glpk", "z3"};
this->addOption(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "Sets which LP solver is preferred.")

2
src/storm/storage/Scheduler.cpp

@ -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().toJson(state);
} else {
stateChoicesJson["s"] = state;
}

220
src/storm/storage/sparse/StateValuations.cpp

@ -1,37 +1,194 @@
#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.
StateValuations::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.
typename StateValuations::StateValuation const& StateValuations::getValuation(storm::storage::sparse::state_type const& stateIndex) const {
STORM_LOG_ASSERT(stateIndex < valuations.size(), "Invalid state index.");
STORM_LOG_ASSERT(assertValuation(valuations[stateIndex]), "Invalid state valuations");
return valuations[stateIndex];
}
std::string StateValuations::getStateInfo(state_type const& state) const {
return getStateValuation(state).toString();
bool StateValuations::getBooleanValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& booleanVariable) const {
auto const& valuation = getValuation(stateIndex);
STORM_LOG_ASSERT(variableToIndexMap.count(booleanVariable) > 0, "Variable " << booleanVariable.getName() << " is not part of this valuation.");
return valuation.booleanValues[variableToIndexMap.at(booleanVariable)];
}
storm::expressions::SimpleValuation const& StateValuations::getStateValuation(storm::storage::sparse::state_type const& state) const {
return valuations[state];
int64_t const& StateValuations::getIntegerValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& integerVariable) const {
auto const& valuation = getValuation(stateIndex);
STORM_LOG_ASSERT(variableToIndexMap.count(integerVariable) > 0, "Variable " << integerVariable.getName() << " is not part of this valuation.");
return valuation.integerValues[variableToIndexMap.at(integerVariable)];
}
storm::RationalNumber const& StateValuations::getRationalValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& rationalVariable) const {
auto const& valuation = getValuation(stateIndex);
STORM_LOG_ASSERT(variableToIndexMap.count(rationalVariable) > 0, "Variable " << rationalVariable.getName() << " is not part of this valuation.");
return valuation.rationalValues[variableToIndexMap.at(rationalVariable)];
}
bool StateValuations::isEmpty(storm::storage::sparse::state_type const& stateIndex) const {
auto const& valuation = getValuation(stateIndex);
return valuation.booleanValues.empty() && valuation.integerValues.empty() && valuation.rationalValues.empty();
}
std::string StateValuations::toString(storm::storage::sparse::state_type const& stateIndex, bool pretty, boost::optional<std::set<storm::expressions::Variable>> const& selectedVariables) const {
auto const& valuation = getValuation(stateIndex);
typename std::map<storm::expressions::Variable, uint64_t>::const_iterator mapIt = variableToIndexMap.begin();
typename std::set<storm::expressions::Variable>::const_iterator setIt;
if (selectedVariables) {
setIt = selectedVariables->begin();
}
std::vector<std::string> 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() << ".");
}
}
auto const& variable = mapIt->first;
std::stringstream stream;
if (pretty) {
if (variable.hasBooleanType() && !valuation.booleanValues[mapIt->second]) {
stream << "!";
}
stream << variable.getName();
if (variable.hasIntegerType()) {
stream << "=" << valuation.integerValues[mapIt->second];
} else if (variable.hasRationalType()) {
stream << "=" << valuation.rationalValues[mapIt->second];
} else {
STORM_LOG_THROW(variable.hasBooleanType(), 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];
}
}
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 StateValuations::Json StateValuations::toJson(storm::storage::sparse::state_type const& stateIndex, boost::optional<std::set<storm::expressions::Variable>> const& selectedVariables) const {
auto const& valuation = getValuation(stateIndex);
typename std::map<storm::expressions::Variable, uint64_t>::const_iterator mapIt = variableToIndexMap.begin();
typename std::set<storm::expressions::Variable>::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() << ".");
}
}
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];
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unexpected variable type.");
}
// Go to next position
if (selectedVariables) {
++setIt;
} else {
++mapIt;
}
}
return result;
}
bool StateValuations::assertValuation(StateValuation const& valuation) const {
storm::storage::BitVector foundBooleanValues(valuation.booleanValues.size(), false);
storm::storage::BitVector foundIntegerValues(valuation.integerValues.size(), false);
storm::storage::BitVector foundRationalValues(valuation.rationalValues.size(), false);
for (auto const& varIndex : 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 {
STORM_LOG_ASSERT(state < getNumberOfStates(), "Invalid state index.");
return this->toString(state);
}
uint_fast64_t StateValuations::getNumberOfStates() const {
return valuations.size();
}
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 +197,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.isEmpty(state), "Adding a valuation to the same state multiple times.");
currentStateValuations.valuations[state] = typename StateValuations::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;
}
}
}

93
src/storm/storage/sparse/StateValuations.h

@ -1,35 +1,68 @@
#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 {
class StateValuationsBuilder;
// A structure holding information about the reachable state space that can be retrieved from the outside.
class StateValuations : public storm::models::sparse::StateAnnotation {
public:
/*!
* Constructs a state information object for the given number of states.
*/
StateValuations(std::vector<storm::expressions::SimpleValuation> const& valuations);
StateValuations(std::vector<storm::expressions::SimpleValuation>&& valuations);
friend class StateValuationsBuilder;
typedef storm::json<storm::RationalNumber> Json;
class StateValuation {
public:
friend class StateValuations;
StateValuation() = default;
StateValuation(std::vector<bool>&& booleanValues, std::vector<int64_t>&& integerValues, std::vector<storm::RationalNumber>&& rationalValues);
private:
std::vector<bool> booleanValues;
std::vector<int64_t> integerValues;
std::vector<storm::RationalNumber> rationalValues;
};
virtual ~StateValuations() = default;
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;
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;
storm::RationalNumber const& getRationalValue(storm::storage::sparse::state_type const& stateIndex, storm::expressions::Variable const& rationalVariable) const;
/// Returns true, if this valuation does not contain any value.
bool isEmpty(storm::storage::sparse::state_type const& stateIndex) const;
/*!
* 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.
*/
std::string toString(storm::storage::sparse::state_type const& stateIndex, bool pretty = true, boost::optional<std::set<storm::expressions::Variable>> const& selectedVariables = boost::none) const;
// Returns the number of states that this object describes.
/*!
* 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(storm::storage::sparse::state_type const& stateIndex, boost::optional<std::set<storm::expressions::Variable>> const& selectedVariables = boost::none) const;
// Returns the (current) number of states that this object describes.
uint_fast64_t getNumberOfStates() const;
/*
@ -45,14 +78,44 @@ namespace storm {
private:
StateValuations(std::map<storm::expressions::Variable, uint64_t> const& variableToIndexMap, std::vector<StateValuation>&& valuations);
bool assertValuation(StateValuation const& valuation) const;
StateValuation const& getValuation(storm::storage::sparse::state_type const& stateIndex) const;
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_ */
Loading…
Cancel
Save