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

Made the SCC generation during decomposition optional.

tempestpy_adaptions
dehnert 12 years ago
parent
961909877a
commit
aee63dcf31
1 changed files with 16 additions and 11 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 25
      src/utility/GraphAnalyzer.h

25
src/utility/GraphAnalyzer.h
View File

@ -417,21 +417,22 @@ public:
} }
template <typename T> template <typename T>
static uint_fast64_t performSccDecomposition(storm::models::AbstractNondeterministicModel<T>& model, std::vector<std::vector<uint_fast64_t>>& stronglyConnectedComponents) {
LOG4CPLUS_INFO(logger, "Computing SCC decomposition...");
static uint_fast64_t performSccDecomposition(storm::models::AbstractNondeterministicModel<T>& model, std::vector<std::vector<uint_fast64_t>*>* stronglyConnectedComponents) {
LOG4CPLUS_INFO(logger, "Computing SCC decomposition.");
// Get the forward transition relation from the model to ease the search. // Get the forward transition relation from the model to ease the search.
storm::models::GraphTransitions<T> forwardTransitions(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), true); storm::models::GraphTransitions<T> forwardTransitions(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), true);
// Perform the actual SCC decomposition based on the graph-transitions of the system. // Perform the actual SCC decomposition based on the graph-transitions of the system.
performSccDecomposition(model.getNumberOfStates(), model.getLabeledStates("init"), forwardTransitions, stronglyConnectedComponents);
uint_fast64_t result = performSccDecomposition(model.getNumberOfStates(), *model.getLabeledStates("init"), forwardTransitions, stronglyConnectedComponents);
LOG4CPLUS_INFO(logger, "Done computing SCCs.");
LOG4CPLUS_INFO(logger, "Done computing SCC decomposition.");
return result;
} }
private: private:
template <typename T> template <typename T>
static uint_fast64_t performSccDecomposition(uint_fast64_t numberOfStates, storm::storage::BitVector const* const initialStates, storm::models::GraphTransitions<T> const& forwardTransitions, std::vector<std::vector<uint_fast64_t>>& stronglyConnectedComponents) {
static uint_fast64_t performSccDecomposition(uint_fast64_t numberOfStates, storm::storage::BitVector const& initialStates, storm::models::GraphTransitions<T> const& forwardTransitions, std::vector<std::vector<uint_fast64_t>*>* stronglyConnectedComponents) {
std::vector<uint_fast64_t> tarjanStack; std::vector<uint_fast64_t> tarjanStack;
tarjanStack.reserve(numberOfStates); tarjanStack.reserve(numberOfStates);
storm::storage::BitVector tarjanStackStates(numberOfStates); storm::storage::BitVector tarjanStackStates(numberOfStates);
@ -441,17 +442,17 @@ private:
storm::storage::BitVector visitedStates(numberOfStates); storm::storage::BitVector visitedStates(numberOfStates);
uint_fast64_t currentIndex = 0; uint_fast64_t currentIndex = 0;
for (auto state : *initialStates) {
for (auto state : initialStates) {
if (!visitedStates.get(state)) { if (!visitedStates.get(state)) {
performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, forwardTransitions, stronglyConnectedComponents); performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, forwardTransitions, stronglyConnectedComponents);
} }
} }
return stronglyConnectedComponents.size();
return stronglyConnectedComponents->size();
} }
template <typename T> template <typename T>
static void performSccDecompositionHelper(uint_fast64_t startState, uint_fast64_t& currentIndex, std::vector<uint_fast64_t>& stateIndices, std::vector<uint_fast64_t>& lowlinks, std::vector<uint_fast64_t>& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, storm::models::GraphTransitions<T>& forwardTransitions, std::vector<std::vector<uint_fast64_t>>& stronglyConnectedComponents) {
static void performSccDecompositionHelper(uint_fast64_t startState, uint_fast64_t& currentIndex, std::vector<uint_fast64_t>& stateIndices, std::vector<uint_fast64_t>& lowlinks, std::vector<uint_fast64_t>& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, storm::models::GraphTransitions<T> const& forwardTransitions, std::vector<std::vector<uint_fast64_t>*>* stronglyConnectedComponents) {
// Create the stacks needed for turning the recursive formulation of Tarjan's algorithm // Create the stacks needed for turning the recursive formulation of Tarjan's algorithm
// into an iterative version. In particular, we keep one stack for states and one stack // into an iterative version. In particular, we keep one stack for states and one stack
// for the iterators. The last one is not strictly needed, but reduces iteration work when // for the iterators. The last one is not strictly needed, but reduces iteration work when
@ -507,7 +508,9 @@ private:
// If the current state is the root of a SCC, we need to pop all states of the SCC from // If the current state is the root of a SCC, we need to pop all states of the SCC from
// the algorithm's stack. // the algorithm's stack.
if (lowlinks[currentState] == stateIndices[currentState]) { if (lowlinks[currentState] == stateIndices[currentState]) {
stronglyConnectedComponents.push_back(std::vector<uint_fast64_t>());
if (stronglyConnectedComponents != nullptr) {
stronglyConnectedComponents->push_back(new std::vector<uint_fast64_t>());
}
uint_fast64_t lastState = 0; uint_fast64_t lastState = 0;
do { do {
@ -516,8 +519,10 @@ private:
tarjanStack.pop_back(); tarjanStack.pop_back();
tarjanStackStates.set(lastState, false); tarjanStackStates.set(lastState, false);
if (stronglyConnectedComponents != nullptr) {
// Add the state to the current SCC. // Add the state to the current SCC.
stronglyConnectedComponents.back().push_back(lastState);
stronglyConnectedComponents->back()->push_back(lastState);
}
} while (lastState != currentState); } while (lastState != currentState);
} }

Write Preview
Loading…
Cancel
Save