From 85e674266d045f52b5faad0dcba0344349169717 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 15 Sep 2013 19:46:34 +0200 Subject: [PATCH] Added support for linking against Gurobi to CMakeLists.txt. Prepared work on the generator of minimal label sets. Former-commit-id: a7a87edcfeeecf9a7528d38502b71038e552fe0d --- CMakeLists.txt | 27 +++++++++- .../MinimalLabelSetGenerator.h | 52 +++++++++++++++++++ src/storm.cpp | 7 ++- 3 files changed, 82 insertions(+), 4 deletions(-) create mode 100644 src/counterexamples/MinimalLabelSetGenerator.h diff --git a/CMakeLists.txt b/CMakeLists.txt index 8ddbdc224..4721fc050 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -68,7 +68,8 @@ option(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_INTELTBB "Sets whether the Intel TBB Extensions should be used." OFF) option(STORM_USE_COTIRE "Sets whether Cotire should be used (for building precompiled headers)." OFF) -option(LINK_LIBCXXABI "Sets whether libc++abi should be linked" OFF) +option(LINK_LIBCXXABI "Sets whether libc++abi should be linked." OFF) +set(GUROBI_ROOT "" CACHE STRING "The root directory of Gurobi (if available).") 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(CUSTOM_BOOST_ROOT "" CACHE STRING "A custom path to the Boost root directory.") @@ -82,6 +83,12 @@ else() message(STATUS "Building RELEASE version.") endif() +if ("${GUROBI_ROOT}" STREQUAL "") + set(ENABLE_GUROBI OFF) +else() + set(ENABLE_GUROBI ON) +endif() + message(STATUS "CMAKE_BUILD_TYPE: ${CMAKE_BUILD_TYPE}") message(STATUS "CMAKE_BUILD_TYPE (ENV): $ENV{CMAKE_BUILD_TYPE}") @@ -157,6 +164,7 @@ file(GLOB_RECURSE STORM_FORMULA_CSL_FILES ${PROJECT_SOURCE_DIR}/src/formula/Csl/ file(GLOB_RECURSE STORM_FORMULA_LTL_FILES ${PROJECT_SOURCE_DIR}/src/formula/Ltl/*.h ${PROJECT_SOURCE_DIR}/src/formula/Ltl/*.cpp) file(GLOB_RECURSE STORM_FORMULA_PRCTL_FILES ${PROJECT_SOURCE_DIR}/src/formula/Prctl/*.h ${PROJECT_SOURCE_DIR}/src/formula/Prctl/*.cpp) file(GLOB_RECURSE STORM_MODELCHECKER_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/*.cpp) +file(GLOB_RECURSE STORM_COUNTEREXAMPLES_FILES ${PROJECT_SOURCE_DIR}/src/counterexamples/*.h ${PROJECT_SOURCE_DIR}/src/counterexamples/*.cpp) file(GLOB_RECURSE STORM_MODELS_FILES ${PROJECT_SOURCE_DIR}/src/models/*.h ${PROJECT_SOURCE_DIR}/src/models/*.cpp) file(GLOB STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOURCE_DIR}/src/parser/*.cpp) file(GLOB_RECURSE STORM_PARSER_PRISMPARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.h ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.cpp) @@ -182,6 +190,7 @@ source_group(formula\\csl FILES ${STORM_FORMULA_CSL_FILES}) source_group(formula\\ltl FILES ${STORM_FORMULA_LTL_FILES}) source_group(formula\\prctl FILES ${STORM_FORMULA_PRCTL_FILES}) source_group(modelchecker FILES ${STORM_MODELCHECKER_FILES}) +source_group(counterexamples FILES ${STORM_COUNTEREXAMPLES_FILES}) source_group(models FILES ${STORM_MODELS_FILES}) source_group(parser FILES ${STORM_PARSER_FILES}) source_group(parser\\prismparser FILES ${STORM_PARSER_PRISMPARSER_FILES}) @@ -279,6 +288,12 @@ if (LTL2DSTAR_LIBRARY_DIRS) link_directories(${LTL2DSTAR_LIBRARY_DIRS}) endif(LTL2DSTAR_LIBRARY_DIRS) +if (ENABLE_GUROBI) + include_directories(${GUROBI_ROOT}/include) + link_directories(${GUROBI_ROOT}/lib) + message (STATUS "Adding ${GUROBI_ROOT}/include and ${GUROBI_ROOT}/lib to include/linking directories.") +endif(ENABLE_GUROBI) + # Add the executables # Must be created *after* Boost was added because of LINK_DIRECTORIES add_executable(storm ${STORM_SOURCES} ${STORM_HEADERS}) @@ -325,7 +340,15 @@ if (STORM_USE_COTIRE) #cotire(storm-functional-tests) #cotire(storm-performance-tests) endif() - + +if (ENABLE_GUROBI) + message (STATUS "Linking in Gurobi.") + target_link_libraries(storm "gurobi55") + target_link_libraries(storm-functional-tests "gurobi55") + target_link_libraries(storm-performance-tests "gurobi55") + add_definitions(-DHAVE_GUROBI) +endif(ENABLE_GUROBI) + # Link against libc++abi if requested. May be needed to build on Linux systems using clang. if (LINK_LIBCXXABI) message (STATUS "Linking against libc++abi.") diff --git a/src/counterexamples/MinimalLabelSetGenerator.h b/src/counterexamples/MinimalLabelSetGenerator.h new file mode 100644 index 000000000..a827b5635 --- /dev/null +++ b/src/counterexamples/MinimalLabelSetGenerator.h @@ -0,0 +1,52 @@ +/* + * MinimalLabelSetGenerator.h + * + * Created on: 15.09.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_COUNTEREXAMPLES_MINIMALCOMMANDSETGENERATOR_MDP_H_ +#define STORM_COUNTEREXAMPLES_MINIMALCOMMANDSETGENERATOR_MDP_H_ + +#ifdef HAVE_GUROBI +#include +#endif + +#include "src/models/Mdp.h" +#include "src/exceptions/NotImplementedException.h" +#include "src/storage/SparseMatrix.h" +#include "src/storage/BitVector.h" + +namespace storm { + namespace counterexamples { + + /*! + * This class provides functionality to generate a minimal counterexample to a probabilistic reachability + * property in terms of used labels. + */ + template + class MinimalLabelSetGenerator { + + static std::unordered_set getMinimalLabelSet(storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, T lowerProbabilityBound, bool checkThresholdFeasible = false) { +#ifdef HAVE_GUROBI + // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. + // (2) Identify relevant labels and states. + // (3) Encode resulting system as MILP problem. + // (3.1) Initialize MILP solver. + // (3.2) Create variables. + // (3.3) Construct objective function. + // (3.4) Construct constraint system. + // (4) Read off result from MILP variables. + // (5) Potentially verify whether the resulting system exceeds the given threshold. + // (6) Return result. +#else + throw storm::exceptions::NotImplementedException() << "This functionality is unavailable if StoRM is compiled without support for Gurobi."; +#endif + } + + }; + + } +} + +#endif /* STORM_COUNTEREXAMPLES_MINIMALLABELSETGENERATOR_MDP_H_ */ diff --git a/src/storm.cpp b/src/storm.cpp index 3ec2bba2a..537c52d5e 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -26,13 +26,16 @@ #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/solver/GmmxxLinearEquationSolver.h" #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" +#include "src/counterexamples/MinimalLabelSetGenerator.h" #include "src/parser/AutoParser.h" #include "src/parser/PrctlParser.h" -#include "src/settings/Settings.h" -#include "src/utility/StormOptions.h" // Registers all standard options #include "src/utility/ErrorHandling.h" #include "src/formula/Prctl.h" +#include "src/settings/Settings.h" +// Registers all standard options +#include "src/utility/StormOptions.h" + #include "src/parser/PrctlFileParser.h" #include "src/parser/LtlFileParser.h"