sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

allowing to read transient variables in guards of edges in JIT-based JANI model builder and making the optimization level an option

main
dehnert 8 years ago
parent
6fd75ac37e
commit
3bcdc1b579
3 changed files with 30 additions and 16 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 36
      src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
  2. 7
      src/storm/settings/modules/JitBuilderSettings.cpp
  3. 3
      src/storm/settings/modules/JitBuilderSettings.h

36
src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
View File

@ -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 %}
}

7
src/storm/settings/modules/JitBuilderSettings.cpp
View File

@ -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.
}

3
src/storm/settings/modules/JitBuilderSettings.h
View File

@ -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;
};
}

Write Preview
Loading…
Cancel
Save