From 2b57211a98f8e23e93a94dc25b9ca9d03e7932f0 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 24 Mar 2020 14:51:48 +0100 Subject: [PATCH 1/2] cli: Making sure that the warning for unsupported model checking queries is only displayed in the main binary. --- src/storm-cli-utilities/cli.cpp | 4 +- src/storm-cli-utilities/model-handling.h | 51 ++++++++++++++---------- 2 files changed, 32 insertions(+), 23 deletions(-) diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp index 869fc2942..12d5771bd 100644 --- a/src/storm-cli-utilities/cli.cpp +++ b/src/storm-cli-utilities/cli.cpp @@ -256,9 +256,11 @@ namespace storm { // Preprocess the symbolic input std::tie(symbolicInput, mpi) = preprocessSymbolicInput(symbolicInput); + STORM_LOG_WARN_COND(mpi.isCompatible, "The model checking query does not seem to be supported for the selected engine. Storm will try to solve the query, but you will most likely get an error for at least one of the provided properties."); + // Export symbolic input (if requested) exportSymbolicInput(symbolicInput); - + #ifdef STORM_HAVE_CARL switch (mpi.verificationValueType) { case ModelProcessingInformation::ValueType::Parametric: diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 69af92244..0e4fe4812 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -173,6 +173,10 @@ namespace storm { // The environment used during model checking storm::Environment env; + + // A flag which is set to true, if the settings were detected to be compatible. + // If this is false, it could be that the query can not be handled. + bool isCompatible; }; void getModelProcessingInformationPortfolio(SymbolicInput const& input, ModelProcessingInformation& mpi) { @@ -261,30 +265,33 @@ namespace storm { } // Check whether these settings are compatible with the provided input. - bool incompatibleSettings = false; if (input.model) { - switch (mpi.verificationValueType) { - case ModelProcessingInformation::ValueType::Parametric: - incompatibleSettings = !storm::utility::canHandle(mpi.engine, input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties, input.model.get()); - break; - case ModelProcessingInformation::ValueType::Exact: - incompatibleSettings = !storm::utility::canHandle(mpi.engine, input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties, input.model.get()); - break; - case ModelProcessingInformation::ValueType::FinitePrecision: - incompatibleSettings = !storm::utility::canHandle(mpi.engine, input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties, input.model.get()); - break; - } - } - if (incompatibleSettings) { - if (usePortfolio) { - bool useExact = mpi.verificationValueType != ModelProcessingInformation::ValueType::FinitePrecision; - STORM_LOG_WARN("The settings picked by the portfolio engine (engine=" << mpi.engine << ", bisim=" << mpi.applyBisimulation << ", exact=" << useExact << ") are incompatible with this model. Falling back to default settings."); - mpi.engine = storm::utility::Engine::Sparse; - mpi.applyBisimulation = false; - mpi.verificationValueType = originalVerificationValueType; - } else { - STORM_LOG_WARN("The model checking query does not seem to be supported for the selected engine. Storm will try to solve the query, but you will most likely get an error for at least one of the provided properties."); + auto checkCompatibleSettings = [&mpi, &input] { + switch (mpi.verificationValueType) { + case ModelProcessingInformation::ValueType::Parametric: + return storm::utility::canHandle(mpi.engine, input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties, input.model.get()); + case ModelProcessingInformation::ValueType::Exact: + return storm::utility::canHandle(mpi.engine, input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties, input.model.get()); + break; + case ModelProcessingInformation::ValueType::FinitePrecision: + return storm::utility::canHandle(mpi.engine, input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties, input.model.get()); + } + }; + mpi.isCompatible = checkCompatibleSettings(); + if (!mpi.isCompatible) { + if (usePortfolio) { + bool useExact = mpi.verificationValueType != ModelProcessingInformation::ValueType::FinitePrecision; + STORM_LOG_WARN("The settings picked by the portfolio engine (engine=" << mpi.engine << ", bisim=" << mpi.applyBisimulation << ", exact=" << useExact << ") are incompatible with this model. Falling back to default settings."); + mpi.engine = storm::utility::Engine::Sparse; + mpi.applyBisimulation = false; + mpi.verificationValueType = originalVerificationValueType; + // Retry check with new settings + mpi.isCompatible = checkCompatibleSettings(); + } } + } else { + // If there is no input model, nothing has to be done, actually + mpi.isCompatible = true; } // Set whether a transformation to jani is required or necessary From 1187c0fca1655ac46bc6ba66daf79805421b4972 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 24 Mar 2020 15:06:44 +0100 Subject: [PATCH 2/2] Added a CMAKE option for ThinLTO --- CMakeLists.txt | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 5ef92dd45..d1b58879e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -33,6 +33,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_USE_THIN_LTO "Sets whether thin link-time optimizations are enabled (faster compile times than normal LTO)." OFF) +MARK_AS_ADVANCED(STORM_USE_THIN_LTO) option(STORM_PORTABLE "Sets whether a build needs to be portable." OFF) MARK_AS_ADVANCED(STORM_PORTABLE) # Force POPCNT is helpful for portable code targetting platforms with SSE4.2 operation support. @@ -267,7 +269,10 @@ elseif (STORM_COMPILER_GCC) set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -rdynamic") endif () -if (STORM_USE_LTO) +if (STORM_USE_THIN_LTO) + set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -flto=thin") + message(STATUS "Storm - Enabling link-time optimizations using ThinLTO.") +elseif (STORM_USE_LTO) set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -flto") # Fix for problems that occurred when using LTO on gcc. This should be removed when it