Browse Source

Faster compilation times!

Former-commit-id: a8dc8fa612
tempestpy_adaptions
sjunges 9 years ago
parent
commit
f219437acf
  1. 12
      CMakeLists.txt
  2. 11
      src/cli/cli.cpp
  3. 29
      src/cli/cli.h
  4. 1
      src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
  5. 9
      src/modelchecker/prctl/HybridMdpPrctlModelChecker.h
  6. 1
      src/modelchecker/propositional/SparsePropositionalModelChecker.h
  7. 10
      src/modelchecker/propositional/SymbolicPropositionalModelChecker.h
  8. 1
      src/models/ModelBase.h
  9. 1
      src/models/sparse/Dtmc.h
  10. 5
      src/models/sparse/Model.h
  11. 1
      src/models/symbolic/Model.cpp
  12. 1
      src/storage/DeterministicModelBisimulationDecomposition.h
  13. 10
      src/storm.cpp
  14. 36
      src/utility/storm.h
  15. 1
      test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp

12
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})

11
src/utility/cli.cpp → 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 {
}
}
}
}
}

29
src/cli/cli.h

@ -0,0 +1,29 @@
#ifndef STORM_UTILITY_CLI_H_
#define STORM_UTILITY_CLI_H_
#include <string>
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

1
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"

9
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<storm::dd::DdType T> class Mdp;
}
}
namespace modelchecker {
template<storm::dd::DdType DdType, typename ValueType>
class HybridMdpPrctlModelChecker : public SymbolicPropositionalModelChecker<DdType> {

1
src/modelchecker/propositional/SparsePropositionalModelChecker.h

@ -3,7 +3,6 @@
#include "src/modelchecker/AbstractModelChecker.h"
#include "src/models/sparse/Model.h"
namespace storm {
namespace modelchecker {

10
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<storm::dd::DdType Type> class Model;
}
}
namespace modelchecker {
template<storm::dd::DdType Type>
class SymbolicPropositionalModelChecker : public AbstractModelChecker {
public:

1
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 {

1
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 {

5
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 {

1
src/models/symbolic/Model.cpp

@ -3,6 +3,7 @@
#include <boost/algorithm/string/join.hpp>
#include "src/exceptions/IllegalArgumentException.h"
#include "src/exceptions/InvalidOperationException.h"
#include "src/adapters/AddExpressionAdapter.h"

1
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 {

10
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();

36
src/utility/cli.h → 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 <iostream>
#include <iomanip>
@ -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<typename ValueType>
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional<std::string> const& stateRewardsFile = boost::optional<std::string>(), boost::optional<std::string> const& transitionRewardsFile = boost::optional<std::string>()) {
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 */

1
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"

Loading…
Cancel
Save