From 3eb675f8c066863589bc85534f11b5dd721510f1 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 6 Apr 2017 15:57:30 +0200 Subject: [PATCH] used helper methods instead of own implementations --- .../SparseDtmcInstantiationModelChecker.cpp | 30 ++++--------------- .../SparseMdpInstantiationModelChecker.cpp | 30 ++++--------------- src/storm/solver/SolverSelectionOptions.h | 1 + src/storm/utility/vector.h | 20 ++++++++++--- 4 files changed, 28 insertions(+), 53 deletions(-) diff --git a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp index 190914458..6b3d376a8 100644 --- a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp @@ -4,6 +4,7 @@ #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" +#include "storm/utility/vector.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidStateException.h" @@ -59,14 +60,8 @@ namespace storm { if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { // Extract the maybe states from the current result. assert(hint.hasResultHint()); - storm::storage::BitVector maybeStates(hint.getResultHint().size(), true); - uint_fast64_t stateIndex = 0; - for (auto const& value : hint.getResultHint()) { - if (storm::utility::isZero(value) || storm::utility::isOne(value)) { - maybeStates.set(stateIndex, false); - } - ++stateIndex; - } + storm::storage::BitVector maybeStates = ~storm::utility::vector::filter(hint.getResultHint(), + [] (ConstantType const& value) -> bool { return storm::utility::isZero(value) || storm::utility::isOne(value); }); hint.setMaybeStates(std::move(maybeStates)); hint.setComputeOnlyMaybeStates(true); } @@ -98,14 +93,7 @@ namespace storm { if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { // Extract the maybe states from the current result. assert(hint.hasResultHint()); - storm::storage::BitVector maybeStates(hint.getResultHint().size(), true); - uint_fast64_t stateIndex = 0; - for (auto const& value : hint.getResultHint()) { - if (storm::utility::isInfinity(value)) { - maybeStates.set(stateIndex, false); - } - ++stateIndex; - } + storm::storage::BitVector maybeStates = ~storm::utility::vector::filterInfinity(hint.getResultHint()); // We need to exclude the target states from the maybe states. // Note that we can not consider the states with reward zero since a valuation might set a reward to zero std::unique_ptr subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula()); @@ -138,14 +126,8 @@ namespace storm { result = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); } - storm::storage::BitVector maybeStates(hint.getResultHint().size(), true); - uint_fast64_t stateIndex = 0; - for (auto const& value : hint.getResultHint()) { - if (storm::utility::isZero(value)) { - maybeStates.set(stateIndex, false); - } - ++stateIndex; - } + + storm::storage::BitVector maybeStates = storm::utility::vector::filterGreaterZero(hint.getResultHint()); // We need to exclude the target states from the maybe states. // Note that we can not consider the states with probability one since a state might reach a target state with prob 1 within >0 steps std::unique_ptr subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula()); diff --git a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp index e7a8a1cd8..943053d62 100644 --- a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp @@ -5,6 +5,7 @@ #include "storm/modelChecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelChecker/hints/ExplicitModelCheckerHint.h" #include "storm/utility/graph.h" +#include "storm/utility/vector.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidStateException.h" @@ -67,15 +68,8 @@ namespace storm { if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { // Extract the maybe states from the current result. assert(hint.hasResultHint()); - storm::storage::BitVector maybeStates(hint.getResultHint().size(), true); - uint_fast64_t stateIndex = 0; - for (auto const& value : hint.getResultHint()) { - if (storm::utility::isZero(value) || storm::utility::isOne(value)) { - maybeStates.set(stateIndex, false); - } - ++stateIndex; - } - + storm::storage::BitVector maybeStates = ~storm::utility::vector::filter(hint.getResultHint(), + [] (ConstantType const& value) -> bool { return storm::utility::isZero(value) || storm::utility::isOne(value); }); hint.setMaybeStates(std::move(maybeStates)); hint.setComputeOnlyMaybeStates(true); @@ -119,14 +113,7 @@ namespace storm { if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) { // Extract the maybe states from the current result. assert(hint.hasResultHint()); - storm::storage::BitVector maybeStates(hint.getResultHint().size(), true); - uint_fast64_t stateIndex = 0; - for (auto const& value : hint.getResultHint()) { - if (storm::utility::isInfinity(value)) { - maybeStates.set(stateIndex, false); - } - ++stateIndex; - } + storm::storage::BitVector maybeStates = ~storm::utility::vector::filterInfinity(hint.getResultHint()); // We need to exclude the target states from the maybe states. // Note that we can not consider the states with reward zero since a valuation might set a reward to zero std::unique_ptr subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula()); @@ -164,14 +151,7 @@ namespace storm { result = quantitativeResult->template asExplicitQuantitativeCheckResult().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult().getValueVector())); } - storm::storage::BitVector maybeStates(hint.getResultHint().size(), true); - uint_fast64_t stateIndex = 0; - for (auto const& value : hint.getResultHint()) { - if (storm::utility::isZero(value)) { - maybeStates.set(stateIndex, false); - } - ++stateIndex; - } + storm::storage::BitVector maybeStates = storm::utility::vector::filterGreaterZero(hint.getResultHint()); // We need to exclude the target states from the maybe states. // Note that we can not consider the states with probability one since a state might reach a target state with prob 1 within >0 steps std::unique_ptr subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula()); diff --git a/src/storm/solver/SolverSelectionOptions.h b/src/storm/solver/SolverSelectionOptions.h index 8b6668570..b93014053 100644 --- a/src/storm/solver/SolverSelectionOptions.h +++ b/src/storm/solver/SolverSelectionOptions.h @@ -7,6 +7,7 @@ namespace storm { namespace solver { ExtendEnumsWithSelectionField(MinMaxMethod, PolicyIteration, ValueIteration, Topological) + ExtendEnumsWithSelectionField(GameMethod, PolicyIteration, ValueIteration) ExtendEnumsWithSelectionField(LpSolverType, Gurobi, Glpk, Z3) ExtendEnumsWithSelectionField(EquationSolverType, Native, Gmmxx, Eigen, Elimination) diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h index 9cbbc4da4..9482d35b2 100644 --- a/src/storm/utility/vector.h +++ b/src/storm/utility/vector.h @@ -448,11 +448,13 @@ namespace storm { */ template storm::storage::BitVector filter(std::vector const& values, std::function const& function) { - storm::storage::BitVector result(values.size()); + storm::storage::BitVector result(values.size(), false); uint_fast64_t currentIndex = 0; for (auto const& value : values) { - result.set(currentIndex, function(value)); + if (function(value)) { + result.set(currentIndex, true); + } ++currentIndex; } @@ -468,8 +470,7 @@ namespace storm { */ template storm::storage::BitVector filterGreaterZero(std::vector const& values) { - std::function fnc = [] (T const& value) -> bool { return value > storm::utility::zero(); }; - return filter(values, fnc); + return filter(values, [] (T const& value) -> bool { return value > storm::utility::zero(); }); } /*! @@ -494,6 +495,17 @@ namespace storm { return filter(values, storm::utility::isOne); } + /*! + * Retrieves a bit vector containing all the indices for which the value at this position is equal to one + * + * @param values The vector of values. + * @return The resulting bit vector. + */ + template + storm::storage::BitVector filterInfinity(std::vector const& values) { + return filter(values, storm::utility::isInfinity); + } + /** * Sum the entries from values that are set to one in the filter vector. * @param values