TimQu
6 years ago
4 changed files with 416 additions and 12 deletions
-
101src/storm/generator/JaniNextStateGenerator.cpp
-
20src/storm/generator/JaniNextStateGenerator.h
-
183src/storm/generator/TransientVariableInformation.cpp
-
124src/storm/generator/TransientVariableInformation.h
@ -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 <cmath>
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace generator { |
||||
|
|
||||
|
template <> |
||||
|
TransientVariableData<storm::RationalFunction>::TransientVariableData(storm::expressions::Variable const& variable, boost::optional<storm::RationalFunction> const& lowerBound, boost::optional<storm::RationalFunction> 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 <typename VariableType> |
||||
|
TransientVariableData<VariableType>::TransientVariableData(storm::expressions::Variable const& variable, boost::optional<VariableType> const& lowerBound, boost::optional<VariableType> 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 <typename VariableType> |
||||
|
TransientVariableData<VariableType>::TransientVariableData(storm::expressions::Variable const& variable, VariableType const& defaultValue, bool global) : variable(variable), defaultValue(defaultValue) { |
||||
|
// Intentionally left empty.
|
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
TransientVariableInformation<ValueType>::TransientVariableInformation(storm::jani::Model const& model, std::vector<std::reference_wrapper<storm::jani::Automaton const>> const& parallelAutomata) { |
||||
|
|
||||
|
createVariablesForVariableSet(model.getGlobalVariables(), true); |
||||
|
|
||||
|
for (auto const& automatonRef : parallelAutomata) { |
||||
|
createVariablesForAutomaton(automatonRef.get()); |
||||
|
} |
||||
|
|
||||
|
sortVariables(); |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void TransientVariableInformation<ValueType>::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<uint64_t> 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 <typename ValueType> |
||||
|
TransientVariableData<bool> const& TransientVariableInformation<ValueType>::getBooleanArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t arrayIndex) { |
||||
|
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) { |
||||
|
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) { |
||||
|
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]]; |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void TransientVariableInformation<ValueType>::createVariablesForAutomaton(storm::jani::Automaton const& automaton) { |
||||
|
createVariablesForVariableSet(automaton.getVariables(), false); |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void TransientVariableInformation<ValueType>::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<int64_t> lowerBound; |
||||
|
boost::optional<int64_t> 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<ValueType>(variable.getInitExpression().evaluateAsRational()), global); |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void TransientVariableInformation<ValueType>::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<bool> const& a, TransientVariableData<bool> const& b) { return a.variable < b.variable; } ); |
||||
|
std::sort(integerVariableInformation.begin(), integerVariableInformation.end(), [] (TransientVariableData<int64_t> const& a, TransientVariableData<int64_t> const& b) { return a.variable < b.variable; } ); |
||||
|
std::sort(rationalVariableInformation.begin(), rationalVariableInformation.end(), [] (TransientVariableData<ValueType> const& a, TransientVariableData<ValueType> const& b) { return a.variable < b.variable; } ); |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType> |
||||
|
void TransientVariableInformation<ValueType>::setDefaultValuesInEvaluator(storm::expressions::ExpressionEvaluator<ValueType>& 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<double>; |
||||
|
template class TransientVariableInformation<storm::RationalNumber>; |
||||
|
template class TransientVariableInformation<storm::RationalFunction>; |
||||
|
|
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,124 @@ |
|||||
|
#pragma once |
||||
|
|
||||
|
#include <vector> |
||||
|
#include <unordered_map> |
||||
|
#include <boost/optional.hpp> |
||||
|
|
||||
|
#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 <typename ValueType> |
||||
|
class ExpressionEvaluator; |
||||
|
} |
||||
|
|
||||
|
namespace generator { |
||||
|
|
||||
|
|
||||
|
// A structure storing information about a transient variable |
||||
|
|
||||
|
template <typename VariableType> |
||||
|
struct TransientVariableData { |
||||
|
TransientVariableData(storm::expressions::Variable const& variable, boost::optional<VariableType> const& lowerBound, boost::optional<VariableType> 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<VariableType> lowerBound; |
||||
|
|
||||
|
// The upper bound of its range. |
||||
|
boost::optional<VariableType> upperBound; |
||||
|
|
||||
|
// Its default value |
||||
|
VariableType defaultValue; |
||||
|
|
||||
|
// A flag indicating whether the variable is a global one. |
||||
|
bool global; |
||||
|
|
||||
|
}; |
||||
|
|
||||
|
template<typename ValueType> |
||||
|
struct TransientVariableValuation { |
||||
|
std::vector<std::pair<TransientVariableData<bool> const*, bool>> booleanValues; |
||||
|
std::vector<std::pair<TransientVariableData<int64_t> const*, int64_t>> integerValues; |
||||
|
std::vector<std::pair<TransientVariableData<ValueType> const*, ValueType>> rationalValues; |
||||
|
|
||||
|
void clear() { |
||||
|
booleanValues.clear(); |
||||
|
integerValues.clear(); |
||||
|
rationalValues.clear(); |
||||
|
} |
||||
|
|
||||
|
void setInEvaluator(storm::expressions::ExpressionEvaluator<ValueType>& 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<typename ValueType> |
||||
|
struct TransientVariableInformation { |
||||
|
TransientVariableInformation(storm::jani::Model const& model, std::vector<std::reference_wrapper<storm::jani::Automaton const>> const& parallelAutomata); |
||||
|
|
||||
|
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); |
||||
|
|
||||
|
void setDefaultValuesInEvaluator(storm::expressions::ExpressionEvaluator<ValueType>& evaluator) const; |
||||
|
|
||||
|
std::vector<TransientVariableData<bool>> booleanVariableInformation; |
||||
|
std::vector<TransientVariableData<int64_t>> integerVariableInformation; |
||||
|
std::vector<TransientVariableData<ValueType>> rationalVariableInformation; |
||||
|
|
||||
|
/// Replacements for each array variable |
||||
|
std::unordered_map<storm::expressions::Variable, std::vector<uint64_t>> 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); |
||||
|
}; |
||||
|
|
||||
|
} |
||||
|
} |
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue