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

conditional probabilities in MDPs (Baier method) available in sparse MDP model checker 

Former-commit-id: 76136c5e72
main
dehnert 9 years ago
parent
756b2c5e30
commit
3e38e73efe
4 changed files with 116 additions and 0 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. 21
      src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
  2. 1
      src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
  3. 90
      src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  4. 4
      src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h

21
src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
View File

@ -47,6 +47,12 @@ namespace storm {
if (formula.isGloballyFormula()) {
return true;
}
if (formula.isConditionalPathFormula()) {
storm::logic::ConditionalPathFormula const& conditionalPathFormula = formula.asConditionalPathFormula();
if (conditionalPathFormula.getLeftSubformula().isEventuallyFormula() && conditionalPathFormula.getRightSubformula().isEventuallyFormula()) {
return this->canHandle(conditionalPathFormula.getLeftSubformula()) && this->canHandle(conditionalPathFormula.getRightSubformula());
}
}
return false;
}
@ -90,6 +96,21 @@ namespace storm {
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret)));
}
template<typename SparseMdpModelType>
std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidPropertyException, "Cannot compute conditional probabilities on MDPs with more than one initial state.");
STORM_LOG_THROW(pathFormula.getLeftSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula.");
STORM_LOG_THROW(pathFormula.getRightSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Illegal conditional probability formula.");
std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula().asEventuallyFormula().getSubformula());
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula().asEventuallyFormula().getSubformula());
ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
return storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeConditionalProbabilities(optimalityType.get(), *this->getModel().getInitialStates().begin(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory);
}
template<typename SparseMdpModelType>
std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeUntilProbabilitiesForInitialStates(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType, boost::optional<storm::logic::BoundInfo<ValueType>> const& bound) {
STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");

1
src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
View File

@ -37,6 +37,7 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;
virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;
virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;
virtual std::unique_ptr<CheckResult> computeUntilProbabilitiesForInitialStates(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>(), boost::optional<storm::logic::BoundInfo<ValueType>> const& bound =boost::optional<storm::logic::BoundInfo<ValueType>>());
virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional<std::string> const& rewardModelName = boost::optional<std::string>(), bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;
virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional<std::string> const& rewardModelName = boost::optional<std::string>(), bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;

90
src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
View File

@ -1,5 +1,7 @@
#include "src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/models/sparse/StandardRewardModel.h"
#include "src/storage/MaximalEndComponentDecomposition.h"
@ -494,6 +496,94 @@ namespace storm {
return solver->getContinuousValue(lambda);
}
template<typename ValueType>
std::unique_ptr<CheckResult> SparseMdpPrctlHelper<ValueType>::computeConditionalProbabilities(OptimizationDirection dir, storm::storage::sparse::state_type initialState, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
// We solve the max-case and later adjust the result if the optimization direction was to minimize.
// FIXME: actually do this.
storm::storage::BitVector initialStatesBitVector(transitionMatrix.getRowGroupCount());
initialStatesBitVector.set(initialState);
storm::storage::BitVector allStates(initialStatesBitVector.size(), true);
std::vector<ValueType> conditionProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, conditionStates, false, false, minMaxLinearEquationSolverFactory).result);
std::vector<ValueType> targetProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, transitionMatrix, backwardTransitions, allStates, targetStates, false, false, minMaxLinearEquationSolverFactory).result);
storm::storage::BitVector statesWithProbabilityGreater0E(transitionMatrix.getRowGroupCount(), true);
storm::storage::sparse::state_type state = 0;
for (auto const& element : conditionProbabilities) {
if (storm::utility::isZero(element)) {
statesWithProbabilityGreater0E.set(state, false);
}
++state;
}
// If the conditional probability is undefined for the initial state, we return directly.
if (!statesWithProbabilityGreater0E.get(initialState)) {
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(initialState, storm::utility::infinity<ValueType>()));
}
// Determine those states that need to be equipped with a restart mechanism.
storm::storage::BitVector problematicStates = storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, allStates, conditionStates | targetStates);
// Otherwise, we build the transformed MDP.
storm::storage::BitVector relevantStates = storm::utility::graph::getReachableStates(transitionMatrix, initialStatesBitVector, allStates, conditionStates | targetStates);
std::vector<uint_fast64_t> numberOfStatesBeforeRelevantStates = relevantStates.getNumberOfSetBitsBeforeIndices();
storm::storage::sparse::state_type newGoalState = relevantStates.getNumberOfSetBits();
storm::storage::sparse::state_type newStopState = newGoalState + 1;
storm::storage::sparse::state_type newFailState = newStopState + 1;
// Build the transitions of the (relevant) states of the original model.
storm::storage::SparseMatrixBuilder<ValueType> builder(0, newFailState + 1, 0, true, true);
uint_fast64_t currentRow = 0;
for (auto state : relevantStates) {
builder.newRowGroup(currentRow);
if (targetStates.get(state)) {
builder.addNextValue(currentRow, newGoalState, conditionProbabilities[state]);
if (!storm::utility::isZero(conditionProbabilities[state])) {
builder.addNextValue(currentRow, newFailState, 1 - conditionProbabilities[state]);
}
++currentRow;
} else if (conditionStates.get(state)) {
builder.addNextValue(currentRow, newGoalState, targetProbabilities[state]);
if (!storm::utility::isZero(targetProbabilities[state])) {
builder.addNextValue(currentRow, newStopState, 1 - targetProbabilities[state]);
}
++currentRow;
} else {
for (uint_fast64_t row = transitionMatrix.getRowGroupIndices()[state]; row < transitionMatrix.getRowGroupIndices()[state + 1]; ++row) {
for (auto const& successorEntry : transitionMatrix.getRow(row)) {
builder.addNextValue(currentRow, numberOfStatesBeforeRelevantStates[successorEntry.getColumn()], successorEntry.getValue());
}
++currentRow;
}
if (problematicStates.get(state)) {
builder.addNextValue(currentRow, numberOfStatesBeforeRelevantStates[initialState], storm::utility::one<ValueType>());
++currentRow;
}
}
}
// Now build the transitions of the newly introduced states.
builder.newRowGroup(currentRow);
builder.addNextValue(currentRow, newGoalState, storm::utility::one<ValueType>());
++currentRow;
builder.newRowGroup(currentRow);
builder.addNextValue(currentRow, newStopState, storm::utility::one<ValueType>());
++currentRow;
builder.newRowGroup(currentRow);
builder.addNextValue(currentRow, numberOfStatesBeforeRelevantStates[initialState], storm::utility::one<ValueType>());
++currentRow;
// Finally, build the matrix and dispatch the query as a reachability query.
storm::storage::BitVector newGoalStates(newFailState + 1);
newGoalStates.set(newGoalState);
storm::storage::SparseMatrix<ValueType> newTransitionMatrix = builder.build();
storm::storage::SparseMatrix<ValueType> newBackwardTransitions = newTransitionMatrix.transpose(true);
std::vector<ValueType> goalProbabilities = std::move(computeUntilProbabilities(OptimizationDirection::Maximize, newTransitionMatrix, newBackwardTransitions, storm::storage::BitVector(newFailState + 1, true), newGoalStates, false, false, minMaxLinearEquationSolverFactory).result);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(initialState, goalProbabilities[numberOfStatesBeforeRelevantStates[initialState]]));
}
template class SparseMdpPrctlHelper<double>;
template std::vector<double> SparseMdpPrctlHelper<double>::computeInstantaneousRewards(OptimizationDirection dir, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::models::sparse::StandardRewardModel<double> const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory);
template std::vector<double> SparseMdpPrctlHelper<double>::computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::models::sparse::StandardRewardModel<double> const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory);

4
src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h
View File

@ -25,6 +25,8 @@ namespace storm {
}
namespace modelchecker {
class CheckResult;
namespace helper {
template <typename ValueType>
@ -55,6 +57,8 @@ namespace storm {
static std::vector<ValueType> computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
static std::unique_ptr<CheckResult> computeConditionalProbabilities(OptimizationDirection dir, storm::storage::sparse::state_type initialState, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
private:
static std::vector<ValueType> computeReachabilityRewardsHelper(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);

Write Preview
Loading…
Cancel
Save