From 637b58b19198e42143a9f41ca41ce31c7f98b102 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 18 Nov 2016 16:13:04 +0100 Subject: [PATCH] Adaptions to Jit based model builder due to new functionality of copying headers to include folder --- .../jit/ExplicitJitJaniModelBuilder.cpp | 67 +++---------------- .../builder/jit/ExplicitJitJaniModelBuilder.h | 10 +-- .../settings/modules/JitBuilderSettings.cpp | 25 ++----- .../settings/modules/JitBuilderSettings.h | 10 +-- src/storm/storage/sparse/StateStorage.cpp | 4 +- 5 files changed, 26 insertions(+), 90 deletions(-) diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index e1f198fa4..31b80d3c8 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -67,21 +67,16 @@ namespace storm { } else { boostIncludeDirectory = STORM_BOOST_INCLUDE_DIR; } - if (settings.isStormRootSet()) { - stormRoot = settings.getStormRoot(); + if (settings.isStormIncludeDirectorySet()) { + stormIncludeDirectory = settings.getStormIncludeDirectory(); } else { - stormRoot = STORM_CPP_BASE_PATH; + stormIncludeDirectory = STORM_BUILD_DIR "/include"; } if (settings.isCarlIncludeDirectorySet()) { carlIncludeDirectory = settings.getCarlIncludeDirectory(); } else { carlIncludeDirectory = STORM_CARL_INCLUDE_DIR; } - if (settings.isStormConfigDirectorySet()) { - stormConfigurationDirectory = settings.getStormConfigDirectory(); - } else { - stormConfigurationDirectory = STORM_BUILD_DIR "/include"; - } // Register all transient variables as transient. for (auto const& variable : this->model.getGlobalVariables().getTransientVariables()) { @@ -324,46 +319,14 @@ namespace storm { } template - bool ExplicitJitJaniModelBuilder::checkStormAvailable() const { + bool ExplicitJitJaniModelBuilder::checkStormHeadersAvailable() const { bool result = true; - std::string problem = "Unable to compile program using Storm data structures. Is Storm's root directory '" + stormRoot + "' set correctly? Does the directory contain the source subtree under src/ ?"; + std::string problem = "Unable to compile program using Storm headers. Is Storm's include directory '" + stormIncludeDirectory + "' set correctly? Does the directory contain all the headers (in particular 'storm-config.h'?"; try { std::string program = R"( #include "storm/builder/RewardModelInformation.h" - - int main() { - return 0; - } - )"; - boost::filesystem::path temporaryFile = writeToTemporaryFile(program); - std::string temporaryFilename = boost::filesystem::absolute(temporaryFile).string(); - boost::filesystem::path outputFile = temporaryFile; - outputFile += ".out"; - std::string outputFilename = boost::filesystem::absolute(outputFile).string(); - boost::optional error = execute(compiler + " " + compilerFlags + " " + temporaryFilename + " -I" + stormRoot + " -o " + outputFilename); - - if (error) { - result = false; - STORM_LOG_ERROR(problem); - STORM_LOG_TRACE(error.get()); - } else { - boost::filesystem::remove(outputFile); - } - } catch(std::exception const& e) { - result = false; - STORM_LOG_ERROR(problem); - } - return result; - } - - template - bool ExplicitJitJaniModelBuilder::checkStormConfigurationAvailable() const { - bool result = true; - std::string problem = "Unable to compile program using Storm configuration. Is Storm's configuration directory '" + stormConfigurationDirectory + "' set correctly? Does the directory contain the file storm-config.h?"; - try { - std::string program = R"( #include "storm-config.h" - + int main() { return 0; } @@ -373,7 +336,7 @@ namespace storm { boost::filesystem::path outputFile = temporaryFile; outputFile += ".out"; std::string outputFilename = boost::filesystem::absolute(outputFile).string(); - boost::optional error = execute(compiler + " " + compilerFlags + " " + temporaryFilename + " -I" + stormRoot + " -o " + outputFilename); + boost::optional error = execute(compiler + " " + compilerFlags + " " + temporaryFilename + " -I" + stormIncludeDirectory + " -o " + outputFilename); if (error) { result = false; @@ -395,7 +358,7 @@ namespace storm { std::string problem = "Unable to compile program using Carl data structures. Is Carls's include directory '" + carlIncludeDirectory + "' set correctly?"; try { std::string program = R"( -#include "storm/adapters/NumberAdapter.h" +#include "storm/adapters/CarlAdapter.h" int main() { return 0; @@ -406,7 +369,7 @@ namespace storm { boost::filesystem::path outputFile = temporaryFile; outputFile += ".out"; std::string outputFilename = boost::filesystem::absolute(outputFile).string(); - boost::optional error = execute(compiler + " " + compilerFlags + " " + temporaryFilename + " -I" + stormRoot + " -I" + stormConfigurationDirectory + " -I" + carlIncludeDirectory + " -o " + outputFilename); + boost::optional error = execute(compiler + " " + compilerFlags + " " + temporaryFilename + " -I" + stormIncludeDirectory + " -I" + carlIncludeDirectory + " -o " + outputFilename); if (error) { result = false; @@ -462,20 +425,12 @@ namespace storm { STORM_LOG_DEBUG("Success."); STORM_LOG_DEBUG("Checking whether Storm's headers are available."); - result = checkStormAvailable(); - if (!result) { - return result; - } - STORM_LOG_DEBUG("Success."); - - STORM_LOG_DEBUG("Checking whether Storm's configuration is available."); - result = checkStormConfigurationAvailable(); + result = checkStormHeadersAvailable(); if (!result) { return result; } STORM_LOG_DEBUG("Success."); - if (std::is_same::value) { STORM_LOG_DEBUG("Checking whether Carl's headers are available."); result = checkCarlAvailable(); @@ -2401,7 +2356,7 @@ namespace storm { dynamicLibraryPath += DYLIB_EXTENSION; std::string dynamicLibraryFilename = boost::filesystem::absolute(dynamicLibraryPath).string(); - std::string command = compiler + " " + sourceFilename + " " + compilerFlags + " -I" + stormRoot + " -I" + stormConfigurationDirectory + " -I" + boostIncludeDirectory + " -I" + carlIncludeDirectory + " -o " + dynamicLibraryFilename; + std::string command = compiler + " " + sourceFilename + " " + compilerFlags + " -I" + stormIncludeDirectory + " -I" + boostIncludeDirectory + " -I" + carlIncludeDirectory + " -o " + dynamicLibraryFilename; boost::optional error = execute(command); if (error) { diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h index 3f6d75ba2..ca3f6b3c2 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h @@ -64,8 +64,7 @@ namespace storm { bool checkCompilerFlagsWork() const; bool checkBoostAvailable() const; bool checkBoostDllAvailable() const; - bool checkStormAvailable() const; - bool checkStormConfigurationAvailable() const; + bool checkStormHeadersAvailable() const; bool checkCarlAvailable() const; /*! @@ -180,11 +179,8 @@ namespace storm { /// The include directory of boost. std::string boostIncludeDirectory; - /// The root directory of storm. - std::string stormRoot; - - /// The configuration directory of storm. - std::string stormConfigurationDirectory; + /// The include directory of storm. + std::string stormIncludeDirectory; /// The include directory of carl. std::string carlIncludeDirectory; diff --git a/src/storm/settings/modules/JitBuilderSettings.cpp b/src/storm/settings/modules/JitBuilderSettings.cpp index 71697677d..2944ccee3 100644 --- a/src/storm/settings/modules/JitBuilderSettings.cpp +++ b/src/storm/settings/modules/JitBuilderSettings.cpp @@ -16,8 +16,7 @@ namespace storm { const std::string JitBuilderSettings::doctorOptionName = "doctor"; const std::string JitBuilderSettings::compilerOptionName = "compiler"; - const std::string JitBuilderSettings::stormRootOptionName = "storm"; - const std::string JitBuilderSettings::stormConfigDirectoryOptionName = "stormconf"; + const std::string JitBuilderSettings::stormIncludeDirectoryOptionName = "storm"; const std::string JitBuilderSettings::boostIncludeDirectoryOptionName = "boost"; const std::string JitBuilderSettings::carlIncludeDirectoryOptionName = "carl"; const std::string JitBuilderSettings::compilerFlagsOptionName = "cxxflags"; @@ -26,10 +25,8 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, doctorOptionName, false, "Show debugging information on why the jit-based model builder is not working on your system.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, compilerOptionName, false, "The compiler in the jit-based model builder.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the executable. Defaults to c++.").setDefaultValueString("c++").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, stormRootOptionName, false, "The root directory of Storm.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory that contains the src/ subtree of Storm.").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, stormConfigDirectoryOptionName, false, "The directory containing Storm's configuration (storm-config.h).") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory that contains storm-config.h.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, stormIncludeDirectoryOptionName, false, "The include directory of Storm.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory that contains the headers of Storm.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, boostIncludeDirectoryOptionName, false, "The include directory of boost.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory containing the boost headers version >= 1.61.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, carlIncludeDirectoryOptionName, false, "The include directory of carl.") @@ -46,20 +43,12 @@ namespace storm { return this->getOption(compilerOptionName).getArgumentByName("name").getValueAsString(); } - bool JitBuilderSettings::isStormRootSet() const { - return this->getOption(stormRootOptionName).getHasOptionBeenSet(); + bool JitBuilderSettings::isStormIncludeDirectorySet() const { + return this->getOption(stormIncludeDirectoryOptionName).getHasOptionBeenSet(); } - std::string JitBuilderSettings::getStormRoot() const { - return this->getOption(stormRootOptionName).getArgumentByName("dir").getValueAsString(); - } - - bool JitBuilderSettings::isStormConfigDirectorySet() const { - return this->getOption(stormConfigDirectoryOptionName).getHasOptionBeenSet(); - } - - std::string JitBuilderSettings::getStormConfigDirectory() const { - return this->getOption(stormConfigDirectoryOptionName).getArgumentByName("dir").getValueAsString(); + std::string JitBuilderSettings::getStormIncludeDirectory() const { + return this->getOption(stormIncludeDirectoryOptionName).getArgumentByName("dir").getValueAsString(); } bool JitBuilderSettings::isBoostIncludeDirectorySet() const { diff --git a/src/storm/settings/modules/JitBuilderSettings.h b/src/storm/settings/modules/JitBuilderSettings.h index 503d798db..fb169ff20 100644 --- a/src/storm/settings/modules/JitBuilderSettings.h +++ b/src/storm/settings/modules/JitBuilderSettings.h @@ -18,11 +18,8 @@ namespace storm { bool isCompilerSet() const; std::string getCompiler() const; - bool isStormRootSet() const; - std::string getStormRoot() const; - - bool isStormConfigDirectorySet() const; - std::string getStormConfigDirectory() const; + bool isStormIncludeDirectorySet() const; + std::string getStormIncludeDirectory() const; bool isBoostIncludeDirectorySet() const; std::string getBoostIncludeDirectory() const; @@ -40,8 +37,7 @@ namespace storm { private: static const std::string compilerOptionName; - static const std::string stormRootOptionName; - static const std::string stormConfigDirectoryOptionName; + static const std::string stormIncludeDirectoryOptionName; static const std::string boostIncludeDirectoryOptionName; static const std::string carlIncludeDirectoryOptionName; static const std::string compilerFlagsOptionName; diff --git a/src/storm/storage/sparse/StateStorage.cpp b/src/storm/storage/sparse/StateStorage.cpp index 2b3219c8a..a007ab2ea 100644 --- a/src/storm/storage/sparse/StateStorage.cpp +++ b/src/storm/storage/sparse/StateStorage.cpp @@ -14,8 +14,8 @@ namespace storm { return stateToId.size(); } - template class StateStorage; - template class StateStorage; + template struct StateStorage; + template struct StateStorage; } } }