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<std::reference_wrapper<Edge const>>& edges, uint64_t position) {" << std::endl;
+ indent(vectorSource, indentLevel) << "void get_edges_" << synchronizationVectorIndex << "(StateType const& state, TransientVariables const& transientIn, std::vector<std::reference_wrapper<Edge const>>& 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<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore) {" << std::endl;
+ indent(vectorSource, indentLevel) << "void exploreSynchronizationVector_" << synchronizationVectorIndex << "(StateType const& state, TransientVariables const& transientIn, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& 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<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore) {
+ void exploreNonSynchronizingEdges(StateType const& in, TransientVariables const& transientIn, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore) {
{% for edge in nonsynch_edges %}{
if ({$edge.guard}) {
Choice<IndexType, ValueType>& 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<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore) {
+ void exploreSynchronizingEdges(StateType const& state, TransientVariables const& transientIn, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& 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;
};
}