diff --git a/CMakeLists.txt b/CMakeLists.txt
index cd51e1343..ee5bf36be 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -25,8 +25,8 @@ option(STORM_DEVELOPER "Sets whether the development mode is used." OFF)
option(STORM_ALLWARNINGS "Compile with even more warnings" OFF)
option(STORM_USE_LTO "Sets whether link-time optimizations are enabled." ON)
MARK_AS_ADVANCED(STORM_USE_LTO)
-option(STORM_PORTABLE_RELEASE "Sets whether a release build needs to be portable to another machine." OFF)
-MARK_AS_ADVANCED(STORM_PORTABLE_RELEASE)
+option(STORM_PORTABLE "Sets whether a build needs to be portable." OFF)
+MARK_AS_ADVANCED(STORM_PORTABLE)
option(STORM_USE_POPCNT "Sets whether the popcnt instruction is going to be used." ON)
MARK_AS_ADVANCED(STORM_USE_POPCNT)
option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be linked statically." OFF)
@@ -239,7 +239,7 @@ if (STORM_USE_LTO)
endif()
# In release mode, we turn on even more optimizations if we do not have to provide a portable binary.
-if (NOT STORM_PORTABLE_RELEASE)
+if (NOT STORM_PORTABLE)
set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -march=native")
endif ()
diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
index 9dcf30aed..64fc5d7b3 100644
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@@ -351,7 +351,7 @@ ExternalProject_Add(
DOWNLOAD_COMMAND ""
PREFIX "sylvan"
SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/sylvan
- CMAKE_ARGS -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DSYLVAN_BUILD_TEST=Off -DSYLVAN_BUILD_EXAMPLES=Off -DCMAKE_BUILD_TYPE=Release -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DUSE_CARL=ON -Dcarl_INCLUDE_DIR=${carl_INCLUDE_DIR} -DSYLVAN_PORTABLE=${STORM_PORTABLE_RELEASE} -Dcarl_LIBRARIES=${carl_LIBRARIES}
+ CMAKE_ARGS -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DSYLVAN_BUILD_TEST=Off -DSYLVAN_BUILD_EXAMPLES=Off -DCMAKE_BUILD_TYPE=Release -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DUSE_CARL=ON -Dcarl_INCLUDE_DIR=${carl_INCLUDE_DIR} -DSYLVAN_PORTABLE=${STORM_PORTABLE} -Dcarl_LIBRARIES=${carl_LIBRARIES}
BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/sylvan
BUILD_IN_SOURCE 0
INSTALL_COMMAND ""
diff --git a/resources/3rdparty/include_cpptemplate.cmake b/resources/3rdparty/include_cpptemplate.cmake
index e6f341b31..3cf4f43b4 100644
--- a/resources/3rdparty/include_cpptemplate.cmake
+++ b/resources/3rdparty/include_cpptemplate.cmake
@@ -24,6 +24,6 @@ set(CPPTEMPLATE_INCLUDE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/cpptemplate)
set(CPPTEMPLATE_STATIC_LIBRARY ${STORM_3RDPARTY_BINARY_DIR}/cpptemplate/cpptemplate${STATIC_EXT})
add_dependencies(resources cpptemplate)
-message(STATUS "Storm - Linking with cpptemplate.")
+message(STATUS "storm - Linking with cpptemplate.")
add_imported_library(cpptempl STATIC ${CPPTEMPLATE_STATIC_LIBRARY} ${CPPTEMPLATE_INCLUDE_DIR})
list(APPEND STORM_DEP_TARGETS cpptempl_STATIC)
\ No newline at end of file
diff --git a/resources/3rdparty/include_cudd.cmake b/resources/3rdparty/include_cudd.cmake
index 1c03de839..8f17fb35b 100644
--- a/resources/3rdparty/include_cudd.cmake
+++ b/resources/3rdparty/include_cudd.cmake
@@ -17,7 +17,7 @@ endif()
set(CUDD_LIB_DIR ${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0/lib)
set(STORM_CUDD_FLAGS "CFLAGS=-O3 -w -DPIC -DHAVE_IEEE_754 -fno-common -ffast-math -fno-finite-math-only")
-if (NOT STORM_PORTABLE_RELEASE)
+if (NOT STORM_PORTABLE)
set(STORM_CUDD_FLAGS "${STORM_CUDD_FLAGS} -march=native")
endif()
@@ -54,4 +54,4 @@ else()
list(APPEND STORM_DEP_TARGETS cudd_STATIC)
endif()
-message(STATUS "Storm - Linking with CUDD ${CUDD_VERSION_STRING}.")
+message(STATUS "storm - Linking with CUDD ${CUDD_VERSION_STRING}.")
diff --git a/resources/3rdparty/include_glpk.cmake b/resources/3rdparty/include_glpk.cmake
index e7dc55149..1f1eed1f1 100644
--- a/resources/3rdparty/include_glpk.cmake
+++ b/resources/3rdparty/include_glpk.cmake
@@ -1,8 +1,8 @@
find_package(GLPK QUIET)
if(GLPK_FOUND)
- message (STATUS "Storm - Using system version of glpk.")
+ message (STATUS "storm - Using system version of glpk.")
else()
- message (STATUS "Storm - Using shipped version of glpk.")
+ message (STATUS "storm - Using shipped version of glpk.")
set(GLPK_LIB_DIR ${STORM_3RDPARTY_BINARY_DIR}/glpk-4.57/lib)
ExternalProject_Add(glpk_ext
DOWNLOAD_COMMAND ""
@@ -25,7 +25,7 @@ endif()
# Since there is a shipped version, always use GLPK
set(STORM_HAVE_GLPK ON)
-message (STATUS "Storm - Linking with glpk ${GLPK_VERSION_STRING}")
+message (STATUS "storm - Linking with glpk ${GLPK_VERSION_STRING}")
add_imported_library(glpk SHARED ${GLPK_LIBRARIES} ${GLPK_INCLUDE_DIR})
list(APPEND STORM_DEP_TARGETS glpk_SHARED)
\ No newline at end of file
diff --git a/resources/3rdparty/include_xerces.cmake b/resources/3rdparty/include_xerces.cmake
index 4a464835d..d7ed7e1f9 100644
--- a/resources/3rdparty/include_xerces.cmake
+++ b/resources/3rdparty/include_xerces.cmake
@@ -1,9 +1,9 @@
if(USE_XERCESC)
find_package(XercesC QUIET)
if(XercesC_FOUND)
- message(STATUS "Storm - Use system version of xerces.")
+ message(STATUS "storm - Use system version of xerces.")
else()
- message(STATUS "Storm - Use shipped version of xerces.")
+ message(STATUS "storm - Use shipped version of xerces.")
set(XercesC_LIB_DIR ${STORM_3RDPARTY_BINARY_DIR}/xercesc-3.1.2/lib)
ExternalProject_Add(
xercesc
@@ -31,7 +31,7 @@ if(USE_XERCESC)
add_dependencies(resources xercesc)
endif()
- message (STATUS "Storm - Linking with xercesc.")
+ message (STATUS "storm - Linking with xercesc.")
set(STORM_HAVE_XERCES ON)
include_directories(${XercesC_INCLUDE_DIRS})
if(APPLE)
@@ -44,5 +44,5 @@ if(USE_XERCESC)
list(APPEND STORM_GSPN_LINK_LIBRARIES ${XercesC_LIBRARIES} ${COREFOUNDATION_LIBRARY} ${CORESERVICES_LIBRARY} ${CURL_LIBRARIES})
else()
set(STORM_HAVE_XERCES OFF)
- message (WARNING "Storm - Building without Xerces disables parsing XML formats (for GSPNs)")
+ message (WARNING "torm - Building without Xerces disables parsing XML formats (for GSPNs)")
endif(USE_XERCESC)
diff --git a/src/storm-dft-cli/CMakeLists.txt b/src/storm-dft-cli/CMakeLists.txt
index f44c57103..515022607 100644
--- a/src/storm-dft-cli/CMakeLists.txt
+++ b/src/storm-dft-cli/CMakeLists.txt
@@ -1,4 +1,7 @@
# Create storm-dft.
add_executable(storm-dft-cli ${PROJECT_SOURCE_DIR}/src/storm-dft-cli/storm-dyftee.cpp)
target_link_libraries(storm-dft-cli storm-dft) # Adding headers for xcode
-set_target_properties(storm-dft-cli PROPERTIES OUTPUT_NAME "storm-dft")
\ No newline at end of file
+set_target_properties(storm-dft-cli PROPERTIES OUTPUT_NAME "storm-dft")
+
+# installation
+install(TARGETS storm-dft-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
\ No newline at end of file
diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp
index 308037d77..5f4cdaee4 100644
--- a/src/storm-dft-cli/storm-dyftee.cpp
+++ b/src/storm-dft-cli/storm-dyftee.cpp
@@ -80,7 +80,7 @@ void analyzeWithSMT(std::string filename) {
* Initialize the settings manager.
*/
void initializeSettings() {
- storm::settings::mutableManager().setName("StoRM-DyFTeE", "storm-dft");
+ storm::settings::mutableManager().setName("storm-DyFTeE", "storm-dft");
// Register all known settings modules.
storm::settings::addModule<storm::settings::modules::GeneralSettings>();
@@ -117,7 +117,7 @@ void initializeSettings() {
int main(const int argc, const char** argv) {
try {
storm::utility::setUp();
- storm::cli::printHeader("StoRM-DyFTeE", argc, argv);
+ storm::cli::printHeader("storm-DyFTeE", argc, argv);
initializeSettings();
bool optionsCorrect = storm::cli::parseOptions(argc, argv);
@@ -250,10 +250,10 @@ int main(const int argc, const char** argv) {
storm::utility::cleanUp();
return 0;
} catch (storm::exceptions::BaseException const& exception) {
- STORM_LOG_ERROR("An exception caused StoRM-DyFTeE to terminate. The message of the exception is: " << exception.what());
+ STORM_LOG_ERROR("An exception caused storm-DyFTeE to terminate. The message of the exception is: " << exception.what());
return 1;
} catch (std::exception const& exception) {
- STORM_LOG_ERROR("An unexpected exception occurred and caused StoRM-DyFTeE to terminate. The message of this exception is: " << exception.what());
+ STORM_LOG_ERROR("An unexpected exception occurred and caused storm-DyFTeE to terminate. The message of this exception is: " << exception.what());
return 2;
}
}
diff --git a/src/storm-dft/CMakeLists.txt b/src/storm-dft/CMakeLists.txt
index 10d9b8508..16fa40e48 100644
--- a/src/storm-dft/CMakeLists.txt
+++ b/src/storm-dft/CMakeLists.txt
@@ -11,3 +11,6 @@ file(GLOB_RECURSE STORM_DFT_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-dft/*/*.h)
# Create storm-pgcl.
add_library(storm-dft SHARED ${STORM_DFT_SOURCES} ${STORM_DFT_HEADERS})
target_link_libraries(storm-dft storm storm-gspn ${STORM_DFT_LINK_LIBRARIES})
+
+# installation
+install(TARGETS storm-dft RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
diff --git a/src/storm-gspn-cli/CMakeLists.txt b/src/storm-gspn-cli/CMakeLists.txt
index 343b8acc8..2898325f3 100644
--- a/src/storm-gspn-cli/CMakeLists.txt
+++ b/src/storm-gspn-cli/CMakeLists.txt
@@ -1,3 +1,6 @@
add_executable(storm-gspn-cli ${PROJECT_SOURCE_DIR}/src/storm-gspn-cli/storm-gspn.cpp)
target_link_libraries(storm-gspn-cli storm-gspn) # Adding headers for xcode
set_target_properties(storm-gspn-cli PROPERTIES OUTPUT_NAME "storm-gspn")
+
+# installation
+install(TARGETS storm-gspn-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
\ No newline at end of file
diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp
index 5ea31f30c..2dd98e645 100644
--- a/src/storm-gspn-cli/storm-gspn.cpp
+++ b/src/storm-gspn-cli/storm-gspn.cpp
@@ -40,7 +40,7 @@
* Initialize the settings manager.
*/
void initializeSettings() {
- storm::settings::mutableManager().setName("StoRM-GSPN", "storm-gspn");
+ storm::settings::mutableManager().setName("storm-GSPN", "storm-gspn");
// Register all known settings modules.
storm::settings::addModule<storm::settings::modules::GeneralSettings>();
@@ -75,7 +75,7 @@ std::unordered_map<std::string, uint64_t> parseCapacitiesList(std::string const&
int main(const int argc, const char **argv) {
try {
storm::utility::setUp();
- storm::cli::printHeader("StoRM-GSPN", argc, argv);
+ storm::cli::printHeader("storm-GSPN", argc, argv);
initializeSettings();
bool optionsCorrect = storm::cli::parseOptions(argc, argv);
@@ -147,10 +147,10 @@ int main(const int argc, const char **argv) {
storm::utility::cleanUp();
return 0;
} catch (storm::exceptions::BaseException const& exception) {
- STORM_LOG_ERROR("An exception caused StoRM to terminate. The message of the exception is: " << exception.what());
+ STORM_LOG_ERROR("An exception caused storm to terminate. The message of the exception is: " << exception.what());
return 1;
} catch (std::exception const& exception) {
- STORM_LOG_ERROR("An unexpected exception occurred and caused StoRM to terminate. The message of this exception is: " << exception.what());
+ STORM_LOG_ERROR("An unexpected exception occurred and caused storm to terminate. The message of this exception is: " << exception.what());
return 2;
}
}
diff --git a/src/storm-gspn/CMakeLists.txt b/src/storm-gspn/CMakeLists.txt
index a5478280d..564b696bd 100644
--- a/src/storm-gspn/CMakeLists.txt
+++ b/src/storm-gspn/CMakeLists.txt
@@ -11,3 +11,6 @@ file(GLOB_RECURSE STORM_GSPN_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-gspn/*/*.h)
# Create storm-pgcl.
add_library(storm-gspn SHARED ${STORM_GSPN_SOURCES} ${STORM_GSPN_HEADERS})
target_link_libraries(storm-gspn storm ${STORM_GSPN_LINK_LIBRARIES})
+
+# installation
+install(TARGETS storm-gspn RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
\ No newline at end of file
diff --git a/src/storm-gspn/parser/GspnParser.cpp b/src/storm-gspn/parser/GspnParser.cpp
index b92b6f006..cf5c698f0 100644
--- a/src/storm-gspn/parser/GspnParser.cpp
+++ b/src/storm-gspn/parser/GspnParser.cpp
@@ -81,7 +81,7 @@ namespace storm {
delete errHandler;
xercesc::XMLPlatformUtils::Terminate();
#else
- STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Storm is not compiled with XML support: " << filename << " can not be parsed");
+ STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "storm is not compiled with XML support: " << filename << " can not be parsed");
#endif
}
}
diff --git a/src/storm-pgcl-cli/CMakeLists.txt b/src/storm-pgcl-cli/CMakeLists.txt
index d8884639e..0f051a1b4 100644
--- a/src/storm-pgcl-cli/CMakeLists.txt
+++ b/src/storm-pgcl-cli/CMakeLists.txt
@@ -1,3 +1,6 @@
add_executable(storm-pgcl-cli ${PROJECT_SOURCE_DIR}/src/storm-pgcl-cli/storm-pgcl.cpp)
target_link_libraries(storm-pgcl-cli storm-pgcl)
-set_target_properties(storm-pgcl-cli PROPERTIES OUTPUT_NAME "storm-pgcl")
\ No newline at end of file
+set_target_properties(storm-pgcl-cli PROPERTIES OUTPUT_NAME "storm-pgcl")
+
+# installation
+install(TARGETS storm-pgcl-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
\ No newline at end of file
diff --git a/src/storm-pgcl-cli/storm-pgcl.cpp b/src/storm-pgcl-cli/storm-pgcl.cpp
index 37accc430..6a6707177 100644
--- a/src/storm-pgcl-cli/storm-pgcl.cpp
+++ b/src/storm-pgcl-cli/storm-pgcl.cpp
@@ -25,7 +25,7 @@
* Initialize the settings manager.
*/
void initializeSettings() {
- storm::settings::mutableManager().setName("StoRM-PGCL", "storm-pgcl");
+ storm::settings::mutableManager().setName("storm-PGCL", "storm-pgcl");
// Register all known settings modules.
storm::settings::addModule<storm::settings::modules::GeneralSettings>();
@@ -59,7 +59,7 @@ void programGraphToDotFile(storm::ppg::ProgramGraph const& prog) {
int main(const int argc, const char** argv) {
try {
storm::utility::setUp();
- storm::cli::printHeader("StoRM-PGCL", argc, argv);
+ storm::cli::printHeader("storm-PGCL", argc, argv);
initializeSettings();
bool optionsCorrect = storm::cli::parseOptions(argc, argv);
@@ -96,10 +96,10 @@ int main(const int argc, const char** argv) {
}
}catch (storm::exceptions::BaseException const& exception) {
- STORM_LOG_ERROR("An exception caused StoRM-PGCL to terminate. The message of the exception is: " << exception.what());
+ STORM_LOG_ERROR("An exception caused storm-PGCL to terminate. The message of the exception is: " << exception.what());
return 1;
} catch (std::exception const& exception) {
- STORM_LOG_ERROR("An unexpected exception occurred and caused StoRM-PGCL to terminate. The message of this exception is: " << exception.what());
+ STORM_LOG_ERROR("An unexpected exception occurred and caused storm-PGCL to terminate. The message of this exception is: " << exception.what());
return 2;
}
}
diff --git a/src/storm-pgcl/CMakeLists.txt b/src/storm-pgcl/CMakeLists.txt
index bd1ffc932..e20a99483 100644
--- a/src/storm-pgcl/CMakeLists.txt
+++ b/src/storm-pgcl/CMakeLists.txt
@@ -11,3 +11,6 @@ file(GLOB_RECURSE STORM_PGCL_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-pgcl/*/*.h)
# Create storm-pgcl.
add_library(storm-pgcl SHARED ${STORM_PGCL_SOURCES} ${STORM_PGCL_HEADERS})
target_link_libraries(storm-pgcl storm)
+
+# installation
+install(TARGETS storm-pgcl RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
\ No newline at end of file
diff --git a/src/storm/CMakeLists.txt b/src/storm/CMakeLists.txt
index d9135dcb9..1a722e207 100644
--- a/src/storm/CMakeLists.txt
+++ b/src/storm/CMakeLists.txt
@@ -20,11 +20,11 @@ set(STORM_MAIN_SOURCES ${STORM_MAIN_FILE})
# Add custom additional include or link directories
if (ADDITIONAL_INCLUDE_DIRS)
- message(STATUS "StoRM - Using additional include directories ${ADDITIONAL_INCLUDE_DIRS}")
+ message(STATUS "storm - Using additional include directories ${ADDITIONAL_INCLUDE_DIRS}")
include_directories(${ADDITIONAL_INCLUDE_DIRS})
endif(ADDITIONAL_INCLUDE_DIRS)
if (ADDITIONAL_LINK_DIRS)
- message(STATUS "StoRM - Using additional link directories ${ADDITIONAL_LINK_DIRS}")
+ message(STATUS "storm - Using additional link directories ${ADDITIONAL_LINK_DIRS}")
link_directories(${ADDITIONAL_LINK_DIRS})
endif(ADDITIONAL_LINK_DIRS)
@@ -68,5 +68,6 @@ add_custom_target(copy_storm_headers DEPENDS ${STORM_OUTPUT_HEADERS} ${STORM_LIB
add_dependencies(storm copy_storm_headers)
add_dependencies(storm copy_resources_headers)
-# install command
-install(TARGETS storm-main storm RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
\ No newline at end of file
+# installation
+install(TARGETS storm RUNTIME DESTINATION bin LIBRARY DESTINATION lib)
+install(TARGETS storm-main RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
index 3c6789324..ce2bd80c1 100644
--- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
+++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
@@ -324,7 +324,7 @@ namespace storm {
template <typename ValueType, typename RewardModelType>
bool ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::checkStormHeadersAvailable() const {
bool result = true;
- std::string problem = "Unable to compile program using Storm headers. Is Storm's include directory '" + stormIncludeDirectory + "' set correctly? Does the directory contain all the headers (in particular 'storm-config.h'?";
+ std::string problem = "Unable to compile program using storm headers. Is storm's include directory '" + stormIncludeDirectory + "' set correctly? Does the directory contain all the headers (in particular 'storm-config.h')?";
try {
std::string program = R"(
#include "storm/builder/RewardModelInformation.h"
diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index c5fb7ef8b..efdb54d42 100644
--- a/src/storm/cli/cli.cpp
+++ b/src/storm/cli/cli.cpp
@@ -47,92 +47,95 @@ namespace storm {
char temp[512];
return (GetCurrentDir(temp, 512 - 1) ? std::string(temp) : std::string(""));
}
-
- void printHeader(const std::string name, const int argc, const char* argv[]) {
- std::cout << name << std::endl;
- std::cout << "---------------" << std::endl << std::endl;
-
-
- std::cout << storm::utility::StormVersion::longVersionString() << std::endl;
+
+ void printHeader(std::string const& name, const int argc, const char* argv[]) {
+ STORM_PRINT(name << " " << storm::utility::StormVersion::shortVersionString() << std::endl << std::endl);
+
+ // "Compute" the command line argument string with which storm was invoked.
+ std::stringstream commandStream;
+ for (int i = 1; i < argc; ++i) {
+ commandStream << argv[i] << " ";
+ }
+
+ std::string command = commandStream.str();
+
+ if (!command.empty()) {
+ STORM_PRINT("Command line arguments: " << commandStream.str() << std::endl);
+ STORM_PRINT("Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl);
+ }
+ }
+
+ void printVersion(std::string const& name) {
+ STORM_PRINT(storm::utility::StormVersion::longVersionString() << std::endl);
+ STORM_PRINT(storm::utility::StormVersion::buildInfo() << std::endl);
+
#ifdef STORM_HAVE_INTELTBB
- std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl;
+ STORM_PRINT("Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl);
#endif
#ifdef STORM_HAVE_GLPK
- std::cout << "Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl;
+ STORM_PRINT("Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl);
#endif
#ifdef STORM_HAVE_GUROBI
- std::cout << "Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl;
+ STORM_PRINT("Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl);
#endif
#ifdef STORM_HAVE_Z3
unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber;
Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber);
- std::cout << "Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl;
+ STORM_PRINT("Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl);
#endif
#ifdef STORM_HAVE_MSAT
char* msatVersion = msat_get_version();
- std::cout << "Linked with " << msatVersion << "." << std::endl;
+ STORM_PRINT("Linked with " << msatVersion << "." << std::endl);
msat_free(msatVersion);
#endif
#ifdef STORM_HAVE_SMTRAT
- std::cout << "Linked with SMT-RAT " << SMTRAT_VERSION << "." << std::endl;
+ STORM_PRINT("Linked with SMT-RAT " << SMTRAT_VERSION << "." << std::endl);
#endif
#ifdef STORM_HAVE_CARL
- std::cout << "Linked with CARL." << std::endl;
// TODO get version string
+ STORM_PRINT("Linked with CARL." << std::endl);
#endif
-
+
#ifdef STORM_HAVE_CUDA
int deviceCount = 0;
cudaError_t error_id = cudaGetDeviceCount(&deviceCount);
-
- if (error_id == cudaSuccess)
- {
- std::cout << "Compiled with CUDA support, ";
+
+ if (error_id == cudaSuccess) {
+ STORM_PRINT("Compiled with CUDA support, ");
// This function call returns 0 if there are no CUDA capable devices.
- if (deviceCount == 0)
- {
- std::cout<< "but there are no available device(s) that support CUDA." << std::endl;
- } else
- {
- std::cout << "detected " << deviceCount << " CUDA Capable device(s):" << std::endl;
+ if (deviceCount == 0){
+ STORM_PRINT("but there are no available device(s) that support CUDA." << std::endl);
+ } else {
+ STORM_PRINT("detected " << deviceCount << " CUDA capable device(s):" << std::endl);
}
-
+
int dev, driverVersion = 0, runtimeVersion = 0;
-
- for (dev = 0; dev < deviceCount; ++dev)
- {
+
+ for (dev = 0; dev < deviceCount; ++dev) {
cudaSetDevice(dev);
cudaDeviceProp deviceProp;
cudaGetDeviceProperties(&deviceProp, dev);
-
- std::cout << "CUDA Device " << dev << ": \"" << deviceProp.name << "\"" << std::endl;
-
+
+ STORM_PRINT("CUDA device " << dev << ": \"" << deviceProp.name << "\"" << std::endl);
+
// Console log
cudaDriverGetVersion(&driverVersion);
cudaRuntimeGetVersion(&runtimeVersion);
- std::cout << " CUDA Driver Version / Runtime Version " << driverVersion / 1000 << "." << (driverVersion % 100) / 10 << " / " << runtimeVersion / 1000 << "." << (runtimeVersion % 100) / 10 << std::endl;
- std::cout << " CUDA Capability Major/Minor version number: " << deviceProp.major<<"."<<deviceProp.minor <<std::endl;
+ STORM_PRINT(" CUDA Driver Version / Runtime Version " << driverVersion / 1000 << "." << (driverVersion % 100) / 10 << " / " << runtimeVersion / 1000 << "." << (runtimeVersion % 100) / 10 << std::endl);
+ STORM_PRINT(" CUDA Capability Major/Minor version number: " << deviceProp.major << "." << deviceProp.minor << std::endl);
}
- std::cout << std::endl;
+ STORM_PRINT(std::endl);
}
else {
- std::cout << "Compiled with CUDA support, but an error occured trying to find CUDA devices." << std::endl;
+ STORM_PRINT("Compiled with CUDA support, but an error occured trying to find CUDA devices." << std::endl);
}
#endif
-
- // "Compute" the command line argument string with which STORM was invoked.
- std::stringstream commandStream;
- for (int i = 1; i < argc; ++i) {
- commandStream << argv[i] << " ";
- }
- std::cout << "Command line arguments: " << commandStream.str() << std::endl;
- std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl;
}
-
+
void showTimeAndMemoryStatistics(uint64_t wallclockMilliseconds) {
struct rusage ru;
getrusage(RUSAGE_SELF, &ru);
-
+
std::cout << std::endl << "Performance statistics:" << std::endl;
#ifdef MACOS
// For Mac OS, this is returned in bytes.
@@ -148,7 +151,7 @@ namespace storm {
std::cout << " * wallclock time: " << (wallclockMilliseconds/1000) << "." << std::setw(3) << std::setfill('0') << (wallclockMilliseconds % 1000) << "s" << std::endl;
}
}
-
+
bool parseOptions(const int argc, const char* argv[]) {
try {
storm::settings::mutableManager().setFromCommandLine(argc, argv);
@@ -172,7 +175,7 @@ namespace storm {
}
if (general.isVersionSet()) {
- storm::settings::manager().printVersion();
+ printVersion("storm");
return false;
}
@@ -183,20 +186,20 @@ namespace storm {
storm::utility::setLogLevel(l3pp::LogLevel::DEBUG);
}
if (debug.isTraceSet()) {
- storm::utility::setLogLevel(l3pp::LogLevel::TRACE);
+ storm::utility::setLogLevel(l3pp::LogLevel::TRACE);
}
if (debug.isLogfileSet()) {
storm::utility::initializeFileLogging();
}
return true;
}
-
+
void processOptions() {
STORM_LOG_TRACE("Processing options.");
if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isLogfileSet()) {
storm::utility::initializeFileLogging();
}
-
+
boost::optional<std::set<std::string>> propertyFilter;
std::string propertyFilterString = storm::settings::getModule<storm::settings::modules::IOSettings>().getPropertyFilter();
if (propertyFilterString != "all") {
@@ -242,7 +245,7 @@ namespace storm {
// Get the string that assigns values to the unknown currently undefined constants in the model and formula.
std::string constantDefinitionString = ioSettings.getConstantDefinitionString();
std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
-
+
// Then proceed to parsing the properties (if given), since the model we are building may depend on the property.
STORM_LOG_TRACE("Parsing properties.");
if (ioSettings.isPropertySet()) {
@@ -293,19 +296,19 @@ namespace storm {
}
} else if (ioSettings.isExplicitSet()) {
STORM_LOG_THROW(coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Only the sparse engine supports explicit model input.");
-
+
// If the model is given in an explicit format, we parse the properties without allowing expressions
// in formulas.
std::vector<storm::jani::Property> properties;
if (ioSettings.isPropertySet()) {
properties = storm::parsePropertiesForExplicit(ioSettings.getProperty(), propertyFilter);
}
-
+
buildAndCheckExplicitModel<double>(properties, true);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}
}
-
+
}
}
diff --git a/src/storm/cli/cli.h b/src/storm/cli/cli.h
index f48d53f23..3fd41e914 100644
--- a/src/storm/cli/cli.h
+++ b/src/storm/cli/cli.h
@@ -8,7 +8,9 @@ namespace storm {
std::string getCurrentWorkingDirectory();
- void printHeader(std::string name, const int argc, const char* argv[]);
+ void printHeader(std::string const& name, const int argc, const char* argv[]);
+
+ void printVersion(std::string const& name);
void showTimeAndMemoryStatistics(uint64_t wallclockMilliseconds = 0);
diff --git a/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h b/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h
index e30aade7b..6359d04a6 100644
--- a/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h
+++ b/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h
@@ -1745,7 +1745,7 @@ namespace storm {
return commandSet;
#else
- throw storm::exceptions::NotImplementedException() << "This functionality is unavailable since StoRM has been compiled without support for Z3.";
+ throw storm::exceptions::NotImplementedException() << "This functionality is unavailable since storm has been compiled without support for Z3.";
#endif
}
@@ -1801,7 +1801,7 @@ namespace storm {
std::cout << std::endl << "-------------------------------------------" << std::endl;
#else
- throw storm::exceptions::NotImplementedException() << "This functionality is unavailable since StoRM has been compiled without support for Z3.";
+ throw storm::exceptions::NotImplementedException() << "This functionality is unavailable since storm has been compiled without support for Z3.";
#endif
}
diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp
index efe033d08..624260887 100644
--- a/src/storm/parser/JaniParser.cpp
+++ b/src/storm/parser/JaniParser.cpp
@@ -245,12 +245,12 @@ namespace storm {
}
}
}
- STORM_LOG_THROW(!(accTime && accSteps), storm::exceptions::NotSupportedException, "Storm does not allow to accumulate over both time and steps");
+ STORM_LOG_THROW(!(accTime && accSteps), storm::exceptions::NotSupportedException, "storm does not allow to accumulate over both time and steps");
if (propertyStructure.count("step-instant") > 0) {
storm::expressions::Expression stepInstantExpr = parseExpression(propertyStructure.at("step-instant"), "Step instant in " + context);
- STORM_LOG_THROW(!stepInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "Storm only allows constant step-instants");
+ STORM_LOG_THROW(!stepInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "storm only allows constant step-instants");
int64_t stepInstant = stepInstantExpr.evaluateAsInt();
STORM_LOG_THROW(stepInstant >= 0, storm::exceptions::InvalidJaniException, "Only non-negative step-instants are allowed");
if(!accTime && !accSteps) {
@@ -270,7 +270,7 @@ namespace storm {
}
} else if (propertyStructure.count("time-instant") > 0) {
storm::expressions::Expression timeInstantExpr = parseExpression(propertyStructure.at("time-instant"), "time instant in " + context);
- STORM_LOG_THROW(!timeInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "Storm only allows constant time-instants");
+ STORM_LOG_THROW(!timeInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "storm only allows constant time-instants");
double timeInstant = timeInstantExpr.evaluateAsDouble();
STORM_LOG_THROW(timeInstant >= 0, storm::exceptions::InvalidJaniException, "Only non-negative time-instants are allowed");
if(!accTime && !accSteps) {
@@ -292,7 +292,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Instant/Cumul. Reward for reward constraints not supported currently.");
}
- //STORM_LOG_THROW(!accTime && !accSteps, storm::exceptions::NotSupportedException, "Storm only allows accumulation if a step- or time-bound is given.");
+ //STORM_LOG_THROW(!accTime && !accSteps, storm::exceptions::NotSupportedException, "storm only allows accumulation if a step- or time-bound is given.");
if (rewExpr.isVariable()) {
std::string rewardName = rewExpr.getVariables().begin()->getName();
@@ -336,9 +336,9 @@ namespace storm {
}
if (propertyStructure.count("step-bounds") > 0) {
storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("step-bounds"));
- STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports step-bounded until with an upper bound");
+ STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "storm only supports step-bounded until with an upper bound");
if(pi.hasLowerBound()) {
- STORM_LOG_THROW(pi.lowerBound.evaluateAsInt() == 0, storm::exceptions::NotSupportedException, "Storm only supports step-bounded until without a (non-trivial) lower-bound");
+ STORM_LOG_THROW(pi.lowerBound.evaluateAsInt() == 0, storm::exceptions::NotSupportedException, "storm only supports step-bounded until without a (non-trivial) lower-bound");
}
int64_t upperBound = pi.upperBound.evaluateAsInt();
if(pi.upperBoundStrict) {
@@ -348,7 +348,7 @@ namespace storm {
return std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundType::Steps);
} else if (propertyStructure.count("time-bounds") > 0) {
storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("time-bounds"));
- STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound.");
+ STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "storm only supports time-bounded until with an upper bound.");
double lowerBound = 0.0;
if(pi.hasLowerBound()) {
lowerBound = pi.lowerBound.evaluateAsDouble();
@@ -359,7 +359,7 @@ namespace storm {
return std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundType::Time);
} else if (propertyStructure.count("reward-bounds") > 0 ) {
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by Storm");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by storm");
}
if (args[0]->isTrueFormula()) {
return std::make_shared<storm::logic::EventuallyFormula const>(args[1], storm::logic::FormulaContext::Reward);
@@ -372,9 +372,9 @@ namespace storm {
if (propertyStructure.count("step-bounds") > 0) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Globally and step-bounds are not supported currently");
} else if (propertyStructure.count("time-bounds") > 0) {
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Globally and time bounds are not supported by Storm");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Globally and time bounds are not supported by storm");
} else if (propertyStructure.count("reward-bounds") > 0 ) {
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by Storm");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by storm");
}
return std::make_shared<storm::logic::GloballyFormula const>(args[1]);
diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp
index b5db92f3d..8fefca91c 100644
--- a/src/storm/settings/SettingsManager.cpp
+++ b/src/storm/settings/SettingsManager.cpp
@@ -257,11 +257,6 @@ namespace storm {
STORM_PRINT(std::endl);
}
- void SettingsManager::printVersion() const {
- STORM_PRINT(storm::utility::StormVersion::shortVersionString());
- STORM_PRINT(std::endl);
- }
-
uint_fast64_t SettingsManager::getPrintLengthOfLongestOption() const {
uint_fast64_t length = 0;
for (auto const& moduleName : this->moduleNames) {
diff --git a/src/storm/settings/SettingsManager.h b/src/storm/settings/SettingsManager.h
index 1ae89382e..201e7f896 100644
--- a/src/storm/settings/SettingsManager.h
+++ b/src/storm/settings/SettingsManager.h
@@ -80,11 +80,6 @@ namespace storm {
* @param maxLength The maximal length of an option name (necessary for proper alignment).
*/
void printHelpForModule(std::string const& moduleName, uint_fast64_t maxLength = 30) const;
-
- /*!
- * This function prints the version string to the command line.
- */
- void printVersion() const;
/*!
* Retrieves the only existing instance of a settings manager.
diff --git a/src/storm/settings/modules/JitBuilderSettings.cpp b/src/storm/settings/modules/JitBuilderSettings.cpp
index 2944ccee3..127434055 100644
--- a/src/storm/settings/modules/JitBuilderSettings.cpp
+++ b/src/storm/settings/modules/JitBuilderSettings.cpp
@@ -25,8 +25,8 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, doctorOptionName, false, "Show debugging information on why the jit-based model builder is not working on your system.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, compilerOptionName, false, "The compiler in the jit-based model builder.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the executable. Defaults to c++.").setDefaultValueString("c++").build()).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, stormIncludeDirectoryOptionName, false, "The include directory of Storm.")
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory that contains the headers of Storm.").build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, stormIncludeDirectoryOptionName, false, "The include directory of storm.")
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory that contains the headers of storm.").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, boostIncludeDirectoryOptionName, false, "The include directory of boost.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory containing the boost headers version >= 1.61.").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, carlIncludeDirectoryOptionName, false, "The include directory of carl.")
diff --git a/src/storm/solver/GlpkLpSolver.h b/src/storm/solver/GlpkLpSolver.h
index 35f94953a..63be0ede7 100644
--- a/src/storm/solver/GlpkLpSolver.h
+++ b/src/storm/solver/GlpkLpSolver.h
@@ -134,103 +134,103 @@ namespace storm {
class GlpkLpSolver : public LpSolver {
public:
GlpkLpSolver(std::string const& name, OptimizationDirection const& modelSense) {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
GlpkLpSolver(std::string const& name) : LpSolver(MINIMIZE) {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
GlpkLpSolver(OptimizationDirection const& modelSense) : LpSolver(modelSense) {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
GlpkLpSolver() : LpSolver(MINIMIZE) {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual ~GlpkLpSolver() {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual storm::expressions::Variable addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual void update() const override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual void addConstraint(std::string const& name, storm::expressions::Expression const& constraint) override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual void optimize() const override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual bool isInfeasible() const override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual bool isUnbounded() const override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual bool isOptimal() const override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual double getContinuousValue(storm::expressions::Variable const& variable) const override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual bool getBinaryValue(storm::expressions::Variable const& variable) const override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual double getObjectiveValue() const override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual void writeModelToFile(std::string const& filename) const override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
};
#endif
diff --git a/src/storm/solver/GurobiLpSolver.cpp b/src/storm/solver/GurobiLpSolver.cpp
index 2754cc292..d624f2cfb 100644
--- a/src/storm/solver/GurobiLpSolver.cpp
+++ b/src/storm/solver/GurobiLpSolver.cpp
@@ -357,19 +357,19 @@ namespace storm {
}
#else
GurobiLpSolver::GurobiLpSolver(std::string const&, OptimizationDirection const&) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
GurobiLpSolver::GurobiLpSolver(std::string const&) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
GurobiLpSolver::GurobiLpSolver(OptimizationDirection const&) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
GurobiLpSolver::GurobiLpSolver() {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
GurobiLpSolver::~GurobiLpSolver() {
@@ -377,86 +377,86 @@ namespace storm {
}
storm::expressions::Variable GurobiLpSolver::addBoundedContinuousVariable(std::string const&, double, double, double) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
storm::expressions::Variable GurobiLpSolver::addLowerBoundedContinuousVariable(std::string const&, double, double ) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; }
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; }
storm::expressions::Variable GurobiLpSolver::addUpperBoundedContinuousVariable(std::string const&, double, double ) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
storm::expressions::Variable GurobiLpSolver::addUnboundedContinuousVariable(std::string const&, double ) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
storm::expressions::Variable GurobiLpSolver::addBoundedIntegerVariable(std::string const&, double, double, double) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
storm::expressions::Variable GurobiLpSolver::addLowerBoundedIntegerVariable(std::string const&, double, double) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
storm::expressions::Variable GurobiLpSolver::addUpperBoundedIntegerVariable(std::string const&, double, double) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
storm::expressions::Variable GurobiLpSolver::addUnboundedIntegerVariable(std::string const&, double) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
storm::expressions::Variable GurobiLpSolver::addBinaryVariable(std::string const&, double) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
void GurobiLpSolver::update() const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
void GurobiLpSolver::addConstraint(std::string const&, storm::expressions::Expression const&) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
void GurobiLpSolver::optimize() const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
bool GurobiLpSolver::isInfeasible() const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
bool GurobiLpSolver::isUnbounded() const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
bool GurobiLpSolver::isOptimal() const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
double GurobiLpSolver::getContinuousValue(storm::expressions::Variable const&) const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
int_fast64_t GurobiLpSolver::getIntegerValue(storm::expressions::Variable const&) const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
bool GurobiLpSolver::getBinaryValue(storm::expressions::Variable const&) const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
double GurobiLpSolver::getObjectiveValue() const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
void GurobiLpSolver::writeModelToFile(std::string const&) const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
void GurobiLpSolver::toggleOutput(bool) const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
#endif
diff --git a/src/storm/solver/MathsatSmtSolver.cpp b/src/storm/solver/MathsatSmtSolver.cpp
index ef362e12f..d7501ad53 100644
--- a/src/storm/solver/MathsatSmtSolver.cpp
+++ b/src/storm/solver/MathsatSmtSolver.cpp
@@ -107,7 +107,7 @@ namespace storm {
#ifdef STORM_HAVE_MSAT
msat_push_backtrack_point(env);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -115,7 +115,7 @@ namespace storm {
#ifdef STORM_HAVE_MSAT
msat_pop_backtrack_point(env);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -123,7 +123,7 @@ namespace storm {
#ifdef STORM_HAVE_MSAT
SmtSolver::pop(n);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -132,7 +132,7 @@ namespace storm {
#ifdef STORM_HAVE_MSAT
msat_reset_env(env);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -141,7 +141,7 @@ namespace storm {
#ifdef STORM_HAVE_MSAT
msat_assert_formula(env, expressionAdapter->translateExpression(e));
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -162,7 +162,7 @@ namespace storm {
}
return this->lastResult;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -190,7 +190,7 @@ namespace storm {
}
return this->lastResult;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -219,7 +219,7 @@ namespace storm {
}
return this->lastResult;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
#endif
@@ -230,7 +230,7 @@ namespace storm {
STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable.");
return this->convertMathsatModelToValuation();
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -239,7 +239,7 @@ namespace storm {
STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable.");
return std::shared_ptr<SmtSolver::ModelReference>(new MathsatModelReference(this->getManager(), env, *expressionAdapter));
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -279,7 +279,7 @@ namespace storm {
this->allSat(important, [&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; });
return valuations;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -379,7 +379,7 @@ namespace storm {
this->pop();
return static_cast<uint_fast64_t>(numberOfModels);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -405,7 +405,7 @@ namespace storm {
this->pop();
return static_cast<uint_fast64_t>(numberOfModels);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -426,7 +426,7 @@ namespace storm {
return unsatAssumptions;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -440,7 +440,7 @@ namespace storm {
}
msat_set_itp_group(env, groupIter->second);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -462,7 +462,7 @@ namespace storm {
return this->expressionAdapter->translateExpression(interpolant);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
}
diff --git a/src/storm/solver/NativeLinearEquationSolver.h b/src/storm/solver/NativeLinearEquationSolver.h
index aeb0cc807..2a978cdbc 100644
--- a/src/storm/solver/NativeLinearEquationSolver.h
+++ b/src/storm/solver/NativeLinearEquationSolver.h
@@ -38,7 +38,7 @@ namespace storm {
};
/*!
- * A class that uses Storm's native matrix operations to implement the LinearEquationSolver interface.
+ * A class that uses storm's native matrix operations to implement the LinearEquationSolver interface.
*/
template<typename ValueType>
class NativeLinearEquationSolver : public LinearEquationSolver<ValueType> {
diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
index c29b0452c..cb1cbd5f0 100644
--- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
@@ -112,8 +112,8 @@ namespace storm {
STORM_LOG_WARN("Iterative solver did not converged after " << globalIterations << " iterations.");
}
#else
- STORM_LOG_ERROR("The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!");
- throw storm::exceptions::InvalidStateException() << "The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!";
+ STORM_LOG_ERROR("The useGpu Flag of a SCC was set, but this version of storm does not support CUDA acceleration. Internal Error!");
+ throw storm::exceptions::InvalidStateException() << "The useGpu Flag of a SCC was set, but this version of storm does not support CUDA acceleration. Internal Error!";
#endif
} else {
storm::storage::BitVector fullSystem(this->A.getRowGroupCount(), true);
@@ -213,8 +213,8 @@ namespace storm {
}
globalIterations += localIterations;
#else
- STORM_LOG_ERROR("The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!");
- throw storm::exceptions::InvalidStateException() << "The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!";
+ STORM_LOG_ERROR("The useGpu Flag of a SCC was set, but this version of storm does not support CUDA acceleration. Internal Error!");
+ throw storm::exceptions::InvalidStateException() << "The useGpu Flag of a SCC was set, but this version of storm does not support CUDA acceleration. Internal Error!";
#endif
} else {
//std::cout << "WARNING: Using CPU based TopoSolver! (double)" << std::endl;
diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h
index e706d48cd..c8af93f13 100644
--- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h
+++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h
@@ -73,7 +73,7 @@ namespace storm {
#ifdef STORM_HAVE_CUDA
return basicValueIteration_mvReduce_uint64_double_minimize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without CUDA support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without CUDA support.");
#endif
}
template <>
@@ -92,7 +92,7 @@ namespace storm {
#ifdef STORM_HAVE_CUDA
return basicValueIteration_mvReduce_uint64_float_minimize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without CUDA support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without CUDA support.");
#endif
}
@@ -116,7 +116,7 @@ namespace storm {
#ifdef STORM_HAVE_CUDA
return basicValueIteration_mvReduce_uint64_double_maximize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without CUDA support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without CUDA support.");
#endif
}
template <>
@@ -135,7 +135,7 @@ namespace storm {
#ifdef STORM_HAVE_CUDA
return basicValueIteration_mvReduce_uint64_float_maximize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without CUDA support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without CUDA support.");
#endif
}
diff --git a/src/storm/solver/Z3SmtSolver.cpp b/src/storm/solver/Z3SmtSolver.cpp
index e033504ef..cb291bcb9 100644
--- a/src/storm/solver/Z3SmtSolver.cpp
+++ b/src/storm/solver/Z3SmtSolver.cpp
@@ -19,7 +19,7 @@ namespace storm {
z3::expr z3ExprValuation = model.eval(z3Expr, true);
return this->expressionAdapter.translateExpression(z3ExprValuation).isTrue();
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -30,7 +30,7 @@ namespace storm {
z3::expr z3ExprValuation = model.eval(z3Expr, true);
return this->expressionAdapter.translateExpression(z3ExprValuation).evaluateAsInt();
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -41,7 +41,7 @@ namespace storm {
z3::expr z3ExprValuation = model.eval(z3Expr, true);
return this->expressionAdapter.translateExpression(z3ExprValuation).evaluateAsDouble();
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -68,7 +68,7 @@ namespace storm {
#ifdef STORM_HAVE_Z3
this->solver->push();
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -77,7 +77,7 @@ namespace storm {
#ifdef STORM_HAVE_Z3
this->solver->pop();
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -86,7 +86,7 @@ namespace storm {
#ifdef STORM_HAVE_Z3
this->solver->pop(static_cast<unsigned int>(n));
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -95,7 +95,7 @@ namespace storm {
#ifdef STORM_HAVE_Z3
this->solver->reset();
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -104,7 +104,7 @@ namespace storm {
#ifdef STORM_HAVE_Z3
this->solver->add(expressionAdapter->translateExpression(assertion));
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -125,7 +125,7 @@ namespace storm {
}
return this->lastResult;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -152,7 +152,7 @@ namespace storm {
}
return this->lastResult;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -180,7 +180,7 @@ namespace storm {
}
return this->lastResult;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
#endif
@@ -190,7 +190,7 @@ namespace storm {
STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable.");
return this->convertZ3ModelToValuation(this->solver->get_model());
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -199,7 +199,7 @@ namespace storm {
STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable.");
return std::shared_ptr<SmtSolver::ModelReference>(new Z3ModelReference(this->getManager(), this->solver->get_model(), *this->expressionAdapter));
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -234,7 +234,7 @@ namespace storm {
this->allSat(important, static_cast<std::function<bool(storm::expressions::SimpleValuation&)>>([&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; }));
return valuations;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -276,7 +276,7 @@ namespace storm {
this->pop();
return numberOfModels;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -317,7 +317,7 @@ namespace storm {
this->pop();
return numberOfModels;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -335,7 +335,7 @@ namespace storm {
return unsatAssumptions;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -346,7 +346,7 @@ namespace storm {
solver->set(paramObject);
return true;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -357,7 +357,7 @@ namespace storm {
solver->set(paramObject);
return true;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp
index ba6a54f8a..834ce8623 100644
--- a/src/storm/storage/jani/JSONExporter.cpp
+++ b/src/storm/storage/jani/JSONExporter.cpp
@@ -182,7 +182,7 @@ namespace storm {
}
boost::any FormulaToJaniJson::visit(storm::logic::CumulativeRewardFormula const&, boost::any const&) const {
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm currently does not support translating cummulative reward formulae");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm currently does not support translating cummulative reward formulae");
}
boost::any FormulaToJaniJson::visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const {
diff --git a/src/storm/storm.cpp b/src/storm/storm.cpp
index 20126f488..73c5a8a15 100644
--- a/src/storm/storm.cpp
+++ b/src/storm/storm.cpp
@@ -17,8 +17,8 @@ int main(const int argc, const char** argv) {
try {
storm::utility::Stopwatch totalTimer(true);
storm::utility::setUp();
- storm::cli::printHeader("Storm", argc, argv);
- storm::settings::initializeAll("Storm", "storm");
+ storm::cli::printHeader("storm", argc, argv);
+ storm::settings::initializeAll("storm", "storm");
bool optionsCorrect = storm::cli::parseOptions(argc, argv);
if (!optionsCorrect) {
return -1;
@@ -36,10 +36,10 @@ int main(const int argc, const char** argv) {
}
return 0;
} catch (storm::exceptions::BaseException const& exception) {
- STORM_LOG_ERROR("An exception caused Storm to terminate. The message of the exception is: " << exception.what());
+ STORM_LOG_ERROR("An exception caused storm to terminate. The message of the exception is: " << exception.what());
return 1;
} catch (std::exception const& exception) {
- STORM_LOG_ERROR("An unexpected exception occurred and caused Storm to terminate. The message of this exception is: " << exception.what());
+ STORM_LOG_ERROR("An unexpected exception occurred and caused storm to terminate. The message of this exception is: " << exception.what());
return 2;
}
}
diff --git a/src/storm/utility/ExplicitExporter.cpp b/src/storm/utility/ExplicitExporter.cpp
index 33e9bf3b3..1f40ab538 100644
--- a/src/storm/utility/ExplicitExporter.cpp
+++ b/src/storm/utility/ExplicitExporter.cpp
@@ -31,7 +31,7 @@ namespace storm {
exitRates = sparseModel->template as<storm::models::sparse::MarkovAutomaton<ValueType>>()->getExitRates();
}
- os << "// Exported by Storm" << std::endl;
+ os << "// Exported by storm" << std::endl;
os << "// Original model type: " << sparseModel->getType() << std::endl;
os << "@type: mdp" << std::endl;
os << "@parameters" << std::endl;
diff --git a/src/storm/utility/storm-version.h b/src/storm/utility/storm-version.h
index 12bad5c21..2cd72c00b 100644
--- a/src/storm/utility/storm-version.h
+++ b/src/storm/utility/storm-version.h
@@ -41,13 +41,13 @@ namespace storm {
static std::string shortVersionString() {
std::stringstream sstream;
- sstream << "Storm " << versionMajor << "." << versionMinor << "." << versionPatch;
+ sstream << versionMajor << "." << versionMinor << "." << versionPatch;
return sstream.str();
}
static std::string longVersionString() {
std::stringstream sstream;
- sstream << "version: " << versionMajor << "." << versionMinor << "." << versionPatch;
+ sstream << "Version " << versionMajor << "." << versionMinor << "." << versionPatch;
if (commitsAhead && commitsAhead.get() > 0) {
sstream << " (+" << commitsAhead.get() << " commits)";
}
@@ -57,7 +57,6 @@ namespace storm {
if (dirty && dirty.get() == 1) {
sstream << " (dirty)";
}
- sstream << "." << std::endl;
return sstream.str();
}
diff --git a/src/test/storm-test.cpp b/src/test/storm-test.cpp
index b63398a9b..a88084304 100644
--- a/src/test/storm-test.cpp
+++ b/src/test/storm-test.cpp
@@ -2,7 +2,7 @@
#include "storm/settings/SettingsManager.h"
int main(int argc, char **argv) {
- storm::settings::initializeAll("StoRM (Functional) Testing Suite", "test");
+ storm::settings::initializeAll("storm (Functional) Testing Suite", "test");
::testing::InitGoogleTest(&argc, argv);
return RUN_ALL_TESTS();
}