sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

JaniBuilder: Fixed several issues that occurred with branch reward expressions over non-transient variables, including GitHub issue #47

main
Tim Quatmann 7 years ago
parent
ce9d784c35
commit
c8ea0f60da
5 changed files with 74 additions and 26 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 5
      src/storm/builder/DdJaniModelBuilder.cpp
  2. 62
      src/storm/generator/JaniNextStateGenerator.cpp
  3. 6
      src/storm/generator/JaniNextStateGenerator.h
  4. 11
      src/storm/storage/jani/Model.cpp
  5. 16
      src/storm/storage/jani/Model.h

5
src/storm/builder/DdJaniModelBuilder.cpp
View File

@ -1975,13 +1975,13 @@ namespace storm {
std::vector<storm::expressions::Variable> rewardVariables;
if (options.isBuildAllRewardModelsSet()) {
for (auto const& rewExpr : model.getAllRewardModelExpressions()) {
STORM_LOG_ERROR_COND(rewExpr.second.isVariable(), "The DD-builder can not build the non-trivial reward expression '" << rewExpr.second << "'.");
STORM_LOG_THROW(!model.isNonTrivialRewardModelExpression(rewExpr.first), storm::exceptions::NotSupportedException, "The DD-builder can not build the non-trivial reward expression '" << rewExpr.second << "'.");
rewardVariables.push_back(rewExpr.second.getBaseExpression().asVariableExpression().getVariable());
}
} else {
for (auto const& rewardModelName : options.getRewardModelNames()) {
STORM_LOG_THROW(!model.isNonTrivialRewardModelExpression(rewardModelName), storm::exceptions::NotSupportedException, "The DD-builder can not build the non-trivial reward expression '" << rewardModelName << "'.");
auto const& rewExpr = model.getRewardModelExpression(rewardModelName);
STORM_LOG_ERROR_COND(rewExpr.isVariable(), "The DD-builder can not build the non-trivial reward expression '" << rewExpr << "'.");
rewardVariables.push_back(rewExpr.getBaseExpression().asVariableExpression().getVariable());
}
}
@ -2070,6 +2070,7 @@ namespace storm {
// Lift the transient edge destinations. We can do so, as we know that there are no assignment levels (because that's not supported anyway).
if (preparedModel.hasTransientEdgeDestinationAssignments()) {
// This operation is correct as we are asserting that there are no assignment levels and no non-trivial reward expressions.
preparedModel.liftTransientEdgeDestinationAssignments();
}

62
src/storm/generator/JaniNextStateGenerator.cpp
View File

@ -40,7 +40,7 @@ namespace storm {
}
template<typename ValueType, typename StateType>
JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool) : NextStateGenerator<ValueType, StateType>(model.getExpressionManager(), options), model(model), rewardExpressions(), hasStateActionRewards(false) {
JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool) : NextStateGenerator<ValueType, StateType>(model.getExpressionManager(), options), model(model), rewardExpressions(), hasStateActionRewards(false), evaluateRewardExpressionsAtEdges(false), evaluateRewardExpressionsAtDestinations(false) {
STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels.");
auto features = this->model.getModelFeatures();
@ -54,11 +54,26 @@ namespace storm {
}
STORM_LOG_THROW(features.empty(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator does not support the following model feature(s): " << features.toString() << ".");
// Preprocess the edge assignments:
if (this->model.usesAssignmentLevels()) {
// Get the reward expressions to be build. Also find out whether there is a non-trivial one.
bool hasNonTrivialRewardExpressions = false;
if (this->options.isBuildAllRewardModelsSet()) {
rewardExpressions = this->model.getAllRewardModelExpressions();
hasNonTrivialRewardExpressions = this->model.hasNonTrivialRewardExpression();
} else {
// Extract the reward models from the model based on the names we were given.
for (auto const& rewardModelName : this->options.getRewardModelNames()) {
rewardExpressions.emplace_back(rewardModelName, this->model.getRewardModelExpression(rewardModelName));
hasNonTrivialRewardExpressions = hasNonTrivialRewardExpressions || this->model.isNonTrivialRewardModelExpression(rewardModelName);
}
}
// We try to lift the edge destination assignments to the edges as this reduces the number of evaluator calls.
// However, this will only be helpful if there are no assignment levels and only trivial reward expressions.
if (hasNonTrivialRewardExpressions || this->model.usesAssignmentLevels()) {
this->model.pushEdgeAssignmentsToDestinations();
} else {
this->model.liftTransientEdgeDestinationAssignments(storm::jani::AssignmentLevelFinder().getLowestAssignmentLevel(this->model));
evaluateRewardExpressionsAtEdges = true;
}
// Create all synchronization-related information, e.g. the automata that are put in parallel.
@ -71,18 +86,10 @@ namespace storm {
this->transientVariableInformation = TransientVariableInformation<ValueType>(this->model, this->parallelAutomata);
this->transientVariableInformation.registerArrayVariableReplacements(arrayEliminatorData);
// Create a proper evalator.
// Create a proper evaluator.
this->evaluator = std::make_unique<storm::expressions::ExpressionEvaluator<ValueType>>(this->model.getManager());
this->transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator);
if (this->options.isBuildAllRewardModelsSet()) {
rewardExpressions = this->model.getAllRewardModelExpressions();
} else {
// Extract the reward models from the model based on the names we were given.
for (auto const& rewardModelName : this->options.getRewardModelNames()) {
rewardExpressions.emplace_back(rewardModelName, this->model.getRewardModelExpression(rewardModelName));
}
}
// Build the information structs for the reward models.
buildRewardModelInformation();
@ -541,18 +548,19 @@ namespace storm {
}
Choice<ValueType> choice(edge.getActionIndex(), static_cast<bool>(exitRate));
std::vector<ValueType> stateActionRewards;
// Perform the transient edge assignments and create the state action rewards
TransientVariableValuation<ValueType> transientVariableValuation;
if (!edge.getAssignments().empty()) {
if (!evaluateRewardExpressionsAtEdges || edge.getAssignments().empty()) {
stateActionRewards.resize(rewardModelInformation.size(), storm::utility::zero<ValueType>());
} else {
for (int64_t assignmentLevel = edge.getAssignments().getLowestLevel(true); assignmentLevel <= edge.getAssignments().getHighestLevel(true); ++assignmentLevel) {
transientVariableValuation.clear();
applyTransientUpdate(transientVariableValuation, edge.getAssignments().getTransientAssignments(assignmentLevel), *this->evaluator);
transientVariableValuation.setInEvaluator(*this->evaluator, this->getOptions().isExplorationChecksSet());
}
}
std::vector<ValueType> stateActionRewards = evaluateRewardExpressions();
if (!edge.getAssignments().empty()) {
stateActionRewards = evaluateRewardExpressions();
transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator);
}
@ -591,8 +599,11 @@ namespace storm {
}
}
}
addEvaluatedRewardExpressions(stateActionRewards, probability);
if (evaluateRewardExpressionsAtDestinations) {
unpackStateIntoEvaluator(newState, this->variableInformation, *this->evaluator);
evaluatorChanged = true;
addEvaluatedRewardExpressions(stateActionRewards, probability);
}
if (evaluatorChanged) {
// Restore the old variable valuation
@ -650,7 +661,7 @@ namespace storm {
// Perform the edge assignments (if there are any)
TransientVariableValuation<ValueType> transientVariableValuation;
if (lowestEdgeAssignmentLevel <= highestEdgeAssignmentLevel) {
if (evaluateRewardExpressionsAtEdges && lowestEdgeAssignmentLevel <= highestEdgeAssignmentLevel) {
for (int64_t assignmentLevel = lowestEdgeAssignmentLevel; assignmentLevel <= highestEdgeAssignmentLevel; ++assignmentLevel) {
transientVariableValuation.clear();
for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
@ -718,7 +729,11 @@ namespace storm {
evaluatorChanged = true;
transientVariableValuation.setInEvaluator(*this->evaluator, this->getOptions().isExplorationChecksSet());
}
addEvaluatedRewardExpressions(stateActionRewards, successorProbability);
if (evaluateRewardExpressionsAtDestinations) {
unpackStateIntoEvaluator(successorState, this->variableInformation, *this->evaluator);
evaluatorChanged = true;
addEvaluatedRewardExpressions(stateActionRewards, successorProbability);
}
if (evaluatorChanged) {
// Restore the old state information
unpackStateIntoEvaluator(state, this->variableInformation, *this->evaluator);
@ -977,11 +992,18 @@ namespace storm {
storm::jani::RewardModelInformation info(this->model, rewardModel.second);
rewardModelInformation.emplace_back(rewardModel.first, info.hasStateRewards(), false, false);
STORM_LOG_THROW(this->options.isScaleAndLiftTransitionRewardsSet() || !info.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Transition rewards are not supported and a reduction to action-based rewards was not possible.");
if (info.hasTransitionRewards()) {
evaluateRewardExpressionsAtDestinations = true;
}
if (info.hasActionRewards() || (this->options.isScaleAndLiftTransitionRewardsSet() && info.hasTransitionRewards())) {
hasStateActionRewards = true;
rewardModelInformation.back().setHasStateActionRewards();
}
}
if (!hasStateActionRewards) {
evaluateRewardExpressionsAtDestinations = false;
evaluateRewardExpressionsAtEdges = false;
}
}
template<typename ValueType, typename StateType>

6
src/storm/generator/JaniNextStateGenerator.h
View File

@ -167,6 +167,12 @@ namespace storm {
/// A flag that stores whether at least one of the selected reward models has state-action rewards.
bool hasStateActionRewards;
/// A flag that stores whether we shall evaluate reward expressions at edges
bool evaluateRewardExpressionsAtEdges;
/// A flag that stores whether we shall evaluate reward expressions at edge destinations
bool evaluateRewardExpressionsAtDestinations;
/// Data from eliminated array expressions. These are required to keep references to array variables in LValues alive.
storm::jani::ArrayEliminatorData arrayEliminatorData;

11
src/storm/storage/jani/Model.cpp
View File

@ -789,10 +789,19 @@ namespace storm {
return *expressionManager;
}
bool Model::hasNonTrivialRewardExpression() const {
return !nonTrivialRewardModels.empty();
}
bool Model::isNonTrivialRewardModelExpression(std::string const& identifier) const {
return nonTrivialRewardModels.count(identifier) > 0;
}
bool Model::addNonTrivialRewardExpression(std::string const& identifier, storm::expressions::Expression const& rewardExpression) {
if (nonTrivialRewardModels.count(identifier) > 0) {
if (isNonTrivialRewardModelExpression(identifier)) {
return false;
} else {
STORM_LOG_THROW(!globalVariables.hasVariable(identifier) || !globalVariables.getVariable(identifier).isTransient(), storm::exceptions::InvalidArgumentException, "Non trivial reward expression with identifier '" << identifier << "' clashes with global transient variable of the same name.");
nonTrivialRewardModels.emplace(identifier, rewardExpression);
return true;
}

16
src/storm/storage/jani/Model.h
View File

@ -285,9 +285,19 @@ namespace storm {
* Retrieves the manager responsible for the expressions in the JANI model.
*/
storm::expressions::ExpressionManager& getExpressionManager() const;
/*!
* Returns true iff there is a non-trivial reward model, i.e., a reward model that does not consist of a single, global, numerical, transient variable.
*/
bool hasNonTrivialRewardExpression() const;
/*!
* Returns true iff the given identifier corresponds to a non-trivial reward expression i.e., a reward model that does not consist of a single, global, numerical, transient variable.
*/
bool isNonTrivialRewardModelExpression(std::string const& identifier) const;
/*!
* Adds a (non-trivial) reward model, i.e., a reward model that does not consist of a single, global, numerical variable.
* Adds a reward expression, i.e., a reward model that does not consist of a single, global, numerical, transient variable.
* @return true if a new reward model was added and false if a reward model with this identifier is already present in the model (in which case no reward model is added)
*/
bool addNonTrivialRewardExpression(std::string const& identifier, storm::expressions::Expression const& rewardExpression);
@ -577,7 +587,7 @@ namespace storm {
bool undefinedConstantsAreGraphPreserving() const;
/*!
* Lifts the common edge destination assignments to edge assignments.
* Lifts the common edge destination assignments of transient variables to edge assignments.
* @param maxLevel the maximum level of assignments that are to be lifted.
*/
void liftTransientEdgeDestinationAssignments(int64_t maxLevel = 0);

Write Preview
Loading…
Cancel
Save