From 33127c9b6e2dd8d0990af84238eefbfabdde3da6 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 4 Apr 2019 21:41:06 +0200 Subject: [PATCH] JaniNextStateGenerator: Fixed references to the unpreprocessed model. --- src/storm/generator/JaniNextStateGenerator.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 7b12a4f96..185ebfa44 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -43,7 +43,7 @@ namespace storm { JaniNextStateGenerator::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool) : NextStateGenerator(model.getExpressionManager(), options), model(model), rewardExpressions(), hasStateActionRewards(false) { STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels."); - auto features = model.getModelFeatures(); + auto features = this->model.getModelFeatures(); features.remove(storm::jani::ModelFeature::DerivedOperators); features.remove(storm::jani::ModelFeature::StateExitRewards); // Eliminate arrays if necessary. @@ -72,15 +72,15 @@ namespace storm { this->transientVariableInformation.registerArrayVariableReplacements(arrayEliminatorData); // Create a proper evalator. - this->evaluator = std::make_unique>(model.getManager()); + this->evaluator = std::make_unique>(this->model.getManager()); this->transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator); if (this->options.isBuildAllRewardModelsSet()) { - rewardExpressions = model.getAllRewardModelExpressions(); + 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, model.getRewardModelExpression(rewardModelName)); + rewardExpressions.emplace_back(rewardModelName, this->model.getRewardModelExpression(rewardModelName)); } } @@ -96,9 +96,9 @@ namespace storm { // If it's a label, i.e. refers to a transient boolean variable we need to derive the expression // for the label so we can cut off the exploration there. if (expressionOrLabelAndBool.first.getLabel() != "init" && expressionOrLabelAndBool.first.getLabel() != "deadlock") { - STORM_LOG_THROW(model.getGlobalVariables().hasVariable(expressionOrLabelAndBool.first.getLabel()) , storm::exceptions::InvalidSettingsException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'."); + STORM_LOG_THROW(this->model.getGlobalVariables().hasVariable(expressionOrLabelAndBool.first.getLabel()) , storm::exceptions::InvalidSettingsException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'."); - storm::jani::Variable const& variable = model.getGlobalVariables().getVariable(expressionOrLabelAndBool.first.getLabel()); + storm::jani::Variable const& variable = this->model.getGlobalVariables().getVariable(expressionOrLabelAndBool.first.getLabel()); STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-boolean variable '" << expressionOrLabelAndBool.first.getLabel() << "'."); STORM_LOG_THROW(variable.isTransient(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-transient variable '" << expressionOrLabelAndBool.first.getLabel() << "'.");