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

rewardbounded: Moved epoch model analysis to a separate file.

main
Tim Quatmann 6 years ago
parent
661d922d2e
commit
82402ba3ae
8 changed files with 312 additions and 204 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. 2
      src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp
  2. 2
      src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.h
  3. 79
      src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
  4. 105
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  5. 248
      src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp
  6. 48
      src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.h
  7. 8
      src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp
  8. 24
      src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h

2
src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp
View File

@ -309,7 +309,7 @@ namespace storm {
}
template <class SparseMdpModelType>
void RewardBoundedMdpPcaaWeightVectorChecker<SparseMdpModelType>::updateCachedData(Environment const& env, typename helper::rewardbounded::MultiDimensionalRewardUnfolding<ValueType, false>::EpochModel const& epochModel, EpochCheckingData& cachedData, std::vector<ValueType> const& weightVector) {
void RewardBoundedMdpPcaaWeightVectorChecker<SparseMdpModelType>::updateCachedData(Environment const& env, helper::rewardbounded::EpochModel<ValueType, false> const& epochModel, EpochCheckingData& cachedData, std::vector<ValueType> const& weightVector) {
if (epochModel.epochMatrixChanged) {
// Update the cached MinMaxSolver data

2
src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.h
View File

@ -64,7 +64,7 @@ namespace storm {
void computeEpochSolution(Environment const& env, typename helper::rewardbounded::MultiDimensionalRewardUnfolding<ValueType, false>::Epoch const& epoch, std::vector<ValueType> const& weightVector, EpochCheckingData& cachedData);
void updateCachedData(Environment const& env, typename helper::rewardbounded::MultiDimensionalRewardUnfolding<ValueType, false>::EpochModel const& epochModel, EpochCheckingData& cachedData, std::vector<ValueType> const& weightVector);
void updateCachedData(Environment const& env, typename helper::rewardbounded::EpochModel<ValueType, false> const& epochModel, EpochCheckingData& cachedData, std::vector<ValueType> const& weightVector);
storm::utility::Stopwatch swAll, swEpochModelBuild, swEpochModelAnalysis;
uint64_t numCheckedEpochs, numChecks;

79
src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
View File

@ -81,75 +81,6 @@ namespace storm {
return result;
}
template<typename ValueType>
std::vector<ValueType> analyzeTrivialDtmcEpochModel(typename rewardbounded::MultiDimensionalRewardUnfolding<ValueType, true>::EpochModel& epochModel) {
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) {
while (*stepChoiceIt < state) {
++stepChoiceIt;
++stepSolutionIt;
}
if (epochModel.objectiveRewardFilter.front().get(state)) {
if (*stepChoiceIt == state) {
epochResult.push_back(epochModel.objectiveRewards.front()[state] + *stepSolutionIt);
} else {
epochResult.push_back(epochModel.objectiveRewards.front()[state]);
}
} else {
if (*stepChoiceIt == state) {
epochResult.push_back(*stepSolutionIt);
} else {
epochResult.push_back(storm::utility::zero<ValueType>());
}
}
}
return epochResult;
}
template<typename ValueType>
std::vector<ValueType> analyzeNonTrivialDtmcEpochModel(Environment const& env, typename rewardbounded::MultiDimensionalRewardUnfolding<ValueType, true>::EpochModel& epochModel, std::vector<ValueType>& x, std::vector<ValueType>& b, std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>>& linEqSolver, boost::optional<ValueType> const& lowerBound, boost::optional<ValueType> const& upperBound) {
// Update some data for the case that the Matrix has changed
if (epochModel.epochMatrixChanged) {
x.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
storm::solver::GeneralLinearEquationSolverFactory<ValueType> linearEquationSolverFactory;
linEqSolver = linearEquationSolverFactory.create(env, epochModel.epochMatrix);
linEqSolver->setCachingEnabled(true);
auto req = linEqSolver->getRequirements(env);
if (lowerBound) {
linEqSolver->setLowerBound(lowerBound.get());
req.clearLowerBounds();
}
if (upperBound) {
linEqSolver->setUpperBound(upperBound.get());
req.clearUpperBounds();
}
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
}
// 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
linEqSolver->solveEquations(env, x, b);
return storm::utility::vector::filterVector(x, epochModel.epochInStates);
}
template<>
std::map<storm::storage::sparse::state_type, storm::RationalFunction> SparseDtmcPrctlHelper<storm::RationalFunction>::computeRewardBoundedValues(Environment const& env, storm::models::sparse::Dtmc<storm::RationalFunction> const& model, std::shared_ptr<storm::logic::OperatorFormula const> rewardBoundedFormula) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The specified property is not supported by this value type.");
@ -184,8 +115,7 @@ namespace storm {
// Set the correct equation problem format.
storm::solver::GeneralLinearEquationSolverFactory<ValueType> linearEquationSolverFactory;
rewardUnfolding.setEquationSystemFormatForEpochModel(linearEquationSolverFactory.getEquationProblemFormat(preciseEnv));
bool convertToEquationSystem = linearEquationSolverFactory.getEquationProblemFormat(preciseEnv) == solver::LinearEquationSolverProblemFormat::EquationSystem;
storm::utility::ProgressMeasurement progress("epochs");
progress.setMaxCount(epochOrder.size());
progress.startNewMeasurement(0);
@ -194,12 +124,7 @@ namespace storm {
swBuild.start();
auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch);
swBuild.stop(); swCheck.start();
// If the epoch matrix is empty we do not need to solve a linear equation system
if ((convertToEquationSystem && epochModel.epochMatrix.isIdentityMatrix()) || (!convertToEquationSystem && epochModel.epochMatrix.getEntryCount() == 0)) {
rewardUnfolding.setSolutionForCurrentEpoch(analyzeTrivialDtmcEpochModel<ValueType>(epochModel));
} else {
rewardUnfolding.setSolutionForCurrentEpoch(analyzeNonTrivialDtmcEpochModel<ValueType>(preciseEnv, epochModel, x, b, linEqSolver, lowerBound, upperBound));
}
rewardUnfolding.setSolutionForCurrentEpoch(epochModel.analyzeSingleObjective(preciseEnv, x, b, linEqSolver, lowerBound, upperBound));
swCheck.stop();
if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExportCdfSet() && !rewardUnfolding.getEpochManager().hasBottomDimension(epoch)) {
std::vector<ValueType> cdfEntry;

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

@ -90,103 +90,7 @@ namespace storm {
return result;
}
template<typename ValueType>
std::vector<ValueType> analyzeTrivialMdpEpochModel(OptimizationDirection dir, typename rewardbounded::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> analyzeNonTrivialMdpEpochModel(Environment const& env, OptimizationDirection dir, typename rewardbounded::MultiDimensionalRewardUnfolding<ValueType, true>::EpochModel& epochModel, std::vector<ValueType>& x, std::vector<ValueType>& b, std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>& minMaxSolver, boost::optional<ValueType> const& lowerBound, boost::optional<ValueType> const& upperBound) {
// Update some data for the case that the Matrix has changed
if (epochModel.epochMatrixChanged) {
x.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory;
minMaxSolver = minMaxLinearEquationSolverFactory.create(env, epochModel.epochMatrix);
minMaxSolver->setHasUniqueSolution();
minMaxSolver->setOptimizationDirection(dir);
minMaxSolver->setCachingEnabled(true);
minMaxSolver->setTrackScheduler(true);
auto req = minMaxSolver->getRequirements(env, dir, false);
if (lowerBound) {
minMaxSolver->setLowerBound(lowerBound.get());
req.clearLowerBounds();
}
if (upperBound) {
minMaxSolver->setUpperBound(upperBound.get());
req.clearUpperBounds();
}
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " 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(env, x, b);
return storm::utility::vector::filterVector(x, epochModel.epochInStates);
}
template<typename ValueType>
std::map<storm::storage::sparse::state_type, ValueType> SparseMdpPrctlHelper<ValueType>::computeRewardBoundedValues(Environment const& env, OptimizationDirection dir, rewardbounded::MultiDimensionalRewardUnfolding<ValueType, true>& rewardUnfolding, storm::storage::BitVector const& initialStates) {
storm::utility::Stopwatch swAll(true), swBuild, swCheck;
@ -218,12 +122,7 @@ namespace storm {
swBuild.start();
auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch);
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) {
rewardUnfolding.setSolutionForCurrentEpoch(analyzeTrivialMdpEpochModel<ValueType>(dir, epochModel));
} else {
rewardUnfolding.setSolutionForCurrentEpoch(analyzeNonTrivialMdpEpochModel<ValueType>(preciseEnv, dir, epochModel, x, b, minMaxSolver, lowerBound, upperBound));
}
rewardUnfolding.setSolutionForCurrentEpoch(epochModel.analyzeSingleObjective(preciseEnv, dir, x, b, minMaxSolver, lowerBound, upperBound));
swCheck.stop();
if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExportCdfSet() && !rewardUnfolding.getEpochManager().hasBottomDimension(epoch)) {
std::vector<ValueType> cdfEntry;

248
src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp
View File

@ -0,0 +1,248 @@
#include "storm/modelchecker/prctl/helper/rewardbounded/EpochModel.h"
#include "storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h"
#include "storm/exceptions/UncheckedRequirementException.h"
namespace storm {
namespace modelchecker {
namespace helper {
namespace rewardbounded {
template<typename ValueType>
std::vector<ValueType> analyzeTrivialDtmcEpochModel(EpochModel<ValueType, true>& epochModel) {
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) {
while (*stepChoiceIt < state) {
++stepChoiceIt;
++stepSolutionIt;
}
if (epochModel.objectiveRewardFilter.front().get(state)) {
if (*stepChoiceIt == state) {
epochResult.push_back(epochModel.objectiveRewards.front()[state] + *stepSolutionIt);
} else {
epochResult.push_back(epochModel.objectiveRewards.front()[state]);
}
} else {
if (*stepChoiceIt == state) {
epochResult.push_back(*stepSolutionIt);
} else {
epochResult.push_back(storm::utility::zero<ValueType>());
}
}
}
return epochResult;
}
template<typename ValueType>
std::vector<ValueType> analyzeNonTrivialDtmcEpochModel(Environment const& env, EpochModel<ValueType, true>& epochModel, std::vector<ValueType>& x, std::vector<ValueType>& b, std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>>& linEqSolver, boost::optional<ValueType> const& lowerBound, boost::optional<ValueType> const& upperBound) {
// Update some data for the case that the Matrix has changed
if (epochModel.epochMatrixChanged) {
x.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
storm::solver::GeneralLinearEquationSolverFactory<ValueType> linearEquationSolverFactory;
linEqSolver = linearEquationSolverFactory.create(env, epochModel.epochMatrix);
linEqSolver->setCachingEnabled(true);
auto req = linEqSolver->getRequirements(env);
if (lowerBound) {
linEqSolver->setLowerBound(lowerBound.get());
req.clearLowerBounds();
}
if (upperBound) {
linEqSolver->setUpperBound(upperBound.get());
req.clearUpperBounds();
}
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
}
// 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
linEqSolver->solveEquations(env, x, b);
return storm::utility::vector::filterVector(x, epochModel.epochInStates);
}
template<typename ValueType>
std::vector<ValueType> analyzeTrivialMdpEpochModel(OptimizationDirection dir, EpochModel<ValueType, true>& 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> analyzeNonTrivialMdpEpochModel(Environment const& env, OptimizationDirection dir, EpochModel<ValueType, true>& epochModel, std::vector<ValueType>& x, std::vector<ValueType>& b, std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>& minMaxSolver, boost::optional<ValueType> const& lowerBound, boost::optional<ValueType> const& upperBound) {
// Update some data for the case that the Matrix has changed
if (epochModel.epochMatrixChanged) {
x.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory;
minMaxSolver = minMaxLinearEquationSolverFactory.create(env, epochModel.epochMatrix);
minMaxSolver->setHasUniqueSolution();
minMaxSolver->setOptimizationDirection(dir);
minMaxSolver->setCachingEnabled(true);
minMaxSolver->setTrackScheduler(true);
auto req = minMaxSolver->getRequirements(env, dir, false);
if (lowerBound) {
minMaxSolver->setLowerBound(lowerBound.get());
req.clearLowerBounds();
}
if (upperBound) {
minMaxSolver->setUpperBound(upperBound.get());
req.clearUpperBounds();
}
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " 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(env, x, b);
return storm::utility::vector::filterVector(x, epochModel.epochInStates);
}
template<>
std::vector<double> EpochModel<double, true>::analyzeSingleObjective(
const storm::Environment &env, std::vector<double> &x, std::vector<double> &b,
std::unique_ptr<storm::solver::LinearEquationSolver<double>> &linEqSolver,
const boost::optional<double> &lowerBound, const boost::optional<double> &upperBound) {
STORM_LOG_ASSERT(epochMatrix.hasTrivialRowGrouping(), "This operation is only allowed if no nondeterminism is present.");
STORM_LOG_ASSERT(equationSolverProblemFormat.is_initialized(), "Unknown equation problem format.");
// If the epoch matrix is empty we do not need to solve a linear equation system
bool convertToEquationSystem = (equationSolverProblemFormat == storm::solver::LinearEquationSolverProblemFormat::EquationSystem);
if ((convertToEquationSystem && epochMatrix.isIdentityMatrix()) || (!convertToEquationSystem && epochMatrix.getEntryCount() == 0)) {
return analyzeTrivialDtmcEpochModel<double>(*this);
} else {
return analyzeNonTrivialDtmcEpochModel<double>(env, *this, x, b, linEqSolver, lowerBound, upperBound);
}
}
template<>
std::vector<double> EpochModel<double, true>::analyzeSingleObjective(
const storm::Environment &env, storm::OptimizationDirection dir, std::vector<double> &x,
std::vector<double> &b,
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<double>> &minMaxSolver,
const boost::optional<double> &lowerBound, const boost::optional<double> &upperBound) {
// If the epoch matrix is empty we do not need to solve a linear equation system
if (epochMatrix.getEntryCount() == 0) {
return analyzeTrivialMdpEpochModel<double>(dir, *this);
} else {
return analyzeNonTrivialMdpEpochModel<double>(env, dir, *this, x, b, minMaxSolver, lowerBound, upperBound);
}
}
template<>
std::vector<storm::RationalNumber> EpochModel<storm::RationalNumber, true>::analyzeSingleObjective(
const storm::Environment &env, std::vector<storm::RationalNumber> &x, std::vector<storm::RationalNumber> &b,
std::unique_ptr<storm::solver::LinearEquationSolver<storm::RationalNumber>> &linEqSolver,
const boost::optional<storm::RationalNumber> &lowerBound, const boost::optional<storm::RationalNumber> &upperBound) {
STORM_LOG_ASSERT(epochMatrix.hasTrivialRowGrouping(), "This operation is only allowed if no nondeterminism is present.");
STORM_LOG_ASSERT(equationSolverProblemFormat.is_initialized(), "Unknown equation problem format.");
// If the epoch matrix is empty we do not need to solve a linear equation system
bool convertToEquationSystem = (equationSolverProblemFormat == storm::solver::LinearEquationSolverProblemFormat::EquationSystem);
if ((convertToEquationSystem && epochMatrix.isIdentityMatrix()) || (!convertToEquationSystem && epochMatrix.getEntryCount() == 0)) {
return analyzeTrivialDtmcEpochModel<storm::RationalNumber>(*this);
} else {
return analyzeNonTrivialDtmcEpochModel<storm::RationalNumber>(env, *this, x, b, linEqSolver, lowerBound, upperBound);
}
}
template<>
std::vector<storm::RationalNumber> EpochModel<storm::RationalNumber, true>::analyzeSingleObjective(
const storm::Environment &env, storm::OptimizationDirection dir, std::vector<storm::RationalNumber> &x,
std::vector<storm::RationalNumber> &b,
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<storm::RationalNumber>> &minMaxSolver,
const boost::optional<storm::RationalNumber> &lowerBound, const boost::optional<storm::RationalNumber> &upperBound) {
// If the epoch matrix is empty we do not need to solve a linear equation system
if (epochMatrix.getEntryCount() == 0) {
return analyzeTrivialMdpEpochModel<storm::RationalNumber>(dir, *this);
} else {
return analyzeNonTrivialMdpEpochModel<storm::RationalNumber>(env, dir, *this, x, b, minMaxSolver, lowerBound, upperBound);
}
}
template class EpochModel<double, true>;
template class EpochModel<double, false>;
template class EpochModel<storm::RationalNumber, true>;
template class EpochModel<storm::RationalNumber, false>;
}
}
}
}

48
src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.h
View File

@ -0,0 +1,48 @@
#pragma once
#include <vector>
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/BitVector.h"
#include "storm/solver/LinearEquationSolverProblemFormat.h"
#include "storm/solver/OptimizationDirection.h"
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/solver/LinearEquationSolver.h"
namespace storm {
class Environment;
namespace modelchecker {
namespace helper {
namespace rewardbounded {
template<typename ValueType, bool SingleObjectiveMode>
struct EpochModel {
typedef typename std::conditional<SingleObjectiveMode, ValueType, std::vector < ValueType>>::type SolutionType;
bool epochMatrixChanged;
storm::storage::SparseMatrix<ValueType> epochMatrix;
storm::storage::BitVector stepChoices;
std::vector<SolutionType> stepSolutions;
std::vector<std::vector<ValueType>> objectiveRewards;
std::vector<storm::storage::BitVector> objectiveRewardFilter;
storm::storage::BitVector epochInStates;
/// In case of DTMCs we have different options for the equation problem format the epoch model will have.
boost::optional<storm::solver::LinearEquationSolverProblemFormat> equationSolverProblemFormat;
/*!
* Analyzes the epoch model, i.e., solves the represented equation system. This method assumes a nondeterministic model.
*/
std::vector<ValueType> analyzeSingleObjective(Environment const& env, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType>& b, std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>>& minMaxSolver, boost::optional<ValueType> const& lowerBound, boost::optional<ValueType> const& upperBound);
/*!
* Analyzes the epoch model, i.e., solves the represented equation system. This method assumes a deterministic model.
*/
std::vector<ValueType> analyzeSingleObjective(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType>& b, std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>>& linEqSolver, boost::optional<ValueType> const& lowerBound, boost::optional<ValueType> const& upperBound);
};
}
}
}
}

8
src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp
View File

@ -287,7 +287,7 @@ namespace storm {
}
template<typename ValueType, bool SingleObjectiveMode>
typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::EpochModel& MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::setCurrentEpoch(Epoch const& epoch) {
EpochModel<ValueType, SingleObjectiveMode>& MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::setCurrentEpoch(Epoch const& epoch) {
STORM_LOG_DEBUG("Setting model for epoch " << epochManager.toString(epoch));
// Check if we need to update the current epoch class
@ -446,8 +446,8 @@ namespace storm {
if (model.isOfType(storm::models::ModelType::Dtmc)) {
assert(zeroObjRewardChoices.size() == productModel->getProduct().getNumberOfStates());
assert(stepChoices.size() == productModel->getProduct().getNumberOfStates());
STORM_LOG_ASSERT(equationSolverProblemFormatForEpochModel.is_initialized(), "Linear equation problem format was not set.");
bool convertToEquationSystem = equationSolverProblemFormatForEpochModel.get() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem;
STORM_LOG_ASSERT(epochModel.equationSolverProblemFormat.is_initialized(), "Linear equation problem format was not set.");
bool convertToEquationSystem = epochModel.equationSolverProblemFormat.get() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem;
// For DTMCs we consider the subsystem induced by the considered states.
// The transitions for states with zero reward are filtered out to guarantee a unique solution of the eq-system.
auto backwardTransitions = epochModel.epochMatrix.transpose(true);
@ -547,7 +547,7 @@ namespace storm {
template<typename ValueType, bool SingleObjectiveMode>
void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::setEquationSystemFormatForEpochModel(storm::solver::LinearEquationSolverProblemFormat eqSysFormat) {
STORM_LOG_ASSERT(model.isOfType(storm::models::ModelType::Dtmc), "Trying to set the equation problem format although the model is not deterministic.");
equationSolverProblemFormatForEpochModel = eqSysFormat;
epochModel.equationSolverProblemFormat = eqSysFormat;
}

24
src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h
View File

@ -6,6 +6,7 @@
#include "storm/storage/SparseMatrix.h"
#include "storm/modelchecker/multiobjective/Objective.h"
#include "storm/modelchecker/prctl/helper/rewardbounded/EpochManager.h"
#include "storm/modelchecker/prctl/helper/rewardbounded/EpochModel.h"
#include "storm/modelchecker/prctl/helper/rewardbounded/ProductModel.h"
#include "storm/modelchecker/prctl/helper/rewardbounded/Dimension.h"
#include "storm/models/sparse/Model.h"
@ -27,17 +28,7 @@ namespace storm {
typedef typename EpochManager::EpochClass EpochClass;
typedef typename std::conditional<SingleObjectiveMode, ValueType, std::vector<ValueType>>::type SolutionType;
struct EpochModel {
bool epochMatrixChanged;
storm::storage::SparseMatrix<ValueType> epochMatrix;
storm::storage::BitVector stepChoices;
std::vector<SolutionType> stepSolutions;
std::vector<std::vector<ValueType>> objectiveRewards;
std::vector<storm::storage::BitVector> objectiveRewardFilter;
storm::storage::BitVector epochInStates;
};
/*
*
* @param model The (preprocessed) model
@ -52,7 +43,7 @@ namespace storm {
Epoch getStartEpoch();
std::vector<Epoch> getEpochComputationOrder(Epoch const& startEpoch);
EpochModel& setCurrentEpoch(Epoch const& epoch);
EpochModel<ValueType, SingleObjectiveMode>& setCurrentEpoch(Epoch const& epoch);
void setEquationSystemFormatForEpochModel(storm::solver::LinearEquationSolverProblemFormat eqSysFormat);
@ -117,13 +108,10 @@ namespace storm {
std::vector<uint64_t> epochModelToProductChoiceMap;
std::shared_ptr<std::vector<uint64_t> const> productStateToEpochModelInStateMap;
std::set<Epoch> possibleEpochSteps;
EpochModel epochModel;
EpochModel<ValueType, SingleObjectiveMode> epochModel;
boost::optional<Epoch> currentEpoch;
// In case of DTMCs we have different options for the equation problem format the epoch model will have.
boost::optional<storm::solver::LinearEquationSolverProblemFormat> equationSolverProblemFormatForEpochModel;
EpochManager epochManager;
std::vector<Dimension<ValueType>> dimensions;

Write Preview
Loading…
Cancel
Save