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

added feature to compute step-bounded until probabilities in parametric models 

Former-commit-id: 172e87cb55
main
dehnert 10 years ago
parent
98d173ca3c
commit
0f6e6e4da1
5 changed files with 174 additions and 48 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. 120
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
  2. 1
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
  3. 85
      src/utility/graph.cpp
  4. 4
      src/utility/graph.h
  5. 4
      test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp

120
src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
View File

@ -99,6 +99,11 @@ namespace storm {
return true;
}
}
} else if (formula.isBoundedUntilFormula()) {
storm::logic::BoundedUntilFormula const& boundedUntilFormula = formula.asBoundedUntilFormula();
if (boundedUntilFormula.getLeftSubformula().isPropositionalFormula() && boundedUntilFormula.getRightSubformula().isPropositionalFormula()) {
return true;
}
} else if (formula.isReachabilityRewardFormula()) {
storm::logic::ReachabilityRewardFormula reachabilityRewardFormula = formula.asReachabilityRewardFormula();
if (reachabilityRewardFormula.getSubformula().isPropositionalFormula()) {
@ -115,6 +120,107 @@ namespace storm {
return false;
}
template<typename SparseDtmcModelType>
std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
// Retrieve the appropriate bitvectors by model checking the subformulas.
std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
storm::storage::BitVector const& phiStates = leftResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
storm::storage::BitVector const& psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
// Start by determining the states that have a non-zero probability of reaching the target states within the
// time bound.
storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel().getBackwardTransitions(), phiStates, psiStates, true, pathFormula.getDiscreteTimeBound());
statesWithProbabilityGreater0 &= ~psiStates;
// Determine whether we need to perform some further computation.
bool furtherComputationNeeded = true;
if (computeResultsForInitialStatesOnly && this->getModel().getInitialStates().isDisjointFrom(statesWithProbabilityGreater0)) {
STORM_LOG_DEBUG("The probability for all initial states was found in a preprocessing step.");
furtherComputationNeeded = false;
} else if (statesWithProbabilityGreater0.empty()) {
STORM_LOG_DEBUG("The probability for all states was found in a preprocessing step.");
furtherComputationNeeded = false;
}
storm::storage::SparseMatrix<ValueType> const& transitionMatrix = this->getModel().getTransitionMatrix();
storm::storage::BitVector const& initialStates = this->getModel().getInitialStates();
std::vector<ValueType> result(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
if (furtherComputationNeeded) {
uint_fast64_t timeBound = pathFormula.getDiscreteTimeBound();
if (computeResultsForInitialStatesOnly) {
// Determine the set of states that is reachable from the initial state without jumping over a target state.
storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(transitionMatrix, initialStates, phiStates, psiStates, true, timeBound);
// Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
statesWithProbabilityGreater0 &= reachableStates;
}
// We then build the submatrix that only has the transitions of the maybe states.
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, statesWithProbabilityGreater0, statesWithProbabilityGreater0, true);
std::vector<std::size_t> distancesFromInitialStates;
storm::storage::BitVector relevantStates;
if (computeResultsForInitialStatesOnly) {
// Determine the set of initial states of the sub-model.
storm::storage::BitVector subInitialStates = this->getModel().getInitialStates() % statesWithProbabilityGreater0;
// Precompute the distances of the relevant states to the initial states.
distancesFromInitialStates = storm::utility::graph::getDistances(submatrix, subInitialStates, statesWithProbabilityGreater0);
// Set all states to be relevant for later use.
relevantStates = storm::storage::BitVector(statesWithProbabilityGreater0.getNumberOfSetBits(), true);
}
// Create the vector of one-step probabilities to go to target states.
std::vector<ValueType> b = transitionMatrix.getConstrainedRowSumVector(statesWithProbabilityGreater0, psiStates);
// Create the vector with which to multiply.
std::vector<ValueType> subresult(b);
std::vector<ValueType> tmp(subresult.size());
// Subtract one from the time bound because initializing the sub-result to b already accounts for one step.
--timeBound;
// Perform matrix-vector multiplications until the time-bound is met.
for (uint_fast64_t timeStep = 0; timeStep < timeBound; ++timeStep) {
submatrix.multiplyWithVector(subresult, tmp);
storm::utility::vector::addVectors(tmp, b, subresult);
// If we are computing the results for the initial states only, we can use the minimal distance from
// each state to the initial states to determine whether we still need to consider the values for
// these states. If not, we can null-out all their probabilities.
if (computeResultsForInitialStatesOnly) {
for (auto state : relevantStates) {
if (distancesFromInitialStates[state] > (timeBound - timeStep)) {
for (auto& element : submatrix.getRow(state)) {
element.setValue(storm::utility::zero<ValueType>());
}
b[state] = storm::utility::zero<ValueType>();
relevantStates.set(state, false);
}
}
}
}
// Set the values of the resulting vector accordingly.
storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, subresult);
}
storm::utility::vector::setVectorValues<ValueType>(result, psiStates, storm::utility::one<ValueType>());
// Construct check result based on whether we have computed values for all states or just the initial states.
std::unique_ptr<CheckResult> checkResult(new ExplicitQuantitativeCheckResult<ValueType>(result));
if (computeResultsForInitialStatesOnly) {
// If we computed the results for the initial (and prob 0 and prob1) states only, we need to filter the
// result to only communicate these results.
checkResult->filter(ExplicitQualitativeCheckResult(this->getModel().getInitialStates() | psiStates));
}
return checkResult;
}
template<typename SparseDtmcModelType>
std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<SparseDtmcModelType>::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<OptimizationDirection> const& optimalityType) {
// Retrieve the appropriate bitvectors by model checking the subformulas.
@ -763,10 +869,8 @@ namespace storm {
entry.setValue(storm::utility::simplify(entry.getValue() * loopProbability));
}
}
if (!computeRewards) {
values[state] = storm::utility::simplify(values[state] * loopProbability);
}
}
STORM_LOG_TRACE((hasSelfLoop ? "State has self-loop." : "State does not have a self-loop."));
@ -872,18 +976,8 @@ namespace storm {
predecessorForwardTransitions = std::move(newSuccessors);
STORM_LOG_TRACE("Fixed new next-state probabilities of predecessor state " << predecessor << ".");
if (!computeRewards) {
// Add the probabilities to go to a target state in just one step if we have to compute probabilities.
values[predecessor] += storm::utility::simplify(multiplyFactor * values[state]);
} else {
// If we are computing rewards, we basically scale the state reward of the state to eliminate and
// add the result to the state reward of the predecessor.
if (hasSelfLoop) {
values[predecessor] += storm::utility::simplify(multiplyFactor * loopProbability * values[state]);
} else {
// Compute the new value for the predecessor.
values[predecessor] += storm::utility::simplify(multiplyFactor * values[state]);
}
}
if (priorityQueue != nullptr) {
STORM_LOG_TRACE("Updating priority of predecessor.");

1
src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
View File

@ -25,6 +25,7 @@ namespace storm {
// The implemented methods of the AbstractModelChecker interface.
virtual bool canHandle(storm::logic::Formula const& formula) const override;
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> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, 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;
virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional<OptimizationDirection> const& optimalityType = boost::optional<OptimizationDirection>()) override;

85
src/utility/graph.cpp
View File

@ -27,28 +27,55 @@ namespace storm {
namespace graph {
template<typename T>
storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates) {
storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps) {
storm::storage::BitVector reachableStates(initialStates);
uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount();
// Initialize the stack used for the DFS with the states.
std::vector<uint_fast64_t> stack(initialStates.begin(), initialStates.end());
// Initialize the stack for the step bound, if the number of steps is bounded.
std::vector<uint_fast64_t> stepStack;
std::vector<uint_fast64_t> remainingSteps;
if (useStepBound) {
stepStack.reserve(numberOfStates);
stepStack.insert(stepStack.begin(), targetStates.getNumberOfSetBits(), maximalSteps);
remainingSteps.resize(numberOfStates);
for (auto state : targetStates) {
remainingSteps[state] = maximalSteps;
}
}
// Perform the actual DFS.
uint_fast64_t currentState = 0;
uint_fast64_t currentState = 0, currentStepBound = 0;
while (!stack.empty()) {
currentState = stack.back();
stack.pop_back();
if (useStepBound) {
currentStepBound = stepStack.back();
stepStack.pop_back();
}
for (auto const& successor : transitionMatrix.getRowGroup(currentState)) {
// Only explore the state if the transition was actually there and the successor has not yet
// been visited.
if (successor.getValue() != storm::utility::zero<T>() && !reachableStates.get(successor.getColumn())) {
if (successor.getValue() != storm::utility::zero<T>() && !reachableStates.get(successor.getColumn()) && (!useStepBound || remainingSteps[successor.getColumn()] < currentStepBound - 1)) {
// If the successor is one of the target states, we need to include it, but must not explore
// it further.
if (targetStates.get(successor.getColumn())) {
reachableStates.set(successor.getColumn());
} else if (constraintStates.get(successor.getColumn())) {
// However, if the state is in the constrained set of states, we need to follow it.
// However, if the state is in the constrained set of states, we potentially need to follow it.
if (useStepBound) {
remainingSteps[successor.getColumn()] = currentStepBound - 1;
stepStack.push_back(currentStepBound - 1);
if (currentStepBound == 0) {
continue;
}
}
reachableStates.set(successor.getColumn());
stack.push_back(successor.getColumn());
}
@ -128,19 +155,19 @@ namespace storm {
}
for (typename storm::storage::SparseMatrix<T>::const_iterator entryIt = backwardTransitions.begin(currentState), entryIte = backwardTransitions.end(currentState); entryIt != entryIte; ++entryIt) {
if (phiStates[entryIt->getColumn()] && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) || (useStepBound && remainingSteps[entryIt->getColumn()] < currentStepBound - 1))) {
if (phiStates[entryIt->getColumn()] && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) && (!useStepBound || remainingSteps[entryIt->getColumn()] < currentStepBound - 1))) {
// If we don't have a bound on the number of steps to take, just add the state to the stack.
if (!useStepBound) {
statesWithProbabilityGreater0.set(entryIt->getColumn(), true);
stack.push_back(entryIt->getColumn());
} else if (currentStepBound > 0) {
if (useStepBound) {
// If there is at least one more step to go, we need to push the state and the new number of steps.
remainingSteps[entryIt->getColumn()] = currentStepBound - 1;
statesWithProbabilityGreater0.set(entryIt->getColumn(), true);
stack.push_back(entryIt->getColumn());
stepStack.push_back(currentStepBound - 1);
if (currentStepBound == 0) {
continue;
}
}
statesWithProbabilityGreater0.set(entryIt->getColumn(), true);
stack.push_back(entryIt->getColumn());
}
}
}
@ -379,19 +406,20 @@ namespace storm {
}
for (typename storm::storage::SparseMatrix<T>::const_iterator entryIt = backwardTransitions.begin(currentState), entryIte = backwardTransitions.end(currentState); entryIt != entryIte; ++entryIt) {
if (phiStates.get(entryIt->getColumn()) && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) || (useStepBound && remainingSteps[entryIt->getColumn()] < currentStepBound - 1))) {
if (phiStates.get(entryIt->getColumn()) && (!statesWithProbabilityGreater0.get(entryIt->getColumn()) && (!useStepBound || remainingSteps[entryIt->getColumn()] < currentStepBound - 1))) {
// If we don't have a bound on the number of steps to take, just add the state to the stack.
if (!useStepBound) {
statesWithProbabilityGreater0.set(entryIt->getColumn(), true);
stack.push_back(entryIt->getColumn());
} else if (currentStepBound > 0) {
if (useStepBound) {
// If there is at least one more step to go, we need to push the state and the new number of steps.
remainingSteps[entryIt->getColumn()] = currentStepBound - 1;
statesWithProbabilityGreater0.set(entryIt->getColumn(), true);
stack.push_back(entryIt->getColumn());
stepStack.push_back(currentStepBound - 1);
if (currentStepBound == 0) {
continue;
}
}
statesWithProbabilityGreater0.set(entryIt->getColumn(), true);
stack.push_back(entryIt->getColumn());
}
}
}
@ -527,7 +555,7 @@ namespace storm {
}
for(typename storm::storage::SparseMatrix<T>::const_iterator predecessorEntryIt = backwardTransitions.begin(currentState), predecessorEntryIte = backwardTransitions.end(currentState); predecessorEntryIt != predecessorEntryIte; ++predecessorEntryIt) {
if (phiStates.get(predecessorEntryIt->getColumn()) && (!statesWithProbabilityGreater0.get(predecessorEntryIt->getColumn()) || (useStepBound && remainingSteps[predecessorEntryIt->getColumn()] < currentStepBound - 1))) {
if (phiStates.get(predecessorEntryIt->getColumn()) && (!statesWithProbabilityGreater0.get(predecessorEntryIt->getColumn()) && (!useStepBound || remainingSteps[predecessorEntryIt->getColumn()] < currentStepBound - 1))) {
// Check whether the predecessor has at least one successor in the current state set for every
// nondeterministic choice.
bool addToStatesWithProbabilityGreater0 = true;
@ -549,17 +577,18 @@ namespace storm {
// If we need to add the state, then actually add it and perform further search from the state.
if (addToStatesWithProbabilityGreater0) {
// If we don't have a bound on the number of steps to take, just add the state to the stack.
if (!useStepBound) {
statesWithProbabilityGreater0.set(predecessorEntryIt->getColumn(), true);
stack.push_back(predecessorEntryIt->getColumn());
} else if (currentStepBound > 0) {
if (useStepBound) {
// If there is at least one more step to go, we need to push the state and the new number of steps.
remainingSteps[predecessorEntryIt->getColumn()] = currentStepBound - 1;
statesWithProbabilityGreater0.set(predecessorEntryIt->getColumn(), true);
stack.push_back(predecessorEntryIt->getColumn());
stepStack.push_back(currentStepBound - 1);
if (currentStepBound == 0) {
continue;
}
}
statesWithProbabilityGreater0.set(predecessorEntryIt->getColumn(), true);
stack.push_back(predecessorEntryIt->getColumn());
}
}
}
}
@ -927,7 +956,7 @@ namespace storm {
template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates);
template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps);
template std::vector<std::size_t> getDistances(storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::BitVector> const& subsystem);
@ -993,7 +1022,7 @@ namespace storm {
template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<float> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates);
template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<float> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps);
template std::vector<std::size_t> getDistances(storm::storage::SparseMatrix<float> const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::BitVector> const& subsystem);
@ -1048,7 +1077,7 @@ namespace storm {
#ifdef STORM_HAVE_CARL
template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates);
template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps);
template std::vector<std::size_t> getDistances(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::BitVector> const& subsystem);

4
src/utility/graph.h
View File

@ -55,9 +55,11 @@ namespace storm {
* @param initialStates The set of states from which to start the search.
* @param constraintStates The set of states that must not be left.
* @param targetStates The target states that may not be passed.
* @param useStepBound A flag that indicates whether or not to use the given number of maximal steps for the search.
* @param maximalSteps The maximal number of steps to reach the psi states.
*/
template<typename T>
storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates);
storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<T> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0);
/*!
* Performs a breadth-first search through the underlying graph structure to compute the distance from all

4
test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp
View File

@ -131,7 +131,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) {
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0448979, quantitativeResult3[0], storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(1.0448979, quantitativeResult2[0], storm::settings::generalSettings().getPrecision());
}
Write Preview
Loading…
Cancel
Save