Browse Source

capitalization error and fix for cumulative rewards

tempestpy_adaptions
TimQu 8 years ago
parent
commit
77e71b7876
  1. 6
      src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp
  2. 2
      src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp

6
src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp

@ -1,9 +1,9 @@
#include "SparseMdpInstantiationModelChecker.h" #include "SparseMdpInstantiationModelChecker.h"
#include "storm/logic/FragmentSpecification.h" #include "storm/logic/FragmentSpecification.h"
#include "storm/modelChecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/modelChecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/modelChecker/hints/ExplicitModelCheckerHint.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/modelchecker/hints/ExplicitModelCheckerHint.h"
#include "storm/utility/graph.h" #include "storm/utility/graph.h"
#include "storm/utility/vector.h" #include "storm/utility/vector.h"

2
src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp

@ -189,7 +189,7 @@ namespace storm {
typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel.getRewardModel(checkTask.getRewardModel()) : this->parametricModel.getUniqueRewardModel(); typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel.getRewardModel(checkTask.getRewardModel()) : this->parametricModel.getUniqueRewardModel();
std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix()); std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix());
parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, maybeStates, maybeStates);
parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), maybeStates);
computePlayer1Matrix(); computePlayer1Matrix();
applyPreviousResultAsHint = false; applyPreviousResultAsHint = false;

Loading…
Cancel
Save