diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index eb19fede0..7109b7b1d 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -75,6 +75,8 @@ namespace storm { this->checkValid(); this->variableInformation = VariableInformation(this->model, this->parallelAutomata, options.getReservedBitsForUnboundedVariables(), options.isAddOutOfBoundsStateSet()); this->variableInformation.registerArrayVariableReplacements(arrayEliminatorData); + this->transientVariableInformation = TransientVariableInformation(this->model, this->parallelAutomata); + this->transientVariableInformation.registerArrayVariableReplacements(arrayEliminatorData); // Create a proper evalator. this->evaluator = std::make_unique>(model.getManager()); @@ -326,7 +328,7 @@ namespace storm { // Iterate over all boolean assignments and carry them out. auto boolIt = this->variableInformation.booleanVariables.begin(); - for (; assignmentIt != assignmentIte && assignmentIt->getAssignedExpression().hasBooleanType() && assignmentIt->getLValue().isVariable(); ++assignmentIt) { + for (; assignmentIt != assignmentIte && assignmentIt->lValueIsVariable() && assignmentIt->getExpressionVariable().hasBooleanType(); ++assignmentIt) { while (assignmentIt->getExpressionVariable() != boolIt->variable) { ++boolIt; } @@ -335,7 +337,7 @@ namespace storm { // Iterate over all integer assignments and carry them out. auto integerIt = this->variableInformation.integerVariables.begin(); - for (; assignmentIt != assignmentIte && assignmentIt->getAssignedExpression().hasIntegerType() && assignmentIt->getLValue().isVariable(); ++assignmentIt) { + for (; assignmentIt != assignmentIte && assignmentIt->lValueIsVariable() && assignmentIt->getExpressionVariable().hasIntegerType(); ++assignmentIt) { while (assignmentIt->getExpressionVariable() != integerIt->variable) { ++integerIt; } @@ -348,12 +350,11 @@ namespace storm { STORM_LOG_THROW(assignedValue >= integerIt->lowerBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'."); STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'."); } - newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound); STORM_LOG_ASSERT(static_cast(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ")."); } // Iterate over all array access assignments and carry them out. - for (; assignmentIt != assignmentIte && assignmentIt->getLValue().isArrayAccess(); ++assignmentIt) { + for (; assignmentIt != assignmentIte && assignmentIt->lValueIsArrayAccess(); ++assignmentIt) { int_fast64_t arrayIndex = expressionEvaluator.asInt(assignmentIt->getLValue().getArrayIndex()); if (assignmentIt->getAssignedExpression().hasIntegerType()) { IntegerVariableInformation const& intInfo = this->variableInformation.getIntegerArrayVariableReplacement(assignmentIt->getLValue().getArray().getExpressionVariable(), arrayIndex); @@ -381,6 +382,71 @@ namespace storm { return newState; } + template + void JaniNextStateGenerator::applyTransientUpdate(TransientVariableValuation& transientValuation, storm::jani::EdgeDestination const& destination, int64_t assignmentLevel, storm::expressions::ExpressionEvaluator const& expressionEvaluator) { + + // Perform the assignments. + auto const& assignments = destination.getOrderedAssignments().getTransientAssignments(assignmentLevel); + auto assignmentIt = assignments.begin(); + auto assignmentIte = assignments.end(); + + // Iterate over all boolean assignments and carry them out. + auto boolIt = this->transientVariableInformation.booleanVariableInformation.begin(); + for (; assignmentIt != assignmentIte && assignmentIt->lValueIsVariable() && assignmentIt->getExpressionVariable().hasBooleanType(); ++assignmentIt) { + while (assignmentIt->getExpressionVariable() != boolIt->variable) { + ++boolIt; + } + transientValuation.booleanValues.emplace_back(&(*boolIt), expressionEvaluator.asBool(assignmentIt->getAssignedExpression())); + } + // Iterate over all integer assignments and carry them out. + auto integerIt = this->transientVariableInformation.integerVariableInformation.begin(); + for (; assignmentIt != assignmentIte && assignmentIt->lValueIsVariable() && assignmentIt->getExpressionVariable().hasIntegerType(); ++assignmentIt) { + while (assignmentIt->getExpressionVariable() != integerIt->variable) { + ++integerIt; + } + int64_t assignedValue = expressionEvaluator.asInt(assignmentIt->getAssignedExpression()); + if (this->options.isExplorationChecksSet()) { + STORM_LOG_THROW(assignedValue >= integerIt->lowerBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'."); + STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'."); + } + transientValuation.integerValues.emplace_back(&(*integerIt), assignedValue); + } + // Iterate over all rational assignments and carry them out. + auto rationalIt = this->transientVariableInformation.rationalVariableInformation.begin(); + for (; assignmentIt != assignmentIte && assignmentIt->lValueIsVariable() && assignmentIt->getExpressionVariable().hasRationalType(); ++assignmentIt) { + while (assignmentIt->getExpressionVariable() != rationalIt->variable) { + ++rationalIt; + } + transientValuation.rationalValues.emplace_back(&(*rationalIt), expressionEvaluator.asRational(assignmentIt->getAssignedExpression())); + } + + // Iterate over all array access assignments and carry them out. + for (; assignmentIt != assignmentIte && assignmentIt->lValueIsArrayAccess(); ++assignmentIt) { + int_fast64_t arrayIndex = expressionEvaluator.asInt(assignmentIt->getLValue().getArrayIndex()); + storm::expressions::Type const& baseType = assignmentIt->getLValue().getArray().getExpressionVariable().getType(); + if (baseType.isIntegerType()) { + auto const& intInfo = this->transientVariableInformation.getIntegerArrayVariableReplacement(assignmentIt->getLValue().getArray().getExpressionVariable(), arrayIndex); + int64_t assignedValue = expressionEvaluator.asInt(assignmentIt->getAssignedExpression()); + if (this->options.isExplorationChecksSet()) { + STORM_LOG_THROW(assignedValue >= intInfo.lowerBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getLValue() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'."); + STORM_LOG_THROW(assignedValue <= intInfo.upperBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getLValue() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'."); + } + transientValuation.integerValues.emplace_back(&intInfo, assignedValue); + } else if (baseType.isBooleanType()) { + auto const& boolInfo = this->transientVariableInformation.getBooleanArrayVariableReplacement(assignmentIt->getLValue().getArray().getExpressionVariable(), arrayIndex); + transientValuation.booleanValues.emplace_back(&boolInfo, expressionEvaluator.asBool(assignmentIt->getAssignedExpression())); + } else if (baseType.isRationalType()) { + auto const& rationalInfo = this->transientVariableInformation.getRationalArrayVariableReplacement(assignmentIt->getLValue().getArray().getExpressionVariable(), arrayIndex); + transientValuation.rationalValues.emplace_back(&rationalInfo, expressionEvaluator.asRational(assignmentIt->getAssignedExpression())); + } else { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unhandled type of base variable."); + } + } + + // Check that we processed all assignments. + STORM_LOG_ASSERT(assignmentIt == assignmentIte, "Not all assignments were consumed."); + } + template StateBehavior JaniNextStateGenerator::expand(StateToIdCallback const& stateToIdCallback) { // Prepare the result, in case we return early. @@ -486,6 +552,7 @@ namespace storm { } Choice choice(edge.getActionIndex(), static_cast(exitRate)); + TransientVariableValuation transientVariableValuation; std::vector stateActionRewards(rewardVariables.size(), storm::utility::zero()); // Iterate over all updates of the current command. @@ -498,10 +565,12 @@ namespace storm { // seen, we also add it to the set of states that have yet to be explored. int64_t assignmentLevel = edge.getLowestAssignmentLevel(); // Might be the largest possible integer, if there is no assignment int64_t const& highestLevel = edge.getHighestAssignmentLevel(); - bool hasTransientRewardAssignments = destination.hasTransientAssignment(); + bool hasTransientAssignments = destination.hasTransientAssignment(); CompressedState newState = applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex], assignmentLevel, *this->evaluator); - if (hasTransientRewardAssignments) { + if (hasTransientAssignments) { + transientVariableValuation.clear(); STORM_LOG_ASSERT(this->options.isScaleAndLiftTransitionRewardsSet(), "Transition rewards are not supported and scaling to action rewards is disabled."); + applyTransientUpdate(transientVariableValuation, destination, assignmentLevel, *this->evaluator); // Create the rewards for this destination auto valueIt = stateActionRewards.begin(); performTransientAssignments(destination.getOrderedAssignments().getTransientAssignments(assignmentLevel), *this->evaluator, [&] (ValueType const& value) { *valueIt += (value * probability); ++valueIt; } ); @@ -510,15 +579,21 @@ namespace storm { while (assignmentLevel < highestLevel) { ++assignmentLevel; unpackStateIntoEvaluator(newState, this->variableInformation, *this->evaluator); + transientVariableValuation.setInEvaluator(*this->evaluator, this->getOptions().isExplorationChecksSet()); + transientVariableValuation.clear(); newState = applyUpdate(newState, destination, this->variableInformation.locationVariables[automatonIndex], assignmentLevel, *this->evaluator); - if (hasTransientRewardAssignments) { + if (hasTransientAssignments) { + applyTransientUpdate(transientVariableValuation, destination, assignmentLevel, *this->evaluator); // update the rewards for this destination auto valueIt = stateActionRewards.begin(); performTransientAssignments(destination.getOrderedAssignments().getTransientAssignments(assignmentLevel), *this->evaluator, [&] (ValueType const& value) { *valueIt += (value * probability); ++valueIt; } ); } } - // Restore the old state information + // Restore the old information unpackStateIntoEvaluator(state, this->variableInformation, *this->evaluator); + if (hasTransientAssignments) { + this->transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator); + } } StateType stateIndex = stateToIdCallback(newState); @@ -589,6 +664,7 @@ namespace storm { numDestinations *= edge.getNumberOfDestinations(); } std::vector destinationRewards; + TransientVariableValuation transientVariableValuation; std::vector destinations; std::vector locationVars; destinations.reserve(iteratorList.size()); @@ -599,6 +675,7 @@ namespace storm { destinations.clear(); locationVars.clear(); destinationRewards.assign(rewardVariables.size(), storm::utility::zero()); + transientVariableValuation.clear(); CompressedState successorState = state; ValueType successorProbability = storm::utility::one(); @@ -621,7 +698,8 @@ namespace storm { } successorState = applyUpdate(successorState, *destinations.back(), *locationVars.back(), lowestLevel, *this->evaluator); - + applyTransientUpdate(transientVariableValuation, *destinations.back(), lowestLevel, *this->evaluator); + // add the reward for this destination to the destination rewards auto valueIt = destinationRewards.begin(); performTransientAssignments(destinations.back()->getOrderedAssignments().getTransientAssignments(lowestLevel), *this->evaluator, [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); @@ -634,9 +712,13 @@ namespace storm { while (assignmentLevel < highestLevel) { ++assignmentLevel; unpackStateIntoEvaluator(successorState, this->variableInformation, *this->evaluator); + transientVariableValuation.setInEvaluator(*this->evaluator, this->getOptions().isExplorationChecksSet()); + transientVariableValuation.clear(); + auto locationVarIt = locationVars.begin(); for (auto const& destPtr : destinations) { successorState = applyUpdate(successorState, *destPtr, **locationVarIt, assignmentLevel, *this->evaluator); + applyTransientUpdate(transientVariableValuation, *destinations.back(), lowestLevel, *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; } ); @@ -645,6 +727,7 @@ namespace storm { } // Restore the old state information unpackStateIntoEvaluator(state, this->variableInformation, *this->evaluator); + this->transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator); } StateType id = stateToIdCallback(successorState); distribution.add(id, successorProbability); diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h index 43f195c3b..1dbc4440e 100644 --- a/src/storm/generator/JaniNextStateGenerator.h +++ b/src/storm/generator/JaniNextStateGenerator.h @@ -3,6 +3,7 @@ #include #include "storm/generator/NextStateGenerator.h" +#include "storm/generator/TransientVariableInformation.h" #include "storm/storage/jani/Model.h" #include "storm/storage/jani/ArrayEliminator.h" @@ -72,12 +73,23 @@ namespace storm { * Applies an update to the state currently loaded into the evaluator and applies the resulting values to * the given compressed state. * @params state The state to which to apply the new values. - * @params update The update to apply. + * @params destination The update to apply. * @params locationVariable The location variable that is being updated. * @params assignmentLevel The assignmentLevel that is to be considered for the update. * @return The resulting state. */ - CompressedState applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& update, storm::generator::LocationVariableInformation const& locationVariable, int64_t assignmentlevel, storm::expressions::ExpressionEvaluator const& expressionEvaluator); + CompressedState applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& destination, storm::generator::LocationVariableInformation const& locationVariable, int64_t assignmentlevel, storm::expressions::ExpressionEvaluator const& expressionEvaluator); + + /*! + * Applies an update to the state currently loaded into the evaluator and applies the resulting values to + * the given compressed state. + * @params state The state to which to apply the new values. + * @params destination The update to apply. + * @params locationVariable The location variable that is being updated. + * @params assignmentLevel The assignmentLevel that is to be considered for the update. + * @return The resulting state. + */ + void applyTransientUpdate(TransientVariableValuation& transientValuation, storm::jani::EdgeDestination const& destination, int64_t assignmentlevel, storm::expressions::ExpressionEvaluator const& expressionEvaluator); /*! * Retrieves all choices possible from the given state. @@ -151,7 +163,9 @@ namespace storm { /// Data from eliminated array expressions. These are required to keep references to array variables in LValues alive. storm::jani::ArrayEliminatorData arrayEliminatorData; - + + /// Information about the transient variables of the model. + TransientVariableInformation transientVariableInformation; }; } diff --git a/src/storm/generator/TransientVariableInformation.cpp b/src/storm/generator/TransientVariableInformation.cpp new file mode 100644 index 000000000..461b43eb0 --- /dev/null +++ b/src/storm/generator/TransientVariableInformation.cpp @@ -0,0 +1,183 @@ +#include "storm/generator/TransientVariableInformation.h" + +#include "storm/storage/jani/Model.h" + +#include "storm/storage/jani/Automaton.h" +#include "storm/storage/jani/ArrayEliminator.h" +#include "storm/storage/jani/AutomatonComposition.h" +#include "storm/storage/jani/ParallelComposition.h" +#include "storm/storage/expressions/ExpressionManager.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/WrongFormatException.h" +#include "storm/exceptions/OutOfRangeException.h" + + +#include + +namespace storm { + namespace generator { + + template <> + TransientVariableData::TransientVariableData(storm::expressions::Variable const& variable, boost::optional const& lowerBound, boost::optional const& upperBound, storm::RationalFunction const& defaultValue, bool global) : variable(variable), lowerBound(lowerBound), upperBound(upperBound), defaultValue(defaultValue) { + // There is no '<=' for rational functions. Therefore, do not check the bounds for this ValueType + } + + template + TransientVariableData::TransientVariableData(storm::expressions::Variable const& variable, boost::optional const& lowerBound, boost::optional const& upperBound, VariableType const& defaultValue, bool global) : variable(variable), lowerBound(lowerBound), upperBound(upperBound), defaultValue(defaultValue) { + STORM_LOG_THROW(!lowerBound.is_initialized() || lowerBound.get() <= defaultValue, storm::exceptions::OutOfRangeException, "The default value for transient variable " << variable.getName() << " is smaller than its lower bound."); + STORM_LOG_THROW(!upperBound.is_initialized() || defaultValue <= upperBound.get(), storm::exceptions::OutOfRangeException, "The default value for transient variable " << variable.getName() << " is higher than its upper bound."); + } + + template + TransientVariableData::TransientVariableData(storm::expressions::Variable const& variable, VariableType const& defaultValue, bool global) : variable(variable), defaultValue(defaultValue) { + // Intentionally left empty. + } + + template + TransientVariableInformation::TransientVariableInformation(storm::jani::Model const& model, std::vector> const& parallelAutomata) { + + createVariablesForVariableSet(model.getGlobalVariables(), true); + + for (auto const& automatonRef : parallelAutomata) { + createVariablesForAutomaton(automatonRef.get()); + } + + sortVariables(); + } + + template + void TransientVariableInformation::registerArrayVariableReplacements(storm::jani::ArrayEliminatorData const& arrayEliminatorData) { + arrayVariableToElementInformations.clear(); + // Find for each replaced array variable the corresponding references in this variable information + for (auto const& arrayVariable : arrayEliminatorData.eliminatedArrayVariables) { + if (arrayVariable->isTransient()) { + STORM_LOG_ASSERT(arrayEliminatorData.replacements.count(arrayVariable->getExpressionVariable()) > 0, "No replacement for array variable."); + auto const& replacements = arrayEliminatorData.replacements.find(arrayVariable->getExpressionVariable())->second; + std::vector varInfoIndices; + for (auto const& replacedVar : replacements) { + if (replacedVar->getExpressionVariable().hasIntegerType()) { + uint64_t index = 0; + for (auto const& intInfo : integerVariableInformation) { + if (intInfo.variable == replacedVar->getExpressionVariable()) { + varInfoIndices.push_back(index); + break; + } + ++index; + } + STORM_LOG_ASSERT(!varInfoIndices.empty() && varInfoIndices.back() == index, "Could not find a basic variable for replacement of array variable " << replacedVar->getExpressionVariable().getName() << " ."); + } else if (replacedVar->getExpressionVariable().hasBooleanType()) { + uint64_t index = 0; + for (auto const& boolInfo : booleanVariableInformation) { + if (boolInfo.variable == replacedVar->getExpressionVariable()) { + varInfoIndices.push_back(index); + break; + } + ++index; + } + STORM_LOG_ASSERT(!varInfoIndices.empty() && varInfoIndices.back() == index, "Could not find a basic variable for replacement of array variable " << replacedVar->getExpressionVariable().getName() << " ."); + } else if (replacedVar->getExpressionVariable().hasRationalType()) { + uint64_t index = 0; + for (auto const& rationalInfo : rationalVariableInformation) { + if (rationalInfo.variable == replacedVar->getExpressionVariable()) { + varInfoIndices.push_back(index); + break; + } + ++index; + } + STORM_LOG_ASSERT(!varInfoIndices.empty() && varInfoIndices.back() == index, "Could not find a basic variable for replacement of array variable " << replacedVar->getExpressionVariable().getName() << " ."); + } else { + STORM_LOG_ASSERT(false, "Unhandled type of base variable."); + } + } + this->arrayVariableToElementInformations.emplace(arrayVariable->getExpressionVariable(), std::move(varInfoIndices)); + } + } + } + + template + TransientVariableData const& TransientVariableInformation::getBooleanArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t arrayIndex) { + std::vector 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 + TransientVariableData const& TransientVariableInformation::getIntegerArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t arrayIndex) { + std::vector 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 + TransientVariableData const& TransientVariableInformation::getRationalArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t arrayIndex) { + std::vector 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]]; + } + + template + void TransientVariableInformation::createVariablesForAutomaton(storm::jani::Automaton const& automaton) { + createVariablesForVariableSet(automaton.getVariables(), false); + } + + template + void TransientVariableInformation::createVariablesForVariableSet(storm::jani::VariableSet const& variableSet, bool global) { + for (auto const& variable : variableSet.getBooleanVariables()) { + if (variable.isTransient()) { + booleanVariableInformation.emplace_back(variable.getExpressionVariable(), variable.getInitExpression().evaluateAsBool(), global); + } + } + for (auto const& variable : variableSet.getBoundedIntegerVariables()) { + if (variable.isTransient()) { + boost::optional lowerBound; + boost::optional upperBound; + if (variable.hasLowerBound()) { + lowerBound = variable.getLowerBound().evaluateAsInt(); + } + if (variable.hasUpperBound()) { + upperBound = variable.getUpperBound().evaluateAsInt(); + } + integerVariableInformation.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, variable.getInitExpression().evaluateAsInt(), global); + } + } + for (auto const& variable : variableSet.getUnboundedIntegerVariables()) { + if (variable.isTransient()) { + integerVariableInformation.emplace_back(variable.getExpressionVariable(), variable.getInitExpression().evaluateAsInt(), global); + } + } + for (auto const& variable : variableSet.getRealVariables()) { + if (variable.isTransient()) { + rationalVariableInformation.emplace_back(variable.getExpressionVariable(), storm::utility::convertNumber(variable.getInitExpression().evaluateAsRational()), global); + } + } + } + + template + void TransientVariableInformation::sortVariables() { + // Sort the variables so we can make some assumptions when iterating over them (in the next-state generators). + std::sort(booleanVariableInformation.begin(), booleanVariableInformation.end(), [] (TransientVariableData const& a, TransientVariableData const& b) { return a.variable < b.variable; } ); + std::sort(integerVariableInformation.begin(), integerVariableInformation.end(), [] (TransientVariableData const& a, TransientVariableData const& b) { return a.variable < b.variable; } ); + std::sort(rationalVariableInformation.begin(), rationalVariableInformation.end(), [] (TransientVariableData const& a, TransientVariableData const& b) { return a.variable < b.variable; } ); + } + + template + void TransientVariableInformation::setDefaultValuesInEvaluator(storm::expressions::ExpressionEvaluator& evaluator) const { + for (auto const& variableData : booleanVariableInformation) { + evaluator.setBooleanValue(variableData.variable, variableData.defaultValue); + } + for (auto const& variableData : integerVariableInformation) { + evaluator.setIntegerValue(variableData.variable, variableData.defaultValue); + } + for (auto const& variableData : rationalVariableInformation) { + evaluator.setRationalValue(variableData.variable, variableData.defaultValue); + } + } + + template class TransientVariableInformation; + template class TransientVariableInformation; + template class TransientVariableInformation; + + } +} diff --git a/src/storm/generator/TransientVariableInformation.h b/src/storm/generator/TransientVariableInformation.h new file mode 100644 index 000000000..8300b6702 --- /dev/null +++ b/src/storm/generator/TransientVariableInformation.h @@ -0,0 +1,124 @@ +#pragma once + +#include +#include +#include + +#include "storm/storage/expressions/Variable.h" +#include "storm/storage/expressions/Expression.h" +#include "storm/storage/expressions/ExpressionEvaluator.h" +#include "storm/utility/macros.h" + +#include "storm/exceptions/OutOfRangeException.h" + +namespace storm { + + namespace jani { + class Model; + class Automaton; + class ArrayEliminatorData; + class VariableSet; + } + + namespace expressions { + template + class ExpressionEvaluator; + } + + namespace generator { + + + // A structure storing information about a transient variable + + template + struct TransientVariableData { + TransientVariableData(storm::expressions::Variable const& variable, boost::optional const& lowerBound, boost::optional const& upperBound, VariableType const& defaultValue, bool global = false); + TransientVariableData(storm::expressions::Variable const& variable, VariableType const& defaultValue, bool global = false); + + // The integer variable. + storm::expressions::Variable variable; + + // The lower bound of its range. + boost::optional lowerBound; + + // The upper bound of its range. + boost::optional upperBound; + + // Its default value + VariableType defaultValue; + + // A flag indicating whether the variable is a global one. + bool global; + + }; + + template + struct TransientVariableValuation { + std::vector const*, bool>> booleanValues; + std::vector const*, int64_t>> integerValues; + std::vector const*, ValueType>> rationalValues; + + void clear() { + booleanValues.clear(); + integerValues.clear(); + rationalValues.clear(); + } + + void setInEvaluator(storm::expressions::ExpressionEvaluator& evaluator, bool explorationChecks) const { + for (auto const& varValue : booleanValues) { + evaluator.setBooleanValue(varValue.first->variable, varValue.second); + } + for (auto const& varValue : integerValues) { + if (explorationChecks) { + STORM_LOG_THROW(!varValue.first->lowerBound.is_initialized() || varValue.first->lowerBound.get() <= varValue.second, storm::exceptions::OutOfRangeException, "The assigned value for transient variable " << varValue.first->variable.getName() << " is smaller than its lower bound."); + STORM_LOG_THROW(varValue.first->upperBound.is_initialized() || varValue.second <= varValue.first->upperBound.get(), storm::exceptions::OutOfRangeException, "The assigned value for transient variable " << varValue.first->variable.getName() << " is higher than its upper bound."); + } + evaluator.setIntegerValue(varValue.first->variable, varValue.second); + } + for (auto const& varValue : rationalValues) { + evaluator.setRationalValue(varValue.first->variable, varValue.second); + } + } + }; + + // A structure storing information about the used variables of the program. + template + struct TransientVariableInformation { + TransientVariableInformation(storm::jani::Model const& model, std::vector> const& parallelAutomata); + + TransientVariableInformation() = default; + + void registerArrayVariableReplacements(storm::jani::ArrayEliminatorData const& arrayEliminatorData); + TransientVariableData const& getBooleanArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t index); + TransientVariableData const& getIntegerArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t index); + TransientVariableData const& getRationalArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t index); + + void setDefaultValuesInEvaluator(storm::expressions::ExpressionEvaluator& evaluator) const; + + std::vector> booleanVariableInformation; + std::vector> integerVariableInformation; + std::vector> rationalVariableInformation; + + /// Replacements for each array variable + std::unordered_map> arrayVariableToElementInformations; + + + private: + /*! + * Sorts the variables to establish a known ordering. + */ + void sortVariables(); + + /*! + * Creates all necessary variables for a JANI automaton. + */ + void createVariablesForAutomaton(storm::jani::Automaton const& automaton); + + /*! + * Creates all non-transient variables from the given set + */ + void createVariablesForVariableSet(storm::jani::VariableSet const& variableSet, bool global); + }; + + } +}