From 71f2e83bc0792909bdfb1d8a7b8b05f635e5150e Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 26 Oct 2016 16:52:17 +0200 Subject: [PATCH] completed moving from monolithic generation to callback-based approach. added building labels to jit-based model builder, added support for options of other builders (selection of labels, reward models, etc) Former-commit-id: 5729c1c8ca7796b2c81a5fb744b0a8f7f13c7b39 [formerly 890198a9078aba74ebf43e5b69adb1acc1749815] Former-commit-id: df2528638d2c9593327c0a10c5457dcd6c701001 --- src/builder/BuilderOptions.cpp | 188 +++++ src/builder/jit/Choice.cpp | 39 + src/builder/jit/Choice.h | 10 + src/builder/jit/Distribution.cpp | 95 ++- src/builder/jit/Distribution.h | 19 + src/builder/jit/DistributionEntry.cpp | 21 + src/builder/jit/DistributionEntry.h | 4 + .../jit/ExplicitJitJaniModelBuilder.cpp | 716 ++++++++++++++++++ src/builder/jit/ExplicitJitJaniModelBuilder.h | 93 +++ src/builder/jit/JitModelBuilderInterface.cpp | 10 +- src/builder/jit/ModelComponentBuilder.cpp | 64 -- src/builder/jit/ModelComponentsBuilder.cpp | 76 ++ ...nentBuilder.h => ModelComponentsBuilder.h} | 16 +- src/builder/jit/StateBehaviour.cpp | 56 ++ src/builder/jit/StateBehaviour.h | 11 + src/generator/NextStateGenerator.cpp | 178 +---- src/generator/NextStateGenerator.h | 116 +-- src/utility/storm.h | 5 +- 18 files changed, 1335 insertions(+), 382 deletions(-) create mode 100644 src/builder/BuilderOptions.cpp create mode 100644 src/builder/jit/ExplicitJitJaniModelBuilder.cpp create mode 100644 src/builder/jit/ExplicitJitJaniModelBuilder.h delete mode 100644 src/builder/jit/ModelComponentBuilder.cpp create mode 100644 src/builder/jit/ModelComponentsBuilder.cpp rename src/builder/jit/{ModelComponentBuilder.h => ModelComponentsBuilder.h} (62%) diff --git a/src/builder/BuilderOptions.cpp b/src/builder/BuilderOptions.cpp new file mode 100644 index 000000000..438aa72cd --- /dev/null +++ b/src/builder/BuilderOptions.cpp @@ -0,0 +1,188 @@ +#include "src/builder/BuilderOptions.h" + +#include "src/logic/Formulas.h" + +#include "src/utility/macros.h" +#include "src/exceptions/InvalidSettingsException.h" + +namespace storm { + namespace builder { + + LabelOrExpression::LabelOrExpression(storm::expressions::Expression const& expression) : labelOrExpression(expression) { + // Intentionally left empty. + } + + LabelOrExpression::LabelOrExpression(std::string const& label) : labelOrExpression(label) { + // Intentionally left empty. + } + + bool LabelOrExpression::isLabel() const { + return labelOrExpression.which() == 0; + } + + std::string const& LabelOrExpression::getLabel() const { + return boost::get(labelOrExpression); + } + + bool LabelOrExpression::isExpression() const { + return labelOrExpression.which() == 1; + } + + storm::expressions::Expression const& LabelOrExpression::getExpression() const { + return boost::get(labelOrExpression); + } + + BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false) { + // Intentionally left empty. + } + + BuilderOptions::BuilderOptions(storm::logic::Formula const& formula) : BuilderOptions() { + this->preserveFormula(formula); + this->setTerminalStatesFromFormula(formula); + } + + BuilderOptions::BuilderOptions(std::vector> const& formulas) : BuilderOptions() { + if (!formulas.empty()) { + for (auto const& formula : formulas) { + this->preserveFormula(*formula); + } + if (formulas.size() == 1) { + this->setTerminalStatesFromFormula(*formulas.front()); + } + } + } + + void BuilderOptions::preserveFormula(storm::logic::Formula const& formula) { + // If we already had terminal states, we need to erase them. + if (hasTerminalStates()) { + clearTerminalStates(); + } + + // Determine the reward models we need to build. + std::set referencedRewardModels = formula.getReferencedRewardModels(); + for (auto const& rewardModelName : referencedRewardModels) { + rewardModelNames.push_back(rewardModelName); + } + + // Extract all the labels used in the formula. + std::vector> atomicLabelFormulas = formula.getAtomicLabelFormulas(); + for (auto const& formula : atomicLabelFormulas) { + addLabel(formula->getLabel()); + } + + // Extract all the expressions used in the formula. + std::vector> atomicExpressionFormulas = formula.getAtomicExpressionFormulas(); + for (auto const& formula : atomicExpressionFormulas) { + addLabel(formula->getExpression()); + } + } + + void BuilderOptions::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { + if (formula.isAtomicExpressionFormula()) { + addTerminalExpression(formula.asAtomicExpressionFormula().getExpression(), true); + } else if (formula.isAtomicLabelFormula()) { + addTerminalLabel(formula.asAtomicLabelFormula().getLabel(), true); + } else if (formula.isEventuallyFormula()) { + storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula(); + if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) { + this->setTerminalStatesFromFormula(sub); + } + } else if (formula.isUntilFormula()) { + storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula(); + if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { + this->setTerminalStatesFromFormula(right); + } + storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula(); + if (left.isAtomicExpressionFormula()) { + addTerminalExpression(left.asAtomicExpressionFormula().getExpression(), false); + } else if (left.isAtomicLabelFormula()) { + addTerminalLabel(left.asAtomicLabelFormula().getLabel(), false); + } + } else if (formula.isProbabilityOperatorFormula()) { + storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula(); + if (sub.isEventuallyFormula() || sub.isUntilFormula()) { + this->setTerminalStatesFromFormula(sub); + } + } + } + + std::vector const& BuilderOptions::getRewardModelNames() const { + return rewardModelNames; + } + + std::set const& BuilderOptions::getLabelNames() const { + return labelNames; + } + + std::vector const& BuilderOptions::getExpressionLabels() const { + return expressionLabels; + } + + std::vector> const& BuilderOptions::getTerminalStates() const { + return terminalStates; + } + + bool BuilderOptions::hasTerminalStates() const { + return !terminalStates.empty(); + } + + void BuilderOptions::clearTerminalStates() { + terminalStates.clear(); + } + + bool BuilderOptions::isBuildChoiceLabelsSet() const { + return buildChoiceLabels; + } + + bool BuilderOptions::isBuildAllRewardModelsSet() const { + return buildAllRewardModels; + } + + bool BuilderOptions::isBuildAllLabelsSet() const { + return buildAllLabels; + } + + BuilderOptions& BuilderOptions::setBuildAllRewardModels() { + buildAllRewardModels = true; + return *this; + } + + BuilderOptions& BuilderOptions::addRewardModel(std::string const& rewardModelName) { + STORM_LOG_THROW(!buildAllRewardModels, storm::exceptions::InvalidSettingsException, "Cannot add reward model, because all reward models are built anyway."); + rewardModelNames.emplace_back(rewardModelName); + return *this; + } + + BuilderOptions& BuilderOptions::setBuildAllLabels() { + buildAllLabels = true; + return *this; + } + + BuilderOptions& BuilderOptions::addLabel(storm::expressions::Expression const& expression) { + expressionLabels.emplace_back(expression); + return *this; + } + + BuilderOptions& BuilderOptions::addLabel(std::string const& labelName) { + STORM_LOG_THROW(!buildAllLabels, storm::exceptions::InvalidSettingsException, "Cannot add label, because all labels are built anyway."); + labelNames.insert(labelName); + return *this; + } + + BuilderOptions& BuilderOptions::addTerminalExpression(storm::expressions::Expression const& expression, bool value) { + terminalStates.push_back(std::make_pair(LabelOrExpression(expression), value)); + return *this; + } + + BuilderOptions& BuilderOptions::addTerminalLabel(std::string const& label, bool value) { + terminalStates.push_back(std::make_pair(LabelOrExpression(label), value)); + return *this; + } + + BuilderOptions& BuilderOptions::setBuildChoiceLabels(bool newValue) { + buildChoiceLabels = newValue; + return *this; + } + + } +} diff --git a/src/builder/jit/Choice.cpp b/src/builder/jit/Choice.cpp index f5b5ce59b..461f0e88e 100644 --- a/src/builder/jit/Choice.cpp +++ b/src/builder/jit/Choice.cpp @@ -1,19 +1,58 @@ #include "src/builder/jit/Choice.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace builder { namespace jit { + template + Choice::Choice() : compressed(true) { + // Intentionally left empty. + } + template void Choice::add(DistributionEntry const& entry) { distribution.add(entry); } + + template + void Choice::add(IndexType const& index, ValueType const& value) { + distribution.add(index, value); + } + template + void Choice::add(Choice&& choice) { + distribution.add(std::move(choice.getDistribution())); + } + template Distribution const& Choice::getDistribution() const { return distribution; } + template + void Choice::divideDistribution(ValueType const& value) { + distribution.divide(value); + } + + template + void Choice::compress() { + if (!compressed) { + distribution.compress(); + compressed = true; + } + } + + template + Distribution& Choice::getDistribution() { + return distribution; + } + + template class Choice; + template class Choice; + template class Choice; + } } } diff --git a/src/builder/jit/Choice.h b/src/builder/jit/Choice.h index fb4e81f55..4df890fea 100644 --- a/src/builder/jit/Choice.h +++ b/src/builder/jit/Choice.h @@ -9,12 +9,22 @@ namespace storm { template class Choice { public: + Choice(); + void add(DistributionEntry const& entry); + void add(IndexType const& index, ValueType const& value); + void add(Choice&& choice); Distribution const& getDistribution() const; + void divideDistribution(ValueType const& value); + + void compress(); private: + Distribution& getDistribution(); + Distribution distribution; + bool compressed; }; } diff --git a/src/builder/jit/Distribution.cpp b/src/builder/jit/Distribution.cpp index 07599dcfd..81dc6d459 100644 --- a/src/builder/jit/Distribution.cpp +++ b/src/builder/jit/Distribution.cpp @@ -1,43 +1,96 @@ #include "src/builder/jit/Distribution.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace builder { namespace jit { + template + Distribution::Distribution() : compressed(true) { + // Intentionally left empty. + } + template void Distribution::add(DistributionEntry const& entry) { storage.push_back(entry); + compressed = storage.back().getIndex() < entry.getIndex(); + } + + template + void Distribution::add(IndexType const& index, ValueType const& value) { + storage.emplace_back(index, value); + compressed = storage.back().getIndex() < index; + } + + template + void Distribution::add(Distribution&& distribution) { + storage.insert(storage.end(), std::make_move_iterator(distribution.begin()), std::make_move_iterator(distribution.end())); + compressed = false; } 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); + if (!compressed) { + 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->getIndex() == first->getIndex())) { + if (++result != first) { + *result = std::move(*first); + } + } else { + result->addToValue(first->getValue()); } - } else { - result->addToValue(first->getValue()); } + ++result; + + storage.resize(std::distance(storage.begin(), result)); } - ++result; - - storage.resize(std::distance(storage.begin(), result)); } } + template + void Distribution::divide(ValueType const& value) { + for (auto& entry : storage) { + entry.divide(value); + } + } + + template + typename Distribution::ContainerType::iterator Distribution::begin() { + return storage.begin(); + } + + template + typename Distribution::ContainerType::const_iterator Distribution::begin() const { + return storage.begin(); + } + + template + typename Distribution::ContainerType::iterator Distribution::end() { + return storage.end(); + } + + template + typename Distribution::ContainerType::const_iterator Distribution::end() const { + return storage.end(); + } + + template class Distribution; + template class Distribution; + template class Distribution; + } } } diff --git a/src/builder/jit/Distribution.h b/src/builder/jit/Distribution.h index 15728b53a..9ce989366 100644 --- a/src/builder/jit/Distribution.h +++ b/src/builder/jit/Distribution.h @@ -13,17 +13,34 @@ namespace storm { public: typedef std::vector> ContainerType; + Distribution(); + /*! * Adds the given entry to the distribution. */ void add(DistributionEntry const& entry); + /*! + * Adds the given entry to the distribution. + */ + void add(IndexType const& index, ValueType const& value); + + /*! + * Adds the given other distribution to the distribution. + */ + void add(Distribution&& distribution); + /*! * 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(); + /*! + * Divides all values in the distribution by the provided value. + */ + void divide(ValueType const& value); + /*! * 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 @@ -37,6 +54,8 @@ namespace storm { private: // The underlying storage of the distribution. ContainerType storage; + + bool compressed; }; } diff --git a/src/builder/jit/DistributionEntry.cpp b/src/builder/jit/DistributionEntry.cpp index 146dd33eb..b6b909881 100644 --- a/src/builder/jit/DistributionEntry.cpp +++ b/src/builder/jit/DistributionEntry.cpp @@ -1,9 +1,16 @@ #include "src/builder/jit/DistributionEntry.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace builder { namespace jit { + template + DistributionEntry::DistributionEntry() : index(0), value(0) { + // Intentionally left empty. + } + template DistributionEntry::DistributionEntry(IndexType const& index, ValueType const& value) : index(index), value(value) { // Intentionally left empty. @@ -19,6 +26,20 @@ namespace storm { return value; } + template + void DistributionEntry::addToValue(ValueType const& value) { + this->value += value; + } + + template + void DistributionEntry::divide(ValueType const& value) { + this->value /= value; + } + + template class DistributionEntry; + template class DistributionEntry; + template class DistributionEntry; + } } } diff --git a/src/builder/jit/DistributionEntry.h b/src/builder/jit/DistributionEntry.h index 6f8559ecd..fa0abc3fb 100644 --- a/src/builder/jit/DistributionEntry.h +++ b/src/builder/jit/DistributionEntry.h @@ -7,11 +7,15 @@ namespace storm { template class DistributionEntry { public: + DistributionEntry(); DistributionEntry(IndexType const& index, ValueType const& value); IndexType const& getIndex() const; ValueType const& getValue() const; + void addToValue(ValueType const& value); + void divide(ValueType const& value); + private: IndexType index; ValueType value; diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp new file mode 100644 index 000000000..41df6f10d --- /dev/null +++ b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -0,0 +1,716 @@ +#include "src/builder/jit/ExplicitJitJaniModelBuilder.h" + +#include +#include +#include + +#include "src/adapters/CarlAdapter.h" + +#include "src/solver/SmtSolver.h" + +#include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/StandardRewardModel.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 { + namespace jit { + + 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, storm::builder::BuilderOptions const& options) : options(options), model(model), modelComponentsBuilder(model.getModelType()) { + + for (auto const& automaton : this->model.getAutomata()) { + locationVariables.emplace(automaton.getName(), model.getManager().declareFreshIntegerVariable(false, automaton.getName() + "_")); + } + } + + template + std::string ExplicitJitJaniModelBuilder::createSourceCode() { + std::string sourceTemplate = R"( + +#define NDEBUG + +#include +#include +#include +#include +#include +#include +#include + +#include "resources/3rdparty/sparsepp/sparsepp.h" + +#include "src/builder/jit/JitModelBuilderInterface.h" +#include "src/builder/jit/StateBehaviour.h" +#include "src/builder/jit/ModelComponentsBuilder.h" + + namespace storm { + namespace builder { + namespace jit { + + typedef uint32_t IndexType; + typedef double ValueType; + + 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::jit::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 { + namespace jit { + + static bool model_is_deterministic() { + return {$deterministic_model}; + } + + static bool model_is_discrete_time() { + return {$discrete_time_model}; + } + + class StateSet { + public: + StateType const& peek() const { + return storage.front(); + } + + StateType get() { + StateType result = std::move(storage.front()); + storage.pop(); + return result; + } + + void add(StateType const& state) { + storage.push(state); + } + + bool empty() const { + return storage.empty(); + } + + private: + std::queue storage; + }; + + class JitBuilder : public JitModelBuilderInterface { + public: + JitBuilder(ModelComponentsBuilder& modelComponentsBuilder) : JitModelBuilderInterface(modelComponentsBuilder) { + {% for state in initialStates %}{ + StateType state; + {% for assignment in state %}state.{$assignment.variable} = {$assignment.value}; + {% endfor %}initialStates.push_back(state); + } + {% endfor %} + } + + virtual storm::models::sparse::Model>* build() override { + std::cout << "starting building process" << std::endl; + explore(initialStates); + std::cout << "finished building process with " << stateIds.size() << " states" << std::endl; + + std::cout << "building labeling" << std::endl; + label(); + std::cout << "finished building labeling" << std::endl; + + return this->modelComponentsBuilder.build(stateIds.size()); + } + + void label() { + uint64_t labelCount = 0; + {% for label in labels %}this->modelComponentsBuilder.registerLabel("{$label.name}", stateIds.size()); + ++labelCount; + {% endfor %} + this->modelComponentsBuilder.registerLabel("init", stateIds.size()); + this->modelComponentsBuilder.registerLabel("deadlock", stateIds.size()); + + for (auto const& stateEntry : stateIds) { + auto const& state = stateEntry.first; + {% for label in labels %}if ({$label.predicate}) { + this->modelComponentsBuilder.addLabel(stateEntry.second, {$loop.index} - 1); + } + {% endfor %} + } + + for (auto const& state : initialStates) { + auto stateIt = stateIds.find(state); + if (stateIt != stateIds.end()) { + this->modelComponentsBuilder.addLabel(stateIt->second, labelCount); + } + } + + for (auto const& stateId : deadlockStates) { + this->modelComponentsBuilder.addLabel(stateId, labelCount + 1); + } + } + + void explore(std::vector const& initialStates) { + for (auto const& state : initialStates) { + explore(state); + } + } + + void explore(StateType const& initialState) { + StateSet statesToExplore; + getOrAddIndex(initialState, statesToExplore); + + StateBehaviour behaviour; + while (!statesToExplore.empty()) { + StateType currentState = statesToExplore.get(); + IndexType currentIndex = getIndex(currentState); +#ifndef NDEBUG + std::cout << "Exploring state " << currentState << ", id " << currentIndex << std::endl; +#endif + + exploreNonSynchronizingEdges(currentState, currentIndex, behaviour, statesToExplore); + + this->addStateBehaviour(currentIndex, behaviour); + behaviour.clear(); + } + } + + void exploreNonSynchronizingEdges(StateType const& sourceState, IndexType const& currentIndex, StateBehaviour& behaviour, StateSet& statesToExplore) { + {% for edge in nonSynchronizingEdges %}if ({$edge.guard}) { + Choice& choice = behaviour.addChoice(); + {% for destination in edge.destinations %}{ + StateType targetState(sourceState); + {% for assignment in destination.nonTransientAssignments %}targetState.{$assignment.variable} = {$assignment.value}; + {% endfor %} + IndexType targetStateIndex = getOrAddIndex(targetState, statesToExplore); + choice.add(targetStateIndex, {$destination.value}); + } + {% endfor %} + } + {% endfor %} + } + + IndexType getOrAddIndex(StateType const& state, StateSet& statesToExplore) { + auto it = stateIds.find(state); + if (it != stateIds.end()) { + return it->second; + } else { + IndexType newIndex = static_cast(stateIds.size()); + stateIds.insert(std::make_pair(state, newIndex)); +#ifndef NDEBUG + std::cout << "inserting state " << state << std::endl; +#endif + statesToExplore.add(state); + return newIndex; + } + } + + IndexType getIndex(StateType const& state) const { + auto it = stateIds.find(state); + if (it != stateIds.end()) { + return it->second; + } else { + return stateIds.at(state); + } + } + + void addStateBehaviour(IndexType const& stateId, StateBehaviour& behaviour) { + if (behaviour.empty()) { + deadlockStates.push_back(stateId); + } + + JitModelBuilderInterface::addStateBehaviour(stateId, behaviour); + } + + static JitModelBuilderInterface* create(ModelComponentsBuilder& modelComponentsBuilder) { + return new JitBuilder(modelComponentsBuilder); + } + + private: + spp::sparse_hash_map stateIds; + std::vector initialStates; + std::vector deadlockStates; + }; + + BOOST_DLL_ALIAS(storm::builder::jit::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); + cpptempl::data_list labels = generateLabels(); + modelData["labels"] = cpptempl::make_data(labels); + 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"] = getQualifiedVariableName(automaton, this->locationVariables.at(automaton.getName())); + 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::generateLabels() { + cpptempl::data_list labels; + + // As in JANI we can use transient boolean variable assignments in locations to identify states, we need to + // create a list of boolean transient variables and the expressions that define them. + for (auto const& variable : model.getGlobalVariables().getTransientVariables()) { + if (variable->isBooleanVariable()) { + if (this->options.isBuildAllLabelsSet() || this->options.getLabelNames().find(variable->getName()) != this->options.getLabelNames().end()) { + cpptempl::data_map label; + label["name"] = variable->getName(); + label["predicate"] = expressionTranslator.translate(model.getLabelExpression(variable->asBooleanVariable(), locationVariables), storm::expressions::ToCppTranslationOptions("state.")); + labels.push_back(label); + } + } + } + + for (auto const& expression : this->options.getExpressionLabels()) { + cpptempl::data_map label; + label["name"] = expression.toString(); + label["predicate"] = expressionTranslator.translate(expression, storm::expressions::ToCppTranslationOptions("state.")); + labels.push_back(label); + } + + return labels; + } + + 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 variable.getExpressionVariable().getName(); + } + + template + std::string ExplicitJitJaniModelBuilder::getQualifiedVariableName(storm::jani::Automaton const& automaton, storm::expressions::Variable const& variable) const { + return 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(modelComponentsBuilder)); + } + + template + boost::filesystem::path ExplicitJitJaniModelBuilder::writeSourceToTemporaryFile(std::string const& source) { + boost::filesystem::path temporaryFile = boost::filesystem::unique_path("%%%%-%%%%-%%%%-%%%%.cpp"); + std::ofstream out(temporaryFile.native()); + out << source << std::endl; + out.close(); + return temporaryFile; + } + + 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 start = std::chrono::high_resolution_clock::now(); + auto sparseModel = builder->build(); + auto end = std::chrono::high_resolution_clock::now(); + std::cout << "Building model took " << std::chrono::duration_cast(end - start).count() << "ms." << std::endl; + + // (7) delete the shared library + boost::filesystem::remove(dynamicLibraryPath); + + // Return the constructed model. + return std::shared_ptr>(sparseModel); + } + + template class ExplicitJitJaniModelBuilder>; + template class ExplicitJitJaniModelBuilder>; + template class ExplicitJitJaniModelBuilder>; + + } + } +} diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.h b/src/builder/jit/ExplicitJitJaniModelBuilder.h new file mode 100644 index 000000000..4c182db48 --- /dev/null +++ b/src/builder/jit/ExplicitJitJaniModelBuilder.h @@ -0,0 +1,93 @@ +#pragma once + +#include + +#include +#include +#include + +#include "cpptempl.h" + +#include "src/storage/jani/Model.h" +#include "src/storage/expressions/ToCppVisitor.h" + +#include "src/builder/BuilderOptions.h" +#include "src/builder/jit/JitModelBuilderInterface.h" +#include "src/builder/jit/ModelComponentsBuilder.h" + +namespace storm { + namespace models { + namespace sparse { + template + class Model; + + template + class StandardRewardModel; + } + } + + namespace builder { + namespace jit { + + typedef uint32_t IndexType; + + template > + class ExplicitJitJaniModelBuilder { + public: + typedef JitModelBuilderInterface* (CreateFunctionType)(ModelComponentsBuilder& modelComponentsBuilder); + typedef boost::function ImportFunctionType; + + ExplicitJitJaniModelBuilder(storm::jani::Model const& model, storm::builder::BuilderOptions const& options = storm::builder::BuilderOptions()); + + 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 generateLabels(); + 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 getQualifiedVariableName(storm::jani::Automaton const& automaton, storm::expressions::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::builder::BuilderOptions options; + storm::jani::Model model; + std::map locationVariables; + + ModelComponentsBuilder modelComponentsBuilder; + typename ExplicitJitJaniModelBuilder::ImportFunctionType jitBuilderGetFunction; + std::unique_ptr> builder; + + std::unordered_map variableToName; + storm::expressions::ToCppVisitor expressionTranslator; + }; + + } + } +} diff --git a/src/builder/jit/JitModelBuilderInterface.cpp b/src/builder/jit/JitModelBuilderInterface.cpp index 49b9b4409..acb054c22 100644 --- a/src/builder/jit/JitModelBuilderInterface.cpp +++ b/src/builder/jit/JitModelBuilderInterface.cpp @@ -1,5 +1,7 @@ #include "src/builder/jit/JitModelBuilderInterface.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace builder { namespace jit { @@ -15,10 +17,14 @@ namespace storm { } template - void JitModelBuilderInterface::addStateBehaviour(StateBehaviour const& behaviour) { - modelComponentsBuilder.addStateBehaviour(behaviour); + void JitModelBuilderInterface::addStateBehaviour(IndexType const& stateId, StateBehaviour& behaviour) { + modelComponentsBuilder.addStateBehaviour(stateId, behaviour); } + template class JitModelBuilderInterface; + template class JitModelBuilderInterface; + template class JitModelBuilderInterface; + } } } diff --git a/src/builder/jit/ModelComponentBuilder.cpp b/src/builder/jit/ModelComponentBuilder.cpp deleted file mode 100644 index e4aabc04d..000000000 --- a/src/builder/jit/ModelComponentBuilder.cpp +++ /dev/null @@ -1,64 +0,0 @@ -#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/ModelComponentsBuilder.cpp b/src/builder/jit/ModelComponentsBuilder.cpp new file mode 100644 index 000000000..2a02a6a7e --- /dev/null +++ b/src/builder/jit/ModelComponentsBuilder.cpp @@ -0,0 +1,76 @@ +#include "src/builder/jit/ModelComponentsBuilder.h" + +#include "src/models/sparse/StateLabeling.h" +#include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/StandardRewardModel.h" + +#include "src/utility/macros.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)), currentRowGroup(0), currentRow(0), transitionMatrixBuilder(std::make_unique>(0, 0, 0, true, !isDeterministicModel)) { + // Intentionally left empty. + } + + template + ModelComponentsBuilder::~ModelComponentsBuilder() { + // Intentionally left empty. + } + + template + void ModelComponentsBuilder::addStateBehaviour(IndexType const& stateId, StateBehaviour& behaviour) { + // Compress the choices and reduce them depending on the model type. + behaviour.reduce(modelType); + + STORM_LOG_ASSERT(stateId == currentRowGroup, "Expected states in different order."); + + if (!isDeterministicModel) { + transitionMatrixBuilder->newRowGroup(currentRow); + } + for (auto const& choice : behaviour.getChoices()) { + // Add the elements to the transition matrix. + for (auto const& element : choice.getDistribution()) { + transitionMatrixBuilder->addNextValue(currentRow, element.getIndex(), element.getValue()); + } + + // Proceed to next row. + ++currentRow; + } + ++currentRowGroup; + } + + template + storm::models::sparse::Model>* ModelComponentsBuilder::build(IndexType const& stateCount) { + // Start by building the labeling object. + storm::models::sparse::StateLabeling stateLabeling(stateCount); + for (auto& label : labels) { + stateLabeling.addLabel(label.first, std::move(label.second)); + } + + if (modelType == storm::jani::ModelType::DTMC) { + return new storm::models::sparse::Dtmc>(this->transitionMatrixBuilder->build(), std::move(stateLabeling)); + } else { + return nullptr; + } + } + + template + void ModelComponentsBuilder::registerLabel(std::string const& name, IndexType const& stateCount) { + labels.emplace_back(name, storm::storage::BitVector(stateCount)); + } + + template + void ModelComponentsBuilder::addLabel(IndexType const& stateId, IndexType const& labelIndex) { + labels[labelIndex].second.set(stateId); + } + + template class ModelComponentsBuilder; + template class ModelComponentsBuilder; + template class ModelComponentsBuilder; + + } + } +} diff --git a/src/builder/jit/ModelComponentBuilder.h b/src/builder/jit/ModelComponentsBuilder.h similarity index 62% rename from src/builder/jit/ModelComponentBuilder.h rename to src/builder/jit/ModelComponentsBuilder.h index 2929b6146..6b399ff94 100644 --- a/src/builder/jit/ModelComponentBuilder.h +++ b/src/builder/jit/ModelComponentsBuilder.h @@ -10,6 +10,8 @@ namespace storm { namespace storage { template class SparseMatrixBuilder; + + class BitVector; } namespace models { @@ -19,6 +21,8 @@ namespace storm { template class Model; + + class StateLabeling; } } @@ -29,16 +33,24 @@ namespace storm { class ModelComponentsBuilder { public: ModelComponentsBuilder(storm::jani::ModelType const& modelType); + ~ModelComponentsBuilder(); - void addStateBehaviour(StateBehaviour const& behaviour); + void addStateBehaviour(IndexType const& stateIndex, StateBehaviour& behaviour); - storm::models::sparse::Model>* build(); + storm::models::sparse::Model>* build(IndexType const& stateCount); + + void registerLabel(std::string const& name, IndexType const& stateCount); + void addLabel(IndexType const& stateId, IndexType const& labelIndex); private: storm::jani::ModelType modelType; bool isDeterministicModel; bool isDiscreteTimeModel; + + IndexType currentRowGroup; + IndexType currentRow; std::unique_ptr> transitionMatrixBuilder; + std::vector> labels; }; } diff --git a/src/builder/jit/StateBehaviour.cpp b/src/builder/jit/StateBehaviour.cpp index 93a595fa2..7409abb1f 100644 --- a/src/builder/jit/StateBehaviour.cpp +++ b/src/builder/jit/StateBehaviour.cpp @@ -1,12 +1,20 @@ #include "src/builder/jit/StateBehaviour.h" +#include "src/adapters/CarlAdapter.h" + namespace storm { namespace builder { namespace jit { + template + StateBehaviour::StateBehaviour() : compressed(true) { + // Intentionally left empty. + } + template void StateBehaviour::addChoice(Choice&& choice) { choices.emplace_back(std::move(choice)); + } template @@ -15,11 +23,59 @@ namespace storm { return choices.back(); } + template + typename StateBehaviour::ContainerType const& StateBehaviour::getChoices() const { + return choices; + } + + template + void StateBehaviour::reduce(storm::jani::ModelType const& modelType) { + if (choices.size() > 1) { + if (modelType == storm::jani::ModelType::DTMC || modelType == storm::jani::ModelType::CTMC) { + std::size_t totalCount = choices.size(); + for (auto it = ++choices.begin(), ite = choices.end(); it != ite; ++it) { + choices.front().add(std::move(*it)); + } + choices.resize(1); + choices.front().compress(); + + if (modelType == storm::jani::ModelType::DTMC) { + choices.front().divideDistribution(static_cast(totalCount)); + } + } + } + } + + template + void StateBehaviour::compress() { + if (!compressed) { + for (auto& choice : choices) { + choice.compress(); + } + compressed = true; + } + } + + template + bool StateBehaviour::empty() const { + return choices.empty(); + } + + template + std::size_t StateBehaviour::size() const { + return choices.size(); + } + template void StateBehaviour::clear() { choices.clear(); + compressed = true; } + template class StateBehaviour; + template class StateBehaviour; + template class StateBehaviour; + } } } diff --git a/src/builder/jit/StateBehaviour.h b/src/builder/jit/StateBehaviour.h index 8b515b40e..1a56eeda7 100644 --- a/src/builder/jit/StateBehaviour.h +++ b/src/builder/jit/StateBehaviour.h @@ -1,5 +1,6 @@ #pragma once +#include "src/storage/jani/ModelType.h" #include "src/builder/jit/Choice.h" namespace storm { @@ -11,13 +12,23 @@ namespace storm { public: typedef std::vector> ContainerType; + StateBehaviour(); + void addChoice(Choice&& choice); Choice& addChoice(); + ContainerType const& getChoices() const; + + void reduce(storm::jani::ModelType const& modelType); + void compress(); + + bool empty() const; + std::size_t size() const; void clear(); private: ContainerType choices; + bool compressed; }; } diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp index cf15f0a3f..f8bdde9fd 100644 --- a/src/generator/NextStateGenerator.cpp +++ b/src/generator/NextStateGenerator.cpp @@ -14,183 +14,7 @@ namespace storm { namespace generator { - - LabelOrExpression::LabelOrExpression(storm::expressions::Expression const& expression) : labelOrExpression(expression) { - // Intentionally left empty. - } - - LabelOrExpression::LabelOrExpression(std::string const& label) : labelOrExpression(label) { - // Intentionally left empty. - } - - bool LabelOrExpression::isLabel() const { - return labelOrExpression.which() == 0; - } - - std::string const& LabelOrExpression::getLabel() const { - return boost::get(labelOrExpression); - } - - bool LabelOrExpression::isExpression() const { - return labelOrExpression.which() == 1; - } - - storm::expressions::Expression const& LabelOrExpression::getExpression() const { - return boost::get(labelOrExpression); - } - - NextStateGeneratorOptions::NextStateGeneratorOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false) { - // Intentionally left empty. - } - - NextStateGeneratorOptions::NextStateGeneratorOptions(storm::logic::Formula const& formula) : NextStateGeneratorOptions() { - this->preserveFormula(formula); - this->setTerminalStatesFromFormula(formula); - } - - NextStateGeneratorOptions::NextStateGeneratorOptions(std::vector> const& formulas) : NextStateGeneratorOptions() { - if (!formulas.empty()) { - for (auto const& formula : formulas) { - this->preserveFormula(*formula); - } - if (formulas.size() == 1) { - this->setTerminalStatesFromFormula(*formulas.front()); - } - } - } - - void NextStateGeneratorOptions::preserveFormula(storm::logic::Formula const& formula) { - // If we already had terminal states, we need to erase them. - if (hasTerminalStates()) { - clearTerminalStates(); - } - - // Determine the reward models we need to build. - std::set referencedRewardModels = formula.getReferencedRewardModels(); - for (auto const& rewardModelName : referencedRewardModels) { - rewardModelNames.push_back(rewardModelName); - } - - // Extract all the labels used in the formula. - std::vector> atomicLabelFormulas = formula.getAtomicLabelFormulas(); - for (auto const& formula : atomicLabelFormulas) { - addLabel(formula->getLabel()); - } - - // Extract all the expressions used in the formula. - std::vector> atomicExpressionFormulas = formula.getAtomicExpressionFormulas(); - for (auto const& formula : atomicExpressionFormulas) { - addLabel(formula->getExpression()); - } - } - - void NextStateGeneratorOptions::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { - if (formula.isAtomicExpressionFormula()) { - addTerminalExpression(formula.asAtomicExpressionFormula().getExpression(), true); - } else if (formula.isAtomicLabelFormula()) { - addTerminalLabel(formula.asAtomicLabelFormula().getLabel(), true); - } else if (formula.isEventuallyFormula()) { - storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula(); - if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) { - this->setTerminalStatesFromFormula(sub); - } - } else if (formula.isUntilFormula()) { - storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula(); - if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { - this->setTerminalStatesFromFormula(right); - } - storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula(); - if (left.isAtomicExpressionFormula()) { - addTerminalExpression(left.asAtomicExpressionFormula().getExpression(), false); - } else if (left.isAtomicLabelFormula()) { - addTerminalLabel(left.asAtomicLabelFormula().getLabel(), false); - } - } else if (formula.isProbabilityOperatorFormula()) { - storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula(); - if (sub.isEventuallyFormula() || sub.isUntilFormula()) { - this->setTerminalStatesFromFormula(sub); - } - } - } - - std::vector const& NextStateGeneratorOptions::getRewardModelNames() const { - return rewardModelNames; - } - - std::set const& NextStateGeneratorOptions::getLabelNames() const { - return labelNames; - } - - std::vector const& NextStateGeneratorOptions::getExpressionLabels() const { - return expressionLabels; - } - - std::vector> const& NextStateGeneratorOptions::getTerminalStates() const { - return terminalStates; - } - - bool NextStateGeneratorOptions::hasTerminalStates() const { - return !terminalStates.empty(); - } - - void NextStateGeneratorOptions::clearTerminalStates() { - terminalStates.clear(); - } - - bool NextStateGeneratorOptions::isBuildChoiceLabelsSet() const { - return buildChoiceLabels; - } - - bool NextStateGeneratorOptions::isBuildAllRewardModelsSet() const { - return buildAllRewardModels; - } - - bool NextStateGeneratorOptions::isBuildAllLabelsSet() const { - return buildAllLabels; - } - - NextStateGeneratorOptions& NextStateGeneratorOptions::setBuildAllRewardModels() { - buildAllRewardModels = true; - return *this; - } - - NextStateGeneratorOptions& NextStateGeneratorOptions::addRewardModel(std::string const& rewardModelName) { - STORM_LOG_THROW(!buildAllRewardModels, storm::exceptions::InvalidSettingsException, "Cannot add reward model, because all reward models are built anyway."); - rewardModelNames.emplace_back(rewardModelName); - return *this; - } - - NextStateGeneratorOptions& NextStateGeneratorOptions::setBuildAllLabels() { - buildAllLabels = true; - return *this; - } - - NextStateGeneratorOptions& NextStateGeneratorOptions::addLabel(storm::expressions::Expression const& expression) { - expressionLabels.emplace_back(expression); - return *this; - } - - NextStateGeneratorOptions& NextStateGeneratorOptions::addLabel(std::string const& labelName) { - STORM_LOG_THROW(!buildAllLabels, storm::exceptions::InvalidSettingsException, "Cannot add label, because all labels are built anyway."); - labelNames.insert(labelName); - return *this; - } - - NextStateGeneratorOptions& NextStateGeneratorOptions::addTerminalExpression(storm::expressions::Expression const& expression, bool value) { - terminalStates.push_back(std::make_pair(LabelOrExpression(expression), value)); - return *this; - } - - NextStateGeneratorOptions& NextStateGeneratorOptions::addTerminalLabel(std::string const& label, bool value) { - terminalStates.push_back(std::make_pair(LabelOrExpression(label), value)); - return *this; - } - - NextStateGeneratorOptions& NextStateGeneratorOptions::setBuildChoiceLabels(bool newValue) { - buildChoiceLabels = newValue; - return *this; - } - + RewardModelInformation::RewardModelInformation(std::string const& name, bool stateRewards, bool stateActionRewards, bool transitionRewards) : name(name), stateRewards(stateRewards), stateActionRewards(stateActionRewards), transitionRewards(transitionRewards) { // Intentionally left empty. } diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h index b9b7bfe23..ec3ee8763 100644 --- a/src/generator/NextStateGenerator.h +++ b/src/generator/NextStateGenerator.h @@ -10,6 +10,8 @@ #include "src/storage/BitVectorHashMap.h" #include "src/storage/expressions/ExpressionEvaluator.h" +#include "src/builder/BuilderOptions.h" + #include "src/generator/VariableInformation.h" #include "src/generator/CompressedState.h" #include "src/generator/StateBehavior.h" @@ -17,120 +19,8 @@ #include "src/utility/ConstantsComparator.h" namespace storm { - namespace expressions { - class Expression; - class ExpressionManager; - } - - namespace models { - namespace sparse { - class StateLabeling; - } - } - - namespace logic { - class Formula; - } - namespace generator { - class LabelOrExpression { - public: - LabelOrExpression(storm::expressions::Expression const& expression); - LabelOrExpression(std::string const& label); - - bool isLabel() const; - std::string const& getLabel() const; - bool isExpression() const; - storm::expressions::Expression const& getExpression() const; - - private: - /// An optional label for the expression. - boost::variant labelOrExpression; - }; - - class NextStateGeneratorOptions { - public: - /*! - * Creates an object representing the default options. - */ - NextStateGeneratorOptions(bool buildAllRewardModels = false, bool buildAllLabels = false); - - /*! - * Creates an object representing the suggested building options assuming that the given formula is the - * only one to check. Additional formulas may be preserved by calling preserveFormula. - * - * @param formula The formula based on which to choose the building options. - */ - NextStateGeneratorOptions(storm::logic::Formula const& formula); - - /*! - * Creates an object representing the suggested building options assuming that the given formulas are - * the only ones to check. Additional formulas may be preserved by calling preserveFormula. - * - * @param formula Thes formula based on which to choose the building options. - */ - NextStateGeneratorOptions(std::vector> const& formulas); - - /*! - * Changes the options in a way that ensures that the given formula can be checked on the model once it - * has been built. - * - * @param formula The formula that is to be ''preserved''. - */ - void preserveFormula(storm::logic::Formula const& formula); - - /*! - * Analyzes the given formula and sets an expression for the states states of the model that can be - * treated as terminal states. Note that this may interfere with checking properties different than the - * one provided. - * - * @param formula The formula used to (possibly) derive an expression for the terminal states of the - * model. - */ - void setTerminalStatesFromFormula(storm::logic::Formula const& formula); - - std::vector const& getRewardModelNames() const; - std::set const& getLabelNames() const; - std::vector const& getExpressionLabels() const; - std::vector> const& getTerminalStates() const; - bool hasTerminalStates() const; - void clearTerminalStates(); - bool isBuildChoiceLabelsSet() const; - bool isBuildAllRewardModelsSet() const; - bool isBuildAllLabelsSet() const; - - NextStateGeneratorOptions& setBuildAllRewardModels(); - NextStateGeneratorOptions& addRewardModel(std::string const& rewardModelName); - NextStateGeneratorOptions& setBuildAllLabels(); - NextStateGeneratorOptions& addLabel(storm::expressions::Expression const& expression); - NextStateGeneratorOptions& addLabel(std::string const& labelName); - NextStateGeneratorOptions& addTerminalExpression(storm::expressions::Expression const& expression, bool value); - NextStateGeneratorOptions& addTerminalLabel(std::string const& label, bool value); - NextStateGeneratorOptions& setBuildChoiceLabels(bool newValue); - - private: - /// A flag that indicates whether all reward models are to be built. In this case, the reward model names are - /// to be ignored. - bool buildAllRewardModels; - - /// The names of the reward models to generate. - std::vector rewardModelNames; - - /// A flag that indicates whether all labels are to be built. In this case, the label names are to be ignored. - bool buildAllLabels; - - /// A set of labels to build. - std::set labelNames; - - /// The expression that are to be used for creating the state labeling. - std::vector expressionLabels; - - /// If one of these labels/expressions evaluates to the given bool, the state generator can abort the exploration. - std::vector> terminalStates; - - /// A flag indicating whether or not to build choice labels. - bool buildChoiceLabels; - }; + typedef storm::builder::BuilderOptions NextStateGeneratorOptions; enum class ModelType { DTMC, diff --git a/src/utility/storm.h b/src/utility/storm.h index 705a58034..77723821b 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -1,4 +1,3 @@ - #ifndef STORM_H #define STORM_H @@ -109,7 +108,7 @@ namespace storm { template std::shared_ptr> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { - storm::generator::NextStateGeneratorOptions options(formulas); + storm::builder::BuilderOptions options(formulas); // Generate command labels if we are going to build a counterexample later. if (storm::settings::getModule().isMinimalCommandSetGenerationSet()) { @@ -118,7 +117,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::jit::ExplicitJitJaniModelBuilder builder(model.asJaniModel()); + storm::builder::jit::ExplicitJitJaniModelBuilder builder(model.asJaniModel(), options); return builder.build(); } else { std::shared_ptr> generator;