From 6d6e142236ea5c4fce26802ad2cace392ee3e50a Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 20 Nov 2020 12:25:29 +0100 Subject: [PATCH] Fixed an issue with JANI models concerning properties using transient variable expressions. --- CHANGELOG.md | 3 ++ .../generator/JaniNextStateGenerator.cpp | 30 +++++++++---------- src/storm/generator/JaniNextStateGenerator.h | 17 ++++++++++- src/storm/generator/NextStateGenerator.cpp | 7 +++++ src/storm/generator/NextStateGenerator.h | 9 ++++++ 5 files changed, 49 insertions(+), 17 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 42c9feec6..c9481759d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -13,6 +13,9 @@ Version 1.6.x - Added support for generating optimal schedulers for globally formulae - Simulator supports exact arithmetic - Added switch `--no-simplify` to disable simplification of PRISM programs (which sometimes costs a bit of time on extremely large inputs) +- Fixed issues with JANI inputs concerning + - transient variable expressions in properties and + - integer variables with either only an upper or only a lower bound. - `storm-pomdp`: States can be labelled with values for observable predicates - `storm-pomdp`: (Only API) Track state estimates - `storm-pomdp`: (Only API) Reduce computation of state estimates to computation on unrolled MDP diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 8592cd834..df9530494 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -457,7 +457,7 @@ namespace storm { } template - TransientVariableValuation JaniNextStateGenerator::getTransientVariableValuationAtLocations(std::vector const& locations) const { + TransientVariableValuation JaniNextStateGenerator::getTransientVariableValuationAtLocations(std::vector const& locations, storm::expressions::ExpressionEvaluator const& evaluator) const { uint64_t automatonIndex = 0; TransientVariableValuation transientVariableValuation; for (auto const& automatonRef : this->parallelAutomata) { @@ -465,12 +465,19 @@ namespace storm { uint64_t currentLocationIndex = locations[automatonIndex]; storm::jani::Location const& location = automaton.getLocation(currentLocationIndex); STORM_LOG_ASSERT(!location.getAssignments().hasMultipleLevels(true), "Indexed assignments at locations are not supported in the jani standard."); - applyTransientUpdate(transientVariableValuation, location.getAssignments().getTransientAssignments(), *this->evaluator); + applyTransientUpdate(transientVariableValuation, location.getAssignments().getTransientAssignments(), evaluator); ++automatonIndex; } return transientVariableValuation; } + template + void JaniNextStateGenerator::unpackTransientVariableValuesIntoEvaluator(CompressedState const& state, storm::expressions::ExpressionEvaluator& evaluator) const { + transientVariableInformation.setDefaultValuesInEvaluator(evaluator); + auto transientVariableValuation = getTransientVariableValuationAtLocations(getLocations(state), evaluator); + transientVariableValuation.setInEvaluator(evaluator, this->getOptions().isExplorationChecksSet()); + } + template storm::storage::sparse::StateValuationsBuilder JaniNextStateGenerator::initializeStateValuationsBuilder() const { auto result = NextStateGenerator::initializeStateValuationsBuilder(); @@ -500,7 +507,7 @@ namespace storm { extractVariableValues(*this->state, this->variableInformation, integerValues, booleanValues, integerValues); // Add values for transient variables - auto transientVariableValuation = getTransientVariableValuationAtLocations(getLocations(*this->state)); + auto transientVariableValuation = getTransientVariableValuationAtLocations(getLocations(*this->state), *this->evaluator); { auto varIt = transientVariableValuation.booleanValues.begin(); auto varIte = transientVariableValuation.booleanValues.end(); @@ -551,7 +558,7 @@ namespace storm { // 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); + auto transientVariableValuation = getTransientVariableValuationAtLocations(locations, *this->evaluator); transientVariableValuation.setInEvaluator(*this->evaluator, this->getOptions().isExplorationChecksSet()); result.addStateRewards(evaluateRewardExpressions()); this->transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator); @@ -1096,26 +1103,17 @@ namespace storm { template storm::models::sparse::StateLabeling JaniNextStateGenerator::label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices) { + // As in JANI we can use transient boolean variable assignments in locations to identify states, we need to // create a list of boolean transient variables and the expressions that define them. - std::unordered_map transientVariableToExpressionMap; - bool translateArrays = !this->arrayEliminatorData.replacements.empty(); + std::vector> transientVariableExpressions; for (auto const& variable : model.getGlobalVariables().getTransientVariables()) { if (variable.isBooleanVariable()) { if (this->options.isBuildAllLabelsSet() || this->options.getLabelNames().find(variable.getName()) != this->options.getLabelNames().end()) { - storm::expressions::Expression labelExpression = model.getLabelExpression(variable.asBooleanVariable(), this->parallelAutomata); - if (translateArrays) { - labelExpression = this->arrayEliminatorData.transformExpression(labelExpression); - } - transientVariableToExpressionMap[variable.getExpressionVariable()] = std::move(labelExpression); + transientVariableExpressions.emplace_back(variable.getName(), variable.getExpressionVariable().getExpression()); } } } - - std::vector> transientVariableExpressions; - for (auto const& element : transientVariableToExpressionMap) { - transientVariableExpressions.push_back(std::make_pair(element.first.getName(), element.second)); - } return NextStateGenerator::label(stateStorage, initialStateIndices, deadlockStateIndices, transientVariableExpressions); } diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h index de4fe24ed..26e3ac632 100644 --- a/src/storm/generator/JaniNextStateGenerator.h +++ b/src/storm/generator/JaniNextStateGenerator.h @@ -65,6 +65,15 @@ namespace storm { virtual std::shared_ptr generateChoiceOrigins(std::vector& dataForChoiceOrigins) const override; + /*! + * Sets the values of all transient variables in the current state to the given evaluator. + * @pre The values of non-transient variables have been set in the provided evaluator + * @param state The current state + * @param evaluator the evaluator to which the values will be set + * @post The values of all transient variables are set in the given evaluator (including the transient variables without an explicit assignment in the current locations). + */ + virtual void unpackTransientVariableValuesIntoEvaluator(CompressedState const& state, storm::expressions::ExpressionEvaluator& evaluator) const override; + private: /*! * Retrieves the location index from the given state. @@ -119,7 +128,13 @@ namespace storm { */ virtual storm::storage::BitVector evaluateObservationLabels(CompressedState const& state) const override; - TransientVariableValuation getTransientVariableValuationAtLocations(std::vector const& locations) const; + /*! + * Computes the values of the transient variables assigned in the given locations. + * @note Only the the transient variables with an explicit assignment in the provided locations are contained in the returned struct. + * @pre The values of non-transient variables have been set in the provided evaluator + * @return a struct containing the values of the transient variables within the given locations + */ + TransientVariableValuation getTransientVariableValuationAtLocations(std::vector const& locations, storm::expressions::ExpressionEvaluator const& evaluator) const; /*! * Retrieves all choices possible from the given state. diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp index e62825d17..b68380935 100644 --- a/src/storm/generator/NextStateGenerator.cpp +++ b/src/storm/generator/NextStateGenerator.cpp @@ -169,6 +169,7 @@ namespace storm { auto const& states = stateStorage.stateToId; for (auto const& stateIndexPair : states) { unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, *this->evaluator); + unpackTransientVariableValuesIntoEvaluator(stateIndexPair.first, *this->evaluator); for (auto const& label : labelsAndExpressions) { // Add label to state, if the corresponding expression is true. @@ -209,6 +210,12 @@ namespace storm { return result; } + template + void NextStateGenerator::unpackTransientVariableValuesIntoEvaluator(CompressedState const&, storm::expressions::ExpressionEvaluator&) const { + // Intentionally left empty. + // This method should be overwritten in case there are transient variables (e.g. JANI). + } + template void NextStateGenerator::postprocess(StateBehavior& result) { // If the model we build is a Markov Automaton, we postprocess the choices to sum all Markovian choices diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h index 59f50843e..126d0fa5a 100644 --- a/src/storm/generator/NextStateGenerator.h +++ b/src/storm/generator/NextStateGenerator.h @@ -95,6 +95,15 @@ namespace storm { */ storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices, std::vector> labelsAndExpressions); + /*! + * Sets the values of all transient variables in the current state to the given evaluator. + * @pre The values of non-transient variables have been set in the provided evaluator + * @param state The current state + * @param evaluator the evaluator to which the values will be set + * @post The values of all transient variables are set in the given evaluator (including the transient variables without an explicit assignment in the current locations). + */ + virtual void unpackTransientVariableValuesIntoEvaluator(CompressedState const& state, storm::expressions::ExpressionEvaluator& evaluator) const; + virtual storm::storage::BitVector evaluateObservationLabels(CompressedState const& state) const =0; virtual storm::storage::sparse::StateValuationsBuilder initializeObservationValuationsBuilder() const;