Browse Source

Fixed Running PLA without simplification

tempestpy_adaptions
TimQu 7 years ago
parent
commit
eab7e409e9
  1. 2
      src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp

2
src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp

@ -139,7 +139,7 @@ namespace storm {
// if there are maybestates, create the parameterLifter
if (!maybeStates.empty()) {
// Create the vector of one-step probabilities to go to target states.
std::vector<typename SparseModelType::ValueType> b = this->parametricModel->getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel->getTransitionMatrix().getRowCount(), true), psiStates);
std::vector<typename SparseModelType::ValueType> b = this->parametricModel->getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel->getTransitionMatrix().getRowCount(), true), statesWithProbability01.second);
parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel->getTransitionMatrix(), b, maybeStates, maybeStates, regionSplitEstimationsEnabled);
}

Loading…
Cancel
Save