sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Fixed minor pcaa bugs that were introduced due to recent changes

tempestpy_adaptions
TimQu 8 years ago
parent
d15348ab80
commit
e70f7716fe
2 changed files with 65 additions and 67 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 16
      src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp
  2. 116
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp

16
src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp
View File

@ -358,14 +358,10 @@ namespace storm {
// compute a choice vector for the probabilistic states that is optimal w.r.t. the weighted reward vector
minMax.solver->solveEquations(PS.weightedSolutionVector, minMax.b);
auto newScheduler = minMax.solver->getScheduler();
if(consideredObjectives.getNumberOfSetBits() == 1 && !storm::utility::isZero(weightVector[*consideredObjectives.begin()])) {
if(consideredObjectives.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*consideredObjectives.begin()])) {
// In this case there is no need to perform the computation on the individual objectives
optimalChoicesAtCurrentEpoch = newScheduler->getChoices();
auto objIndex = *consideredObjectives.begin();
PS.objectiveSolutionVectors[objIndex] = PS.weightedSolutionVector;
if(!storm::utility::isOne(weightVector[objIndex])) {
storm::utility::vector::scaleVectorInPlace(PS.objectiveSolutionVectors[objIndex], storm::utility::one<ValueType>()/weightVector[objIndex]);
}
PS.objectiveSolutionVectors[*consideredObjectives.begin()] = PS.weightedSolutionVector;
} else {
// check whether the linEqSolver needs to be updated, i.e., whether the scheduler has changed
if(linEq.solver == nullptr || newScheduler->getChoices() != optimalChoicesAtCurrentEpoch) {
@ -407,13 +403,9 @@ namespace storm {
storm::utility::vector::addVectors(MS.weightedRewardVector, MS.auxChoiceValues, MS.weightedSolutionVector);
MS.toPS.multiplyWithVector(PS.weightedSolutionVector, MS.auxChoiceValues);
storm::utility::vector::addVectors(MS.weightedSolutionVector, MS.auxChoiceValues, MS.weightedSolutionVector);
if(consideredObjectives.getNumberOfSetBits() == 1 && !storm::utility::isZero(weightVector[*consideredObjectives.begin()])) {
if(consideredObjectives.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*consideredObjectives.begin()])) {
// In this case there is no need to perform the computation on the individual objectives
auto objIndex = *consideredObjectives.begin();
MS.objectiveSolutionVectors[objIndex] = MS.weightedSolutionVector;
if(!storm::utility::isOne(weightVector[objIndex])) {
storm::utility::vector::scaleVectorInPlace(MS.objectiveSolutionVectors[objIndex], storm::utility::one<ValueType>()/weightVector[objIndex]);
}
MS.objectiveSolutionVectors[*consideredObjectives.begin()] = MS.weightedSolutionVector;
} else {
for(auto objIndex : consideredObjectives) {
MS.toMS.multiplyWithVector(MS.objectiveSolutionVectors[objIndex], MS.auxChoiceValues);

116
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp
View File

@ -158,65 +158,71 @@ namespace storm {
template <class SparseModelType>
void SparsePcaaWeightVectorChecker<SparseModelType>::unboundedIndividualPhase(std::vector<ValueType> const& weightVector) {
if(objectivesWithNoUpperTimeBound.getNumberOfSetBits()==1) {
auto objIndex = *objectivesWithNoUpperTimeBound.begin();
objectiveResults[objIndex] = weightedResult;
if(!storm::utility::isZero(weightVector[objIndex])) {
storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], storm::utility::one<ValueType>()/weightVector[objIndex]);
}
if(objectivesWithNoUpperTimeBound.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*objectivesWithNoUpperTimeBound.begin()])) {
objectiveResults[*objectivesWithNoUpperTimeBound.begin()] = weightedResult;
for (uint_fast64_t objIndex2 = 0; objIndex2 < objectives.size(); ++objIndex2) {
if(objIndex != objIndex2) {
if(*objectivesWithNoUpperTimeBound.begin() != objIndex2) {
objectiveResults[objIndex2] = std::vector<ValueType>(model.getNumberOfStates(), storm::utility::zero<ValueType>());
}
}
} else {
storm::storage::SparseMatrix<ValueType> deterministicMatrix = model.getTransitionMatrix().selectRowsFromRowGroups(this->scheduler.getChoices(), true);
storm::storage::SparseMatrix<ValueType> deterministicBackwardTransitions = deterministicMatrix.transpose();
std::vector<ValueType> deterministicStateRewards(deterministicMatrix.getRowCount());
storm::solver::GeneralLinearEquationSolverFactory<ValueType> linearEquationSolverFactory;
// We compute an estimate for the results of the individual objectives which is obtained from the weighted result and the result of the objectives computed so far.
// Note that weightedResult = Sum_{i=1}^{n} w_i * objectiveResult_i.
std::vector<ValueType> weightedSumOfUncheckedObjectives = weightedResult;
ValueType sumOfWeightsOfUncheckedObjectives = storm::utility::vector::sum_if(weightVector, objectivesWithNoUpperTimeBound);
for(uint_fast64_t const& objIndex : storm::utility::vector::getSortedIndices(weightVector)) {
if(objectivesWithNoUpperTimeBound.get(objIndex)){
offsetsToLowerBound[objIndex] = storm::utility::zero<ValueType>();
offsetsToUpperBound[objIndex] = storm::utility::zero<ValueType>();
storm::utility::vector::selectVectorValues(deterministicStateRewards, this->scheduler.getChoices(), model.getTransitionMatrix().getRowGroupIndices(), discreteActionRewards[objIndex]);
storm::storage::BitVector statesWithRewards = ~storm::utility::vector::filterZero(deterministicStateRewards);
// As target states, we pick the states from which no reward is reachable.
storm::storage::BitVector targetStates = ~storm::utility::graph::performProbGreater0(deterministicBackwardTransitions, storm::storage::BitVector(deterministicMatrix.getRowCount(), true), statesWithRewards);
// Compute the estimate for this objective
if(!storm::utility::isZero(weightVector[objIndex])) {
objectiveResults[objIndex] = weightedSumOfUncheckedObjectives;
storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], storm::utility::one<ValueType>() / sumOfWeightsOfUncheckedObjectives);
}
// Make sure that the objectiveResult is initialized in some way
objectiveResults[objIndex].resize(model.getNumberOfStates(), storm::utility::zero<ValueType>());
// Invoke the linear equation solver
objectiveResults[objIndex] = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeReachabilityRewards(deterministicMatrix,
deterministicBackwardTransitions,
deterministicStateRewards,
targetStates,
false, //no qualitative checking,
linearEquationSolverFactory,
objectiveResults[objIndex]);
// Update the estimate for the next objectives.
if(!storm::utility::isZero(weightVector[objIndex])) {
storm::utility::vector::addScaledVector(weightedSumOfUncheckedObjectives, objectiveResults[objIndex], -weightVector[objIndex]);
sumOfWeightsOfUncheckedObjectives -= weightVector[objIndex];
}
} else {
objectiveResults[objIndex] = std::vector<ValueType>(model.getNumberOfStates(), storm::utility::zero<ValueType>());
}
}
}
} else {
storm::storage::SparseMatrix<ValueType> deterministicMatrix = model.getTransitionMatrix().selectRowsFromRowGroups(this->scheduler.getChoices(), true);
storm::storage::SparseMatrix<ValueType> deterministicBackwardTransitions = deterministicMatrix.transpose();
std::vector<ValueType> deterministicStateRewards(deterministicMatrix.getRowCount());
storm::solver::GeneralLinearEquationSolverFactory<ValueType> linearEquationSolverFactory;
// We compute an estimate for the results of the individual objectives which is obtained from the weighted result and the result of the objectives computed so far.
// Note that weightedResult = Sum_{i=1}^{n} w_i * objectiveResult_i.
std::vector<ValueType> weightedSumOfUncheckedObjectives = weightedResult;
ValueType sumOfWeightsOfUncheckedObjectives = storm::utility::vector::sum_if(weightVector, objectivesWithNoUpperTimeBound);
for (uint_fast64_t const &objIndex : storm::utility::vector::getSortedIndices(weightVector)) {
if (objectivesWithNoUpperTimeBound.get(objIndex)) {
offsetsToLowerBound[objIndex] = storm::utility::zero<ValueType>();
offsetsToUpperBound[objIndex] = storm::utility::zero<ValueType>();
storm::utility::vector::selectVectorValues(deterministicStateRewards, this->scheduler.getChoices(), model.getTransitionMatrix().getRowGroupIndices(), discreteActionRewards[objIndex]);
storm::storage::BitVector statesWithRewards = ~storm::utility::vector::filterZero(deterministicStateRewards);
// As maybestates we pick the states from which a state with reward is reachable
storm::storage::BitVector maybeStates = storm::utility::graph::performProbGreater0(deterministicBackwardTransitions, storm::storage::BitVector(deterministicMatrix.getRowCount(), true), statesWithRewards);
// Compute the estimate for this objective
if (!storm::utility::isZero(weightVector[objIndex])) {
objectiveResults[objIndex] = weightedSumOfUncheckedObjectives;
storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], storm::utility::one<ValueType>() / sumOfWeightsOfUncheckedObjectives);
}
// Make sure that the objectiveResult is initialized correctly
objectiveResults[objIndex].resize(model.getNumberOfStates(), storm::utility::zero<ValueType>());
if (!maybeStates.empty()) {
storm::storage::SparseMatrix<ValueType> submatrix = deterministicMatrix.getSubmatrix(
true, maybeStates, maybeStates, true);
// Converting the matrix from the fixpoint notation to the form needed for the equation
// system. That is, we go from x = A*x + b to (I-A)x = b.
submatrix.convertToEquationSystem();
// Prepare solution vector and rhs of the equation system.
std::vector<ValueType> x = storm::utility::vector::filterVector(objectiveResults[objIndex], maybeStates);
std::vector<ValueType> b = storm::utility::vector::filterVector(deterministicStateRewards, maybeStates);
// Now solve the resulting equation system.
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(std::move(submatrix));
solver->solveEquations(x, b);
// Set the result for this objective accordingly
storm::utility::vector::setVectorValues<ValueType>(objectiveResults[objIndex], maybeStates, x);
storm::utility::vector::setVectorValues<ValueType>(objectiveResults[objIndex], ~maybeStates, storm::utility::zero<ValueType>());
}
// Update the estimate for the next objectives.
if (!storm::utility::isZero(weightVector[objIndex])) {
storm::utility::vector::addScaledVector(weightedSumOfUncheckedObjectives, objectiveResults[objIndex], -weightVector[objIndex]);
sumOfWeightsOfUncheckedObjectives -= weightVector[objIndex];
}
} else {
objectiveResults[objIndex] = std::vector<ValueType>(model.getNumberOfStates(), storm::utility::zero<ValueType>());
}
}
}
}
template <class SparseModelType>

Write Preview
Loading…
Cancel
Save