From 1c1120ef6620fcc06928f93dc863649cc068a30c Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 25 Oct 2016 22:29:41 +0200 Subject: [PATCH] more work on jit-based builder Former-commit-id: 579adb85eb3367047f65d7273e889c9114e07057 [formerly 574a25aa3d5cfce00bfbaa7c5333ef04b62b739b] Former-commit-id: 2a1d2ca2c264935a7b0e21dc9c2658def42d1a5b --- src/builder/ExplicitJitJaniModelBuilder.cpp | 778 ------------------- src/builder/ExplicitJitJaniModelBuilder.h | 83 -- src/builder/JitModelBuilderInterface.h | 23 - src/builder/jit/Choice.cpp | 19 + src/builder/jit/Choice.h | 22 + src/builder/jit/Distribution.cpp | 43 + src/builder/jit/Distribution.h | 44 ++ src/builder/jit/DistributionEntry.cpp | 24 + src/builder/jit/DistributionEntry.h | 22 + src/builder/jit/JitModelBuilderInterface.cpp | 24 + src/builder/jit/ModelComponentBuilder.cpp | 64 ++ src/builder/jit/ModelComponentBuilder.h | 46 ++ src/builder/jit/StateBehaviour.cpp | 25 + src/builder/jit/StateBehaviour.h | 25 + src/storage/jani/ModelType.cpp | 14 + src/storage/jani/ModelType.h | 5 +- src/utility/storm.h | 4 +- 17 files changed, 378 insertions(+), 887 deletions(-) delete mode 100644 src/builder/ExplicitJitJaniModelBuilder.cpp delete mode 100644 src/builder/ExplicitJitJaniModelBuilder.h delete mode 100644 src/builder/JitModelBuilderInterface.h create mode 100644 src/builder/jit/Choice.cpp create mode 100644 src/builder/jit/Choice.h create mode 100644 src/builder/jit/Distribution.cpp create mode 100644 src/builder/jit/Distribution.h create mode 100644 src/builder/jit/DistributionEntry.cpp create mode 100644 src/builder/jit/DistributionEntry.h create mode 100644 src/builder/jit/JitModelBuilderInterface.cpp create mode 100644 src/builder/jit/ModelComponentBuilder.cpp create mode 100644 src/builder/jit/ModelComponentBuilder.h create mode 100644 src/builder/jit/StateBehaviour.cpp create mode 100644 src/builder/jit/StateBehaviour.h diff --git a/src/builder/ExplicitJitJaniModelBuilder.cpp b/src/builder/ExplicitJitJaniModelBuilder.cpp deleted file mode 100644 index ece9175f2..000000000 --- a/src/builder/ExplicitJitJaniModelBuilder.cpp +++ /dev/null @@ -1,778 +0,0 @@ -#include "src/builder/ExplicitJitJaniModelBuilder.h" - -#include -#include -#include - -#include "src/adapters/CarlAdapter.h" - -#include "src/solver/SmtSolver.h" - -#include "src/utility/macros.h" -#include "src/utility/solver.h" -#include "src/exceptions/InvalidStateException.h" -#include "src/exceptions/NotSupportedException.h" -#include "src/exceptions/UnexpectedException.h" - -namespace storm { - namespace builder { - - static const std::string CXX_COMPILER = "clang++"; - 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"; - - template - ExplicitJitJaniModelBuilder::ExplicitJitJaniModelBuilder(storm::jani::Model const& model) : model(model) { - // Intentionally left empty. - } - - template - std::string ExplicitJitJaniModelBuilder::createSourceCode() { - std::string sourceTemplate = R"( - -#define NDEBUG - -#include -#include -#include -#include -#include -#include - -#include "resources/3rdparty/sparsepp/sparsepp.h" - -#include "src/builder/JitModelBuilderInterface.h" -#include "src/storage/SparseMatrix.h" -#include "src/models/sparse/Dtmc.h" -#include "src/models/sparse/StandardRewardModel.h" - -namespace storm { - namespace builder { - - typedef uint32_t IndexType; - - struct StateType { - // Boolean variables. - {% for variable in stateVariables.boolean %}bool {$variable.name} : 1; - {% endfor %} - // Bounded integer variables. - {% for variable in stateVariables.boundedInteger %}uint64_t {$variable.name} : {$variable.numberOfBits}; - {% endfor %} - // Location variables. - {% for variable in stateVariables.locations %}uint64_t {$variable.name} : {$variable.numberOfBits}; - {% endfor %} - }; - - bool operator==(StateType const& first, StateType const& second) { - bool result = true; - {% for variable in stateVariables.boolean %}result &= !(first.{$variable.name} ^ second.{$variable.name}); - {% endfor %} - {% for variable in stateVariables.boundedInteger %}result &= first.{$variable.name} == second.{$variable.name}; - {% endfor %} - {% for variable in stateVariables.locations %}result &= first.{$variable.name} == second.{$variable.name}; - {% endfor %} - return result; - } - - std::ostream& operator<<(std::ostream& out, StateType const& state) { - out << "<"; - {% for variable in stateVariables.boolean %}out << "{$variable.name}=" << state.{$variable.name} << ", "; - {% endfor %} - {% for variable in stateVariables.boundedInteger %}out << "{$variable.name}=" << state.{$variable.name} << ", "; - {% endfor %} - {% for variable in stateVariables.locations %}out << "{$variable.name}=" << state.{$variable.name} << ", "; - {% endfor %} - out << ">"; - return out; - } - - } -} - -namespace std { - template <> - struct hash { - std::size_t operator()(storm::builder::StateType const& state) 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 stateVariables.boolean %}spp::hash_combine(seed, state.{$variable.name}); - {% endfor %} - {% for variable in stateVariables.boundedInteger %}spp::hash_combine(seed, state.{$variable.name}); - {% endfor %} - {% for variable in stateVariables.locations %}spp::hash_combine(seed, state.{$variable.name}); - {% endfor %} - return seed; - } - }; -} - -namespace storm { - namespace builder { - - typedef double ValueType; - - static bool model_is_deterministic() { - return {$deterministic_model}; - } - - static bool model_is_discrete_time() { - return {$discrete_time_model}; - } - - class Entry { - public: - Entry() : column(0), value(0) { - // Intentionally left empty. - } - - Entry(IndexType const& column, ValueType const& value) : column(column), value(value) { - // Intentionally left empty. - } - - IndexType const& getColumn() const { - return column; - } - - ValueType const& getValue() const { - return value; - } - - void addToValue(ValueType const& value) { - this->value += value; - } - - void scaleValue(ValueType const& divisor) { - this->value /= divisor; - } - - private: - IndexType column; - ValueType value; - }; - - class Choice { - public: - typedef std::vector ContainerType; - - void add(IndexType const& stateIndex, ValueType const& value) { - distribution.push_back(Entry(stateIndex, value)); - } - - void add(Choice&& choice) { - distribution.insert(distribution.end(), std::make_move_iterator(choice.getDistribution().begin()), std::make_move_iterator(choice.getDistribution().end())); - } - - void makeUniqueAndShrink() { - std::sort(distribution.begin(), distribution.end(), - [] (Entry const& a, Entry const& b) { - return a.getColumn() < b.getColumn(); - } - ); - - // Code taken from std::unique and modified to fit needs. - auto first = distribution.begin(); - auto last = distribution.end(); - - if (first != last) { - auto result = first; - while (++first != last) { - if (!(result->getColumn() == first->getColumn())) { - if (++result != first) { - *result = std::move(*first); - } - } else { - result->addToValue(first->getValue()); - } - } - ++result; - - distribution.resize(std::distance(distribution.begin(), result)); - } - } - - ContainerType const& getDistribution() const { - return distribution; - } - - ContainerType& getDistribution() { - return distribution; - } - - private: - ContainerType distribution; - }; - - class StateSet { - public: - StateType const& peek() const { - return storage.back(); - } - - StateType get() { - StateType result = std::move(storage.back()); - storage.pop_back(); - return result; - } - - void add(StateType const& state) { - storage.push_back(state); - } - - bool empty() const { - return storage.empty(); - } - - private: - std::vector storage; - }; - - struct ModelComponents { - ModelComponents() : transitionMatrixBuilder(0, 0, 0, true, !model_is_deterministic()), stateLabeling(), rewardModels(), choiceLabeling() { - // Intentionally left empty. - } - - storm::storage::SparseMatrixBuilder transitionMatrixBuilder; - storm::models::sparse::StateLabeling stateLabeling; - std::unordered_map> rewardModels; - boost::optional>> choiceLabeling; - - storm::models::sparse::Model* createModel() { - if (model_is_discrete_time()) { - if (model_is_deterministic()) { - return new storm::models::sparse::Dtmc(std::move(this->transitionMatrixBuilder.build()), std::move(this->stateLabeling), std::move(this->rewardModels), std::move(this->choiceLabeling)); - } else { - return nullptr; - } - } else { - return nullptr; - } - } - }; - - class JitBuilder : public JitModelBuilderInterface { - public: - JitBuilder() : currentRow(0), modelComponents() { - {% for state in initialStates %}{ - StateType state; - {% for assignment in state %}state.{$assignment.variable} = {$assignment.value}; - {% endfor %}initialStates.push_back(state); - } - {% 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; - return modelComponents.createModel(); - } - - void explore(std::vector const& initialStates) { - for (auto const& state : initialStates) { - explore(state); - } - } - - void explore(StateType const& initialState) { - StateSet statesToExplore; - getOrAddIndex(initialState, statesToExplore); - - std::vector choices; - while (!statesToExplore.empty()) { - StateType currentState = statesToExplore.get(); - IndexType currentIndex = getIndex(currentState); -#ifndef NDEBUG - std::cout << "Exploring state " << currentState << ", id " << currentIndex << std::endl; -#endif - - exploreNonSynchronizingEdges(currentState, currentIndex, choices, statesToExplore); - - addChoicesForState(currentIndex, choices); - choices.clear(); - } - } - - void exploreNonSynchronizingEdges(StateType const& sourceState, IndexType const& currentIndex, std::vector& choices, StateSet& statesToExplore) { - {% for edge in nonSynchronizingEdges %}if ({$edge.guard}) { - choices.emplace_back(); - {% for destination in edge.destinations %}{ - StateType targetState(sourceState); - {% for assignment in destination.nonTransientAssignments %}targetState.{$assignment.variable} = {$assignment.value}; - {% endfor %} - IndexType targetStateIndex = getOrAddIndex(targetState, statesToExplore); - choices.back().add(targetStateIndex, {$destination.value}); - } - {% endfor %} - } - {% endfor %} - } - - void addChoicesForState(IndexType const& stateId, std::vector& choices) { - // If there is more than one choice in a deterministic model, we need to combine the choices into one - // global choice. - bool choiceIsGuaranteedDistribution = false; - if (model_is_deterministic() && choices.size() > 1) { - uint64_t choiceCount = choices.size(); - - // We do this by adding the entries of choices after the first one to the first one and then making - // the distribution unique again. - for (auto it = ++choices.begin(), ite = choices.end(); it != ite; ++it) { - choices.front().add(std::move(*it)); - } - choices.resize(1); - choices.front().makeUniqueAndShrink(); - - // If we are dealing with a discrete-time model, we need to scale the probabilities such that they - // form a probability distribution. - if (model_is_discrete_time()) { - for (auto& element : choices.front().getDistribution()) { - element.scaleValue(choiceCount); - } - } - choiceIsGuaranteedDistribution = true; - } - - for (auto& choice : choices) { - if (!choiceIsGuaranteedDistribution) { - // Create a proper distribution without duplicate entries. - choice.makeUniqueAndShrink(); - } - - // Add the elements to the transition matrix. - for (auto const& element : choice.getDistribution()) { - modelComponents.transitionMatrixBuilder.addNextValue(currentRow, element.getColumn(), element.getValue()); - } - - // Proceed to next row. - ++currentRow; - } - } - - 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); - } - } - - static JitModelBuilderInterface* create() { - return new JitBuilder(); - } - - private: - spp::sparse_hash_map stateIds; - std::vector initialStates; - - uint64_t currentRow; - ModelComponents modelComponents; - }; - - BOOST_DLL_ALIAS(storm::builder::JitBuilder::create, create_builder) - - } -} -)"; - - cpptempl::data_map modelData; - modelData["stateVariables"] = generateStateVariables(); - cpptempl::data_list initialStates = generateInitialStates(); - modelData["initialStates"] = cpptempl::make_data(initialStates); - cpptempl::data_list nonSynchronizingEdges = generateNonSynchronizingEdges(); - modelData["nonSynchronizingEdges"] = cpptempl::make_data(nonSynchronizingEdges); - modelData["deterministic_model"] = model.isDeterministicModel() ? "true" : "false"; - modelData["discrete_time_model"] = model.isDiscreteTimeModel() ? "true" : "false"; - return cpptempl::parse(sourceTemplate, modelData); - } - - template - cpptempl::data_list ExplicitJitJaniModelBuilder::generateInitialStates() { - 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(true)); - - // 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& automaton : this->model.getAutomata()) { - 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 : this->model.getAutomata()) { - initialLocationsIterators.push_back(automaton.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 = this->model.getAutomata()[index]; - 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] == this->model.getAutomata()[index].getInitialLocationIndices().cend()) { - initialLocationsIterators[index] = this->model.getAutomata()[index].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::generateStateVariables() { - cpptempl::data_list booleanVariables; - cpptempl::data_list boundedIntegerVariables; - cpptempl::data_list locationVariables; - - for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) { - cpptempl::data_map booleanVariable; - std::string variableName = getQualifiedVariableName(variable); - variableToName[variable.getExpressionVariable()] = variableName; - booleanVariable["name"] = variableName; - booleanVariables.push_back(booleanVariable); - } - for (auto const& variable : model.getGlobalVariables().getBoundedIntegerVariables()) { - cpptempl::data_map boundedIntegerVariable; - std::string variableName = getQualifiedVariableName(variable); - variableToName[variable.getExpressionVariable()] = variableName; - - uint64_t range = static_cast(variable.getUpperBound().evaluateAsInt() - variable.getLowerBound().evaluateAsInt() + 1); - uint64_t numberOfBits = static_cast(std::ceil(std::log2(range))); - - boundedIntegerVariable["name"] = variableName; - boundedIntegerVariable["numberOfBits"] = std::to_string(numberOfBits); - boundedIntegerVariables.push_back(boundedIntegerVariable); - } - for (auto const& automaton : model.getAutomata()) { - for (auto const& variable : automaton.getVariables().getBooleanVariables()) { - cpptempl::data_map booleanVariable; - std::string variableName = getQualifiedVariableName(automaton, variable); - variableToName[variable.getExpressionVariable()] = variableName; - booleanVariable["name"] = variableName; - booleanVariables.push_back(booleanVariable); - } - for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) { - cpptempl::data_map boundedIntegerVariable; - std::string variableName = getQualifiedVariableName(automaton, variable); - variableToName[variable.getExpressionVariable()] = variableName; - - uint64_t range = static_cast(variable.getUpperBound().evaluateAsInt() - variable.getLowerBound().evaluateAsInt()); - uint64_t numberOfBits = static_cast(std::ceil(std::log2(range))); - - boundedIntegerVariable["name"] = variableName; - boundedIntegerVariable["numberOfBits"] = std::to_string(numberOfBits); - boundedIntegerVariables.push_back(boundedIntegerVariable); - } - - // Only generate a location variable if there is more than one location for the automaton. - if (automaton.getNumberOfLocations() > 1) { - cpptempl::data_map locationVariable; - locationVariable["name"] = getLocationVariableName(automaton); - locationVariable["numberOfBits"] = static_cast(std::ceil(std::log2(automaton.getNumberOfLocations()))); - locationVariables.push_back(locationVariable); - } - } - - cpptempl::data_map stateVariables; - stateVariables["boolean"] = cpptempl::make_data(booleanVariables); - stateVariables["boundedInteger"] = cpptempl::make_data(boundedIntegerVariables); - stateVariables["locations"] = cpptempl::make_data(locationVariables); - return stateVariables; - } - - template - cpptempl::data_list ExplicitJitJaniModelBuilder::generateNonSynchronizingEdges() { - cpptempl::data_list edges; - for (auto const& automaton : this->model.getAutomata()) { - for (auto const& edge : automaton.getEdges()) { - if (edge.getActionIndex() == storm::jani::Model::SILENT_ACTION_INDEX) { - edges.push_back(generateEdge(edge)); - } - } - } - - return edges; - } - - template - cpptempl::data_map ExplicitJitJaniModelBuilder::generateEdge(storm::jani::Edge const& edge) { - cpptempl::data_map edgeData; - - cpptempl::data_list destinations; - for (auto const& destination : edge.getDestinations()) { - destinations.push_back(generateDestination(destination)); - } - - edgeData["guard"] = expressionTranslator.translate(edge.getGuard(), storm::expressions::ToCppTranslationOptions("sourceState.")); - edgeData["destinations"] = cpptempl::make_data(destinations); - return edgeData; - } - - template - cpptempl::data_map ExplicitJitJaniModelBuilder::generateDestination(storm::jani::EdgeDestination const& destination) { - cpptempl::data_map destinationData; - - cpptempl::data_list nonTransientAssignments; - for (auto const& assignment : destination.getOrderedAssignments().getNonTransientAssignments()) { - nonTransientAssignments.push_back(generateAssignment(assignment, "targetState.")); - } - - destinationData["nonTransientAssignments"] = cpptempl::make_data(nonTransientAssignments); - destinationData["value"] = expressionTranslator.translate(destination.getProbability(), storm::expressions::ToCppTranslationOptions("sourceState.", "double")); - return destinationData; - } - - 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"] = getLocationVariableName(automaton); - result["value"] = asString(value); - return result; - } - - template - cpptempl::data_map ExplicitJitJaniModelBuilder::generateAssignment(storm::jani::Assignment const& assignment, std::string const& prefix) { - cpptempl::data_map result; - result["variable"] = getVariableName(assignment.getExpressionVariable()); - result["value"] = expressionTranslator.translate(assignment.getAssignedExpression(), prefix); - return result; - } - - template - std::string const& ExplicitJitJaniModelBuilder::getVariableName(storm::expressions::Variable const& variable) const { - return variableToName.at(variable); - } - - template - std::string ExplicitJitJaniModelBuilder::getQualifiedVariableName(storm::jani::Variable const& variable) const { - return variable.getName(); - } - - template - std::string ExplicitJitJaniModelBuilder::getQualifiedVariableName(storm::jani::Automaton const& automaton, storm::jani::Variable const& variable) const { - return automaton.getName() + variable.getName(); - } - - template - std::string ExplicitJitJaniModelBuilder::getLocationVariableName(storm::jani::Automaton const& automaton) const { - return automaton.getName() + "_location"; - } - - template - std::string ExplicitJitJaniModelBuilder::asString(bool value) const { - std::stringstream out; - out << std::boolalpha << value; - return out.str(); - } - - 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()); - } - - 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; - } - - template - boost::filesystem::path ExplicitJitJaniModelBuilder::compileSourceToSharedLibrary(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; - 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 sparseModel = builder->build(); - - // (7) delete the shared library - boost::filesystem::remove(dynamicLibraryPath); - - // Return the constructed model. - return std::shared_ptr>(sparseModel); - } - - template class ExplicitJitJaniModelBuilder>; - template class ExplicitJitJaniModelBuilder>; - template class ExplicitJitJaniModelBuilder>; - - } -} diff --git a/src/builder/ExplicitJitJaniModelBuilder.h b/src/builder/ExplicitJitJaniModelBuilder.h deleted file mode 100644 index 769ba15c6..000000000 --- a/src/builder/ExplicitJitJaniModelBuilder.h +++ /dev/null @@ -1,83 +0,0 @@ -#pragma once - -#include - -#include -#include -#include - -#include "cpptempl.h" - -#include "src/storage/jani/Model.h" -#include "src/storage/expressions/ToCppVisitor.h" - -#include "src/models/sparse/StandardRewardModel.h" - -#include "src/builder/JitModelBuilderInterface.h" - -namespace storm { - namespace models { - namespace sparse { - template - class Model; - - template - class StandardRewardModel; - } - } - - namespace builder { - - template > - class ExplicitJitJaniModelBuilder { - public: - typedef JitModelBuilderInterface* (CreateFunctionType)(); - typedef boost::function ImportFunctionType; - - ExplicitJitJaniModelBuilder(storm::jani::Model const& model); - - std::shared_ptr> build(); - - 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); - - static boost::optional execute(std::string command); - - // Functions that generate data maps or data templates. - cpptempl::data_list generateInitialStates(); - cpptempl::data_map generateStateVariables(); - cpptempl::data_list generateNonSynchronizingEdges(); - - cpptempl::data_map generateEdge(storm::jani::Edge const& edge); - cpptempl::data_map generateDestination(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, std::string const& prefix = ""); - - // Auxiliary functions that perform regularly needed steps. - std::string const& getVariableName(storm::expressions::Variable const& variable) const; - std::string getQualifiedVariableName(storm::jani::Automaton const& automaton, storm::jani::Variable const& variable) const; - std::string getQualifiedVariableName(storm::jani::Variable const& variable) const; - std::string getLocationVariableName(storm::jani::Automaton const& automaton) const; - std::string asString(bool value) const; - - template - std::string asString(ValueTypePrime value) const; - - storm::jani::Model model; - typename ExplicitJitJaniModelBuilder::ImportFunctionType jitBuilderGetFunction; - std::unique_ptr> builder; - - std::unordered_map variableToName; - storm::expressions::ToCppVisitor expressionTranslator; - }; - - } -} diff --git a/src/builder/JitModelBuilderInterface.h b/src/builder/JitModelBuilderInterface.h deleted file mode 100644 index 05c7f67af..000000000 --- a/src/builder/JitModelBuilderInterface.h +++ /dev/null @@ -1,23 +0,0 @@ -#pragma once - -#include - -#include "src/models/sparse/Model.h" - -namespace storm { - namespace builder { - - template - class JitModelBuilderInterface { - public: - virtual ~JitModelBuilderInterface() { - // Intentionally left empty. - } - - virtual storm::models::sparse::Model* build() { - return nullptr; - } - }; - - } -} diff --git a/src/builder/jit/Choice.cpp b/src/builder/jit/Choice.cpp new file mode 100644 index 000000000..f5b5ce59b --- /dev/null +++ b/src/builder/jit/Choice.cpp @@ -0,0 +1,19 @@ +#include "src/builder/jit/Choice.h" + +namespace storm { + namespace builder { + namespace jit { + + template + void Choice::add(DistributionEntry const& entry) { + distribution.add(entry); + } + + template + Distribution const& Choice::getDistribution() const { + return distribution; + } + + } + } +} diff --git a/src/builder/jit/Choice.h b/src/builder/jit/Choice.h new file mode 100644 index 000000000..fb4e81f55 --- /dev/null +++ b/src/builder/jit/Choice.h @@ -0,0 +1,22 @@ +#pragma once + +#include "src/builder/jit/Distribution.h" + +namespace storm { + namespace builder { + namespace jit { + + template + class Choice { + public: + void add(DistributionEntry const& entry); + + Distribution const& getDistribution() const; + + private: + Distribution distribution; + }; + + } + } +} diff --git a/src/builder/jit/Distribution.cpp b/src/builder/jit/Distribution.cpp new file mode 100644 index 000000000..07599dcfd --- /dev/null +++ b/src/builder/jit/Distribution.cpp @@ -0,0 +1,43 @@ +#include "src/builder/jit/Distribution.h" + +namespace storm { + namespace builder { + namespace jit { + + template + void Distribution::add(DistributionEntry const& entry) { + storage.push_back(entry); + } + + template + void Distribution::compress() { + std::sort(storage.begin(), storage.end(), + [] (DistributionEntry const& a, DistributionEntry const& b) { + return a.getIndex() < b.getIndex(); + } + ); + + // Code taken from std::unique and modified to fit needs. + auto first = storage.begin(); + auto last = storage.end(); + + if (first != last) { + auto result = first; + while (++first != last) { + if (!(result->getColumn() == first->getColumn())) { + if (++result != first) { + *result = std::move(*first); + } + } else { + result->addToValue(first->getValue()); + } + } + ++result; + + storage.resize(std::distance(storage.begin(), result)); + } + } + + } + } +} diff --git a/src/builder/jit/Distribution.h b/src/builder/jit/Distribution.h new file mode 100644 index 000000000..15728b53a --- /dev/null +++ b/src/builder/jit/Distribution.h @@ -0,0 +1,44 @@ +#pragma once + +#include + +#include "src/builder/jit/DistributionEntry.h" + +namespace storm { + namespace builder { + namespace jit { + + template + class Distribution { + public: + typedef std::vector> ContainerType; + + /*! + * Adds the given entry to the distribution. + */ + void add(DistributionEntry const& entry); + + /*! + * Compresses the internal storage by summing the values of entries which agree on the index. As a side + * effect, this sorts the entries in the distribution by their index. + */ + void compress(); + + /*! + * Access to iterators over the entries of the distribution. Note that there may be multiple entries for + * the same index. Also, no order is guaranteed. After a call to compress, the order is guaranteed to be + * ascending wrt. index and there are no elements with the same index. + */ + typename ContainerType::iterator begin(); + typename ContainerType::const_iterator begin() const; + typename ContainerType::iterator end(); + typename ContainerType::const_iterator end() const; + + private: + // The underlying storage of the distribution. + ContainerType storage; + }; + + } + } +} diff --git a/src/builder/jit/DistributionEntry.cpp b/src/builder/jit/DistributionEntry.cpp new file mode 100644 index 000000000..146dd33eb --- /dev/null +++ b/src/builder/jit/DistributionEntry.cpp @@ -0,0 +1,24 @@ +#include "src/builder/jit/DistributionEntry.h" + +namespace storm { + namespace builder { + namespace jit { + + template + DistributionEntry::DistributionEntry(IndexType const& index, ValueType const& value) : index(index), value(value) { + // Intentionally left empty. + } + + template + IndexType const& DistributionEntry::getIndex() const { + return index; + } + + template + ValueType const& DistributionEntry::getValue() const { + return value; + } + + } + } +} diff --git a/src/builder/jit/DistributionEntry.h b/src/builder/jit/DistributionEntry.h new file mode 100644 index 000000000..6f8559ecd --- /dev/null +++ b/src/builder/jit/DistributionEntry.h @@ -0,0 +1,22 @@ +#pragma once + +namespace storm { + namespace builder { + namespace jit { + + template + class DistributionEntry { + public: + DistributionEntry(IndexType const& index, ValueType const& value); + + IndexType const& getIndex() const; + ValueType const& getValue() const; + + private: + IndexType index; + ValueType value; + }; + + } + } +} diff --git a/src/builder/jit/JitModelBuilderInterface.cpp b/src/builder/jit/JitModelBuilderInterface.cpp new file mode 100644 index 000000000..49b9b4409 --- /dev/null +++ b/src/builder/jit/JitModelBuilderInterface.cpp @@ -0,0 +1,24 @@ +#include "src/builder/jit/JitModelBuilderInterface.h" + +namespace storm { + namespace builder { + namespace jit { + + template + JitModelBuilderInterface::JitModelBuilderInterface(ModelComponentsBuilder& modelComponentsBuilder) : modelComponentsBuilder(modelComponentsBuilder) { + // Intentionally left empty. + } + + template + JitModelBuilderInterface::~JitModelBuilderInterface() { + // Intentionally left empty. + } + + template + void JitModelBuilderInterface::addStateBehaviour(StateBehaviour const& behaviour) { + modelComponentsBuilder.addStateBehaviour(behaviour); + } + + } + } +} diff --git a/src/builder/jit/ModelComponentBuilder.cpp b/src/builder/jit/ModelComponentBuilder.cpp new file mode 100644 index 000000000..e4aabc04d --- /dev/null +++ b/src/builder/jit/ModelComponentBuilder.cpp @@ -0,0 +1,64 @@ +#include "src/builder/jit/ModelComponentBuilder.h" + +#include "src/storage/SparseMatrix.h" + +namespace storm { + namespace builder { + namespace jit { + + template + ModelComponentsBuilder::ModelComponentsBuilder(storm::jani::ModelType const& modelType) : modelType(modelType), isDeterministicModel(storm::jani::isDeterministicModel(modelType)), isDiscreteTimeModel(storm::jani::isDiscreteTimeModel(modelType)), transitionMatrixBuilder(std::make_unique>(0, 0, 0, true, !isDeterministicModel)) { + // Intentionally left empty. + } + + template + void ModelComponentsBuilder::addStateBehaviour(StateBehaviour const& behaviour) { + // If there is more than one choice in a deterministic model, we need to combine the choices into one + // global choice. + bool choiceIsGuaranteedDistribution = false; + if (model_is_deterministic() && choices.size() > 1) { + uint64_t choiceCount = choices.size(); + + // We do this by adding the entries of choices after the first one to the first one and then making + // the distribution unique again. + for (auto it = ++choices.begin(), ite = choices.end(); it != ite; ++it) { + choices.front().add(std::move(*it)); + } + choices.resize(1); + choices.front().makeUniqueAndShrink(); + + // If we are dealing with a discrete-time model, we need to scale the probabilities such that they + // form a probability distribution. + if (model_is_discrete_time()) { + for (auto& element : choices.front().getDistribution()) { + element.scaleValue(choiceCount); + } + } + choiceIsGuaranteedDistribution = true; + } + + for (auto& choice : choices) { + if (!choiceIsGuaranteedDistribution) { + // Create a proper distribution without duplicate entries. + choice.makeUniqueAndShrink(); + } + + // Add the elements to the transition matrix. + for (auto const& element : choice.getDistribution()) { + modelComponents.transitionMatrixBuilder.addNextValue(currentRow, element.getColumn(), element.getValue()); + } + + // Proceed to next row. + ++currentRow; + } + } + + template + storm::models::sparse::Model>* ModelComponentsBuilder::build() { + // FIXME + return nullptr; + } + + } + } +} diff --git a/src/builder/jit/ModelComponentBuilder.h b/src/builder/jit/ModelComponentBuilder.h new file mode 100644 index 000000000..2929b6146 --- /dev/null +++ b/src/builder/jit/ModelComponentBuilder.h @@ -0,0 +1,46 @@ +#pragma once + +#include + +#include "src/builder/jit/StateBehaviour.h" + +#include "src/storage/jani/ModelType.h" + +namespace storm { + namespace storage { + template + class SparseMatrixBuilder; + } + + namespace models { + namespace sparse { + template + class StandardRewardModel; + + template + class Model; + } + } + + namespace builder { + namespace jit { + + template + class ModelComponentsBuilder { + public: + ModelComponentsBuilder(storm::jani::ModelType const& modelType); + + void addStateBehaviour(StateBehaviour const& behaviour); + + storm::models::sparse::Model>* build(); + + private: + storm::jani::ModelType modelType; + bool isDeterministicModel; + bool isDiscreteTimeModel; + std::unique_ptr> transitionMatrixBuilder; + }; + + } + } +} diff --git a/src/builder/jit/StateBehaviour.cpp b/src/builder/jit/StateBehaviour.cpp new file mode 100644 index 000000000..93a595fa2 --- /dev/null +++ b/src/builder/jit/StateBehaviour.cpp @@ -0,0 +1,25 @@ +#include "src/builder/jit/StateBehaviour.h" + +namespace storm { + namespace builder { + namespace jit { + + template + void StateBehaviour::addChoice(Choice&& choice) { + choices.emplace_back(std::move(choice)); + } + + template + Choice& StateBehaviour::addChoice() { + choices.emplace_back(); + return choices.back(); + } + + template + void StateBehaviour::clear() { + choices.clear(); + } + + } + } +} diff --git a/src/builder/jit/StateBehaviour.h b/src/builder/jit/StateBehaviour.h new file mode 100644 index 000000000..8b515b40e --- /dev/null +++ b/src/builder/jit/StateBehaviour.h @@ -0,0 +1,25 @@ +#pragma once + +#include "src/builder/jit/Choice.h" + +namespace storm { + namespace builder { + namespace jit { + + template + class StateBehaviour { + public: + typedef std::vector> ContainerType; + + void addChoice(Choice&& choice); + Choice& addChoice(); + + void clear(); + + private: + ContainerType choices; + }; + + } + } +} diff --git a/src/storage/jani/ModelType.cpp b/src/storage/jani/ModelType.cpp index 460145340..365c01195 100644 --- a/src/storage/jani/ModelType.cpp +++ b/src/storage/jani/ModelType.cpp @@ -78,5 +78,19 @@ namespace storm { return ModelType::UNDEFINED; } + bool isDeterministicModel(ModelType const& modelType) { + if (modelType == ModelType::DTMC && modelType == ModelType::DTMC) { + return true; + } + return false; + } + + bool isDiscreteTimeModel(ModelType const& modelType) { + if (modelType == ModelType::DTMC || modelType == ModelType::MDP) { + return true; + } + return false; + } + } } diff --git a/src/storage/jani/ModelType.h b/src/storage/jani/ModelType.h index c8a906d6c..9d71763db 100644 --- a/src/storage/jani/ModelType.h +++ b/src/storage/jani/ModelType.h @@ -13,5 +13,8 @@ namespace storm { std::string to_string(ModelType const& type); std::ostream& operator<<(std::ostream& stream, ModelType const& type); + bool isDeterministicModel(ModelType const& modelType); + bool isDiscreteTimeModel(ModelType const& modelType); + } -} \ No newline at end of file +} diff --git a/src/utility/storm.h b/src/utility/storm.h index ef87ec104..705a58034 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -47,7 +47,7 @@ // Headers of builders. #include "src/builder/ExplicitModelBuilder.h" -#include "src/builder/ExplicitJitJaniModelBuilder.h" +#include "src/builder/jit/ExplicitJitJaniModelBuilder.h" #include "src/builder/DdPrismModelBuilder.h" #include "src/builder/DdJaniModelBuilder.h" @@ -118,7 +118,7 @@ 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::ExplicitJitJaniModelBuilder builder(model.asJaniModel()); + storm::builder::jit::ExplicitJitJaniModelBuilder builder(model.asJaniModel()); return builder.build(); } else { std::shared_ptr> generator;