From eeb0f620ec91db8e0548e1f1ac5e5dca631453ba Mon Sep 17 00:00:00 2001 From: Mavo Date: Wed, 18 May 2016 14:16:57 +0200 Subject: [PATCH] STORM_DEVELOPER mode introduced Former-commit-id: 2749e19eab2ed0c63aea34e7f116ca2804183dc2 --- CMakeLists.txt | 12 +++++------ .../SparseDtmcEliminationModelChecker.cpp | 4 ++++ src/storage/BitVector.cpp | 20 +++++++++---------- 3 files changed, 20 insertions(+), 16 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 13ccb71fc..f2621cf4d 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -18,7 +18,7 @@ include(ExternalProject) ## CMake options of StoRM ## ############################################################# -option(STORM_DEBUG "Sets whether the DEBUG mode is used" ON) +option(STORM_DEVELOPER "Sets whether the development mode is used" OFF) option(STORM_USE_POPCNT "Sets whether the popcnt instruction is going to be used." ON) option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be linked statically." ON) option(STORM_USE_INTELTBB "Sets whether the Intel TBB libraries should be used." OFF) @@ -40,11 +40,11 @@ set(MSAT_ROOT "" CACHE STRING "The hint to the root directory of MathSAT (option set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.") set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the link directories.") -# If the DEBUG option was turned on, we will target a debug version and a release version otherwise. -if (STORM_DEBUG) - set (CMAKE_BUILD_TYPE "DEBUG") -else() - set (CMAKE_BUILD_TYPE "RELEASE") +# If the STORM_DEVELOPER option was turned on, we will target a debug version. +if (STORM_DEVELOPER) + message(STATUS "StoRM - Using development mode") + set(CMAKE_BUILD_TYPE "DEBUG" CACHE STRING "Set the build type" FORCE) + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DSTORM_DEV") endif() message(STATUS "StoRM - Building ${CMAKE_BUILD_TYPE} version.") diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 0f67cca4a..5a6045f66 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -271,7 +271,9 @@ namespace storm { while (priorityQueue->hasNextState()) { storm::storage::sparse::state_type state = priorityQueue->popNextState(); stateEliminator.eliminateState(state, true); +#ifdef STORM_DEV STORM_LOG_ASSERT(checkConsistent(flexibleMatrix, flexibleBackwardTransitions), "The forward and backward transition matrices became inconsistent."); +#endif } // Now, we set the values of all states in BSCCs to that of the representative value (and clear the @@ -903,7 +905,9 @@ namespace storm { if (removeForwardTransitions) { values[state] = storm::utility::zero(); } +#ifdef STORM_DEV STORM_LOG_ASSERT(checkConsistent(transitionMatrix, backwardTransitions), "The forward and backward transition matrices became inconsistent."); +#endif } } diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index fcbceca7b..a60b8c10c 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -12,8 +12,8 @@ #include -#ifndef NDEBUG -//#define ASSERT_BITVECTOR +#ifdef STORM_DEV +#define ASSERT_BITVECTOR #endif namespace storm { @@ -725,11 +725,11 @@ namespace storm { if (result.get(i) != get(start + i)) { STORM_LOG_ERROR("Getting of bits not correct for index " << i); STORM_LOG_ERROR("Getting from " << start << " with length " << length); - stringstream stream; + std::stringstream stream; printBits(stream); stream << std::endl; result.printBits(stream); - STORM_LOG_ERROR(stream); + STORM_LOG_ERROR(stream.str()); STORM_LOG_ASSERT(false, "Getting of bits not correct."); } } @@ -738,11 +738,11 @@ namespace storm { if (original.get(i) != get(i)) { STORM_LOG_ERROR("Getting did change bitvector at index " << i); STORM_LOG_ERROR("Getting from " << start << " with length " << length); - stringstream stream; + std::stringstream stream; printBits(stream); stream << std::endl; original.printBits(stream); - STORM_LOG_ERROR(stream); + STORM_LOG_ERROR(stream.str()); STORM_LOG_ASSERT(false, "Getting of bits not correct."); } } @@ -818,11 +818,11 @@ namespace storm { if (other.get(i) != get(start + i)) { STORM_LOG_ERROR("Setting of bits not correct for index " << i); STORM_LOG_ERROR("Setting from " << start << " with length " << other.bitCount); - stringstream stream; + std::stringstream stream; printBits(stream); stream << std::endl; other.printBits(stream); - STORM_LOG_ERROR(stream); + STORM_LOG_ERROR(stream.str()); STORM_LOG_ASSERT(false, "Setting of bits not correct."); } } @@ -831,11 +831,11 @@ namespace storm { if (original.get(i) != get(i)) { STORM_LOG_ERROR("Setting did change bitvector at index " << i); STORM_LOG_ERROR("Setting from " << start << " with length " << other.bitCount); - stringstream stream; + std::stringstream stream; printBits(stream); stream << std::endl; original.printBits(stream); - STORM_LOG_ERROR(stream); + STORM_LOG_ERROR(stream.str()); STORM_LOG_ASSERT(false, "Setting of bits not correct."); } }