diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp index d4d729d21..271a4e873 100644 --- a/src/storm/builder/BuilderOptions.cpp +++ b/src/storm/builder/BuilderOptions.cpp @@ -1,6 +1,7 @@ #include "storm/builder/BuilderOptions.h" #include "storm/logic/Formulas.h" +#include "storm/logic/FragmentSpecification.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/BuildSettings.h" @@ -36,7 +37,7 @@ namespace storm { return boost::get(labelOrExpression); } - BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), explorationChecks(false), addOverlappingGuardsLabel(false), addOutOfBoundsState(false), showProgress(false), showProgressDelay(0) { + BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), scaleAndLiftTransitionRewards(true), explorationChecks(false), addOverlappingGuardsLabel(false), addOutOfBoundsState(false), showProgress(false), showProgressDelay(0) { // Intentionally left empty. } @@ -85,6 +86,10 @@ namespace storm { for (auto const& formula : atomicExpressionFormulas) { addLabel(formula->getExpression()); } + + storm::logic::FragmentSpecification transitionRewardScalingFragment = storm::logic::csl().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setLongRunAverageOperatorsAllowed(true).setMultiObjectiveFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setStepBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedCumulativeRewardFormulasAllowed(true); + scaleAndLiftTransitionRewards = scaleAndLiftTransitionRewards && formula.isInFragment(transitionRewardScalingFragment); + } void BuilderOptions::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { @@ -160,6 +165,10 @@ namespace storm { return buildAllLabels; } + bool BuilderOptions::isScaleAndLiftTransitionRewardsSet() const { + return scaleAndLiftTransitionRewards; + } + bool BuilderOptions::isAddOutOfBoundsStateSet() const { return addOutOfBoundsState; } @@ -237,6 +246,11 @@ namespace storm { return *this; } + BuilderOptions& BuilderOptions::setScaleAndLiftTransitionRewards(bool newValue) { + scaleAndLiftTransitionRewards = newValue; + return *this; + } + BuilderOptions& BuilderOptions::setAddOutOfBoundsState(bool newValue) { addOutOfBoundsState = newValue; return *this; diff --git a/src/storm/builder/BuilderOptions.h b/src/storm/builder/BuilderOptions.h index 904d45de6..eba9ff1da 100644 --- a/src/storm/builder/BuilderOptions.h +++ b/src/storm/builder/BuilderOptions.h @@ -107,6 +107,7 @@ namespace storm { bool isBuildAllLabelsSet() const; bool isExplorationChecksSet() const; bool isShowProgressSet() const; + bool isScaleAndLiftTransitionRewardsSet() const; bool isAddOutOfBoundsStateSet() const; bool isAddOverlappingGuardLabelSet() const; uint64_t getShowProgressDelay() const; @@ -157,6 +158,13 @@ namespace storm { * @return this */ BuilderOptions& setExplorationChecks(bool newValue = true); + + /** + * Should extra checks be performed during exploration + * @param newValue The new value (default true) + * @return this + */ + BuilderOptions& setScaleAndLiftTransitionRewards(bool newValue = true); /** * Should a state for out of bounds be constructed @@ -191,16 +199,19 @@ namespace storm { /// If one of these labels/expressions evaluates to the given bool, the builder can abort the exploration. std::vector> terminalStates; - + /// A flag indicating whether or not to build choice labels. bool buildChoiceLabels; - + /// A flag indicating whether or not to build for each state the variable valuation from which it originates. bool buildStateValuations; // A flag that indicates whether or not to generate the information from which parts of the model specification // each choice originates. bool buildChoiceOrigins; + + /// A flag that stores whether potentially occurring transition rewards should be scaled and lifted to the edge + bool scaleAndLiftTransitionRewards; /// A flag that stores whether exploration checks are to be performed. bool explorationChecks; @@ -216,6 +227,7 @@ namespace storm { /// The delay for printing progress information. uint64_t showProgressDelay; + }; } diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 6bba78c1a..8f68f4c1c 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -42,6 +42,7 @@ namespace storm { STORM_LOG_THROW(!model.hasNonGlobalTransientVariable(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support automata-local transient variables."); STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels."); + // Eliminate arrays if necessary. if (this->model.containsArrayVariables()) { arrayEliminatorData = this->model.eliminateArrays(true); } @@ -50,8 +51,16 @@ namespace storm { uint64_t lowestAssignmentLevel = storm::jani::AssignmentLevelFinder().getLowestAssignmentLevel(this->model); if (this->model.hasTransientEdgeDestinationAssignments()) { this->model.liftTransientEdgeDestinationAssignments(lowestAssignmentLevel); + if (this->model.hasTransientEdgeDestinationAssignments()) { + STORM_LOG_THROW(options.isScaleAndLiftTransitionRewardsSet(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support transient edge destination assignments."); + } else { + // There are no edge destination assignments so we turn the lifting to edges off. + this->options.setScaleAndLiftTransitionRewards(false); + } + } else { + // There are no edge destination assignments so we turn the lifting to edges off. + this->options.setScaleAndLiftTransitionRewards(false); } - STORM_LOG_THROW(!this->model.hasTransientEdgeDestinationAssignments(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support transient edge destination assignments."); // Create all synchronization-related information, e.g. the automata that are put in parallel. this->createSynchronizationInformation(); @@ -358,7 +367,7 @@ namespace storm { uint64_t currentLocationIndex = locations[automatonIndex]; storm::jani::Location const& location = automaton.getLocation(currentLocationIndex); auto valueIt = stateRewards.begin(); - performTransientAssignments(location.getAssignments().getTransientAssignments(), [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); + performTransientAssignments(location.getAssignments().getTransientAssignments(), *this->evaluator, [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); ++automatonIndex; } result.addStateRewards(std::move(stateRewards)); @@ -446,6 +455,7 @@ namespace storm { } Choice choice(edge.getActionIndex(), static_cast(exitRate)); + std::vector stateActionRewards(rewardVariables.size(), storm::utility::zero()); // Iterate over all updates of the current command. ValueType probabilitySum = storm::utility::zero(); @@ -457,13 +467,26 @@ namespace storm { // seen, we also add it to the set of states that have yet to be explored. uint64_t assignmentLevel = edge.getLowestAssignmentLevel(); // Might be the largest possible integer, if there is no assignment uint64_t const& highestLevel = edge.getHighestAssignmentLevel(); + bool hasTransientRewardAssignments = destination.hasTransientAssignment(); CompressedState newState = applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex], assignmentLevel, *this->evaluator); + if (hasTransientRewardAssignments) { + STORM_LOG_ASSERT(this->options.isScaleAndLiftTransitionRewardsSet(), "Transition rewards are not supported and scaling to action rewards is disabled."); + // Create the rewards for this destination + auto valueIt = stateActionRewards.begin(); + performTransientAssignments(destination.getOrderedAssignments().getTransientAssignments(assignmentLevel), *this->evaluator, [&] (ValueType const& value) { *valueIt += (value * probability); ++valueIt; } ); + } while (assignmentLevel < highestLevel) { ++assignmentLevel; - auto nextLevelEvaluator = storm::expressions::ExpressionEvaluator(model.getManager()); - unpackStateIntoEvaluator(newState, this->variableInformation, nextLevelEvaluator); - newState = applyUpdate(newState, destination, this->variableInformation.locationVariables[automatonIndex], assignmentLevel, nextLevelEvaluator); + auto currentLevelEvaluator = storm::expressions::ExpressionEvaluator(model.getManager()); + unpackStateIntoEvaluator(newState, this->variableInformation, currentLevelEvaluator); + newState = applyUpdate(newState, destination, this->variableInformation.locationVariables[automatonIndex], assignmentLevel, currentLevelEvaluator); + if (hasTransientRewardAssignments) { + // update the rewards for this destination + auto valueIt = stateActionRewards.begin(); + performTransientAssignments(destination.getOrderedAssignments().getTransientAssignments(assignmentLevel), currentLevelEvaluator, [&] (ValueType const& value) { *valueIt += (value * probability); ++valueIt; } ); + } } + StateType stateIndex = stateToIdCallback(newState); // Update the choice by adding the probability/target state to it. @@ -476,8 +499,10 @@ namespace storm { } } - // Create the state-action reward for the newly created choice. - performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&choice] (ValueType const& value) { choice.addReward(value); } ); + // Create the state-action reward for the newly created choice. Note that edge assignments are all transient and we assume that no transient variables occur on the rhs of transient assignments, i.e., the assignment level does not matter here + auto valueIt = stateActionRewards.begin(); + performTransientAssignments(edge.getAssignments().getTransientAssignments(), *this->evaluator, [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); + choice.addRewards(std::move(stateActionRewards)); if (this->options.isExplorationChecksSet()) { // Check that the resulting distribution is in fact a distribution. @@ -510,7 +535,7 @@ namespace storm { bool done = false; while (!done) { std::vector stateActionRewards(rewardVariables.size(), storm::utility::zero()); - + currentDistribution.add(state, storm::utility::one()); EdgeIndexSet edgeIndices; @@ -531,26 +556,31 @@ namespace storm { storm::jani::Edge const& edge = *indexAndEdge.second; for (auto const& destination : edge.getDestinations()) { - for (auto const& stateProbability : currentDistribution) { - // Compute the new state under the current update and add it to the set of new target states. - CompressedState newTargetState = applyUpdate(stateProbability.getState(), destination, this->variableInformation.locationVariables[edgeCombination[i].first], assignmentLevel, *this->evaluator); - - // If the new state was already found as a successor state, update the probability - // and otherwise insert it. - ValueType probability = stateProbability.getValue() * this->evaluator->asRational(destination.getProbability()); - if (edge.hasRate()) { - probability *= this->evaluator->asRational(edge.getRate()); + ValueType destinationProbability = this->evaluator->asRational(destination.getProbability()); + if (!storm::utility::isZero(destinationProbability)) { + if (destination.hasTransientAssignment()) { + STORM_LOG_ASSERT(this->options.isScaleAndLiftTransitionRewardsSet(), "Transition rewards are not supported and scaling to action rewards is disabled."); + // add the rewards for this destination + auto valueIt = stateActionRewards.begin(); + performTransientAssignments(edge.getAssignments().getTransientAssignments(), *this->evaluator, [&] (ValueType const& value) { *valueIt += (value * destinationProbability); ++valueIt; } ); } - if (probability != storm::utility::zero()) { - nextDistribution.add(newTargetState, probability); + for (auto const& stateProbability : currentDistribution) { + // Compute the new state under the current update and add it to the set of new target states. + CompressedState newTargetState = applyUpdate(stateProbability.getState(), destination, this->variableInformation.locationVariables[edgeCombination[i].first], assignmentLevel, *this->evaluator); + + // If the new state was already found as a successor state, update the probability + // and insert it. + ValueType probability = destinationProbability * stateProbability.getValue(); + if (edge.hasRate()) { + probability *= this->evaluator->asRational(edge.getRate()); + } + if (probability != storm::utility::zero()) { + nextDistribution.add(newTargetState, probability); + } } } } - // Create the state-action reward for the newly created choice. - auto valueIt = stateActionRewards.begin(); - performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); - nextDistribution.compress(); // If there is one more command to come, shift the target states one time step back. @@ -562,13 +592,18 @@ namespace storm { // If there are different assignment levels, we need to expand the possible destinations which causes an exponential blowup... uint64_t destinationId = 0; bool lastDestinationId = false; + std::vector destinationRewards; + std::vector destinations; + std::vector locationVars; + destinations.reserve(iteratorList.size()); + locationVars.reserve(iteratorList.size()); + do { // First assignment level - std::vector destinations; - std::vector locationVars; - destinations.reserve(iteratorList.size()); - locationVars.reserve(iteratorList.size()); + destinations.clear(); + locationVars.clear(); + destinationRewards.assign(destinationRewards.size(), storm::utility::zero()); CompressedState successorState = state; ValueType successorProbability = storm::utility::one(); @@ -591,10 +626,12 @@ namespace storm { if (storm::utility::isZero(successorProbability)) { break; } - // Create the state-action reward for the newly created choice. - auto valueIt = stateActionRewards.begin(); - performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); + successorState = applyUpdate(successorState, *destinations.back(), *locationVars.back(), assignmentLevel, *this->evaluator); + + // add the reward for this destination to the destination rewards + auto valueIt = destinationRewards.begin(); + performTransientAssignments(destinations.back()->getOrderedAssignments().getTransientAssignments(assignmentLevel), *this->evaluator, [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); } if (!storm::utility::isZero(successorProbability)) { @@ -606,17 +643,27 @@ namespace storm { auto locationVarIt = locationVars.begin(); for (auto const& destPtr : destinations) { successorState = applyUpdate(successorState, *destPtr, **locationVarIt, assignmentLevel, currentLevelEvaluator); + // add the reward for this destination to the destination rewards + auto valueIt = destinationRewards.begin(); + performTransientAssignments(destinations.back()->getOrderedAssignments().getTransientAssignments(assignmentLevel), currentLevelEvaluator, [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); ++locationVarIt; } } nextDistribution.add(successorState, successorProbability); + storm::utility::vector::addScaledVector(stateActionRewards, destinationRewards, successorProbability); } - ++destinationId; } while (!lastDestinationId); std::cout << std::endl; } + for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { + storm::jani::Edge const& edge = *iteratorList[i]->second; + // Add the state-action reward for the newly created choice. Note that edge assignments are all transient and we assume that no transient variables occur on the rhs of transient assignments, i.e., the assignment level does not matter here + auto valueIt = stateActionRewards.begin(); + performTransientAssignments(edge.getAssignments().getTransientAssignments(), *this->evaluator, [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); + } + // At this point, we applied all commands of the current command combination and newTargetStates // contains all target states and their respective probabilities. That means we are now ready to // add the choice to the list of transitions. @@ -792,7 +839,7 @@ namespace storm { } template - void JaniNextStateGenerator::performTransientAssignments(storm::jani::detail::ConstAssignments const& transientAssignments, std::function const& callback) { + void JaniNextStateGenerator::performTransientAssignments(storm::jani::detail::ConstAssignments const& transientAssignments, storm::expressions::ExpressionEvaluator const& expressionEvaluator, std::function const& callback) { // If there are no reward variables, there is no need to iterate at all. if (rewardVariables.empty()) { return; @@ -810,7 +857,7 @@ namespace storm { if (rewardVariableIt == rewardVariableIte) { break; } else if (*rewardVariableIt == assignment.getExpressionVariable()) { - callback(ValueType(this->evaluator->asRational(assignment.getAssignedExpression()))); + callback(ValueType(expressionEvaluator.asRational(assignment.getAssignedExpression()))); ++rewardVariableIt; } } diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h index c80452f8c..bec4112cd 100644 --- a/src/storm/generator/JaniNextStateGenerator.h +++ b/src/storm/generator/JaniNextStateGenerator.h @@ -105,7 +105,7 @@ namespace storm { * Treats the given transient assignments by calling the callback function whenever a transient assignment * to one of the reward variables of this generator is performed. */ - void performTransientAssignments(storm::jani::detail::ConstAssignments const& transientAssignments, std::function const& callback); + void performTransientAssignments(storm::jani::detail::ConstAssignments const& transientAssignments, storm::expressions::ExpressionEvaluator const& expressionEvaluator, std::function const& callback); /*! * Builds the information structs for the reward models. diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp index c81e7df0d..8b46a3d7a 100644 --- a/src/storm/storage/jani/OrderedAssignments.cpp +++ b/src/storm/storage/jani/OrderedAssignments.cpp @@ -81,18 +81,10 @@ namespace storm { } bool OrderedAssignments::hasMultipleLevels(bool onlyTransient) const { - if (allAssignments.empty()) { + if ((onlyTransient ? transientAssignments : allAssignments).empty()) { return false; } - if (onlyTransient) { - for (auto const& a : allAssignments) { - if (a->isTransient()) { - return a->getLevel() != 0 || getHighestLevel(true) != 0; - } - } - return false; // no transient assignments - } - return getLowestLevel(false) != 0 || getHighestLevel(false) != 0; + return getLowestLevel(onlyTransient) != 0 || getHighestLevel(onlyTransient) != 0; } bool OrderedAssignments::empty() const { @@ -110,31 +102,15 @@ namespace storm { } int_fast64_t OrderedAssignments::getLowestLevel(bool onlyTransient) const { - assert(!allAssignments.empty()); - if (onlyTransient) { - for (auto const& a : allAssignments) { - if (a->getLValue().isTransient()) { - return a->getLevel(); - } - } - // assert that at least one transient variable is contained. - assert(false); - } - return allAssignments.front()->getLevel(); + auto const& as = onlyTransient ? transientAssignments : allAssignments; + assert(!as.empty()); + return as.front()->getLevel(); } int_fast64_t OrderedAssignments::getHighestLevel(bool onlyTransient) const { - assert(!allAssignments.empty()); - if (onlyTransient) { - for (auto aIt = allAssignments.rbegin(); aIt != allAssignments.rend(); ++aIt) { - if ((*aIt)->getLValue().isTransient()) { - return (*aIt)->getLevel(); - } - } - // assert that at least one transient variable is contained. - assert(false); - } - return allAssignments.back()->getLevel(); + auto const& as = onlyTransient ? transientAssignments : allAssignments; + assert(!as.empty()); + return as.back()->getLevel(); } bool OrderedAssignments::contains(Assignment const& assignment) const { @@ -222,6 +198,18 @@ namespace storm { return detail::ConstAssignments(nonTransientAssignments.begin(), nonTransientAssignments.end()); } + detail::ConstAssignments OrderedAssignments::getTransientAssignments(int_fast64_t assignmentLevel) const { + auto begin = transientAssignments.begin(); + while (begin != transientAssignments.end() && (*begin)->getLevel() < assignmentLevel) { + ++begin; + } + auto end = begin; + while (end != transientAssignments.end() && (*begin)->getLevel() == assignmentLevel) { + ++end; + } + return detail::ConstAssignments(begin, end); + } + bool OrderedAssignments::hasTransientAssignment() const { return !transientAssignments.empty(); } diff --git a/src/storm/storage/jani/OrderedAssignments.h b/src/storm/storage/jani/OrderedAssignments.h index 54ac16e0d..4d15268e7 100644 --- a/src/storm/storage/jani/OrderedAssignments.h +++ b/src/storm/storage/jani/OrderedAssignments.h @@ -96,6 +96,11 @@ namespace storm { */ detail::ConstAssignments getTransientAssignments() const; + /*! + * Returns all transient assignments in this set of assignments. + */ + detail::ConstAssignments getTransientAssignments(int_fast64_t assignmentLevel) const; + /*! * Returns all non-transient assignments in this set of assignments. */