From f983317b54bce91e8472bc9ab6652d73564eeda9 Mon Sep 17 00:00:00 2001 From: PBerger Date: Tue, 25 Dec 2012 02:37:56 +0100 Subject: [PATCH] Renaming MRMC to STORM, see #42 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Markt und Straßen stehn verlassen, still erleuchtet jedes Haus, Sinnend' geh ich durch die Gassen, alles sieht so festlich aus. An den Fenstern haben Frauen buntes Spielzeug fromm geschmückt, Tausend Kindlein stehn und schauen, sind so wunderstill beglückt. Und ich wandre aus den Mauern Bis hinaus ins freie Feld, Hehres Glänzen, heil'ges Schauern! Wie so weit und still die Welt! Sterne hoch die Kreise schlingen, Aus des Schnees Einsamkeit Steigt's wie wunderbares Singen- O du gnadenreiche Zeit! Merry Christmas commit ;) --- CMakeLists.txt | 84 ++++++++--------- doc/Doxyfile.in | 2 +- mrmc-config.h.in | 4 - resources/BUILD.txt | 2 +- resources/GUIDELINES.txt | 2 +- src/adapters/GmmxxAdapter.h | 6 +- src/exceptions/BaseException.h | 12 +-- src/exceptions/FileIoException.h | 10 +- src/exceptions/InvalidArgumentException.h | 12 +-- src/exceptions/InvalidSettingsException.h | 12 +-- src/exceptions/InvalidStateException.h | 12 +-- src/exceptions/NoConvergenceException.h | 12 +-- src/exceptions/OutOfRangeException.h | 12 +-- src/exceptions/WrongFileFormatException.h | 12 +-- src/formula/And.h | 12 +-- src/formula/Ap.h | 12 +-- src/formula/BoundedUntil.h | 12 +-- src/formula/Formulas.h | 6 +- src/formula/Next.h | 12 +-- src/formula/Not.h | 12 +-- src/formula/Or.h | 12 +-- src/formula/PctlFormula.h | 10 +- src/formula/PctlPathFormula.h | 12 +-- src/formula/PctlStateFormula.h | 12 +-- src/formula/ProbabilisticIntervalOperator.h | 16 ++-- src/formula/ProbabilisticNoBoundsOperator.h | 12 +-- src/formula/ProbabilisticOperator.h | 16 ++-- src/formula/Until.h | 12 +-- src/modelChecker/DtmcPrctlModelChecker.h | 78 +++++++-------- src/modelChecker/EigenDtmcPrctlModelChecker.h | 52 +++++----- src/modelChecker/GmmxxDtmcPrctlModelChecker.h | 58 ++++++------ src/models/AtomicPropositionsLabeling.h | 32 +++---- src/models/Ctmc.h | 36 +++---- src/models/Dtmc.h | 36 +++---- src/models/GraphTransitions.h | 16 ++-- .../AtomicPropositionLabelingParser.cpp | 10 +- src/parser/AtomicPropositionLabelingParser.h | 14 +-- src/parser/AutoTransitionParser.cpp | 6 +- src/parser/AutoTransitionParser.h | 10 +- .../DeterministicSparseTransitionParser.cpp | 8 +- .../DeterministicSparseTransitionParser.h | 14 +-- src/parser/DtmcParser.cpp | 16 ++-- src/parser/DtmcParser.h | 10 +- ...NonDeterministicSparseTransitionParser.cpp | 8 +- .../NonDeterministicSparseTransitionParser.h | 14 +-- src/parser/Parser.cpp | 26 ++--- src/parser/Parser.h | 10 +- src/parser/PrctlParser.cpp | 8 +- src/parser/PrctlParser.h | 14 +-- src/parser/SparseStateRewardParser.cpp | 6 +- src/parser/SparseStateRewardParser.h | 10 +- src/reward/RewardModel.h | 10 +- src/solver/GraphAnalyzer.h | 26 ++--- src/storage/BitVector.h | 16 ++-- src/storage/JacobiDecomposition.h | 24 ++--- src/storage/SquareSparseMatrix.h | 68 +++++++------- src/{mrmc.cpp => storm.cpp} | 46 ++++----- src/utility/ConstTemplates.h | 10 +- src/utility/IoUtility.cpp | 14 +-- src/utility/IoUtility.h | 14 +-- src/utility/OsDetection.h | 6 +- src/utility/Settings.cpp | 26 ++--- src/utility/Settings.h | 18 ++-- src/utility/Vector.h | 16 ++-- storm-config.h.in | 4 + test/mrmc-tests.cpp | 4 +- test/parser/ParseDtmcTest.cpp | 12 +-- test/parser/ReadLabFileTest.cpp | 16 ++-- test/parser/ReadTraFileTest.cpp | 18 ++-- test/reward/RewardModelTest.cpp | 2 +- test/storage/BitVectorTest.cpp | 36 +++---- test/storage/SquareSparseMatrixTest.cpp | 94 +++++++++---------- 72 files changed, 667 insertions(+), 667 deletions(-) delete mode 100644 mrmc-config.h.in rename src/{mrmc.cpp => storm.cpp} (70%) create mode 100644 storm-config.h.in 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]