Browse Source

STORM_DEVELOPER mode introduced

Former-commit-id: 2749e19eab
tempestpy_adaptions
Mavo 9 years ago
parent
commit
eeb0f620ec
  1. 12
      CMakeLists.txt
  2. 4
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
  3. 20
      src/storage/BitVector.cpp

12
CMakeLists.txt

@ -18,7 +18,7 @@ include(ExternalProject)
## CMake options of StoRM ## 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(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(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) 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_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.")
set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the link 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() endif()
message(STATUS "StoRM - Building ${CMAKE_BUILD_TYPE} version.") message(STATUS "StoRM - Building ${CMAKE_BUILD_TYPE} version.")

4
src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp

@ -271,7 +271,9 @@ namespace storm {
while (priorityQueue->hasNextState()) { while (priorityQueue->hasNextState()) {
storm::storage::sparse::state_type state = priorityQueue->popNextState(); storm::storage::sparse::state_type state = priorityQueue->popNextState();
stateEliminator.eliminateState(state, true); stateEliminator.eliminateState(state, true);
#ifdef STORM_DEV
STORM_LOG_ASSERT(checkConsistent(flexibleMatrix, flexibleBackwardTransitions), "The forward and backward transition matrices became inconsistent."); 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 // 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) { if (removeForwardTransitions) {
values[state] = storm::utility::zero<ValueType>(); values[state] = storm::utility::zero<ValueType>();
} }
#ifdef STORM_DEV
STORM_LOG_ASSERT(checkConsistent(transitionMatrix, backwardTransitions), "The forward and backward transition matrices became inconsistent."); STORM_LOG_ASSERT(checkConsistent(transitionMatrix, backwardTransitions), "The forward and backward transition matrices became inconsistent.");
#endif
} }
} }

20
src/storage/BitVector.cpp

@ -12,8 +12,8 @@
#include <bitset> #include <bitset>
#ifndef NDEBUG
//#define ASSERT_BITVECTOR
#ifdef STORM_DEV
#define ASSERT_BITVECTOR
#endif #endif
namespace storm { namespace storm {
@ -725,11 +725,11 @@ namespace storm {
if (result.get(i) != get(start + i)) { if (result.get(i) != get(start + i)) {
STORM_LOG_ERROR("Getting of bits not correct for index " << i); STORM_LOG_ERROR("Getting of bits not correct for index " << i);
STORM_LOG_ERROR("Getting from " << start << " with length " << length); STORM_LOG_ERROR("Getting from " << start << " with length " << length);
stringstream stream;
std::stringstream stream;
printBits(stream); printBits(stream);
stream << std::endl; stream << std::endl;
result.printBits(stream); result.printBits(stream);
STORM_LOG_ERROR(stream);
STORM_LOG_ERROR(stream.str());
STORM_LOG_ASSERT(false, "Getting of bits not correct."); STORM_LOG_ASSERT(false, "Getting of bits not correct.");
} }
} }
@ -738,11 +738,11 @@ namespace storm {
if (original.get(i) != get(i)) { if (original.get(i) != get(i)) {
STORM_LOG_ERROR("Getting did change bitvector at index " << i); STORM_LOG_ERROR("Getting did change bitvector at index " << i);
STORM_LOG_ERROR("Getting from " << start << " with length " << length); STORM_LOG_ERROR("Getting from " << start << " with length " << length);
stringstream stream;
std::stringstream stream;
printBits(stream); printBits(stream);
stream << std::endl; stream << std::endl;
original.printBits(stream); original.printBits(stream);
STORM_LOG_ERROR(stream);
STORM_LOG_ERROR(stream.str());
STORM_LOG_ASSERT(false, "Getting of bits not correct."); STORM_LOG_ASSERT(false, "Getting of bits not correct.");
} }
} }
@ -818,11 +818,11 @@ namespace storm {
if (other.get(i) != get(start + i)) { if (other.get(i) != get(start + i)) {
STORM_LOG_ERROR("Setting of bits not correct for index " << i); STORM_LOG_ERROR("Setting of bits not correct for index " << i);
STORM_LOG_ERROR("Setting from " << start << " with length " << other.bitCount); STORM_LOG_ERROR("Setting from " << start << " with length " << other.bitCount);
stringstream stream;
std::stringstream stream;
printBits(stream); printBits(stream);
stream << std::endl; stream << std::endl;
other.printBits(stream); other.printBits(stream);
STORM_LOG_ERROR(stream);
STORM_LOG_ERROR(stream.str());
STORM_LOG_ASSERT(false, "Setting of bits not correct."); STORM_LOG_ASSERT(false, "Setting of bits not correct.");
} }
} }
@ -831,11 +831,11 @@ namespace storm {
if (original.get(i) != get(i)) { if (original.get(i) != get(i)) {
STORM_LOG_ERROR("Setting did change bitvector at index " << i); STORM_LOG_ERROR("Setting did change bitvector at index " << i);
STORM_LOG_ERROR("Setting from " << start << " with length " << other.bitCount); STORM_LOG_ERROR("Setting from " << start << " with length " << other.bitCount);
stringstream stream;
std::stringstream stream;
printBits(stream); printBits(stream);
stream << std::endl; stream << std::endl;
original.printBits(stream); original.printBits(stream);
STORM_LOG_ERROR(stream);
STORM_LOG_ERROR(stream.str());
STORM_LOG_ASSERT(false, "Setting of bits not correct."); STORM_LOG_ASSERT(false, "Setting of bits not correct.");
} }
} }

Loading…
Cancel
Save