diff --git a/CMakeLists.txt b/CMakeLists.txt index 1a5a9a0bd..ae2c1fa2c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -20,7 +20,7 @@ else() set (STORM_LIB_SUFFIX a) 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_LIBRARIES ${GTEST_LIBRARY}) # as we dont use FindGTest anymore + set (GTEST_LIBRARIES ${GTEST_LIBRARY} ${GTEST_MAIN_LIBRARY}) # as we dont use FindGTest anymore endif() message(STATUS "GTEST_INCLUDE_DIR is ${GTEST_INCLUDE_DIR}") 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_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_IR_FILES ${PROJECT_SOURCE_DIR}/src/ir/*.h ${PROJECT_SOURCE_DIR}/src/ir/*.cpp) # Test Sources # 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(storage FILES ${STORM_STORAGE_FILES}) source_group(utility FILES ${STORM_UTILITY_FILES}) +source_group(ir FILES ${STORM_IR_FILES}) source_group(test FILES ${STORM_TEST_FILES}) # Add base folder for better inclusion paths diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index f7594ba05..7048ab3ed 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -47,44 +47,23 @@ class AbstractDeterministicModel: public AbstractModel { } /*! - * 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 extractSccDependencyGraph(std::vector> const& stronglyConnectedComponents, std::map 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 sccDependencyGraph(numberOfStates); - sccDependencyGraph.initialize(); - - for (uint_fast64_t currentSccIndex = 0; currentSccIndex < stronglyConnectedComponents.size(); ++currentSccIndex) { - // Get the actual SCC. - std::vector const& scc = stronglyConnectedComponents[currentSccIndex]; - - // Now, we determine the SCCs which are reachable (in one step) from the current SCC. - std::set allTargetSccs; - for (auto state : scc) { - for (typename storm::storage::SparseMatrix::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); - - return sccDependencyGraph; + virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) { + return this->getTransitionMatrix()->constColumnIteratorBegin(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::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) { + return this->getTransitionMatrix()->constColumnIteratorEnd(state); } }; diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 364e501b0..e50aa683f 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -91,7 +91,56 @@ class AbstractModel: public std::enable_shared_from_this> { * @param stronglyConnectedComponents A vector containing the SCCs of the system. * @param stateToSccMap A mapping from state indices to */ - virtual storm::storage::SparseMatrix extractSccDependencyGraph(std::vector> const& stronglyConnectedComponents, std::map const& stateToSccMap) = 0; + virtual storm::storage::SparseMatrix extractSccDependencyGraph(std::vector> const& stronglyConnectedComponents, std::map 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 sccDependencyGraph(numberOfStates); + sccDependencyGraph.initialize(); + + for (uint_fast64_t currentSccIndex = 0; currentSccIndex < stronglyConnectedComponents.size(); ++currentSccIndex) { + // Get the actual SCC. + std::vector const& scc = stronglyConnectedComponents[currentSccIndex]; + + // Now, we determine the SCCs which are reachable (in one step) from the current SCC. + std::set allTargetSccs; + for (auto state : scc) { + for (typename storm::storage::SparseMatrix::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::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::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) = 0; /*! * Returns the state space size of the model. diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index 4c51f0863..cd2700a49 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -58,49 +58,6 @@ class AbstractNondeterministicModel: public AbstractModel { uint_fast64_t getNumberOfChoices() const { 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 extractSccDependencyGraph(std::vector> const& stronglyConnectedComponents, std::map 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 sccDependencyGraph(numberOfStates); - sccDependencyGraph.initialize(); - - for (uint_fast64_t currentSccIndex = 0; currentSccIndex < stronglyConnectedComponents.size(); ++currentSccIndex) { - // Get the actual SCC. - std::vector const& scc = stronglyConnectedComponents[currentSccIndex]; - - // Now, we determine the SCCs which are reachable (in one step) from the current SCC. - std::set allTargetSccs; - for (auto state : scc) { - for (uint_fast64_t rowIndex = (*nondeterministicChoiceIndices)[state]; rowIndex < (*nondeterministicChoiceIndices)[state + 1]; ++rowIndex) { - for (typename storm::storage::SparseMatrix::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. @@ -120,6 +77,26 @@ class AbstractNondeterministicModel: public AbstractModel { std::shared_ptr> getNondeterministicChoiceIndices() const { 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::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::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) { + return this->getTransitionMatrix()->constColumnIteratorEnd((*nondeterministicChoiceIndices)[state + 1] - 1); + } private: /*! A vector of indices mapping states to the choices (rows) in the transition matrix. */