Browse Source

fix in sparse ctmc model checker: bounded until returned empty result in case there are no non-prob0-states

tempestpy_adaptions
dehnert 8 years ago
parent
commit
b3a02b6e8a
  1. 2
      src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
  2. 1
      src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp

2
src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp

@ -186,6 +186,8 @@ namespace storm {
}
}
}
} else {
result = std::vector<ValueType>(numberOfStates, storm::utility::zero<ValueType>());
}
return result;

1
src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp

@ -61,6 +61,7 @@ namespace storm {
if (this->isResultForAllStates()) {
map_type newMap;
for (auto const& element : filterTruthValues) {
STORM_LOG_THROW(element < this->getValueVector().size(), storm::exceptions::InvalidAccessException, "Invalid index in results.");
newMap.emplace(element, this->getValueVector()[element]);

Loading…
Cancel
Save