diff --git a/CMakeLists.txt b/CMakeLists.txt index 5c71fb44e..cd069197c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,25 +1,25 @@ cmake_minimum_required (VERSION 2.6) # Set project name -project (mrmc CXX C) +project (storm CXX C) # Set the version number -set (MRMC_CPP_VERSION_MAJOR 1) -set (MRMC_CPP_VERSION_MINOR 0) +set (STORM_CPP_VERSION_MAJOR 1) +set (STORM_CPP_VERSION_MINOR 0) # Set all GTest references to the version in the repository and show it as output set (GTEST_INCLUDE_DIR resources/3rdparty/gtest-1.6.0/include) if(MSVC) - set (MRMC_LIB_SUFFIX lib) - set (GTEST_LIBRARY_DEBUG ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/build/Debug/gtest.${MRMC_LIB_SUFFIX}) - set (GTEST_MAIN_LIBRARY_DEBUG ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/build/Debug/gtest_main.${MRMC_LIB_SUFFIX}) - set (GTEST_LIBRARY ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/build/Release/gtest.${MRMC_LIB_SUFFIX}) - set (GTEST_MAIN_LIBRARY ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/build/Release/gtest_main.${MRMC_LIB_SUFFIX}) + set (STORM_LIB_SUFFIX lib) + set (GTEST_LIBRARY_DEBUG ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/build/Debug/gtest.${STORM_LIB_SUFFIX}) + set (GTEST_MAIN_LIBRARY_DEBUG ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/build/Debug/gtest_main.${STORM_LIB_SUFFIX}) + set (GTEST_LIBRARY ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/build/Release/gtest.${STORM_LIB_SUFFIX}) + set (GTEST_MAIN_LIBRARY ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/build/Release/gtest_main.${STORM_LIB_SUFFIX}) set (GTEST_LIBRARIES optimized ${GTEST_LIBRARY} debug ${GTEST_LIBRARY_DEBUG}) else() - set (MRMC_LIB_SUFFIX a) - set (GTEST_LIBRARY ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/libgtest.${MRMC_LIB_SUFFIX}) - set (GTEST_MAIN_LIBRARY ${PROJECT_SOURCE_DIR}/resources/3rdparty/gtest-1.6.0/libgtest_main.${MRMC_LIB_SUFFIX}) + 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 endif() message(STATUS "GTEST_INCLUDE_DIR is ${GTEST_INCLUDE_DIR}") @@ -29,9 +29,9 @@ message(STATUS "GTEST_MAIN_LIBRARY is ${GTEST_MAIN_LIBRARY}") # Set all log4cplus references the version in the repository set (LOG4CPLUS_INCLUDE_DIR ${PROJECT_SOURCE_DIR}/resources/3rdparty/log4cplus-1.1.0/include) if (MSVC) - set (LOG4CPLUS_LIBRARIES optimized ${PROJECT_SOURCE_DIR}/resources/3rdparty/log4cplus-1.1.0/msvc10/x64/bin.Release/log4cplusS.${MRMC_LIB_SUFFIX} debug ${PROJECT_SOURCE_DIR}/resources/3rdparty/log4cplus-1.1.0/msvc10/x64/bin.Debug/log4cplusSD.${MRMC_LIB_SUFFIX}) + set (LOG4CPLUS_LIBRARIES optimized ${PROJECT_SOURCE_DIR}/resources/3rdparty/log4cplus-1.1.0/msvc10/x64/bin.Release/log4cplusS.${STORM_LIB_SUFFIX} debug ${PROJECT_SOURCE_DIR}/resources/3rdparty/log4cplus-1.1.0/msvc10/x64/bin.Debug/log4cplusSD.${STORM_LIB_SUFFIX}) else() - set (LOG4CPLUS_LIBRARIES ${PROJECT_SOURCE_DIR}/resources/3rdparty/log4cplus-1.1.0/src/liblog4cplus.${MRMC_LIB_SUFFIX}) + set (LOG4CPLUS_LIBRARIES ${PROJECT_SOURCE_DIR}/resources/3rdparty/log4cplus-1.1.0/src/liblog4cplus.${STORM_LIB_SUFFIX}) endif() message(STATUS "LOG4CPLUS_INCLUDE_DIR is ${LOG4CPLUS_INCLUDE_DIR}") message(STATUS "LOG4CPLUS_LIBRARY is ${LOG4CPLUS_LIBRARIES}") @@ -82,29 +82,29 @@ else(CLANG) endif(USE_POPCNT) endif() -# Add the binary folder to the search path for include files so that we will find mrmc-config.h +# Add the binary folder to the search path for include files so that we will find storm-config.h include_directories("${PROJECT_BINARY_DIR}") # Base path for test files -set(MRMC_CPP_TESTS_BASE_PATH ${PROJECT_SOURCE_DIR}/test) -message(STATUS "MRMC_CPP_TESTS_BASE_PATH is ${MRMC_CPP_TESTS_BASE_PATH}") +set(STORM_CPP_TESTS_BASE_PATH ${PROJECT_SOURCE_DIR}/test) +message(STATUS "STORM_CPP_TESTS_BASE_PATH is ${STORM_CPP_TESTS_BASE_PATH}") # Main Sources -file(GLOB_RECURSE MRMC_HEADERS ${PROJECT_SOURCE_DIR}/src/*.h) -file(GLOB_RECURSE MRMC_SOURCES ${PROJECT_SOURCE_DIR}/src/*.cpp) +file(GLOB_RECURSE STORM_HEADERS ${PROJECT_SOURCE_DIR}/src/*.h) +file(GLOB_RECURSE STORM_SOURCES ${PROJECT_SOURCE_DIR}/src/*.cpp) # Test Sources # Note that the tests also need the source files, except for the main file -file(GLOB_RECURSE MRMC_TEST_HEADERS ${PROJECT_SOURCE_DIR}/test/*.h) -file(GLOB_RECURSE MRMC_TEST_SOURCES ${PROJECT_SOURCE_DIR}/test/*.cpp ${PROJECT_SOURCE_DIR}/src/*/*.cpp) +file(GLOB_RECURSE STORM_TEST_HEADERS ${PROJECT_SOURCE_DIR}/test/*.h) +file(GLOB_RECURSE STORM_TEST_SOURCES ${PROJECT_SOURCE_DIR}/test/*.cpp ${PROJECT_SOURCE_DIR}/src/*/*.cpp) # Main Grouping -source_group(Headers FILES ${MRMC_HEADERS}) -source_group(Sources FILES ${MRMC_SOURCES}) +source_group(Headers FILES ${STORM_HEADERS}) +source_group(Sources FILES ${STORM_SOURCES}) # Test Grouping -source_group(Headers FILES ${MRMC_TEST_HEADERS}) -source_group(Sources FILES ${MRMC_TEST_SOURCES}) +source_group(Headers FILES ${STORM_TEST_HEADERS}) +source_group(Sources FILES ${STORM_TEST_SOURCES}) # Add base folder for better inclusion paths include_directories("${PROJECT_SOURCE_DIR}") @@ -138,12 +138,12 @@ include_directories(${GMMXX_INCLUDE_DIR}) # Add the executables # Must be created *after* Boost was added because of LINK_DIRECTORIES -add_executable(mrmc ${MRMC_SOURCES} ${MRMC_HEADERS}) -add_executable(mrmc-tests ${MRMC_TEST_SOURCES} ${MRMC_TEST_HEADERS}) +add_executable(storm ${STORM_SOURCES} ${STORM_HEADERS}) +add_executable(storm-tests ${STORM_TEST_SOURCES} ${STORM_TEST_HEADERS}) # Add target link deps for Boost program options -target_link_libraries(mrmc ${Boost_LIBRARIES}) -target_link_libraries(mrmc-tests ${Boost_LIBRARIES}) +target_link_libraries(storm ${Boost_LIBRARIES}) +target_link_libraries(storm-tests ${Boost_LIBRARIES}) # Add a target to generate API documentation with Doxygen if(DOXYGEN_FOUND) @@ -161,9 +161,9 @@ if (GTEST_INCLUDE_DIR) enable_testing() include_directories(${GTEST_INCLUDE_DIR}) - target_link_libraries(mrmc-tests ${GTEST_LIBRARIES}) + target_link_libraries(storm-tests ${GTEST_LIBRARIES}) - add_test(NAME mrmc-tests COMMAND mrmc-tests) + add_test(NAME storm-tests COMMAND storm-tests) if(MSVC) # VS2012 doesn't support correctly the tuples yet add_definitions( /D _VARIADIC_MAX=10 ) endif() @@ -171,29 +171,29 @@ endif(GTEST_INCLUDE_DIR) if (LOG4CPLUS_INCLUDE_DIR) include_directories(${LOG4CPLUS_INCLUDE_DIR}) - target_link_libraries(mrmc ${LOG4CPLUS_LIBRARIES}) - target_link_libraries(mrmc-tests ${LOG4CPLUS_LIBRARIES}) + target_link_libraries(storm ${LOG4CPLUS_LIBRARIES}) + target_link_libraries(storm-tests ${LOG4CPLUS_LIBRARIES}) # On Linux, we have to link against librt if (UNIX AND NOT APPLE) - target_link_libraries(mrmc rt) - target_link_libraries(mrmc-tests rt) + target_link_libraries(storm rt) + target_link_libraries(storm-tests rt) endif(UNIX AND NOT APPLE) endif(LOG4CPLUS_INCLUDE_DIR) if (THREADS_FOUND) include_directories(${THREADS_INCLUDE_DIRS}) - target_link_libraries (mrmc ${CMAKE_THREAD_LIBS_INIT}) - target_link_libraries (mrmc-tests ${CMAKE_THREAD_LIBS_INIT}) + target_link_libraries (storm ${CMAKE_THREAD_LIBS_INIT}) + target_link_libraries (storm-tests ${CMAKE_THREAD_LIBS_INIT}) endif(THREADS_FOUND) # Configure a header file to pass some of the CMake settings to the source code configure_file ( - "${PROJECT_SOURCE_DIR}/mrmc-config.h.in" - "${PROJECT_BINARY_DIR}/mrmc-config.h" + "${PROJECT_SOURCE_DIR}/storm-config.h.in" + "${PROJECT_BINARY_DIR}/storm-config.h" ) -add_custom_target(memcheck valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/mrmc ${PROJECT_SOURCE_DIR}/examples/dtmc/crowds/crowds5_5.tra examples/dtmc/crowds/crowds5_5.lab - DEPENDS mrmc) -add_custom_target(memcheck-tests valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/mrmc-tests - DEPENDS mrmc-tests) +add_custom_target(memcheck valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm ${PROJECT_SOURCE_DIR}/examples/dtmc/crowds/crowds5_5.tra examples/dtmc/crowds/crowds5_5.lab + DEPENDS storm) +add_custom_target(memcheck-tests valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm-tests + DEPENDS storm-tests) diff --git a/doc/Doxyfile.in b/doc/Doxyfile.in index d1f2cf7b4..a328991e3 100644 --- a/doc/Doxyfile.in +++ b/doc/Doxyfile.in @@ -26,7 +26,7 @@ DOXYFILE_ENCODING = UTF-8 # identify the project. Note that if you do not use Doxywizard you need # to put quotes around the project name if it contains spaces. -PROJECT_NAME = "MRMC C++" +PROJECT_NAME = "STORM" # The PROJECT_NUMBER tag can be used to enter a project or revision number. # This could be handy for archiving the generated documentation or diff --git a/mrmc-config.h.in b/mrmc-config.h.in deleted file mode 100644 index 5546d324b..000000000 --- a/mrmc-config.h.in +++ /dev/null @@ -1,4 +0,0 @@ -// the configured options and settings for MRMC_CPP -#define MRMC_CPP_VERSION_MAJOR @MRMC_CPP_VERSION_MAJOR@ -#define MRMC_CPP_VERSION_MINOR @MRMC_CPP_VERSION_MINOR@ -#define MRMC_CPP_TESTS_BASE_PATH "@MRMC_CPP_TESTS_BASE_PATH@" \ No newline at end of file diff --git a/resources/BUILD.txt b/resources/BUILD.txt index e6e7d9769..aa1934a44 100644 --- a/resources/BUILD.txt +++ b/resources/BUILD.txt @@ -26,4 +26,4 @@ Prerequisites: The other fields should be auto completed after to next "Configure" round If no error occured during the last CMake Configure round, press Generate. -Now you can build MRMC-Cpp using the generated project/makefiles in the Build folder you selected. \ No newline at end of file +Now you can build STORM using the generated project/makefiles in the Build folder you selected. \ No newline at end of file diff --git a/resources/GUIDELINES.txt b/resources/GUIDELINES.txt index 86dd3e9b2..201c51c68 100644 --- a/resources/GUIDELINES.txt +++ b/resources/GUIDELINES.txt @@ -1,4 +1,4 @@ -/* ---------------------------------- GUIDELINES FOR MRMC DEVELOPMENT ---------------------------------- */ +/* ---------------------------------- GUIDELINES FOR STORM DEVELOPMENT ---------------------------------- */ In general, we adhere to the Google Styleguide for C++, found under http://google-styleguide.googlecode.com/svn/trunk/cppguide.xml diff --git a/src/adapters/GmmxxAdapter.h b/src/adapters/GmmxxAdapter.h index ed3f2a893..43a3f8302 100644 --- a/src/adapters/GmmxxAdapter.h +++ b/src/adapters/GmmxxAdapter.h @@ -15,7 +15,7 @@ extern log4cplus::Logger logger; -namespace mrmc { +namespace storm { namespace adapters { @@ -26,7 +26,7 @@ public: * @return A pointer to a column-major sparse matrix in gmm++ format. */ template - static gmm::csr_matrix* toGmmxxSparseMatrix(mrmc::storage::SquareSparseMatrix const& matrix) { + static gmm::csr_matrix* toGmmxxSparseMatrix(storm::storage::SquareSparseMatrix const& matrix) { uint_fast64_t realNonZeros = matrix.getNonZeroEntryCount() + matrix.getDiagonalNonZeroEntryCount(); LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to gmm++ format."); @@ -103,6 +103,6 @@ public: } //namespace adapters -} //namespace mrmc +} //namespace storm #endif /* GMMXXADAPTER_H_ */ diff --git a/src/exceptions/BaseException.h b/src/exceptions/BaseException.h index d8767e8d9..d3f9308ff 100644 --- a/src/exceptions/BaseException.h +++ b/src/exceptions/BaseException.h @@ -1,10 +1,10 @@ -#ifndef MRMC_EXCEPTIONS_BASEEXCEPTION_H_ -#define MRMC_EXCEPTIONS_BASEEXCEPTION_H_ +#ifndef STORM_EXCEPTIONS_BASEEXCEPTION_H_ +#define STORM_EXCEPTIONS_BASEEXCEPTION_H_ #include #include -namespace mrmc { +namespace storm { namespace exceptions { template @@ -40,12 +40,12 @@ class BaseException : public std::exception }; } // namespace exceptions -} // namespace mrmc +} // namespace storm /* Macro to generate descendant exception classes. * As all classes are nearly the same, this makes changing common features much easier. */ -#define MRMC_EXCEPTION_DEFINE_NEW(exception_name) class exception_name : public BaseException { \ +#define STORM_EXCEPTION_DEFINE_NEW(exception_name) class exception_name : public BaseException { \ public: \ exception_name() : BaseException() { \ } \ @@ -56,4 +56,4 @@ public: \ }; -#endif // MRMC_EXCEPTIONS_BASEEXCEPTION_H_ +#endif // STORM_EXCEPTIONS_BASEEXCEPTION_H_ diff --git a/src/exceptions/FileIoException.h b/src/exceptions/FileIoException.h index 0d31af7fd..2d7e63d47 100644 --- a/src/exceptions/FileIoException.h +++ b/src/exceptions/FileIoException.h @@ -5,19 +5,19 @@ * Author: Thomas Heinemann */ -#ifndef MRMC_EXCEPTIONS_FILEIOEXCEPTION_H_ -#define MRMC_EXCEPTIONS_FILEIOEXCEPTION_H_ +#ifndef STORM_EXCEPTIONS_FILEIOEXCEPTION_H_ +#define STORM_EXCEPTIONS_FILEIOEXCEPTION_H_ #include "src/exceptions/BaseException.h" -namespace mrmc { +namespace storm { namespace exceptions { -MRMC_EXCEPTION_DEFINE_NEW(FileIoException) +STORM_EXCEPTION_DEFINE_NEW(FileIoException) } } -#endif /* MRMC_EXCEPTIONS_FILEIOEXCEPTION_H_ */ +#endif /* STORM_EXCEPTIONS_FILEIOEXCEPTION_H_ */ diff --git a/src/exceptions/InvalidArgumentException.h b/src/exceptions/InvalidArgumentException.h index c6c07e68a..fac516554 100644 --- a/src/exceptions/InvalidArgumentException.h +++ b/src/exceptions/InvalidArgumentException.h @@ -1,18 +1,18 @@ -#ifndef MRMC_EXCEPTIONS_INVALIDARGUMENTEXCEPTION_H_ -#define MRMC_EXCEPTIONS_INVALIDARGUMENTEXCEPTION_H_ +#ifndef STORM_EXCEPTIONS_INVALIDARGUMENTEXCEPTION_H_ +#define STORM_EXCEPTIONS_INVALIDARGUMENTEXCEPTION_H_ #include "src/exceptions/BaseException.h" -namespace mrmc { +namespace storm { namespace exceptions { /*! * @brief This exception is thrown when a parameter is invalid in this context */ -MRMC_EXCEPTION_DEFINE_NEW(InvalidArgumentException) +STORM_EXCEPTION_DEFINE_NEW(InvalidArgumentException) } // namespace exceptions -} // namespace mrmc -#endif // MRMC_EXCEPTIONS_INVALIDARGUMENTEXCEPTION_H_ +} // namespace storm +#endif // STORM_EXCEPTIONS_INVALIDARGUMENTEXCEPTION_H_ diff --git a/src/exceptions/InvalidSettingsException.h b/src/exceptions/InvalidSettingsException.h index a399d82ae..12b0ba5b2 100644 --- a/src/exceptions/InvalidSettingsException.h +++ b/src/exceptions/InvalidSettingsException.h @@ -1,14 +1,14 @@ -#ifndef MRMC_EXCEPTIONS_INVALIDSETTINGSEXCEPTION_H_ -#define MRMC_EXCEPTIONS_INVALIDSETTINGSEXCEPTION_H_ +#ifndef STORM_EXCEPTIONS_INVALIDSETTINGSEXCEPTION_H_ +#define STORM_EXCEPTIONS_INVALIDSETTINGSEXCEPTION_H_ #include "src/exceptions/BaseException.h" -namespace mrmc { +namespace storm { namespace exceptions { -MRMC_EXCEPTION_DEFINE_NEW(InvalidSettingsException) +STORM_EXCEPTION_DEFINE_NEW(InvalidSettingsException) } // namespace exceptions -} // namespace mrmc +} // namespace storm -#endif // MRMC_EXCEPTIONS_INVALIDSETTINGSEXCEPTION_H_ +#endif // STORM_EXCEPTIONS_INVALIDSETTINGSEXCEPTION_H_ diff --git a/src/exceptions/InvalidStateException.h b/src/exceptions/InvalidStateException.h index c971321bf..13ae5dca2 100644 --- a/src/exceptions/InvalidStateException.h +++ b/src/exceptions/InvalidStateException.h @@ -1,9 +1,9 @@ -#ifndef MRMC_EXCEPTIONS_INVALIDSTATEEXCEPTION_H_ -#define MRMC_EXCEPTIONS_INVALIDSTATEEXCEPTION_H_ +#ifndef STORM_EXCEPTIONS_INVALIDSTATEEXCEPTION_H_ +#define STORM_EXCEPTIONS_INVALIDSTATEEXCEPTION_H_ #include "src/exceptions/BaseException.h" -namespace mrmc { +namespace storm { namespace exceptions { @@ -11,10 +11,10 @@ namespace exceptions { * @brief This exception is thrown when a memory request can't be * fulfilled. */ -MRMC_EXCEPTION_DEFINE_NEW(InvalidStateException) +STORM_EXCEPTION_DEFINE_NEW(InvalidStateException) } // namespace exceptions -} // namespace mrmc +} // namespace storm -#endif // MRMC_EXCEPTIONS_INVALIDSTATEEXCEPTION_H_ +#endif // STORM_EXCEPTIONS_INVALIDSTATEEXCEPTION_H_ diff --git a/src/exceptions/NoConvergenceException.h b/src/exceptions/NoConvergenceException.h index 1e7753b1c..a3fdd3ba3 100644 --- a/src/exceptions/NoConvergenceException.h +++ b/src/exceptions/NoConvergenceException.h @@ -1,17 +1,17 @@ -#ifndef MRMC_EXCEPTIONS_NOCONVERGENCEEXCEPTION_H_ -#define MRMC_EXCEPTIONS_NOCONVERGENCEEXCEPTION_H_ +#ifndef STORM_EXCEPTIONS_NOCONVERGENCEEXCEPTION_H_ +#define STORM_EXCEPTIONS_NOCONVERGENCEEXCEPTION_H_ #include "src/exceptions/BaseException.h" -namespace mrmc { +namespace storm { namespace exceptions { /*! * @brief This exception is thrown when an iterative solver failed to converge with the given maxIterations */ -MRMC_EXCEPTION_DEFINE_NEW(NoConvergenceException) +STORM_EXCEPTION_DEFINE_NEW(NoConvergenceException) } // namespace exceptions -} // namespace mrmc +} // namespace storm -#endif // MRMC_EXCEPTIONS_NOCONVERGENCEEXCEPTION_H_ +#endif // STORM_EXCEPTIONS_NOCONVERGENCEEXCEPTION_H_ diff --git a/src/exceptions/OutOfRangeException.h b/src/exceptions/OutOfRangeException.h index decd36fda..af0856213 100644 --- a/src/exceptions/OutOfRangeException.h +++ b/src/exceptions/OutOfRangeException.h @@ -1,18 +1,18 @@ -#ifndef MRMC_EXCEPTIONS_OUTOFRANGEEXCEPTION_H_ -#define MRMC_EXCEPTIONS_OUTOFRANGEEXCEPTION_H_ +#ifndef STORM_EXCEPTIONS_OUTOFRANGEEXCEPTION_H_ +#define STORM_EXCEPTIONS_OUTOFRANGEEXCEPTION_H_ #include "src/exceptions/BaseException.h" -namespace mrmc { +namespace storm { namespace exceptions { /* * @briefThis exception is thrown when a parameter is not in the range of valid values */ -MRMC_EXCEPTION_DEFINE_NEW(OutOfRangeException) +STORM_EXCEPTION_DEFINE_NEW(OutOfRangeException) } // namespace exceptions -} // namespace mrmc -#endif // MRMC_EXCEPTIONS_OUTOFRANGEEXCEPTION_H_ +} // namespace storm +#endif // STORM_EXCEPTIONS_OUTOFRANGEEXCEPTION_H_ diff --git a/src/exceptions/WrongFileFormatException.h b/src/exceptions/WrongFileFormatException.h index 182660a30..56dadcb96 100644 --- a/src/exceptions/WrongFileFormatException.h +++ b/src/exceptions/WrongFileFormatException.h @@ -5,12 +5,12 @@ * Author: Thomas Heinemann */ -#ifndef MRMC_EXCEPTIONS_WRONGFILEFORMATEXCEPTION_H_ -#define MRMC_EXCEPTIONS_WRONGFILEFORMATEXCEPTION_H_ +#ifndef STORM_EXCEPTIONS_WRONGFILEFORMATEXCEPTION_H_ +#define STORM_EXCEPTIONS_WRONGFILEFORMATEXCEPTION_H_ #include "src/exceptions/BaseException.h" -namespace mrmc { +namespace storm { namespace exceptions { @@ -18,10 +18,10 @@ namespace exceptions { * @brief This exception is thrown when an input file * contains invalid or missing keys. */ -MRMC_EXCEPTION_DEFINE_NEW(WrongFileFormatException) +STORM_EXCEPTION_DEFINE_NEW(WrongFileFormatException) } //namespace exceptions -} //namespace mrmc +} //namespace storm -#endif /* MRMC_EXCEPTIONS_WRONGFILEFORMATEXCEPTION_H_ */ +#endif /* STORM_EXCEPTIONS_WRONGFILEFORMATEXCEPTION_H_ */ diff --git a/src/formula/And.h b/src/formula/And.h index 62cc46964..d166fd7c5 100644 --- a/src/formula/And.h +++ b/src/formula/And.h @@ -5,13 +5,13 @@ * Author: Thomas Heinemann */ -#ifndef MRMC_FORMULA_AND_H_ -#define MRMC_FORMULA_AND_H_ +#ifndef STORM_FORMULA_AND_H_ +#define STORM_FORMULA_AND_H_ #include "PctlStateFormula.h" #include -namespace mrmc { +namespace storm { namespace formula { @@ -141,7 +141,7 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { + virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { return modelChecker.checkAnd(*this); } @@ -152,6 +152,6 @@ private: } //namespace formula -} //namespace mrmc +} //namespace storm -#endif /* MRMC_FORMULA_AND_H_ */ +#endif /* STORM_FORMULA_AND_H_ */ diff --git a/src/formula/Ap.h b/src/formula/Ap.h index 1f636d7df..e479d0c61 100644 --- a/src/formula/Ap.h +++ b/src/formula/Ap.h @@ -5,12 +5,12 @@ * Author: Thomas Heinemann */ -#ifndef MRMC_FORMULA_AP_H_ -#define MRMC_FORMULA_AP_H_ +#ifndef STORM_FORMULA_AP_H_ +#define STORM_FORMULA_AP_H_ #include "PctlStateFormula.h" -namespace mrmc { +namespace storm { namespace formula { @@ -77,7 +77,7 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { + virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { return modelChecker.checkAp(*this); } @@ -87,6 +87,6 @@ private: } //namespace formula -} //namespace mrmc +} //namespace storm -#endif /* MRMC_FORMULA_AP_H_ */ +#endif /* STORM_FORMULA_AP_H_ */ diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h index 281c112bc..36d5c7fc1 100644 --- a/src/formula/BoundedUntil.h +++ b/src/formula/BoundedUntil.h @@ -5,15 +5,15 @@ * Author: Thomas Heinemann */ -#ifndef MRMC_FORMULA_BOUNDEDUNTIL_H_ -#define MRMC_FORMULA_BOUNDEDUNTIL_H_ +#ifndef STORM_FORMULA_BOUNDEDUNTIL_H_ +#define STORM_FORMULA_BOUNDEDUNTIL_H_ #include "PctlPathFormula.h" #include "PctlStateFormula.h" #include "boost/integer/integer_mask.hpp" #include -namespace mrmc { +namespace storm { namespace formula { @@ -166,7 +166,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { + virtual std::vector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { return modelChecker.checkBoundedUntil(*this); } @@ -178,6 +178,6 @@ private: } //namespace formula -} //namespace mrmc +} //namespace storm -#endif /* MRMC_FORMULA_BOUNDEDUNTIL_H_ */ +#endif /* STORM_FORMULA_BOUNDEDUNTIL_H_ */ diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h index 8db8c1f0d..3cd6ce94c 100644 --- a/src/formula/Formulas.h +++ b/src/formula/Formulas.h @@ -5,8 +5,8 @@ * Author: chris */ -#ifndef MRMC_FORMULA_FORMULAS_H_ -#define MRMC_FORMULA_FORMULAS_H_ +#ifndef STORM_FORMULA_FORMULAS_H_ +#define STORM_FORMULA_FORMULAS_H_ #include "And.h" #include "Ap.h" @@ -22,4 +22,4 @@ #include "ProbabilisticIntervalOperator.h" #include "Until.h" -#endif /* MRMC_FORMULA_FORMULAS_H_ */ +#endif /* STORM_FORMULA_FORMULAS_H_ */ diff --git a/src/formula/Next.h b/src/formula/Next.h index 07924846e..7b8214757 100644 --- a/src/formula/Next.h +++ b/src/formula/Next.h @@ -5,13 +5,13 @@ * Author: Thomas Heinemann */ -#ifndef MRMC_FORMULA_NEXT_H_ -#define MRMC_FORMULA_NEXT_H_ +#ifndef STORM_FORMULA_NEXT_H_ +#define STORM_FORMULA_NEXT_H_ #include "PctlPathFormula.h" #include "PctlStateFormula.h" -namespace mrmc { +namespace storm { namespace formula { @@ -112,7 +112,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { + virtual std::vector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { return modelChecker.checkNext(*this); } @@ -122,6 +122,6 @@ private: } //namespace formula -} //namespace mrmc +} //namespace storm -#endif /* MRMC_FORMULA_NEXT_H_ */ +#endif /* STORM_FORMULA_NEXT_H_ */ diff --git a/src/formula/Not.h b/src/formula/Not.h index 26ae6320c..03d5cf572 100644 --- a/src/formula/Not.h +++ b/src/formula/Not.h @@ -5,12 +5,12 @@ * Author: Thomas Heinemann */ -#ifndef MRMC_FORMULA_NOT_H_ -#define MRMC_FORMULA_NOT_H_ +#ifndef STORM_FORMULA_NOT_H_ +#define STORM_FORMULA_NOT_H_ #include "PctlStateFormula.h" -namespace mrmc { +namespace storm { namespace formula { @@ -105,7 +105,7 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { + virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { return modelChecker.checkNot(*this); } @@ -115,6 +115,6 @@ private: } //namespace formula -} //namespace MRMC +} //namespace storm -#endif /* MRMC_FORMULA_NOT_H_ */ +#endif /* STORM_FORMULA_NOT_H_ */ diff --git a/src/formula/Or.h b/src/formula/Or.h index bc1302185..524ca58e7 100644 --- a/src/formula/Or.h +++ b/src/formula/Or.h @@ -5,12 +5,12 @@ * Author: Thomas Heinemann */ -#ifndef MRMC_FORMULA_OR_H_ -#define MRMC_FORMULA_OR_H_ +#ifndef STORM_FORMULA_OR_H_ +#define STORM_FORMULA_OR_H_ #include "PctlStateFormula.h" -namespace mrmc { +namespace storm { namespace formula { @@ -140,7 +140,7 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { + virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { return modelChecker.checkOr(*this); } @@ -151,6 +151,6 @@ private: } //namespace formula -} //namespace mrmc +} //namespace storm -#endif /* MRMC_FORMULA_OR_H_ */ +#endif /* STORM_FORMULA_OR_H_ */ diff --git a/src/formula/PctlFormula.h b/src/formula/PctlFormula.h index a4d910483..394e3cfa2 100644 --- a/src/formula/PctlFormula.h +++ b/src/formula/PctlFormula.h @@ -5,12 +5,12 @@ * Author: Thomas Heinemann */ -#ifndef MRMC_FORMULA_PCTLFORMULA_H_ -#define MRMC_FORMULA_PCTLFORMULA_H_ +#ifndef STORM_FORMULA_PCTLFORMULA_H_ +#define STORM_FORMULA_PCTLFORMULA_H_ #include -namespace mrmc { +namespace storm { namespace formula { @@ -43,6 +43,6 @@ public: } //namespace formula -} //namespace mrmc +} //namespace storm -#endif /* MRMC_FORMULA_PCTLFORMULA_H_ */ +#endif /* STORM_FORMULA_PCTLFORMULA_H_ */ diff --git a/src/formula/PctlPathFormula.h b/src/formula/PctlPathFormula.h index 9b6a38b94..f929c642a 100644 --- a/src/formula/PctlPathFormula.h +++ b/src/formula/PctlPathFormula.h @@ -5,14 +5,14 @@ * Author: Thomas Heinemann */ -#ifndef MRMC_FORMULA_PCTLPATHFORMULA_H_ -#define MRMC_FORMULA_PCTLPATHFORMULA_H_ +#ifndef STORM_FORMULA_PCTLPATHFORMULA_H_ +#define STORM_FORMULA_PCTLPATHFORMULA_H_ #include "PctlFormula.h" #include "modelChecker/DtmcPrctlModelChecker.h" #include -namespace mrmc { +namespace storm { namespace formula { @@ -55,11 +55,11 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector* check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const = 0; + virtual std::vector* check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const = 0; }; } //namespace formula -} //namespace mrmc +} //namespace storm -#endif /* MRMC_FORMULA_PCTLPATHFORMULA_H_ */ +#endif /* STORM_FORMULA_PCTLPATHFORMULA_H_ */ diff --git a/src/formula/PctlStateFormula.h b/src/formula/PctlStateFormula.h index c4eee14f2..bfd035e4d 100644 --- a/src/formula/PctlStateFormula.h +++ b/src/formula/PctlStateFormula.h @@ -5,14 +5,14 @@ * Author: Thomas Heinemann */ -#ifndef MRMC_FORMULA_PCTLSTATEFORMULA_H_ -#define MRMC_FORMULA_PCTLSTATEFORMULA_H_ +#ifndef STORM_FORMULA_PCTLSTATEFORMULA_H_ +#define STORM_FORMULA_PCTLSTATEFORMULA_H_ #include "PctlFormula.h" #include "storage/BitVector.h" #include "modelChecker/DtmcPrctlModelChecker.h" -namespace mrmc { +namespace storm { namespace formula { @@ -55,12 +55,12 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const = 0; + virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const = 0; }; } //namespace formula -} //namespace mrmc +} //namespace storm -#endif /* MRMC_FORMULA_PCTLSTATEFORMULA_H_ */ +#endif /* STORM_FORMULA_PCTLSTATEFORMULA_H_ */ diff --git a/src/formula/ProbabilisticIntervalOperator.h b/src/formula/ProbabilisticIntervalOperator.h index 7a832c480..2ca2b9bbb 100644 --- a/src/formula/ProbabilisticIntervalOperator.h +++ b/src/formula/ProbabilisticIntervalOperator.h @@ -5,14 +5,14 @@ * Author: Thomas Heinemann */ -#ifndef MRMC_FORMULA_PROBABILISTICINTERVALOPERATOR_H_ -#define MRMC_FORMULA_PROBABILISTICINTERVALOPERATOR_H_ +#ifndef STORM_FORMULA_PROBABILISTICINTERVALOPERATOR_H_ +#define STORM_FORMULA_PROBABILISTICINTERVALOPERATOR_H_ #include "PctlStateFormula.h" #include "PctlPathFormula.h" #include "utility/ConstTemplates.h" -namespace mrmc { +namespace storm { namespace formula { @@ -49,8 +49,8 @@ public: * Empty constructor */ ProbabilisticIntervalOperator() { - upper = mrmc::utility::constGetZero(); - lower = mrmc::utility::constGetZero(); + upper = storm::utility::constGetZero(); + lower = storm::utility::constGetZero(); pathFormula = NULL; } @@ -159,7 +159,7 @@ public: * * @returns A bit vector indicating all states that satisfy the formula represented by the called object. */ - virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { + virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { return modelChecker.checkProbabilisticIntervalOperator(*this); } @@ -171,6 +171,6 @@ private: } //namespace formula -} //namespace mrmc +} //namespace storm -#endif /* MRMC_FORMULA_PROBABILISTICINTERVALOPERATOR_H_ */ +#endif /* STORM_FORMULA_PROBABILISTICINTERVALOPERATOR_H_ */ diff --git a/src/formula/ProbabilisticNoBoundsOperator.h b/src/formula/ProbabilisticNoBoundsOperator.h index 7406db5e2..3f76cd9fd 100644 --- a/src/formula/ProbabilisticNoBoundsOperator.h +++ b/src/formula/ProbabilisticNoBoundsOperator.h @@ -5,13 +5,13 @@ * Author: thomas */ -#ifndef MRMC_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_ -#define MRMC_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_ +#ifndef STORM_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_ +#define STORM_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_ #include "PctlFormula.h" #include "PctlPathFormula.h" -namespace mrmc { +namespace storm { namespace formula { /*! @@ -45,7 +45,7 @@ namespace formula { * @see PctlFormula */ template -class ProbabilisticNoBoundsOperator: public mrmc::formula::PctlFormula { +class ProbabilisticNoBoundsOperator: public storm::formula::PctlFormula { public: /*! * Empty constructor @@ -103,6 +103,6 @@ private: }; } /* namespace formula */ -} /* namespace mrmc */ +} /* namespace storm */ -#endif /* MRMC_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_ */ +#endif /* STORM_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_ */ diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h index 36fc5f374..118bf1cdb 100644 --- a/src/formula/ProbabilisticOperator.h +++ b/src/formula/ProbabilisticOperator.h @@ -5,12 +5,12 @@ * Author: Thomas Heinemann */ -#ifndef MRMC_FORMULA_PROBABILISTICOPERATOR_H_ -#define MRMC_FORMULA_PROBABILISTICOPERATOR_H_ +#ifndef STORM_FORMULA_PROBABILISTICOPERATOR_H_ +#define STORM_FORMULA_PROBABILISTICOPERATOR_H_ #include "PctlStateFormula.h" -namespace mrmc { +namespace storm { namespace formula { /*! @@ -39,7 +39,7 @@ namespace formula { * @see PctlFormula */ template -class ProbabilisticOperator : public mrmc::formula::PctlStateFormula { +class ProbabilisticOperator : public storm::formula::PctlStateFormula { public: /*! * Empty constructor @@ -129,8 +129,8 @@ public: * @returns A bit vector indicating all states that satisfy the formula represented by the * called object. */ - virtual mrmc::storage::BitVector *check( - const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { + virtual storm::storage::BitVector *check( + const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { return modelChecker.checkProbabilisticOperator(*this); } @@ -153,6 +153,6 @@ private: }; } /* namespace formula */ -} /* namespace mrmc */ +} /* namespace storm */ -#endif /* MRMC_FORMULA_PROBABILISTICOPERATOR_H_ */ +#endif /* STORM_FORMULA_PROBABILISTICOPERATOR_H_ */ diff --git a/src/formula/Until.h b/src/formula/Until.h index 3f094e3a3..be86a1153 100644 --- a/src/formula/Until.h +++ b/src/formula/Until.h @@ -5,13 +5,13 @@ * Author: Thomas Heinemann */ -#ifndef MRMC_FORMULA_UNTIL_H_ -#define MRMC_FORMULA_UNTIL_H_ +#ifndef STORM_FORMULA_UNTIL_H_ +#define STORM_FORMULA_UNTIL_H_ #include "PctlPathFormula.h" #include "PctlStateFormula.h" -namespace mrmc { +namespace storm { namespace formula { @@ -140,7 +140,7 @@ public: * * @returns A vector indicating the probability that the formula holds for each state. */ - virtual std::vector *check(const mrmc::modelChecker::DtmcPrctlModelChecker& modelChecker) const { + virtual std::vector *check(const storm::modelChecker::DtmcPrctlModelChecker& modelChecker) const { return modelChecker.checkUntil(*this); } @@ -151,6 +151,6 @@ private: } //namespace formula -} //namespace mrmc +} //namespace storm -#endif /* MRMC_FORMULA_UNTIL_H_ */ +#endif /* STORM_FORMULA_UNTIL_H_ */ diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index fe0f8b565..5f48a8e8d 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -5,10 +5,10 @@ * Author: Thomas Heinemann */ -#ifndef MRMC_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ -#define MRMC_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ +#ifndef STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ +#define STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ -namespace mrmc { +namespace storm { namespace modelChecker { @@ -37,7 +37,7 @@ class DtmcPrctlModelChecker; extern log4cplus::Logger logger; -namespace mrmc { +namespace storm { namespace modelChecker { @@ -58,7 +58,7 @@ public: * * @param model The dtmc model which is checked. */ - explicit DtmcPrctlModelChecker(mrmc::models::Dtmc& model) : model(model) { + explicit DtmcPrctlModelChecker(storm::models::Dtmc& model) : model(model) { } @@ -67,8 +67,8 @@ public: * * @param modelChecker The model checker that is copied. */ - explicit DtmcPrctlModelChecker(const mrmc::modelChecker::DtmcPrctlModelChecker* modelChecker) { - this->model = new mrmc::models::Dtmc(modelChecker->getModel()); + explicit DtmcPrctlModelChecker(const storm::modelChecker::DtmcPrctlModelChecker* modelChecker) { + this->model = new storm::models::Dtmc(modelChecker->getModel()); } /*! @@ -81,7 +81,7 @@ public: /*! * @returns A reference to the dtmc of the model checker. */ - mrmc::models::Dtmc& getModel() const { + storm::models::Dtmc& getModel() const { return this->model; } @@ -89,7 +89,7 @@ public: * Sets the DTMC model which is checked * @param model */ - void setModel(mrmc::models::Dtmc& model) { + void setModel(storm::models::Dtmc& model) { this->model = &model; } @@ -98,9 +98,9 @@ public: * states. * @param stateFormula The formula to be checked. */ - void check(const mrmc::formula::PctlStateFormula& stateFormula) { + void check(const storm::formula::PctlStateFormula& stateFormula) { LOG4CPLUS_INFO(logger, "Model checking formula " << stateFormula.toString()); - mrmc::storage::BitVector* result = stateFormula.check(*this); + storm::storage::BitVector* result = stateFormula.check(*this); LOG4CPLUS_INFO(logger, "Result for initial states:"); for (auto initialState : *this->getModel().getLabeledStates("init")) { LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied")); @@ -113,7 +113,7 @@ public: * (probability) for all initial states. * @param probabilisticNoBoundsFormula The formula to be checked. */ - void check(const mrmc::formula::ProbabilisticNoBoundsOperator& probabilisticNoBoundsFormula) { + void check(const storm::formula::ProbabilisticNoBoundsOperator& probabilisticNoBoundsFormula) { LOG4CPLUS_INFO(logger, "Model checking formula " << probabilisticNoBoundsFormula.toString()); std::cout << "Model checking formula: " << probabilisticNoBoundsFormula.toString() << std::endl; std::vector* result = checkProbabilisticNoBoundsOperator(probabilisticNoBoundsFormula); @@ -133,7 +133,7 @@ public: * @param formula The state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - mrmc::storage::BitVector* checkStateFormula(const mrmc::formula::PctlStateFormula& formula) const { + storm::storage::BitVector* checkStateFormula(const storm::formula::PctlStateFormula& formula) const { return formula.check(*this); } @@ -143,9 +143,9 @@ public: * @param formula The And formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - mrmc::storage::BitVector* checkAnd(const mrmc::formula::And& formula) const { - mrmc::storage::BitVector* result = checkStateFormula(formula.getLeft()); - mrmc::storage::BitVector* right = checkStateFormula(formula.getRight()); + storm::storage::BitVector* checkAnd(const storm::formula::And& formula) const { + storm::storage::BitVector* result = checkStateFormula(formula.getLeft()); + storm::storage::BitVector* right = checkStateFormula(formula.getRight()); (*result) &= (*right); delete right; return result; @@ -157,13 +157,13 @@ public: * @param formula The Ap state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - mrmc::storage::BitVector* checkAp(const mrmc::formula::Ap& formula) const { + storm::storage::BitVector* checkAp(const storm::formula::Ap& formula) const { if (formula.getAp().compare("true") == 0) { - return new mrmc::storage::BitVector(this->getModel().getNumberOfStates(), true); + return new storm::storage::BitVector(this->getModel().getNumberOfStates(), true); } else if (formula.getAp().compare("false") == 0) { - return new mrmc::storage::BitVector(this->getModel().getNumberOfStates()); + return new storm::storage::BitVector(this->getModel().getNumberOfStates()); } - return new mrmc::storage::BitVector(*this->getModel().getLabeledStates(formula.getAp())); + return new storm::storage::BitVector(*this->getModel().getLabeledStates(formula.getAp())); } /*! @@ -172,8 +172,8 @@ public: * @param formula The Not state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - mrmc::storage::BitVector* checkNot(const mrmc::formula::Not& formula) const { - mrmc::storage::BitVector* result = checkStateFormula(formula.getChild()); + storm::storage::BitVector* checkNot(const storm::formula::Not& formula) const { + storm::storage::BitVector* result = checkStateFormula(formula.getChild()); result->complement(); return result; } @@ -184,9 +184,9 @@ public: * @param formula The Or state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - mrmc::storage::BitVector* checkOr(const mrmc::formula::Or& formula) const { - mrmc::storage::BitVector* result = checkStateFormula(formula.getLeft()); - mrmc::storage::BitVector* right = checkStateFormula(formula.getRight()); + storm::storage::BitVector* checkOr(const storm::formula::Or& formula) const { + storm::storage::BitVector* result = checkStateFormula(formula.getLeft()); + storm::storage::BitVector* right = checkStateFormula(formula.getRight()); (*result) |= (*right); delete right; return result; @@ -199,11 +199,11 @@ public: * @param formula The state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - mrmc::storage::BitVector* checkProbabilisticOperator( - const mrmc::formula::ProbabilisticOperator& formula) const { + storm::storage::BitVector* checkProbabilisticOperator( + const storm::formula::ProbabilisticOperator& formula) const { std::vector* probabilisticResult = this->checkPathFormula(formula.getPathFormula()); - mrmc::storage::BitVector* result = new mrmc::storage::BitVector(this->getModel().getNumberOfStates()); + storm::storage::BitVector* result = new storm::storage::BitVector(this->getModel().getNumberOfStates()); Type bound = formula.getBound(); for (uint_fast64_t i = 0; i < this->getModel().getNumberOfStates(); ++i) { if ((*probabilisticResult)[i] == bound) result->set(i, true); @@ -221,13 +221,13 @@ public: * @param formula The state formula to check * @returns The set of states satisfying the formula, represented by a bit vector */ - mrmc::storage::BitVector* checkProbabilisticIntervalOperator( - const mrmc::formula::ProbabilisticIntervalOperator& formula) const { + storm::storage::BitVector* checkProbabilisticIntervalOperator( + const storm::formula::ProbabilisticIntervalOperator& formula) const { // First, we need to compute the probability for satisfying the path formula for each state. std::vector* probabilisticResult = this->checkPathFormula(formula.getPathFormula()); // Create resulting bit vector, which will hold the yes/no-answer for every state. - mrmc::storage::BitVector* result = new mrmc::storage::BitVector(this->getModel().getNumberOfStates()); + storm::storage::BitVector* result = new storm::storage::BitVector(this->getModel().getNumberOfStates()); // Now, we can compute which states meet the bound specified in this operator, i.e. // lie in the interval that was given along with this operator, and set the corresponding bits @@ -252,7 +252,7 @@ public: * @returns The set of states satisfying the formula, represented by a bit vector */ std::vector* checkProbabilisticNoBoundsOperator( - const mrmc::formula::ProbabilisticNoBoundsOperator& formula) const { + const storm::formula::ProbabilisticNoBoundsOperator& formula) const { return formula.getPathFormula().check(*this); } @@ -263,7 +263,7 @@ public: * @param formula The path formula to check * @returns for each state the probability that the path formula holds. */ - std::vector* checkPathFormula(const mrmc::formula::PctlPathFormula& formula) const { + std::vector* checkPathFormula(const storm::formula::PctlPathFormula& formula) const { return formula.check(*this); } @@ -273,7 +273,7 @@ public: * @param formula The Bounded Until path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector* checkBoundedUntil(const mrmc::formula::BoundedUntil& formula) const = 0; + virtual std::vector* checkBoundedUntil(const storm::formula::BoundedUntil& formula) const = 0; /*! * The check method for a path formula with a Next operator node as root in its formula tree @@ -281,7 +281,7 @@ public: * @param formula The Next path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector* checkNext(const mrmc::formula::Next& formula) const = 0; + virtual std::vector* checkNext(const storm::formula::Next& formula) const = 0; /*! * The check method for a path formula with an Until operator node as root in its formula tree @@ -289,14 +289,14 @@ public: * @param formula The Until path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector* checkUntil(const mrmc::formula::Until& formula) const = 0; + virtual std::vector* checkUntil(const storm::formula::Until& formula) const = 0; private: - mrmc::models::Dtmc& model; + storm::models::Dtmc& model; }; } //namespace modelChecker -} //namespace mrmc +} //namespace storm -#endif /* MRMC_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ */ +#endif /* STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ */ diff --git a/src/modelChecker/EigenDtmcPrctlModelChecker.h b/src/modelChecker/EigenDtmcPrctlModelChecker.h index e5cee0782..3c387bec5 100644 --- a/src/modelChecker/EigenDtmcPrctlModelChecker.h +++ b/src/modelChecker/EigenDtmcPrctlModelChecker.h @@ -5,8 +5,8 @@ * Author: */ -#ifndef MRMC_MODELCHECKER_EIGENDTMCPRCTLMODELCHECKER_H_ -#define MRMC_MODELCHECKER_EIGENDTMCPRCTLMODELCHECKER_H_ +#ifndef STORM_MODELCHECKER_EIGENDTMCPRCTLMODELCHECKER_H_ +#define STORM_MODELCHECKER_EIGENDTMCPRCTLMODELCHECKER_H_ #include "src/utility/Vector.h" @@ -27,7 +27,7 @@ extern log4cplus::Logger logger; -namespace mrmc { +namespace storm { namespace modelChecker { @@ -38,17 +38,17 @@ template class EigenDtmcPrctlModelChecker : public DtmcPrctlModelChecker { public: - explicit EigenDtmcPrctlModelChecker(mrmc::models::Dtmc& dtmc) : DtmcPrctlModelChecker(dtmc) { } + explicit EigenDtmcPrctlModelChecker(storm::models::Dtmc& dtmc) : DtmcPrctlModelChecker(dtmc) { } virtual ~EigenDtmcPrctlModelChecker() { } - virtual std::vector* checkBoundedUntil(const mrmc::formula::BoundedUntil& formula) const { + virtual std::vector* checkBoundedUntil(const storm::formula::BoundedUntil& formula) const { // First, we need to compute the states that satisfy the sub-formulas of the until-formula. - mrmc::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft()); - mrmc::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight()); + storm::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft()); + storm::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight()); // Copy the matrix before we make any changes. - mrmc::storage::SquareSparseMatrix tmpMatrix(*this->getModel().getTransitionProbabilityMatrix()); + storm::storage::SquareSparseMatrix tmpMatrix(*this->getModel().getTransitionProbabilityMatrix()); // Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. tmpMatrix.makeRowsAbsorbing((~*leftStates | *rightStates) | *rightStates); @@ -64,7 +64,7 @@ public: std::vector* result = new std::vector(stateCount); - mrmc::utility::setVectorValues(result, *rightStates, mrmc::utility::constGetOne()); + storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne()); Type *p = &((*result)[0]); // get the address storing the data for result MapType vectorMap(p, result->size()); // vectorMap shares data @@ -83,9 +83,9 @@ public: return result; } - virtual std::vector* checkNext(const mrmc::formula::Next& formula) const { + virtual std::vector* checkNext(const storm::formula::Next& formula) const { // First, we need to compute the states that satisfy the sub-formula of the next-formula. - mrmc::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild()); + storm::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild()); // Transform the transition probability matrix to the gmm++ format to use its arithmetic. Eigen::SparseMatrix* eigenMatrix = this->getModel().getTransitionProbabilityMatrix()->toEigenSparseMatrix(); @@ -93,7 +93,7 @@ public: // Create the vector with which to multiply and initialize it correctly. std::vector x(this->getModel().getNumberOfStates()); - mrmc::utility::setVectorValues(&x, *nextStates, mrmc::utility::constGetOne()); + storm::utility::setVectorValues(&x, *nextStates, storm::utility::constGetOne()); // Delete not needed next states bit vector. delete nextStates; @@ -118,16 +118,16 @@ public: return result; } - virtual std::vector* checkUntil(const mrmc::formula::Until& formula) const { + virtual std::vector* checkUntil(const storm::formula::Until& formula) const { // First, we need to compute the states that satisfy the sub-formulas of the until-formula. - mrmc::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft()); - mrmc::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight()); + storm::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft()); + storm::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight()); // Then, we need to identify the states which have to be taken out of the matrix, i.e. // all states that have probability 0 and 1 of satisfying the until-formula. - mrmc::storage::BitVector notExistsPhiUntilPsiStates(this->getModel().getNumberOfStates()); - mrmc::storage::BitVector alwaysPhiUntilPsiStates(this->getModel().getNumberOfStates()); - mrmc::solver::GraphAnalyzer::getPhiUntilPsiStates(this->getModel(), *leftStates, *rightStates, ¬ExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates); + storm::storage::BitVector notExistsPhiUntilPsiStates(this->getModel().getNumberOfStates()); + storm::storage::BitVector alwaysPhiUntilPsiStates(this->getModel().getNumberOfStates()); + storm::solver::GraphAnalyzer::getPhiUntilPsiStates(this->getModel(), *leftStates, *rightStates, ¬ExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates); notExistsPhiUntilPsiStates.complement(); delete leftStates; @@ -135,7 +135,7 @@ public: LOG4CPLUS_INFO(logger, "Found " << notExistsPhiUntilPsiStates.getNumberOfSetBits() << " 'no' states."); LOG4CPLUS_INFO(logger, "Found " << alwaysPhiUntilPsiStates.getNumberOfSetBits() << " 'yes' states."); - mrmc::storage::BitVector maybeStates = ~(notExistsPhiUntilPsiStates | alwaysPhiUntilPsiStates); + storm::storage::BitVector maybeStates = ~(notExistsPhiUntilPsiStates | alwaysPhiUntilPsiStates); LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); // Create resulting vector and set values accordingly. @@ -148,7 +148,7 @@ public: typedef Eigen::Map MapType; // Now we can eliminate the rows and columns from the original transition probability matrix. - mrmc::storage::SquareSparseMatrix* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates); + storm::storage::SquareSparseMatrix* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates); // Converting the matrix to the form needed for the equation system. That is, we go from // x = A*x + b to (I-A)x = b. submatrix->convertToEquationSystem(); @@ -195,7 +195,7 @@ public: LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: InvalidInput"); } else if(solver.info() == Eigen::ComputationInfo::NoConvergence) { // NoConvergence - throw mrmc::exceptions::NoConvergenceException("Solving of Submatrix with Eigen failed", solver.iterations(), solver.maxIterations()); + throw storm::exceptions::NoConvergenceException("Solving of Submatrix with Eigen failed", solver.iterations(), solver.maxIterations()); } else if(solver.info() == Eigen::ComputationInfo::NumericalIssue) { // NumericalIssue LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: NumericalIssue"); @@ -205,14 +205,14 @@ public: } // Set values of resulting vector according to result. - mrmc::utility::setVectorValues(result, maybeStates, x); + storm::utility::setVectorValues(result, maybeStates, x); // Delete temporary matrix. delete eigenSubMatrix; } - mrmc::utility::setVectorValues(result, notExistsPhiUntilPsiStates, mrmc::utility::constGetZero()); - mrmc::utility::setVectorValues(result, alwaysPhiUntilPsiStates, mrmc::utility::constGetOne()); + storm::utility::setVectorValues(result, notExistsPhiUntilPsiStates, storm::utility::constGetZero()); + storm::utility::setVectorValues(result, alwaysPhiUntilPsiStates, storm::utility::constGetOne()); return result; } @@ -220,6 +220,6 @@ public: } //namespace modelChecker -} //namespace mrmc +} //namespace storm -#endif /* MRMC_MODELCHECKER_EIGENDTMCPRCTLMODELCHECKER_H_ */ +#endif /* STORM_MODELCHECKER_EIGENDTMCPRCTLMODELCHECKER_H_ */ diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index bc4582519..ab7bce9b9 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -5,8 +5,8 @@ * Author: Christian Dehnert */ -#ifndef MRMC_MODELCHECKER_GMMXXDTMCPRCTLMODELCHECKER_H_ -#define MRMC_MODELCHECKER_GMMXXDTMCPRCTLMODELCHECKER_H_ +#ifndef STORM_MODELCHECKER_GMMXXDTMCPRCTLMODELCHECKER_H_ +#define STORM_MODELCHECKER_GMMXXDTMCPRCTLMODELCHECKER_H_ #include @@ -26,7 +26,7 @@ extern log4cplus::Logger logger; -namespace mrmc { +namespace storm { namespace modelChecker { @@ -37,27 +37,27 @@ template class GmmxxDtmcPrctlModelChecker : public DtmcPrctlModelChecker { public: - explicit GmmxxDtmcPrctlModelChecker(mrmc::models::Dtmc& dtmc) : DtmcPrctlModelChecker(dtmc) { } + explicit GmmxxDtmcPrctlModelChecker(storm::models::Dtmc& dtmc) : DtmcPrctlModelChecker(dtmc) { } virtual ~GmmxxDtmcPrctlModelChecker() { } - virtual std::vector* checkBoundedUntil(const mrmc::formula::BoundedUntil& formula) const { + virtual std::vector* checkBoundedUntil(const storm::formula::BoundedUntil& formula) const { // First, we need to compute the states that satisfy the sub-formulas of the until-formula. - mrmc::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft()); - mrmc::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight()); + storm::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft()); + storm::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight()); // Copy the matrix before we make any changes. - mrmc::storage::SquareSparseMatrix tmpMatrix(*this->getModel().getTransitionProbabilityMatrix()); + storm::storage::SquareSparseMatrix tmpMatrix(*this->getModel().getTransitionProbabilityMatrix()); // Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates); // Transform the transition probability matrix to the gmm++ format to use its arithmetic. - gmm::csr_matrix* gmmxxMatrix = mrmc::adapters::GmmxxAdapter::toGmmxxSparseMatrix(tmpMatrix); + gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(tmpMatrix); // Create the vector with which to multiply. std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - mrmc::utility::setVectorValues(result, *rightStates, mrmc::utility::constGetOne()); + storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne()); // Now perform matrix-vector multiplication as long as we meet the bound of the formula. std::vector* swap = nullptr; @@ -76,16 +76,16 @@ public: return result; } - virtual std::vector* checkNext(const mrmc::formula::Next& formula) const { + virtual std::vector* checkNext(const storm::formula::Next& formula) const { // First, we need to compute the states that satisfy the sub-formula of the next-formula. - mrmc::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild()); + storm::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild()); // Transform the transition probability matrix to the gmm++ format to use its arithmetic. - gmm::csr_matrix* gmmxxMatrix = mrmc::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*this->getModel().getTransitionProbabilityMatrix()); + gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*this->getModel().getTransitionProbabilityMatrix()); // Create the vector with which to multiply and initialize it correctly. std::vector x(this->getModel().getNumberOfStates()); - mrmc::utility::setVectorValues(&x, *nextStates, mrmc::utility::constGetOne()); + storm::utility::setVectorValues(&x, *nextStates, storm::utility::constGetOne()); // Delete obsolete sub-result. delete nextStates; @@ -101,16 +101,16 @@ public: return result; } - virtual std::vector* checkUntil(const mrmc::formula::Until& formula) const { + virtual std::vector* checkUntil(const storm::formula::Until& formula) const { // First, we need to compute the states that satisfy the sub-formulas of the until-formula. - mrmc::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft()); - mrmc::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight()); + storm::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft()); + storm::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight()); // Then, we need to identify the states which have to be taken out of the matrix, i.e. // all states that have probability 0 and 1 of satisfying the until-formula. - mrmc::storage::BitVector notExistsPhiUntilPsiStates(this->getModel().getNumberOfStates()); - mrmc::storage::BitVector alwaysPhiUntilPsiStates(this->getModel().getNumberOfStates()); - mrmc::solver::GraphAnalyzer::getPhiUntilPsiStates(this->getModel(), *leftStates, *rightStates, ¬ExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates); + storm::storage::BitVector notExistsPhiUntilPsiStates(this->getModel().getNumberOfStates()); + storm::storage::BitVector alwaysPhiUntilPsiStates(this->getModel().getNumberOfStates()); + storm::solver::GraphAnalyzer::getPhiUntilPsiStates(this->getModel(), *leftStates, *rightStates, ¬ExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates); notExistsPhiUntilPsiStates.complement(); // Delete sub-results that are obsolete now. @@ -119,7 +119,7 @@ public: LOG4CPLUS_INFO(logger, "Found " << notExistsPhiUntilPsiStates.getNumberOfSetBits() << " 'no' states."); LOG4CPLUS_INFO(logger, "Found " << alwaysPhiUntilPsiStates.getNumberOfSetBits() << " 'yes' states."); - mrmc::storage::BitVector maybeStates = ~(notExistsPhiUntilPsiStates | alwaysPhiUntilPsiStates); + storm::storage::BitVector maybeStates = ~(notExistsPhiUntilPsiStates | alwaysPhiUntilPsiStates); LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); // Create resulting vector and set values accordingly. @@ -128,13 +128,13 @@ public: // Only try to solve system if there are states for which the probability is unknown. if (maybeStates.getNumberOfSetBits() > 0) { // Now we can eliminate the rows and columns from the original transition probability matrix. - mrmc::storage::SquareSparseMatrix* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates); + storm::storage::SquareSparseMatrix* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates); // Converting the matrix from the fixpoint notation to the form needed for the equation // system. That is, we go from x = A*x + b to (I-A)x = b. submatrix->convertToEquationSystem(); // Transform the submatrix to the gmm++ format to use its solvers. - gmm::csr_matrix* gmmxxMatrix = mrmc::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*submatrix); + gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*submatrix); delete submatrix; // Initialize the x vector with 0.5 for each element. This is the initial guess for @@ -148,7 +148,7 @@ public: this->getModel().getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &b); // Get the settings object to customize linear solving. - mrmc::settings::Settings* s = mrmc::settings::instance(); + storm::settings::Settings* s = storm::settings::instance(); // Prepare an iteration object that determines the accuracy, maximum number of iterations // and the like. @@ -215,15 +215,15 @@ public: } // Set values of resulting vector according to result. - mrmc::utility::setVectorValues(result, maybeStates, x); + storm::utility::setVectorValues(result, maybeStates, x); // Delete temporary matrix. delete gmmxxMatrix; } // Set values of resulting vector that are known exactly. - mrmc::utility::setVectorValues(result, notExistsPhiUntilPsiStates, mrmc::utility::constGetZero()); - mrmc::utility::setVectorValues(result, alwaysPhiUntilPsiStates, mrmc::utility::constGetOne()); + storm::utility::setVectorValues(result, notExistsPhiUntilPsiStates, storm::utility::constGetZero()); + storm::utility::setVectorValues(result, alwaysPhiUntilPsiStates, storm::utility::constGetOne()); return result; } @@ -278,6 +278,6 @@ public: } //namespace modelChecker -} //namespace mrmc +} //namespace storm -#endif /* MRMC_MODELCHECKER_GMMXXDTMCPRCTLMODELCHECKER_H_ */ +#endif /* STORM_MODELCHECKER_GMMXXDTMCPRCTLMODELCHECKER_H_ */ diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h index f4d52b783..66b5c879f 100644 --- a/src/models/AtomicPropositionsLabeling.h +++ b/src/models/AtomicPropositionsLabeling.h @@ -5,8 +5,8 @@ * Author: Thomas Heinemann */ -#ifndef MRMC_MODELS_ATOMICPROPOSITIONSLABELING_H_ -#define MRMC_MODELS_ATOMICPROPOSITIONSLABELING_H_ +#ifndef STORM_MODELS_ATOMICPROPOSITIONSLABELING_H_ +#define STORM_MODELS_ATOMICPROPOSITIONSLABELING_H_ #include "src/storage/BitVector.h" #include "src/exceptions/OutOfRangeException.h" @@ -15,7 +15,7 @@ #include #include -namespace mrmc { +namespace storm { namespace models { @@ -36,9 +36,9 @@ public: */ AtomicPropositionsLabeling(const uint_fast64_t stateCount, const uint_fast64_t apCountMax) : stateCount(stateCount), apCountMax(apCountMax), apsCurrent(0) { - this->singleLabelings = new mrmc::storage::BitVector*[apCountMax]; + this->singleLabelings = new storm::storage::BitVector*[apCountMax]; for (uint_fast64_t i = 0; i < apCountMax; ++i) { - this->singleLabelings[i] = new mrmc::storage::BitVector(stateCount); + this->singleLabelings[i] = new storm::storage::BitVector(stateCount); } } @@ -53,9 +53,9 @@ public: apCountMax(atomicPropositionsLabeling.apCountMax), apsCurrent(atomicPropositionsLabeling.apsCurrent), nameToLabelingMap(atomicPropositionsLabeling.nameToLabelingMap) { - this->singleLabelings = new mrmc::storage::BitVector*[apCountMax]; + this->singleLabelings = new storm::storage::BitVector*[apCountMax]; for (uint_fast64_t i = 0; i < apCountMax; ++i) { - this->singleLabelings[i] = new mrmc::storage::BitVector(*atomicPropositionsLabeling.singleLabelings[i]); + this->singleLabelings[i] = new storm::storage::BitVector(*atomicPropositionsLabeling.singleLabelings[i]); } } @@ -82,10 +82,10 @@ public: */ uint_fast64_t addAtomicProposition(std::string ap) { if (nameToLabelingMap.count(ap) != 0) { - throw mrmc::exceptions::OutOfRangeException("Atomic Proposition already exists."); + throw storm::exceptions::OutOfRangeException("Atomic Proposition already exists."); } if (apsCurrent >= apCountMax) { - throw mrmc::exceptions::OutOfRangeException("Added more atomic propositions than" + throw storm::exceptions::OutOfRangeException("Added more atomic propositions than" "previously declared."); } nameToLabelingMap[ap] = apsCurrent; @@ -110,10 +110,10 @@ public: */ void addAtomicPropositionToState(std::string ap, const uint_fast64_t state) { if (nameToLabelingMap.count(ap) == 0) { - throw mrmc::exceptions::OutOfRangeException() << "Atomic Proposition '" << ap << "' unknown."; + throw storm::exceptions::OutOfRangeException() << "Atomic Proposition '" << ap << "' unknown."; } if (state >= stateCount) { - throw mrmc::exceptions::OutOfRangeException("State index out of range."); + throw storm::exceptions::OutOfRangeException("State index out of range."); } this->singleLabelings[nameToLabelingMap[ap]]->set(state, true); } @@ -125,7 +125,7 @@ public: */ std::set getPropositionsForState(uint_fast64_t state) { if (state >= stateCount) { - throw mrmc::exceptions::OutOfRangeException("State index out of range."); + throw storm::exceptions::OutOfRangeException("State index out of range."); } std::set result; for (auto it = nameToLabelingMap.begin(); @@ -164,7 +164,7 @@ public: * @return A pointer to an instance of SingleAtomicPropositionLabeling that * represents the labeling of the states with the given atomic proposition. */ - mrmc::storage::BitVector* getAtomicProposition(std::string ap) { + storm::storage::BitVector* getAtomicProposition(std::string ap) { return (this->singleLabelings[nameToLabelingMap[ap]]); } @@ -222,11 +222,11 @@ private: * a particular atomic proposition, the map from names to indices in this * array has to be used. */ - mrmc::storage::BitVector** singleLabelings; + storm::storage::BitVector** singleLabelings; }; } // namespace models -} // namespace mrmc +} // namespace storm -#endif /* MRMC_MODELS_ATOMICPROPOSITIONSLABELING_H_ */ +#endif /* STORM_MODELS_ATOMICPROPOSITIONSLABELING_H_ */ diff --git a/src/models/Ctmc.h b/src/models/Ctmc.h index 5101cd556..7f21528f0 100644 --- a/src/models/Ctmc.h +++ b/src/models/Ctmc.h @@ -5,8 +5,8 @@ * Author: Christian Dehnert */ -#ifndef MRMC_MODELS_CTMC_H_ -#define MRMC_MODELS_CTMC_H_ +#ifndef STORM_MODELS_CTMC_H_ +#define STORM_MODELS_CTMC_H_ #include #include @@ -18,7 +18,7 @@ #include "src/storage/SquareSparseMatrix.h" #include "src/exceptions/InvalidArgumentException.h" -namespace mrmc { +namespace storm { namespace models { @@ -39,10 +39,10 @@ public: * @param stateLabeling The labeling that assigns a set of atomic * propositions to each state. */ - Ctmc(std::shared_ptr> rateMatrix, - std::shared_ptr stateLabeling, + Ctmc(std::shared_ptr> rateMatrix, + std::shared_ptr stateLabeling, std::shared_ptr> stateRewards = nullptr, - std::shared_ptr> transitionRewardMatrix = nullptr) + std::shared_ptr> transitionRewardMatrix = nullptr) : rateMatrix(rateMatrix), stateLabeling(stateLabeling), stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix), backwardTransitions(nullptr) { @@ -57,7 +57,7 @@ public: stateLabeling(ctmc.stateLabeling), stateRewards(ctmc.stateRewards), transitionRewardMatrix(ctmc.transitionRewardMatrix) { if (ctmc.backardTransitions != nullptr) { - this->backwardTransitions = new mrmc::models::GraphTransitions(*ctmc.backwardTransitions); + this->backwardTransitions = new storm::models::GraphTransitions(*ctmc.backwardTransitions); } } @@ -94,7 +94,7 @@ public: * @return A bit vector in which exactly those bits are set to true that * correspond to a state labeled with the given atomic proposition. */ - mrmc::storage::BitVector* getLabeledStates(std::string ap) const { + storm::storage::BitVector* getLabeledStates(std::string ap) const { return this->stateLabeling->getAtomicProposition(ap); } @@ -104,7 +104,7 @@ public: * @return A pointer to the matrix representing the transition probability * function. */ - std::shared_ptr> getTransitionRateMatrix() const { + std::shared_ptr> getTransitionRateMatrix() const { return this->rateMatrix; } @@ -112,7 +112,7 @@ public: * Returns a pointer to the matrix representing the transition rewards. * @return A pointer to the matrix representing the transition rewards. */ - std::shared_ptr> getTransitionRewardMatrix() const { + std::shared_ptr> getTransitionRewardMatrix() const { return this->transitionRewardMatrix; } @@ -135,9 +135,9 @@ public: * Retrieves a reference to the backwards transition relation. * @return A reference to the backwards transition relation. */ - mrmc::models::GraphTransitions& getBackwardTransitions() { + storm::models::GraphTransitions& getBackwardTransitions() { if (this->backwardTransitions == nullptr) { - this->backwardTransitions = new mrmc::models::GraphTransitions(this->probabilityMatrix, false); + this->backwardTransitions = new storm::models::GraphTransitions(this->probabilityMatrix, false); } return *this->backwardTransitions; } @@ -164,26 +164,26 @@ public: private: /*! A matrix representing the transition rate function of the CTMC. */ - std::shared_ptr> rateMatrix; + std::shared_ptr> rateMatrix; /*! The labeling of the states of the CTMC. */ - std::shared_ptr stateLabeling; + std::shared_ptr stateLabeling; /*! The state-based rewards of the CTMC. */ std::shared_ptr> stateRewards; /*! The transition-based rewards of the CTMC. */ - std::shared_ptr> transitionRewardMatrix; + std::shared_ptr> transitionRewardMatrix; /*! * A data structure that stores the predecessors for all states. This is * needed for backwards directed searches. */ - mrmc::models::GraphTransitions* backwardTransitions; + storm::models::GraphTransitions* backwardTransitions; }; } // namespace models -} // namespace mrmc +} // namespace storm -#endif /* MRMC_MODELS_DTMC_H_ */ +#endif /* STORM_MODELS_DTMC_H_ */ diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 0018d5274..69831533b 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -5,8 +5,8 @@ * Author: Christian Dehnert */ -#ifndef MRMC_MODELS_DTMC_H_ -#define MRMC_MODELS_DTMC_H_ +#ifndef STORM_MODELS_DTMC_H_ +#define STORM_MODELS_DTMC_H_ #include #include @@ -18,7 +18,7 @@ #include "src/storage/SquareSparseMatrix.h" #include "src/exceptions/InvalidArgumentException.h" -namespace mrmc { +namespace storm { namespace models { @@ -39,10 +39,10 @@ public: * @param stateLabeling The labeling that assigns a set of atomic * propositions to each state. */ - Dtmc(std::shared_ptr> probabilityMatrix, - std::shared_ptr stateLabeling, + Dtmc(std::shared_ptr> probabilityMatrix, + std::shared_ptr stateLabeling, std::shared_ptr> stateRewards = nullptr, - std::shared_ptr> transitionRewardMatrix = nullptr) + std::shared_ptr> transitionRewardMatrix = nullptr) : probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix), backwardTransitions(nullptr) { @@ -60,7 +60,7 @@ public: stateLabeling(dtmc.stateLabeling), stateRewards(dtmc.stateRewards), transitionRewardMatrix(dtmc.transitionRewardMatrix) { if (dtmc.backardTransitions != nullptr) { - this->backwardTransitions = new mrmc::models::GraphTransitions(*dtmc.backwardTransitions); + this->backwardTransitions = new storm::models::GraphTransitions(*dtmc.backwardTransitions); } if (!this->checkValidityProbabilityMatrix()) { std::cerr << "Probability matrix is invalid" << std::endl; @@ -100,7 +100,7 @@ public: * @return A bit vector in which exactly those bits are set to true that * correspond to a state labeled with the given atomic proposition. */ - mrmc::storage::BitVector* getLabeledStates(std::string ap) const { + storm::storage::BitVector* getLabeledStates(std::string ap) const { return this->stateLabeling->getAtomicProposition(ap); } @@ -110,7 +110,7 @@ public: * @return A pointer to the matrix representing the transition probability * function. */ - std::shared_ptr> getTransitionProbabilityMatrix() const { + std::shared_ptr> getTransitionProbabilityMatrix() const { return this->probabilityMatrix; } @@ -118,7 +118,7 @@ public: * Returns a pointer to the matrix representing the transition rewards. * @return A pointer to the matrix representing the transition rewards. */ - std::shared_ptr> getTransitionRewardMatrix() const { + std::shared_ptr> getTransitionRewardMatrix() const { return this->transitionRewardMatrix; } @@ -141,9 +141,9 @@ public: * Retrieves a reference to the backwards transition relation. * @return A reference to the backwards transition relation. */ - mrmc::models::GraphTransitions& getBackwardTransitions() { + storm::models::GraphTransitions& getBackwardTransitions() { if (this->backwardTransitions == nullptr) { - this->backwardTransitions = new mrmc::models::GraphTransitions(this->probabilityMatrix, false); + this->backwardTransitions = new storm::models::GraphTransitions(this->probabilityMatrix, false); } return *this->backwardTransitions; } @@ -184,26 +184,26 @@ private: } /*! A matrix representing the transition probability function of the DTMC. */ - std::shared_ptr> probabilityMatrix; + std::shared_ptr> probabilityMatrix; /*! The labeling of the states of the DTMC. */ - std::shared_ptr stateLabeling; + std::shared_ptr stateLabeling; /*! The state-based rewards of the DTMC. */ std::shared_ptr> stateRewards; /*! The transition-based rewards of the DTMC. */ - std::shared_ptr> transitionRewardMatrix; + std::shared_ptr> transitionRewardMatrix; /*! * A data structure that stores the predecessors for all states. This is * needed for backwards directed searches. */ - mrmc::models::GraphTransitions* backwardTransitions; + storm::models::GraphTransitions* backwardTransitions; }; } // namespace models -} // namespace mrmc +} // namespace storm -#endif /* MRMC_MODELS_DTMC_H_ */ +#endif /* STORM_MODELS_DTMC_H_ */ diff --git a/src/models/GraphTransitions.h b/src/models/GraphTransitions.h index 6d45bad88..3ccc6bed5 100644 --- a/src/models/GraphTransitions.h +++ b/src/models/GraphTransitions.h @@ -5,15 +5,15 @@ * Author: Christian Dehnert */ -#ifndef MRMC_MODELS_GRAPHTRANSITIONS_H_ -#define MRMC_MODELS_GRAPHTRANSITIONS_H_ +#ifndef STORM_MODELS_GRAPHTRANSITIONS_H_ +#define STORM_MODELS_GRAPHTRANSITIONS_H_ #include "src/storage/SquareSparseMatrix.h" #include #include -namespace mrmc { +namespace storm { namespace models { @@ -39,7 +39,7 @@ public: * @param forward If set to true, this objects will store the graph structure * of the backwards transition relation. */ - GraphTransitions(std::shared_ptr> transitionMatrix, bool forward) + GraphTransitions(std::shared_ptr> transitionMatrix, bool forward) : successorList(nullptr), stateIndications(nullptr), numberOfStates(transitionMatrix->getRowCount()), numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) { if (forward) { this->initializeForward(transitionMatrix); @@ -87,7 +87,7 @@ private: * Initializes this graph transitions object using the forward transition * relation given by means of a sparse matrix. */ - void initializeForward(std::shared_ptr> transitionMatrix) { + void initializeForward(std::shared_ptr> transitionMatrix) { this->successorList = new uint_fast64_t[numberOfNonZeroTransitions]; this->stateIndications = new uint_fast64_t[numberOfStates + 1]; @@ -109,7 +109,7 @@ private: * relation, whose forward transition relation is given by means of a sparse * matrix. */ - void initializeBackward(std::shared_ptr> transitionMatrix) { + void initializeBackward(std::shared_ptr> transitionMatrix) { this->successorList = new uint_fast64_t[numberOfNonZeroTransitions](); this->stateIndications = new uint_fast64_t[numberOfStates + 1](); @@ -173,6 +173,6 @@ private: } // namespace models -} // namespace mrmc +} // namespace storm -#endif /* MRMC_MODELS_GRAPHTRANSITIONS_H_ */ +#endif /* STORM_MODELS_GRAPHTRANSITIONS_H_ */ diff --git a/src/parser/AtomicPropositionLabelingParser.cpp b/src/parser/AtomicPropositionLabelingParser.cpp index f5fcbc5c6..07dc2d344 100644 --- a/src/parser/AtomicPropositionLabelingParser.cpp +++ b/src/parser/AtomicPropositionLabelingParser.cpp @@ -26,7 +26,7 @@ #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; -namespace mrmc { +namespace storm { namespace parser { @@ -87,14 +87,14 @@ AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t n LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). File header is corrupted."); if (! foundDecl) LOG4CPLUS_ERROR(logger, "\tDid not find #DECLARATION token."); if (! foundEnd) LOG4CPLUS_ERROR(logger, "\tDid not find #END token."); - throw mrmc::exceptions::WrongFileFormatException(); + throw storm::exceptions::WrongFileFormatException(); } } /* * create labeling object with given node and proposition count */ - this->labeling = std::shared_ptr(new mrmc::models::AtomicPropositionsLabeling(node_count, proposition_count)); + this->labeling = std::shared_ptr(new storm::models::AtomicPropositionsLabeling(node_count, proposition_count)); /* * second run: add propositions and node labels to labeling @@ -117,7 +117,7 @@ AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t n * if token is longer than our buffer, the following strncpy code might get risky... */ LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). Atomic proposition with length > " << (sizeof(proposition)-1) << " was found."); - throw mrmc::exceptions::WrongFileFormatException(); + throw storm::exceptions::WrongFileFormatException(); } else if (cnt > 0) { /* * next token is: #DECLARATION: just skip it @@ -179,4 +179,4 @@ AtomicPropositionLabelingParser::AtomicPropositionLabelingParser(uint_fast64_t n } } //namespace parser -} //namespace mrmc +} //namespace storm diff --git a/src/parser/AtomicPropositionLabelingParser.h b/src/parser/AtomicPropositionLabelingParser.h index d6d7fa84c..e2a24b6e9 100644 --- a/src/parser/AtomicPropositionLabelingParser.h +++ b/src/parser/AtomicPropositionLabelingParser.h @@ -1,5 +1,5 @@ -#ifndef MRMC_PARSER_LABPARSER_H_ -#define MRMC_PARSER_LABPARSER_H_ +#ifndef STORM_PARSER_LABPARSER_H_ +#define STORM_PARSER_LABPARSER_H_ #include "src/models/AtomicPropositionsLabeling.h" #include "boost/integer/integer_mask.hpp" @@ -8,7 +8,7 @@ #include -namespace mrmc { +namespace storm { namespace parser { /*! @@ -21,15 +21,15 @@ class AtomicPropositionLabelingParser : Parser { public: AtomicPropositionLabelingParser(uint_fast64_t node_count, std::string const &filename); - std::shared_ptr getLabeling() { + std::shared_ptr getLabeling() { return this->labeling; } private: - std::shared_ptr labeling; + std::shared_ptr labeling; }; } // namespace parser -} // namespace mrmc +} // namespace storm -#endif /* MRMC_PARSER_LABPARSER_H_ */ +#endif /* STORM_PARSER_LABPARSER_H_ */ diff --git a/src/parser/AutoTransitionParser.cpp b/src/parser/AutoTransitionParser.cpp index 402e8e14e..517f72850 100644 --- a/src/parser/AutoTransitionParser.cpp +++ b/src/parser/AutoTransitionParser.cpp @@ -5,7 +5,7 @@ #include "DeterministicSparseTransitionParser.h" #include "NonDeterministicSparseTransitionParser.h" -namespace mrmc { +namespace storm { namespace parser { AutoTransitionParser::AutoTransitionParser(const std::string& filename) @@ -20,7 +20,7 @@ AutoTransitionParser::AutoTransitionParser(const std::string& filename) else { LOG4CPLUS_ERROR(logger, "Could not determine file type of " << filename << ". Filename suggests " << name << " but transitions look like " << transitions); LOG4CPLUS_ERROR(logger, "Please fix your file and try again."); - throw mrmc::exceptions::WrongFileFormatException() << "Could not determine type of file " << filename; + throw storm::exceptions::WrongFileFormatException() << "Could not determine type of file " << filename; } } else { if ((hint == name) && (name == transitions)) this->type = name; @@ -77,4 +77,4 @@ std::pair AutoTransitionParser::analyzeContent(co } //namespace parser -} //namespace mrmc +} //namespace storm diff --git a/src/parser/AutoTransitionParser.h b/src/parser/AutoTransitionParser.h index a964ac1fe..334173975 100644 --- a/src/parser/AutoTransitionParser.h +++ b/src/parser/AutoTransitionParser.h @@ -1,5 +1,5 @@ -#ifndef MRMC_PARSER_AUTOPARSER_H_ -#define MRMC_PARSER_AUTOPARSER_H_ +#ifndef STORM_PARSER_AUTOPARSER_H_ +#define STORM_PARSER_AUTOPARSER_H_ #include "src/models/AtomicPropositionsLabeling.h" #include "boost/integer/integer_mask.hpp" @@ -10,7 +10,7 @@ #include #include -namespace mrmc { +namespace storm { namespace parser { /*! @@ -83,6 +83,6 @@ class AutoTransitionParser : Parser { }; } // namespace parser -} // namespace mrmc +} // namespace storm -#endif /* MRMC_PARSER_AUTOPARSER_H_ */ +#endif /* STORM_PARSER_AUTOPARSER_H_ */ diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index d5dd504c1..f3d3b9d00 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -24,7 +24,7 @@ #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; -namespace mrmc { +namespace storm { namespace parser{ /*! @@ -131,7 +131,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st if (non_zero == 0) { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": erroneous file format."); - throw mrmc::exceptions::WrongFileFormatException(); + throw storm::exceptions::WrongFileFormatException(); } /* @@ -155,7 +155,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st * non-zero elements has to be specified (which is non_zero, computed by make_first_pass) */ LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << "."); - this->matrix = std::shared_ptr>(new mrmc::storage::SquareSparseMatrix(maxnode + 1)); + this->matrix = std::shared_ptr>(new storm::storage::SquareSparseMatrix(maxnode + 1)); if (this->matrix == NULL) { LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << "."); @@ -189,4 +189,4 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st } } //namespace parser -} //namespace mrmc +} //namespace storm diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index b90924fbd..a5b8560de 100644 --- a/src/parser/DeterministicSparseTransitionParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -1,5 +1,5 @@ -#ifndef MRMC_PARSER_TRAPARSER_H_ -#define MRMC_PARSER_TRAPARSER_H_ +#ifndef STORM_PARSER_TRAPARSER_H_ +#define STORM_PARSER_TRAPARSER_H_ #include "src/storage/SquareSparseMatrix.h" @@ -8,7 +8,7 @@ #include -namespace mrmc { +namespace storm { namespace parser { /*! @@ -19,18 +19,18 @@ class DeterministicSparseTransitionParser : public Parser { public: DeterministicSparseTransitionParser(std::string const &filename); - std::shared_ptr> getMatrix() { + std::shared_ptr> getMatrix() { return this->matrix; } private: - std::shared_ptr> matrix; + std::shared_ptr> matrix; uint_fast64_t firstPass(char* buf, uint_fast64_t &maxnode); }; } // namespace parser -} // namespace mrmc +} // namespace storm -#endif /* MRMC_PARSER_TRAPARSER_H_ */ +#endif /* STORM_PARSER_TRAPARSER_H_ */ diff --git a/src/parser/DtmcParser.cpp b/src/parser/DtmcParser.cpp index edeab198d..4f4ed2645 100644 --- a/src/parser/DtmcParser.cpp +++ b/src/parser/DtmcParser.cpp @@ -10,7 +10,7 @@ #include "AtomicPropositionLabelingParser.h" #include "SparseStateRewardParser.h" -namespace mrmc { +namespace storm { namespace parser { /*! @@ -25,25 +25,25 @@ namespace parser { */ DtmcParser::DtmcParser(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { - mrmc::parser::DeterministicSparseTransitionParser tp(transitionSystemFile); + storm::parser::DeterministicSparseTransitionParser tp(transitionSystemFile); uint_fast64_t stateCount = tp.getMatrix()->getRowCount(); std::shared_ptr> stateRewards = nullptr; - std::shared_ptr> transitionRewards = nullptr; + std::shared_ptr> transitionRewards = nullptr; - mrmc::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile); + storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile); if (stateRewardFile != "") { - mrmc::parser::SparseStateRewardParser srp(stateCount, stateRewardFile); + storm::parser::SparseStateRewardParser srp(stateCount, stateRewardFile); stateRewards = srp.getStateRewards(); } if (transitionRewardFile != "") { - mrmc::parser::DeterministicSparseTransitionParser trp(transitionRewardFile); + storm::parser::DeterministicSparseTransitionParser trp(transitionRewardFile); transitionRewards = trp.getMatrix(); } - dtmc = std::shared_ptr>(new mrmc::models::Dtmc(tp.getMatrix(), lp.getLabeling(), stateRewards, transitionRewards)); + dtmc = std::shared_ptr>(new storm::models::Dtmc(tp.getMatrix(), lp.getLabeling(), stateRewards, transitionRewards)); } } /* namespace parser */ -} /* namespace mrmc */ +} /* namespace storm */ diff --git a/src/parser/DtmcParser.h b/src/parser/DtmcParser.h index 844617e91..b4ab4a3b5 100644 --- a/src/parser/DtmcParser.h +++ b/src/parser/DtmcParser.h @@ -11,7 +11,7 @@ #include "Parser.h" #include "models/Dtmc.h" -namespace mrmc { +namespace storm { namespace parser { /*! @@ -22,19 +22,19 @@ namespace parser { * * @Note The labeling representation in the file may use at most as much nodes as are specified in the dtmc. */ -class DtmcParser: public mrmc::parser::Parser { +class DtmcParser: public storm::parser::Parser { public: DtmcParser(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); - std::shared_ptr> getDtmc() { + std::shared_ptr> getDtmc() { return this->dtmc; } private: - std::shared_ptr> dtmc; + std::shared_ptr> dtmc; }; } /* namespace parser */ -} /* namespace mrmc */ +} /* namespace storm */ #endif /* DTMCPARSER_H_ */ diff --git a/src/parser/NonDeterministicSparseTransitionParser.cpp b/src/parser/NonDeterministicSparseTransitionParser.cpp index b03c3bed6..822235c11 100644 --- a/src/parser/NonDeterministicSparseTransitionParser.cpp +++ b/src/parser/NonDeterministicSparseTransitionParser.cpp @@ -24,7 +24,7 @@ #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; -namespace mrmc { +namespace storm { namespace parser{ /*! @@ -144,7 +144,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s if (non_zero == nullptr) { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": erroneous file format."); - throw mrmc::exceptions::WrongFileFormatException(); + throw storm::exceptions::WrongFileFormatException(); } /* @@ -168,7 +168,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s * non-zero elements has to be specified (which is non_zero, computed by make_first_pass) */ LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << "."); - this->matrix = std::shared_ptr>(new mrmc::storage::SquareSparseMatrix(maxnode + 1)); + this->matrix = std::shared_ptr>(new storm::storage::SquareSparseMatrix(maxnode + 1)); if (this->matrix == NULL) { LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << "."); @@ -204,4 +204,4 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s } } //namespace parser -} //namespace mrmc +} //namespace storm diff --git a/src/parser/NonDeterministicSparseTransitionParser.h b/src/parser/NonDeterministicSparseTransitionParser.h index e1a29ef20..bc144b160 100644 --- a/src/parser/NonDeterministicSparseTransitionParser.h +++ b/src/parser/NonDeterministicSparseTransitionParser.h @@ -1,5 +1,5 @@ -#ifndef MRMC_PARSER_NONDETTRAPARSER_H_ -#define MRMC_PARSER_NONDETTRAPARSER_H_ +#ifndef STORM_PARSER_NONDETTRAPARSER_H_ +#define STORM_PARSER_NONDETTRAPARSER_H_ #include "src/storage/SquareSparseMatrix.h" @@ -9,7 +9,7 @@ #include #include -namespace mrmc { +namespace storm { namespace parser { /*! @@ -20,18 +20,18 @@ class NonDeterministicSparseTransitionParser : public Parser { public: NonDeterministicSparseTransitionParser(std::string const &filename); - std::shared_ptr> getMatrix() { + std::shared_ptr> getMatrix() { return this->matrix; } private: - std::shared_ptr> matrix; + std::shared_ptr> matrix; std::unique_ptr> firstPass(char* buf, uint_fast64_t &maxnode, uint_fast64_t &maxchoice); }; } // namespace parser -} // namespace mrmc +} // namespace storm -#endif /* MRMC_PARSER_NONDETTRAPARSER_H_ */ +#endif /* STORM_PARSER_NONDETTRAPARSER_H_ */ diff --git a/src/parser/Parser.cpp b/src/parser/Parser.cpp index cbcfc0b57..0c53f3ffa 100644 --- a/src/parser/Parser.cpp +++ b/src/parser/Parser.cpp @@ -13,17 +13,17 @@ extern log4cplus::Logger logger; /*! * Calls strtol() internally and checks if the new pointer is different * from the original one, i.e. if str != *end. If they are the same, a - * mrmc::exceptions::WrongFileFormatException will be thrown. + * storm::exceptions::WrongFileFormatException will be thrown. * @param str String to parse * @param end New pointer will be written there * @return Result of strtol() */ -uint_fast64_t mrmc::parser::Parser::checked_strtol(const char* str, char** end) { +uint_fast64_t storm::parser::Parser::checked_strtol(const char* str, char** end) { uint_fast64_t res = strtol(str, end, 10); if (str == *end) { LOG4CPLUS_ERROR(logger, "Error while parsing integer. Next input token is not a number."); LOG4CPLUS_ERROR(logger, "\tUpcoming input is: \"" << std::string(str, 0, 16) << "\""); - throw mrmc::exceptions::WrongFileFormatException("Error while parsing integer. Next input token is not a number."); + throw storm::exceptions::WrongFileFormatException("Error while parsing integer. Next input token is not a number."); } return res; } @@ -34,7 +34,7 @@ uint_fast64_t mrmc::parser::Parser::checked_strtol(const char* str, char** end) * @param buf String buffer * @return pointer to first non-whitespace character */ -char* mrmc::parser::Parser::trimWhitespaces(char* buf) { +char* storm::parser::Parser::trimWhitespaces(char* buf) { /*TODO: Maybe use memcpy to copy all the stuff from the first non-whitespace char * to the position of the buffer, so we don't have to keep track of 2 pointers. */ @@ -48,7 +48,7 @@ char* mrmc::parser::Parser::trimWhitespaces(char* buf) { * and a log entry is written. * @param filename file to be opened */ -mrmc::parser::MappedFile::MappedFile(const char* filename) { +storm::parser::MappedFile::MappedFile(const char* filename) { #if defined LINUX || defined MACOSX /* * Do file mapping for reasonable systems. @@ -60,20 +60,20 @@ mrmc::parser::MappedFile::MappedFile(const char* filename) { if (stat64(filename, &(this->st)) != 0) { #endif LOG4CPLUS_ERROR(logger, "Error in stat(" << filename << ")."); - throw exceptions::FileIoException("mrmc::parser::MappedFile Error in stat()"); + throw exceptions::FileIoException("storm::parser::MappedFile Error in stat()"); } this->file = open(filename, O_RDONLY); if (this->file < 0) { LOG4CPLUS_ERROR(logger, "Error in open(" << filename << ")."); - throw exceptions::FileIoException("mrmc::parser::MappedFile Error in open()"); + throw exceptions::FileIoException("storm::parser::MappedFile Error in open()"); } this->data = (char*) mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE, this->file, 0); if (this->data == (char*)-1) { close(this->file); LOG4CPLUS_ERROR(logger, "Error in mmap(" << filename << ")."); - throw exceptions::FileIoException("mrmc::parser::MappedFile Error in mmap()"); + throw exceptions::FileIoException("storm::parser::MappedFile Error in mmap()"); } this->dataend = this->data + this->st.st_size; #elif defined WINDOWS @@ -83,20 +83,20 @@ mrmc::parser::MappedFile::MappedFile(const char* filename) { */ if (_stat64(filename, &(this->st)) != 0) { LOG4CPLUS_ERROR(logger, "Error in _stat(" << filename << ")."); - throw exceptions::FileIoException("mrmc::parser::MappedFile Error in stat()"); + throw exceptions::FileIoException("storm::parser::MappedFile Error in stat()"); } this->file = CreateFileA(filename, GENERIC_READ, 0, NULL, OPEN_ALWAYS, FILE_ATTRIBUTE_NORMAL, NULL); if (this->file == INVALID_HANDLE_VALUE) { LOG4CPLUS_ERROR(logger, "Error in CreateFileA(" << filename << ")."); - throw exceptions::FileIoException("mrmc::parser::MappedFile Error in CreateFileA()"); + throw exceptions::FileIoException("storm::parser::MappedFile Error in CreateFileA()"); } this->mapping = CreateFileMappingA(this->file, NULL, PAGE_READONLY, (DWORD)(st.st_size >> 32), (DWORD)st.st_size, NULL); if (this->mapping == NULL) { CloseHandle(this->file); LOG4CPLUS_ERROR(logger, "Error in CreateFileMappingA(" << filename << ")."); - throw exceptions::FileIoException("mrmc::parser::MappedFile Error in CreateFileMappingA()"); + throw exceptions::FileIoException("storm::parser::MappedFile Error in CreateFileMappingA()"); } this->data = static_cast(MapViewOfFile(this->mapping, FILE_MAP_READ, 0, 0, this->st.st_size)); @@ -104,7 +104,7 @@ mrmc::parser::MappedFile::MappedFile(const char* filename) { CloseHandle(this->mapping); CloseHandle(this->file); LOG4CPLUS_ERROR(logger, "Error in MapViewOfFile(" << filename << ")."); - throw exceptions::FileIoException("mrmc::parser::MappedFile Error in MapViewOfFile()"); + throw exceptions::FileIoException("storm::parser::MappedFile Error in MapViewOfFile()"); } this->dataend = this->data + this->st.st_size; #endif @@ -113,7 +113,7 @@ mrmc::parser::MappedFile::MappedFile(const char* filename) { /*! * Will unmap the data and close the file. */ -mrmc::parser::MappedFile::~MappedFile() { +storm::parser::MappedFile::~MappedFile() { #if defined LINUX || defined MACOSX munmap(this->data, this->st.st_size); close(this->file); diff --git a/src/parser/Parser.h b/src/parser/Parser.h index 03f6f002a..9aa8eef79 100644 --- a/src/parser/Parser.h +++ b/src/parser/Parser.h @@ -5,8 +5,8 @@ * Author: Gereon Kremer */ -#ifndef MRMC_PARSER_PARSER_H_ -#define MRMC_PARSER_PARSER_H_ +#ifndef STORM_PARSER_PARSER_H_ +#define STORM_PARSER_PARSER_H_ #include "src/utility/OsDetection.h" @@ -19,7 +19,7 @@ #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFileFormatException.h" -namespace mrmc { +namespace storm { /*! * @brief Contains all file parser and helper classes. @@ -110,6 +110,6 @@ namespace parser { }; } // namespace parser -} // namespace mrmc +} // namespace storm -#endif /* MRMC_PARSER_PARSER_H_ */ +#endif /* STORM_PARSER_PARSER_H_ */ diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index f1a23077a..9c0850ca5 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -58,7 +58,7 @@ namespace /*! * @brief Resulting formula. */ - mrmc::formula::PctlFormula* result; + storm::formula::PctlFormula* result; struct dump { @@ -109,7 +109,7 @@ namespace * const double T = 9; * const double p = 0.01; * - * Parser can be run via ./mrmc --test-prctl foo bar + * Parser can be run via ./storm --test-prctl foo bar * foo and bar are necessary, otherwise the option parser fails... */ @@ -130,10 +130,10 @@ namespace }; } -mrmc::parser::PrctlParser::PrctlParser(const char* filename) +storm::parser::PrctlParser::PrctlParser(const char* filename) { SpiritParser p; - mrmc::parser::MappedFile file(filename); + storm::parser::MappedFile file(filename); char* data = file.data; if (bs::qi::parse< char const* >(data, file.dataend, p)) diff --git a/src/parser/PrctlParser.h b/src/parser/PrctlParser.h index 24dc746bb..79c2e81c7 100644 --- a/src/parser/PrctlParser.h +++ b/src/parser/PrctlParser.h @@ -1,10 +1,10 @@ -#ifndef MRMC_PARSER_PRCTLPARSER_H_ -#define MRMC_PARSER_PRCTLPARSER_H_ +#ifndef STORM_PARSER_PRCTLPARSER_H_ +#define STORM_PARSER_PRCTLPARSER_H_ #include "src/formula/PctlFormula.h" #include "src/parser/Parser.h" -namespace mrmc { +namespace storm { namespace parser { /*! @@ -18,16 +18,16 @@ class PrctlParser : Parser /*! * @brief return formula object parsed from file. */ - mrmc::formula::PctlFormula* getFormula() + storm::formula::PctlFormula* getFormula() { return this->formula; } private: - mrmc::formula::PctlFormula* formula; + storm::formula::PctlFormula* formula; }; } // namespace parser -} // namespace mrmc +} // namespace storm -#endif /* MRMC_PARSER_PRCTLPARSER_H_ */ +#endif /* STORM_PARSER_PRCTLPARSER_H_ */ diff --git a/src/parser/SparseStateRewardParser.cpp b/src/parser/SparseStateRewardParser.cpp index 871bc9ab6..bac83a2c0 100644 --- a/src/parser/SparseStateRewardParser.cpp +++ b/src/parser/SparseStateRewardParser.cpp @@ -25,7 +25,7 @@ #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; -namespace mrmc { +namespace storm { namespace parser { @@ -57,7 +57,7 @@ SparseStateRewardParser::SparseStateRewardParser(uint_fast64_t stateCount, std:: reward = strtod(buf, &buf); if (reward < 0.0) { LOG4CPLUS_ERROR(logger, "Expected positive probability but got \"" << std::string(buf, 0, 16) << "\"."); - throw mrmc::exceptions::WrongFileFormatException() << "State reward file specifies illegal reward value."; + throw storm::exceptions::WrongFileFormatException() << "State reward file specifies illegal reward value."; } (*this->stateRewards)[state] = reward; @@ -69,4 +69,4 @@ SparseStateRewardParser::SparseStateRewardParser(uint_fast64_t stateCount, std:: } //namespace parser -} //namespace mrmc +} //namespace storm diff --git a/src/parser/SparseStateRewardParser.h b/src/parser/SparseStateRewardParser.h index 604070759..3ed71e1c2 100644 --- a/src/parser/SparseStateRewardParser.h +++ b/src/parser/SparseStateRewardParser.h @@ -1,12 +1,12 @@ -#ifndef MRMC_PARSER_SPARSESTATEREWARDPARSER_H_ -#define MRMC_PARSER_SPARSESTATEREWARDPARSER_H_ +#ifndef STORM_PARSER_SPARSESTATEREWARDPARSER_H_ +#define STORM_PARSER_SPARSESTATEREWARDPARSER_H_ #include "boost/integer/integer_mask.hpp" #include "src/parser/Parser.h" #include #include -namespace mrmc { +namespace storm { namespace parser { @@ -27,6 +27,6 @@ class SparseStateRewardParser : Parser { } // namespace parser -} // namespace mrmc +} // namespace storm -#endif /* MRMC_PARSER_SPARSESTATEREWARDPARSER_H_ */ +#endif /* STORM_PARSER_SPARSESTATEREWARDPARSER_H_ */ diff --git a/src/reward/RewardModel.h b/src/reward/RewardModel.h index c2ffb8b79..abf79f164 100644 --- a/src/reward/RewardModel.h +++ b/src/reward/RewardModel.h @@ -5,14 +5,14 @@ * Author: Philipp Berger */ -#ifndef MRMC_REWARD_REWARDMODEL_H_ -#define MRMC_REWARD_REWARDMODEL_H_ +#ifndef STORM_REWARD_REWARDMODEL_H_ +#define STORM_REWARD_REWARDMODEL_H_ #include #include "boost/integer/integer_mask.hpp" -namespace mrmc { +namespace storm { namespace reward { @@ -74,6 +74,6 @@ class RewardModel { } //namespace reward -} //namespace mrmc +} //namespace storm -#endif /* MRMC_REWARD_REWARDMODEL_H_ */ +#endif /* STORM_REWARD_REWARDMODEL_H_ */ diff --git a/src/solver/GraphAnalyzer.h b/src/solver/GraphAnalyzer.h index 6660ad2f9..3c99b4426 100644 --- a/src/solver/GraphAnalyzer.h +++ b/src/solver/GraphAnalyzer.h @@ -5,8 +5,8 @@ * Author: Christian Dehnert */ -#ifndef MRMC_SOLVER_GRAPHANALYZER_H_ -#define MRMC_SOLVER_GRAPHANALYZER_H_ +#ifndef STORM_SOLVER_GRAPHANALYZER_H_ +#define STORM_SOLVER_GRAPHANALYZER_H_ #include "src/models/Dtmc.h" #include "src/exceptions/InvalidArgumentException.h" @@ -16,7 +16,7 @@ extern log4cplus::Logger logger; -namespace mrmc { +namespace storm { namespace solver { @@ -34,15 +34,15 @@ public: * a paths satisfying phi until psi. */ template - static void getExistsPhiUntilPsiStates(mrmc::models::Dtmc& model, const mrmc::storage::BitVector& phiStates, const mrmc::storage::BitVector& psiStates, mrmc::storage::BitVector* existsPhiUntilPsiStates) { + static void getExistsPhiUntilPsiStates(storm::models::Dtmc& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* existsPhiUntilPsiStates) { // Check for valid parameter. if (existsPhiUntilPsiStates == nullptr) { LOG4CPLUS_ERROR(logger, "Parameter 'existsPhiUntilPhiStates' must not be null."); - throw mrmc::exceptions::InvalidArgumentException("Parameter 'existsPhiUntilPhiStates' must not be null."); + throw storm::exceptions::InvalidArgumentException("Parameter 'existsPhiUntilPhiStates' must not be null."); } // Get the backwards transition relation from the model to ease the search. - mrmc::models::GraphTransitions& backwardTransitions = model.getBackwardTransitions(); + storm::models::GraphTransitions& backwardTransitions = model.getBackwardTransitions(); // Add all psi states as the already satisfy the condition. *existsPhiUntilPsiStates |= psiStates; @@ -81,11 +81,11 @@ public: * have paths satisfying phi until psi. */ template - static void getAlwaysPhiUntilPsiStates(mrmc::models::Dtmc& model, const mrmc::storage::BitVector& phiStates, const mrmc::storage::BitVector& psiStates, const mrmc::storage::BitVector& existsPhiUntilPsiStates, mrmc::storage::BitVector* alwaysPhiUntilPsiStates) { + static void getAlwaysPhiUntilPsiStates(storm::models::Dtmc& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, const storm::storage::BitVector& existsPhiUntilPsiStates, storm::storage::BitVector* alwaysPhiUntilPsiStates) { // Check for valid parameter. if (alwaysPhiUntilPsiStates == nullptr) { LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null."); - throw mrmc::exceptions::InvalidArgumentException("Parameter 'alwaysPhiUntilPhiStates' must not be null."); + throw storm::exceptions::InvalidArgumentException("Parameter 'alwaysPhiUntilPhiStates' must not be null."); } GraphAnalyzer::getExistsPhiUntilPsiStates(model, ~psiStates, ~existsPhiUntilPsiStates, alwaysPhiUntilPsiStates); @@ -105,15 +105,15 @@ public: * have paths satisfying phi until psi. */ template - static void getPhiUntilPsiStates(mrmc::models::Dtmc& model, const mrmc::storage::BitVector& phiStates, const mrmc::storage::BitVector& psiStates, mrmc::storage::BitVector* existsPhiUntilPsiStates, mrmc::storage::BitVector* alwaysPhiUntilPsiStates) { + static void getPhiUntilPsiStates(storm::models::Dtmc& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* existsPhiUntilPsiStates, storm::storage::BitVector* alwaysPhiUntilPsiStates) { // Check for valid parameters. if (existsPhiUntilPsiStates == nullptr) { LOG4CPLUS_ERROR(logger, "Parameter 'existsPhiUntilPhiStates' must not be null."); - throw mrmc::exceptions::InvalidArgumentException("Parameter 'existsPhiUntilPhiStates' must not be null."); + throw storm::exceptions::InvalidArgumentException("Parameter 'existsPhiUntilPhiStates' must not be null."); } if (alwaysPhiUntilPsiStates == nullptr) { LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null."); - throw mrmc::exceptions::InvalidArgumentException("Parameter 'alwaysPhiUntilPhiStates' must not be null."); + throw storm::exceptions::InvalidArgumentException("Parameter 'alwaysPhiUntilPhiStates' must not be null."); } // Perform search. @@ -125,6 +125,6 @@ public: } // namespace solver -} // namespace mrmc +} // namespace storm -#endif /* MRMC_SOLVER_GRAPHANALYZER_H_ */ +#endif /* STORM_SOLVER_GRAPHANALYZER_H_ */ diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index 041272daf..091092824 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -1,5 +1,5 @@ -#ifndef MRMC_STORAGE_BITVECTOR_H_ -#define MRMC_STORAGE_BITVECTOR_H_ +#ifndef STORM_STORAGE_BITVECTOR_H_ +#define STORM_STORAGE_BITVECTOR_H_ #include #include @@ -18,7 +18,7 @@ extern log4cplus::Logger logger; #include -namespace mrmc { +namespace storm { namespace storage { @@ -102,7 +102,7 @@ public: // Check whether the given length is valid. if (length == 0) { LOG4CPLUS_ERROR(logger, "Trying to create bit vector of size 0."); - throw mrmc::exceptions::InvalidArgumentException("Trying to create a bit vector of size 0."); + throw storm::exceptions::InvalidArgumentException("Trying to create a bit vector of size 0."); } // Compute the correct number of buckets needed to store the given number of bits @@ -205,7 +205,7 @@ public: */ void set(const uint_fast64_t index, const bool value) { uint_fast64_t bucket = index >> 6; - if (bucket >= this->bucketCount) throw mrmc::exceptions::OutOfRangeException(); + if (bucket >= this->bucketCount) throw storm::exceptions::OutOfRangeException(); uint_fast64_t mask = static_cast(1) << (index & mod64mask); if (value) { this->bucketArray[bucket] |= mask; @@ -223,7 +223,7 @@ public: */ bool get(const uint_fast64_t index) const { uint_fast64_t bucket = index >> 6; - if (bucket >= this->bucketCount) throw mrmc::exceptions::OutOfRangeException(); + if (bucket >= this->bucketCount) throw storm::exceptions::OutOfRangeException(); uint_fast64_t mask = static_cast(1) << (index & mod64mask); return ((this->bucketArray[bucket] & mask) == mask); } @@ -542,6 +542,6 @@ private: } // namespace storage -} // namespace mrmc +} // namespace storm -#endif // MRMC_STORAGE_BITVECTOR_H_ +#endif // STORM_STORAGE_BITVECTOR_H_ diff --git a/src/storage/JacobiDecomposition.h b/src/storage/JacobiDecomposition.h index 950f89aa5..d62f36712 100644 --- a/src/storage/JacobiDecomposition.h +++ b/src/storage/JacobiDecomposition.h @@ -1,5 +1,5 @@ -#ifndef MRMC_STORAGE_JACOBIDECOMPOSITION_H_ -#define MRMC_STORAGE_JACOBIDECOMPOSITION_H_ +#ifndef STORM_STORAGE_JACOBIDECOMPOSITION_H_ +#define STORM_STORAGE_JACOBIDECOMPOSITION_H_ #include "boost/integer/integer_mask.hpp" @@ -8,7 +8,7 @@ extern log4cplus::Logger logger; -namespace mrmc { +namespace storm { namespace storage { @@ -26,7 +26,7 @@ template class JacobiDecomposition { public: - JacobiDecomposition(mrmc::storage::SquareSparseMatrix * const jacobiLuMatrix, mrmc::storage::SquareSparseMatrix * const jacobiDInvMatrix) : jacobiLuMatrix(jacobiLuMatrix), jacobiDInvMatrix(jacobiDInvMatrix) { + JacobiDecomposition(storm::storage::SquareSparseMatrix * const jacobiLuMatrix, storm::storage::SquareSparseMatrix * const jacobiDInvMatrix) : jacobiLuMatrix(jacobiLuMatrix), jacobiDInvMatrix(jacobiDInvMatrix) { } ~JacobiDecomposition() { @@ -39,7 +39,7 @@ public: * Ownership stays with this class. * @return A reference to the Jacobi LU Matrix */ - mrmc::storage::SquareSparseMatrix& getJacobiLUReference() { + storm::storage::SquareSparseMatrix& getJacobiLUReference() { return *(this->jacobiLuMatrix); } @@ -48,7 +48,7 @@ public: * Ownership stays with this class. * @return A reference to the Jacobi D^{-1} Matrix */ - mrmc::storage::SquareSparseMatrix& getJacobiDInvReference() { + storm::storage::SquareSparseMatrix& getJacobiDInvReference() { return *(this->jacobiDInvMatrix); } @@ -57,7 +57,7 @@ public: * Ownership stays with this class. * @return A pointer to the Jacobi LU Matrix */ - mrmc::storage::SquareSparseMatrix* getJacobiLU() { + storm::storage::SquareSparseMatrix* getJacobiLU() { return this->jacobiLuMatrix; } @@ -66,7 +66,7 @@ public: * Ownership stays with this class. * @return A pointer to the Jacobi D^{-1} Matrix */ - mrmc::storage::SquareSparseMatrix* getJacobiDInv() { + storm::storage::SquareSparseMatrix* getJacobiDInv() { return this->jacobiDInvMatrix; } @@ -81,16 +81,16 @@ private: /*! * Pointer to the LU Matrix */ - mrmc::storage::SquareSparseMatrix *jacobiLuMatrix; + storm::storage::SquareSparseMatrix *jacobiLuMatrix; /*! * Pointer to the D^{-1} Matrix */ - mrmc::storage::SquareSparseMatrix *jacobiDInvMatrix; + storm::storage::SquareSparseMatrix *jacobiDInvMatrix; }; } // namespace storage -} // namespace mrmc +} // namespace storm -#endif // MRMC_STORAGE_JACOBIDECOMPOSITION_H_ +#endif // STORM_STORAGE_JACOBIDECOMPOSITION_H_ diff --git a/src/storage/SquareSparseMatrix.h b/src/storage/SquareSparseMatrix.h index 2132ba42c..fc657a7df 100644 --- a/src/storage/SquareSparseMatrix.h +++ b/src/storage/SquareSparseMatrix.h @@ -1,5 +1,5 @@ -#ifndef MRMC_STORAGE_SQUARESPARSEMATRIX_H_ -#define MRMC_STORAGE_SQUARESPARSEMATRIX_H_ +#ifndef STORM_STORAGE_SQUARESPARSEMATRIX_H_ +#define STORM_STORAGE_SQUARESPARSEMATRIX_H_ #include #include @@ -24,9 +24,9 @@ extern log4cplus::Logger logger; // Forward declaration for adapter classes. -namespace mrmc { namespace adapters{ class GmmxxAdapter; } } +namespace storm { namespace adapters{ class GmmxxAdapter; } } -namespace mrmc { +namespace storm { namespace storage { @@ -42,7 +42,7 @@ public: /*! * Declare adapter classes as friends to use internal data. */ - friend class mrmc::adapters::GmmxxAdapter; + friend class storm::adapters::GmmxxAdapter; /*! * If we only want to iterate over the columns of the non-zero entries of @@ -90,7 +90,7 @@ public: // Check whether copying the matrix is safe. if (ssm.hasError()) { LOG4CPLUS_ERROR(logger, "Trying to copy sparse matrix in error state."); - throw mrmc::exceptions::InvalidArgumentException("Trying to copy sparse matrix in error state."); + throw storm::exceptions::InvalidArgumentException("Trying to copy sparse matrix in error state."); } else { // Try to prepare the internal storage and throw an error in case // of a failure. @@ -154,15 +154,15 @@ public: if (internalStatus != MatrixStatus::UnInitialized) { triggerErrorState(); LOG4CPLUS_ERROR(logger, "Trying to initialize matrix that is not uninitialized."); - throw mrmc::exceptions::InvalidStateException("Trying to initialize matrix that is not uninitialized."); + throw storm::exceptions::InvalidStateException("Trying to initialize matrix that is not uninitialized."); } else if (rowCount == 0) { triggerErrorState(); LOG4CPLUS_ERROR(logger, "Trying to create initialize a matrix with 0 rows."); - throw mrmc::exceptions::InvalidArgumentException("Trying to create initialize a matrix with 0 rows."); + throw storm::exceptions::InvalidArgumentException("Trying to create initialize a matrix with 0 rows."); } else if (((rowCount * rowCount) - rowCount) < nonZeroEntries) { triggerErrorState(); LOG4CPLUS_ERROR(logger, "Trying to initialize a matrix with more non-zero entries than there can be."); - throw mrmc::exceptions::InvalidArgumentException("Trying to initialize a matrix with more non-zero entries than there can be."); + throw storm::exceptions::InvalidArgumentException("Trying to initialize a matrix with more non-zero entries than there can be."); } else { // If it is safe, initialize necessary members and prepare the // internal storage. @@ -193,7 +193,7 @@ public: if (!eigenSparseMatrix.isCompressed()) { triggerErrorState(); LOG4CPLUS_ERROR(logger, "Trying to initialize from an Eigen matrix that is not in compressed form."); - throw mrmc::exceptions::InvalidArgumentException("Trying to initialize from an Eigen matrix that is not in compressed form."); + throw storm::exceptions::InvalidArgumentException("Trying to initialize from an Eigen matrix that is not in compressed form."); } // Compute the actual (i.e. non-diagonal) number of non-zero entries. @@ -286,7 +286,7 @@ public: if ((row > rowCount) || (col > rowCount)) { triggerErrorState(); LOG4CPLUS_ERROR(logger, "Trying to add a value at illegal position (" << row << ", " << col << ")."); - throw mrmc::exceptions::OutOfRangeException("Trying to add a value at illegal position."); + throw storm::exceptions::OutOfRangeException("Trying to add a value at illegal position."); } if (row == col) { // Set a diagonal element. @@ -319,11 +319,11 @@ public: if (!isInitialized()) { triggerErrorState(); LOG4CPLUS_ERROR(logger, "Trying to finalize an uninitialized matrix."); - throw mrmc::exceptions::InvalidStateException("Trying to finalize an uninitialized matrix."); + throw storm::exceptions::InvalidStateException("Trying to finalize an uninitialized matrix."); } else if (currentSize != nonZeroEntryCount) { triggerErrorState(); LOG4CPLUS_ERROR(logger, "Trying to finalize a matrix that was initialized with more non-zero entries than given."); - throw mrmc::exceptions::InvalidStateException("Trying to finalize a matrix that was initialized with more non-zero entries than given."); + throw storm::exceptions::InvalidStateException("Trying to finalize a matrix that was initialized with more non-zero entries than given."); } else { // Fill in the missing entries in the row_indications array. // (Can happen because of empty rows at the end.) @@ -357,7 +357,7 @@ public: // Check for illegal access indices. if ((row > rowCount) || (col > rowCount)) { LOG4CPLUS_ERROR(logger, "Trying to read a value from illegal position (" << row << ", " << col << ")."); - throw mrmc::exceptions::OutOfRangeException("Trying to read a value from illegal position."); + throw storm::exceptions::OutOfRangeException("Trying to read a value from illegal position."); return false; } @@ -407,7 +407,7 @@ public: // Check for illegal access indices. if ((row > rowCount) || (col > rowCount)) { LOG4CPLUS_ERROR(logger, "Trying to read a value from illegal position (" << row << ", " << col << ")."); - throw mrmc::exceptions::OutOfRangeException("Trying to read a value from illegal position."); + throw storm::exceptions::OutOfRangeException("Trying to read a value from illegal position."); } // Read elements on the diagonal directly. @@ -434,7 +434,7 @@ public: ++rowStart; } - throw mrmc::exceptions::InvalidArgumentException("Trying to get a reference to a non-existant value."); + throw storm::exceptions::InvalidArgumentException("Trying to get a reference to a non-existant value."); } /*! @@ -526,7 +526,7 @@ public: if (!isReadReady()) { triggerErrorState(); LOG4CPLUS_ERROR(logger, "Trying to convert a matrix that is not in a readable state to an Eigen matrix."); - throw mrmc::exceptions::InvalidStateException("Trying to convert a matrix that is not in a readable state to an Eigen matrix."); + throw storm::exceptions::InvalidStateException("Trying to convert a matrix that is not in a readable state to an Eigen matrix."); } else { // Create the resulting matrix. int_fast32_t eigenRows = static_cast(rowCount); @@ -545,8 +545,8 @@ public: // than an average row, the other solution might be faster. // The desired conversion method may be set by an appropriate define. -#define MRMC_USE_TRIPLETCONVERT -# ifdef MRMC_USE_TRIPLETCONVERT +#define STORM_USE_TRIPLETCONVERT +# ifdef STORM_USE_TRIPLETCONVERT // FIXME: Wouldn't it be more efficient to add the elements in // order including the diagonal elements? Otherwise, Eigen has to @@ -581,7 +581,7 @@ public: // Let Eigen create a matrix from the given list of triplets. mat->setFromTriplets(tripletList.begin(), tripletList.end()); -# else // NOT MRMC_USE_TRIPLETCONVERT +# else // NOT STORM_USE_TRIPLETCONVERT // Reserve the average number of non-zero elements per row for each // row. @@ -607,7 +607,7 @@ public: ++rowStart; } } -# endif // MRMC_USE_TRIPLETCONVERT +# endif // STORM_USE_TRIPLETCONVERT // Make the matrix compressed, i.e. remove remaining zero-entries. mat->makeCompressed(); @@ -646,7 +646,7 @@ public: * @param rows A bit vector indicating which rows to make absorbing. * @return True iff the operation was successful. */ - bool makeRowsAbsorbing(const mrmc::storage::BitVector rows) { + bool makeRowsAbsorbing(const storm::storage::BitVector rows) { bool result = true; for (auto row : rows) { result &= makeRowAbsorbing(row); @@ -666,7 +666,7 @@ public: // Check whether the accessed state exists. if (row > rowCount) { LOG4CPLUS_ERROR(logger, "Trying to make an illegal row " << row << " absorbing."); - throw mrmc::exceptions::OutOfRangeException("Trying to make an illegal row absorbing."); + throw storm::exceptions::OutOfRangeException("Trying to make an illegal row absorbing."); return false; } @@ -676,12 +676,12 @@ public: uint_fast64_t rowEnd = rowIndications[row + 1]; while (rowStart < rowEnd) { - valueStorage[rowStart] = mrmc::utility::constGetZero(); + valueStorage[rowStart] = storm::utility::constGetZero(); ++rowStart; } // Set the element on the diagonal to one. - diagonalStorage[row] = mrmc::utility::constGetOne(); + diagonalStorage[row] = storm::utility::constGetOne(); return true; } @@ -693,7 +693,7 @@ public: * @return The sum of the elements in the given row whose column bits * are set to one on the given constraint. */ - T getConstrainedRowSum(const uint_fast64_t row, const mrmc::storage::BitVector& constraint) const { + T getConstrainedRowSum(const uint_fast64_t row, const storm::storage::BitVector& constraint) const { T result(0); for (uint_fast64_t i = rowIndications[row]; i < rowIndications[row + 1]; ++i) { if (constraint.get(columnIndications[i])) { @@ -711,7 +711,7 @@ public: * @param resultVector A pointer to the resulting vector that has at least * as many elements as there are bits set to true in the constraint. */ - void getConstrainedRowCountVector(const mrmc::storage::BitVector& rowConstraint, const mrmc::storage::BitVector& columnConstraint, std::vector* resultVector) const { + void getConstrainedRowCountVector(const storm::storage::BitVector& rowConstraint, const storm::storage::BitVector& columnConstraint, std::vector* resultVector) const { uint_fast64_t currentRowCount = 0; for (auto row : rowConstraint) { (*resultVector)[currentRowCount++] = getConstrainedRowSum(row, columnConstraint); @@ -724,13 +724,13 @@ public: * @param constraint A bit vector indicating which rows and columns to drop. * @return A pointer to a sparse matrix that is a sub-matrix of the current one. */ - SquareSparseMatrix* getSubmatrix(mrmc::storage::BitVector& constraint) const { + SquareSparseMatrix* getSubmatrix(storm::storage::BitVector& constraint) const { LOG4CPLUS_DEBUG(logger, "Creating a sub-matrix with " << constraint.getNumberOfSetBits() << " rows."); // Check for valid constraint. if (constraint.getNumberOfSetBits() == 0) { LOG4CPLUS_ERROR(logger, "Trying to create a sub-matrix of size 0."); - throw mrmc::exceptions::InvalidArgumentException("Trying to create a sub-matrix of size 0."); + throw storm::exceptions::InvalidArgumentException("Trying to create a sub-matrix of size 0."); } // First, we need to determine the number of non-zero entries of the @@ -812,7 +812,7 @@ public: * Calculates the Jacobi-Decomposition of this sparse matrix. * @return A pointer to a class containing the matrix L+U and the inverted diagonal matrix D^-1 */ - mrmc::storage::JacobiDecomposition* getJacobiDecomposition() const { + storm::storage::JacobiDecomposition* getJacobiDecomposition() const { uint_fast64_t rowCount = this->getRowCount(); SquareSparseMatrix *resultLU = new SquareSparseMatrix(this); SquareSparseMatrix *resultDinv = new SquareSparseMatrix(rowCount); @@ -821,10 +821,10 @@ public: // copy diagonal entries to other matrix for (int i = 0; i < rowCount; ++i) { resultDinv->addNextValue(i, i, resultLU->getValue(i, i)); - resultLU->getValue(i, i) = mrmc::utility::constGetZero(); + resultLU->getValue(i, i) = storm::utility::constGetZero(); } - return new mrmc::storage::JacobiDecomposition(resultLU, resultDinv); + return new storm::storage::JacobiDecomposition(resultLU, resultDinv); } /*! @@ -1077,6 +1077,6 @@ private: } // namespace storage -} // namespace mrmc +} // namespace storm -#endif // MRMC_STORAGE_SQUARESPARSEMATRIX_H_ +#endif // STORM_STORAGE_SQUARESPARSEMATRIX_H_ diff --git a/src/mrmc.cpp b/src/storm.cpp similarity index 70% rename from src/mrmc.cpp rename to src/storm.cpp index 16f4cf9f4..f692179c0 100644 --- a/src/mrmc.cpp +++ b/src/storm.cpp @@ -1,7 +1,7 @@ /* - * MRMC - C++ Rebuild + * STORM - a C++ Rebuild of MRMC * - * MRMC is a model checker for discrete-time and continuous-time Markov + * STORM (Stochastic Reward Model Checker) is a model checker for discrete-time and continuous-time Markov * reward models. It supports reward extensions of PCTL and CSL (PRCTL * and CSRL), and allows for the automated verification of properties * concerning long-run and instantaneous rewards as well as cumulative @@ -18,7 +18,7 @@ #include #include -#include "mrmc-config.h" +#include "storm-config.h" #include "src/models/Dtmc.h" #include "src/storage/SquareSparseMatrix.h" #include "src/models/AtomicPropositionsLabeling.h" @@ -55,7 +55,7 @@ void initializeLogger() { * Sets up the logging to file. */ void setUpFileLogging() { - mrmc::settings::Settings* s = mrmc::settings::instance(); + storm::settings::Settings* s = storm::settings::instance(); log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender(s->getString("logfile"))); fileLogAppender->setName("mainFileAppender"); fileLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %F:%L: %m%n"))); @@ -66,11 +66,11 @@ void setUpFileLogging() { * Prints the header. */ void printHeader(const int argc, const char* argv[]) { - std::cout << "MRMC" << std::endl; + std::cout << "STORM" << std::endl; std::cout << "====" << std::endl << std::endl; std::cout << "Version: 1.0" << std::endl; - // "Compute" the command line argument string with which MRMC was invoked. + // "Compute" the command line argument string with which STORM was invoked. std::stringstream commandStream; for (int i = 0; i < argc; ++i) { commandStream << argv[i] << " "; @@ -92,24 +92,24 @@ void printFooter() { * @return True iff the program should continue to run after parsing the options. */ bool parseOptions(const int argc, const char* argv[]) { - mrmc::settings::Settings* s = nullptr; + storm::settings::Settings* s = nullptr; try { - mrmc::settings::Settings::registerModule>(); - s = mrmc::settings::newInstance(argc, argv, nullptr); - } catch (mrmc::exceptions::InvalidSettingsException& e) { + storm::settings::Settings::registerModule>(); + s = storm::settings::newInstance(argc, argv, nullptr); + } catch (storm::exceptions::InvalidSettingsException& e) { std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl; - std::cout << std::endl << mrmc::settings::help; + std::cout << std::endl << storm::settings::help; delete s; return false; } if (s->isSet("help")) { - std::cout << mrmc::settings::help; + std::cout << storm::settings::help; delete s; return false; } if (s->isSet("test-prctl")) { - mrmc::parser::PrctlParser parser(s->getString("test-prctl").c_str()); + storm::parser::PrctlParser parser(s->getString("test-prctl").c_str()); delete s; return false; } @@ -133,8 +133,8 @@ bool parseOptions(const int argc, const char* argv[]) { * Function to perform some cleanup. */ void cleanUp() { - if (mrmc::settings::instance() != nullptr) { - delete mrmc::settings::instance(); + if (storm::settings::instance() != nullptr) { + delete storm::settings::instance(); } } @@ -142,17 +142,17 @@ void cleanUp() { * Simple testing procedure. */ void testChecking() { - mrmc::settings::Settings* s = mrmc::settings::instance(); - mrmc::parser::DtmcParser dtmcParser(s->getString("trafile"), s->getString("labfile")); - std::shared_ptr> dtmc = dtmcParser.getDtmc(); + storm::settings::Settings* s = storm::settings::instance(); + storm::parser::DtmcParser dtmcParser(s->getString("trafile"), s->getString("labfile")); + std::shared_ptr> dtmc = dtmcParser.getDtmc(); dtmc->printModelInformationToStream(std::cout); - mrmc::formula::Ap* trueFormula = new mrmc::formula::Ap("true"); - mrmc::formula::Ap* observe0Greater1Formula = new mrmc::formula::Ap("observe0Greater1"); - mrmc::formula::Until* untilFormula = new mrmc::formula::Until(trueFormula, observe0Greater1Formula); - mrmc::formula::ProbabilisticNoBoundsOperator* probFormula = new mrmc::formula::ProbabilisticNoBoundsOperator(untilFormula); - mrmc::modelChecker::GmmxxDtmcPrctlModelChecker* mc = new mrmc::modelChecker::GmmxxDtmcPrctlModelChecker(*dtmc); + storm::formula::Ap* trueFormula = new storm::formula::Ap("true"); + storm::formula::Ap* observe0Greater1Formula = new storm::formula::Ap("observe0Greater1"); + storm::formula::Until* untilFormula = new storm::formula::Until(trueFormula, observe0Greater1Formula); + storm::formula::ProbabilisticNoBoundsOperator* probFormula = new storm::formula::ProbabilisticNoBoundsOperator(untilFormula); + storm::modelChecker::GmmxxDtmcPrctlModelChecker* mc = new storm::modelChecker::GmmxxDtmcPrctlModelChecker(*dtmc); mc->check(*probFormula); delete mc; diff --git a/src/utility/ConstTemplates.h b/src/utility/ConstTemplates.h index 2547764df..23fe315ad 100644 --- a/src/utility/ConstTemplates.h +++ b/src/utility/ConstTemplates.h @@ -5,10 +5,10 @@ * Author: Thomas Heinemann */ -#ifndef MRMC_UTILITY_CONSTTEMPLATES_H_ -#define MRMC_UTILITY_CONSTTEMPLATES_H_ +#ifndef STORM_UTILITY_CONSTTEMPLATES_H_ +#define STORM_UTILITY_CONSTTEMPLATES_H_ -namespace mrmc { +namespace storm { namespace utility { @@ -112,7 +112,7 @@ inline double constGetOne() { } //namespace utility -} //namespace mrmc +} //namespace storm -#endif /* MRMC_UTILITY_CONSTTEMPLATES_H_ */ +#endif /* STORM_UTILITY_CONSTTEMPLATES_H_ */ diff --git a/src/utility/IoUtility.cpp b/src/utility/IoUtility.cpp index 3dc4d49af..e3fc7dbaf 100644 --- a/src/utility/IoUtility.cpp +++ b/src/utility/IoUtility.cpp @@ -11,12 +11,12 @@ #include -namespace mrmc { +namespace storm { namespace utility { -void dtmcToDot(mrmc::models::Dtmc const &dtmc, std::string filename) { - std::shared_ptr> matrix(dtmc.getTransitionProbabilityMatrix()); +void dtmcToDot(storm::models::Dtmc const &dtmc, std::string filename) { + std::shared_ptr> matrix(dtmc.getTransitionProbabilityMatrix()); double* diagonal_storage = matrix->getDiagonalStoragePointer(); std::ofstream file; @@ -60,13 +60,13 @@ void dtmcToDot(mrmc::models::Dtmc const &dtmc, std::string filename) { } //TODO: Should this stay here or be integrated in the new parser structure? -/*mrmc::models::Dtmc* parseDTMC(std::string const &tra_file, std::string const &lab_file) { - mrmc::parser::DeterministicSparseTransitionParser tp(tra_file); +/*storm::models::Dtmc* parseDTMC(std::string const &tra_file, std::string const &lab_file) { + storm::parser::DeterministicSparseTransitionParser tp(tra_file); uint_fast64_t node_count = tp.getMatrix()->getRowCount(); - mrmc::parser::AtomicPropositionLabelingParser lp(node_count, lab_file); + storm::parser::AtomicPropositionLabelingParser lp(node_count, lab_file); - mrmc::models::Dtmc* result = new mrmc::models::Dtmc(tp.getMatrix(), lp.getLabeling()); + storm::models::Dtmc* result = new storm::models::Dtmc(tp.getMatrix(), lp.getLabeling()); return result; }*/ diff --git a/src/utility/IoUtility.h b/src/utility/IoUtility.h index 112ca85cd..1f6d5b602 100644 --- a/src/utility/IoUtility.h +++ b/src/utility/IoUtility.h @@ -5,12 +5,12 @@ * Author: Thomas Heinemann */ -#ifndef MRMC_UTILITY_IOUTILITY_H_ -#define MRMC_UTILITY_IOUTILITY_H_ +#ifndef STORM_UTILITY_IOUTILITY_H_ +#define STORM_UTILITY_IOUTILITY_H_ #include "src/models/Dtmc.h" -namespace mrmc { +namespace storm { namespace utility { @@ -25,7 +25,7 @@ namespace utility { it will be overwritten. */ -void dtmcToDot(mrmc::models::Dtmc const &dtmc, std::string filename); +void dtmcToDot(storm::models::Dtmc const &dtmc, std::string filename); /*! Parses a transition file and a labeling file and produces a DTMC out of them. @@ -36,10 +36,10 @@ void dtmcToDot(mrmc::models::Dtmc const &dtmc, std::string filename); @returns The DTMC described by the two files. */ -//mrmc::models::Dtmc* parseDTMC(std::string const &tra_file, std::string const &lab_file); +//storm::models::Dtmc* parseDTMC(std::string const &tra_file, std::string const &lab_file); } //namespace utility -} //namespace mrmc +} //namespace storm -#endif /* MRMC_UTILITY_IOUTILITY_H_ */ +#endif /* STORM_UTILITY_IOUTILITY_H_ */ diff --git a/src/utility/OsDetection.h b/src/utility/OsDetection.h index 6409b80da..bc459d40c 100644 --- a/src/utility/OsDetection.h +++ b/src/utility/OsDetection.h @@ -1,5 +1,5 @@ -#ifndef MRMC_UTILITY_OSDETECTION_H_ -#define MRMC_UTILITY_OSDETECTION_H_ +#ifndef STORM_UTILITY_OSDETECTION_H_ +#define STORM_UTILITY_OSDETECTION_H_ #if defined __linux__ || defined __linux # define LINUX @@ -19,4 +19,4 @@ # error Could not detect Operating System #endif -#endif // MRMC_UTILITY_OSDETECTION_H_ +#endif // STORM_UTILITY_OSDETECTION_H_ diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp index 0e2978a28..0c89d08d8 100644 --- a/src/utility/Settings.cpp +++ b/src/utility/Settings.cpp @@ -15,7 +15,7 @@ extern log4cplus::Logger logger; #include -namespace mrmc { +namespace storm { namespace settings { namespace bpo = boost::program_options; @@ -23,11 +23,11 @@ namespace bpo = boost::program_options; /* * static initializers */ -std::unique_ptr mrmc::settings::Settings::desc = nullptr; -std::string mrmc::settings::Settings::binaryName = ""; -mrmc::settings::Settings* mrmc::settings::Settings::inst = nullptr; +std::unique_ptr storm::settings::Settings::desc = nullptr; +std::string storm::settings::Settings::binaryName = ""; +storm::settings::Settings* storm::settings::Settings::inst = nullptr; -std::map< std::pair, std::shared_ptr > mrmc::settings::Settings::modules; +std::map< std::pair, std::shared_ptr > storm::settings::Settings::modules; /*! * The constructor fills the option descriptions, parses the @@ -102,16 +102,16 @@ Settings::Settings(const int argc, const char* argv[], const char* filename) { LOG4CPLUS_ERROR(logger, "Could not read config file"); } catch (bpo::required_option e) { - throw mrmc::exceptions::InvalidSettingsException() << "Required option missing"; + throw storm::exceptions::InvalidSettingsException() << "Required option missing"; } catch (bpo::validation_error e) { - throw mrmc::exceptions::InvalidSettingsException() << "Validation failed: " << e.what(); + throw storm::exceptions::InvalidSettingsException() << "Validation failed: " << e.what(); } catch (bpo::invalid_command_line_syntax e) { - throw mrmc::exceptions::InvalidSettingsException() << e.what(); + throw storm::exceptions::InvalidSettingsException() << e.what(); } catch (bpo::error e) { - throw mrmc::exceptions::InvalidSettingsException() << e.what(); + throw storm::exceptions::InvalidSettingsException() << e.what(); } } @@ -180,11 +180,11 @@ void Settings::secondRun(const int argc, const char* argv[], const char* filenam * options and the list of available command line options. * * Use it like this: - * @code std::cout << mrmc::settings::help; @endcode + * @code std::cout << storm::settings::help; @endcode */ std::ostream& help(std::ostream& os) { - os << "Usage: " << mrmc::settings::Settings::binaryName << " [options]