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

Further work on SCC-based mc. 

Former-commit-id: 4e5c1fb188
main
dehnert 11 years ago
parent
1cc930f0e4
commit
77e2693ccc
4 changed files with 139 additions and 36 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. 76
      src/modelchecker/reachability/SparseSccModelChecker.cpp
  2. 39
      src/modelchecker/reachability/SparseSccModelChecker.h
  3. 3
      src/storm.cpp
  4. 57
      src/utility/graph.h

76
src/modelchecker/reachability/SparseSccModelChecker.cpp
View File

@ -1,4 +1,7 @@
#include "src/modelchecker/reachability/SparseSccModelChecker.h"
#include "src/storage/StronglyConnectedComponentDecomposition.h"
#include "src/utility/graph.h"
#include "src/exceptions/ExceptionMacros.h"
namespace storm {
namespace modelchecker {
@ -6,23 +9,88 @@ namespace storm {
template<typename ValueType>
ValueType SparseSccModelChecker<ValueType>::computeReachabilityProbability(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
// First, do some sanity checks to establish some required properties.
LOG_THROW(dtmc.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state.");
typename FlexibleSparseMatrix<ValueType>::index_type initialStateIndex = *dtmc.getInitialStates().begin();
storm::storage::BitVector relevantStates = storm::utility::graph::getReachableStates(dtmc.getTransitionMatrix(), dtmc.getInitialStates(), phiStates, psiStates);
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(dtmc, phiStates, psiStates);
storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first);
storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second);
storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
return 0;
// If the initial state is known to have either probability 0 or 1, we can directly return the result.
if (!maybeStates.get(initialStateIndex)) {
return statesWithProbability0.get(initialStateIndex) ? 0 : 1;
}
// Otherwise, we build the submatrix that only has maybe states
submatrix = dtmc.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates);
// Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily.
FlexibleSparseMatrix<ValueType> flexibleMatrix = getFlexibleSparseMatrix(dtmc.getTransitionMatrix());
// Then, we recursively treat all SCCs.
treatScc(dtmc, flexibleMatrix, storm::storage::BitVector(dtmc.getNumberOfStates(), true), 0);
// Now, we return the value for the only initial state.
return flexibleMatrix.getRow(initialStateIndex)[0].getValue();
}
template<typename ValueType>
void SparseSccModelChecker<ValueType>::treatScc(storm::models::Dtmc<ValueType> const& dtmc, FlexibleSparseMatrix<ValueType>& matrix, storm::storage::BitVector const& scc, uint_fast64_t level) {
if (level < 2) {
// Here, we further decompose the SCC into sub-SCCs.
storm::storage::StronglyConnectedComponentDecomposition<ValueType> decomposition(dtmc, scc, true, false);
// And then recursively treat all sub-SCCs.
for (auto const& newScc : decomposition) {
treatScc(dtmc, matrix, scc, level + 1);
}
} else {
// In this case, we perform simple state elimination in the current SCC.
}
}
template<typename ValueType>
FlexibleSparseMatrix<ValueType>::FlexibleSparseMatrix(index_type rows) : data(rows) {
// Intentionally left empty.
}
template<typename ValueType>
void FlexibleSparseMatrix<ValueType>::reserveInRow(index_type row, index_type numberOfElements) {
this->data[row].reserve(numberOfElements);
}
template<typename ValueType>
typename FlexibleSparseMatrix<ValueType>::row_type& FlexibleSparseMatrix<ValueType>::getRow(index_type index) {
return this->data[index];
}
template<typename ValueType>
typename SparseSccModelChecker<ValueType>::FlexibleSparseMatrix SparseSccModelChecker<ValueType>::getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix) {
FlexibleSparseMatrix flexibleMatrix(matrix.getRowCount());
FlexibleSparseMatrix<ValueType> SparseSccModelChecker<ValueType>::getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix) {
FlexibleSparseMatrix<ValueType> flexibleMatrix(matrix.getRowCount());
for (SparseSccModelChecker<ValueType>::FlexibleMatrix::index_type row = 0; row < matrix.getRowCount(); ++row) {
for (typename FlexibleSparseMatrix<ValueType>::index_type rowIndex = 0; rowIndex < matrix.getRowCount(); ++rowIndex) {
typename storm::storage::SparseMatrix<ValueType>::const_rows row = matrix.getRow(rowIndex);
flexibleMatrix.reserveInRow(rowIndex, row.getNumberOfEntries());
for (auto const& element : row) {
flexibleMatrix.getRow(rowIndex).emplace_back(element);
}
}
return flexibleMatrix;
}
template class FlexibleSparseMatrix<double>;
template class SparseSccModelChecker<double>;
} // namespace reachability

39
src/modelchecker/reachability/SparseSccModelChecker.h
View File

@ -3,33 +3,36 @@
namespace storm {
namespace modelchecker {
namespace reachability {
template<typename ValueType>
class FlexibleSparseMatrix {
public:
typedef uint_fast64_t index_type;
typedef ValueType value_type;
typedef std::vector<storm::storage::MatrixEntry<index_type, value_type>> row_type;
FlexibleSparseMatrix() = default;
FlexibleSparseMatrix(index_type rows);
void reserveInRow(index_type row, index_type numberOfElements);
row_type& getRow(index_type);
private:
std::vector<row_type> data;
};
template<typename ValueType>
class SparseSccModelChecker {
private:
class FlexibleSparseMatrix {
public:
typedef uint_fast64_t index_type;
typedef ValueType value_type;
typedef std::vector<storm::storage::MatrixEntry<index_type, value_type>> row_type;
FlexibleSparseMatrix(index_type rows);
void reserveInRow(index_type row, index_type numberOfElements);
row_type& getRow(index_type);
private:
std::vector<row_type> data;
};
public:
static ValueType computeReachabilityProbability(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
private:
void treatScc(storm::storage::SparseMatrix<ValueType>& matrix, storm::storage::BitVector const& scc, uint_fast64_t level) const;
FlexibleSparseMatrix getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix);
static void treatScc(storm::models::Dtmc<ValueType> const& dtmc, FlexibleSparseMatrix<ValueType>& matrix, storm::storage::BitVector const& scc, uint_fast64_t level);
static FlexibleSparseMatrix<ValueType> getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix);
};
}
}

3
src/storm.cpp
View File

@ -232,7 +232,8 @@ int main(const int argc, const char* argv[]) {
storm::storage::BitVector trueStates(model->getNumberOfStates(), true);
storm::storage::BitVector oneStates = model->getLabeledStates("one");
modelChecker.computeReachabilityProbability(*model->as<storm::models::Dtmc<double>>(), trueStates, oneStates);
double value = modelChecker.computeReachabilityProbability(*model->as<storm::models::Dtmc<double>>(), trueStates, oneStates);
std::cout << "computed value " << value << std::endl;
if (s->isSet("mincmd")) {
if (model->getType() != storm::models::MDP) {

57
src/utility/graph.h
View File

@ -33,11 +33,41 @@ namespace storm {
namespace graph {
/*!
* Performs a backwards breadt-first search trough the underlying graph structure
* Performs a forward depth-first search through the underlying graph structure to identify the states that
* are reachable from the given set only passing through a constrained set of states until some target
* have been reached.
*
* @param transitionMatrix The transition relation of the graph structure to search.
* @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.
*/
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 reachableStates(initialStates);
storm::storage::BitVector visitedStates(initialStates);
// Initialize the stack used for the DFS with the states.
std::vector<uint_fast64_t> stack(initialStates.begin(), initialStates.end());
// Perform the actual DFS.
uint_fast64_t currentState = 0;
while (!stack.empty()) {
currentState = stack.back();
stack.pop_back();
// TODO: actually search
}
return reachableStates;
}
/*!
* Performs a backward depth-first search trough the underlying graph structure
* of the given model to determine which states of the model have a positive probability
* of satisfying phi until psi. The resulting states are written to the given bit vector.
*
* @param model The model whose graph structure to search.
* @param backwardTransitions The reversed transition relation of the graph structure to search.
* @param phiStates A bit vector of all states satisfying phi.
* @param psiStates A bit vector of all states satisfying psi.
* @param useStepBound A flag that indicates whether or not to use the given number of maximal steps for the search.
@ -45,9 +75,10 @@ namespace storm {
* @return A bit vector with all indices of states that have a probability greater than 0.
*/
template <typename T>
storm::storage::BitVector performProbGreater0(storm::models::AbstractDeterministicModel<T> const& model, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) {
storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) {
// Prepare the resulting bit vector.
storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates());
uint_fast64_t numberOfStates = phiStates.size();
storm::storage::BitVector statesWithProbabilityGreater0(numberOfStates);
// Add all psi states as the already satisfy the condition.
statesWithProbabilityGreater0 |= psiStates;
@ -59,9 +90,9 @@ namespace storm {
std::vector<uint_fast64_t> stepStack;
std::vector<uint_fast64_t> remainingSteps;
if (useStepBound) {
stepStack.reserve(model.getNumberOfStates());
stepStack.reserve(numberOfStates);
stepStack.insert(stepStack.begin(), psiStates.getNumberOfSetBits(), maximalSteps);
remainingSteps.resize(model.getNumberOfStates());
remainingSteps.resize(numberOfStates);
for (auto state : psiStates) {
remainingSteps[state] = maximalSteps;
}
@ -106,7 +137,7 @@ namespace storm {
* characterizes the states that possess at least one path to a target state.
* The results are written to the given bit vector.
*
* @param model The model whose graph structure to search.
* @param backwardTransitions The reversed transition relation of the graph structure to search.
* @param phiStates A bit vector of all states satisfying phi.
* @param psiStates A bit vector of all states satisfying psi.
* @param statesWithProbabilityGreater0 A reference to a bit vector of states that possess a positive
@ -114,8 +145,8 @@ namespace storm {
* @return A bit vector with all indices of states that have a probability greater than 1.
*/
template <typename T>
storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel<T> const& model, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0) {
storm::storage::BitVector statesWithProbability1 = performProbGreater0(model, backwardTransitions, ~psiStates, ~statesWithProbabilityGreater0);
storm::storage::BitVector performProb1(storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0) {
storm::storage::BitVector statesWithProbability1 = performProbGreater0(backwardTransitions, ~psiStates, ~statesWithProbabilityGreater0);
statesWithProbability1.complement();
return statesWithProbability1;
}
@ -127,15 +158,15 @@ namespace storm {
* characterizes the states that possess at least one path to a target state.
* The results are written to the given bit vector.
*
* @param model The model whose graph structure to search.
* @param backwardTransitions The reversed transition relation of the graph structure to search.
* @param phiStates A bit vector of all states satisfying phi.
* @param psiStates A bit vector of all states satisfying psi.
* @return A bit vector with all indices of states that have a probability greater than 1.
*/
template <typename T>
storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel<T> const& model, storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
storm::storage::BitVector statesWithProbabilityGreater0 = performProbGreater0(model, backwardTransitions, phiStates, psiStates);
storm::storage::BitVector statesWithProbability1 = performProbGreater0(model, backwardTransitions, ~psiStates, ~(statesWithProbabilityGreater0));
storm::storage::BitVector performProb1(storm::storage::SparseMatrix<T> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
storm::storage::BitVector statesWithProbabilityGreater0 = performProbGreater0(backwardTransitions, phiStates, psiStates);
storm::storage::BitVector statesWithProbability1 = performProbGreater0(backwardTransitions, ~psiStates, ~(statesWithProbabilityGreater0));
statesWithProbability1.complement();
return statesWithProbability1;
}

Write Preview
Loading…
Cancel
Save