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

all DTMC model checkers now support checking globally formulas 

Former-commit-id: b330937007
main
dehnert 9 years ago
parent
84205a0bf6
commit
d42f52d983
19 changed files with 128 additions and 24 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. 7
      src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
  2. 1
      src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h
  3. 11
      src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
  4. 1
      src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
  5. 19
      src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp
  6. 1
      src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h
  7. 37
      src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
  8. 16
      src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h
  9. 9
      src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
  10. 2
      src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h
  11. 7
      src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
  12. 2
      src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h
  13. 13
      src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
  14. 2
      src/modelchecker/results/ExplicitQuantitativeCheckResult.h
  15. 11
      src/modelchecker/results/HybridQuantitativeCheckResult.cpp
  16. 2
      src/modelchecker/results/HybridQuantitativeCheckResult.h
  17. 3
      src/modelchecker/results/QuantitativeCheckResult.h
  18. 6
      src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp
  19. 2
      src/modelchecker/results/SymbolicQuantitativeCheckResult.h

7
src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
View File

@ -47,6 +47,13 @@ namespace storm {
return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeUntilProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory);
}
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula());
SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeGloballyProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory);
}
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula());

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

@ -21,6 +21,7 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;
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> 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;
virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional<std::string> const& rewardModelName = boost::optional<std::string>(), bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;

11
src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
View File

@ -36,6 +36,9 @@ namespace storm {
if (formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula()) {
return true;
}
if (formula.isGloballyFormula()) {
return true;
}
if (formula.isProbabilityOperatorFormula()) {
return this->canHandle(formula.asProbabilityOperatorFormula().getSubformula());
}
@ -78,6 +81,14 @@ namespace storm {
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}
template<typename SparseDtmcModelType>
std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula());
ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeGloballyProbabilities(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), qualitative, *linearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}
template<typename SparseDtmcModelType>
std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional<std::string> const& rewardModelName, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");

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

@ -23,6 +23,7 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;
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> 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;

19
src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp
View File

@ -31,7 +31,16 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
bool SymbolicDtmcPrctlModelChecker<DdType, ValueType>::canHandle(storm::logic::Formula const& formula) const {
return formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula();
if (formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula()) {
return true;
}
if (formula.isProbabilityOperatorFormula()) {
return this->canHandle(formula.asProbabilityOperatorFormula().getSubformula());
}
if (formula.isGloballyFormula()) {
return true;
}
return false;
}
template<storm::dd::DdType DdType, typename ValueType>
@ -44,6 +53,14 @@ namespace storm {
return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult));
}
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula());
SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
storm::dd::Add<DdType> numericResult = storm::modelchecker::helper::SymbolicDtmcPrctlHelper<DdType, ValueType>::computeGloballyProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), qualitative, *this->linearEquationSolverFactory);
return std::unique_ptr<SymbolicQuantitativeCheckResult<DdType>>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), numericResult));
}
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<CheckResult> SymbolicDtmcPrctlModelChecker<DdType, ValueType>::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula());

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

@ -18,6 +18,7 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;
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> 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;
virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, boost::optional<std::string> const& rewardModelName = boost::optional<std::string>(), bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;

37
src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
View File

@ -24,7 +24,7 @@ namespace storm {
namespace helper {
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<CheckResult> HybridDtmcPrctlHelper<DdType, ValueType>::computeUntilProbabilities(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
std::unique_ptr<CheckResult> HybridDtmcPrctlHelper<DdType, ValueType>::computeUntilProbabilities(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
// We need to identify the states which have to be taken out of the matrix, i.e. all states that have
// probability 0 and 1 of satisfying the until-formula.
std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> statesWithProbability01 = storm::utility::graph::performProb01(model, transitionMatrix, phiStates, psiStates);
@ -50,7 +50,7 @@ namespace storm {
// Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting
// non-maybe states in the matrix.
storm::dd::Add<DdType> submatrix = transitionMatrix * maybeStatesAdd;
storm::dd::Add<DdType, ValueType> submatrix = transitionMatrix * maybeStatesAdd;
// Then compute the vector that contains the one-step probabilities to a state with probability 1 for all
// maybe states.
@ -83,13 +83,20 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<CheckResult> HybridDtmcPrctlHelper<DdType, ValueType>::computeNextProbabilities(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& nextStates) {
storm::dd::Add<DdType> result = transitionMatrix * nextStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd<ValueType>();
std::unique_ptr<CheckResult> HybridDtmcPrctlHelper<DdType, ValueType>::computeGloballyProbabilities(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
std::unique_ptr<CheckResult> result = computeUntilProbabilities(model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory);
result->asQuantitativeCheckResult().oneMinus();
return result;
}
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<CheckResult> HybridDtmcPrctlHelper<DdType, ValueType>::computeNextProbabilities(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& nextStates) {
storm::dd::Add<DdType, ValueType> result = transitionMatrix * nextStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd<ValueType>();
return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), result.sumAbstract(model.getColumnVariables())));
}
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<CheckResult> HybridDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
std::unique_ptr<CheckResult> HybridDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
// We need to identify the states which have to be taken out of the matrix, i.e. all states that have
// probability 0 or 1 of satisfying the until-formula.
storm::dd::Bdd<DdType> statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(model, transitionMatrix.notZero(), phiStates, psiStates, stepBound);
@ -105,12 +112,12 @@ namespace storm {
// Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting
// non-maybe states in the matrix.
storm::dd::Add<DdType> submatrix = transitionMatrix * maybeStatesAdd;
storm::dd::Add<DdType, ValueType> submatrix = transitionMatrix * maybeStatesAdd;
// Then compute the vector that contains the one-step probabilities to a state with probability 1 for all
// maybe states.
storm::dd::Add<DdType> prob1StatesAsColumn = psiStates.template toAdd<ValueType>().swapVariables(model.getRowColumnMetaVariablePairs());
storm::dd::Add<DdType> subvector = (submatrix * prob1StatesAsColumn).sumAbstract(model.getColumnVariables());
storm::dd::Add<DdType, ValueType> prob1StatesAsColumn = psiStates.template toAdd<ValueType>().swapVariables(model.getRowColumnMetaVariablePairs());
storm::dd::Add<DdType, ValueType> subvector = (submatrix * prob1StatesAsColumn).sumAbstract(model.getColumnVariables());
// Finally cut away all columns targeting non-maybe states.
submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs());
@ -134,7 +141,7 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<CheckResult> HybridDtmcPrctlHelper<DdType, ValueType>::computeInstantaneousRewards(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
std::unique_ptr<CheckResult> HybridDtmcPrctlHelper<DdType, ValueType>::computeInstantaneousRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
// Only compute the result if the model has at least one reward this->getModel().
STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
@ -156,12 +163,12 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<CheckResult> HybridDtmcPrctlHelper<DdType, ValueType>::computeCumulativeRewards(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
std::unique_ptr<CheckResult> HybridDtmcPrctlHelper<DdType, ValueType>::computeCumulativeRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
// Only compute the result if the model has at least one reward this->getModel().
STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
// Compute the reward vector to add in each step based on the available reward models.
storm::dd::Add<DdType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix, model.getColumnVariables());
storm::dd::Add<DdType, ValueType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix, model.getColumnVariables());
// Create the ODD for the translation between symbolic and explicit storage.
storm::dd::Odd odd = model.getReachableStates().createOdd();
@ -182,7 +189,7 @@ namespace storm {
}
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<CheckResult> HybridDtmcPrctlHelper<DdType, ValueType>::computeReachabilityRewards(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd<DdType> const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
std::unique_ptr<CheckResult> HybridDtmcPrctlHelper<DdType, ValueType>::computeReachabilityRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd<DdType> const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
// Only compute the result if there is at least one reward model.
STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
@ -207,14 +214,14 @@ namespace storm {
storm::dd::Odd odd = maybeStates.createOdd();
// Create the matrix and the vector for the equation system.
storm::dd::Add<DdType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
storm::dd::Add<DdType, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
// Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting
// non-maybe states in the matrix.
storm::dd::Add<DdType> submatrix = transitionMatrix * maybeStatesAdd;
storm::dd::Add<DdType, ValueType> submatrix = transitionMatrix * maybeStatesAdd;
// Then compute the state reward vector to use in the computation.
storm::dd::Add<DdType> subvector = rewardModel.getTotalRewardVector(maybeStatesAdd, submatrix, model.getColumnVariables());
storm::dd::Add<DdType, ValueType> subvector = rewardModel.getTotalRewardVector(maybeStatesAdd, submatrix, model.getColumnVariables());
// Finally cut away all columns targeting non-maybe states and convert the matrix into the matrix needed
// for solving the equation system (i.e. compute (I-A)).

16
src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h
View File

@ -18,19 +18,21 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
class HybridDtmcPrctlHelper {
public:
typedef typename storm::models::symbolic::Model<DdType>::RewardModelType RewardModelType;
typedef typename storm::models::symbolic::Model<DdType, ValueType>::RewardModelType RewardModelType;
static std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::unique_ptr<CheckResult> computeNextProbabilities(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& nextStates);
static std::unique_ptr<CheckResult> computeNextProbabilities(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& nextStates);
static std::unique_ptr<CheckResult> computeUntilProbabilities(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::unique_ptr<CheckResult> computeUntilProbabilities(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::unique_ptr<CheckResult> computeCumulativeRewards(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::unique_ptr<CheckResult> computeGloballyProbabilities(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::unique_ptr<CheckResult> computeCumulativeRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::unique_ptr<CheckResult> computeReachabilityRewards(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd<DdType> const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::unique_ptr<CheckResult> computeReachabilityRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd<DdType> const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
};
}

9
src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
View File

@ -104,6 +104,15 @@ namespace storm {
return result;
}
template<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeGloballyProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
std::vector<ValueType> result = computeUntilProbabilities(transitionMatrix, backwardTransitions, storm::storage::BitVector(transitionMatrix.getRowCount(), true), ~psiStates, qualitative, linearEquationSolverFactory);
for (auto& entry : result) {
entry = storm::utility::one<ValueType>() - entry;
}
return result;
}
template<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeNextProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
// Create the vector with which to multiply and initialize it correctly.

2
src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h
View File

@ -25,6 +25,8 @@ namespace storm {
static std::vector<ValueType> computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::vector<ValueType> computeGloballyProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::vector<ValueType> computeCumulativeRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::vector<ValueType> computeInstantaneousRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);

7
src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
View File

@ -67,6 +67,13 @@ namespace storm {
}
}
template<storm::dd::DdType DdType, typename ValueType>
storm::dd::Add<DdType, ValueType> SymbolicDtmcPrctlHelper<DdType, ValueType>::computeGloballyProbabilities(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory) {
storm::dd::Add<DdType, ValueType> result = computeUntilProbabilities(model, transitionMatrix, model.getReachableStates(), !psiStates && model.getReachableStates(), qualitative, linearEquationSolverFactory);
result = result.getDdManager().template getAddOne<ValueType>() - result;
return result;
}
template<storm::dd::DdType DdType, typename ValueType>
storm::dd::Add<DdType, ValueType> SymbolicDtmcPrctlHelper<DdType, ValueType>::computeNextProbabilities(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& nextStates) {
storm::dd::Add<DdType, ValueType> result = transitionMatrix * nextStates.swapVariables(model.getRowColumnMetaVariablePairs()).template toAdd<ValueType>();

2
src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h
View File

@ -23,6 +23,8 @@ namespace storm {
static storm::dd::Add<DdType, ValueType> computeUntilProbabilities(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory);
static storm::dd::Add<DdType, ValueType> computeGloballyProbabilities(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory);
static storm::dd::Add<DdType, ValueType> computeCumulativeRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory);
static storm::dd::Add<DdType, ValueType> computeInstantaneousRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory);

13
src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
View File

@ -218,6 +218,19 @@ namespace storm {
return true;
}
template<typename ValueType>
void ExplicitQuantitativeCheckResult<ValueType>::oneMinus() {
if (this->isResultForAllStates()) {
for (auto& element : boost::get<vector_type>(values)) {
element = storm::utility::one<ValueType>() - element;
}
} else {
for (auto& element : boost::get<map_type>(values)) {
element.second = storm::utility::one<ValueType>() - element.second;
}
}
}
template class ExplicitQuantitativeCheckResult<double>;
#ifdef STORM_HAVE_CARL

2
src/modelchecker/results/ExplicitQuantitativeCheckResult.h
View File

@ -49,6 +49,8 @@ namespace storm {
virtual void filter(QualitativeCheckResult const& filter) override;
virtual void oneMinus() override;
private:
// The values of the quantitative check result.
boost::variant<vector_type, map_type> values;

11
src/modelchecker/results/HybridQuantitativeCheckResult.cpp
View File

@ -164,6 +164,17 @@ namespace storm {
return max;
}
template<storm::dd::DdType Type, typename ValueType>
void HybridQuantitativeCheckResult<Type, ValueType>::oneMinus() {
storm::dd::Add<Type> one = symbolicValues.getDdManager().template getAddOne<ValueType>();
storm::dd::Add<Type> zero = symbolicValues.getDdManager().template getAddZero<ValueType>();
symbolicValues = symbolicStates.ite(one - symbolicValues, zero);
for (auto& element : explicitValues) {
element = storm::utility::one<ValueType>() - element;
}
}
// Explicitly instantiate the class.
template class HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>;
template class HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>;

2
src/modelchecker/results/HybridQuantitativeCheckResult.h
View File

@ -50,6 +50,8 @@ namespace storm {
virtual ValueType getMax() const;
virtual void oneMinus() override;
private:
// The set of all reachable states.
storm::dd::Bdd<Type> reachableStates;

3
src/modelchecker/results/QuantitativeCheckResult.h
View File

@ -7,11 +7,12 @@ namespace storm {
namespace modelchecker {
class QuantitativeCheckResult : public CheckResult {
public:
virtual ~QuantitativeCheckResult() = default;
virtual std::unique_ptr<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const;
virtual void oneMinus() = 0;
virtual bool isQuantitative() const override;
};
}

6
src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp
View File

@ -89,6 +89,12 @@ namespace storm {
return this->values.getMax();
}
template<storm::dd::DdType Type, typename ValueType>
void SymbolicQuantitativeCheckResult<Type, ValueType>::oneMinus() {
storm::dd::Add<Type> one = values.getDdManager().template getAddOne<ValueType>();
values = one - values;
}
// Explicitly instantiate the class.
template class SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>;
template class SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>;

2
src/modelchecker/results/SymbolicQuantitativeCheckResult.h
View File

@ -38,6 +38,8 @@ namespace storm {
virtual ValueType getMax() const;
virtual void oneMinus() override;
private:
// The set of all reachable states.
storm::dd::Bdd<Type> reachableStates;

Write Preview
Loading…
Cancel
Save