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

Renaming MRMC to STORM, see #42 

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 ;)
main
PBerger 12 years ago
parent
a9b6e92306
commit
f983317b54
72 changed files with 667 additions and 667 deletions
Split View
  1. 84
      CMakeLists.txt
  2. 2
      doc/Doxyfile.in
  3. 4
      mrmc-config.h.in
  4. 2
      resources/BUILD.txt
  5. 2
      resources/GUIDELINES.txt
  6. 6
      src/adapters/GmmxxAdapter.h
  7. 12
      src/exceptions/BaseException.h
  8. 10
      src/exceptions/FileIoException.h
  9. 12
      src/exceptions/InvalidArgumentException.h
  10. 12
      src/exceptions/InvalidSettingsException.h
  11. 12
      src/exceptions/InvalidStateException.h
  12. 12
      src/exceptions/NoConvergenceException.h
  13. 12
      src/exceptions/OutOfRangeException.h
  14. 12
      src/exceptions/WrongFileFormatException.h
  15. 12
      src/formula/And.h
  16. 12
      src/formula/Ap.h
  17. 12
      src/formula/BoundedUntil.h
  18. 6
      src/formula/Formulas.h
  19. 12
      src/formula/Next.h
  20. 12
      src/formula/Not.h
  21. 12
      src/formula/Or.h
  22. 10
      src/formula/PctlFormula.h
  23. 12
      src/formula/PctlPathFormula.h
  24. 12
      src/formula/PctlStateFormula.h
  25. 16
      src/formula/ProbabilisticIntervalOperator.h
  26. 12
      src/formula/ProbabilisticNoBoundsOperator.h
  27. 16
      src/formula/ProbabilisticOperator.h
  28. 12
      src/formula/Until.h
  29. 78
      src/modelChecker/DtmcPrctlModelChecker.h
  30. 52
      src/modelChecker/EigenDtmcPrctlModelChecker.h
  31. 58
      src/modelChecker/GmmxxDtmcPrctlModelChecker.h
  32. 32
      src/models/AtomicPropositionsLabeling.h
  33. 36
      src/models/Ctmc.h
  34. 36
      src/models/Dtmc.h
  35. 16
      src/models/GraphTransitions.h
  36. 10
      src/parser/AtomicPropositionLabelingParser.cpp
  37. 14
      src/parser/AtomicPropositionLabelingParser.h
  38. 6
      src/parser/AutoTransitionParser.cpp
  39. 10
      src/parser/AutoTransitionParser.h
  40. 8
      src/parser/DeterministicSparseTransitionParser.cpp
  41. 14
      src/parser/DeterministicSparseTransitionParser.h
  42. 16
      src/parser/DtmcParser.cpp
  43. 10
      src/parser/DtmcParser.h
  44. 8
      src/parser/NonDeterministicSparseTransitionParser.cpp
  45. 14
      src/parser/NonDeterministicSparseTransitionParser.h
  46. 26
      src/parser/Parser.cpp
  47. 10
      src/parser/Parser.h
  48. 8
      src/parser/PrctlParser.cpp
  49. 14
      src/parser/PrctlParser.h
  50. 6
      src/parser/SparseStateRewardParser.cpp
  51. 10
      src/parser/SparseStateRewardParser.h
  52. 10
      src/reward/RewardModel.h
  53. 26
      src/solver/GraphAnalyzer.h
  54. 16
      src/storage/BitVector.h
  55. 24
      src/storage/JacobiDecomposition.h
  56. 68
      src/storage/SquareSparseMatrix.h
  57. 46
      src/storm.cpp
  58. 10
      src/utility/ConstTemplates.h
  59. 14
      src/utility/IoUtility.cpp
  60. 14
      src/utility/IoUtility.h
  61. 6
      src/utility/OsDetection.h
  62. 26
      src/utility/Settings.cpp
  63. 18
      src/utility/Settings.h
  64. 16
      src/utility/Vector.h
  65. 4
      storm-config.h.in
  66. 4
      test/mrmc-tests.cpp
  67. 12
      test/parser/ParseDtmcTest.cpp
  68. 16
      test/parser/ReadLabFileTest.cpp
  69. 18
      test/parser/ReadTraFileTest.cpp
  70. 2
      test/reward/RewardModelTest.cpp
  71. 36
      test/storage/BitVectorTest.cpp
  72. 94
      test/storage/SquareSparseMatrixTest.cpp

84
CMakeLists.txt
View File

@ -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)

2
doc/Doxyfile.in
View File

@ -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

4
mrmc-config.h.in
View File

@ -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@"

2
resources/BUILD.txt
View File

@ -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.
Now you can build STORM using the generated project/makefiles in the Build folder you selected.

2
resources/GUIDELINES.txt
View File

@ -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

6
src/adapters/GmmxxAdapter.h
View File

@ -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<class T>
static gmm::csr_matrix<T>* toGmmxxSparseMatrix(mrmc::storage::SquareSparseMatrix<T> const& matrix) {
static gmm::csr_matrix<T>* toGmmxxSparseMatrix(storm::storage::SquareSparseMatrix<T> 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_ */

12
src/exceptions/BaseException.h
View File

@ -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 <exception>
#include <sstream>
namespace mrmc {
namespace storm {
namespace exceptions {
template<typename E>
@ -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<exception_name> { \
#define STORM_EXCEPTION_DEFINE_NEW(exception_name) class exception_name : public BaseException<exception_name> { \
public: \
exception_name() : BaseException() { \
} \
@ -56,4 +56,4 @@ public: \
};
#endif // MRMC_EXCEPTIONS_BASEEXCEPTION_H_
#endif // STORM_EXCEPTIONS_BASEEXCEPTION_H_

10
src/exceptions/FileIoException.h
View File

@ -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_ */

12
src/exceptions/InvalidArgumentException.h
View File

@ -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_

12
src/exceptions/InvalidSettingsException.h
View File

@ -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_

12
src/exceptions/InvalidStateException.h
View File

@ -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_

12
src/exceptions/NoConvergenceException.h
View File

@ -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_

12
src/exceptions/OutOfRangeException.h
View File

@ -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_

12
src/exceptions/WrongFileFormatException.h
View File

@ -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_ */

12
src/formula/And.h
View File

@ -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 <string>
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<T>& modelChecker) const {
virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& 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_ */

12
src/formula/Ap.h
View File

@ -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<T>& modelChecker) const {
virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& 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_ */

12
src/formula/BoundedUntil.h
View File

@ -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 <string>
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<T> *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& 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_ */

6
src/formula/Formulas.h
View File

@ -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_ */

12
src/formula/Next.h
View File

@ -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<T> *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& 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_ */

12
src/formula/Not.h
View File

@ -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<T>& modelChecker) const {
virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& 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_ */

12
src/formula/Or.h
View File

@ -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<T>& modelChecker) const {
virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& 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_ */

10
src/formula/PctlFormula.h
View File

@ -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 <string>
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_ */

12
src/formula/PctlPathFormula.h
View File

@ -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 <vector>
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<T>* check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const = 0;
virtual std::vector<T>* check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const = 0;
};
} //namespace formula
} //namespace mrmc
} //namespace storm
#endif /* MRMC_FORMULA_PCTLPATHFORMULA_H_ */
#endif /* STORM_FORMULA_PCTLPATHFORMULA_H_ */

12
src/formula/PctlStateFormula.h
View File

@ -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<T>& modelChecker) const = 0;
virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const = 0;
};
} //namespace formula
} //namespace mrmc
} //namespace storm
#endif /* MRMC_FORMULA_PCTLSTATEFORMULA_H_ */
#endif /* STORM_FORMULA_PCTLSTATEFORMULA_H_ */

16
src/formula/ProbabilisticIntervalOperator.h
View File

@ -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<T>();
lower = mrmc::utility::constGetZero<T>();
upper = storm::utility::constGetZero<T>();
lower = storm::utility::constGetZero<T>();
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<T>& modelChecker) const {
virtual storm::storage::BitVector *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& 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_ */

12
src/formula/ProbabilisticNoBoundsOperator.h
View File

@ -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 T>
class ProbabilisticNoBoundsOperator: public mrmc::formula::PctlFormula<T> {
class ProbabilisticNoBoundsOperator: public storm::formula::PctlFormula<T> {
public:
/*!
* Empty constructor
@ -103,6 +103,6 @@ private:
};
} /* namespace formula */
} /* namespace mrmc */
} /* namespace storm */
#endif /* MRMC_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_ */
#endif /* STORM_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_ */

16
src/formula/ProbabilisticOperator.h
View File

@ -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 T>
class ProbabilisticOperator : public mrmc::formula::PctlStateFormula<T> {
class ProbabilisticOperator : public storm::formula::PctlStateFormula<T> {
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<T>& modelChecker) const {
virtual storm::storage::BitVector *check(
const storm::modelChecker::DtmcPrctlModelChecker<T>& 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_ */

12
src/formula/Until.h
View File

@ -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<T> *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
virtual std::vector<T> *check(const storm::modelChecker::DtmcPrctlModelChecker<T>& 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_ */

78
src/modelChecker/DtmcPrctlModelChecker.h
View File

@ -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<Type>& model) : model(model) {
explicit DtmcPrctlModelChecker(storm::models::Dtmc<Type>& model) : model(model) {
}
@ -67,8 +67,8 @@ public:
*
* @param modelChecker The model checker that is copied.
*/
explicit DtmcPrctlModelChecker(const mrmc::modelChecker::DtmcPrctlModelChecker<Type>* modelChecker) {
this->model = new mrmc::models::Dtmc<Type>(modelChecker->getModel());
explicit DtmcPrctlModelChecker(const storm::modelChecker::DtmcPrctlModelChecker<Type>* modelChecker) {
this->model = new storm::models::Dtmc<Type>(modelChecker->getModel());
}
/*!
@ -81,7 +81,7 @@ public:
/*!
* @returns A reference to the dtmc of the model checker.
*/
mrmc::models::Dtmc<Type>& getModel() const {
storm::models::Dtmc<Type>& getModel() const {
return this->model;
}
@ -89,7 +89,7 @@ public:
* Sets the DTMC model which is checked
* @param model
*/
void setModel(mrmc::models::Dtmc<Type>& model) {
void setModel(storm::models::Dtmc<Type>& model) {
this->model = &model;
}
@ -98,9 +98,9 @@ public:
* states.
* @param stateFormula The formula to be checked.
*/
void check(const mrmc::formula::PctlStateFormula<Type>& stateFormula) {
void check(const storm::formula::PctlStateFormula<Type>& 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<Type>& probabilisticNoBoundsFormula) {
void check(const storm::formula::ProbabilisticNoBoundsOperator<Type>& probabilisticNoBoundsFormula) {
LOG4CPLUS_INFO(logger, "Model checking formula " << probabilisticNoBoundsFormula.toString());
std::cout << "Model checking formula: " << probabilisticNoBoundsFormula.toString() << std::endl;
std::vector<Type>* 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<Type>& formula) const {
storm::storage::BitVector* checkStateFormula(const storm::formula::PctlStateFormula<Type>& 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<Type>& formula) const {
mrmc::storage::BitVector* result = checkStateFormula(formula.getLeft());
mrmc::storage::BitVector* right = checkStateFormula(formula.getRight());
storm::storage::BitVector* checkAnd(const storm::formula::And<Type>& 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<Type>& formula) const {
storm::storage::BitVector* checkAp(const storm::formula::Ap<Type>& 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<Type>& formula) const {
mrmc::storage::BitVector* result = checkStateFormula(formula.getChild());
storm::storage::BitVector* checkNot(const storm::formula::Not<Type>& 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<Type>& formula) const {
mrmc::storage::BitVector* result = checkStateFormula(formula.getLeft());
mrmc::storage::BitVector* right = checkStateFormula(formula.getRight());
storm::storage::BitVector* checkOr(const storm::formula::Or<Type>& 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<Type>& formula) const {
storm::storage::BitVector* checkProbabilisticOperator(
const storm::formula::ProbabilisticOperator<Type>& formula) const {
std::vector<Type>* 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<Type>& formula) const {
storm::storage::BitVector* checkProbabilisticIntervalOperator(
const storm::formula::ProbabilisticIntervalOperator<Type>& formula) const {
// First, we need to compute the probability for satisfying the path formula for each state.
std::vector<Type>* 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<Type>* checkProbabilisticNoBoundsOperator(
const mrmc::formula::ProbabilisticNoBoundsOperator<Type>& formula) const {
const storm::formula::ProbabilisticNoBoundsOperator<Type>& 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<Type>* checkPathFormula(const mrmc::formula::PctlPathFormula<Type>& formula) const {
std::vector<Type>* checkPathFormula(const storm::formula::PctlPathFormula<Type>& 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<Type>* checkBoundedUntil(const mrmc::formula::BoundedUntil<Type>& formula) const = 0;
virtual std::vector<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& 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<Type>* checkNext(const mrmc::formula::Next<Type>& formula) const = 0;
virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& 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<Type>* checkUntil(const mrmc::formula::Until<Type>& formula) const = 0;
virtual std::vector<Type>* checkUntil(const storm::formula::Until<Type>& formula) const = 0;
private:
mrmc::models::Dtmc<Type>& model;
storm::models::Dtmc<Type>& model;
};
} //namespace modelChecker
} //namespace mrmc
} //namespace storm
#endif /* MRMC_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ */
#endif /* STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ */

52
src/modelChecker/EigenDtmcPrctlModelChecker.h
View File

@ -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 Type>
class EigenDtmcPrctlModelChecker : public DtmcPrctlModelChecker<Type> {
public:
explicit EigenDtmcPrctlModelChecker(mrmc::models::Dtmc<Type>& dtmc) : DtmcPrctlModelChecker<Type>(dtmc) { }
explicit EigenDtmcPrctlModelChecker(storm::models::Dtmc<Type>& dtmc) : DtmcPrctlModelChecker<Type>(dtmc) { }
virtual ~EigenDtmcPrctlModelChecker() { }
virtual std::vector<Type>* checkBoundedUntil(const mrmc::formula::BoundedUntil<Type>& formula) const {
virtual std::vector<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& 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<Type> tmpMatrix(*this->getModel().getTransitionProbabilityMatrix());
storm::storage::SquareSparseMatrix<Type> 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<Type>* result = new std::vector<Type>(stateCount);
mrmc::utility::setVectorValues(result, *rightStates, mrmc::utility::constGetOne<Type>());
storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne<Type>());
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<Type>* checkNext(const mrmc::formula::Next<Type>& formula) const {
virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& 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<Type, 1, int_fast32_t>* eigenMatrix = this->getModel().getTransitionProbabilityMatrix()->toEigenSparseMatrix();
@ -93,7 +93,7 @@ public:
// Create the vector with which to multiply and initialize it correctly.
std::vector<Type> x(this->getModel().getNumberOfStates());
mrmc::utility::setVectorValues(&x, *nextStates, mrmc::utility::constGetOne<Type>());
storm::utility::setVectorValues(&x, *nextStates, storm::utility::constGetOne<Type>());
// Delete not needed next states bit vector.
delete nextStates;
@ -118,16 +118,16 @@ public:
return result;
}
virtual std::vector<Type>* checkUntil(const mrmc::formula::Until<Type>& formula) const {
virtual std::vector<Type>* checkUntil(const storm::formula::Until<Type>& 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<double>(this->getModel(), *leftStates, *rightStates, &notExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates);
storm::storage::BitVector notExistsPhiUntilPsiStates(this->getModel().getNumberOfStates());
storm::storage::BitVector alwaysPhiUntilPsiStates(this->getModel().getNumberOfStates());
storm::solver::GraphAnalyzer::getPhiUntilPsiStates<double>(this->getModel(), *leftStates, *rightStates, &notExistsPhiUntilPsiStates, &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<VectorType> MapType;
// Now we can eliminate the rows and columns from the original transition probability matrix.
mrmc::storage::SquareSparseMatrix<double>* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates);
storm::storage::SquareSparseMatrix<double>* 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<Type>(result, maybeStates, x);
storm::utility::setVectorValues<Type>(result, maybeStates, x);
// Delete temporary matrix.
delete eigenSubMatrix;
}
mrmc::utility::setVectorValues<Type>(result, notExistsPhiUntilPsiStates, mrmc::utility::constGetZero<Type>());
mrmc::utility::setVectorValues<Type>(result, alwaysPhiUntilPsiStates, mrmc::utility::constGetOne<Type>());
storm::utility::setVectorValues<Type>(result, notExistsPhiUntilPsiStates, storm::utility::constGetZero<Type>());
storm::utility::setVectorValues<Type>(result, alwaysPhiUntilPsiStates, storm::utility::constGetOne<Type>());
return result;
}
@ -220,6 +220,6 @@ public:
} //namespace modelChecker
} //namespace mrmc
} //namespace storm
#endif /* MRMC_MODELCHECKER_EIGENDTMCPRCTLMODELCHECKER_H_ */
#endif /* STORM_MODELCHECKER_EIGENDTMCPRCTLMODELCHECKER_H_ */

58
src/modelChecker/GmmxxDtmcPrctlModelChecker.h
View File

@ -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 <cmath>
@ -26,7 +26,7 @@
extern log4cplus::Logger logger;
namespace mrmc {
namespace storm {
namespace modelChecker {
@ -37,27 +37,27 @@ template <class Type>
class GmmxxDtmcPrctlModelChecker : public DtmcPrctlModelChecker<Type> {
public:
explicit GmmxxDtmcPrctlModelChecker(mrmc::models::Dtmc<Type>& dtmc) : DtmcPrctlModelChecker<Type>(dtmc) { }
explicit GmmxxDtmcPrctlModelChecker(storm::models::Dtmc<Type>& dtmc) : DtmcPrctlModelChecker<Type>(dtmc) { }
virtual ~GmmxxDtmcPrctlModelChecker() { }
virtual std::vector<Type>* checkBoundedUntil(const mrmc::formula::BoundedUntil<Type>& formula) const {
virtual std::vector<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& 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<Type> tmpMatrix(*this->getModel().getTransitionProbabilityMatrix());
storm::storage::SquareSparseMatrix<Type> 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<Type>* gmmxxMatrix = mrmc::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(tmpMatrix);
gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(tmpMatrix);
// Create the vector with which to multiply.
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
mrmc::utility::setVectorValues(result, *rightStates, mrmc::utility::constGetOne<Type>());
storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne<Type>());
// Now perform matrix-vector multiplication as long as we meet the bound of the formula.
std::vector<Type>* swap = nullptr;
@ -76,16 +76,16 @@ public:
return result;
}
virtual std::vector<Type>* checkNext(const mrmc::formula::Next<Type>& formula) const {
virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& 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<Type>* gmmxxMatrix = mrmc::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionProbabilityMatrix());
gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionProbabilityMatrix());
// Create the vector with which to multiply and initialize it correctly.
std::vector<Type> x(this->getModel().getNumberOfStates());
mrmc::utility::setVectorValues(&x, *nextStates, mrmc::utility::constGetOne<Type>());
storm::utility::setVectorValues(&x, *nextStates, storm::utility::constGetOne<Type>());
// Delete obsolete sub-result.
delete nextStates;
@ -101,16 +101,16 @@ public:
return result;
}
virtual std::vector<Type>* checkUntil(const mrmc::formula::Until<Type>& formula) const {
virtual std::vector<Type>* checkUntil(const storm::formula::Until<Type>& 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, &notExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates);
storm::storage::BitVector notExistsPhiUntilPsiStates(this->getModel().getNumberOfStates());
storm::storage::BitVector alwaysPhiUntilPsiStates(this->getModel().getNumberOfStates());
storm::solver::GraphAnalyzer::getPhiUntilPsiStates(this->getModel(), *leftStates, *rightStates, &notExistsPhiUntilPsiStates, &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<Type>* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates);
storm::storage::SquareSparseMatrix<Type>* 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<Type>* gmmxxMatrix = mrmc::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*submatrix);
gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*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<Type>(result, maybeStates, x);
storm::utility::setVectorValues<Type>(result, maybeStates, x);
// Delete temporary matrix.
delete gmmxxMatrix;
}
// Set values of resulting vector that are known exactly.
mrmc::utility::setVectorValues<Type>(result, notExistsPhiUntilPsiStates, mrmc::utility::constGetZero<Type>());
mrmc::utility::setVectorValues<Type>(result, alwaysPhiUntilPsiStates, mrmc::utility::constGetOne<Type>());
storm::utility::setVectorValues<Type>(result, notExistsPhiUntilPsiStates, storm::utility::constGetZero<Type>());
storm::utility::setVectorValues<Type>(result, alwaysPhiUntilPsiStates, storm::utility::constGetOne<Type>());
return result;
}
@ -278,6 +278,6 @@ public:
} //namespace modelChecker
} //namespace mrmc
} //namespace storm
#endif /* MRMC_MODELCHECKER_GMMXXDTMCPRCTLMODELCHECKER_H_ */
#endif /* STORM_MODELCHECKER_GMMXXDTMCPRCTLMODELCHECKER_H_ */

32
src/models/AtomicPropositionsLabeling.h
View File

@ -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 <unordered_map>
#include <set>
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<std::string> 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<std::string> 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_ */

36
src/models/Ctmc.h
View File

@ -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 <ostream>
#include <iostream>
@ -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<mrmc::storage::SquareSparseMatrix<T>> rateMatrix,
std::shared_ptr<mrmc::models::AtomicPropositionsLabeling> stateLabeling,
Ctmc(std::shared_ptr<storm::storage::SquareSparseMatrix<T>> rateMatrix,
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
std::shared_ptr<std::vector<T>> stateRewards = nullptr,
std::shared_ptr<mrmc::storage::SquareSparseMatrix<T>> transitionRewardMatrix = nullptr)
std::shared_ptr<storm::storage::SquareSparseMatrix<T>> 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<T>(*ctmc.backwardTransitions);
this->backwardTransitions = new storm::models::GraphTransitions<T>(*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<mrmc::storage::SquareSparseMatrix<T>> getTransitionRateMatrix() const {
std::shared_ptr<storm::storage::SquareSparseMatrix<T>> 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<mrmc::storage::SquareSparseMatrix<T>> getTransitionRewardMatrix() const {
std::shared_ptr<storm::storage::SquareSparseMatrix<T>> 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<T>& getBackwardTransitions() {
storm::models::GraphTransitions<T>& getBackwardTransitions() {
if (this->backwardTransitions == nullptr) {
this->backwardTransitions = new mrmc::models::GraphTransitions<T>(this->probabilityMatrix, false);
this->backwardTransitions = new storm::models::GraphTransitions<T>(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<mrmc::storage::SquareSparseMatrix<T>> rateMatrix;
std::shared_ptr<storm::storage::SquareSparseMatrix<T>> rateMatrix;
/*! The labeling of the states of the CTMC. */
std::shared_ptr<mrmc::models::AtomicPropositionsLabeling> stateLabeling;
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
/*! The state-based rewards of the CTMC. */
std::shared_ptr<std::vector<T>> stateRewards;
/*! The transition-based rewards of the CTMC. */
std::shared_ptr<mrmc::storage::SquareSparseMatrix<T>> transitionRewardMatrix;
std::shared_ptr<storm::storage::SquareSparseMatrix<T>> transitionRewardMatrix;
/*!
* A data structure that stores the predecessors for all states. This is
* needed for backwards directed searches.
*/
mrmc::models::GraphTransitions<T>* backwardTransitions;
storm::models::GraphTransitions<T>* backwardTransitions;
};
} // namespace models
} // namespace mrmc
} // namespace storm
#endif /* MRMC_MODELS_DTMC_H_ */
#endif /* STORM_MODELS_DTMC_H_ */

36
src/models/Dtmc.h
View File

@ -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 <ostream>
#include <iostream>
@ -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<mrmc::storage::SquareSparseMatrix<T>> probabilityMatrix,
std::shared_ptr<mrmc::models::AtomicPropositionsLabeling> stateLabeling,
Dtmc(std::shared_ptr<storm::storage::SquareSparseMatrix<T>> probabilityMatrix,
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
std::shared_ptr<std::vector<T>> stateRewards = nullptr,
std::shared_ptr<mrmc::storage::SquareSparseMatrix<T>> transitionRewardMatrix = nullptr)
std::shared_ptr<storm::storage::SquareSparseMatrix<T>> 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<T>(*dtmc.backwardTransitions);
this->backwardTransitions = new storm::models::GraphTransitions<T>(*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<mrmc::storage::SquareSparseMatrix<T>> getTransitionProbabilityMatrix() const {
std::shared_ptr<storm::storage::SquareSparseMatrix<T>> 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<mrmc::storage::SquareSparseMatrix<T>> getTransitionRewardMatrix() const {
std::shared_ptr<storm::storage::SquareSparseMatrix<T>> 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<T>& getBackwardTransitions() {
storm::models::GraphTransitions<T>& getBackwardTransitions() {
if (this->backwardTransitions == nullptr) {
this->backwardTransitions = new mrmc::models::GraphTransitions<T>(this->probabilityMatrix, false);
this->backwardTransitions = new storm::models::GraphTransitions<T>(this->probabilityMatrix, false);
}
return *this->backwardTransitions;
}
@ -184,26 +184,26 @@ private:
}
/*! A matrix representing the transition probability function of the DTMC. */
std::shared_ptr<mrmc::storage::SquareSparseMatrix<T>> probabilityMatrix;
std::shared_ptr<storm::storage::SquareSparseMatrix<T>> probabilityMatrix;
/*! The labeling of the states of the DTMC. */
std::shared_ptr<mrmc::models::AtomicPropositionsLabeling> stateLabeling;
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
/*! The state-based rewards of the DTMC. */
std::shared_ptr<std::vector<T>> stateRewards;
/*! The transition-based rewards of the DTMC. */
std::shared_ptr<mrmc::storage::SquareSparseMatrix<T>> transitionRewardMatrix;
std::shared_ptr<storm::storage::SquareSparseMatrix<T>> transitionRewardMatrix;
/*!
* A data structure that stores the predecessors for all states. This is
* needed for backwards directed searches.
*/
mrmc::models::GraphTransitions<T>* backwardTransitions;
storm::models::GraphTransitions<T>* backwardTransitions;
};
} // namespace models
} // namespace mrmc
} // namespace storm
#endif /* MRMC_MODELS_DTMC_H_ */
#endif /* STORM_MODELS_DTMC_H_ */

16
src/models/GraphTransitions.h
View File

@ -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 <algorithm>
#include <memory>
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<mrmc::storage::SquareSparseMatrix<T>> transitionMatrix, bool forward)
GraphTransitions(std::shared_ptr<storm::storage::SquareSparseMatrix<T>> 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<mrmc::storage::SquareSparseMatrix<T>> transitionMatrix) {
void initializeForward(std::shared_ptr<storm::storage::SquareSparseMatrix<T>> 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<mrmc::storage::SquareSparseMatrix<T>> transitionMatrix) {
void initializeBackward(std::shared_ptr<storm::storage::SquareSparseMatrix<T>> 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_ */

10
src/parser/AtomicPropositionLabelingParser.cpp
View File

@ -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<mrmc::models::AtomicPropositionsLabeling>(new mrmc::models::AtomicPropositionsLabeling(node_count, proposition_count));
this->labeling = std::shared_ptr<storm::models::AtomicPropositionsLabeling>(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

14
src/parser/AtomicPropositionLabelingParser.h
View File

@ -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 <memory>
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<mrmc::models::AtomicPropositionsLabeling> getLabeling() {
std::shared_ptr<storm::models::AtomicPropositionsLabeling> getLabeling() {
return this->labeling;
}
private:
std::shared_ptr<mrmc::models::AtomicPropositionsLabeling> labeling;
std::shared_ptr<storm::models::AtomicPropositionsLabeling> labeling;
};
} // namespace parser
} // namespace mrmc
} // namespace storm
#endif /* MRMC_PARSER_LABPARSER_H_ */
#endif /* STORM_PARSER_LABPARSER_H_ */

6
src/parser/AutoTransitionParser.cpp
View File

@ -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<TransitionType,TransitionType> AutoTransitionParser::analyzeContent(co
} //namespace parser
} //namespace mrmc
} //namespace storm

10
src/parser/AutoTransitionParser.h
View File

@ -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 <iostream>
#include <utility>
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_ */

8
src/parser/DeterministicSparseTransitionParser.cpp
View File

@ -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<mrmc::storage::SquareSparseMatrix<double>>(new mrmc::storage::SquareSparseMatrix<double>(maxnode + 1));
this->matrix = std::shared_ptr<storm::storage::SquareSparseMatrix<double>>(new storm::storage::SquareSparseMatrix<double>(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

14
src/parser/DeterministicSparseTransitionParser.h
View File

@ -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 <memory>
namespace mrmc {
namespace storm {
namespace parser {
/*!
@ -19,18 +19,18 @@ class DeterministicSparseTransitionParser : public Parser {
public:
DeterministicSparseTransitionParser(std::string const &filename);
std::shared_ptr<mrmc::storage::SquareSparseMatrix<double>> getMatrix() {
std::shared_ptr<storm::storage::SquareSparseMatrix<double>> getMatrix() {
return this->matrix;
}
private:
std::shared_ptr<mrmc::storage::SquareSparseMatrix<double>> matrix;
std::shared_ptr<storm::storage::SquareSparseMatrix<double>> 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_ */

16
src/parser/DtmcParser.cpp
View File

@ -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<std::vector<double>> stateRewards = nullptr;
std::shared_ptr<mrmc::storage::SquareSparseMatrix<double>> transitionRewards = nullptr;
std::shared_ptr<storm::storage::SquareSparseMatrix<double>> 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<mrmc::models::Dtmc<double>>(new mrmc::models::Dtmc<double>(tp.getMatrix(), lp.getLabeling(), stateRewards, transitionRewards));
dtmc = std::shared_ptr<storm::models::Dtmc<double>>(new storm::models::Dtmc<double>(tp.getMatrix(), lp.getLabeling(), stateRewards, transitionRewards));
}
} /* namespace parser */
} /* namespace mrmc */
} /* namespace storm */

10
src/parser/DtmcParser.h
View File

@ -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<mrmc::models::Dtmc<double>> getDtmc() {
std::shared_ptr<storm::models::Dtmc<double>> getDtmc() {
return this->dtmc;
}
private:
std::shared_ptr<mrmc::models::Dtmc<double>> dtmc;
std::shared_ptr<storm::models::Dtmc<double>> dtmc;
};
} /* namespace parser */
} /* namespace mrmc */
} /* namespace storm */
#endif /* DTMCPARSER_H_ */

8
src/parser/NonDeterministicSparseTransitionParser.cpp
View File

@ -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<mrmc::storage::SquareSparseMatrix<double>>(new mrmc::storage::SquareSparseMatrix<double>(maxnode + 1));
this->matrix = std::shared_ptr<storm::storage::SquareSparseMatrix<double>>(new storm::storage::SquareSparseMatrix<double>(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

14
src/parser/NonDeterministicSparseTransitionParser.h
View File

@ -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 <memory>
#include <vector>
namespace mrmc {
namespace storm {
namespace parser {
/*!
@ -20,18 +20,18 @@ class NonDeterministicSparseTransitionParser : public Parser {
public:
NonDeterministicSparseTransitionParser(std::string const &filename);
std::shared_ptr<mrmc::storage::SquareSparseMatrix<double>> getMatrix() {
std::shared_ptr<storm::storage::SquareSparseMatrix<double>> getMatrix() {
return this->matrix;
}
private:
std::shared_ptr<mrmc::storage::SquareSparseMatrix<double>> matrix;
std::shared_ptr<storm::storage::SquareSparseMatrix<double>> matrix;
std::unique_ptr<std::vector<uint_fast64_t>> 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_ */

26
src/parser/Parser.cpp
View File

@ -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<char*>(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);

10
src/parser/Parser.h
View File

@ -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_ */

8
src/parser/PrctlParser.cpp
View File

@ -58,7 +58,7 @@ namespace
/*!
* @brief Resulting formula.
*/
mrmc::formula::PctlFormula<double>* result;
storm::formula::PctlFormula<double>* 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 <filename> foo bar
* Parser can be run via ./storm --test-prctl <filename> 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))

14
src/parser/PrctlParser.h
View File

@ -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<double>* getFormula()
storm::formula::PctlFormula<double>* getFormula()
{
return this->formula;
}
private:
mrmc::formula::PctlFormula<double>* formula;
storm::formula::PctlFormula<double>* formula;
};
} // namespace parser
} // namespace mrmc
} // namespace storm
#endif /* MRMC_PARSER_PRCTLPARSER_H_ */
#endif /* STORM_PARSER_PRCTLPARSER_H_ */

6
src/parser/SparseStateRewardParser.cpp
View File

@ -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

10
src/parser/SparseStateRewardParser.h
View File

@ -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 <memory>
#include <vector>
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_ */

10
src/reward/RewardModel.h
View File

@ -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 <stdexcept>
#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_ */

26
src/solver/GraphAnalyzer.h
View File

@ -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 <class T>
static void getExistsPhiUntilPsiStates(mrmc::models::Dtmc<T>& model, const mrmc::storage::BitVector& phiStates, const mrmc::storage::BitVector& psiStates, mrmc::storage::BitVector* existsPhiUntilPsiStates) {
static void getExistsPhiUntilPsiStates(storm::models::Dtmc<T>& 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<T>& backwardTransitions = model.getBackwardTransitions();
storm::models::GraphTransitions<T>& 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 <class T>
static void getAlwaysPhiUntilPsiStates(mrmc::models::Dtmc<T>& 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<T>& 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 <class T>
static void getPhiUntilPsiStates(mrmc::models::Dtmc<T>& 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<T>& 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_ */

16
src/storage/BitVector.h
View File

@ -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 <exception>
#include <new>
@ -18,7 +18,7 @@ extern log4cplus::Logger logger;
#include <iostream>
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<uint_fast64_t>(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<uint_fast64_t>(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_

24
src/storage/JacobiDecomposition.h
View File

@ -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 T>
class JacobiDecomposition {
public:
JacobiDecomposition(mrmc::storage::SquareSparseMatrix<T> * const jacobiLuMatrix, mrmc::storage::SquareSparseMatrix<T> * const jacobiDInvMatrix) : jacobiLuMatrix(jacobiLuMatrix), jacobiDInvMatrix(jacobiDInvMatrix) {
JacobiDecomposition(storm::storage::SquareSparseMatrix<T> * const jacobiLuMatrix, storm::storage::SquareSparseMatrix<T> * 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<T>& getJacobiLUReference() {
storm::storage::SquareSparseMatrix<T>& 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<T>& getJacobiDInvReference() {
storm::storage::SquareSparseMatrix<T>& 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<T>* getJacobiLU() {
storm::storage::SquareSparseMatrix<T>* 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<T>* getJacobiDInv() {
storm::storage::SquareSparseMatrix<T>* getJacobiDInv() {
return this->jacobiDInvMatrix;
}
@ -81,16 +81,16 @@ private:
/*!
* Pointer to the LU Matrix
*/
mrmc::storage::SquareSparseMatrix<T> *jacobiLuMatrix;
storm::storage::SquareSparseMatrix<T> *jacobiLuMatrix;
/*!
* Pointer to the D^{-1} Matrix
*/
mrmc::storage::SquareSparseMatrix<T> *jacobiDInvMatrix;
storm::storage::SquareSparseMatrix<T> *jacobiDInvMatrix;
};
} // namespace storage
} // namespace mrmc
} // namespace storm
#endif // MRMC_STORAGE_JACOBIDECOMPOSITION_H_
#endif // STORM_STORAGE_JACOBIDECOMPOSITION_H_

68
src/storage/SquareSparseMatrix.h
View File

@ -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 <exception>
#include <new>
@ -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<int_fast32_t>(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<T>();
valueStorage[rowStart] = storm::utility::constGetZero<T>();
++rowStart;
}
// Set the element on the diagonal to one.
diagonalStorage[row] = mrmc::utility::constGetOne<T>();
diagonalStorage[row] = storm::utility::constGetOne<T>();
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<T>* resultVector) const {
void getConstrainedRowCountVector(const storm::storage::BitVector& rowConstraint, const storm::storage::BitVector& columnConstraint, std::vector<T>* 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<T>* getJacobiDecomposition() const {
storm::storage::JacobiDecomposition<T>* getJacobiDecomposition() const {
uint_fast64_t rowCount = this->getRowCount();
SquareSparseMatrix<T> *resultLU = new SquareSparseMatrix<T>(this);
SquareSparseMatrix<T> *resultDinv = new SquareSparseMatrix<T>(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<T>();
resultLU->getValue(i, i) = storm::utility::constGetZero<T>();
}
return new mrmc::storage::JacobiDecomposition<T>(resultLU, resultDinv);
return new storm::storage::JacobiDecomposition<T>(resultLU, resultDinv);
}
/*!
@ -1077,6 +1077,6 @@ private:
} // namespace storage
} // namespace mrmc
} // namespace storm
#endif // MRMC_STORAGE_SQUARESPARSEMATRIX_H_
#endif // STORM_STORAGE_SQUARESPARSEMATRIX_H_

46
src/mrmc.cpp → src/storm.cpp
View File

@ -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 <sstream>
#include <vector>
#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<log4cplus::Layout>(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<mrmc::modelChecker::GmmxxDtmcPrctlModelChecker<double>>();
s = mrmc::settings::newInstance(argc, argv, nullptr);
} catch (mrmc::exceptions::InvalidSettingsException& e) {
storm::settings::Settings::registerModule<storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>>();
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<mrmc::models::Dtmc<double>> dtmc = dtmcParser.getDtmc();
storm::settings::Settings* s = storm::settings::instance();
storm::parser::DtmcParser dtmcParser(s->getString("trafile"), s->getString("labfile"));
std::shared_ptr<storm::models::Dtmc<double>> dtmc = dtmcParser.getDtmc();
dtmc->printModelInformationToStream(std::cout);
mrmc::formula::Ap<double>* trueFormula = new mrmc::formula::Ap<double>("true");
mrmc::formula::Ap<double>* observe0Greater1Formula = new mrmc::formula::Ap<double>("observe0Greater1");
mrmc::formula::Until<double>* untilFormula = new mrmc::formula::Until<double>(trueFormula, observe0Greater1Formula);
mrmc::formula::ProbabilisticNoBoundsOperator<double>* probFormula = new mrmc::formula::ProbabilisticNoBoundsOperator<double>(untilFormula);
mrmc::modelChecker::GmmxxDtmcPrctlModelChecker<double>* mc = new mrmc::modelChecker::GmmxxDtmcPrctlModelChecker<double>(*dtmc);
storm::formula::Ap<double>* trueFormula = new storm::formula::Ap<double>("true");
storm::formula::Ap<double>* observe0Greater1Formula = new storm::formula::Ap<double>("observe0Greater1");
storm::formula::Until<double>* untilFormula = new storm::formula::Until<double>(trueFormula, observe0Greater1Formula);
storm::formula::ProbabilisticNoBoundsOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundsOperator<double>(untilFormula);
storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>(*dtmc);
mc->check(*probFormula);
delete mc;

10
src/utility/ConstTemplates.h
View File

@ -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_ */

14
src/utility/IoUtility.cpp
View File

@ -11,12 +11,12 @@
#include <fstream>
namespace mrmc {
namespace storm {
namespace utility {
void dtmcToDot(mrmc::models::Dtmc<double> const &dtmc, std::string filename) {
std::shared_ptr<mrmc::storage::SquareSparseMatrix<double>> matrix(dtmc.getTransitionProbabilityMatrix());
void dtmcToDot(storm::models::Dtmc<double> const &dtmc, std::string filename) {
std::shared_ptr<storm::storage::SquareSparseMatrix<double>> matrix(dtmc.getTransitionProbabilityMatrix());
double* diagonal_storage = matrix->getDiagonalStoragePointer();
std::ofstream file;
@ -60,13 +60,13 @@ void dtmcToDot(mrmc::models::Dtmc<double> const &dtmc, std::string filename) {
}
//TODO: Should this stay here or be integrated in the new parser structure?
/*mrmc::models::Dtmc<double>* parseDTMC(std::string const &tra_file, std::string const &lab_file) {
mrmc::parser::DeterministicSparseTransitionParser tp(tra_file);
/*storm::models::Dtmc<double>* 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<double>* result = new mrmc::models::Dtmc<double>(tp.getMatrix(), lp.getLabeling());
storm::models::Dtmc<double>* result = new storm::models::Dtmc<double>(tp.getMatrix(), lp.getLabeling());
return result;
}*/

14
src/utility/IoUtility.h
View File

@ -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<double> const &dtmc, std::string filename);
void dtmcToDot(storm::models::Dtmc<double> 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<double> const &dtmc, std::string filename);
@returns The DTMC described by the two files.
*/
//mrmc::models::Dtmc<double>* parseDTMC(std::string const &tra_file, std::string const &lab_file);
//storm::models::Dtmc<double>* 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_ */

6
src/utility/OsDetection.h
View File

@ -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_

26
src/utility/Settings.cpp
View File

@ -15,7 +15,7 @@ extern log4cplus::Logger logger;
#include <boost/algorithm/string/join.hpp>
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<bpo::options_description> mrmc::settings::Settings::desc = nullptr;
std::string mrmc::settings::Settings::binaryName = "";
mrmc::settings::Settings* mrmc::settings::Settings::inst = nullptr;
std::unique_ptr<bpo::options_description> storm::settings::Settings::desc = nullptr;
std::string storm::settings::Settings::binaryName = "";
storm::settings::Settings* storm::settings::Settings::inst = nullptr;
std::map< std::pair<std::string, std::string>, std::shared_ptr<bpo::options_description> > mrmc::settings::Settings::modules;
std::map< std::pair<std::string, std::string>, std::shared_ptr<bpo::options_description> > 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] <transition file> <label file>" << std::endl;
os << *(mrmc::settings::Settings::desc) << std::endl;
os << "Usage: " << storm::settings::Settings::binaryName << " [options] <transition file> <label file>" << std::endl;
os << *(storm::settings::Settings::desc) << std::endl;
for (auto it : Settings::modules) {
os << *(it.second) << std::endl;
}
@ -192,4 +192,4 @@ std::ostream& help(std::ostream& os) {
}
} // namespace settings
} // namespace mrmc
} // namespace storm

18
src/utility/Settings.h
View File

@ -5,8 +5,8 @@
* Author: Gereon Kremer
*/
#ifndef MRMC_SETTINGS_SETTINGS_H_
#define MRMC_SETTINGS_SETTINGS_H_
#ifndef STORM_SETTINGS_SETTINGS_H_
#define STORM_SETTINGS_SETTINGS_H_
#include <iostream>
#include <sstream>
@ -16,7 +16,7 @@
#include <boost/program_options.hpp>
#include "src/exceptions/InvalidSettingsException.h"
namespace mrmc {
namespace storm {
/*!
* @brief Contains Settings class and associated methods.
@ -34,10 +34,10 @@ namespace settings {
* commandline and additionally load options from a file.
*
* It is meant to be used as a singleton. Call
* @code mrmc::settings::newInstance(argc, argv, filename) @endcode
* @code storm::settings::newInstance(argc, argv, filename) @endcode
* to initialize it and obtain an instance for the first time.
* Afterwards, use
* @code mrmc::settings::instance() @endcode
* @code storm::settings::instance() @endcode
*
* This class can be customized by other parts of the software using
* option modules. An option module can be anything that implements the
@ -52,7 +52,7 @@ namespace settings {
*/
template <typename T>
const T& get(const std::string &name) const {
if (this->vm.count(name) == 0) throw mrmc::exceptions::InvalidSettingsException() << "Could not read option " << name << ".";
if (this->vm.count(name) == 0) throw storm::exceptions::InvalidSettingsException() << "Could not read option " << name << ".";
return this->vm[name].as<T>();
}
@ -75,7 +75,7 @@ namespace settings {
*
* A new settings module can be registered via
* @code
* mrmc::settings::Settings::registerModule<mrmc::ModuleClass>();
* storm::settings::Settings::registerModule<storm::ModuleClass>();
* @endcode
* This has to be done before any parsing takes place, i.e. before newInstance() is called.
*
@ -207,6 +207,6 @@ namespace settings {
}
} // namespace settings
} // namespace mrmc
} // namespace storm
#endif // MRMC_SETTINGS_SETTINGS_H_
#endif // STORM_SETTINGS_SETTINGS_H_

16
src/utility/Vector.h
View File

@ -5,17 +5,17 @@
* Author: Christian Dehnert
*/
#ifndef MRMC_UTILITY_VECTOR_H_
#define MRMC_UTILITY_VECTOR_H_
#ifndef STORM_UTILITY_VECTOR_H_
#define STORM_UTILITY_VECTOR_H_
#include "Eigen/src/Core/Matrix.h"
namespace mrmc {
namespace storm {
namespace utility {
template<class T>
void setVectorValues(std::vector<T>* vector, const mrmc::storage::BitVector& positions, const std::vector<T> values) {
void setVectorValues(std::vector<T>* vector, const storm::storage::BitVector& positions, const std::vector<T> values) {
uint_fast64_t oldPosition = 0;
for (auto position : positions) {
(*vector)[position] = values[oldPosition++];
@ -23,14 +23,14 @@ void setVectorValues(std::vector<T>* vector, const mrmc::storage::BitVector& pos
}
template<class T>
void setVectorValues(std::vector<T>* vector, const mrmc::storage::BitVector& positions, T value) {
void setVectorValues(std::vector<T>* vector, const storm::storage::BitVector& positions, T value) {
for (auto position : positions) {
(*vector)[position] = value;
}
}
template<class T>
void setVectorValues(Eigen::Matrix<T, -1, 1, 0, -1, 1>* eigenVector, const mrmc::storage::BitVector& positions, T value) {
void setVectorValues(Eigen::Matrix<T, -1, 1, 0, -1, 1>* eigenVector, const storm::storage::BitVector& positions, T value) {
for (auto position : positions) {
(*eigenVector)(position, 0) = value;
}
@ -38,6 +38,6 @@ void setVectorValues(Eigen::Matrix<T, -1, 1, 0, -1, 1>* eigenVector, const mrmc:
} //namespace utility
} //namespace mrmc
} //namespace storm
#endif /* MRMC_UTILITY_VECTOR_H_ */
#endif /* STORM_UTILITY_VECTOR_H_ */

4
storm-config.h.in
View File

@ -0,0 +1,4 @@
// the configured options and settings for STORM
#define STORM_CPP_VERSION_MAJOR @STORM_CPP_VERSION_MAJOR@
#define STORM_CPP_VERSION_MINOR @STORM_CPP_VERSION_MINOR@
#define STORM_CPP_TESTS_BASE_PATH "@STORM_CPP_TESTS_BASE_PATH@"

4
test/mrmc-tests.cpp
View File

@ -12,7 +12,7 @@ log4cplus::Logger logger;
* Initializes the logging framework.
*/
void setUpLogging() {
log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender("mrmc-tests.log"));
log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender("storm-tests.log"));
fileLogAppender->setName("mainFileAppender");
fileLogAppender->setLayout(std::auto_ptr<log4cplus::Layout>(new log4cplus::PatternLayout("%-5p - %D{%H:%M} (%r ms) - %F:%L : %m%n")));
logger = log4cplus::Logger::getInstance("mainLogger");
@ -27,7 +27,7 @@ void setUpLogging() {
int main(int argc, char** argv) {
setUpLogging();
std::cout << "MRMC Testing Suite" << std::endl;
std::cout << "STORM Testing Suite" << std::endl;
testing::InitGoogleTest(&argc, argv);

12
test/parser/ParseDtmcTest.cpp
View File

@ -7,17 +7,17 @@
#include "gtest/gtest.h"
#include "mrmc-config.h"
#include "storm-config.h"
#include "src/parser/DtmcParser.h"
#include "src/utility/IoUtility.h"
TEST(ParseDtmcTest, parseAndOutput) {
mrmc::parser::DtmcParser* dtmcParser;
ASSERT_NO_THROW(dtmcParser = new mrmc::parser::DtmcParser(
MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/pctl_general_input_01.tra",
MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
storm::parser::DtmcParser* dtmcParser;
ASSERT_NO_THROW(dtmcParser = new storm::parser::DtmcParser(
STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/pctl_general_input_01.tra",
STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
ASSERT_NO_THROW(mrmc::utility::dtmcToDot(*(dtmcParser->getDtmc()), MRMC_CPP_TESTS_BASE_PATH "/parser/output.dot"));
ASSERT_NO_THROW(storm::utility::dtmcToDot(*(dtmcParser->getDtmc()), STORM_CPP_TESTS_BASE_PATH "/parser/output.dot"));
delete dtmcParser;
}

16
test/parser/ReadLabFileTest.cpp
View File

@ -6,7 +6,7 @@
*/
#include "gtest/gtest.h"
#include "mrmc-config.h"
#include "storm-config.h"
#include "src/models/AtomicPropositionsLabeling.h"
#include "src/parser/AtomicPropositionLabelingParser.h"
#include "src/exceptions/FileIoException.h"
@ -16,17 +16,17 @@
TEST(ReadLabFileTest, NonExistingFileTest) {
//No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-)
ASSERT_THROW(mrmc::parser::AtomicPropositionLabelingParser(0,MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::FileIoException);
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(0,STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException);
}
TEST(ReadLabFileTest, ParseTest) {
//This test is based on a test case from the original MRMC.
mrmc::parser::AtomicPropositionLabelingParser* parser;
storm::parser::AtomicPropositionLabelingParser* parser;
//Parsing the file
ASSERT_NO_THROW(parser = new mrmc::parser::AtomicPropositionLabelingParser(12, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
std::shared_ptr<mrmc::models::AtomicPropositionsLabeling> labeling(parser->getLabeling());
ASSERT_NO_THROW(parser = new storm::parser::AtomicPropositionLabelingParser(12, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
std::shared_ptr<storm::models::AtomicPropositionsLabeling> labeling(parser->getLabeling());
//Checking whether all propositions are in the labelling
@ -86,14 +86,14 @@ TEST(ReadLabFileTest, ParseTest) {
}
TEST(ReadLabFileTest, WrongHeaderTest1) {
ASSERT_THROW(mrmc::parser::AtomicPropositionLabelingParser(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header1.lab"), mrmc::exceptions::WrongFileFormatException);
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header1.lab"), storm::exceptions::WrongFileFormatException);
}
TEST(ReadLabFileTest, WrongHeaderTest2) {
ASSERT_THROW(mrmc::parser::AtomicPropositionLabelingParser(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header2.lab"), mrmc::exceptions::WrongFileFormatException);
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_header2.lab"), storm::exceptions::WrongFileFormatException);
}
TEST(ReadLabFileTest, WrongPropositionTest) {
ASSERT_THROW(mrmc::parser::AtomicPropositionLabelingParser(3, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_proposition.lab"), mrmc::exceptions::WrongFileFormatException);
ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/wrong_format_proposition.lab"), storm::exceptions::WrongFileFormatException);
}

18
test/parser/ReadTraFileTest.cpp
View File

@ -6,7 +6,7 @@
*/
#include "gtest/gtest.h"
#include "mrmc-config.h"
#include "storm-config.h"
#include "src/storage/SquareSparseMatrix.h"
#include "src/parser/DeterministicSparseTransitionParser.h"
#include "src/exceptions/FileIoException.h"
@ -16,15 +16,15 @@
TEST(ReadTraFileTest, NonExistingFileTest) {
//No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-)
ASSERT_THROW(mrmc::parser::DeterministicSparseTransitionParser(MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::FileIoException);
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException);
}
/* The following test case is based on one of the original MRMC test cases
/* The following test case is based on one of the original STORM test cases
*/
TEST(ReadTraFileTest, ParseFileTest1) {
mrmc::parser::DeterministicSparseTransitionParser* parser;
ASSERT_NO_THROW(parser = new mrmc::parser::DeterministicSparseTransitionParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/csl_general_input_01.tra"));
std::shared_ptr<mrmc::storage::SquareSparseMatrix<double>> result = parser->getMatrix();
storm::parser::DeterministicSparseTransitionParser* parser;
ASSERT_NO_THROW(parser = new storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/csl_general_input_01.tra"));
std::shared_ptr<storm::storage::SquareSparseMatrix<double>> result = parser->getMatrix();
if (result != NULL) {
double val = 0;
@ -69,13 +69,13 @@ TEST(ReadTraFileTest, ParseFileTest1) {
}
TEST(ReadTraFileTest, WrongFormatTestHeader1) {
ASSERT_THROW(mrmc::parser::DeterministicSparseTransitionParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header1.tra"), mrmc::exceptions::WrongFileFormatException);
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header1.tra"), storm::exceptions::WrongFileFormatException);
}
TEST(ReadTraFileTest, WrongFormatTestHeader2) {
ASSERT_THROW(mrmc::parser::DeterministicSparseTransitionParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header2.tra"), mrmc::exceptions::WrongFileFormatException);
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_header2.tra"), storm::exceptions::WrongFileFormatException);
}
TEST(ReadTraFileTest, WrongFormatTestTransition) {
ASSERT_THROW(mrmc::parser::DeterministicSparseTransitionParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_transition.tra"), mrmc::exceptions::WrongFileFormatException);
ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser(STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/wrong_format_transition.tra"), storm::exceptions::WrongFileFormatException);
}

2
test/reward/RewardModelTest.cpp
View File

@ -9,7 +9,7 @@
TEST(RewardModelTest, ReadWriteTest) {
// 50 entries
mrmc::reward::RewardModel<std::vector, double> rm(50, 0.0);
storm::reward::RewardModel<std::vector, double> rm(50, 0.0);
double values[50];
for (int i = 0; i < 50; ++i) {

36
test/storage/BitVectorTest.cpp
View File

@ -3,8 +3,8 @@
#include "src/exceptions/InvalidArgumentException.h"
TEST(BitVectorTest, GetSetTest) {
mrmc::storage::BitVector *bv = NULL;
ASSERT_NO_THROW(bv = new mrmc::storage::BitVector(32));
storm::storage::BitVector *bv = NULL;
ASSERT_NO_THROW(bv = new storm::storage::BitVector(32));
for (int i = 0; i < 32; ++i) {
bv->set(i, i % 2 == 0);
@ -17,7 +17,7 @@ TEST(BitVectorTest, GetSetTest) {
}
TEST(BitVectorTest, InitialZeroTest) {
mrmc::storage::BitVector bvA(32);
storm::storage::BitVector bvA(32);
for (int i = 0; i < 32; ++i) {
ASSERT_FALSE(bvA.get(i));
@ -25,7 +25,7 @@ TEST(BitVectorTest, InitialZeroTest) {
}
TEST(BitVectorTest, ResizeTest) {
mrmc::storage::BitVector bvA(32);
storm::storage::BitVector bvA(32);
for (int i = 0; i < 32; ++i) {
bvA.set(i, true);
@ -46,15 +46,15 @@ TEST(BitVectorTest, ResizeTest) {
}
TEST(BitVectorTest, OperatorNotTest) {
mrmc::storage::BitVector bvA(32);
mrmc::storage::BitVector bvB(32);
storm::storage::BitVector bvA(32);
storm::storage::BitVector bvB(32);
for (int i = 0; i < 32; ++i) {
bvA.set(i, i % 2 == 0);
bvB.set(i, i % 2 == 1);
}
mrmc::storage::BitVector bvN = ~bvB;
storm::storage::BitVector bvN = ~bvB;
for (int i = 0; i < 32; ++i) {
ASSERT_EQ(bvA.get(i), bvN.get(i));
@ -62,15 +62,15 @@ TEST(BitVectorTest, OperatorNotTest) {
}
TEST(BitVectorTest, OperatorAndTest) {
mrmc::storage::BitVector bvA(32);
mrmc::storage::BitVector bvB(32);
storm::storage::BitVector bvA(32);
storm::storage::BitVector bvB(32);
for (int i = 0; i < 32; ++i) {
bvA.set(i, i % 2 == 0);
bvB.set(i, i % 2 == 1);
}
mrmc::storage::BitVector bvN = bvA & bvB;
storm::storage::BitVector bvN = bvA & bvB;
for (int i = 0; i < 32; ++i) {
ASSERT_FALSE(bvN.get(i));
@ -78,15 +78,15 @@ TEST(BitVectorTest, OperatorAndTest) {
}
TEST(BitVectorTest, OperatorOrTest) {
mrmc::storage::BitVector bvA(32);
mrmc::storage::BitVector bvB(32);
storm::storage::BitVector bvA(32);
storm::storage::BitVector bvB(32);
for (int i = 0; i < 32; ++i) {
bvA.set(i, i % 2 == 0);
bvB.set(i, i % 2 == 1);
}
mrmc::storage::BitVector bvN = bvA | bvB;
storm::storage::BitVector bvN = bvA | bvB;
for (int i = 0; i < 32; ++i) {
ASSERT_TRUE(bvN.get(i));
@ -94,17 +94,17 @@ TEST(BitVectorTest, OperatorOrTest) {
}
TEST(BitVectorTest, OperatorXorTest) {
mrmc::storage::BitVector bvA(32);
mrmc::storage::BitVector bvB(32);
storm::storage::BitVector bvA(32);
storm::storage::BitVector bvB(32);
for (int i = 0; i < 32; ++i) {
bvA.set(i, true);
bvB.set(i, i % 2 == 1);
}
mrmc::storage::BitVector bvN = bvA ^ bvB;
mrmc::storage::BitVector bvO = ~bvB;
mrmc::storage::BitVector bvP = bvA ^ bvA;
storm::storage::BitVector bvN = bvA ^ bvB;
storm::storage::BitVector bvO = ~bvB;
storm::storage::BitVector bvP = bvA ^ bvA;
for (int i = 0; i < 32; ++i) {
ASSERT_EQ(bvN.get(i), bvO.get(i));

94
test/storage/SquareSparseMatrixTest.cpp
View File

@ -4,70 +4,70 @@
#include "src/exceptions/OutOfRangeException.h"
TEST(SquareSparseMatrixTest, ZeroRowsTest) {
mrmc::storage::SquareSparseMatrix<int> *ssm = new mrmc::storage::SquareSparseMatrix<int>(0);
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
storm::storage::SquareSparseMatrix<int> *ssm = new storm::storage::SquareSparseMatrix<int>(0);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
ASSERT_THROW(ssm->initialize(50), mrmc::exceptions::InvalidArgumentException);
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::Error);
ASSERT_THROW(ssm->initialize(50), storm::exceptions::InvalidArgumentException);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Error);
delete ssm;
}
TEST(SquareSparseMatrixTest, TooManyEntriesTest) {
mrmc::storage::SquareSparseMatrix<int> *ssm = new mrmc::storage::SquareSparseMatrix<int>(2);
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
storm::storage::SquareSparseMatrix<int> *ssm = new storm::storage::SquareSparseMatrix<int>(2);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
ASSERT_THROW(ssm->initialize(10), mrmc::exceptions::InvalidArgumentException);
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::Error);
ASSERT_THROW(ssm->initialize(10), storm::exceptions::InvalidArgumentException);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Error);
delete ssm;
}
TEST(SquareSparseMatrixTest, addNextValueTest) {
mrmc::storage::SquareSparseMatrix<int> *ssm = new mrmc::storage::SquareSparseMatrix<int>(5);
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
storm::storage::SquareSparseMatrix<int> *ssm = new storm::storage::SquareSparseMatrix<int>(5);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
ASSERT_NO_THROW(ssm->initialize(1));
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_THROW(ssm->addNextValue(-1, 1, 1), mrmc::exceptions::OutOfRangeException);
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::Error);
ASSERT_THROW(ssm->addNextValue(-1, 1, 1), storm::exceptions::OutOfRangeException);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Error);
ASSERT_THROW(ssm->addNextValue(1, -1, 1), mrmc::exceptions::OutOfRangeException);
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::Error);
ASSERT_THROW(ssm->addNextValue(1, -1, 1), storm::exceptions::OutOfRangeException);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Error);
ASSERT_THROW(ssm->addNextValue(6, 1, 1), mrmc::exceptions::OutOfRangeException);
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::Error);
ASSERT_THROW(ssm->addNextValue(6, 1, 1), storm::exceptions::OutOfRangeException);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Error);
ASSERT_THROW(ssm->addNextValue(1, 6, 1), mrmc::exceptions::OutOfRangeException);
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::Error);
ASSERT_THROW(ssm->addNextValue(1, 6, 1), storm::exceptions::OutOfRangeException);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Error);
delete ssm;
}
TEST(SquareSparseMatrixTest, finalizeTest) {
mrmc::storage::SquareSparseMatrix<int> *ssm = new mrmc::storage::SquareSparseMatrix<int>(5);
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
storm::storage::SquareSparseMatrix<int> *ssm = new storm::storage::SquareSparseMatrix<int>(5);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
ASSERT_NO_THROW(ssm->initialize(5));
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_NO_THROW(ssm->addNextValue(1, 2, 1));
ASSERT_NO_THROW(ssm->addNextValue(1, 3, 1));
ASSERT_NO_THROW(ssm->addNextValue(1, 4, 1));
ASSERT_NO_THROW(ssm->addNextValue(1, 5, 1));
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_THROW(ssm->finalize(), mrmc::exceptions::InvalidStateException);
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::Error);
ASSERT_THROW(ssm->finalize(), storm::exceptions::InvalidStateException);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Error);
delete ssm;
}
TEST(SquareSparseMatrixTest, Test) {
// 25 rows, 50 non zero entries
mrmc::storage::SquareSparseMatrix<int> *ssm = new mrmc::storage::SquareSparseMatrix<int>(25);
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
storm::storage::SquareSparseMatrix<int> *ssm = new storm::storage::SquareSparseMatrix<int>(25);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
int values[50] = {
0, 1, 2, 3, 4, 5, 6, 7, 8, 9,
@ -96,15 +96,15 @@ TEST(SquareSparseMatrixTest, Test) {
};
ASSERT_NO_THROW(ssm->initialize(50));
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
for (int i = 0; i < 50; ++i) {
ASSERT_NO_THROW(ssm->addNextValue(position_row[i], position_col[i], values[i]));
}
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_NO_THROW(ssm->finalize());
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::ReadReady);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::ReadReady);
int target;
for (int i = 0; i < 50; ++i) {
@ -125,15 +125,15 @@ TEST(SquareSparseMatrixTest, Test) {
ASSERT_EQ(0, target);
}
}
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::ReadReady);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::ReadReady);
delete ssm;
}
TEST(SquareSparseMatrixTest, ConversionFromDenseEigen_ColMajor_SparseMatrixTest) {
// 10 rows, 100 non zero entries
mrmc::storage::SquareSparseMatrix<int> *ssm = new mrmc::storage::SquareSparseMatrix<int>(10);
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
storm::storage::SquareSparseMatrix<int> *ssm = new storm::storage::SquareSparseMatrix<int>(10);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
Eigen::SparseMatrix<int> esm(10, 10);
for (int row = 0; row < 10; ++row) {
@ -149,7 +149,7 @@ TEST(SquareSparseMatrixTest, ConversionFromDenseEigen_ColMajor_SparseMatrixTest)
ASSERT_NO_THROW(ssm->finalize());
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::ReadReady);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::ReadReady);
int target = -1;
for (int row = 0; row < 10; ++row) {
@ -164,8 +164,8 @@ TEST(SquareSparseMatrixTest, ConversionFromDenseEigen_ColMajor_SparseMatrixTest)
TEST(SquareSparseMatrixTest, ConversionFromDenseEigen_RowMajor_SparseMatrixTest) {
// 10 rows, 100 non zero entries
mrmc::storage::SquareSparseMatrix<int> *ssm = new mrmc::storage::SquareSparseMatrix<int>(10);
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
storm::storage::SquareSparseMatrix<int> *ssm = new storm::storage::SquareSparseMatrix<int>(10);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
Eigen::SparseMatrix<int, Eigen::RowMajor> esm(10, 10);
for (int row = 0; row < 10; ++row) {
@ -181,7 +181,7 @@ TEST(SquareSparseMatrixTest, ConversionFromDenseEigen_RowMajor_SparseMatrixTest)
ASSERT_NO_THROW(ssm->finalize());
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::ReadReady);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::ReadReady);
int target = -1;
for (int row = 0; row < 10; ++row) {
@ -196,8 +196,8 @@ TEST(SquareSparseMatrixTest, ConversionFromDenseEigen_RowMajor_SparseMatrixTest)
TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_ColMajor_SparseMatrixTest) {
// 10 rows, 15 non zero entries
mrmc::storage::SquareSparseMatrix<int> *ssm = new mrmc::storage::SquareSparseMatrix<int>(10);
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
storm::storage::SquareSparseMatrix<int> *ssm = new storm::storage::SquareSparseMatrix<int>(10);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
Eigen::SparseMatrix<int> esm(10, 10);
@ -231,7 +231,7 @@ TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_ColMajor_SparseMatrixTest
ASSERT_NO_THROW(ssm->finalize());
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::ReadReady);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::ReadReady);
int target = -1;
@ -245,8 +245,8 @@ TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_ColMajor_SparseMatrixTest
TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest) {
// 10 rows, 15 non zero entries
mrmc::storage::SquareSparseMatrix<int> *ssm = new mrmc::storage::SquareSparseMatrix<int>(10);
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
storm::storage::SquareSparseMatrix<int> *ssm = new storm::storage::SquareSparseMatrix<int>(10);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::UnInitialized);
Eigen::SparseMatrix<int, Eigen::RowMajor> esm(10, 10);
@ -280,7 +280,7 @@ TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest
ASSERT_NO_THROW(ssm->finalize());
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::ReadReady);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::ReadReady);
int target = -1;
@ -294,24 +294,24 @@ TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest
TEST(SquareSparseMatrixTest, ConversionToSparseEigen_RowMajor_SparseMatrixTest) {
int values[100];
mrmc::storage::SquareSparseMatrix<int> *ssm = new mrmc::storage::SquareSparseMatrix<int>(10);
storm::storage::SquareSparseMatrix<int> *ssm = new storm::storage::SquareSparseMatrix<int>(10);
for (uint_fast32_t i = 0; i < 100; ++i) {
values[i] = i;
}
ASSERT_NO_THROW(ssm->initialize(100 - 10));
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
for (uint_fast32_t row = 0; row < 10; ++row) {
for (uint_fast32_t col = 0; col < 10; ++col) {
ASSERT_NO_THROW(ssm->addNextValue(row, col, values[row * 10 + col]));
}
}
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_NO_THROW(ssm->finalize());
ASSERT_EQ(ssm->getState(), mrmc::storage::SquareSparseMatrix<int>::MatrixStatus::ReadReady);
ASSERT_EQ(ssm->getState(), storm::storage::SquareSparseMatrix<int>::MatrixStatus::ReadReady);
Eigen::SparseMatrix<int, Eigen::RowMajor, int_fast32_t>* esm = ssm->toEigenSparseMatrix();

Write Preview
|||||||
100:0
Loading…
Cancel
Save