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

First working version of SCC-based mc. 

Former-commit-id: 57dc865344
tempestpy_adaptions
dehnert 10 years ago
parent
8f7c9d5c25
commit
95ee78ede2
5 changed files with 167 additions and 65 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. 188
      src/modelchecker/reachability/SparseSccModelChecker.cpp
  2. 6
      src/modelchecker/reachability/SparseSccModelChecker.h
  3. 12
      src/storage/SparseMatrix.cpp
  4. 9
      src/storage/SparseMatrix.h
  5. 17
      src/storm.cpp

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

@ -4,6 +4,8 @@
#include "src/storage/StronglyConnectedComponentDecomposition.h"
#include "src/utility/graph.h"
#include "src/utility/vector.h"
#include "src/exceptions/InvalidStateException.h"
#include "src/exceptions/ExceptionMacros.h"
namespace storm {
@ -30,41 +32,35 @@ namespace storm {
// 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(dtmc.getTransitionMatrix(), dtmc.getInitialStates(), maybeStates, statesWithProbability1);
// Subtract from the maybe states the set of states that is not reachable.
// Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
maybeStates &= reachableStates;
// Otherwise, we build the submatrix that only has the transitions of the maybe states.
storm::storage::SparseMatrix<ValueType> 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());
FlexibleSparseMatrix<ValueType> flexibleMatrix = getFlexibleSparseMatrix(submatrix);
// Create a vector for the probabilities to go to a state with probability 1 in one step.
std::vector<ValueType> oneStepProbabilities = dtmc.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1);
for (uint_fast64_t i = 0; i < oneStepProbabilities.size(); ++i) {
std::cout << i << " -> " << oneStepProbabilities[i] << std::endl;
}
// Then, we recursively treat all SCCs.
treatScc(dtmc, flexibleMatrix, oneStepProbabilities, dtmc.getInitialStates() % maybeStates, storm::storage::BitVector(maybeStates.getNumberOfSetBits(), true), submatrix, submatrix.transpose(), false, 0);
FlexibleSparseMatrix<ValueType> backwardTransitions = getFlexibleSparseMatrix(submatrix.transpose(), true);
treatScc(dtmc, flexibleMatrix, oneStepProbabilities, dtmc.getInitialStates() % maybeStates, storm::storage::BitVector(maybeStates.getNumberOfSetBits(), true), submatrix, backwardTransitions, false, 0);
// Now, we return the value for the only initial state.
return oneStepProbabilities[initialStateIndex];
}
template<typename ValueType>
void SparseSccModelChecker<ValueType>::treatScc(storm::models::Dtmc<ValueType> const& dtmc, FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level) {
std::cout << "treating SCC " << scc << " at level " << level << " (entry: " << entryStates << ")" << std::endl;
if (level <= 2) {
std::cout << "1" << std::endl;
void SparseSccModelChecker<ValueType>::treatScc(storm::models::Dtmc<ValueType> const& dtmc, FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level) {
if (level <= 3) {
// Here, we further decompose the SCC into sub-SCCs.
storm::storage::StronglyConnectedComponentDecomposition<ValueType> decomposition(forwardTransitions, scc & ~entryStates, true, false);
std::cout << decomposition << std::endl;
// To eliminate the remaining one-state SCCs, we need to keep track of them.
storm::storage::BitVector remainingStates(scc);
std::cout << "1" << std::endl;
// And then recursively treat all sub-SCCs.
for (auto const& newScc : decomposition) {
// If the SCC consists of just one state, we do not explore it recursively, but rather eliminate
@ -90,8 +86,6 @@ namespace storm {
// Recursively descend in SCC-hierarchy.
treatScc(dtmc, matrix, oneStepProbabilities, entryStates, newSccAsBitVector, forwardTransitions, backwardTransitions, true, level + 1);
}
std::cout << "1" << std::endl;
// If we are not supposed to eliminate the entry states, we need to take them out of the set of
// remaining states.
@ -122,13 +116,16 @@ namespace storm {
}
template<typename ValueType>
void SparseSccModelChecker<ValueType>::eliminateState(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix<ValueType> const& backwardTransitions) {
void SparseSccModelChecker<ValueType>::eliminateState(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix<ValueType>& backwardTransitions) {
ValueType loopProbability = storm::utility::constantZero<ValueType>();
// Start by finding loop probability.
for (auto const& entry : matrix.getRow(state)) {
if (entry.getColumn() == state) {
loopProbability = entry.getValue();
typename FlexibleSparseMatrix<ValueType>::row_type& currentStateSuccessors = matrix.getRow(state);
for (auto const& entry : currentStateSuccessors) {
if (entry.getColumn() >= state) {
if (entry.getColumn() == state) {
loopProbability = entry.getValue();
}
break;
}
}
@ -140,49 +137,128 @@ namespace storm {
}
oneStepProbabilities[state] *= loopProbability;
// Now connect the predecessors of the state to eliminate with its successors.
std::size_t newEntries = matrix.getRow(state).size();
for (auto const& predecessorEntry : backwardTransitions.getRow(state)) {
// First, add all entries of the successor to the list of outgoing transitions of the predecessor.
typename FlexibleSparseMatrix<ValueType>::row_type row = matrix.getRow(predecessorEntry.getColumn());
typename FlexibleSparseMatrix<ValueType>::row_type::iterator multiplyElement = std::find_if(row.begin(), row.end(), [=](storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() == state; });
ValueType multiplyFactor = storm::utility::constantOne<ValueType>();
if (multiplyElement != row.end()) {
// Remove the transition to the state that is to be eliminated.
multiplyElement->setValue(0);
multiplyFactor = multiplyElement->getValue();
// Now connect the predecessors of the state being eliminated with its successors.
typename FlexibleSparseMatrix<ValueType>::row_type& currentStatePredecessors = backwardTransitions.getRow(state);
for (auto const& predecessorEntry : currentStatePredecessors) {
uint_fast64_t predecessor = predecessorEntry.getColumn();
// Skip the state itself as one of its predecessors.
if (predecessor == state) {
continue;
}
// Now scale all the entries in the current row and insert them in the transitions of the predecessor.
row.reserve(row.size() + newEntries);
std::for_each(matrix.getRow(state).begin(), matrix.getRow(state).end(), [&] (storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a) { row.emplace_back(a.getColumn(), multiplyFactor * a.getValue()); });
// Then sort the vector according to their column indices.
std::sort(row.begin(), row.end(), [](storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a, storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& b){ return a.getColumn() < b.getColumn(); });
// Now we can eliminate entries with the same column by simple addition.
typename FlexibleSparseMatrix<ValueType>::row_type::iterator rowIt = row.begin();
typename FlexibleSparseMatrix<ValueType>::row_type::iterator it = row.begin();
typename FlexibleSparseMatrix<ValueType>::row_type::iterator rowIte = row.end();
for (++it; it != rowIte; ++it) {
if (it->getValue() == storm::utility::constantZero<ValueType>()) {
// First, find the probability with which the predecessor can move to the current state, because
// the other probabilities need to be scaled with this factor.
typename FlexibleSparseMatrix<ValueType>::row_type& predecessorForwardTransitions = matrix.getRow(predecessor);
typename FlexibleSparseMatrix<ValueType>::row_type::iterator multiplyElement = std::find_if(predecessorForwardTransitions.begin(), predecessorForwardTransitions.end(), [&](storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() == state; });
// Make sure we have found the probability and set it to zero.
LOG_THROW(multiplyElement != predecessorForwardTransitions.end(), storm::exceptions::InvalidStateException, "No probability for successor found.");
ValueType multiplyFactor = multiplyElement->getValue();
multiplyElement->setValue(0);
// At this point, we need to update the (forward) transitions of the predecessor.
typename FlexibleSparseMatrix<ValueType>::row_type::iterator first1 = predecessorForwardTransitions.begin();
typename FlexibleSparseMatrix<ValueType>::row_type::iterator last1 = predecessorForwardTransitions.end();
typename FlexibleSparseMatrix<ValueType>::row_type::iterator first2 = currentStateSuccessors.begin();
typename FlexibleSparseMatrix<ValueType>::row_type::iterator last2 = currentStateSuccessors.end();
typename FlexibleSparseMatrix<ValueType>::row_type newSuccessors;
newSuccessors.reserve((last1 - first1) + (last2 - first2));
std::insert_iterator<typename FlexibleSparseMatrix<ValueType>::row_type> result(newSuccessors, newSuccessors.end());
// Now we merge the two successor lists. (Code taken from std::set_union and modified to suit our needs).
for (; first1 != last1; ++result) {
// Skip the transitions to the state that is currently being eliminated.
if (first1->getColumn() == state || (first2 != last2 && first2->getColumn() == state)) {
if (first1->getColumn() == state) {
++first1;
}
if (first2 != last2 && first2->getColumn() == state) {
++first2;
}
continue;
}
if (it->getColumn() == rowIt->getColumn()) {
rowIt->setValue(rowIt->getValue() + it->getValue());
if (first2 == last2) {
std::copy_if(first1, last1, result, [&] (storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() != state; } );
break;
}
if (first2->getColumn() < first1->getColumn()) {
*result = *first2 * multiplyFactor;
++first2;
} else if (first1->getColumn() < first2->getColumn()) {
*result = *first1;
++first1;
} else {
++rowIt;
*rowIt = *it;
*result = storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type>(first1->getColumn(), first1->getValue() + multiplyFactor * first2->getValue());
++first1;
++first2;
}
}
for (; first2 != last2; ++first2) {
if (first2->getColumn() != state) {
*result = *first2 * multiplyFactor;
}
}
// Now move the new transitions in place.
predecessorForwardTransitions = std::move(newSuccessors);
// Finally, add the probabilities to go to a target state in just one step.
std::cout << "prior: " << oneStepProbabilities[predecessorEntry.getColumn()] << std::endl;
oneStepProbabilities[predecessorEntry.getColumn()] += oneStepProbabilities[state];
std::cout << "updating one step prob of " << predecessorEntry.getColumn() << " to " << oneStepProbabilities[predecessorEntry.getColumn()] << std::endl;
// Add the probabilities to go to a target state in just one step.
oneStepProbabilities[predecessor] += multiplyFactor * oneStepProbabilities[state];
}
// Finally, we need to add the predecessor to the set of predecessors of every successor.
for (auto const& successorEntry : currentStateSuccessors) {
typename FlexibleSparseMatrix<ValueType>::row_type& successorBackwardTransitions = backwardTransitions.getRow(successorEntry.getColumn());
// Delete the current state as a predecessor of the successor state.
typename FlexibleSparseMatrix<ValueType>::row_type::const_iterator elimIt = std::find_if(successorBackwardTransitions.begin(), successorBackwardTransitions.end(), [&](storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() == state; });
if (elimIt != successorBackwardTransitions.end()) {
successorBackwardTransitions.erase(elimIt);
}
typename FlexibleSparseMatrix<ValueType>::row_type::iterator first1 = successorBackwardTransitions.begin();
typename FlexibleSparseMatrix<ValueType>::row_type::iterator last1 = successorBackwardTransitions.end();
typename FlexibleSparseMatrix<ValueType>::row_type::iterator first2 = currentStatePredecessors.begin();
typename FlexibleSparseMatrix<ValueType>::row_type::iterator last2 = currentStatePredecessors.end();
typename FlexibleSparseMatrix<ValueType>::row_type newPredecessors;
newPredecessors.reserve((last1 - first1) + (last2 - first2));
std::insert_iterator<typename FlexibleSparseMatrix<ValueType>::row_type> result(newPredecessors, newPredecessors.end());
for (; first1 != last1; ++result) {
if (first2 == last2) {
std::copy_if(first1, last1, result, [&] (storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() != state; });
break;
}
if (first2->getColumn() < first1->getColumn()) {
if (first2->getColumn() != state) {
*result = *first2;
}
++first2;
} else {
if (first1->getColumn() != state) {
*result = *first1;
}
if (first1->getColumn() == first2->getColumn()) {
++first2;
}
++first1;
}
}
std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() != state; });
// Now move the new predecessors in place.
successorBackwardTransitions = std::move(newPredecessors);
}
// Clear the eliminated row to reduce memory consumption.
currentStateSuccessors.clear();
currentStateSuccessors.shrink_to_fit();
}
template<typename ValueType>
@ -201,7 +277,7 @@ namespace storm {
}
template<typename ValueType>
FlexibleSparseMatrix<ValueType> SparseSccModelChecker<ValueType>::getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix) {
FlexibleSparseMatrix<ValueType> SparseSccModelChecker<ValueType>::getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix, bool setAllValuesToOne) {
FlexibleSparseMatrix<ValueType> flexibleMatrix(matrix.getRowCount());
for (typename FlexibleSparseMatrix<ValueType>::index_type rowIndex = 0; rowIndex < matrix.getRowCount(); ++rowIndex) {
@ -209,7 +285,11 @@ namespace storm {
flexibleMatrix.reserveInRow(rowIndex, row.getNumberOfEntries());
for (auto const& element : row) {
flexibleMatrix.getRow(rowIndex).emplace_back(element);
if (setAllValuesToOne) {
flexibleMatrix.getRow(rowIndex).emplace_back(element.getColumn(), storm::utility::constantOne<ValueType>());
} else {
flexibleMatrix.getRow(rowIndex).emplace_back(element);
}
}
}

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

@ -33,9 +33,9 @@ namespace storm {
static ValueType computeReachabilityProbability(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
private:
static void treatScc(storm::models::Dtmc<ValueType> const& dtmc, FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level);
static FlexibleSparseMatrix<ValueType> getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix);
static void eliminateState(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
static void treatScc(storm::models::Dtmc<ValueType> const& dtmc, FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level);
static FlexibleSparseMatrix<ValueType> getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix, bool setAllValuesToOne = false);
static void eliminateState(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix<ValueType>& backwardTransitions);
};
}

12
src/storage/SparseMatrix.cpp
View File

@ -53,6 +53,17 @@ namespace storm {
return this->entry;
}
template<typename IndexType, typename ValueType>
MatrixEntry<IndexType, ValueType> MatrixEntry<IndexType, ValueType>::operator*(value_type factor) const {
return MatrixEntry(this->getColumn(), this->getValue() * factor);
}
template<typename IndexTypePrime, typename ValueTypePrime>
std::ostream& operator<<(std::ostream& out, MatrixEntry<IndexTypePrime, ValueTypePrime> const& entry) {
out << "(" << entry.getColumn() << ", " << entry.getValue() << ")";
return out;
}
template<typename ValueType>
SparseMatrixBuilder<ValueType>::SparseMatrixBuilder(index_type rows, index_type columns, index_type entries, bool forceDimensions, bool hasCustomRowGrouping, index_type rowGroups) : initialRowCountSet(rows != 0), initialRowCount(rows), initialColumnCountSet(columns != 0), initialColumnCount(columns), initialEntryCountSet(entries != 0), initialEntryCount(entries), forceInitialDimensions(forceDimensions), hasCustomRowGrouping(hasCustomRowGrouping), initialRowGroupCountSet(rowGroups != 0), initialRowGroupCount(rowGroups), rowGroupIndices(), columnsAndValues(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0), highestColumn(0), currentRowGroup(0) {
// Prepare the internal storage.
@ -948,6 +959,7 @@ namespace storm {
// Explicitly instantiate the entry, builder and the matrix.
template class MatrixEntry<typename SparseMatrix<double>::index_type, double>;
template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, double> const& entry);
template class SparseMatrixBuilder<double>;
template class SparseMatrix<double>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<double> const& matrix);

9
src/storage/SparseMatrix.h
View File

@ -95,6 +95,15 @@ namespace storm {
*/
std::pair<index_type, value_type> const& getColumnValuePair() const;
/*!
* Multiplies the entry with the given factor and returns the result.
*
* @param factor The factor with which to multiply the entry.
*/
MatrixEntry operator*(value_type factor) const;
template<typename IndexTypePrime, typename ValueTypePrime>
friend std::ostream& operator<<(std::ostream& out, MatrixEntry<IndexTypePrime, ValueTypePrime> const& entry);
private:
// The actual matrix entry.
std::pair<index_type, value_type> entry;

17
src/storm.cpp
View File

@ -102,7 +102,7 @@ int main(const int argc, const char* argv[]) {
initializeLogger();
setUp();
try {
// try {
LOG4CPLUS_INFO(logger, "StoRM was invoked.");
// Parse options.
@ -229,10 +229,11 @@ int main(const int argc, const char* argv[]) {
std::cout << "Parsing and translating the Symbolic Input took " << std::chrono::duration_cast<std::chrono::milliseconds>(programTranslationEnd - programTranslationStart).count() << " milliseconds." << std::endl;
storm::modelchecker::reachability::SparseSccModelChecker<double> modelChecker;
storm::storage::BitVector trueStates(model->getNumberOfStates(), true);
storm::storage::BitVector oneStates = model->getLabeledStates("one");
double value = modelChecker.computeReachabilityProbability(*model->as<storm::models::Dtmc<double>>(), trueStates, oneStates);
storm::storage::BitVector targetStates = model->getLabeledStates("observe0Greater1");
// storm::storage::BitVector targetStates = model->getLabeledStates("one");
// storm::storage::BitVector targetStates = model->getLabeledStates("elected");
double value = modelChecker.computeReachabilityProbability(*model->as<storm::models::Dtmc<double>>(), trueStates, targetStates);
std::cout << "computed value " << value << std::endl;
if (s->isSet("mincmd")) {
@ -319,9 +320,9 @@ int main(const int argc, const char* argv[]) {
printUsage();
LOG4CPLUS_INFO(logger, "StoRM terminating.");
return 0;
} catch (std::exception& e) {
LOG4CPLUS_FATAL(logger, "An exception was thrown. Terminating.");
LOG4CPLUS_FATAL(logger, "\t" << e.what());
}
// } catch (std::exception& e) {
// LOG4CPLUS_FATAL(logger, "An exception was thrown. Terminating.");
// LOG4CPLUS_FATAL(logger, "\t" << e.what());
// }
return 1;
}
Write Preview
Loading…
Cancel
Save