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

Added Support for Total Reward Formulas for DTMCs in the Sparse Engine

main
TimQu 7 years ago
parent
dfc0141894
commit
87e34d7b32
9 changed files with 31 additions and 2 deletions
Split View
  1. 2
      src/storm/logic/FragmentSpecification.cpp
  2. 7
      src/storm/modelchecker/AbstractModelChecker.cpp
  3. 1
      src/storm/modelchecker/AbstractModelChecker.h
  4. 6
      src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
  5. 1
      src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
  6. 10
      src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
  7. 2
      src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h
  8. 2
      src/storm/models/sparse/NondeterministicModel.cpp
  9. 2
      src/storm/models/sparse/NondeterministicModel.h

2
src/storm/logic/FragmentSpecification.cpp
View File

@ -59,6 +59,7 @@ namespace storm {
prctl.setCumulativeRewardFormulasAllowed(true);
prctl.setInstantaneousFormulasAllowed(true);
prctl.setReachabilityRewardFormulasAllowed(true);
prctl.setTotalRewardFormulasAllowed(true);
prctl.setLongRunAverageOperatorsAllowed(true);
prctl.setStepBoundedCumulativeRewardFormulasAllowed(true);
prctl.setTimeBoundedCumulativeRewardFormulasAllowed(true);
@ -81,6 +82,7 @@ namespace storm {
csrl.setCumulativeRewardFormulasAllowed(true);
csrl.setInstantaneousFormulasAllowed(true);
csrl.setReachabilityRewardFormulasAllowed(true);
csrl.setTotalRewardFormulasAllowed(true);
csrl.setLongRunAverageOperatorsAllowed(true);
csrl.setTimeBoundedCumulativeRewardFormulasAllowed(true);

7
src/storm/modelchecker/AbstractModelChecker.cpp
View File

@ -105,6 +105,8 @@ namespace storm {
return this->computeInstantaneousRewards(env, rewardMeasureType, checkTask.substituteFormula(rewardFormula.asInstantaneousRewardFormula()));
} else if (rewardFormula.isReachabilityRewardFormula()) {
return this->computeReachabilityRewards(env, rewardMeasureType, checkTask.substituteFormula(rewardFormula.asReachabilityRewardFormula()));
} else if (rewardFormula.isTotalRewardFormula()) {
return this->computeTotalRewards(env, rewardMeasureType, checkTask.substituteFormula(rewardFormula.asTotalRewardFormula()));
} else if (rewardFormula.isLongRunAverageRewardFormula()) {
return this->computeLongRunAverageRewards(env, rewardMeasureType, checkTask.substituteFormula(rewardFormula.asLongRunAverageRewardFormula()));
} else if (rewardFormula.isConditionalRewardFormula()) {
@ -132,6 +134,11 @@ namespace storm {
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
}
template<typename ModelType>
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask<storm::logic::TotalRewardFormula, ValueType> const& checkTask) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
}
template<typename ModelType>
std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) {

1
src/storm/modelchecker/AbstractModelChecker.h
View File

@ -63,6 +63,7 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask);
virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask);
virtual std::unique_ptr<CheckResult> computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask);
virtual std::unique_ptr<CheckResult> computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::TotalRewardFormula, ValueType> const& checkTask);
virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask);
// The methods to compute the long-run average probabilities and timing measures.

6
src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
View File

@ -123,6 +123,12 @@ namespace storm {
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeReachabilityRewards(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.getHint());
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}
template<typename SparseDtmcModelType>
std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask<storm::logic::TotalRewardFormula, ValueType> const& checkTask) {
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeTotalRewards(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), checkTask.isQualitativeSet(), checkTask.getHint());
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}
template<typename SparseDtmcModelType>
std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeLongRunAverageProbabilities(Environment const& env, CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) {

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

@ -30,6 +30,7 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::TotalRewardFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeConditionalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::ConditionalFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) override;

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

@ -383,6 +383,16 @@ namespace storm {
return result;
}
template<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeTotalRewards(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, bool qualitative, ModelCheckerHint const& hint) {
// Identify the states from which only states with zero reward are reachable.
// We can then compute reachability rewards assuming these states as target set.
storm::storage::BitVector statesWithoutReward = rewardModel.getStatesWithZeroReward(transitionMatrix);
storm::storage::BitVector rew0States = storm::utility::graph::performProbGreater0(backwardTransitions, statesWithoutReward, ~statesWithoutReward);
rew0States.complement();
return computeReachabilityRewards(env, std::move(goal), transitionMatrix, backwardTransitions, rewardModel, rew0States, qualitative, hint);
}
template<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, ModelCheckerHint const& hint) {

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

@ -42,6 +42,8 @@ namespace storm {
static std::vector<ValueType> computeInstantaneousRewards(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount);
static std::vector<ValueType> computeTotalRewards(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, bool qualitative, ModelCheckerHint const& hint = ModelCheckerHint());
static std::vector<ValueType> computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, ModelCheckerHint const& hint = ModelCheckerHint());
static std::vector<ValueType> computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, ModelCheckerHint const& hint = ModelCheckerHint());

2
src/storm/models/sparse/NondeterministicModel.cpp
View File

@ -45,7 +45,7 @@ namespace storm {
}
template<typename ValueType, typename RewardModelType>
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> NondeterministicModel<ValueType, RewardModelType>::applyScheduler(storm::storage::Scheduler<ValueType> const& scheduler, bool dropUnreachableStates) {
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> NondeterministicModel<ValueType, RewardModelType>::applyScheduler(storm::storage::Scheduler<ValueType> const& scheduler, bool dropUnreachableStates) const {
storm::storage::SparseModelMemoryProduct<ValueType, RewardModelType> memoryProduct(*this, scheduler);
if (!dropUnreachableStates) {
memoryProduct.setBuildFullProduct();

2
src/storm/models/sparse/NondeterministicModel.h
View File

@ -57,7 +57,7 @@ namespace storm {
* @param scheduler the considered scheduler.
* @param dropUnreachableStates if set, the resulting model only considers the states that are reachable from an initial state
*/
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> applyScheduler(storm::storage::Scheduler<ValueType> const& scheduler, bool dropUnreachableStates = true);
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> applyScheduler(storm::storage::Scheduler<ValueType> const& scheduler, bool dropUnreachableStates = true) const;
virtual void printModelInformationToStream(std::ostream& out) const override;

Write Preview
|||||||
100:0
Loading…
Cancel
Save