diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index cea4cd44d..65cdd4704 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -74,8 +74,8 @@ link_directories(${Boost_LIBRARY_DIRS}) include_directories(${Boost_INCLUDE_DIRS}) list(APPEND STORM_LINK_LIBRARIES ${Boost_LIBRARIES}) message(STATUS "StoRM - Using Boost ${Boost_VERSION} (lib ${Boost_LIB_VERSION})") -#message(STATUS "StoRM - BOOST_INCLUDE_DIRS is ${Boost_INCLUDE_DIRS}") -#message(STATUS "StoRM - BOOST_LIBRARY_DIRS is ${Boost_LIBRARY_DIRS}") +# set the information for the config header +set(STORM_BOOST_INCLUDE_DIR "${Boost_INCLUDE_DIRS}") ############################################################# ## diff --git a/src/builder/BuilderOptions.cpp b/src/builder/BuilderOptions.cpp index 438aa72cd..87dcc69b8 100644 --- a/src/builder/BuilderOptions.cpp +++ b/src/builder/BuilderOptions.cpp @@ -2,6 +2,9 @@ #include "src/logic/Formulas.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/IOSettings.h" + #include "src/utility/macros.h" #include "src/exceptions/InvalidSettingsException.h" @@ -50,6 +53,8 @@ namespace storm { this->setTerminalStatesFromFormula(*formulas.front()); } } + + explorationChecks = storm::settings::getModule().isExplorationChecksSet(); } void BuilderOptions::preserveFormula(storm::logic::Formula const& formula) { @@ -146,6 +151,15 @@ namespace storm { buildAllRewardModels = true; return *this; } + + bool BuilderOptions::isExplorationChecksSet() const { + return explorationChecks; + } + + BuilderOptions& BuilderOptions::setExplorationChecks(bool newValue) { + explorationChecks = newValue; + return *this; + } BuilderOptions& BuilderOptions::addRewardModel(std::string const& rewardModelName) { STORM_LOG_THROW(!buildAllRewardModels, storm::exceptions::InvalidSettingsException, "Cannot add reward model, because all reward models are built anyway."); diff --git a/src/builder/BuilderOptions.h b/src/builder/BuilderOptions.h index 7a7dc4267..751b4b18d 100644 --- a/src/builder/BuilderOptions.h +++ b/src/builder/BuilderOptions.h @@ -91,6 +91,7 @@ namespace storm { bool isBuildChoiceLabelsSet() const; bool isBuildAllRewardModelsSet() const; bool isBuildAllLabelsSet() const; + bool isExplorationChecksSet() const; BuilderOptions& setBuildAllRewardModels(); BuilderOptions& addRewardModel(std::string const& rewardModelName); @@ -100,6 +101,7 @@ namespace storm { BuilderOptions& addTerminalExpression(storm::expressions::Expression const& expression, bool value); BuilderOptions& addTerminalLabel(std::string const& label, bool value); BuilderOptions& setBuildChoiceLabels(bool newValue); + BuilderOptions& setExplorationChecks(bool newValue); private: /// A flag that indicates whether all reward models are to be built. In this case, the reward model names are @@ -123,6 +125,9 @@ namespace storm { /// A flag indicating whether or not to build choice labels. bool buildChoiceLabels; + + /// A flag that stores whether exploration checks are to be performed. + bool explorationChecks; }; } diff --git a/src/builder/jit/Choice.cpp b/src/builder/jit/Choice.cpp index 5173591fa..99c4e7905 100644 --- a/src/builder/jit/Choice.cpp +++ b/src/builder/jit/Choice.cpp @@ -7,10 +7,20 @@ namespace storm { namespace jit { template - Choice::Choice() { + Choice::Choice() : markovian(false) { // Intentionally left empty. } + template + void Choice::setMarkovian(bool value) { + markovian = value; + } + + template + bool Choice::isMarkovian() const { + return markovian; + } + template void Choice::add(DistributionEntry const& entry) { distribution.add(entry); diff --git a/src/builder/jit/Choice.h b/src/builder/jit/Choice.h index 400bb9dbe..2bb1e3b93 100644 --- a/src/builder/jit/Choice.h +++ b/src/builder/jit/Choice.h @@ -11,6 +11,9 @@ namespace storm { public: Choice(); + void setMarkovian(bool value); + bool isMarkovian() const; + void add(DistributionEntry const& entry); void add(IndexType const& index, ValueType const& value); void add(Choice&& choice); @@ -66,6 +69,9 @@ namespace storm { /// The reward values associated with this choice. std::vector rewards; + + /// A flag storing whether this choice is Markovian. + bool markovian; }; } diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp index 7257f100d..5729dc552 100644 --- a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -23,28 +23,62 @@ #include "src/exceptions/NotSupportedException.h" #include "src/exceptions/UnexpectedException.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/JitBuilderSettings.h" + +#include "src/utility/OsDetection.h" +#include "storm-config.h" + namespace storm { namespace builder { namespace jit { - static const std::string CXX_COMPILER = "clang++"; +#ifdef LINUX + static const std::string DYLIB_EXTENSION = ".so"; +#endif +#ifdef MACOSX static const std::string DYLIB_EXTENSION = ".dylib"; - static const std::string COMPILER_FLAGS = "-std=c++11 -stdlib=libc++ -fPIC -O3 -shared -funroll-loops -undefined dynamic_lookup"; - static const std::string STORM_ROOT = "/Users/chris/work/storm"; - static const std::string L3PP_ROOT = "/Users/chris/work/storm/resources/3rdparty/l3pp"; - static const std::string BOOST_ROOT = "/usr/local/Cellar/boost/1.62.0/include"; - static const std::string GMP_ROOT = "/usr/local/Cellar/gmp/6.1.1"; - static const std::string CARL_ROOT = "/Users/chris/work/carl"; - static const std::string CLN_ROOT = "/usr/local/Cellar/cln/1.3.4"; - static const std::string GINAC_ROOT = "/usr/local/Cellar/ginac/1.6.7_1"; +#endif +#ifdef WINDOWS + static const std::string DYLIB_EXTENSION = ".dll"; +#endif template ExplicitJitJaniModelBuilder::ExplicitJitJaniModelBuilder(storm::jani::Model const& model, storm::builder::BuilderOptions const& options) : options(options), model(model), modelComponentsBuilder(model.getModelType()) { + + // Load all options from the settings module. + storm::settings::modules::JitBuilderSettings const& settings = storm::settings::getModule(); + if (settings.isCompilerSet()) { + compiler = settings.getCompiler(); + } else { + compiler = "c++"; + } + if (settings.isCompilerFlagsSet()) { + compilerFlags = settings.getCompilerFlags(); + } else { +#ifdef LINUX + compilerFlags = "-std=c++11 -fPIC -O3 -shared -funroll-loops -undefined dynamic_lookup"; +#endif +#ifdef MACOSX + compilerFlags = "-std=c++11 -stdlib=libc++ -fPIC -O3 -shared -funroll-loops -undefined dynamic_lookup"; +#endif + } + if (settings.isBoostIncludeDirectorySet()) { + boostIncludeDirectory = settings.getBoostIncludeDirectory(); + } else { + boostIncludeDirectory = STORM_BOOST_INCLUDE_DIR; + } + if (settings.isStormRootSet()) { + stormRoot = settings.getStormRoot(); + } else { + stormRoot = STORM_CPP_BASE_PATH; + } + // Register all transient variables as transient. for (auto const& variable : this->model.getGlobalVariables().getTransientVariables()) { transientVariables.insert(variable.getExpressionVariable()); } - + // Construct vector of the automata to be put in parallel. storm::jani::Composition const& topLevelComposition = this->model.getSystemComposition(); if (topLevelComposition.isAutomatonComposition()) { @@ -59,10 +93,7 @@ namespace storm { } } - for (auto& automaton : this->model.getAutomata()) { - automaton.pushEdgeAssignmentsToDestinations(); - } - + // Create location variables for all the automata that we put in parallel. for (auto const& automaton : parallelAutomata) { automatonToLocationVariable.emplace(automaton.get().getName(), this->model.getManager().declareFreshIntegerVariable(false, automaton.get().getName() + "_")); } @@ -71,749 +102,388 @@ namespace storm { #ifdef STORM_HAVE_CARL if (!std::is_same::value && this->model.hasUndefinedConstants()) { #else - if (this->model.hasUndefinedConstants()) { + if (this->model.hasUndefinedConstants()) { #endif - std::vector> undefinedConstants = this->model.getUndefinedConstants(); - std::stringstream stream; - bool printComma = false; - for (auto const& constant : undefinedConstants) { - if (printComma) { - stream << ", "; - } else { - printComma = true; - } - stream << constant.get().getName() << " (" << constant.get().getType() << ")"; + std::vector> undefinedConstants = this->model.getUndefinedConstants(); + std::stringstream stream; + bool printComma = false; + for (auto const& constant : undefinedConstants) { + if (printComma) { + stream << ", "; + } else { + printComma = true; } - stream << "."; - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Model still contains these undefined constants: " + stream.str()); + stream << constant.get().getName() << " (" << constant.get().getType() << ")"; } + stream << "."; + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Model still contains these undefined constants: " + stream.str()); + } #ifdef STORM_HAVE_CARL - else if (std::is_same::value && !this->model.undefinedConstantsAreGraphPreserving()) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The input model contains undefined constants that influence the graph structure of the underlying model, which is not allowed."); - } + else if (std::is_same::value && !this->model.undefinedConstantsAreGraphPreserving()) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The input model contains undefined constants that influence the graph structure of the underlying model, which is not allowed."); + } #endif } template - std::string ExplicitJitJaniModelBuilder::createSourceCode() { - std::string sourceTemplate = R"( + boost::optional ExplicitJitJaniModelBuilder::execute(std::string command) { + auto start = std::chrono::high_resolution_clock::now(); + char buffer[128]; + std::stringstream output; + command += " 2>&1"; -#define NDEBUG + STORM_LOG_TRACE("Executing command: " << command); -#include -#include -#include -#include -#include -#include -#include + std::unique_ptr pipe(popen(command.c_str(), "r")); + STORM_LOG_THROW(pipe, storm::exceptions::InvalidStateException, "Call to popen failed."); -#include "resources/3rdparty/sparsepp/sparsepp.h" + while (!feof(pipe.get())) { + if (fgets(buffer, 128, pipe.get()) != nullptr) + output << buffer; + } + int result = pclose(pipe.get()); + pipe.release(); -#include "src/builder/jit/StateSet.h" -#include "src/builder/jit/JitModelBuilderInterface.h" -#include "src/builder/jit/StateBehaviour.h" -#include "src/builder/jit/ModelComponentsBuilder.h" -#include "src/builder/RewardModelInformation.h" + auto end = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Executing command took " << std::chrono::duration_cast(end - start).count() << "ms."); - namespace storm { - namespace builder { - namespace jit { - - typedef uint32_t IndexType; - typedef double ValueType; - - struct StateType { - // Boolean variables. - {% for variable in nontransient_variables.boolean %}bool {$variable.name} : 1; - {% endfor %} - // Bounded integer variables. - {% for variable in nontransient_variables.boundedInteger %}uint64_t {$variable.name} : {$variable.numberOfBits}; - {% endfor %} - // Unbounded integer variables. - {% for variable in nontransient_variables.unboundedInteger %}int64_t {$variable.name}; - {% endfor %} - // Real variables. - {% for variable in nontransient_variables.real %}double {$variable.name}; - {% endfor %} - // Location variables. - {% for variable in nontransient_variables.locations %}uint64_t {$variable.name} : {$variable.numberOfBits}; - {% endfor %} - }; - - bool operator==(StateType const& first, StateType const& second) { - bool result = true; - {% for variable in nontransient_variables.boolean %}result &= !(first.{$variable.name} ^ second.{$variable.name}); - {% endfor %} - {% for variable in nontransient_variables.boundedInteger %}result &= first.{$variable.name} == second.{$variable.name}; - {% endfor %} - {% for variable in nontransient_variables.unboundedInteger %}result &= first.{$variable.name} == second.{$variable.name}; - {% endfor %} - {% for variable in nontransient_variables.real %}result &= first.{$variable.name} == second.{$variable.name}; - {% endfor %} - {% for variable in nontransient_variables.locations %}result &= first.{$variable.name} == second.{$variable.name}; - {% endfor %} - return result; - } - - std::ostream& operator<<(std::ostream& out, StateType const& in) { - out << "<"; - {% for variable in nontransient_variables.boolean %}out << "{$variable.name}=" << std::boolalpha << in.{$variable.name} << ", " << std::noboolalpha; - {% endfor %} - {% for variable in nontransient_variables.boundedInteger %}out << "{$variable.name}=" << in.{$variable.name} << ", "; - {% endfor %} - {% for variable in nontransient_variables.unboundedInteger %}out << "{$variable.name}=" << in.{$variable.name} << ", "; - {% endfor %} - {% for variable in nontransient_variables.real %}out << "{$variable.name}=" << in.{$variable.name} << ", "; - {% endfor %} - {% for variable in nontransient_variables.locations %}out << "{$variable.name}=" << in.{$variable.name} << ", "; - {% endfor %} - out << ">"; - return out; - } - - struct TransientVariables { - TransientVariables() { - reset(); - } - - void reset() { - {% for variable in transient_variables.boolean %}{$variable.name} = {$variable.init}; - {% endfor %} - {% for variable in transient_variables.boundedInteger %}{$variable.name} = {$variable.init}; - {% endfor %} - {% for variable in transient_variables.unboundedInteger %}{$variable.name} = {$variable.init}; - {% endfor %} - {% for variable in transient_variables.real %}{$variable.name} = {$variable.init}; - {% endfor %} - } - - // Boolean variables. - {% for variable in transient_variables.boolean %}bool {$variable.name} : 1; - {% endfor %} - // Bounded integer variables. - {% for variable in transient_variables.boundedInteger %}uint64_t {$variable.name} : {$variable.numberOfBits}; - {% endfor %} - // Unbounded integer variables. - {% for variable in transient_variables.unboundedInteger %}int64_t {$variable.name}; - {% endfor %} - // Real variables. - {% for variable in transient_variables.real %}double {$variable.name}; - {% endfor %} - }; - - std::ostream& operator<<(std::ostream& out, TransientVariables const& in) { - out << "<"; - {% for variable in transient_variables.boolean %}out << "{$variable.name}=" << std::boolalpha << in.{$variable.name} << ", " << std::noboolalpha; - {% endfor %} - {% for variable in transient_variables.boundedInteger %}out << "{$variable.name}=" << in.{$variable.name} << ", "; - {% endfor %} - {% for variable in transient_variables.unboundedInteger %}out << "{$variable.name}=" << in.{$variable.name} << ", "; - {% endfor %} - {% for variable in transient_variables.real %}out << "{$variable.name}=" << in.{$variable.name} << ", "; - {% endfor %} - out << ">"; - return out; - } + if (WEXITSTATUS(result) == 0) { + return boost::none; + } else { + return "Executing command failed. Got response: " + output.str(); + } + } + + template + boost::filesystem::path ExplicitJitJaniModelBuilder::writeToTemporaryFile(std::string const& content, std::string const& suffix) { + boost::filesystem::path temporaryFile = boost::filesystem::unique_path("%%%%-%%%%-%%%%-%%%%" + suffix); + std::ofstream out(temporaryFile.native()); + out << content << std::endl; + out.close(); + return temporaryFile; + } + + template + bool ExplicitJitJaniModelBuilder::checkTemporaryFileWritable() const { + bool result = true; + std::string problem = "Unable to write to a temporary file. Are the appropriate permissions set?"; + try { + boost::filesystem::path temporaryFile = writeToTemporaryFile("Hello world."); + } catch (std::exception const& e) { + result = false; + STORM_LOG_ERROR(problem); + } + + return result; + } - } + template + bool ExplicitJitJaniModelBuilder::checkCompilerWorks() const { + bool result = true; + std::string problem = "Unable to compile empty program with C++ compiler. Is the C++ compiler '" + compiler + "' installed and working?"; + try { + std::string emptyProgram = R"( +#include + + int main() { + return 0; } + )"; + boost::filesystem::path temporaryFile = writeToTemporaryFile(emptyProgram); + 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 + " " + temporaryFilename + " -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); } - namespace std { - template <> - struct hash { - std::size_t operator()(storm::builder::jit::StateType const& in) const { - // Note: this is faster than viewing the struct as a bit field and taking hash_combine of the bytes. - std::size_t seed = 0; - {% for variable in nontransient_variables.boolean %}spp::hash_combine(seed, in.{$variable.name}); - {% endfor %} - {% for variable in nontransient_variables.boundedInteger %}spp::hash_combine(seed, in.{$variable.name}); - {% endfor %} - {% for variable in nontransient_variables.unboundedInteger %}spp::hash_combine(seed, in.{$variable.name}); - {% endfor %} - {% for variable in nontransient_variables.real %}spp::hash_combine(seed, in.{$variable.name}); - {% endfor %} - {% for variable in nontransient_variables.locations %}spp::hash_combine(seed, in.{$variable.name}); - {% endfor %} - return seed; - } - }; - } + return result; + } - namespace storm { - namespace builder { - namespace jit { - - static bool model_is_deterministic() { - return {$deterministic_model}; - } - - static bool model_is_discrete_time() { - return {$discrete_time_model}; - } - - // Non-synchronizing edges. - {% for edge in nonsynch_edges %}static bool edge_enabled_{$edge.name}(StateType const& in) { - if ({$edge.guard}) { - return true; - } - return false; - } - - static void edge_perform_{$edge.name}(StateType const& in, TransientVariables const& transientIn, TransientVariables& transientOut) { - {% for assignment in edge.transient_assignments %}transientOut.{$assignment.variable} = {$assignment.value}; - {% endfor %} - } - - {% for destination in edge.destinations %} - static void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType const& in, StateType& out) { - {% for level in destination.levels %}if (level == {$level.index}) { - {% for assignment in level.non_transient_assignments %}out.{$assignment.variable} = {$assignment.value}; - {% endfor %} - } - {% endfor %} - } - - static void destination_perform_{$edge.name}_{$destination.name}(StateType const& in, StateType& out) { - {% for level in destination.levels %} - destination_perform_level_{$edge.name}_{$destination.name}({$level.index}, in, out); - {% endfor %} - } + template + bool ExplicitJitJaniModelBuilder::checkCompilerFlagsWork() const { + bool result = true; + std::string problem = "Unable to compile program with the flags '" + compilerFlags + "'. Does the C++ compiler accept these flags?"; + try { + std::string emptyProgram = R"( +#include + + int main() { + return 0; + } + )"; + boost::filesystem::path temporaryFile = writeToTemporaryFile(emptyProgram); + 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 + " -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; + } - static void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType const& in, StateType& out, TransientVariables const& transientIn, TransientVariables& transientOut) { - {% for level in destination.levels %}if (level == {$level.index}) { - {% for assignment in level.non_transient_assignments %}out.{$assignment.variable} = {$assignment.value}; - {% endfor %} - {% for assignment in level.transient_assignments %}transientOut.{$assignment.variable} = {$assignment.value}; - {% endfor %} - } - {% endfor %} - } - - static void destination_perform_{$edge.name}_{$destination.name}(StateType const& in, StateType& out, TransientVariables const& transientIn, TransientVariables& transientOut) { - {% for level in destination.levels %} - destination_perform_level_{$edge.name}_{$destination.name}({$level.index}, in, out, transientIn, transientOut); - {% endfor %} - } - {% endfor %}{% endfor %} - - // Synchronizing edges. - {% for edge in synch_edges %}static bool edge_enabled_{$edge.name}(StateType const& in) { - if ({$edge.guard}) { - return true; - } - return false; - } - - static void edge_perform_{$edge.name}(StateType const& in, TransientVariables const& transientIn, TransientVariables& transientOut) { - {% for assignment in edge.transient_assignments %}transientOut.{$assignment.variable} = {$assignment.value}; - {% endfor %} - } - - {% for destination in edge.destinations %} - static void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType const& in, StateType& out) { - {% for level in destination.levels %}if (level == {$level.index}) { - {% for assignment in level.non_transient_assignments %}out.{$assignment.variable} = {$assignment.value}; - {% endfor %} - } - {% endfor %} - } - - static void destination_perform_{$edge.name}_{$destination.name}(StateType const& in, StateType& out) { - {% for level in destination.levels %} - destination_perform_level_{$edge.name}_{$destination.name}({$level.index}, in, out); - {% endfor %} - } - - static void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType const& in, StateType& out, TransientVariables const& transientIn, TransientVariables& transientOut) { - {% for level in destination.levels %}if (level == {$level.index}) { - {% for assignment in level.non_transient_assignments %}out.{$assignment.variable} = {$assignment.value}; - {% endfor %} - {% for assignment in level.transient_assignments %}transientOut.{$assignment.variable} = {$assignment.value}; - {% endfor %} - } - {% endfor %} - } - - static void destination_perform_{$edge.name}_{$destination.name}(StateType const& in, StateType& out, TransientVariables const& transientIn, TransientVariables& transientOut) { - {% for level in destination.levels %} - destination_perform_level_{$edge.name}_{$destination.name}({$level.index}, in, out, transientIn, transientOut); - {% endfor %} - } - {% endfor %}{% endfor %} - - typedef void (*DestinationLevelFunctionPtr)(int_fast64_t, StateType const&, StateType&, TransientVariables const&, TransientVariables&); - typedef void (*DestinationFunctionPtr)(StateType const&, StateType&, TransientVariables const&, TransientVariables&); - typedef void (*DestinationWithoutTransientLevelFunctionPtr)(int_fast64_t, StateType const&, StateType&); - typedef void (*DestinationWithoutTransientFunctionPtr)(StateType const&, StateType&); - - class Destination { - public: - Destination() : mLowestLevel(0), mHighestLevel(0), mValue(), destinationLevelFunction(nullptr), destinationFunction(nullptr), destinationWithoutTransientLevelFunction(nullptr), destinationWithoutTransientFunction(nullptr) { - // Intentionally left empty. - } - - Destination(int_fast64_t lowestLevel, int_fast64_t highestLevel, ValueType const& value, DestinationLevelFunctionPtr destinationLevelFunction, DestinationFunctionPtr destinationFunction, DestinationWithoutTransientLevelFunctionPtr destinationWithoutTransientLevelFunction, DestinationWithoutTransientFunctionPtr destinationWithoutTransientFunction) : mLowestLevel(lowestLevel), mHighestLevel(highestLevel), mValue(value), destinationLevelFunction(destinationLevelFunction), destinationFunction(destinationFunction), destinationWithoutTransientLevelFunction(destinationWithoutTransientLevelFunction), destinationWithoutTransientFunction(destinationWithoutTransientFunction) { - // Intentionally left empty. - } - - int_fast64_t lowestLevel() const { - return mLowestLevel; - } - - int_fast64_t highestLevel() const { - return mHighestLevel; - } - - ValueType const& value() const { - return mValue; - } - - void perform(int_fast64_t level, StateType const& in, StateType& out, TransientVariables const& transientIn, TransientVariables& transientOut) const { - destinationLevelFunction(level, in, out, transientIn, transientOut); - } - - void perform(StateType const& in, StateType& out, TransientVariables const& transientIn, TransientVariables& transientOut) const { - destinationFunction(in, out, transientIn, transientOut); - } - - void perform(int_fast64_t level, StateType const& in, StateType& out) const { - destinationWithoutTransientLevelFunction(level, in, out); - } - - void perform(StateType const& in, StateType& out) const { - destinationWithoutTransientFunction(in, out); - } - - private: - int_fast64_t mLowestLevel; - int_fast64_t mHighestLevel; - ValueType mValue; - DestinationLevelFunctionPtr destinationLevelFunction; - DestinationFunctionPtr destinationFunction; - DestinationWithoutTransientLevelFunctionPtr destinationWithoutTransientLevelFunction; - DestinationWithoutTransientFunctionPtr destinationWithoutTransientFunction; - }; - - typedef bool (*EdgeEnabledFunctionPtr)(StateType const&); - typedef void (*EdgeTransientFunctionPtr)(StateType const&, TransientVariables const& transientIn, TransientVariables& out); - - class Edge { - public: - typedef std::vector ContainerType; - - Edge() : edgeEnabledFunction(nullptr), edgeTransientFunction(nullptr) { - // Intentionally left empty. - } - - Edge(EdgeEnabledFunctionPtr edgeEnabledFunction, EdgeTransientFunctionPtr edgeTransientFunction = nullptr) : edgeEnabledFunction(edgeEnabledFunction), edgeTransientFunction(edgeTransientFunction) { - // Intentionally left empty. - } - - bool isEnabled(StateType const& in) const { - return edgeEnabledFunction(in); - } - - void addDestination(Destination const& destination) { - destinations.push_back(destination); - } - - void addDestination(int_fast64_t lowestLevel, int_fast64_t highestLevel, ValueType const& value, DestinationLevelFunctionPtr destinationLevelFunction, DestinationFunctionPtr destinationFunction, DestinationWithoutTransientLevelFunctionPtr destinationWithoutTransientLevelFunction, DestinationWithoutTransientFunctionPtr destinationWithoutTransientFunction) { - destinations.emplace_back(lowestLevel, highestLevel, value, destinationLevelFunction, destinationFunction, destinationWithoutTransientLevelFunction, destinationWithoutTransientFunction); - } + template + bool ExplicitJitJaniModelBuilder::checkBoostAvailable() const { + bool result = true; + std::string problem = "Unable to compile program using boost. Is boosts's include directory '" + boostIncludeDirectory + "' set correctly?"; + try { + std::string program = R"( +#include +#include + + 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 + " " + temporaryFilename + " -I" + boostIncludeDirectory + " -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::checkBoostDllAvailable() const { + bool result = true; + std::string problem = "Unable to compile program using boost's dll library. Is boosts's include directory '" + boostIncludeDirectory + "' pointing to a boost installation with version at least 1.61?"; + try { + std::string program = R"( +#include +#include + + 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 + " " + temporaryFilename + " -I" + boostIncludeDirectory + " -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::checkStormAvailable() 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/ ?"; + try { + std::string program = R"( +#include +#include "src/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 + " " + 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::doctor() const { + bool result = true; + + STORM_LOG_DEBUG("Checking whether temporary file is writable."); + result = checkTemporaryFileWritable(); + if (!result) { + return result; + } + STORM_LOG_DEBUG("Success."); + + STORM_LOG_DEBUG("Checking whether compiler invocation works."); + result = checkCompilerWorks(); + if (!result) { + return result; + } + STORM_LOG_DEBUG("Success."); - std::vector const& getDestinations() const { - return destinations; - } - - ContainerType::const_iterator begin() const { - return destinations.begin(); - } + STORM_LOG_DEBUG("Checking whether compiler flags work."); + result = checkCompilerFlagsWork(); + if (!result) { + return result; + } + STORM_LOG_DEBUG("Success."); - ContainerType::const_iterator end() const { - return destinations.end(); - } - - void perform(StateType const& in, TransientVariables const& transientIn, TransientVariables& transientOut) const { - edgeTransientFunction(in, transientIn, transientOut); - } - - private: - EdgeEnabledFunctionPtr edgeEnabledFunction; - EdgeTransientFunctionPtr edgeTransientFunction; - ContainerType destinations; - }; - - void locations_perform(StateType const& in, TransientVariables const& transientIn, TransientVariables& transientOut) { - {% for location in locations %}if ({$location.guard}) { - {% for assignment in location.assignments %}transientOut.{$assignment.variable} = {$assignment.value};{% endfor %} - } - {% endfor %} - } + STORM_LOG_DEBUG("Checking whether boost is available."); + result = checkBoostAvailable(); + if (!result) { + return result; + } + STORM_LOG_DEBUG("Success."); + + STORM_LOG_DEBUG("Checking whether boost dll library is available."); + result = checkBoostDllAvailable(); + if (!result) { + return result; + } + STORM_LOG_DEBUG("Success."); + + STORM_LOG_DEBUG("Checking whether Storm's headers are available."); + result = checkStormAvailable(); + if (result) { + STORM_LOG_DEBUG("Success."); + } + return result; + } + + template + std::shared_ptr> ExplicitJitJaniModelBuilder::build() { + // (0) Assemble information about the model. + cpptempl::data_map modelData = generateModelData(); + + // (1) generate the source code of the shared library + std::string source; + try { + source = createSourceCodeFromSkeleton(modelData); + } catch (std::exception const& e) { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Could not create the source code for model generation (error: " << e.what() << ")."); + } + STORM_LOG_TRACE("Successfully created source code for model generation: " << source); + + // (2) Write the source code to a temporary file. + boost::filesystem::path temporarySourceFile = writeToTemporaryFile(source); + + // (3) Compile the source code to a shared library. + boost::filesystem::path dynamicLibraryPath = compileToSharedLibrary(temporarySourceFile); + STORM_LOG_TRACE("Successfully compiled shared library."); + + // (4) Remove the source code of the shared library we just compiled. + boost::filesystem::remove(temporarySourceFile); + + // (5) Create the builder from the shared library. + createBuilder(dynamicLibraryPath); + + // (6) Execute the build function of the builder in the shared library and build the actual model. + auto start = std::chrono::high_resolution_clock::now(); + auto sparseModel = builder->build(); + auto end = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Building model took " << std::chrono::duration_cast(end - start).count() << "ms."); + + // (7) Delete the shared library. + boost::filesystem::remove(dynamicLibraryPath); + + // Return the constructed model. + return std::shared_ptr>(sparseModel); + } + + template + cpptempl::data_map ExplicitJitJaniModelBuilder::generateModelData() { + cpptempl::data_map modelData; + // Generate trivial model-information. + modelData["deterministic_model"] = model.isDeterministicModel() ? "true" : "false"; + modelData["discrete_time_model"] = model.isDiscreteTimeModel() ? "true" : "false"; - class JitBuilder : public JitModelBuilderInterface { - public: - JitBuilder(ModelComponentsBuilder& modelComponentsBuilder) : JitModelBuilderInterface(modelComponentsBuilder) { - {% for state in initialStates %}{ - StateType state; - {% for assignment in state %}state.{$assignment.variable} = {$assignment.value}; - {% endfor %} - initialStates.push_back(state); - }{% endfor %} - {% for edge in nonsynch_edges %}{ - edge_{$edge.name} = Edge(&edge_enabled_{$edge.name}, edge_perform_{$edge.name}); - {% for destination in edge.destinations %}edge_{$edge.name}.addDestination({$destination.lowestLevel}, {$destination.highestLevel}, {$destination.value}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}); - {% endfor %} - } - {% endfor %} - {% for edge in synch_edges %}{ - edge_{$edge.name} = Edge(&edge_enabled_{$edge.name}, edge_perform_{$edge.name}); - {% for destination in edge.destinations %}edge_{$edge.name}.addDestination({$destination.lowestLevel}, {$destination.highestLevel}, {$destination.value}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}); - {% endfor %} - } - {% endfor %} - {% for reward in rewards %} - modelComponentsBuilder.registerRewardModel(RewardModelInformation("{$reward.name}", {$reward.location_rewards}, {$reward.edge_rewards} || {$reward.destination_rewards}, false)); - {% endfor %} - } - - virtual storm::models::sparse::Model>* build() override { - std::cout << "starting building process" << std::endl; - explore(initialStates); - std::cout << "finished building process with " << stateIds.size() << " states" << std::endl; - - std::cout << "building labeling" << std::endl; - label(); - std::cout << "finished building labeling" << std::endl; - - return this->modelComponentsBuilder.build(stateIds.size()); - } - - void label() { - uint64_t labelCount = 0; - {% for label in labels %}this->modelComponentsBuilder.registerLabel("{$label.name}", stateIds.size()); - ++labelCount; - {% endfor %} - this->modelComponentsBuilder.registerLabel("init", stateIds.size()); - this->modelComponentsBuilder.registerLabel("deadlock", stateIds.size()); - - for (auto const& stateEntry : stateIds) { - auto const& in = stateEntry.first; - {% for label in labels %}if ({$label.predicate}) { - this->modelComponentsBuilder.addLabel(stateEntry.second, {$loop.index} - 1); - } - {% endfor %} - } - - for (auto const& state : initialStates) { - auto stateIt = stateIds.find(state); - if (stateIt != stateIds.end()) { - this->modelComponentsBuilder.addLabel(stateIt->second, labelCount); - } - } - - for (auto const& stateId : deadlockStates) { - this->modelComponentsBuilder.addLabel(stateId, labelCount + 1); - } - } - - void explore(std::vector const& initialStates) { - for (auto const& state : initialStates) { - explore(state); - } - } - - void explore(StateType const& initialState) { - StateSet statesToExplore; - getOrAddIndex(initialState, statesToExplore); - - StateBehaviour behaviour; - while (!statesToExplore.empty()) { - StateType currentState = statesToExplore.get(); - IndexType currentIndex = getIndex(currentState); - - if (!isTerminalState(currentState)) { -#ifndef NDEBUG - std::cout << "Exploring state " << currentState << ", id " << currentIndex << std::endl; -#endif - - behaviour.setExpanded(); - - // Perform transient location assignments. - TransientVariables transientIn; - TransientVariables transientOut; - locations_perform(currentState, transientIn, transientOut); - {% for reward in location_rewards %} - behaviour.addStateReward(transientOut.{$reward.variable}); - {% endfor %} - - // Explore all edges that do not take part in synchronization vectors. - exploreNonSynchronizingEdges(currentState, behaviour, statesToExplore); - - // Explore all edges that participate in synchronization vectors. - exploreSynchronizingEdges(currentState, behaviour, statesToExplore); - } - - this->addStateBehaviour(currentIndex, behaviour); - behaviour.clear(); - } - } - - bool isTerminalState(StateType const& state) const { - {% for expression in terminalExpressions %}if ({$expression}) { - return true; - } - {% endfor %} - return false; - } - - void exploreNonSynchronizingEdges(StateType const& in, StateBehaviour& behaviour, StateSet& statesToExplore) { - {% for edge in nonsynch_edges %}{ - if ({$edge.guard}) { - Choice& choice = behaviour.addChoice(); - choice.resizeRewards({$edge_destination_rewards_count}, 0); - { - TransientVariables transient; - {% if edge.transient_assignments %} - edge_perform_{$edge.name}(in, transient, transient); - {% endif %} - {% for reward in edge_rewards %} - choice.addReward({$reward.index}, transient.{$reward.variable}); - {% endfor %} - } - {% for destination in edge.destinations %}{ - StateType out(in); - TransientVariables transientIn; - TransientVariables transientOut; - destination_perform_{$edge.name}_{$destination.name}(in, out{% if edge.transient_variables_in_destinations %}, transientIn, transientOut{% endif %}); - IndexType outStateIndex = getOrAddIndex(out, statesToExplore); - choice.add(outStateIndex, {$destination.value}); - {% for reward in destination_rewards %} - choice.addReward({$reward.index}, transientOut.{$reward.variable}); - {% endfor %} - } - {% endfor %} - } - } - {% endfor %} - } - - {% for vector in synch_vectors %}{$vector.functions} - {% endfor %} - - void exploreSynchronizingEdges(StateType const& state, StateBehaviour& behaviour, StateSet& statesToExplore) { - {% for vector in synch_vectors %}{ - exploreSynchronizationVector_{$vector.index}(state, behaviour, statesToExplore); - } - {% endfor %} - } - - IndexType getOrAddIndex(StateType const& state, StateSet& statesToExplore) { - auto it = stateIds.find(state); - if (it != stateIds.end()) { - return it->second; - } else { - IndexType newIndex = static_cast(stateIds.size()); - stateIds.insert(std::make_pair(state, newIndex)); -#ifndef NDEBUG - std::cout << "inserting state " << state << std::endl; -#endif - statesToExplore.add(state); - return newIndex; - } - } - - IndexType getIndex(StateType const& state) const { - auto it = stateIds.find(state); - if (it != stateIds.end()) { - return it->second; - } else { - return stateIds.at(state); - } - } - - void addStateBehaviour(IndexType const& stateId, StateBehaviour& behaviour) { - if (behaviour.empty()) { - deadlockStates.push_back(stateId); - } - - JitModelBuilderInterface::addStateBehaviour(stateId, behaviour); - } - - static JitModelBuilderInterface* create(ModelComponentsBuilder& modelComponentsBuilder) { - return new JitBuilder(modelComponentsBuilder); - } - - private: - spp::sparse_hash_map stateIds; - std::vector initialStates; - std::vector deadlockStates; - - {% for edge in nonsynch_edges %}Edge edge_{$edge.name}; - {% endfor %} - {% for edge in synch_edges %}Edge edge_{$edge.name}; - {% endfor %} - }; - - BOOST_DLL_ALIAS(storm::builder::jit::JitBuilder::create, create_builder) - } - } - } - )"; - - cpptempl::data_map modelData; + // Generate non-trivial model-information. generateVariables(modelData); - cpptempl::data_list initialStates = generateInitialStates(); - modelData["initialStates"] = cpptempl::make_data(initialStates); - - // We need to generate the reward information before the edges, because we already use it there. - generateRewards(modelData); + generateInitialStates(modelData); + generateRewards(modelData); // We need to generate the reward information before the edges, because we already use it there. generateEdges(modelData); generateLocations(modelData); - cpptempl::data_list labels = generateLabels(); - modelData["labels"] = cpptempl::make_data(labels); - cpptempl::data_list terminalExpressions = generateTerminalExpressions(); - modelData["terminalExpressions"] = cpptempl::make_data(terminalExpressions); - modelData["deterministic_model"] = model.isDeterministicModel() ? "true" : "false"; - modelData["discrete_time_model"] = model.isDiscreteTimeModel() ? "true" : "false"; - return cpptempl::parse(sourceTemplate, modelData); + generateLabels(modelData); + generateTerminalExpressions(modelData); + + return modelData; } template - cpptempl::data_list ExplicitJitJaniModelBuilder::generateInitialStates() { - cpptempl::data_list initialStates; + cpptempl::data_map ExplicitJitJaniModelBuilder::generateBooleanVariable(storm::jani::BooleanVariable const& variable) { + cpptempl::data_map result; + result["name"] = registerVariable(variable.getExpressionVariable(), variable.isTransient()); + if (variable.hasInitExpression()) { + result["init"] = asString(variable.getInitExpression().evaluateAsBool()); + } + return result; + } + + template + cpptempl::data_map ExplicitJitJaniModelBuilder::generateBoundedIntegerVariable(storm::jani::BoundedIntegerVariable const& variable) { + cpptempl::data_map result; - // Prepare an SMT solver to enumerate all initial states. - storm::utility::solver::SmtSolverFactory factory; - std::unique_ptr solver = factory.create(model.getExpressionManager()); + int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); + int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); - std::vector rangeExpressions = model.getAllRangeExpressions(); - for (auto const& expression : rangeExpressions) { - solver->add(expression); + lowerBounds[variable.getExpressionVariable()] = lowerBound; + if (lowerBound != 0) { + lowerBoundShiftSubstitution[variable.getExpressionVariable()] = variable.getExpressionVariable() + model.getManager().integer(lowerBound); } - solver->add(model.getInitialStatesExpression(parallelAutomata)); - - // Proceed as long as the solver can still enumerate initial states. - while (solver->check() == storm::solver::SmtSolver::CheckResult::Sat) { - // Create fresh state. - cpptempl::data_list initialStateAssignment; - - // Read variable assignment from the solution of the solver. Also, create an expression we can use to - // prevent the variable assignment from being enumerated again. - storm::expressions::Expression blockingExpression; - std::shared_ptr model = solver->getModel(); - for (auto const& variable : this->model.getGlobalVariables().getBooleanVariables()) { - storm::expressions::Variable const& expressionVariable = variable.getExpressionVariable(); - bool variableValue = model->getBooleanValue(expressionVariable); - initialStateAssignment.push_back(generateAssignment(variable, variableValue)); - - storm::expressions::Expression localBlockingExpression = variableValue ? !expressionVariable : expressionVariable; - blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; - } - for (auto const& variable : this->model.getGlobalVariables().getBoundedIntegerVariables()) { - storm::expressions::Variable const& expressionVariable = variable.getExpressionVariable(); - int_fast64_t variableValue = model->getIntegerValue(expressionVariable); - initialStateAssignment.push_back(generateAssignment(variable, variableValue)); - - storm::expressions::Expression localBlockingExpression = expressionVariable != model->getManager().integer(variableValue); - blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; - } - for (auto const& automatonRef : parallelAutomata) { - storm::jani::Automaton const& automaton = automatonRef.get(); - for (auto const& variable : automaton.getVariables().getBooleanVariables()) { - storm::expressions::Variable const& expressionVariable = variable.getExpressionVariable(); - bool variableValue = model->getBooleanValue(expressionVariable); - initialStateAssignment.push_back(generateAssignment(variable, variableValue)); - - storm::expressions::Expression localBlockingExpression = variableValue ? !expressionVariable : expressionVariable; - blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; - } - for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) { - storm::expressions::Variable const& expressionVariable = variable.getExpressionVariable(); - int_fast64_t variableValue = model->getIntegerValue(expressionVariable); - initialStateAssignment.push_back(generateAssignment(variable, variableValue)); - - storm::expressions::Expression localBlockingExpression = expressionVariable != model->getManager().integer(variableValue); - blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; - } - } - - // Gather iterators to the initial locations of all the automata. - std::vector::const_iterator> initialLocationsIterators; - for (auto const& automaton : parallelAutomata) { - initialLocationsIterators.push_back(automaton.get().getInitialLocationIndices().cbegin()); - } - - // Now iterate through all combinations of initial locations. - while (true) { - cpptempl::data_list completeAssignment(initialStateAssignment); - - for (uint64_t index = 0; index < initialLocationsIterators.size(); ++index) { - storm::jani::Automaton const& automaton = parallelAutomata[index].get(); - if (automaton.getNumberOfLocations() > 1) { - completeAssignment.push_back(generateLocationAssignment(automaton, *initialLocationsIterators[index])); - } - } - initialStates.push_back(cpptempl::make_data(completeAssignment)); - - uint64_t index = 0; - for (; index < initialLocationsIterators.size(); ++index) { - ++initialLocationsIterators[index]; - if (initialLocationsIterators[index] == parallelAutomata[index].get().getInitialLocationIndices().cend()) { - initialLocationsIterators[index] = parallelAutomata[index].get().getInitialLocationIndices().cbegin(); - } else { - break; - } - } - - // If we are at the end, leave the loop. - if (index == initialLocationsIterators.size()) { - break; - } - } - - // Block the current initial state to search for the next one. - if (!blockingExpression.isInitialized()) { - break; - } - solver->add(blockingExpression); - } - - return initialStates; - } - - template - cpptempl::data_map ExplicitJitJaniModelBuilder::generateBooleanVariable(storm::jani::BooleanVariable const& variable) { - cpptempl::data_map result; - result["name"] = registerVariable(variable.getExpressionVariable(), variable.isTransient()); - if (variable.hasInitExpression()) { - result["init"] = asString(variable.getInitExpression().evaluateAsBool()); - } - return result; - } - - template - cpptempl::data_map ExplicitJitJaniModelBuilder::generateBoundedIntegerVariable(storm::jani::BoundedIntegerVariable const& variable) { - cpptempl::data_map result; - - int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); - int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); - - lowerBounds[variable.getExpressionVariable()] = lowerBound; - if (lowerBound != 0) { - lowerBoundShiftSubstitution[variable.getExpressionVariable()] = variable.getExpressionVariable() + model.getManager().integer(lowerBound); - } - uint64_t range = static_cast(upperBound - lowerBound + 1); - uint64_t numberOfBits = static_cast(std::ceil(std::log2(range))); + uint64_t range = static_cast(upperBound - lowerBound + 1); + uint64_t numberOfBits = static_cast(std::ceil(std::log2(range))); result["name"] = registerVariable(variable.getExpressionVariable(), variable.isTransient()); result["numberOfBits"] = std::to_string(numberOfBits); if (variable.hasInitExpression()) { result["init"] = asString(variable.getInitExpression().evaluateAsInt() - lowerBound); } - + return result; } @@ -828,7 +498,7 @@ namespace storm { return result; } - + template cpptempl::data_map ExplicitJitJaniModelBuilder::generateRealVariable(storm::jani::RealVariable const& variable) { cpptempl::data_map result; @@ -837,10 +507,10 @@ namespace storm { if (variable.hasInitExpression()) { result["init"] = asString(variable.getInitExpression().evaluateAsDouble()); } - + return result; } - + template cpptempl::data_map ExplicitJitJaniModelBuilder::generateLocationVariable(storm::jani::Automaton const& automaton) { cpptempl::data_map result; @@ -850,7 +520,7 @@ namespace storm { return result; } - + template void ExplicitJitJaniModelBuilder::generateVariables(cpptempl::data_map& modelData) { cpptempl::data_list nonTransientBooleanVariables; @@ -953,34 +623,108 @@ namespace storm { } template - void ExplicitJitJaniModelBuilder::generateLocations(cpptempl::data_map& modelData) { - cpptempl::data_list locations; - - for (auto const& automatonRef : parallelAutomata) { - storm::jani::Automaton const& automaton = automatonRef.get(); - cpptempl::data_map locationData; - uint64_t locationIndex = 0; - for (auto const& location : automaton.getLocations()) { - cpptempl::data_list assignments; - for (auto const& assignment : location.getAssignments()) { - assignments.push_back(generateAssignment(assignment)); + void ExplicitJitJaniModelBuilder::generateInitialStates(cpptempl::data_map& modelData) { + cpptempl::data_list initialStates; + + // Prepare an SMT solver to enumerate all initial states. + storm::utility::solver::SmtSolverFactory factory; + std::unique_ptr solver = factory.create(model.getExpressionManager()); + + std::vector rangeExpressions = model.getAllRangeExpressions(); + for (auto const& expression : rangeExpressions) { + solver->add(expression); + } + solver->add(model.getInitialStatesExpression(parallelAutomata)); + + // Proceed as long as the solver can still enumerate initial states. + while (solver->check() == storm::solver::SmtSolver::CheckResult::Sat) { + // Create fresh state. + cpptempl::data_list initialStateAssignment; + + // Read variable assignment from the solution of the solver. Also, create an expression we can use to + // prevent the variable assignment from being enumerated again. + storm::expressions::Expression blockingExpression; + std::shared_ptr model = solver->getModel(); + for (auto const& variable : this->model.getGlobalVariables().getBooleanVariables()) { + storm::expressions::Variable const& expressionVariable = variable.getExpressionVariable(); + bool variableValue = model->getBooleanValue(expressionVariable); + initialStateAssignment.push_back(generateAssignment(variable, variableValue)); + + storm::expressions::Expression localBlockingExpression = variableValue ? !expressionVariable : expressionVariable; + blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; + } + for (auto const& variable : this->model.getGlobalVariables().getBoundedIntegerVariables()) { + storm::expressions::Variable const& expressionVariable = variable.getExpressionVariable(); + int_fast64_t variableValue = model->getIntegerValue(expressionVariable); + initialStateAssignment.push_back(generateAssignment(variable, variableValue)); + + storm::expressions::Expression localBlockingExpression = expressionVariable != model->getManager().integer(variableValue); + blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; + } + for (auto const& automatonRef : parallelAutomata) { + storm::jani::Automaton const& automaton = automatonRef.get(); + for (auto const& variable : automaton.getVariables().getBooleanVariables()) { + storm::expressions::Variable const& expressionVariable = variable.getExpressionVariable(); + bool variableValue = model->getBooleanValue(expressionVariable); + initialStateAssignment.push_back(generateAssignment(variable, variableValue)); + + storm::expressions::Expression localBlockingExpression = variableValue ? !expressionVariable : expressionVariable; + blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; } - locationData["assignments"] = cpptempl::make_data(assignments); - if (automaton.getNumberOfLocations() > 1) { - locationData["guard"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(getLocationVariable(automaton) == this->model.getManager().integer(locationIndex)), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); - } else { - locationData["guard"] = asString(true); + for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) { + storm::expressions::Variable const& expressionVariable = variable.getExpressionVariable(); + int_fast64_t variableValue = model->getIntegerValue(expressionVariable); + initialStateAssignment.push_back(generateAssignment(variable, variableValue)); + + storm::expressions::Expression localBlockingExpression = expressionVariable != model->getManager().integer(variableValue); + blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; } - ++locationIndex; } - if (!locationData["assignments"]->empty()) { - locations.push_back(locationData); + + // Gather iterators to the initial locations of all the automata. + std::vector::const_iterator> initialLocationsIterators; + for (auto const& automaton : parallelAutomata) { + initialLocationsIterators.push_back(automaton.get().getInitialLocationIndices().cbegin()); } - } - modelData["locations"] = cpptempl::make_data(locations); - } + // Now iterate through all combinations of initial locations. + while (true) { + cpptempl::data_list completeAssignment(initialStateAssignment); + + for (uint64_t index = 0; index < initialLocationsIterators.size(); ++index) { + storm::jani::Automaton const& automaton = parallelAutomata[index].get(); + if (automaton.getNumberOfLocations() > 1) { + completeAssignment.push_back(generateLocationAssignment(automaton, *initialLocationsIterators[index])); + } + } + initialStates.push_back(cpptempl::make_data(completeAssignment)); + + uint64_t index = 0; + for (; index < initialLocationsIterators.size(); ++index) { + ++initialLocationsIterators[index]; + if (initialLocationsIterators[index] == parallelAutomata[index].get().getInitialLocationIndices().cend()) { + initialLocationsIterators[index] = parallelAutomata[index].get().getInitialLocationIndices().cbegin(); + } else { + break; + } + } + + // If we are at the end, leave the loop. + if (index == initialLocationsIterators.size()) { + break; + } + } + + // Block the current initial state to search for the next one. + if (!blockingExpression.isInitialized()) { + break; + } + solver->add(blockingExpression); + } + modelData["initialStates"] = cpptempl::make_data(initialStates); + } + template void ExplicitJitJaniModelBuilder::generateRewards(cpptempl::data_map& modelData) { // Extract the reward models from the program based on the names we were given. @@ -1008,7 +752,7 @@ namespace storm { } STORM_LOG_ASSERT(foundTransientVariable, "Expected to find a fitting transient variable."); } - + std::vector rewardModels; cpptempl::data_list rewards; cpptempl::data_list locationRewards; @@ -1089,71 +833,18 @@ namespace storm { modelData["rewards"] = cpptempl::make_data(rewards); modelData["edge_destination_rewards_count"] = asString(stateActionRewardCount); } - - template - cpptempl::data_list ExplicitJitJaniModelBuilder::generateLabels() { - cpptempl::data_list labels; - - // As in JANI we can use transient boolean variable assignments in locations to identify states, we need to - // create a list of boolean transient variables and the expressions that define them. - for (auto const& variable : model.getGlobalVariables().getTransientVariables()) { - if (variable.isBooleanVariable()) { - if (this->options.isBuildAllLabelsSet() || this->options.getLabelNames().find(variable.getName()) != this->options.getLabelNames().end()) { - cpptempl::data_map label; - label["name"] = variable.getName(); - label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(model.getLabelExpression(variable.asBooleanVariable(), automatonToLocationVariable)), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); - labels.push_back(label); - } - } - } - - for (auto const& expression : this->options.getExpressionLabels()) { - cpptempl::data_map label; - label["name"] = expression.toString(); - label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(expression), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); - labels.push_back(label); + + static std::ostream& indent(std::ostream& out, uint64_t indentLevel) { + for (uint64_t i = 0; i < indentLevel; ++i) { + out << "\t"; } - - return labels; + return out; } - + template - cpptempl::data_list ExplicitJitJaniModelBuilder::generateTerminalExpressions() { - cpptempl::data_list terminalExpressions; - - for (auto const& terminalEntry : options.getTerminalStates()) { - LabelOrExpression const& labelOrExpression = terminalEntry.first; - if (labelOrExpression.isLabel()) { - auto const& variables = model.getGlobalVariables(); - STORM_LOG_THROW(variables.hasVariable(labelOrExpression.getLabel()), storm::exceptions::WrongFormatException, "Terminal label refers to unknown identifier '" << labelOrExpression.getLabel() << "'."); - auto const& variable = variables.getVariable(labelOrExpression.getLabel()); - STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::WrongFormatException, "Terminal label refers to non-boolean variable '" << variable.getName() << "."); - STORM_LOG_THROW(variable.isTransient(), storm::exceptions::WrongFormatException, "Terminal label refers to non-transient variable '" << variable.getName() << "."); - auto labelExpression = model.getLabelExpression(variable.asBooleanVariable(), automatonToLocationVariable); - if (terminalEntry.second) { - labelExpression = !labelExpression; - } - terminalExpressions.push_back(expressionTranslator.translate(shiftVariablesWrtLowerBound(labelExpression), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName))); - } else { - auto expression = terminalEntry.second ? labelOrExpression.getExpression() : !labelOrExpression.getExpression(); - terminalExpressions.push_back(expressionTranslator.translate(shiftVariablesWrtLowerBound(expression), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName))); - } - } - - return terminalExpressions; - } - - std::ostream& indent(std::ostream& out, uint64_t indentLevel) { - for (uint64_t i = 0; i < indentLevel; ++i) { - out << "\t"; - } - return out; - } - - template - cpptempl::data_map ExplicitJitJaniModelBuilder::generateSynchronizationVector(cpptempl::data_map& modelData, storm::jani::ParallelComposition const& parallelComposition, storm::jani::SynchronizationVector const& synchronizationVector, uint64_t synchronizationVectorIndex) { - std::stringstream vectorSource; - uint64_t numberOfActionInputs = synchronizationVector.getNumberOfActionInputs(); + cpptempl::data_map ExplicitJitJaniModelBuilder::generateSynchronizationVector(cpptempl::data_map& modelData, storm::jani::ParallelComposition const& parallelComposition, storm::jani::SynchronizationVector const& synchronizationVector, uint64_t synchronizationVectorIndex) { + std::stringstream vectorSource; + uint64_t numberOfActionInputs = synchronizationVector.getNumberOfActionInputs(); // First, we check whether we need to generate code for a) different assignment levels and b) transient variables. uint64_t position = 0; @@ -1275,7 +966,7 @@ namespace storm { indent(vectorSource, indentLevel + numberOfActionInputs - index) << "}" << std::endl; } indent(vectorSource, indentLevel) << "}" << std::endl << std::endl; - + for (uint64_t index = 0; index < numberOfActionInputs; ++index) { indent(vectorSource, indentLevel) << "void performSynchronizedEdges_" << synchronizationVectorIndex << "_" << index << "(StateType const& in, std::vector>> const& edges, StateBehaviour& behaviour, StateSet& statesToExplore"; if (index > 0) { @@ -1318,7 +1009,7 @@ namespace storm { vectorSource << "edge" << innerIndex << ", "; } vectorSource << " choice);" << std::endl; - + } indent(vectorSource, indentLevel + 1) << "}" << std::endl; indent(vectorSource, indentLevel) << "}" << std::endl << std::endl; @@ -1407,355 +1098,930 @@ namespace storm { uint64_t actionIndex = model.getActionIndex(inputActionName); synchronizingActions[position].insert(actionIndex); - storm::jani::Automaton const& automaton = model.getAutomaton(parallelComposition.getSubcomposition(position).asAutomatonComposition().getAutomatonName()); - bool hasParticipatingEdge = false; - for (auto const& edge : automaton.getEdges()) { - if (edge.getActionIndex() == actionIndex) { - hasParticipatingEdge = true; - break; + storm::jani::Automaton const& automaton = model.getAutomaton(parallelComposition.getSubcomposition(position).asAutomatonComposition().getAutomatonName()); + bool hasParticipatingEdge = false; + for (auto const& edge : automaton.getEdges()) { + if (edge.getActionIndex() == actionIndex) { + hasParticipatingEdge = true; + break; + } + } + + if (!hasParticipatingEdge) { + createVector = false; + } + } + ++position; + } + + if (createVector) { + cpptempl::data_map vector = generateSynchronizationVector(modelData, parallelComposition, synchronizationVector, synchronizationVectorIndex); + vectors.push_back(vector); + } + ++synchronizationVectorIndex; + } + + uint64_t position = 0; + for (auto const& composition : parallelComposition.getSubcompositions()) { + storm::jani::Automaton const& automaton = model.getAutomaton(composition->asAutomatonComposition().getAutomatonName()); + + // Add all edges with an action index that is not mentioned in any synchronization vector as + // non-synchronizing edges. + uint64_t edgeIndex = 0; + for (auto const& edge : automaton.getEdges()) { + if (synchronizingActions[position].find(edge.getActionIndex()) != synchronizingActions[position].end()) { + synchronizingEdges.push_back(generateEdge(automaton, edgeIndex, edge)); + } else { + nonSynchronizingEdges.push_back(generateEdge(automaton, edgeIndex, edge)); + } + ++edgeIndex; + } + + ++position; + } + } + + modelData["nonsynch_edges"] = cpptempl::make_data(nonSynchronizingEdges); + modelData["synch_edges"] = cpptempl::make_data(synchronizingEdges); + modelData["synch_vectors"] = cpptempl::make_data(vectors); + } + + template + cpptempl::data_map ExplicitJitJaniModelBuilder::generateEdge(storm::jani::Automaton const& automaton, uint64_t edgeIndex, storm::jani::Edge const& edge) { + cpptempl::data_map edgeData; + + std::set transientVariablesInEdge; + cpptempl::data_list edgeAssignments; + for (auto const& assignment : edge.getAssignments()) { + transientVariablesInEdge.insert(assignment.getExpressionVariable()); + std::set usedVariables = assignment.getAssignedExpression().getVariables(); + for (auto const& variable : usedVariables) { + if (transientVariables.find(variable) != transientVariables.end()) { + transientVariablesInEdge.insert(variable); + } + } + edgeAssignments.push_back(generateAssignment(assignment)); + } + + cpptempl::data_list destinations; + uint64_t destinationIndex = 0; + std::set transientVariablesInDestinations; + for (auto const& destination : edge.getDestinations()) { + destinations.push_back(generateDestination(destinationIndex, destination)); + + for (auto const& assignment : destination.getOrderedAssignments().getAllAssignments()) { + if (assignment.isTransient()) { + transientVariablesInDestinations.insert(assignment.getExpressionVariable()); + } + std::set usedVariables = assignment.getAssignedExpression().getVariables(); + for (auto const& variable : usedVariables) { + if (transientVariables.find(variable) != transientVariables.end()) { + transientVariablesInDestinations.insert(variable); + } + } + } + + ++destinationIndex; + } + + edgeData["guard"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(edge.getGuard()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); + edgeData["destinations"] = cpptempl::make_data(destinations); + edgeData["name"] = automaton.getName() + "_" + std::to_string(edgeIndex); + edgeData["transient_assignments"] = cpptempl::make_data(edgeAssignments); + + cpptempl::data_list transientVariablesInDestinationsData; + for (auto const& variable : transientVariablesInDestinations) { + transientVariablesInDestinationsData.push_back(getVariableName(variable)); + } + edgeData["transient_variables_in_destinations"] = cpptempl::make_data(transientVariablesInDestinationsData); + cpptempl::data_list transientVariablesInEdgeData; + for (auto const& variable : transientVariablesInEdge) { + transientVariablesInEdgeData.push_back(getVariableName(variable)); + } + edgeData["transient_variables_in_edge"] = cpptempl::make_data(transientVariablesInEdgeData); + return edgeData; + } + + template + cpptempl::data_map ExplicitJitJaniModelBuilder::generateDestination(uint64_t destinationIndex, storm::jani::EdgeDestination const& destination) { + cpptempl::data_map destinationData; + + cpptempl::data_list levels = generateLevels(destination.getOrderedAssignments()); + destinationData["name"] = asString(destinationIndex); + destinationData["levels"] = cpptempl::make_data(levels); + destinationData["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(destination.getProbability()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, "double")); + if (destination.getOrderedAssignments().empty()) { + destinationData["lowestLevel"] = "0"; + destinationData["highestLevel"] = "0"; + } else { + destinationData["lowestLevel"] = asString(destination.getOrderedAssignments().getLowestLevel()); + destinationData["highestLevel"] = asString(destination.getOrderedAssignments().getHighestLevel()); + } + + return destinationData; + } + + template + cpptempl::data_list ExplicitJitJaniModelBuilder::generateLevels(storm::jani::OrderedAssignments const& orderedAssignments) { + cpptempl::data_list levels; + + auto const& assignments = orderedAssignments.getAllAssignments(); + if (!assignments.empty()) { + int_fast64_t currentLevel = assignments.begin()->getLevel(); + + cpptempl::data_list nonTransientAssignmentData; + cpptempl::data_list transientAssignmentData; + for (auto const& assignment : assignments) { + if (assignment.getLevel() != currentLevel) { + cpptempl::data_map level; + level["non_transient_assignments"] = cpptempl::make_data(nonTransientAssignmentData); + level["transient_assignments"] = cpptempl::make_data(transientAssignmentData); + level["index"] = asString(currentLevel); + levels.push_back(level); + + nonTransientAssignmentData = cpptempl::data_list(); + transientAssignmentData = cpptempl::data_list(); + currentLevel = assignment.getLevel(); + } + + if (assignment.isTransient()) { + transientAssignmentData.push_back(generateAssignment(assignment)); + } else { + nonTransientAssignmentData.push_back(generateAssignment(assignment)); + } + } + + // Close the last (open) level. + cpptempl::data_map level; + level["non_transient_assignments"] = cpptempl::make_data(nonTransientAssignmentData); + level["transient_assignments"] = cpptempl::make_data(transientAssignmentData); + level["index"] = asString(currentLevel); + levels.push_back(level); + } + + return levels; + } + + template + template + cpptempl::data_map ExplicitJitJaniModelBuilder::generateAssignment(storm::jani::Variable const& variable, ValueTypePrime value) const { + cpptempl::data_map result; + result["variable"] = getVariableName(variable.getExpressionVariable()); + result["value"] = asString(value); + return result; + } + + template + cpptempl::data_map ExplicitJitJaniModelBuilder::generateLocationAssignment(storm::jani::Automaton const& automaton, uint64_t value) const { + cpptempl::data_map result; + result["variable"] = getVariableName(getLocationVariable(automaton)); + result["value"] = asString(value); + return result; + } + + template + cpptempl::data_map ExplicitJitJaniModelBuilder::generateAssignment(storm::jani::Assignment const& assignment) { + cpptempl::data_map result; + result["variable"] = getVariableName(assignment.getExpressionVariable()); + auto lowerBoundIt = lowerBounds.find(assignment.getExpressionVariable()); + if (lowerBoundIt != lowerBounds.end()) { + if (lowerBoundIt->second < 0) { + result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) + model.getManager().integer(lowerBoundIt->second), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); + } else if (lowerBoundIt->second == 0) { + result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); + } else { + result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) - model.getManager().integer(lowerBoundIt->second), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); + } + } else { + result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); + } + return result; + } + + template + void ExplicitJitJaniModelBuilder::generateLocations(cpptempl::data_map& modelData) { + cpptempl::data_list locations; + + for (auto const& automatonRef : parallelAutomata) { + storm::jani::Automaton const& automaton = automatonRef.get(); + cpptempl::data_map locationData; + uint64_t locationIndex = 0; + for (auto const& location : automaton.getLocations()) { + cpptempl::data_list assignments; + for (auto const& assignment : location.getAssignments()) { + assignments.push_back(generateAssignment(assignment)); + } + locationData["assignments"] = cpptempl::make_data(assignments); + if (automaton.getNumberOfLocations() > 1) { + locationData["guard"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(getLocationVariable(automaton) == this->model.getManager().integer(locationIndex)), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); + } else { + locationData["guard"] = asString(true); + } + ++locationIndex; + } + if (!locationData["assignments"]->empty()) { + locations.push_back(locationData); + } + } + + modelData["locations"] = cpptempl::make_data(locations); + } + + template + void ExplicitJitJaniModelBuilder::generateLabels(cpptempl::data_map& modelData) { + cpptempl::data_list labels; + + // As in JANI we can use transient boolean variable assignments in locations to identify states, we need to + // create a list of boolean transient variables and the expressions that define them. + for (auto const& variable : model.getGlobalVariables().getTransientVariables()) { + if (variable.isBooleanVariable()) { + if (this->options.isBuildAllLabelsSet() || this->options.getLabelNames().find(variable.getName()) != this->options.getLabelNames().end()) { + cpptempl::data_map label; + label["name"] = variable.getName(); + label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(model.getLabelExpression(variable.asBooleanVariable(), automatonToLocationVariable)), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); + labels.push_back(label); + } + } + } + + for (auto const& expression : this->options.getExpressionLabels()) { + cpptempl::data_map label; + label["name"] = expression.toString(); + label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(expression), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); + labels.push_back(label); + } + + modelData["labels"] = cpptempl::make_data(labels); + } + + template + void ExplicitJitJaniModelBuilder::generateTerminalExpressions(cpptempl::data_map& modelData) { + cpptempl::data_list terminalExpressions; + + for (auto const& terminalEntry : options.getTerminalStates()) { + LabelOrExpression const& labelOrExpression = terminalEntry.first; + if (labelOrExpression.isLabel()) { + auto const& variables = model.getGlobalVariables(); + STORM_LOG_THROW(variables.hasVariable(labelOrExpression.getLabel()), storm::exceptions::WrongFormatException, "Terminal label refers to unknown identifier '" << labelOrExpression.getLabel() << "'."); + auto const& variable = variables.getVariable(labelOrExpression.getLabel()); + STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::WrongFormatException, "Terminal label refers to non-boolean variable '" << variable.getName() << "."); + STORM_LOG_THROW(variable.isTransient(), storm::exceptions::WrongFormatException, "Terminal label refers to non-transient variable '" << variable.getName() << "."); + auto labelExpression = model.getLabelExpression(variable.asBooleanVariable(), automatonToLocationVariable); + if (terminalEntry.second) { + labelExpression = !labelExpression; + } + terminalExpressions.push_back(expressionTranslator.translate(shiftVariablesWrtLowerBound(labelExpression), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName))); + } else { + auto expression = terminalEntry.second ? labelOrExpression.getExpression() : !labelOrExpression.getExpression(); + terminalExpressions.push_back(expressionTranslator.translate(shiftVariablesWrtLowerBound(expression), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName))); + } + } + + modelData["terminalExpressions"] = cpptempl::make_data(terminalExpressions); + } + + template + std::string const& ExplicitJitJaniModelBuilder::getVariableName(storm::expressions::Variable const& variable) const { + return variableToName.at(variable); + } + + template + std::string const& ExplicitJitJaniModelBuilder::registerVariable(storm::expressions::Variable const& variable, bool transient) { + // Since the variable name might be illegal as a C++ identifier, we need to prepare it a bit. + variableToName[variable] = variable.getName() + "_jit_"; + if (transient) { + transientVariables.insert(variable); + variablePrefixes[variable] = "transientIn."; + } else { + nontransientVariables.insert(variable); + variablePrefixes[variable] = "in."; + } + return variableToName[variable]; + } + + template + storm::expressions::Variable const& ExplicitJitJaniModelBuilder::getLocationVariable(storm::jani::Automaton const& automaton) const { + return automatonToLocationVariable.at(automaton.getName()); + } + + template + std::string ExplicitJitJaniModelBuilder::asString(bool value) const { + std::stringstream out; + out << std::boolalpha << value; + return out.str(); + } + + template + storm::expressions::Expression ExplicitJitJaniModelBuilder::shiftVariablesWrtLowerBound(storm::expressions::Expression const& expression) { + return expression.substitute(lowerBoundShiftSubstitution); + } + + template + template + std::string ExplicitJitJaniModelBuilder::asString(ValueTypePrime value) const { + return std::to_string(value); + } + + template + std::string ExplicitJitJaniModelBuilder::createSourceCodeFromSkeleton(cpptempl::data_map& modelData) { + std::string sourceTemplate = R"( +#define NDEBUG + +#include +#include +#include +#include +#include +#include +#include + +#include "resources/3rdparty/sparsepp/sparsepp.h" + +#include "src/builder/jit/StateSet.h" +#include "src/builder/jit/JitModelBuilderInterface.h" +#include "src/builder/jit/StateBehaviour.h" +#include "src/builder/jit/ModelComponentsBuilder.h" +#include "src/builder/RewardModelInformation.h" + + namespace storm { + namespace builder { + namespace jit { + + typedef uint32_t IndexType; + typedef double ValueType; + + struct StateType { + // Boolean variables. + {% for variable in nontransient_variables.boolean %}bool {$variable.name} : 1; + {% endfor %} + // Bounded integer variables. + {% for variable in nontransient_variables.boundedInteger %}uint64_t {$variable.name} : {$variable.numberOfBits}; + {% endfor %} + // Unbounded integer variables. + {% for variable in nontransient_variables.unboundedInteger %}int64_t {$variable.name}; + {% endfor %} + // Real variables. + {% for variable in nontransient_variables.real %}double {$variable.name}; + {% endfor %} + // Location variables. + {% for variable in nontransient_variables.locations %}uint64_t {$variable.name} : {$variable.numberOfBits}; + {% endfor %} + }; + + bool operator==(StateType const& first, StateType const& second) { + bool result = true; + {% for variable in nontransient_variables.boolean %}result &= !(first.{$variable.name} ^ second.{$variable.name}); + {% endfor %} + {% for variable in nontransient_variables.boundedInteger %}result &= first.{$variable.name} == second.{$variable.name}; + {% endfor %} + {% for variable in nontransient_variables.unboundedInteger %}result &= first.{$variable.name} == second.{$variable.name}; + {% endfor %} + {% for variable in nontransient_variables.real %}result &= first.{$variable.name} == second.{$variable.name}; + {% endfor %} + {% for variable in nontransient_variables.locations %}result &= first.{$variable.name} == second.{$variable.name}; + {% endfor %} + return result; + } + + std::ostream& operator<<(std::ostream& out, StateType const& in) { + out << "<"; + {% for variable in nontransient_variables.boolean %}out << "{$variable.name}=" << std::boolalpha << in.{$variable.name} << ", " << std::noboolalpha; + {% endfor %} + {% for variable in nontransient_variables.boundedInteger %}out << "{$variable.name}=" << in.{$variable.name} << ", "; + {% endfor %} + {% for variable in nontransient_variables.unboundedInteger %}out << "{$variable.name}=" << in.{$variable.name} << ", "; + {% endfor %} + {% for variable in nontransient_variables.real %}out << "{$variable.name}=" << in.{$variable.name} << ", "; + {% endfor %} + {% for variable in nontransient_variables.locations %}out << "{$variable.name}=" << in.{$variable.name} << ", "; + {% endfor %} + out << ">"; + return out; + } + + struct TransientVariables { + TransientVariables() { + reset(); + } + + void reset() { + {% for variable in transient_variables.boolean %}{$variable.name} = {$variable.init}; + {% endfor %} + {% for variable in transient_variables.boundedInteger %}{$variable.name} = {$variable.init}; + {% endfor %} + {% for variable in transient_variables.unboundedInteger %}{$variable.name} = {$variable.init}; + {% endfor %} + {% for variable in transient_variables.real %}{$variable.name} = {$variable.init}; + {% endfor %} + } + + // Boolean variables. + {% for variable in transient_variables.boolean %}bool {$variable.name} : 1; + {% endfor %} + // Bounded integer variables. + {% for variable in transient_variables.boundedInteger %}uint64_t {$variable.name} : {$variable.numberOfBits}; + {% endfor %} + // Unbounded integer variables. + {% for variable in transient_variables.unboundedInteger %}int64_t {$variable.name}; + {% endfor %} + // Real variables. + {% for variable in transient_variables.real %}double {$variable.name}; + {% endfor %} + }; + + std::ostream& operator<<(std::ostream& out, TransientVariables const& in) { + out << "<"; + {% for variable in transient_variables.boolean %}out << "{$variable.name}=" << std::boolalpha << in.{$variable.name} << ", " << std::noboolalpha; + {% endfor %} + {% for variable in transient_variables.boundedInteger %}out << "{$variable.name}=" << in.{$variable.name} << ", "; + {% endfor %} + {% for variable in transient_variables.unboundedInteger %}out << "{$variable.name}=" << in.{$variable.name} << ", "; + {% endfor %} + {% for variable in transient_variables.real %}out << "{$variable.name}=" << in.{$variable.name} << ", "; + {% endfor %} + out << ">"; + return out; + } + + } + } + } + + namespace std { + template <> + struct hash { + std::size_t operator()(storm::builder::jit::StateType const& in) const { + // Note: this is faster than viewing the struct as a bit field and taking hash_combine of the bytes. + std::size_t seed = 0; + {% for variable in nontransient_variables.boolean %}spp::hash_combine(seed, in.{$variable.name}); + {% endfor %} + {% for variable in nontransient_variables.boundedInteger %}spp::hash_combine(seed, in.{$variable.name}); + {% endfor %} + {% for variable in nontransient_variables.unboundedInteger %}spp::hash_combine(seed, in.{$variable.name}); + {% endfor %} + {% for variable in nontransient_variables.real %}spp::hash_combine(seed, in.{$variable.name}); + {% endfor %} + {% for variable in nontransient_variables.locations %}spp::hash_combine(seed, in.{$variable.name}); + {% endfor %} + return seed; + } + }; + } + + namespace storm { + namespace builder { + namespace jit { + + static bool model_is_deterministic() { + return {$deterministic_model}; + } + + static bool model_is_discrete_time() { + return {$discrete_time_model}; + } + + // Non-synchronizing edges. + {% for edge in nonsynch_edges %}static bool edge_enabled_{$edge.name}(StateType const& in) { + if ({$edge.guard}) { + return true; + } + return false; + } + + static void edge_perform_{$edge.name}(StateType const& in, TransientVariables const& transientIn, TransientVariables& transientOut) { + {% for assignment in edge.transient_assignments %}transientOut.{$assignment.variable} = {$assignment.value}; + {% endfor %} + } + + {% for destination in edge.destinations %} + static void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType const& in, StateType& out) { + {% for level in destination.levels %}if (level == {$level.index}) { + {% for assignment in level.non_transient_assignments %}out.{$assignment.variable} = {$assignment.value}; + {% endfor %} + } + {% endfor %} + } + + static void destination_perform_{$edge.name}_{$destination.name}(StateType const& in, StateType& out) { + {% for level in destination.levels %} + destination_perform_level_{$edge.name}_{$destination.name}({$level.index}, in, out); + {% endfor %} + } + + static void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType const& in, StateType& out, TransientVariables const& transientIn, TransientVariables& transientOut) { + {% for level in destination.levels %}if (level == {$level.index}) { + {% for assignment in level.non_transient_assignments %}out.{$assignment.variable} = {$assignment.value}; + {% endfor %} + {% for assignment in level.transient_assignments %}transientOut.{$assignment.variable} = {$assignment.value}; + {% endfor %} + } + {% endfor %} + } + + static void destination_perform_{$edge.name}_{$destination.name}(StateType const& in, StateType& out, TransientVariables const& transientIn, TransientVariables& transientOut) { + {% for level in destination.levels %} + destination_perform_level_{$edge.name}_{$destination.name}({$level.index}, in, out, transientIn, transientOut); + {% endfor %} + } + {% endfor %}{% endfor %} + + // Synchronizing edges. + {% for edge in synch_edges %}static bool edge_enabled_{$edge.name}(StateType const& in) { + if ({$edge.guard}) { + return true; + } + return false; + } + + static void edge_perform_{$edge.name}(StateType const& in, TransientVariables const& transientIn, TransientVariables& transientOut) { + {% for assignment in edge.transient_assignments %}transientOut.{$assignment.variable} = {$assignment.value}; + {% endfor %} + } + + {% for destination in edge.destinations %} + static void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType const& in, StateType& out) { + {% for level in destination.levels %}if (level == {$level.index}) { + {% for assignment in level.non_transient_assignments %}out.{$assignment.variable} = {$assignment.value}; + {% endfor %} + } + {% endfor %} + } + + static void destination_perform_{$edge.name}_{$destination.name}(StateType const& in, StateType& out) { + {% for level in destination.levels %} + destination_perform_level_{$edge.name}_{$destination.name}({$level.index}, in, out); + {% endfor %} + } + + static void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType const& in, StateType& out, TransientVariables const& transientIn, TransientVariables& transientOut) { + {% for level in destination.levels %}if (level == {$level.index}) { + {% for assignment in level.non_transient_assignments %}out.{$assignment.variable} = {$assignment.value}; + {% endfor %} + {% for assignment in level.transient_assignments %}transientOut.{$assignment.variable} = {$assignment.value}; + {% endfor %} + } + {% endfor %} + } + + static void destination_perform_{$edge.name}_{$destination.name}(StateType const& in, StateType& out, TransientVariables const& transientIn, TransientVariables& transientOut) { + {% for level in destination.levels %} + destination_perform_level_{$edge.name}_{$destination.name}({$level.index}, in, out, transientIn, transientOut); + {% endfor %} + } + {% endfor %}{% endfor %} + + typedef void (*DestinationLevelFunctionPtr)(int_fast64_t, StateType const&, StateType&, TransientVariables const&, TransientVariables&); + typedef void (*DestinationFunctionPtr)(StateType const&, StateType&, TransientVariables const&, TransientVariables&); + typedef void (*DestinationWithoutTransientLevelFunctionPtr)(int_fast64_t, StateType const&, StateType&); + typedef void (*DestinationWithoutTransientFunctionPtr)(StateType const&, StateType&); + + class Destination { + public: + Destination() : mLowestLevel(0), mHighestLevel(0), mValue(), destinationLevelFunction(nullptr), destinationFunction(nullptr), destinationWithoutTransientLevelFunction(nullptr), destinationWithoutTransientFunction(nullptr) { + // Intentionally left empty. + } + + Destination(int_fast64_t lowestLevel, int_fast64_t highestLevel, ValueType const& value, DestinationLevelFunctionPtr destinationLevelFunction, DestinationFunctionPtr destinationFunction, DestinationWithoutTransientLevelFunctionPtr destinationWithoutTransientLevelFunction, DestinationWithoutTransientFunctionPtr destinationWithoutTransientFunction) : mLowestLevel(lowestLevel), mHighestLevel(highestLevel), mValue(value), destinationLevelFunction(destinationLevelFunction), destinationFunction(destinationFunction), destinationWithoutTransientLevelFunction(destinationWithoutTransientLevelFunction), destinationWithoutTransientFunction(destinationWithoutTransientFunction) { + // Intentionally left empty. + } + + int_fast64_t lowestLevel() const { + return mLowestLevel; + } + + int_fast64_t highestLevel() const { + return mHighestLevel; + } + + ValueType const& value() const { + return mValue; + } + + void perform(int_fast64_t level, StateType const& in, StateType& out, TransientVariables const& transientIn, TransientVariables& transientOut) const { + destinationLevelFunction(level, in, out, transientIn, transientOut); + } + + void perform(StateType const& in, StateType& out, TransientVariables const& transientIn, TransientVariables& transientOut) const { + destinationFunction(in, out, transientIn, transientOut); + } + + void perform(int_fast64_t level, StateType const& in, StateType& out) const { + destinationWithoutTransientLevelFunction(level, in, out); + } + + void perform(StateType const& in, StateType& out) const { + destinationWithoutTransientFunction(in, out); + } + + private: + int_fast64_t mLowestLevel; + int_fast64_t mHighestLevel; + ValueType mValue; + DestinationLevelFunctionPtr destinationLevelFunction; + DestinationFunctionPtr destinationFunction; + DestinationWithoutTransientLevelFunctionPtr destinationWithoutTransientLevelFunction; + DestinationWithoutTransientFunctionPtr destinationWithoutTransientFunction; + }; + + typedef bool (*EdgeEnabledFunctionPtr)(StateType const&); + typedef void (*EdgeTransientFunctionPtr)(StateType const&, TransientVariables const& transientIn, TransientVariables& out); + + class Edge { + public: + typedef std::vector ContainerType; + + Edge() : edgeEnabledFunction(nullptr), edgeTransientFunction(nullptr) { + // Intentionally left empty. + } + + Edge(EdgeEnabledFunctionPtr edgeEnabledFunction, EdgeTransientFunctionPtr edgeTransientFunction = nullptr) : edgeEnabledFunction(edgeEnabledFunction), edgeTransientFunction(edgeTransientFunction) { + // Intentionally left empty. + } + + bool isEnabled(StateType const& in) const { + return edgeEnabledFunction(in); + } + + void addDestination(Destination const& destination) { + destinations.push_back(destination); + } + + void addDestination(int_fast64_t lowestLevel, int_fast64_t highestLevel, ValueType const& value, DestinationLevelFunctionPtr destinationLevelFunction, DestinationFunctionPtr destinationFunction, DestinationWithoutTransientLevelFunctionPtr destinationWithoutTransientLevelFunction, DestinationWithoutTransientFunctionPtr destinationWithoutTransientFunction) { + destinations.emplace_back(lowestLevel, highestLevel, value, destinationLevelFunction, destinationFunction, destinationWithoutTransientLevelFunction, destinationWithoutTransientFunction); + } + + std::vector const& getDestinations() const { + return destinations; + } + + ContainerType::const_iterator begin() const { + return destinations.begin(); + } + + ContainerType::const_iterator end() const { + return destinations.end(); + } + + void perform(StateType const& in, TransientVariables const& transientIn, TransientVariables& transientOut) const { + edgeTransientFunction(in, transientIn, transientOut); + } + + private: + EdgeEnabledFunctionPtr edgeEnabledFunction; + EdgeTransientFunctionPtr edgeTransientFunction; + ContainerType destinations; + }; + + void locations_perform(StateType const& in, TransientVariables const& transientIn, TransientVariables& transientOut) { + {% for location in locations %}if ({$location.guard}) { + {% for assignment in location.assignments %}transientOut.{$assignment.variable} = {$assignment.value};{% endfor %} + } + {% endfor %} + } + + class JitBuilder : public JitModelBuilderInterface { + public: + JitBuilder(ModelComponentsBuilder& modelComponentsBuilder) : JitModelBuilderInterface(modelComponentsBuilder) { + {% for state in initialStates %}{ + StateType state; + {% for assignment in state %}state.{$assignment.variable} = {$assignment.value}; + {% endfor %} + initialStates.push_back(state); + }{% endfor %} + {% for edge in nonsynch_edges %}{ + edge_{$edge.name} = Edge(&edge_enabled_{$edge.name}, edge_perform_{$edge.name}); + {% for destination in edge.destinations %}edge_{$edge.name}.addDestination({$destination.lowestLevel}, {$destination.highestLevel}, {$destination.value}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}); + {% endfor %} + } + {% endfor %} + {% for edge in synch_edges %}{ + edge_{$edge.name} = Edge(&edge_enabled_{$edge.name}, edge_perform_{$edge.name}); + {% for destination in edge.destinations %}edge_{$edge.name}.addDestination({$destination.lowestLevel}, {$destination.highestLevel}, {$destination.value}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name}); + {% endfor %} + } + {% endfor %} + {% for reward in rewards %} + modelComponentsBuilder.registerRewardModel(RewardModelInformation("{$reward.name}", {$reward.location_rewards}, {$reward.edge_rewards} || {$reward.destination_rewards}, false)); + {% endfor %} + } + + virtual storm::models::sparse::Model>* build() override { +#ifndef NDEBUG + std::cout << "starting building process" << std::endl; +#endif + explore(initialStates); +#ifndef NDEBUG + std::cout << "finished building process with " << stateIds.size() << " states" << std::endl; +#endif + +#ifndef NDEBUG + std::cout << "building labeling" << std::endl; +#endif + label(); +#ifndef NDEBUG + std::cout << "finished building labeling" << std::endl; +#endif + + return this->modelComponentsBuilder.build(stateIds.size()); + } + + void label() { + uint64_t labelCount = 0; + {% for label in labels %}this->modelComponentsBuilder.registerLabel("{$label.name}", stateIds.size()); + ++labelCount; + {% endfor %} + this->modelComponentsBuilder.registerLabel("init", stateIds.size()); + this->modelComponentsBuilder.registerLabel("deadlock", stateIds.size()); + + for (auto const& stateEntry : stateIds) { + auto const& in = stateEntry.first; + {% for label in labels %}if ({$label.predicate}) { + this->modelComponentsBuilder.addLabel(stateEntry.second, {$loop.index} - 1); + } + {% endfor %} + } + + for (auto const& state : initialStates) { + auto stateIt = stateIds.find(state); + if (stateIt != stateIds.end()) { + this->modelComponentsBuilder.addLabel(stateIt->second, labelCount); + } + } + + for (auto const& stateId : deadlockStates) { + this->modelComponentsBuilder.addLabel(stateId, labelCount + 1); } } - if (!hasParticipatingEdge) { - createVector = false; + void explore(std::vector const& initialStates) { + for (auto const& state : initialStates) { + explore(state); + } } - } - ++position; - } - - if (createVector) { - cpptempl::data_map vector = generateSynchronizationVector(modelData, parallelComposition, synchronizationVector, synchronizationVectorIndex); - vectors.push_back(vector); - } - ++synchronizationVectorIndex; - } - - uint64_t position = 0; - for (auto const& composition : parallelComposition.getSubcompositions()) { - storm::jani::Automaton const& automaton = model.getAutomaton(composition->asAutomatonComposition().getAutomatonName()); - - // Add all edges with an action index that is not mentioned in any synchronization vector as - // non-synchronizing edges. - uint64_t edgeIndex = 0; - for (auto const& edge : automaton.getEdges()) { - if (synchronizingActions[position].find(edge.getActionIndex()) != synchronizingActions[position].end()) { - synchronizingEdges.push_back(generateEdge(automaton, edgeIndex, edge)); - } else { - nonSynchronizingEdges.push_back(generateEdge(automaton, edgeIndex, edge)); - } - ++edgeIndex; - } - - ++position; - } - } - - modelData["nonsynch_edges"] = cpptempl::make_data(nonSynchronizingEdges); - modelData["synch_edges"] = cpptempl::make_data(synchronizingEdges); - modelData["synch_vectors"] = cpptempl::make_data(vectors); - } - - template - cpptempl::data_map ExplicitJitJaniModelBuilder::generateEdge(storm::jani::Automaton const& automaton, uint64_t edgeIndex, storm::jani::Edge const& edge) { - cpptempl::data_map edgeData; - - std::set transientVariablesInEdge; - cpptempl::data_list edgeAssignments; - for (auto const& assignment : edge.getAssignments()) { - transientVariablesInEdge.insert(assignment.getExpressionVariable()); - std::set usedVariables = assignment.getAssignedExpression().getVariables(); - for (auto const& variable : usedVariables) { - if (transientVariables.find(variable) != transientVariables.end()) { - transientVariablesInEdge.insert(variable); - } - } - edgeAssignments.push_back(generateAssignment(assignment)); - } - - cpptempl::data_list destinations; - uint64_t destinationIndex = 0; - std::set transientVariablesInDestinations; - for (auto const& destination : edge.getDestinations()) { - destinations.push_back(generateDestination(destinationIndex, destination)); - - for (auto const& assignment : destination.getOrderedAssignments().getAllAssignments()) { - if (assignment.isTransient()) { - transientVariablesInDestinations.insert(assignment.getExpressionVariable()); - } - std::set usedVariables = assignment.getAssignedExpression().getVariables(); - for (auto const& variable : usedVariables) { - if (transientVariables.find(variable) != transientVariables.end()) { - transientVariablesInDestinations.insert(variable); - } - } - } - - ++destinationIndex; - } - - edgeData["guard"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(edge.getGuard()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); - edgeData["destinations"] = cpptempl::make_data(destinations); - edgeData["name"] = automaton.getName() + "_" + std::to_string(edgeIndex); - edgeData["transient_assignments"] = cpptempl::make_data(edgeAssignments); - - cpptempl::data_list transientVariablesInDestinationsData; - for (auto const& variable : transientVariablesInDestinations) { - transientVariablesInDestinationsData.push_back(getVariableName(variable)); - } - edgeData["transient_variables_in_destinations"] = cpptempl::make_data(transientVariablesInDestinationsData); - cpptempl::data_list transientVariablesInEdgeData; - for (auto const& variable : transientVariablesInEdge) { - transientVariablesInEdgeData.push_back(getVariableName(variable)); - } - edgeData["transient_variables_in_edge"] = cpptempl::make_data(transientVariablesInEdgeData); - return edgeData; - } - - template - cpptempl::data_map ExplicitJitJaniModelBuilder::generateDestination(uint64_t destinationIndex, storm::jani::EdgeDestination const& destination) { - cpptempl::data_map destinationData; - - cpptempl::data_list levels = generateLevels(destination.getOrderedAssignments()); - destinationData["name"] = asString(destinationIndex); - destinationData["levels"] = cpptempl::make_data(levels); - destinationData["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(destination.getProbability()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, "double")); - if (destination.getOrderedAssignments().empty()) { - destinationData["lowestLevel"] = "0"; - destinationData["highestLevel"] = "0"; - } else { - destinationData["lowestLevel"] = asString(destination.getOrderedAssignments().getLowestLevel()); - destinationData["highestLevel"] = asString(destination.getOrderedAssignments().getHighestLevel()); - } - - return destinationData; - } - - template - cpptempl::data_list ExplicitJitJaniModelBuilder::generateLevels(storm::jani::OrderedAssignments const& orderedAssignments) { - cpptempl::data_list levels; - - auto const& assignments = orderedAssignments.getAllAssignments(); - if (!assignments.empty()) { - int_fast64_t currentLevel = assignments.begin()->getLevel(); - - cpptempl::data_list nonTransientAssignmentData; - cpptempl::data_list transientAssignmentData; - for (auto const& assignment : assignments) { - if (assignment.getLevel() != currentLevel) { - cpptempl::data_map level; - level["non_transient_assignments"] = cpptempl::make_data(nonTransientAssignmentData); - level["transient_assignments"] = cpptempl::make_data(transientAssignmentData); - level["index"] = asString(currentLevel); - levels.push_back(level); + + void explore(StateType const& initialState) { + StateSet statesToExplore; + getOrAddIndex(initialState, statesToExplore); + + StateBehaviour behaviour; + while (!statesToExplore.empty()) { + StateType currentState = statesToExplore.get(); + IndexType currentIndex = getIndex(currentState); + + if (!isTerminalState(currentState)) { +#ifndef NDEBUG + std::cout << "Exploring state " << currentState << ", id " << currentIndex << std::endl; +#endif + + behaviour.setExpanded(); + + // Perform transient location assignments. + TransientVariables transientIn; + TransientVariables transientOut; + locations_perform(currentState, transientIn, transientOut); + {% for reward in location_rewards %} + behaviour.addStateReward(transientOut.{$reward.variable}); + {% endfor %} + + // Explore all edges that do not take part in synchronization vectors. + exploreNonSynchronizingEdges(currentState, behaviour, statesToExplore); + + // Explore all edges that participate in synchronization vectors. + exploreSynchronizingEdges(currentState, behaviour, statesToExplore); + } + + this->addStateBehaviour(currentIndex, behaviour); + behaviour.clear(); + } + } + + bool isTerminalState(StateType const& state) const { + {% for expression in terminalExpressions %}if ({$expression}) { + return true; + } + {% endfor %} + return false; + } + + void exploreNonSynchronizingEdges(StateType const& in, StateBehaviour& behaviour, StateSet& statesToExplore) { + {% for edge in nonsynch_edges %}{ + if ({$edge.guard}) { + Choice& choice = behaviour.addChoice(); + choice.resizeRewards({$edge_destination_rewards_count}, 0); + { + TransientVariables transient; + {% if edge.transient_assignments %} + edge_perform_{$edge.name}(in, transient, transient); + {% endif %} + {% for reward in edge_rewards %} + choice.addReward({$reward.index}, transient.{$reward.variable}); + {% endfor %} + } + {% for destination in edge.destinations %}{ + StateType out(in); + TransientVariables transientIn; + TransientVariables transientOut; + destination_perform_{$edge.name}_{$destination.name}(in, out{% if edge.transient_variables_in_destinations %}, transientIn, transientOut{% endif %}); + IndexType outStateIndex = getOrAddIndex(out, statesToExplore); + choice.add(outStateIndex, {$destination.value}); + {% for reward in destination_rewards %} + choice.addReward({$reward.index}, transientOut.{$reward.variable}); + {% endfor %} + } + {% endfor %} + } + } + {% endfor %} + } + + {% for vector in synch_vectors %}{$vector.functions} + {% endfor %} + + void exploreSynchronizingEdges(StateType const& state, StateBehaviour& behaviour, StateSet& statesToExplore) { + {% for vector in synch_vectors %}{ + exploreSynchronizationVector_{$vector.index}(state, behaviour, statesToExplore); + } + {% endfor %} + } + + IndexType getOrAddIndex(StateType const& state, StateSet& statesToExplore) { + auto it = stateIds.find(state); + if (it != stateIds.end()) { + return it->second; + } else { + IndexType newIndex = static_cast(stateIds.size()); + stateIds.insert(std::make_pair(state, newIndex)); +#ifndef NDEBUG + std::cout << "inserting state " << state << std::endl; +#endif + statesToExplore.add(state); + return newIndex; + } + } + + IndexType getIndex(StateType const& state) const { + auto it = stateIds.find(state); + if (it != stateIds.end()) { + return it->second; + } else { + return stateIds.at(state); + } + } + + void addStateBehaviour(IndexType const& stateId, StateBehaviour& behaviour) { + if (behaviour.empty()) { + deadlockStates.push_back(stateId); + } + + JitModelBuilderInterface::addStateBehaviour(stateId, behaviour); + } + + static JitModelBuilderInterface* create(ModelComponentsBuilder& modelComponentsBuilder) { + return new JitBuilder(modelComponentsBuilder); + } + + private: + spp::sparse_hash_map stateIds; + std::vector initialStates; + std::vector deadlockStates; + + {% for edge in nonsynch_edges %}Edge edge_{$edge.name}; + {% endfor %} + {% for edge in synch_edges %}Edge edge_{$edge.name}; + {% endfor %} + }; - nonTransientAssignmentData = cpptempl::data_list(); - transientAssignmentData = cpptempl::data_list(); - currentLevel = assignment.getLevel(); - } - - if (assignment.isTransient()) { - transientAssignmentData.push_back(generateAssignment(assignment)); - } else { - nonTransientAssignmentData.push_back(generateAssignment(assignment)); + BOOST_DLL_ALIAS(storm::builder::jit::JitBuilder::create, create_builder) } } - - // Close the last (open) level. - cpptempl::data_map level; - level["non_transient_assignments"] = cpptempl::make_data(nonTransientAssignmentData); - level["transient_assignments"] = cpptempl::make_data(transientAssignmentData); - level["index"] = asString(currentLevel); - levels.push_back(level); - } - - return levels; - } - - template - template - cpptempl::data_map ExplicitJitJaniModelBuilder::generateAssignment(storm::jani::Variable const& variable, ValueTypePrime value) const { - cpptempl::data_map result; - result["variable"] = getVariableName(variable.getExpressionVariable()); - result["value"] = asString(value); - return result; - } - - template - cpptempl::data_map ExplicitJitJaniModelBuilder::generateLocationAssignment(storm::jani::Automaton const& automaton, uint64_t value) const { - cpptempl::data_map result; - result["variable"] = getVariableName(getLocationVariable(automaton)); - result["value"] = asString(value); - return result; - } - - template - cpptempl::data_map ExplicitJitJaniModelBuilder::generateAssignment(storm::jani::Assignment const& assignment) { - cpptempl::data_map result; - result["variable"] = getVariableName(assignment.getExpressionVariable()); - auto lowerBoundIt = lowerBounds.find(assignment.getExpressionVariable()); - if (lowerBoundIt != lowerBounds.end()) { - if (lowerBoundIt->second < 0) { - result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) + model.getManager().integer(lowerBoundIt->second), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); - } else if (lowerBoundIt->second == 0) { - result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); - } else { - result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) - model.getManager().integer(lowerBoundIt->second), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); - } - } else { - result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); - } - return result; - } - - template - std::string const& ExplicitJitJaniModelBuilder::getVariableName(storm::expressions::Variable const& variable) const { - return variableToName.at(variable); - } - - template - std::string const& ExplicitJitJaniModelBuilder::registerVariable(storm::expressions::Variable const& variable, bool transient) { - std::string variableName; - - // FIXME: Technically, we would need to catch all keywords here... - if (variable.getName() == "default") { - variableName = "__default"; - } else { - variableName = variable.getName(); - } - - variableToName[variable] = variableName; - if (transient) { - transientVariables.insert(variable); - variablePrefixes[variable] = "transientIn."; - } else { - nontransientVariables.insert(variable); - variablePrefixes[variable] = "in."; - } - return variableToName[variable] ; - } - - template - storm::expressions::Variable const& ExplicitJitJaniModelBuilder::getLocationVariable(storm::jani::Automaton const& automaton) const { - return automatonToLocationVariable.at(automaton.getName()); - } - - template - std::string ExplicitJitJaniModelBuilder::asString(bool value) const { - std::stringstream out; - out << std::boolalpha << value; - return out.str(); - } - - template - storm::expressions::Expression ExplicitJitJaniModelBuilder::shiftVariablesWrtLowerBound(storm::expressions::Expression const& expression) { - return expression.substitute(lowerBoundShiftSubstitution); - } - - template - template - std::string ExplicitJitJaniModelBuilder::asString(ValueTypePrime value) const { - return std::to_string(value); - } - - template - boost::optional ExplicitJitJaniModelBuilder::execute(std::string command) { - auto start = std::chrono::high_resolution_clock::now(); - char buffer[128]; - std::stringstream output; - command += " 2>&1"; - - std::cout << "executing " << command << std::endl; - - std::unique_ptr pipe(popen(command.c_str(), "r")); - STORM_LOG_THROW(pipe, storm::exceptions::InvalidStateException, "Call to popen failed."); - - while (!feof(pipe.get())) { - if (fgets(buffer, 128, pipe.get()) != nullptr) - output << buffer; } - int result = pclose(pipe.get()); - pipe.release(); - - auto end = std::chrono::high_resolution_clock::now(); - std::cout << "Executing command took " << std::chrono::duration_cast(end - start).count() << "ms" << std::endl; + )"; - if (WEXITSTATUS(result) == 0) { - return boost::none; - } else { - return "Executing command failed. Got response: " + output.str(); - } - } - - template - void ExplicitJitJaniModelBuilder::createBuilder(boost::filesystem::path const& dynamicLibraryPath) { - jitBuilderGetFunction = boost::dll::import_alias::CreateFunctionType>(dynamicLibraryPath, "create_builder"); - builder = std::unique_ptr>(jitBuilderGetFunction(modelComponentsBuilder)); - } - - template - boost::filesystem::path ExplicitJitJaniModelBuilder::writeSourceToTemporaryFile(std::string const& source) { - boost::filesystem::path temporaryFile = boost::filesystem::unique_path("%%%%-%%%%-%%%%-%%%%.cpp"); - std::ofstream out(temporaryFile.native()); - out << source << std::endl; - out.close(); - return temporaryFile; + return cpptempl::parse(sourceTemplate, modelData); } template - boost::filesystem::path ExplicitJitJaniModelBuilder::compileSourceToSharedLibrary(boost::filesystem::path const& sourceFile) { + boost::filesystem::path ExplicitJitJaniModelBuilder::compileToSharedLibrary(boost::filesystem::path const& sourceFile) { std::string sourceFilename = boost::filesystem::absolute(sourceFile).string(); auto dynamicLibraryPath = sourceFile; dynamicLibraryPath += DYLIB_EXTENSION; std::string dynamicLibraryFilename = boost::filesystem::absolute(dynamicLibraryPath).string(); - std::string command = CXX_COMPILER + " " + sourceFilename + " " + COMPILER_FLAGS + " -I" + STORM_ROOT + " -I" + STORM_ROOT + "/build_xcode/include -I" + L3PP_ROOT + " -I" + BOOST_ROOT + " -I" + GMP_ROOT + "/include -I" + CARL_ROOT + "/src -I" + CLN_ROOT + "/include -I" + GINAC_ROOT + "/include -o " + dynamicLibraryFilename; + std::string command = compiler + " " + sourceFilename + " " + compilerFlags + " -I" + stormRoot + " -I" + stormRoot + "/build_xcode/include -I" + boostIncludeDirectory + " -o " + dynamicLibraryFilename; boost::optional error = execute(command); if (error) { boost::filesystem::remove(sourceFile); STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Compiling shared library failed. Error: " << error.get()); } - + return dynamicLibraryPath; } template - std::shared_ptr> ExplicitJitJaniModelBuilder::build() { - - // (1) generate the source code of the shared library - std::string source; - try { - source = createSourceCode(); - } catch (std::exception const& e) { - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The model could not be successfully built (error: " << e.what() << ")."); - } - std::cout << "created source code: " << source << std::endl; - - // (2) write the source code to a temporary file - boost::filesystem::path temporarySourceFile = writeSourceToTemporaryFile(source); - std::cout << "wrote source to file " << temporarySourceFile.native() << std::endl; - - // (3) compile the shared library - boost::filesystem::path dynamicLibraryPath = compileSourceToSharedLibrary(temporarySourceFile); - std::cout << "successfully compiled shared library" << std::endl; - - // (4) remove the source code we just compiled - boost::filesystem::remove(temporarySourceFile); - - // (5) create the loader from the shared library - createBuilder(dynamicLibraryPath); - - // (6) execute the function in the shared lib - auto start = std::chrono::high_resolution_clock::now(); - auto sparseModel = builder->build(); - auto end = std::chrono::high_resolution_clock::now(); - std::cout << "Building model took " << std::chrono::duration_cast(end - start).count() << "ms." << std::endl; - - // (7) delete the shared library - boost::filesystem::remove(dynamicLibraryPath); - - // Return the constructed model. - return std::shared_ptr>(sparseModel); + void ExplicitJitJaniModelBuilder::createBuilder(boost::filesystem::path const& dynamicLibraryPath) { + jitBuilderCreateFunction = boost::dll::import_alias::CreateFunctionType>(dynamicLibraryPath, "create_builder"); + builder = std::unique_ptr>(jitBuilderCreateFunction(modelComponentsBuilder)); } template class ExplicitJitJaniModelBuilder>; diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.h b/src/builder/jit/ExplicitJitJaniModelBuilder.h index bb0f47aa0..beb148b62 100644 --- a/src/builder/jit/ExplicitJitJaniModelBuilder.h +++ b/src/builder/jit/ExplicitJitJaniModelBuilder.h @@ -38,74 +38,144 @@ namespace storm { typedef JitModelBuilderInterface* (CreateFunctionType)(ModelComponentsBuilder& modelComponentsBuilder); typedef boost::function ImportFunctionType; + /*! + * Creates a model builder for the given model. The provided options are used to determine which part of + * the model is built. + */ ExplicitJitJaniModelBuilder(storm::jani::Model const& model, storm::builder::BuilderOptions const& options = storm::builder::BuilderOptions()); + /*! + * Builds and returns the sparse model. + */ std::shared_ptr> build(); + /*! + * Performs some checks that can help debug why the model builder does not work. Returns true if the + * general infrastructure for the model builder appears to be working. + */ + bool doctor() const; + private: - void createBuilder(boost::filesystem::path const& dynamicLibraryPath); - std::string createSourceCode(); - boost::filesystem::path writeSourceToTemporaryFile(std::string const& source); - boost::filesystem::path compileSourceToSharedLibrary(boost::filesystem::path const& sourceFile); - + // Helper methods for the doctor() procedure. + bool checkTemporaryFileWritable() const; + bool checkCompilerWorks() const; + bool checkCompilerFlagsWork() const; + bool checkBoostAvailable() const; + bool checkBoostDllAvailable() const; + bool checkStormAvailable() const; + + /*! + * Executes the given command. If the command fails with a non-zero error code, the error stream content + * is returned and boost::none otherwise. + */ static boost::optional execute(std::string command); - // Functions that generate data maps or data templates. - cpptempl::data_list generateInitialStates(); - + /*! + * Writes the given content to a temporary file. The temporary file is created to have the provided suffix. + */ + static boost::filesystem::path writeToTemporaryFile(std::string const& content, std::string const& suffix = ".cpp"); + + /*! + * Assembles the information of the model such that it can be put into the source skeleton. + */ + cpptempl::data_map generateModelData(); + + void generateVariables(cpptempl::data_map& modelData); cpptempl::data_map generateBooleanVariable(storm::jani::BooleanVariable const& variable); cpptempl::data_map generateBoundedIntegerVariable(storm::jani::BoundedIntegerVariable const& variable); cpptempl::data_map generateUnboundedIntegerVariable(storm::jani::UnboundedIntegerVariable const& variable); cpptempl::data_map generateRealVariable(storm::jani::RealVariable const& variable); cpptempl::data_map generateLocationVariable(storm::jani::Automaton const& automaton); - void generateVariables(cpptempl::data_map& modelData); - void generateLocations(cpptempl::data_map& modelData); + void generateInitialStates(cpptempl::data_map& modelData); void generateRewards(cpptempl::data_map& modelData); - - cpptempl::data_list generateLabels(); - cpptempl::data_list generateTerminalExpressions(); + void generateLocations(cpptempl::data_map& modelData); + void generateLabels(cpptempl::data_map& modelData); + void generateTerminalExpressions(cpptempl::data_map& modelData); + + // Functions related to the generation of edge data. void generateEdges(cpptempl::data_map& modelData); cpptempl::data_map generateSynchronizationVector(cpptempl::data_map& modelData, storm::jani::ParallelComposition const& parallelComposition, storm::jani::SynchronizationVector const& synchronizationVector, uint64_t synchronizationVectorIndex); cpptempl::data_list generateLevels(storm::jani::OrderedAssignments const& assignments); - cpptempl::data_map generateEdge(storm::jani::Automaton const& automaton, uint64_t edgeIndex, storm::jani::Edge const& edge); cpptempl::data_map generateDestination(uint64_t destinationIndex, storm::jani::EdgeDestination const& destination); - template cpptempl::data_map generateAssignment(storm::jani::Variable const& variable, ValueTypePrime value) const; - cpptempl::data_map generateLocationAssignment(storm::jani::Automaton const& automaton, uint64_t value) const; - cpptempl::data_map generateAssignment(storm::jani::Assignment const& assignment); - + // Auxiliary functions that perform regularly needed steps. std::string const& getVariableName(storm::expressions::Variable const& variable) const; std::string const& registerVariable(storm::expressions::Variable const& variable, bool transient = false); storm::expressions::Variable const& getLocationVariable(storm::jani::Automaton const& automaton) const; - std::string asString(bool value) const; storm::expressions::Expression shiftVariablesWrtLowerBound(storm::expressions::Expression const& expression); - + + // Conversion functions. template std::string asString(ValueTypePrime value) const; - + std::string asString(bool value) const; + + /*! + * Creates the source code for the shared library that performs the model generation. + * + * @param modelData The assembled data of the model to be put into the blueprint. Note that this is not + * modified in this function, but the data needs to be passed as non-const to cpptempl. + */ + std::string createSourceCodeFromSkeleton(cpptempl::data_map& modelData); + + /*! + * Compiles the provided source file to a shared library and returns a path object to the resulting + * binary file. + */ + boost::filesystem::path compileToSharedLibrary(boost::filesystem::path const& sourceFile); + + /*! + * Loads the given shared library and creates the builder from it. + */ + void createBuilder(boost::filesystem::path const& dynamicLibraryPath); + + /// The options to use for model building. storm::builder::BuilderOptions options; + + /// The model specification that is to be built. storm::jani::Model model; + + /// A vector of automata that is to be put in parallel. The automata are references from the model specification. std::vector> parallelAutomata; + /// An object that is responsible for building the components of the model. The shared library gets this + /// as a mechanism to perform a callback in order to register transitions that were found. ModelComponentsBuilder modelComponentsBuilder; - typename ExplicitJitJaniModelBuilder::ImportFunctionType jitBuilderGetFunction; + + /// The function that was loaded from the shared library. We have to keep this function around, because + /// otherwise the shared library gets unloaded. + typename ExplicitJitJaniModelBuilder::ImportFunctionType jitBuilderCreateFunction; + + /// The pointer to the builder object created via the shared library. std::unique_ptr> builder; + // Members that store information about the model. They are used in the process of assembling the model + // data that is used in the skeleton. std::unordered_map variableToName; std::map automatonToLocationVariable; - storm::expressions::ToCppVisitor expressionTranslator; std::map lowerBoundShiftSubstitution; std::map lowerBounds; std::set transientVariables; std::set nontransientVariables; std::unordered_map variablePrefixes; + + /// The compiler binary. + std::string compiler; + + /// The flags passed to the compiler. + std::string compilerFlags; + + /// The include directory of boost. + std::string boostIncludeDirectory; + + /// The root directory of storm. + std::string stormRoot; }; } diff --git a/src/builder/jit/StateBehaviour.cpp b/src/builder/jit/StateBehaviour.cpp index 21056d4b8..12d8e9373 100644 --- a/src/builder/jit/StateBehaviour.cpp +++ b/src/builder/jit/StateBehaviour.cpp @@ -38,7 +38,7 @@ namespace storm { void StateBehaviour::addStateRewards(std::vector&& stateRewards) { this->stateRewards = std::move(stateRewards); } - + template std::vector const& StateBehaviour::getStateRewards() const { return stateRewards; @@ -48,49 +48,9 @@ namespace storm { void StateBehaviour::reduce(storm::jani::ModelType const& modelType) { if (choices.size() > 1) { if (modelType == storm::jani::ModelType::DTMC || modelType == storm::jani::ModelType::CTMC) { - std::size_t totalCount = choices.size(); - - ValueType totalExitRate = modelType == storm::jani::ModelType::DTMC ? static_cast(totalCount) : storm::utility::zero(); - - if (choices.front().getNumberOfRewards() > 0) { - std::vector newRewards(choices.front().getNumberOfRewards()); - - if (modelType == storm::jani::ModelType::CTMC) { - for (auto const& choice : choices) { - ValueType massOfChoice = storm::utility::zero(); - for (auto const& entry : choices.front().getDistribution()) { - massOfChoice += entry.getValue(); - } - - auto outIt = newRewards.begin(); - for (auto const& reward : choice.getRewards()) { - *outIt += reward * massOfChoice / totalExitRate; - ++outIt; - } - } - } else { - for (auto const& choice : choices) { - auto outIt = newRewards.begin(); - for (auto const& reward : choice.getRewards()) { - *outIt += reward / totalExitRate; - ++outIt; - } - } - } - - choices.front().setRewards(std::move(newRewards)); - } - - for (auto it = ++choices.begin(), ite = choices.end(); it != ite; ++it) { - choices.front().add(std::move(*it)); - } - - choices.resize(1); - choices.front().compress(); - - if (modelType == storm::jani::ModelType::DTMC) { - choices.front().divideDistribution(static_cast(totalCount)); - } + reduceDeterministic(modelType); + } else if (modelType == storm::jani::ModelType::MA) { + reduceMarkovAutomaton(); } else { for (auto& choice : choices) { choice.compress(); @@ -101,6 +61,93 @@ namespace storm { } } + template + void StateBehaviour::reduceDeterministic(storm::jani::ModelType const& modelType) { + std::size_t totalCount = choices.size(); + + ValueType totalExitRate = modelType == storm::jani::ModelType::DTMC ? static_cast(totalCount) : storm::utility::zero(); + + if (choices.front().getNumberOfRewards() > 0) { + std::vector newRewards(choices.front().getNumberOfRewards()); + + if (modelType == storm::jani::ModelType::CTMC) { + for (auto const& choice : choices) { + ValueType massOfChoice = storm::utility::zero(); + for (auto const& entry : choices.front().getDistribution()) { + massOfChoice += entry.getValue(); + } + + auto outIt = newRewards.begin(); + for (auto const& reward : choice.getRewards()) { + *outIt += reward * massOfChoice / totalExitRate; + ++outIt; + } + } + } else { + for (auto const& choice : choices) { + auto outIt = newRewards.begin(); + for (auto const& reward : choice.getRewards()) { + *outIt += reward / totalExitRate; + ++outIt; + } + } + } + + choices.front().setRewards(std::move(newRewards)); + } + + for (auto it = ++choices.begin(), ite = choices.end(); it != ite; ++it) { + choices.front().add(std::move(*it)); + } + + choices.resize(1); + choices.front().compress(); + + if (modelType == storm::jani::ModelType::DTMC) { + choices.front().divideDistribution(static_cast(totalCount)); + } + } + + template + void StateBehaviour::reduceMarkovAutomaton() { + // If the model we build is a Markov Automaton, we reduce the choices by summing all Markovian choices + // and making the Markovian choice the very first one (if there is any). + bool foundPreviousMarkovianChoice = false; + uint64_t numberOfChoicesToDelete = 0; + + for (uint_fast64_t index = 0; index + numberOfChoicesToDelete < this->size();) { + Choice& choice = choices[index]; + + if (choice.isMarkovian()) { + if (foundPreviousMarkovianChoice) { + // If there was a previous Markovian choice, we need to sum them. Note that we can assume + // that the previous Markovian choice is the very first one in the choices vector. + choices.front().add(std::move(choice)); + + // Swap the choice to the end to indicate it can be removed (if it's not already there). + if (index != this->size() - 1) { + choice = std::move(choices[choices.size() - 1 - numberOfChoicesToDelete]); + } + ++numberOfChoicesToDelete; + } else { + // If there is no previous Markovian choice, just move the Markovian choice to the front. + if (index != 0) { + std::swap(choices.front(), choice); + foundPreviousMarkovianChoice = true; + } + ++index; + } + } else { + ++index; + } + } + + // Finally remove the choices that were added to other Markovian choices. + if (numberOfChoicesToDelete > 0) { + choices.resize(choices.size() - numberOfChoicesToDelete); + } + } + template bool StateBehaviour::isExpanded() const { return expanded; @@ -120,7 +167,7 @@ namespace storm { std::size_t StateBehaviour::size() const { return choices.size(); } - + template void StateBehaviour::clear() { choices.clear(); diff --git a/src/builder/jit/StateBehaviour.h b/src/builder/jit/StateBehaviour.h index 52c4d0318..ee44446da 100644 --- a/src/builder/jit/StateBehaviour.h +++ b/src/builder/jit/StateBehaviour.h @@ -43,9 +43,20 @@ namespace storm { void clear(); private: + /*! + * Reduces the choices of this state to make it a valid DTMC/CTMC behaviour. + */ + void reduceDeterministic(storm::jani::ModelType const& modelType); + + /*! + * Reduces the choices of this state to make it a valid MA behaviour. + */ + void reduceMarkovAutomaton(); + + /// The actual choices of this behaviour. ContainerType choices; - // The state rewards (under the different, selected reward models) of the state. + /// The state rewards (under the different, selected reward models) of the state. std::vector stateRewards; bool compressed; diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index f9b39e0cc..2cf113f7d 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -273,7 +273,10 @@ namespace storm { ++integerIt; } int_fast64_t assignedValue = this->evaluator->asInt(assignmentIt->getAssignedExpression()); - STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'."); + if (this->options.isExplorationChecksSet()) { + STORM_LOG_THROW(assignedValue >= integerIt->lowerBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'."); + STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'."); + } newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound); STORM_LOG_ASSERT(static_cast(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ")."); } @@ -424,15 +427,20 @@ namespace storm { // Update the choice by adding the probability/target state to it. probability = exitRate ? exitRate.get() * probability : probability; choice.addProbability(stateIndex, probability); - probabilitySum += probability; + + if (this->options.isExplorationChecksSet()) { + probabilitySum += probability; + } } } // Create the state-action reward for the newly created choice. performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&choice] (ValueType const& value) { choice.addReward(value); } ); - // Check that the resulting distribution is in fact a distribution. - STORM_LOG_THROW(!this->isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for edge (actually sum to " << probabilitySum << ")."); + if (this->options.isExplorationChecksSet()) { + // Check that the resulting distribution is in fact a distribution. + STORM_LOG_THROW(!this->isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for edge (actually sum to " << probabilitySum << ")."); + } } ++automatonIndex; @@ -450,8 +458,10 @@ namespace storm { // Only process this action, if there is at least one feasible solution. if (!enabledEdges.empty()) { - // Check whether a global variable is written multiple times in any combination. - checkGlobalVariableWritesValid(enabledEdges); + if (this->options.isExplorationChecksSet()) { + // Check whether a global variable is written multiple times in any combination. + checkGlobalVariableWritesValid(enabledEdges); + } std::vector::const_iterator> iteratorList(enabledEdges.size()); @@ -525,8 +535,10 @@ namespace storm { probabilitySum += stateProbabilityPair.second; } - // Check that the resulting distribution is in fact a distribution. - STORM_LOG_THROW(!this->isDiscreteTimeModel() || !this->comparator.isConstant(probabilitySum) || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not sum to one for some command (actually sum to " << probabilitySum << ")."); + if (this->options.isExplorationChecksSet()) { + // Check that the resulting distribution is in fact a distribution. + STORM_LOG_THROW(!this->isDiscreteTimeModel() || !this->comparator.isConstant(probabilitySum) || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not sum to one for some command (actually sum to " << probabilitySum << ")."); + } // Dispose of the temporary maps. delete currentTargetStates; diff --git a/src/generator/JaniNextStateGenerator.h b/src/generator/JaniNextStateGenerator.h index 06de1a9ea..a581a42e3 100644 --- a/src/generator/JaniNextStateGenerator.h +++ b/src/generator/JaniNextStateGenerator.h @@ -115,7 +115,7 @@ namespace storm { /// A vector storing information about the corresponding reward models (variables). std::vector rewardModelInformation; - // A flag that stores whether at least one of the selected reward models has state-action rewards. + /// A flag that stores whether at least one of the selected reward models has state-action rewards. bool hasStateActionRewards; }; diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp index 6e5a62be0..0c2d62601 100644 --- a/src/generator/NextStateGenerator.cpp +++ b/src/generator/NextStateGenerator.cpp @@ -120,7 +120,7 @@ namespace storm { // Swap the choice to the end to indicate it can be removed (if it's not already there). if (index != result.getNumberOfChoices() - 1) { - std::swap(choice, result.getChoices().back()); + choice = std::move(result.getChoices()[result.getNumberOfChoices() - 1 - numberOfChoicesToDelete]); } ++numberOfChoicesToDelete; } else { diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index ceea1aafe..b9fa22957 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -308,8 +308,10 @@ namespace storm { ++integerIt; } int_fast64_t assignedValue = this->evaluator->asInt(assignmentIt->getExpression()); - STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'."); - STORM_LOG_THROW(assignedValue >= integerIt->lowerBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'."); + if (this->options.isExplorationChecksSet()) { + STORM_LOG_THROW(assignedValue >= integerIt->lowerBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'."); + STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'."); + } newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound); STORM_LOG_ASSERT(static_cast(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ")."); } @@ -422,8 +424,10 @@ namespace storm { choice.addReward(stateActionRewardValue); } - // Check that the resulting distribution is in fact a distribution. - STORM_LOG_THROW(!program.isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ")."); + if (this->options.isExplorationChecksSet()) { + // Check that the resulting distribution is in fact a distribution. + STORM_LOG_THROW(!program.isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ")."); + } } } @@ -508,11 +512,15 @@ namespace storm { for (auto const& stateProbabilityPair : *newTargetStates) { StateType actualIndex = stateToIdCallback(stateProbabilityPair.first); choice.addProbability(actualIndex, stateProbabilityPair.second); - probabilitySum += stateProbabilityPair.second; + if (this->options.isExplorationChecksSet()) { + probabilitySum += stateProbabilityPair.second; + } } - // Check that the resulting distribution is in fact a distribution. - STORM_LOG_THROW(!program.isDiscreteTimeModel() || !this->comparator.isConstant(probabilitySum) || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ")."); + if (this->options.isExplorationChecksSet()) { + // Check that the resulting distribution is in fact a distribution. + STORM_LOG_THROW(!program.isDiscreteTimeModel() || !this->comparator.isConstant(probabilitySum) || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ")."); + } // Create the state-action reward for the newly created choice. for (auto const& rewardModel : rewardModels) { diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index a149a9e92..efa8c405b 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -426,7 +426,6 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown operator " << opString); } } - } storm::jani::Property JaniParser::parseProperty(json const& propertyStructure) { diff --git a/src/settings/modules/IOSettings.cpp b/src/settings/modules/IOSettings.cpp index c63a08afa..09991f716 100644 --- a/src/settings/modules/IOSettings.cpp +++ b/src/settings/modules/IOSettings.cpp @@ -24,6 +24,8 @@ namespace storm { const std::string IOSettings::jitOptionName = "jit"; const std::string IOSettings::explorationOrderOptionName = "explorder"; const std::string IOSettings::explorationOrderOptionShortName = "eo"; + const std::string IOSettings::explorationChecksOptionName = "explchecks"; + const std::string IOSettings::explorationChecksOptionShortName = "ec"; const std::string IOSettings::transitionRewardsOptionName = "transrew"; const std::string IOSettings::stateRewardsOptionName = "staterew"; const std::string IOSettings::choiceLabelingOptionName = "choicelab"; @@ -51,13 +53,14 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, janiInputOptionName, false, "Parses the model given in the JANI format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the JANI input.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, prismToJaniOptionName, false, "If set, the input PRISM model is transformed to JANI.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder if available.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").build()); std::vector explorationOrders = {"dfs", "bfs"}; this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose. Available are: dfs and bfs.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(explorationOrders)).setDefaultValueString("bfs").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, explorationChecksOptionName, false, "If set, additional checks (if available) are performed during model exploration to debug the model.").setShortName(explorationChecksOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, false, "If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); @@ -141,6 +144,10 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown exploration order '" << explorationOrderAsString << "'."); } + bool IOSettings::isExplorationChecksSet() const { + return this->getOption(explorationChecksOptionName).getHasOptionBeenSet(); + } + bool IOSettings::isTransitionRewardsSet() const { return this->getOption(transitionRewardsOptionName).getHasOptionBeenSet(); } diff --git a/src/settings/modules/IOSettings.h b/src/settings/modules/IOSettings.h index cf804f1b9..ea6778adb 100644 --- a/src/settings/modules/IOSettings.h +++ b/src/settings/modules/IOSettings.h @@ -130,6 +130,13 @@ namespace storm { */ bool isExplorationOrderSet() const; + /*! + * Retrieves whether to perform additional checks during model exploration (e.g. out-of-bounds, etc.). + * + * @return True if additional checks are to be performed. + */ + bool isExplorationChecksSet() const; + /*! * Retrieves the exploration order if it was set. * @@ -244,6 +251,8 @@ namespace storm { static const std::string janiInputOptionName; static const std::string prismToJaniOptionName; static const std::string jitOptionName; + static const std::string explorationChecksOptionName; + static const std::string explorationChecksOptionShortName; static const std::string explorationOrderOptionName; static const std::string explorationOrderOptionShortName; static const std::string transitionRewardsOptionName; diff --git a/src/settings/modules/JitBuilderSettings.cpp b/src/settings/modules/JitBuilderSettings.cpp index 217ee61e0..fa44ac4b3 100644 --- a/src/settings/modules/JitBuilderSettings.cpp +++ b/src/settings/modules/JitBuilderSettings.cpp @@ -14,22 +14,60 @@ namespace storm { namespace modules { const std::string JitBuilderSettings::moduleName = "jitbuilder"; - const std::string JitBuilderSettings::noJitOptionName = "nojit"; const std::string JitBuilderSettings::doctorOptionName = "doctor"; - + const std::string JitBuilderSettings::compilerOptionName = "compiler"; + const std::string JitBuilderSettings::stormRootOptionName = "storm"; + const std::string JitBuilderSettings::boostIncludeDirectoryOptionName = "boost"; + const std::string JitBuilderSettings::compilerFlagsOptionName = "cxxflags"; + JitBuilderSettings::JitBuilderSettings() : ModuleSettings(moduleName) { -// this->addOption(storm::settings::OptionBuilder(moduleName, noJitOptionName, false, "Don't use the jit-based explicit model builder.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, doctorOptionName, false, "Show information on why the jit-based explicit model builder is not usable on the current system.").build()); + 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, 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, compilerFlagsOptionName, false, "The flags passed to the compiler.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("flags", "The compiler flags.").build()).build()); + } + + bool JitBuilderSettings::isCompilerSet() const { + return this->getOption(compilerOptionName).getHasOptionBeenSet(); + } + + std::string JitBuilderSettings::getCompiler() const { + return this->getOption(compilerOptionName).getArgumentByName("name").getValueAsString(); + } + + bool JitBuilderSettings::isStormRootSet() const { + return this->getOption(stormRootOptionName).getHasOptionBeenSet(); + } + + std::string JitBuilderSettings::getStormRoot() const { + return this->getOption(stormRootOptionName).getArgumentByName("dir").getValueAsString(); + } + + bool JitBuilderSettings::isBoostIncludeDirectorySet() const { + return this->getOption(boostIncludeDirectoryOptionName).getHasOptionBeenSet(); } -// bool JitBuilderSettings::isNoJitSet() const { -// return this->getOption(noJitOptionName).getHasOptionBeenSet(); -// } + std::string JitBuilderSettings::getBoostIncludeDirectory() const { + return this->getOption(boostIncludeDirectoryOptionName).getArgumentByName("dir").getValueAsString(); + } bool JitBuilderSettings::isDoctorSet() const { return this->getOption(doctorOptionName).getHasOptionBeenSet(); } - + + bool JitBuilderSettings::isCompilerFlagsSet() const { + return this->getOption(compilerFlagsOptionName).getHasOptionBeenSet(); + } + + std::string JitBuilderSettings::getCompilerFlags() const { + return this->getOption(compilerFlagsOptionName).getArgumentByName("flags").getValueAsString(); + } + void JitBuilderSettings::finalize() { // Intentionally left empty. } diff --git a/src/settings/modules/JitBuilderSettings.h b/src/settings/modules/JitBuilderSettings.h index 1080e89b6..abb916170 100644 --- a/src/settings/modules/JitBuilderSettings.h +++ b/src/settings/modules/JitBuilderSettings.h @@ -12,18 +12,31 @@ namespace storm { * Creates a new JitBuilder settings object. */ JitBuilderSettings(); - -// bool isNoJitSet() const; bool isDoctorSet() const; + bool isCompilerSet() const; + std::string getCompiler() const; + + bool isStormRootSet() const; + std::string getStormRoot() const; + + bool isBoostIncludeDirectorySet() const; + std::string getBoostIncludeDirectory() const; + + bool isCompilerFlagsSet() const; + std::string getCompilerFlags() const; + bool check() const override; void finalize() override; static const std::string moduleName; private: - static const std::string noJitOptionName; + static const std::string compilerOptionName; + static const std::string stormRootOptionName; + static const std::string boostIncludeDirectoryOptionName; + static const std::string compilerFlagsOptionName; static const std::string doctorOptionName; }; diff --git a/src/utility/storm.h b/src/utility/storm.h index 9a2c7e080..06089b763 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -22,7 +22,7 @@ #include "src/settings/modules/ParametricSettings.h" #include "src/settings/modules/RegionSettings.h" #include "src/settings/modules/EliminationSettings.h" -#include "src/settings/modules/CoreSettings.h" +#include "src/settings/modules/JitBuilderSettings.h" // Formula headers. #include "src/logic/Formulas.h" @@ -124,7 +124,15 @@ namespace storm { if (storm::settings::getModule().isJitSet()) { STORM_LOG_THROW(model.isJaniModel(), storm::exceptions::NotSupportedException, "Cannot use JIT-based model builder for non-JANI model."); + storm::builder::jit::ExplicitJitJaniModelBuilder builder(model.asJaniModel(), options); + + if (storm::settings::getModule().isDoctorSet()) { + bool result = builder.doctor(); + STORM_LOG_THROW(result, storm::exceptions::InvalidSettingsException, "The JIT-based model builder cannot be used on your system."); + STORM_LOG_INFO("The JIT-based model builder seems to be working."); + } + return builder.build(); } else { std::shared_ptr> generator; diff --git a/storm-config.h.in b/storm-config.h.in index 1bc2eac7d..fa69055be 100644 --- a/storm-config.h.in +++ b/storm-config.h.in @@ -14,6 +14,9 @@ // The path used in the functional and performance tests to load the supplied example files #define STORM_CPP_TESTS_BASE_PATH "@STORM_CPP_TESTS_BASE_PATH@" +// The path to boost used during compilation. +#define STORM_BOOST_INCLUDE_DIR "@STORM_BOOST_INCLUDE_DIR@" + // Whether Gurobi is available and to be used (define/undef) #cmakedefine STORM_HAVE_GUROBI