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

Moved SCC decomposition to AbstractModel class, which was possible due to virtual iterator facilities in model classes.

tempestpy_adaptions
dehnert 12 years ago
parent
6aea8de7ba
commit
5f27a932a9
4 changed files with 88 additions and 81 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. 4
      CMakeLists.txt
  2. 49
      src/models/AbstractDeterministicModel.h
  3. 51
      src/models/AbstractModel.h
  4. 63
      src/models/AbstractNondeterministicModel.h

4
CMakeLists.txt
View File

@ -20,7 +20,7 @@ else()
set (STORM_LIB_SUFFIX a) set (STORM_LIB_SUFFIX a)
set (GTEST_LIBRARY ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/libgtest.${STORM_LIB_SUFFIX}) set (GTEST_LIBRARY ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/libgtest.${STORM_LIB_SUFFIX})
set (GTEST_MAIN_LIBRARY ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/libgtest_main.${STORM_LIB_SUFFIX}) set (GTEST_MAIN_LIBRARY ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/libgtest_main.${STORM_LIB_SUFFIX})
set (GTEST_LIBRARIES ${GTEST_LIBRARY}) # as we dont use FindGTest anymore
set (GTEST_LIBRARIES ${GTEST_LIBRARY} ${GTEST_MAIN_LIBRARY}) # as we dont use FindGTest anymore
endif() endif()
message(STATUS "GTEST_INCLUDE_DIR is ${GTEST_INCLUDE_DIR}") message(STATUS "GTEST_INCLUDE_DIR is ${GTEST_INCLUDE_DIR}")
message(STATUS "GTEST_LIBRARY is ${GTEST_LIBRARY}") message(STATUS "GTEST_LIBRARY is ${GTEST_LIBRARY}")
@ -126,6 +126,7 @@ file(GLOB_RECURSE STORM_MODELS_FILES ${PROJECT_SOURCE_DIR}/src/models/*.h ${PROJ
file(GLOB_RECURSE STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOURCE_DIR}/src/parser/*.cpp) file(GLOB_RECURSE STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOURCE_DIR}/src/parser/*.cpp)
file(GLOB_RECURSE STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp) file(GLOB_RECURSE STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp)
file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PROJECT_SOURCE_DIR}/src/utility/*.cpp) file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PROJECT_SOURCE_DIR}/src/utility/*.cpp)
file(GLOB_RECURSE STORM_IR_FILES ${PROJECT_SOURCE_DIR}/src/ir/*.h ${PROJECT_SOURCE_DIR}/src/ir/*.cpp)
# Test Sources # Test Sources
# Note that the tests also need the source files, except for the main file # Note that the tests also need the source files, except for the main file
@ -141,6 +142,7 @@ source_group(models FILES ${STORM_MODELS_FILES})
source_group(parser FILES ${STORM_PARSER_FILES}) source_group(parser FILES ${STORM_PARSER_FILES})
source_group(storage FILES ${STORM_STORAGE_FILES}) source_group(storage FILES ${STORM_STORAGE_FILES})
source_group(utility FILES ${STORM_UTILITY_FILES}) source_group(utility FILES ${STORM_UTILITY_FILES})
source_group(ir FILES ${STORM_IR_FILES})
source_group(test FILES ${STORM_TEST_FILES}) source_group(test FILES ${STORM_TEST_FILES})
# Add base folder for better inclusion paths # Add base folder for better inclusion paths

49
src/models/AbstractDeterministicModel.h
View File

@ -47,44 +47,23 @@ class AbstractDeterministicModel: public AbstractModel<T> {
} }
/*! /*!
* Extracts the SCC dependency graph from the model according to the given SCC decomposition.
* Returns an iterator to the successors of the given state.
* *
* @param stronglyConnectedComponents A vector containing the SCCs of the system.
* @param stateToSccMap A mapping from state indices to
* @param state The state for which to return the iterator.
* @return An iterator to the successors of the given state.
*/ */
virtual storm::storage::SparseMatrix<bool> extractSccDependencyGraph(std::vector<std::vector<uint_fast64_t>> const& stronglyConnectedComponents, std::map<uint_fast64_t, uint_fast64_t> const& stateToSccMap) {
// The resulting sparse matrix will have as many rows/columns as there are SCCs.
uint_fast64_t numberOfStates = stronglyConnectedComponents.size();
storm::storage::SparseMatrix<bool> sccDependencyGraph(numberOfStates);
sccDependencyGraph.initialize();
for (uint_fast64_t currentSccIndex = 0; currentSccIndex < stronglyConnectedComponents.size(); ++currentSccIndex) {
// Get the actual SCC.
std::vector<uint_fast64_t> const& scc = stronglyConnectedComponents[currentSccIndex];
// Now, we determine the SCCs which are reachable (in one step) from the current SCC.
std::set<uint_fast64_t> allTargetSccs;
for (auto state : scc) {
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator succIt = this->getTransitionMatrix()->constColumnIteratorBegin(state), succIte = this->getTransitionMatrix()->constColumnIteratorEnd(state); succIt != succIte; ++succIt) {
uint_fast64_t targetScc = stateToSccMap.find(*succIt)->second;
// We only need to consider transitions that are actually leaving the SCC.
if (targetScc != currentSccIndex) {
allTargetSccs.insert(targetScc);
}
}
}
// Now we can just enumerate all the target SCCs and insert the corresponding transitions.
for (auto targetScc : allTargetSccs) {
sccDependencyGraph.insertNextValue(currentSccIndex, targetScc, true);
}
}
// Finalize the matrix.
sccDependencyGraph.finalize(true);
virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) {
return this->getTransitionMatrix()->constColumnIteratorBegin(state);
}
return sccDependencyGraph;
/*!
* Returns an iterator pointing to the element past the successors of the given state.
*
* @param state The state for which to return the iterator.
* @return An iterator pointing to the element past the successors of the given state.
*/
virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) {
return this->getTransitionMatrix()->constColumnIteratorEnd(state);
} }
}; };

51
src/models/AbstractModel.h
View File

@ -91,7 +91,56 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
* @param stronglyConnectedComponents A vector containing the SCCs of the system. * @param stronglyConnectedComponents A vector containing the SCCs of the system.
* @param stateToSccMap A mapping from state indices to * @param stateToSccMap A mapping from state indices to
*/ */
virtual storm::storage::SparseMatrix<bool> extractSccDependencyGraph(std::vector<std::vector<uint_fast64_t>> const& stronglyConnectedComponents, std::map<uint_fast64_t, uint_fast64_t> const& stateToSccMap) = 0;
virtual storm::storage::SparseMatrix<bool> extractSccDependencyGraph(std::vector<std::vector<uint_fast64_t>> const& stronglyConnectedComponents, std::map<uint_fast64_t, uint_fast64_t> const& stateToSccMap) {
// The resulting sparse matrix will have as many rows/columns as there are SCCs.
uint_fast64_t numberOfStates = stronglyConnectedComponents.size();
storm::storage::SparseMatrix<bool> sccDependencyGraph(numberOfStates);
sccDependencyGraph.initialize();
for (uint_fast64_t currentSccIndex = 0; currentSccIndex < stronglyConnectedComponents.size(); ++currentSccIndex) {
// Get the actual SCC.
std::vector<uint_fast64_t> const& scc = stronglyConnectedComponents[currentSccIndex];
// Now, we determine the SCCs which are reachable (in one step) from the current SCC.
std::set<uint_fast64_t> allTargetSccs;
for (auto state : scc) {
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator succIt = this->constStateSuccessorIteratorBegin(state), succIte = this->constStateSuccessorIteratorEnd(state); succIt != succIte; ++succIt) {
uint_fast64_t targetScc = stateToSccMap.find(*succIt)->second;
// We only need to consider transitions that are actually leaving the SCC.
if (targetScc != currentSccIndex) {
allTargetSccs.insert(targetScc);
}
}
}
// Now we can just enumerate all the target SCCs and insert the corresponding transitions.
for (auto targetScc : allTargetSccs) {
sccDependencyGraph.insertNextValue(currentSccIndex, targetScc, true);
}
}
// Finalize the matrix.
sccDependencyGraph.finalize(true);
return sccDependencyGraph;
}
/*!
* Returns an iterator to the successors of the given state.
*
* @param state The state for which to return the iterator.
* @return An iterator to the successors of the given state.
*/
virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) = 0;
/*!
* Returns an iterator pointing to the element past the successors of the given state.
*
* @param state The state for which to return the iterator.
* @return An iterator pointing to the element past the successors of the given state.
*/
virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) = 0;
/*! /*!
* Returns the state space size of the model. * Returns the state space size of the model.

63
src/models/AbstractNondeterministicModel.h
View File

@ -59,49 +59,6 @@ class AbstractNondeterministicModel: public AbstractModel<T> {
return this->getTransitionMatrix()->getRowCount(); return this->getTransitionMatrix()->getRowCount();
} }
/*!
* Extracts the SCC dependency graph from the model according to the given SCC decomposition.
*
* @param stronglyConnectedComponents A vector containing the SCCs of the system.
* @param stateToSccMap A mapping from state indices to
*/
virtual storm::storage::SparseMatrix<bool> extractSccDependencyGraph(std::vector<std::vector<uint_fast64_t>> const& stronglyConnectedComponents, std::map<uint_fast64_t, uint_fast64_t> const& stateToSccMap) {
// The resulting sparse matrix will have as many rows/columns as there are SCCs.
uint_fast64_t numberOfStates = stronglyConnectedComponents.size();
storm::storage::SparseMatrix<bool> sccDependencyGraph(numberOfStates);
sccDependencyGraph.initialize();
for (uint_fast64_t currentSccIndex = 0; currentSccIndex < stronglyConnectedComponents.size(); ++currentSccIndex) {
// Get the actual SCC.
std::vector<uint_fast64_t> const& scc = stronglyConnectedComponents[currentSccIndex];
// Now, we determine the SCCs which are reachable (in one step) from the current SCC.
std::set<uint_fast64_t> allTargetSccs;
for (auto state : scc) {
for (uint_fast64_t rowIndex = (*nondeterministicChoiceIndices)[state]; rowIndex < (*nondeterministicChoiceIndices)[state + 1]; ++rowIndex) {
for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator succIt = this->getTransitionMatrix()->constColumnIteratorBegin(rowIndex), succIte = this->getTransitionMatrix()->constColumnIteratorEnd(rowIndex); succIt != succIte; ++succIt) {
uint_fast64_t targetScc = stateToSccMap.find(*succIt)->second;
// We only need to consider transitions that are actually leaving the SCC.
if (targetScc != currentSccIndex) {
allTargetSccs.insert(targetScc);
}
}
}
}
// Now we can just enumerate all the target SCCs and insert the corresponding transitions.
for (auto targetScc : allTargetSccs) {
sccDependencyGraph.insertNextValue(currentSccIndex, targetScc, true);
}
}
// Finalize the matrix.
sccDependencyGraph.finalize(true);
return sccDependencyGraph;
}
/*! /*!
* Retrieves the size of the internal representation of the model in memory. * Retrieves the size of the internal representation of the model in memory.
* @return the size of the internal representation of the model in memory * @return the size of the internal representation of the model in memory
@ -121,6 +78,26 @@ class AbstractNondeterministicModel: public AbstractModel<T> {
return nondeterministicChoiceIndices; return nondeterministicChoiceIndices;
} }
/*!
* Returns an iterator to the successors of the given state.
*
* @param state The state for which to return the iterator.
* @return An iterator to the successors of the given state.
*/
virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) {
return this->getTransitionMatrix()->constColumnIteratorBegin((*nondeterministicChoiceIndices)[state]);
}
/*!
* Returns an iterator pointing to the element past the successors of the given state.
*
* @param state The state for which to return the iterator.
* @return An iterator pointing to the element past the successors of the given state.
*/
virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) {
return this->getTransitionMatrix()->constColumnIteratorEnd((*nondeterministicChoiceIndices)[state + 1] - 1);
}
private: private:
/*! A vector of indices mapping states to the choices (rows) in the transition matrix. */ /*! A vector of indices mapping states to the choices (rows) in the transition matrix. */
std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices; std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices;

Write Preview
Loading…
Cancel
Save