Browse Source

Fixed typo and renamed a variable.

tempestpy_adaptions
TimQu 6 years ago
parent
commit
0bf9f27e31
  1. 2
      src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
  2. 8
      src/storm/storage/MaximalEndComponentDecomposition.cpp

2
src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

@ -70,7 +70,7 @@ namespace storm {
std::unique_ptr<CheckResult> rightResultPointer = this->check(env, pathFormula.getRightSubformula()); std::unique_ptr<CheckResult> rightResultPointer = this->check(env, pathFormula.getRightSubformula());
ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
STORM_LOG_THROW(pathFormula.getTimeBoundReference().isTimeBound(), storm::exceptions::NotImplementedException, "Currently step-bounded and reward=bpimded properties on MAs are not supported.");
STORM_LOG_THROW(pathFormula.getTimeBoundReference().isTimeBound(), storm::exceptions::NotImplementedException, "Currently step-bounded and reward-bounded properties on MAs are not supported.");
double lowerBound = 0; double lowerBound = 0;
double upperBound = 0; double upperBound = 0;
if (pathFormula.hasLowerBound()) { if (pathFormula.hasLowerBound()) {

8
src/storm/storage/MaximalEndComponentDecomposition.cpp

@ -74,10 +74,10 @@ namespace storm {
if (states) { if (states) {
endComponentStateSets.emplace_back(states->begin(), states->end(), true); endComponentStateSets.emplace_back(states->begin(), states->end(), true);
} else { } else {
std::vector<storm::storage::sparse::state_type> states;
states.resize(transitionMatrix.getRowGroupCount());
std::iota(states.begin(), states.end(), 0);
endComponentStateSets.emplace_back(states.begin(), states.end(), true);
std::vector<storm::storage::sparse::state_type> allStates;
allStates.resize(transitionMatrix.getRowGroupCount());
std::iota(allStates.begin(), allStates.end(), 0);
endComponentStateSets.emplace_back(allStates.begin(), allStates.end(), true);
} }
storm::storage::BitVector statesToCheck(numberOfStates); storm::storage::BitVector statesToCheck(numberOfStates);
storm::storage::BitVector includedChoices; storm::storage::BitVector includedChoices;

Loading…
Cancel
Save