From f219437acfb852b993e0dd42b68ba1f71c66a52d Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 26 Aug 2015 16:44:00 +0200 Subject: [PATCH] Faster compilation times! Former-commit-id: a8dc8fa612af10bb22a9200651e9a1bb466b3c61 --- CMakeLists.txt | 12 +++++-- src/{utility => cli}/cli.cpp | 11 +++--- src/cli/cli.h | 29 +++++++++++++++ .../prctl/HybridMdpPrctlModelChecker.cpp | 1 + .../prctl/HybridMdpPrctlModelChecker.h | 9 +++-- .../SparsePropositionalModelChecker.h | 1 - .../SymbolicPropositionalModelChecker.h | 10 +++++- src/models/ModelBase.h | 1 - src/models/sparse/Dtmc.h | 1 - src/models/sparse/Model.h | 5 ++- src/models/symbolic/Model.cpp | 1 + ...erministicModelBisimulationDecomposition.h | 1 + src/storm.cpp | 10 +++--- src/utility/{cli.h => storm.h} | 36 +++++-------------- .../GmmxxHybridMdpPrctlModelCheckerTest.cpp | 1 + 15 files changed, 82 insertions(+), 47 deletions(-) rename src/{utility => cli}/cli.cpp (98%) create mode 100644 src/cli/cli.h rename src/utility/{cli.h => storm.h} (96%) diff --git a/CMakeLists.txt b/CMakeLists.txt index ef0a82022..41d058a4b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -371,10 +371,11 @@ endif() ############################################################# file(GLOB_RECURSE STORM_HEADERS ${PROJECT_SOURCE_DIR}/src/*.h) file(GLOB_RECURSE STORM_SOURCES_WITHOUT_MAIN ${PROJECT_SOURCE_DIR}/src/*/*.cpp) +file(GLOB_RECURSE STORM_SOURCES_CLI ${PROJECT_SOURCE_DIR}/src/cli/*.cpp) file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm.cpp) -set(STORM_SOURCES "${STORM_SOURCES_WITHOUT_MAIN};${STORM_MAIN_FILE};") file(GLOB_RECURSE STORM_ADAPTERS_FILES ${PROJECT_SOURCE_DIR}/src/adapters/*.h ${PROJECT_SOURCE_DIR}/src/adapters/*.cpp) file(GLOB_RECURSE STORM_BUILDER_FILES ${PROJECT_SOURCE_DIR}/src/builder/*.h ${PROJECT_SOURCE_DIR}/src/builder/*.cpp) +file(GLOB_RECURSE STORM_CLI_FILES ${PROJECT_SOURCE_DIR}/src/cli/*.h ${PROJECT_SOURCE_DIR}/src/cli/*.cpp) file(GLOB_RECURSE STORM_EXCEPTIONS_FILES ${PROJECT_SOURCE_DIR}/src/exceptions/*.h ${PROJECT_SOURCE_DIR}/src/exceptions/*.cpp) file(GLOB_RECURSE STORM_LOGIC_FILES ${PROJECT_SOURCE_DIR}/src/logic/*.h ${PROJECT_SOURCE_DIR}/src/logic/*.cpp) file(GLOB STORM_MODELCHECKER_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/*.cpp) @@ -410,10 +411,15 @@ file(GLOB_RECURSE STORM_PERFORMANCE_TEST_FILES ${STORM_CPP_TESTS_BASE_PATH}/perf # Additional include files like the storm-config.h file(GLOB_RECURSE STORM_BUILD_HEADERS ${PROJECT_BINARY_DIR}/include/*.h) +set(STORM_LIB_SOURCES ${STORM_SOURCES_WITHOUT_MAIN}) +list(REMOVE_ITEM STORM_LIB_SOURCES ${STORM_SOURCES_CLI}) +set(STORM_MAIN_SOURCES ${STORM_SOURCES_CLI} ${STORM_MAIN_FILE}) + # Group the headers and sources source_group(main FILES ${STORM_MAIN_FILE}) source_group(adapters FILES ${STORM_ADAPTERS_FILES}) source_group(builder FILES ${STORM_BUILDER_FILES}) +source_group(cli FILES ${STORM_CLI_FILES}) source_group(exceptions FILES ${STORM_EXCEPTIONS_FILES}) source_group(logic FILES ${STORM_LOGIC_FILES}) source_group(generated FILES ${STORM_BUILD_HEADERS} ${STORM_BUILD_SOURCES}) @@ -492,8 +498,8 @@ endif() ## All link_directories() calls MUST be made before this point # ## # ############################################################################### -add_library(storm ${STORM_SOURCES_WITHOUT_MAIN} ${STORM_HEADERS}) -add_executable(storm-main ${STORM_MAIN_FILE}) +add_library(storm ${STORM_LIB_SOURCES}) +add_executable(storm-main ${STORM_MAIN_SOURCES}) target_link_libraries(storm-main storm) set_target_properties(storm-main PROPERTIES OUTPUT_NAME "storm") add_executable(storm-functional-tests ${STORM_FUNCTIONAL_TEST_MAIN_FILE} ${STORM_FUNCTIONAL_TEST_FILES}) diff --git a/src/utility/cli.cpp b/src/cli/cli.cpp similarity index 98% rename from src/utility/cli.cpp rename to src/cli/cli.cpp index 219e566ae..6198db9f3 100644 --- a/src/utility/cli.cpp +++ b/src/cli/cli.cpp @@ -1,9 +1,12 @@ #include "cli.h" +#include "../utility/storm.h" #include "src/settings/modules/DebugSettings.h" #include "src/exceptions/OptionParserException.h" +#include "src/utility/storm-version.h" + // Includes for the linked libraries and versions header. #ifdef STORM_HAVE_INTELTBB # include "tbb/tbb_stddef.h" @@ -30,7 +33,6 @@ #endif namespace storm { - namespace utility { namespace cli { std::string getCurrentWorkingDirectory() { char temp[512]; @@ -196,14 +198,14 @@ namespace storm { LOG4CPLUS_INFO(logger, "Enabled trace mode, log output gets printed to console."); } if (storm::settings::debugSettings().isLogfileSet()) { - initializeFileLogging(); + storm::utility::initializeFileLogging(); } return true; } void processOptions() { if (storm::settings::debugSettings().isLogfileSet()) { - initializeFileLogging(); + storm::utility::initializeFileLogging(); } storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); @@ -253,5 +255,4 @@ namespace storm { } } - } -} \ No newline at end of file + } \ No newline at end of file diff --git a/src/cli/cli.h b/src/cli/cli.h new file mode 100644 index 000000000..896b7bee2 --- /dev/null +++ b/src/cli/cli.h @@ -0,0 +1,29 @@ +#ifndef STORM_UTILITY_CLI_H_ +#define STORM_UTILITY_CLI_H_ + +#include + +namespace storm { + namespace cli { + + std::string getCurrentWorkingDirectory(); + + void printHeader(const int argc, const char* argv[]); + + void printUsage(); + + /*! + * Parses the given command line arguments. + * + * @param argc The argc argument of main(). + * @param argv The argv argument of main(). + * @return True iff the program should continue to run after parsing the options. + */ + bool parseOptions(const int argc, const char* argv[]); + + + void processOptions(); + } +} + +#endif diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index 8aa20c54f..762c8126d 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -4,6 +4,7 @@ #include "src/storage/dd/CuddOdd.h" +#include "src/models/symbolic/Mdp.h" #include "src/models/symbolic/StandardRewardModel.h" #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h index bf5a7a48a..03838e6c0 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.h @@ -3,11 +3,16 @@ #include "src/modelchecker/propositional/SymbolicPropositionalModelChecker.h" -#include "src/models/symbolic/Mdp.h" - #include "src/utility/solver.h" +#include "src/storage/dd/DdType.h" namespace storm { + namespace models { + namespace symbolic { + template class Mdp; + } + } + namespace modelchecker { template class HybridMdpPrctlModelChecker : public SymbolicPropositionalModelChecker { diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.h b/src/modelchecker/propositional/SparsePropositionalModelChecker.h index f24ece9ab..9565a4bc9 100644 --- a/src/modelchecker/propositional/SparsePropositionalModelChecker.h +++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.h @@ -3,7 +3,6 @@ #include "src/modelchecker/AbstractModelChecker.h" -#include "src/models/sparse/Model.h" namespace storm { namespace modelchecker { diff --git a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h index ec3433dec..03b863d6c 100644 --- a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h +++ b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h @@ -2,11 +2,19 @@ #define STORM_MODELCHECKER_SYMBOLICPROPOSITIONALMODELCHECKER_H_ #include "src/modelchecker/AbstractModelChecker.h" -#include "src/models/symbolic/Model.h" + +#include "src/storage/dd/DdType.h" namespace storm { + namespace models { + namespace symbolic { + template class Model; + } + } + namespace modelchecker { + template class SymbolicPropositionalModelChecker : public AbstractModelChecker { public: diff --git a/src/models/ModelBase.h b/src/models/ModelBase.h index 24f6d627d..4bbe31b64 100644 --- a/src/models/ModelBase.h +++ b/src/models/ModelBase.h @@ -5,7 +5,6 @@ #include "src/models/ModelType.h" #include "src/utility/macros.h" -#include "src/exceptions/InvalidOperationException.h" namespace storm { namespace models { diff --git a/src/models/sparse/Dtmc.h b/src/models/sparse/Dtmc.h index 334422dba..bf1b5c3e4 100644 --- a/src/models/sparse/Dtmc.h +++ b/src/models/sparse/Dtmc.h @@ -4,7 +4,6 @@ #include "src/models/sparse/DeterministicModel.h" #include "src/utility/OsDetection.h" -#include "src/utility/constants.h" #include "src/adapters/CarlAdapter.h" namespace storm { diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h index bf9da8713..514d2ee0c 100644 --- a/src/models/sparse/Model.h +++ b/src/models/sparse/Model.h @@ -9,11 +9,14 @@ #include "src/models/ModelBase.h" #include "src/models/sparse/StateLabeling.h" #include "src/storage/sparse/StateType.h" -#include "src/storage/BitVector.h" #include "src/storage/SparseMatrix.h" #include "src/utility/OsDetection.h" namespace storm { + namespace storage { + class BitVector; + } + namespace models { namespace sparse { diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index 7c31e3fa1..408f8af7c 100644 --- a/src/models/symbolic/Model.cpp +++ b/src/models/symbolic/Model.cpp @@ -3,6 +3,7 @@ #include #include "src/exceptions/IllegalArgumentException.h" +#include "src/exceptions/InvalidOperationException.h" #include "src/adapters/AddExpressionAdapter.h" diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h index 3b0fba916..d66591f76 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/DeterministicModelBisimulationDecomposition.h @@ -13,6 +13,7 @@ #include "src/storage/Distribution.h" #include "src/utility/constants.h" #include "src/utility/OsDetection.h" +#include "src/exceptions/InvalidOperationException.h" namespace storm { namespace utility { diff --git a/src/storm.cpp b/src/storm.cpp index 2ed0a42d3..3b060120b 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -1,22 +1,22 @@ // Include other headers. #include "src/exceptions/BaseException.h" #include "src/utility/macros.h" -#include "src/utility/cli.h" - +#include "src/cli/cli.h" +#include "src/utility/initialize.h" /*! * Main entry point of the executable storm. */ int main(const int argc, const char** argv) { try { storm::utility::setUp(); - storm::utility::cli::printHeader(argc, argv); - bool optionsCorrect = storm::utility::cli::parseOptions(argc, argv); + storm::cli::printHeader(argc, argv); + bool optionsCorrect = storm::cli::parseOptions(argc, argv); if (!optionsCorrect) { return -1; } // From this point on we are ready to carry out the actual computations. - storm::utility::cli::processOptions(); + storm::cli::processOptions(); // All operations have now been performed, so we clean up everything and terminate. storm::utility::cleanUp(); diff --git a/src/utility/cli.h b/src/utility/storm.h similarity index 96% rename from src/utility/cli.h rename to src/utility/storm.h index c28394f6d..35960d474 100644 --- a/src/utility/cli.h +++ b/src/utility/storm.h @@ -1,5 +1,6 @@ -#ifndef STORM_UTILITY_CLI_H_ -#define STORM_UTILITY_CLI_H_ + +#ifndef STORM_H +#define STORM_H #include #include @@ -15,8 +16,6 @@ // Headers that provide auxiliary functionality. -#include "src/utility/storm-version.h" -#include "src/utility/OsDetection.h" #include "src/settings/SettingsManager.h" @@ -72,25 +71,9 @@ #include "src/exceptions/NotImplementedException.h" namespace storm { - namespace utility { - namespace cli { - - std::string getCurrentWorkingDirectory(); - - void printHeader(const int argc, const char* argv[]); - - void printUsage(); - - /*! - * Parses the given command line arguments. - * - * @param argc The argc argument of main(). - * @param argv The argv argument of main(). - * @return True iff the program should continue to run after parsing the options. - */ - bool parseOptions(const int argc, const char* argv[]); - - template + + + template std::shared_ptr> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional const& stateRewardsFile = boost::optional(), boost::optional const& transitionRewardsFile = boost::optional()) { return storm::parser::AutoParser::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : ""); } @@ -411,9 +394,8 @@ namespace storm { } } - void processOptions(); - } - } + } -#endif +#endif /* STORM_H */ + diff --git a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp index c148a92d9..5be1cd015 100644 --- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -11,6 +11,7 @@ #include "src/parser/FormulaParser.h" #include "src/builder/DdPrismModelBuilder.h" #include "src/models/symbolic/Dtmc.h" +#include "src/models/symbolic/Mdp.h" #include "src/models/symbolic/StandardRewardModel.h" #include "src/settings/SettingsManager.h"