From 3bcdc1b579719c4e6e0f999bcbfeeaf457dd69be Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 11 Jul 2017 22:01:41 +0200 Subject: [PATCH] allowing to read transient variables in guards of edges in JIT-based JANI model builder and making the optimization level an option --- .../jit/ExplicitJitJaniModelBuilder.cpp | 36 ++++++++++--------- .../settings/modules/JitBuilderSettings.cpp | 7 ++++ .../settings/modules/JitBuilderSettings.h | 3 ++ 3 files changed, 30 insertions(+), 16 deletions(-) diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index f647d86b4..5547a71d4 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -73,12 +73,16 @@ namespace storm { if (settings.isCompilerFlagsSet()) { compilerFlags = settings.getCompilerFlags(); } else { + std::stringstream flagStream; #ifdef LINUX - compilerFlags = "-std=c++14 -fPIC -O3 -march=native -shared"; + flagStream << "-std=c++14 -fPIC -march=native -shared "; #endif #ifdef MACOSX - compilerFlags = "-std=c++14 -stdlib=libc++ -fPIC -march=native -O3 -shared -undefined dynamic_lookup "; + flagStream << "-std=c++14 -stdlib=libc++ -fPIC -march=native -shared -undefined dynamic_lookup "; #endif + + flagStream << "-O" << settings.getOptimizationLevel(); + compilerFlags = flagStream.str(); } if (settings.isBoostIncludeDirectorySet()) { boostIncludeDirectory = settings.getBoostIncludeDirectory(); @@ -1171,7 +1175,7 @@ namespace storm { indent(vectorSource, indentLevel) << "}" << std::endl << std::endl; } - indent(vectorSource, indentLevel) << "void get_edges_" << synchronizationVectorIndex << "(StateType const& state, std::vector>& edges, uint64_t position) {" << std::endl; + indent(vectorSource, indentLevel) << "void get_edges_" << synchronizationVectorIndex << "(StateType const& state, TransientVariables const& transientIn, std::vector>& edges, uint64_t position) {" << std::endl; position = 0; uint64_t participatingPosition = 0; for (auto const& inputActionName : synchronizationVector.getInput()) { @@ -1184,7 +1188,7 @@ namespace storm { for (auto const& edge : automaton.getEdges()) { if (edge.getActionIndex() == actionIndex) { std::string edgeName = automaton.getName() + "_" + std::to_string(edgeIndex); - indent(vectorSource, indentLevel + 2) << "if (edge_enabled_" << edgeName << "(state)) {" << std::endl; + indent(vectorSource, indentLevel + 2) << "if (edge_enabled_" << edgeName << "(state, transientIn)) {" << std::endl; indent(vectorSource, indentLevel + 3) << "edges.emplace_back(edge_" << edgeName << ");" << std::endl; indent(vectorSource, indentLevel + 2) << "}" << std::endl; } @@ -1198,7 +1202,7 @@ namespace storm { } indent(vectorSource, indentLevel) << "}" << std::endl << std::endl; - indent(vectorSource, indentLevel) << "void exploreSynchronizationVector_" << synchronizationVectorIndex << "(StateType const& state, StateBehaviour& behaviour, StateSet& statesToExplore) {" << std::endl; + indent(vectorSource, indentLevel) << "void exploreSynchronizationVector_" << synchronizationVectorIndex << "(StateType const& state, TransientVariables const& transientIn, StateBehaviour& behaviour, StateSet& statesToExplore) {" << std::endl; indent(vectorSource, indentLevel + 1) << "#ifndef NDEBUG" << std::endl; indent(vectorSource, indentLevel + 1) << "std::cout << \"exploring synchronization vector " << synchronizationVectorIndex << "\" << std::endl;" << std::endl; indent(vectorSource, indentLevel + 1) << "#endif" << std::endl; @@ -1207,7 +1211,7 @@ namespace storm { participatingPosition = 0; for (auto const& input : synchronizationVector.getInput()) { if (!storm::jani::SynchronizationVector::isNoActionInput(input)) { - indent(vectorSource, indentLevel + 1) << "get_edges_" << synchronizationVectorIndex << "(state, edges[" << participatingPosition << "], " << participatingPosition << ");" << std::endl; + indent(vectorSource, indentLevel + 1) << "get_edges_" << synchronizationVectorIndex << "(state, transientIn, edges[" << participatingPosition << "], " << participatingPosition << ");" << std::endl; indent(vectorSource, indentLevel + 1) << "if (edges[" << participatingPosition << "].empty()) {" << std::endl; indent(vectorSource, indentLevel + 2) << "return;" << std::endl; indent(vectorSource, indentLevel + 1) << "}" << std::endl; @@ -1902,7 +1906,7 @@ namespace storm { {% endif %} // Non-synchronizing edges. - {% for edge in nonsynch_edges %}static bool edge_enabled_{$edge.name}(StateType const& in) { + {% for edge in nonsynch_edges %}static bool edge_enabled_{$edge.name}(StateType const& in, TransientVariables const& transientIn) { if ({$edge.guard}) { return true; } @@ -1979,7 +1983,7 @@ namespace storm { {% endfor %}{% endfor %} // Synchronizing edges. - {% for edge in synch_edges %}static bool edge_enabled_{$edge.name}(StateType const& in) { + {% for edge in synch_edges %}static bool edge_enabled_{$edge.name}(StateType const& in, TransientVariables const& transientIn) { if ({$edge.guard}) { return true; } @@ -2109,7 +2113,7 @@ namespace storm { DestinationWithoutTransientFunctionPtr destinationWithoutTransientFunction; }; - typedef bool (*EdgeEnabledFunctionPtr)(StateType const&); + typedef bool (*EdgeEnabledFunctionPtr)(StateType const&, TransientVariables const& transientIn); typedef void (*EdgeTransientFunctionPtr)(StateType const&, TransientVariables const& transientIn, TransientVariables& out {% if exploration_checks %}, VariableWrites& variableWrites {% endif %}); class Edge { @@ -2124,8 +2128,8 @@ namespace storm { // Intentionally left empty. } - bool isEnabled(StateType const& in) const { - return edgeEnabledFunction(in); + bool isEnabled(StateType const& in, TransientVariables const& transientIn) const { + return edgeEnabledFunction(in, transientIn); } void addDestination(Destination const& destination) { @@ -2281,10 +2285,10 @@ namespace storm { {% endfor %} // Explore all edges that do not take part in synchronization vectors. - exploreNonSynchronizingEdges(currentState, behaviour, statesToExplore); + exploreNonSynchronizingEdges(currentState, transientOut, behaviour, statesToExplore); // Explore all edges that participate in synchronization vectors. - exploreSynchronizingEdges(currentState, behaviour, statesToExplore); + exploreSynchronizingEdges(currentState, transientOut, behaviour, statesToExplore); } {% if dontFixDeadlocks %} @@ -2307,7 +2311,7 @@ namespace storm { return false; } - void exploreNonSynchronizingEdges(StateType const& in, StateBehaviour& behaviour, StateSet& statesToExplore) { + void exploreNonSynchronizingEdges(StateType const& in, TransientVariables const& transientIn, StateBehaviour& behaviour, StateSet& statesToExplore) { {% for edge in nonsynch_edges %}{ if ({$edge.guard}) { Choice& choice = behaviour.addChoice(!model_is_deterministic() && !model_is_discrete_time() && {$edge.markovian}); @@ -2347,9 +2351,9 @@ namespace storm { {% for vector in synch_vectors %}{$vector.functions} {% endfor %} - void exploreSynchronizingEdges(StateType const& state, StateBehaviour& behaviour, StateSet& statesToExplore) { + void exploreSynchronizingEdges(StateType const& state, TransientVariables const& transientIn, StateBehaviour& behaviour, StateSet& statesToExplore) { {% for vector in synch_vectors %}{ - exploreSynchronizationVector_{$vector.index}(state, behaviour, statesToExplore); + exploreSynchronizationVector_{$vector.index}(state, transientIn, behaviour, statesToExplore); } {% endfor %} } diff --git a/src/storm/settings/modules/JitBuilderSettings.cpp b/src/storm/settings/modules/JitBuilderSettings.cpp index 127434055..b779f23f5 100644 --- a/src/storm/settings/modules/JitBuilderSettings.cpp +++ b/src/storm/settings/modules/JitBuilderSettings.cpp @@ -20,6 +20,7 @@ namespace storm { const std::string JitBuilderSettings::boostIncludeDirectoryOptionName = "boost"; const std::string JitBuilderSettings::carlIncludeDirectoryOptionName = "carl"; const std::string JitBuilderSettings::compilerFlagsOptionName = "cxxflags"; + const std::string JitBuilderSettings::optimizationLevelOptionName = "opt"; JitBuilderSettings::JitBuilderSettings() : ModuleSettings(moduleName) { 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()); @@ -33,6 +34,8 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory containing the carl headers.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, compilerFlagsOptionName, false, "The flags passed to the compiler.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("flags", "The compiler flags.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, optimizationLevelOptionName, false, "The optimization level to use.") + .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("level", "The compiler flags.").setDefaultValueUnsignedInteger(3).build()).build()); } bool JitBuilderSettings::isCompilerSet() const { @@ -79,6 +82,10 @@ namespace storm { return this->getOption(compilerFlagsOptionName).getArgumentByName("flags").getValueAsString(); } + uint64_t JitBuilderSettings::getOptimizationLevel() const { + return this->getOption(optimizationLevelOptionName).getArgumentByName("level").getValueAsUnsignedInteger(); + } + void JitBuilderSettings::finalize() { // Intentionally left empty. } diff --git a/src/storm/settings/modules/JitBuilderSettings.h b/src/storm/settings/modules/JitBuilderSettings.h index fb169ff20..ad3eb89ac 100644 --- a/src/storm/settings/modules/JitBuilderSettings.h +++ b/src/storm/settings/modules/JitBuilderSettings.h @@ -30,6 +30,8 @@ namespace storm { bool isCompilerFlagsSet() const; std::string getCompilerFlags() const; + uint64_t getOptimizationLevel() const; + bool check() const override; void finalize() override; @@ -42,6 +44,7 @@ namespace storm { static const std::string carlIncludeDirectoryOptionName; static const std::string compilerFlagsOptionName; static const std::string doctorOptionName; + static const std::string optimizationLevelOptionName; }; }