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

used helper methods instead of own implementations

tempestpy_adaptions
TimQu 8 years ago
parent
502cf4d6e0
commit
3eb675f8c0
4 changed files with 28 additions and 53 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. 30
      src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp
  2. 30
      src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp
  3. 1
      src/storm/solver/SolverSelectionOptions.h
  4. 20
      src/storm/utility/vector.h

30
src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp
View File

@ -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<ConstantType>(hint.getResultHint(),
[] (ConstantType const& value) -> bool { return storm::utility::isZero<ConstantType>(value) || storm::utility::isOne<ConstantType>(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<CheckResult> subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula());
@ -138,14 +126,8 @@ namespace storm {
result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().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<CheckResult> subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula());

30
src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp
View File

@ -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<ConstantType>(hint.getResultHint(),
[] (ConstantType const& value) -> bool { return storm::utility::isZero<ConstantType>(value) || storm::utility::isOne<ConstantType>(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<CheckResult> subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula());
@ -164,14 +151,7 @@ namespace storm {
result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().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<CheckResult> subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula());

1
src/storm/solver/SolverSelectionOptions.h
View File

@ -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)

20
src/storm/utility/vector.h
View File

@ -448,11 +448,13 @@ namespace storm {
*/
template<class T>
storm::storage::BitVector filter(std::vector<T> const& values, std::function<bool (T const& value)> 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<class T>
storm::storage::BitVector filterGreaterZero(std::vector<T> const& values) {
std::function<bool (T const&)> fnc = [] (T const& value) -> bool { return value > storm::utility::zero<T>(); };
return filter(values, fnc);
return filter<T>(values, [] (T const& value) -> bool { return value > storm::utility::zero<T>(); });
}
/*!
@ -494,6 +495,17 @@ namespace storm {
return filter<T>(values, storm::utility::isOne<T>);
}
/*!
* 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<class T>
storm::storage::BitVector filterInfinity(std::vector<T> const& values) {
return filter<T>(values, storm::utility::isInfinity<T>);
}
/**
* Sum the entries from values that are set to one in the filter vector.
* @param values

Write Preview
Loading…
Cancel
Save