diff --git a/src/builder/ExplicitJitJaniModelBuilder.cpp b/src/builder/ExplicitJitJaniModelBuilder.cpp index fc042874e..ece9175f2 100644 --- a/src/builder/ExplicitJitJaniModelBuilder.cpp +++ b/src/builder/ExplicitJitJaniModelBuilder.cpp @@ -2,74 +2,679 @@ #include #include +#include -#include "cpptempl.h" +#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"; - static const std::string STORM_ROOT = "/Users/chris/work/storm2"; - static const std::string BOOST_ROOT = "/usr/local/Cellar/boost/1.61.0_1/include"; + 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) { + template + ExplicitJitJaniModelBuilder::ExplicitJitJaniModelBuilder(storm::jani::Model const& model) : model(model) { // Intentionally left empty. } - template - std::string ExplicitJitJaniModelBuilder::createSourceCode() { + template + std::string ExplicitJitJaniModelBuilder::createSourceCode() { std::string sourceTemplate = R"( - #include - #include - #include +#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; + } - #include "src/builder/JitModelBuilderInterface.h" - #include "resources/3rdparty/sparsepp/sparsepp.h" + 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); + } - namespace storm { - namespace builder { + 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; + } + } + }; - struct StateType { - {% for stateVariable in stateVariables %}int64_t {$stateVariable.name} : {$stateVariable.bitwidth};{% endfor %} - }; + 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(); - class JitBuilder : public JitModelBuilderInterface { - public: - JitBuilder() { - // Intentionally left empty. + // 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(); + } - virtual void build() override { - std::cout << "building in progress" << std::endl; - } + 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)); - static JitModelBuilderInterface* create() { - return new JitBuilder(); - } + 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)); - private: - spp::sparse_hash_map stateIds; - }; + 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)); - BOOST_DLL_ALIAS(storm::builder::JitBuilder::create, create_builder) + 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); } - )"; - cpptempl::data_map modelData; - return cpptempl::parse(sourceTemplate, modelData); + return initialStates; } - template - boost::optional ExplicitJitJaniModelBuilder::execute(std::string command) { + 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"; @@ -85,22 +690,25 @@ namespace storm { } 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"); + + 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) { + 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; @@ -108,14 +716,14 @@ namespace storm { return temporaryFile; } - template - boost::filesystem::path ExplicitJitJaniModelBuilder::compileSourceToSharedLibrary(boost::filesystem::path const& sourceFile) { + 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" + BOOST_ROOT + " -o " + dynamicLibraryFilename; + 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) { @@ -126,11 +734,16 @@ namespace storm { return dynamicLibraryPath; } - template - std::shared_ptr>> ExplicitJitJaniModelBuilder::build() { - + template + std::shared_ptr> ExplicitJitJaniModelBuilder::build() { + // (1) generate the source code of the shared library - std::string source = createSourceCode(); + 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 @@ -146,20 +759,20 @@ namespace storm { // (5) create the loader from the shared library createBuilder(dynamicLibraryPath); - + // (6) execute the function in the shared lib - builder->build(); - - // (7) use result to build the model - - // (8) delete the shared library + auto sparseModel = builder->build(); + + // (7) delete the shared library boost::filesystem::remove(dynamicLibraryPath); - // FIXME - return nullptr; + // Return the constructed model. + return std::shared_ptr>(sparseModel); } - - template class ExplicitJitJaniModelBuilder; + + template class ExplicitJitJaniModelBuilder>; + template class ExplicitJitJaniModelBuilder>; + template class ExplicitJitJaniModelBuilder>; } } diff --git a/src/builder/ExplicitJitJaniModelBuilder.h b/src/builder/ExplicitJitJaniModelBuilder.h index dbb28fd18..769ba15c6 100644 --- a/src/builder/ExplicitJitJaniModelBuilder.h +++ b/src/builder/ExplicitJitJaniModelBuilder.h @@ -6,7 +6,12 @@ #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" @@ -23,7 +28,7 @@ namespace storm { namespace builder { - template + template > class ExplicitJitJaniModelBuilder { public: typedef JitModelBuilderInterface* (CreateFunctionType)(); @@ -31,7 +36,7 @@ namespace storm { ExplicitJitJaniModelBuilder(storm::jani::Model const& model); - std::shared_ptr>> build(); + std::shared_ptr> build(); private: void createBuilder(boost::filesystem::path const& dynamicLibraryPath); @@ -41,9 +46,37 @@ namespace storm { static boost::optional execute(std::string command); - storm::jani::Model const& model; - typename ExplicitJitJaniModelBuilder::ImportFunctionType jitBuilderGetFunction; + // 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 index d88dcfc82..05c7f67af 100644 --- a/src/builder/JitModelBuilderInterface.h +++ b/src/builder/JitModelBuilderInterface.h @@ -1,5 +1,9 @@ #pragma once +#include + +#include "src/models/sparse/Model.h" + namespace storm { namespace builder { @@ -10,8 +14,8 @@ namespace storm { // Intentionally left empty. } - virtual void build() { - // Intentionally left empty. + virtual storm::models::sparse::Model* build() { + return nullptr; } }; diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index f4b009b7e..549072728 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -7,6 +7,7 @@ #include "src/exceptions/NotImplementedException.h" #include "src/exceptions/InvalidSettingsException.h" +#include "src/exceptions/UnexpectedException.h" namespace storm { namespace cli { @@ -201,6 +202,8 @@ namespace storm { void buildAndCheckSymbolicModelWithSparseEngine(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { // Start by building the model. std::shared_ptr markovModel = buildSparseModel(model, formulas); + + STORM_LOG_THROW(markovModel, storm::exceptions::UnexpectedException, "The model was not successfully built."); // Print some information about the model. markovModel->printModelInformationToStream(std::cout); diff --git a/src/settings/modules/IOSettings.cpp b/src/settings/modules/IOSettings.cpp index c174f1f51..e92cd2556 100644 --- a/src/settings/modules/IOSettings.cpp +++ b/src/settings/modules/IOSettings.cpp @@ -20,6 +20,7 @@ namespace storm { const std::string IOSettings::prismInputOptionName = "prism"; const std::string IOSettings::janiInputOptionName = "jani"; const std::string IOSettings::prismToJaniOptionName = "prism2jani"; + const std::string IOSettings::jitOptionName = "jit"; const std::string IOSettings::explorationOrderOptionName = "explorder"; const std::string IOSettings::explorationOrderOptionShortName = "eo"; const std::string IOSettings::transitionRewardsOptionName = "transrew"; @@ -44,6 +45,7 @@ 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()); std::vector explorationOrders = {"dfs", "bfs"}; this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName) @@ -102,6 +104,10 @@ namespace storm { std::string IOSettings::getJaniInputFilename() const { return this->getOption(janiInputOptionName).getArgumentByName("filename").getValueAsString(); } + + bool IOSettings::isJitSet() const { + return this->getOption(jitOptionName).getHasOptionBeenSet(); + } bool IOSettings::isExplorationOrderSet() const { return this->getOption(explorationOrderOptionName).getHasOptionBeenSet(); diff --git a/src/settings/modules/IOSettings.h b/src/settings/modules/IOSettings.h index ae6ce6831..6b9810873 100644 --- a/src/settings/modules/IOSettings.h +++ b/src/settings/modules/IOSettings.h @@ -102,6 +102,13 @@ namespace storm { */ std::string getJaniInputFilename() const; + /*! + * Retrieves whether the option to use the JIT builder is set. + * + * @return True iff the JIT builder is to be used. + */ + bool isJitSet() const; + /*! * Retrieves whether the model exploration order was set. * @@ -206,6 +213,7 @@ namespace storm { static const std::string prismInputOptionName; static const std::string janiInputOptionName; static const std::string prismToJaniOptionName; + static const std::string jitOptionName; static const std::string explorationOrderOptionName; static const std::string explorationOrderOptionShortName; static const std::string transitionRewardsOptionName; diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 5389e6e85..f5447995a 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -24,20 +24,19 @@ namespace storm { template class TopologicalValueIterationMinMaxLinearEquationSolver; } - - } namespace storm { namespace storage { class BitVector; + // Forward declare matrix class. - template class SparseMatrix; + template + class SparseMatrix; typedef uint_fast64_t SparseMatrixIndexType; - template class MatrixEntry { public: diff --git a/src/storage/bisimulation/BisimulationDecomposition.h b/src/storage/bisimulation/BisimulationDecomposition.h index 6507e3b07..eac212781 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.h +++ b/src/storage/bisimulation/BisimulationDecomposition.h @@ -90,7 +90,6 @@ namespace storm { */ void preserveFormula(ModelType const& model, storm::logic::Formula const& formula); - /** * Sets the bisimulation type. If the bisimulation type is set to weak, * we also change the bounded flag (as bounded properties are not preserved under @@ -123,6 +122,7 @@ namespace storm { assert(optimalityType); return optimalityType.get(); } + // A flag that indicates whether a measure driven initial partition is to be used. If this flag is set // to true, the two optional pairs phiStatesAndLabel and psiStatesAndLabel must be set. Then, the // measure driven initial partition wrt. to the states phi and psi is taken. diff --git a/src/storage/expressions/ToCppVisitor.cpp b/src/storage/expressions/ToCppVisitor.cpp new file mode 100644 index 000000000..08043120c --- /dev/null +++ b/src/storage/expressions/ToCppVisitor.cpp @@ -0,0 +1,268 @@ +#include "src/storage/expressions/ToCppVisitor.h" + +#include "src/storage/expressions/Expressions.h" + +namespace storm { + namespace expressions { + + ToCppTranslationOptions::ToCppTranslationOptions(std::string const& prefix, std::string const& valueTypeCast) : valueTypeCast(valueTypeCast), prefix(prefix) { + // Intentionally left empty. + } + + std::string const& ToCppTranslationOptions::getPrefix() const { + return prefix; + } + + bool ToCppTranslationOptions::hasValueTypeCast() const { + return !valueTypeCast.empty(); + } + + std::string const& ToCppTranslationOptions::getValueTypeCast() const { + return valueTypeCast; + } + + void ToCppTranslationOptions::clearValueTypeCast() { + valueTypeCast = ""; + } + + std::string ToCppVisitor::translate(storm::expressions::Expression const& expression, ToCppTranslationOptions const& options) { + expression.accept(*this, options); + std::string result = stream.str(); + stream.str(""); + return result; + } + + boost::any ToCppVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) { + ToCppTranslationOptions conditionOptions = boost::any_cast(data); + conditionOptions.clearValueTypeCast(); + stream << "("; + expression.getCondition()->accept(*this, conditionOptions); + stream << " ? "; + expression.getThenExpression()->accept(*this, data); + stream << " : "; + expression.getElseExpression()->accept(*this, data); + stream << ")"; + return boost::none; + } + + boost::any ToCppVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { + ToCppTranslationOptions newOptions = boost::any_cast(data); + newOptions.clearValueTypeCast(); + + switch (expression.getOperatorType()) { + case BinaryBooleanFunctionExpression::OperatorType::And: + stream << "("; + expression.getFirstOperand()->accept(*this, newOptions); + stream << " && "; + expression.getSecondOperand()->accept(*this, newOptions); + stream << ")"; + break; + case BinaryBooleanFunctionExpression::OperatorType::Or: + stream << "("; + expression.getFirstOperand()->accept(*this, newOptions); + stream << " || "; + expression.getSecondOperand()->accept(*this, newOptions); + stream << ")"; + break; + case BinaryBooleanFunctionExpression::OperatorType::Xor: + stream << "("; + expression.getFirstOperand()->accept(*this, newOptions); + stream << " ^ "; + expression.getSecondOperand()->accept(*this, newOptions); + stream << ")"; + break; + case BinaryBooleanFunctionExpression::OperatorType::Implies: + stream << "(!"; + expression.getFirstOperand()->accept(*this, newOptions); + stream << " || "; + expression.getSecondOperand()->accept(*this, newOptions); + stream << ")"; + break; + case BinaryBooleanFunctionExpression::OperatorType::Iff: + stream << "!("; + expression.getFirstOperand()->accept(*this, newOptions); + stream << " ^ "; + expression.getSecondOperand()->accept(*this, newOptions); + stream << ")"; + break; + } + return boost::none; + } + + boost::any ToCppVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) { + switch (expression.getOperatorType()) { + case BinaryNumericalFunctionExpression::OperatorType::Plus: + stream << "("; + expression.getFirstOperand()->accept(*this, data); + stream << " + "; + expression.getSecondOperand()->accept(*this, data); + stream << ")"; + break; + case BinaryNumericalFunctionExpression::OperatorType::Minus: + stream << "("; + expression.getFirstOperand()->accept(*this, data); + stream << " - "; + expression.getSecondOperand()->accept(*this, data); + stream << ")"; + break; + case BinaryNumericalFunctionExpression::OperatorType::Times: + stream << "("; + expression.getFirstOperand()->accept(*this, data); + stream << " * "; + expression.getSecondOperand()->accept(*this, data); + stream << ")"; + break; + case BinaryNumericalFunctionExpression::OperatorType::Divide: + stream << "("; + expression.getFirstOperand()->accept(*this, data); + stream << " / "; + expression.getSecondOperand()->accept(*this, data); + stream << ")"; + break; + case BinaryNumericalFunctionExpression::OperatorType::Min: + stream << "std::min("; + expression.getFirstOperand()->accept(*this, data); + stream << ", "; + expression.getSecondOperand()->accept(*this, data); + stream << ")"; + break; + case BinaryNumericalFunctionExpression::OperatorType::Max: + stream << "std::max("; + expression.getFirstOperand()->accept(*this, data); + stream << ", "; + expression.getSecondOperand()->accept(*this, data); + stream << ")"; + break; + case BinaryNumericalFunctionExpression::OperatorType::Power: + stream << "std::pow("; + expression.getFirstOperand()->accept(*this, data); + stream << ", "; + expression.getSecondOperand()->accept(*this, data); + stream << ")"; + break; + } + return boost::none; + } + + boost::any ToCppVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) { + ToCppTranslationOptions newOptions = boost::any_cast(data); + newOptions.clearValueTypeCast(); + + switch (expression.getRelationType()) { + case BinaryRelationExpression::RelationType::Equal: + stream << "("; + expression.getFirstOperand()->accept(*this, newOptions); + stream << " == "; + expression.getSecondOperand()->accept(*this, newOptions); + stream << ")"; + break; + case BinaryRelationExpression::RelationType::NotEqual: + stream << "("; + expression.getFirstOperand()->accept(*this, newOptions); + stream << " != "; + expression.getSecondOperand()->accept(*this, newOptions); + stream << ")"; + break; + case BinaryRelationExpression::RelationType::Less: + stream << "("; + expression.getFirstOperand()->accept(*this, newOptions); + stream << " < "; + expression.getSecondOperand()->accept(*this, newOptions); + stream << ")"; + break; + case BinaryRelationExpression::RelationType::LessOrEqual: + stream << "("; + expression.getFirstOperand()->accept(*this, newOptions); + stream << " <= "; + expression.getSecondOperand()->accept(*this, newOptions); + stream << ")"; + break; + case BinaryRelationExpression::RelationType::Greater: + stream << "("; + expression.getFirstOperand()->accept(*this, newOptions); + stream << " > "; + expression.getSecondOperand()->accept(*this, newOptions); + stream << ")"; + break; + case BinaryRelationExpression::RelationType::GreaterOrEqual: + stream << "("; + expression.getFirstOperand()->accept(*this, newOptions); + stream << " >= "; + expression.getSecondOperand()->accept(*this, newOptions); + stream << ")"; + break; + } + return boost::none; + } + + boost::any ToCppVisitor::visit(VariableExpression const& expression, boost::any const& data) { + ToCppTranslationOptions const& options = boost::any_cast(data); + if (options.hasValueTypeCast()) { + stream << "static_cast<" << options.getValueTypeCast() << ">("; + } + stream << options.getPrefix() << expression.getVariableName(); + if (options.hasValueTypeCast()) { + stream << ")"; + } + return boost::none; + } + + boost::any ToCppVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { + ToCppTranslationOptions newOptions = boost::any_cast(data); + newOptions.clearValueTypeCast(); + + switch (expression.getOperatorType()) { + case UnaryBooleanFunctionExpression::OperatorType::Not: + stream << "!("; + expression.getOperand()->accept(*this, newOptions); + stream << ")"; + break; + } + return boost::none; + } + + boost::any ToCppVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) { + switch (expression.getOperatorType()) { + case UnaryNumericalFunctionExpression::OperatorType::Minus: + stream << "-("; + expression.getOperand()->accept(*this, data); + stream << ")"; + break; + case UnaryNumericalFunctionExpression::OperatorType::Floor: + stream << "std::floor("; + expression.getOperand()->accept(*this, data); + stream << ")"; + break; + case UnaryNumericalFunctionExpression::OperatorType::Ceil: + stream << "std::ceil("; + expression.getOperand()->accept(*this, data); + stream << ")"; + break; + } + return boost::none; + } + + boost::any ToCppVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) { + stream << std::boolalpha << expression.getValue(); + return boost::none; + } + + boost::any ToCppVisitor::visit(IntegerLiteralExpression const& expression, boost::any const& data) { + ToCppTranslationOptions const& options = boost::any_cast(data); + if (options.hasValueTypeCast()) { + stream << "static_cast<" << options.getValueTypeCast() << ">("; + } + stream << expression.getValue(); + if (options.hasValueTypeCast()) { + stream << ")"; + } + return boost::none; + } + + boost::any ToCppVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) { + stream << expression.getValueAsDouble(); + return boost::none; + } + + } +} diff --git a/src/storage/expressions/ToCppVisitor.h b/src/storage/expressions/ToCppVisitor.h new file mode 100644 index 000000000..7b65c6af4 --- /dev/null +++ b/src/storage/expressions/ToCppVisitor.h @@ -0,0 +1,46 @@ +#pragma once + +#include + +#include "src/storage/expressions/ExpressionVisitor.h" + +namespace storm { + namespace expressions { + class Expression; + + class ToCppTranslationOptions { + public: + ToCppTranslationOptions(std::string const& prefix = "", std::string const& valueTypeCast = ""); + + std::string const& getPrefix() const; + + bool hasValueTypeCast() const; + std::string const& getValueTypeCast() const; + void clearValueTypeCast(); + + private: + std::string valueTypeCast; + std::string prefix; + }; + + class ToCppVisitor : public ExpressionVisitor { + public: + std::string translate(storm::expressions::Expression const& expression, ToCppTranslationOptions const& options = ToCppTranslationOptions()); + + virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BinaryRelationExpression const& expression, boost::any const& data) override; + virtual boost::any visit(VariableExpression const& expression, boost::any const& data) override; + virtual boost::any visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) override; + virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override; + virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override; + virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override; + + private: + std::stringstream stream; + }; + + } +} diff --git a/src/utility/storm.h b/src/utility/storm.h index c5df89d64..ef87ec104 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -47,6 +47,7 @@ // Headers of builders. #include "src/builder/ExplicitModelBuilder.h" +#include "src/builder/ExplicitJitJaniModelBuilder.h" #include "src/builder/DdPrismModelBuilder.h" #include "src/builder/DdJaniModelBuilder.h" @@ -115,16 +116,22 @@ namespace storm { options.setBuildChoiceLabels(true); } - std::shared_ptr> generator; - if (model.isPrismProgram()) { - generator = std::make_shared>(model.asPrismProgram(), options); - } else if (model.isJaniModel()) { - generator = std::make_shared>(model.asJaniModel(), options); + 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()); + return builder.build(); } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot build sparse model from this symbolic model description."); + std::shared_ptr> generator; + if (model.isPrismProgram()) { + generator = std::make_shared>(model.asPrismProgram(), options); + } else if (model.isJaniModel()) { + generator = std::make_shared>(model.asJaniModel(), options); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot build sparse model from this symbolic model description."); + } + storm::builder::ExplicitModelBuilder builder(generator); + return builder.build(); } - storm::builder::ExplicitModelBuilder builder(generator); - return builder.build(); } template