Browse Source

needed to add some utility::vector::toString(...)s

Former-commit-id: f61d69ff9c
tempestpy_adaptions
TimQu 9 years ago
parent
commit
33e99b7b93
  1. 6
      src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp
  2. 4
      src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp

6
src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp

@ -201,7 +201,7 @@ namespace storm {
template <class SparseModelType, typename RationalNumberType> template <class SparseModelType, typename RationalNumberType>
typename SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::WeightVector SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::findSeparatingVector(Point const& pointToBeSeparated, std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> const& underApproximation, storm::storage::BitVector& individualObjectivesToBeChecked) { typename SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::WeightVector SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::findSeparatingVector(Point const& pointToBeSeparated, std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> const& underApproximation, storm::storage::BitVector& individualObjectivesToBeChecked) {
STORM_LOG_DEBUG("Searching a weight vector to seperate the point given by " << storm::utility::vector::convertNumericVector<double>(pointToBeSeparated) << ".");
STORM_LOG_DEBUG("Searching a weight vector to seperate the point given by " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(pointToBeSeparated)) << ".");
if(underApproximation->isEmpty()) { if(underApproximation->isEmpty()) {
// In this case, every weight vector is separating // In this case, every weight vector is separating
@ -238,7 +238,7 @@ namespace storm {
} }
STORM_LOG_THROW(farestHalfspaceIndex<halfspaces.size(), storm::exceptions::UnexpectedException, "There is no seperating vector."); STORM_LOG_THROW(farestHalfspaceIndex<halfspaces.size(), storm::exceptions::UnexpectedException, "There is no seperating vector.");
STORM_LOG_DEBUG("Found separating weight vector: " << storm::utility::vector::convertNumericVector<double>(halfspaces[farestHalfspaceIndex].normalVector()) << ".");
STORM_LOG_DEBUG("Found separating weight vector: " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(halfspaces[farestHalfspaceIndex].normalVector())) << ".");
return halfspaces[farestHalfspaceIndex].normalVector(); return halfspaces[farestHalfspaceIndex].normalVector();
} }
@ -267,7 +267,7 @@ namespace storm {
// Reset the precision back to the previous values // Reset the precision back to the previous values
weightVectorChecker->setMaximumLowerUpperBoundGap(*oldMaximumLowerUpperBoundGap); weightVectorChecker->setMaximumLowerUpperBoundGap(*oldMaximumLowerUpperBoundGap);
} }
STORM_LOG_DEBUG("weighted objectives checker result (lower bounds) is " << storm::utility::vector::convertNumericVector<double>(weightVectorChecker->getLowerBoundsOfInitialStateResults()));
STORM_LOG_DEBUG("weighted objectives checker result (lower bounds) is " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(weightVectorChecker->getLowerBoundsOfInitialStateResults())));
if(saveScheduler) { if(saveScheduler) {
result.refinementSteps().emplace_back(direction, result.refinementSteps().emplace_back(direction,

4
src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp

@ -36,7 +36,7 @@ namespace storm {
template <class SparseModelType> template <class SparseModelType>
void SparseMultiObjectiveWeightVectorChecker<SparseModelType>::check(std::vector<ValueType> const& weightVector) { void SparseMultiObjectiveWeightVectorChecker<SparseModelType>::check(std::vector<ValueType> const& weightVector) {
checkHasBeenCalled=true; checkHasBeenCalled=true;
STORM_LOG_DEBUG("Invoked WeightVectorChecker with weights " << std::endl << "\t" << storm::utility::vector::convertNumericVector<double>(weightVector));
STORM_LOG_DEBUG("Invoked WeightVectorChecker with weights " << std::endl << "\t" << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(weightVector)));
std::vector<ValueType> weightedRewardVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>()); std::vector<ValueType> weightedRewardVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>());
for(auto objIndex : objectivesWithNoUpperTimeBound) { for(auto objIndex : objectivesWithNoUpperTimeBound) {
storm::utility::vector::addScaledVector(weightedRewardVector, discreteActionRewards[objIndex], weightVector[objIndex]); storm::utility::vector::addScaledVector(weightedRewardVector, discreteActionRewards[objIndex], weightVector[objIndex]);
@ -50,7 +50,7 @@ namespace storm {
break; break;
} }
} }
STORM_LOG_DEBUG("Weight vector check done. Lower bounds for results in initial state: " << storm::utility::vector::convertNumericVector<double>(getLowerBoundsOfInitialStateResults()));
STORM_LOG_DEBUG("Weight vector check done. Lower bounds for results in initial state: " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(getLowerBoundsOfInitialStateResults())));
} }
template <class SparseModelType> template <class SparseModelType>

Loading…
Cancel
Save