Browse Source

Resolved compiling issues due to recent merge

tempestpy_adaptions
TimQu 8 years ago
parent
commit
1d329176ba
  1. 2
      src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp
  2. 2
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp
  3. 4
      src/storm/models/sparse/StandardRewardModel.cpp

2
src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp

@ -379,7 +379,7 @@ namespace storm {
storm::storage::BitVector targetStateAsVector(result.preprocessedModel->getNumberOfStates(), false);
targetStateAsVector.set(*mergerResult.targetState, true);
// The overapproximation for the possible ec choices consists of the states that can reach the target states with prob. 0 and the target state itself.
result.possibleECChoices = result.preprocessedModel->getTransitionMatrix().getRowIndicesOfRowGroups(storm::utility::graph::performProb0E(*result.preprocessedModel, result.preprocessedModel->getBackwardTransitions(), storm::storage::BitVector(targetStateAsVector.size(), true), targetStateAsVector));
result.possibleECChoices = result.preprocessedModel->getTransitionMatrix().getRowFilter(storm::utility::graph::performProb0E(*result.preprocessedModel, result.preprocessedModel->getBackwardTransitions(), storm::storage::BitVector(targetStateAsVector.size(), true), targetStateAsVector));
result.possibleECChoices.set(result.preprocessedModel->getTransitionMatrix().getRowGroupIndices()[*mergerResult.targetState], true);
// There is an additional state in the result
result.possibleBottomStates.resize(result.possibleBottomStates.size() + 1, true);

2
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp

@ -96,7 +96,7 @@ namespace storm {
}
STORM_LOG_INFO("Weight vector check done. Lower bounds for results in initial state: " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(getUnderApproximationOfInitialStateResults())));
// Validate that the results are sufficiently precise
ValueType resultingWeightedPrecision = storm::utility::abs(storm::utility::vector::dotProduct(getOverApproximationOfInitialStateResults(), weightVector) - storm::utility::vector::dotProduct(getUnderApproximationOfInitialStateResults(), weightVector));
ValueType resultingWeightedPrecision = storm::utility::abs<ValueType>(storm::utility::vector::dotProduct(getOverApproximationOfInitialStateResults(), weightVector) - storm::utility::vector::dotProduct(getUnderApproximationOfInitialStateResults(), weightVector));
resultingWeightedPrecision /= storm::utility::sqrt(storm::utility::vector::dotProduct(weightVector, weightVector));
STORM_LOG_THROW(resultingWeightedPrecision <= weightedPrecision, storm::exceptions::UnexpectedException, "The desired precision was not reached");
}

4
src/storm/models/sparse/StandardRewardModel.cpp

@ -266,11 +266,11 @@ namespace storm {
if (this->hasStateActionRewards()) {
result = storm::utility::vector::filterZero(this->getStateActionRewardVector());
if (this->hasStateRewards()) {
result &= transitionMatrix.getRowIndicesOfRowGroups(storm::utility::vector::filterZero(this->getStateRewardVector()));
result &= transitionMatrix.getRowFilter(storm::utility::vector::filterZero(this->getStateRewardVector()));
}
} else {
if (this->hasStateRewards()) {
result = transitionMatrix.getRowIndicesOfRowGroups(storm::utility::vector::filterZero(this->getStateRewardVector()));
result = transitionMatrix.getRowFilter(storm::utility::vector::filterZero(this->getStateRewardVector()));
} else {
result = storm::storage::BitVector(transitionMatrix.getRowCount(), true);
}

Loading…
Cancel
Save