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

clean up single objective reward bounded case

tempestpy_adaptions
TimQu 7 years ago
parent
016fedd58e
commit
117d1b5c99
4 changed files with 120 additions and 121 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. 12
      src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
  2. 10
      src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp
  3. 20
      src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h
  4. 199
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

12
src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
View File

@ -49,17 +49,7 @@ namespace storm {
auto initEpoch = rewardUnfolding.getStartEpoch();
auto epochOrder = rewardUnfolding.getEpochComputationOrder(initEpoch);
EpochCheckingData cachedData;
ValueType precision = storm::utility::convertNumber<ValueType>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
uint64_t epochCount = 0;
for (uint64_t dim = 0; dim < rewardUnfolding.getEpochManager().getDimensionCount(); ++dim) {
epochCount += rewardUnfolding.getEpochManager().getDimensionOfEpoch(initEpoch, dim) + 1;
}
if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isSoundSet()) {
precision = precision / storm::utility::convertNumber<ValueType>(epochCount);
}
if (numChecks == 1) {
STORM_PRINT_AND_LOG("Objective/Dimension/Epoch count is: " << this->objectives.size() << "/" << rewardUnfolding.getEpochManager().getDimensionCount() << "/" << epochOrder.size() << "." << std::endl);
}
ValueType precision = rewardUnfolding.getRequiredEpochModelPrecision(initEpoch, storm::utility::convertNumber<ValueType>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()));
storm::utility::ProgressMeasurement progress("epochs");
progress.setMaxCount(epochOrder.size());

10
src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp
View File

@ -537,6 +537,16 @@ namespace storm {
return stringstream.str();
}
template<typename ValueType, bool SingleObjectiveMode>
ValueType MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getRequiredEpochModelPrecision(Epoch const& startEpoch, ValueType const& precision) {
// if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isSoundSet()) {
uint64_t sumOfDimensions = 0;
for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) {
sumOfDimensions += epochManager.getDimensionOfEpoch(startEpoch, dim) + 1;
}
return precision / storm::utility::convertNumber<ValueType>(sumOfDimensions);
}
template<typename ValueType, bool SingleObjectiveMode>
void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::setSolutionForCurrentEpoch(std::vector<SolutionType>&& inStateSolutions) {
STORM_LOG_ASSERT(currentEpoch, "Tried to set a solution for the current epoch, but no epoch was specified before.");

20
src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h
View File

@ -46,25 +46,18 @@ namespace storm {
MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp<ValueType> const& model, std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives);
MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp<ValueType> const& model, std::shared_ptr<storm::logic::OperatorFormula const> objectiveFormula);
~MultiDimensionalRewardUnfolding() {
std::cout << "Implicit unfolding statistics: " << std::endl;
std::cout << " Memory Product size: " << productModel->getProduct().getNumberOfStates() << std::endl;
std::cout << " maxSolutionsStored: " << maxSolutionsStored << std::endl;
std::cout << "Occurring Epoch model sizes: ";
for (auto const& i : epochModelSizes) {
std::cout << i << " ";
}
std::cout << std::endl;
std::cout << "---------------------------------------------" << std::endl;
std::cout << std::endl;
}
~MultiDimensionalRewardUnfolding() = default;
Epoch getStartEpoch();
std::vector<Epoch> getEpochComputationOrder(Epoch const& startEpoch);
EpochModel& setCurrentEpoch(Epoch const& epoch);
/*!
* Returns the precision required for the analyzis of each epoch model in order to achieve the given overall precision
*/
ValueType getRequiredEpochModelPrecision(Epoch const& startEpoch, ValueType const& precision);
void setSolutionForCurrentEpoch(std::vector<SolutionType>&& inStateSolutions);
SolutionType const& getInitialStateResult(Epoch const& epoch); // Assumes that the initial state is unique
SolutionType const& getInitialStateResult(Epoch const& epoch, uint64_t initialStateIndex);
@ -79,7 +72,6 @@ namespace storm {
void initializeObjectives(std::vector<Epoch>& epochSteps);
void computeMaxDimensionValues();
void initializeMemoryProduct(std::vector<Epoch> const& epochSteps);

199
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
View File

@ -82,6 +82,105 @@ namespace storm {
return result;
}
template<typename ValueType>
std::vector<ValueType> analyzeTrivialEpochModel(OptimizationDirection dir, typename storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding<ValueType, true>::EpochModel& epochModel) {
// Assert that the epoch model is indeed trivial
assert(epochModel.epochMatrix.getEntryCount() == 0);
std::vector<ValueType> epochResult;
epochResult.reserve(epochModel.epochInStates.getNumberOfSetBits());
auto stepSolutionIt = epochModel.stepSolutions.begin();
auto stepChoiceIt = epochModel.stepChoices.begin();
for (auto const& state : epochModel.epochInStates) {
// Obtain the best choice for this state
ValueType bestValue;
uint64_t lastChoice = epochModel.epochMatrix.getRowGroupIndices()[state + 1];
bool isFirstChoice = true;
for (uint64_t choice = epochModel.epochMatrix.getRowGroupIndices()[state]; choice < lastChoice; ++choice) {
while (*stepChoiceIt < choice) {
++stepChoiceIt;
++stepSolutionIt;
}
ValueType choiceValue = storm::utility::zero<ValueType>();
if (epochModel.objectiveRewardFilter.front().get(choice)) {
choiceValue += epochModel.objectiveRewards.front()[choice];
}
if (*stepChoiceIt == choice) {
choiceValue += *stepSolutionIt;
}
if (isFirstChoice) {
bestValue = std::move(choiceValue);
isFirstChoice = false;
} else {
if (storm::solver::minimize(dir)) {
if (choiceValue < bestValue) {
bestValue = std::move(choiceValue);
}
} else {
if (choiceValue > bestValue) {
bestValue = std::move(choiceValue);
}
}
}
}
// Insert the solution w.r.t. this choice
epochResult.push_back(std::move(bestValue));
}
return epochResult;
}
template<typename ValueType>
std::vector<ValueType> analyzeNonTrivialEpochModel(OptimizationDirection dir, typename storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding<ValueType, true>::EpochModel& epochModel, std::vector<ValueType>& x, std::vector<ValueType>& b, std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>& minMaxSolver, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ValueType const& precision, SolutionType const& type) {
// Update some data for the case that the Matrix has changed
if (epochModel.epochMatrixChanged) {
x.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
minMaxSolver = minMaxLinearEquationSolverFactory.create(epochModel.epochMatrix);
minMaxSolver->setHasUniqueSolution();
minMaxSolver->setPrecision(precision);
minMaxSolver->setOptimizationDirection(dir);
minMaxSolver->setCachingEnabled(true);
minMaxSolver->setTrackScheduler(true);
auto req = minMaxSolver->getRequirements(dir);
minMaxSolver->setLowerBound(storm::utility::zero<ValueType>());
req.clearLowerBounds();
if (type == SolutionType::UntilProbabilities) {
minMaxSolver->setUpperBound(storm::utility::one<ValueType>());
req.clearUpperBounds();
} else if (type == SolutionType::ExpectedRewards) {
// TODO
STORM_LOG_WARN_COND(!req.requiresUpperBounds(), "Upper bounds for expected reward are not specified.");
}
STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked.");
minMaxSolver->setRequirementsChecked();
} else {
auto choicesTmp = minMaxSolver->getSchedulerChoices();
minMaxSolver->setInitialScheduler(std::move(choicesTmp));
}
// Prepare the right hand side of the equation system
b.assign(epochModel.epochMatrix.getRowCount(), storm::utility::zero<ValueType>());
std::vector<ValueType> const& objectiveValues = epochModel.objectiveRewards.front();
for (auto const& choice : epochModel.objectiveRewardFilter.front()) {
b[choice] = objectiveValues[choice];
}
auto stepSolutionIt = epochModel.stepSolutions.begin();
for (auto const& choice : epochModel.stepChoices) {
b[choice] += *stepSolutionIt;
++stepSolutionIt;
}
assert(stepSolutionIt == epochModel.stepSolutions.end());
// Solve the minMax equation system
minMaxSolver->solveEquations(x, b);
return storm::utility::vector::filterVector(x, epochModel.epochInStates);
}
template<typename ValueType>
std::map<storm::storage::sparse::state_type, ValueType> SparseMdpPrctlHelper<ValueType>::computeRewardBoundedValues(SolutionType const& type, OptimizationDirection dir, storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding<ValueType, true>& rewardUnfolding, storm::storage::BitVector const& initialStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
storm::utility::Stopwatch swAll(true), swBuild, swCheck;
@ -92,14 +191,8 @@ namespace storm {
std::vector<ValueType> x, b;
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> minMaxSolver;
ValueType precision = storm::utility::convertNumber<ValueType>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
uint64_t epochCount = 0;
for (uint64_t dim = 0; dim < rewardUnfolding.getEpochManager().getDimensionCount(); ++dim) {
epochCount += rewardUnfolding.getEpochManager().getDimensionOfEpoch(initEpoch, dim) + 1;
}
if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isSoundSet()) {
precision = precision / storm::utility::convertNumber<ValueType>(epochCount);
}
ValueType precision = rewardUnfolding.getRequiredEpochModelPrecision(initEpoch, storm::utility::convertNumber<ValueType>(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision()));
storm::utility::ProgressMeasurement progress("epochs");
progress.setMaxCount(epochOrder.size());
progress.startNewMeasurement(0);
@ -110,95 +203,9 @@ namespace storm {
swBuild.stop(); swCheck.start();
// If the epoch matrix is empty we do not need to solve a linear equation system
if (epochModel.epochMatrix.getEntryCount() == 0) {
std::vector<ValueType> epochResult;
epochResult.reserve(epochModel.epochInStates.getNumberOfSetBits());
auto stepSolutionIt = epochModel.stepSolutions.begin();
auto stepChoiceIt = epochModel.stepChoices.begin();
for (auto const& state : epochModel.epochInStates) {
// Obtain the best choice for this state
ValueType bestValue;
uint64_t lastChoice = epochModel.epochMatrix.getRowGroupIndices()[state + 1];
bool isFirstChoice = true;
for (uint64_t choice = epochModel.epochMatrix.getRowGroupIndices()[state]; choice < lastChoice; ++choice) {
while (*stepChoiceIt < choice) {
++stepChoiceIt;
++stepSolutionIt;
}
ValueType choiceValue = storm::utility::zero<ValueType>();
if (epochModel.objectiveRewardFilter.front().get(choice)) {
choiceValue += epochModel.objectiveRewards.front()[choice];
}
if (*stepChoiceIt == choice) {
choiceValue += *stepSolutionIt;
}
if (isFirstChoice) {
bestValue = std::move(choiceValue);
isFirstChoice = false;
} else {
if (storm::solver::minimize(dir)) {
if (choiceValue < bestValue) {
bestValue = std::move(choiceValue);
}
} else {
if (choiceValue > bestValue) {
bestValue = std::move(choiceValue);
}
}
}
}
// Insert the solution w.r.t. this choice
epochResult.push_back(std::move(bestValue));
}
rewardUnfolding.setSolutionForCurrentEpoch(std::move(epochResult));
rewardUnfolding.setSolutionForCurrentEpoch(analyzeTrivialEpochModel<ValueType>(dir, epochModel));
} else {
// Update some data for the case that the Matrix has changed
if (epochModel.epochMatrixChanged) {
x.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
minMaxSolver = minMaxLinearEquationSolverFactory.create(epochModel.epochMatrix);
minMaxSolver->setHasUniqueSolution();
minMaxSolver->setPrecision(precision);
minMaxSolver->setOptimizationDirection(dir);
minMaxSolver->setCachingEnabled(true);
minMaxSolver->setTrackScheduler(true);
auto req = minMaxSolver->getRequirements(dir);
minMaxSolver->setLowerBound(storm::utility::zero<ValueType>());
req.clearLowerBounds();
if (type == SolutionType::UntilProbabilities) {
minMaxSolver->setUpperBound(storm::utility::one<ValueType>());
req.clearUpperBounds();
} else if (type == SolutionType::ExpectedRewards) {
// TODO
STORM_LOG_WARN_COND(!req.requiresUpperBounds(), "Upper bounds for expected reward are not specified.");
}
STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked.");
minMaxSolver->setRequirementsChecked();
} else {
auto choicesTmp = minMaxSolver->getSchedulerChoices();
minMaxSolver->setInitialScheduler(std::move(choicesTmp));
}
// Prepare the right hand side of the equation system
b.assign(epochModel.epochMatrix.getRowCount(), storm::utility::zero<ValueType>());
std::vector<ValueType> const& objectiveValues = epochModel.objectiveRewards.front();
for (auto const& choice : epochModel.objectiveRewardFilter.front()) {
b[choice] = objectiveValues[choice];
}
auto stepSolutionIt = epochModel.stepSolutions.begin();
for (auto const& choice : epochModel.stepChoices) {
b[choice] += *stepSolutionIt;
++stepSolutionIt;
}
assert(stepSolutionIt == epochModel.stepSolutions.end());
// Solve the minMax equation system
minMaxSolver->solveEquations(x, b);
// Plug in the result into the reward unfolding
rewardUnfolding.setSolutionForCurrentEpoch(storm::utility::vector::filterVector(x, epochModel.epochInStates));
rewardUnfolding.setSolutionForCurrentEpoch(analyzeNonTrivialEpochModel<ValueType>(dir, epochModel, x, b, minMaxSolver, minMaxLinearEquationSolverFactory, precision, type));
}
swCheck.stop();
++numCheckedEpochs;

Write Preview
Loading…
Cancel
Save