Browse Source
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)
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:tempestpy_adaptions5729c1c8ca[formerly890198a907] Former-commit-id:df2528638d
dehnert
8 years ago
18 changed files with 1335 additions and 382 deletions
-
188src/builder/BuilderOptions.cpp
-
39src/builder/jit/Choice.cpp
-
10src/builder/jit/Choice.h
-
95src/builder/jit/Distribution.cpp
-
19src/builder/jit/Distribution.h
-
21src/builder/jit/DistributionEntry.cpp
-
4src/builder/jit/DistributionEntry.h
-
716src/builder/jit/ExplicitJitJaniModelBuilder.cpp
-
93src/builder/jit/ExplicitJitJaniModelBuilder.h
-
10src/builder/jit/JitModelBuilderInterface.cpp
-
64src/builder/jit/ModelComponentBuilder.cpp
-
76src/builder/jit/ModelComponentsBuilder.cpp
-
16src/builder/jit/ModelComponentsBuilder.h
-
56src/builder/jit/StateBehaviour.cpp
-
11src/builder/jit/StateBehaviour.h
-
178src/generator/NextStateGenerator.cpp
-
116src/generator/NextStateGenerator.h
-
5src/utility/storm.h
@ -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<std::string>(labelOrExpression); |
|||
} |
|||
|
|||
bool LabelOrExpression::isExpression() const { |
|||
return labelOrExpression.which() == 1; |
|||
} |
|||
|
|||
storm::expressions::Expression const& LabelOrExpression::getExpression() const { |
|||
return boost::get<storm::expressions::Expression>(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<std::shared_ptr<storm::logic::Formula const>> 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<std::string> referencedRewardModels = formula.getReferencedRewardModels(); |
|||
for (auto const& rewardModelName : referencedRewardModels) { |
|||
rewardModelNames.push_back(rewardModelName); |
|||
} |
|||
|
|||
// Extract all the labels used in the formula.
|
|||
std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabelFormulas = formula.getAtomicLabelFormulas(); |
|||
for (auto const& formula : atomicLabelFormulas) { |
|||
addLabel(formula->getLabel()); |
|||
} |
|||
|
|||
// Extract all the expressions used in the formula.
|
|||
std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>> 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<std::string> const& BuilderOptions::getRewardModelNames() const { |
|||
return rewardModelNames; |
|||
} |
|||
|
|||
std::set<std::string> const& BuilderOptions::getLabelNames() const { |
|||
return labelNames; |
|||
} |
|||
|
|||
std::vector<storm::expressions::Expression> const& BuilderOptions::getExpressionLabels() const { |
|||
return expressionLabels; |
|||
} |
|||
|
|||
std::vector<std::pair<LabelOrExpression, bool>> 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; |
|||
} |
|||
|
|||
} |
|||
} |
|||
@ -1,19 +1,58 @@ |
|||
#include "src/builder/jit/Choice.h"
|
|||
|
|||
#include "src/adapters/CarlAdapter.h"
|
|||
|
|||
namespace storm { |
|||
namespace builder { |
|||
namespace jit { |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
Choice<IndexType, ValueType>::Choice() : compressed(true) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
void Choice<IndexType, ValueType>::add(DistributionEntry<IndexType, ValueType> const& entry) { |
|||
distribution.add(entry); |
|||
} |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
void Choice<IndexType, ValueType>::add(IndexType const& index, ValueType const& value) { |
|||
distribution.add(index, value); |
|||
} |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
void Choice<IndexType, ValueType>::add(Choice<IndexType, ValueType>&& choice) { |
|||
distribution.add(std::move(choice.getDistribution())); |
|||
} |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
Distribution<IndexType, ValueType> const& Choice<IndexType, ValueType>::getDistribution() const { |
|||
return distribution; |
|||
} |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
void Choice<IndexType, ValueType>::divideDistribution(ValueType const& value) { |
|||
distribution.divide(value); |
|||
} |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
void Choice<IndexType, ValueType>::compress() { |
|||
if (!compressed) { |
|||
distribution.compress(); |
|||
compressed = true; |
|||
} |
|||
} |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
Distribution<IndexType, ValueType>& Choice<IndexType, ValueType>::getDistribution() { |
|||
return distribution; |
|||
} |
|||
|
|||
template class Choice<uint32_t, double>; |
|||
template class Choice<uint32_t, storm::RationalNumber>; |
|||
template class Choice<uint32_t, storm::RationalFunction>; |
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -1,43 +1,96 @@ |
|||
#include "src/builder/jit/Distribution.h"
|
|||
|
|||
#include "src/adapters/CarlAdapter.h"
|
|||
|
|||
namespace storm { |
|||
namespace builder { |
|||
namespace jit { |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
Distribution<IndexType, ValueType>::Distribution() : compressed(true) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
void Distribution<IndexType, ValueType>::add(DistributionEntry<IndexType, ValueType> const& entry) { |
|||
storage.push_back(entry); |
|||
compressed = storage.back().getIndex() < entry.getIndex(); |
|||
} |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
void Distribution<IndexType, ValueType>::add(IndexType const& index, ValueType const& value) { |
|||
storage.emplace_back(index, value); |
|||
compressed = storage.back().getIndex() < index; |
|||
} |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
void Distribution<IndexType, ValueType>::add(Distribution&& distribution) { |
|||
storage.insert(storage.end(), std::make_move_iterator(distribution.begin()), std::make_move_iterator(distribution.end())); |
|||
compressed = false; |
|||
} |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
void Distribution<IndexType, ValueType>::compress() { |
|||
std::sort(storage.begin(), storage.end(), |
|||
[] (DistributionEntry<IndexType, ValueType> const& a, DistributionEntry<IndexType, ValueType> 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<IndexType, ValueType> const& a, DistributionEntry<IndexType, ValueType> 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 <typename IndexType, typename ValueType> |
|||
void Distribution<IndexType, ValueType>::divide(ValueType const& value) { |
|||
for (auto& entry : storage) { |
|||
entry.divide(value); |
|||
} |
|||
} |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
typename Distribution<IndexType, ValueType>::ContainerType::iterator Distribution<IndexType, ValueType>::begin() { |
|||
return storage.begin(); |
|||
} |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
typename Distribution<IndexType, ValueType>::ContainerType::const_iterator Distribution<IndexType, ValueType>::begin() const { |
|||
return storage.begin(); |
|||
} |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
typename Distribution<IndexType, ValueType>::ContainerType::iterator Distribution<IndexType, ValueType>::end() { |
|||
return storage.end(); |
|||
} |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
typename Distribution<IndexType, ValueType>::ContainerType::const_iterator Distribution<IndexType, ValueType>::end() const { |
|||
return storage.end(); |
|||
} |
|||
|
|||
template class Distribution<uint32_t, double>; |
|||
template class Distribution<uint32_t, storm::RationalNumber>; |
|||
template class Distribution<uint32_t, storm::RationalFunction>; |
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,716 @@ |
|||
#include "src/builder/jit/ExplicitJitJaniModelBuilder.h"
|
|||
|
|||
#include <iostream>
|
|||
#include <cstdio>
|
|||
#include <chrono>
|
|||
|
|||
#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 <typename ValueType, typename RewardModelType> |
|||
ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::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 <typename ValueType, typename RewardModelType> |
|||
std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::createSourceCode() { |
|||
std::string sourceTemplate = R"( |
|||
|
|||
#define NDEBUG
|
|||
|
|||
#include <cstdint>
|
|||
#include <iostream>
|
|||
#include <vector>
|
|||
#include <queue>
|
|||
#include <cmath>
|
|||
#include <unordered_map>
|
|||
#include <boost/dll/alias.hpp>
|
|||
|
|||
#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<storm::builder::jit::StateType> { |
|||
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<StateType> storage; |
|||
}; |
|||
|
|||
class JitBuilder : public JitModelBuilderInterface<IndexType, ValueType> { |
|||
public: |
|||
JitBuilder(ModelComponentsBuilder<IndexType, ValueType>& 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<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>* 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<StateType> const& initialStates) { |
|||
for (auto const& state : initialStates) { |
|||
explore(state); |
|||
} |
|||
} |
|||
|
|||
void explore(StateType const& initialState) { |
|||
StateSet statesToExplore; |
|||
getOrAddIndex(initialState, statesToExplore); |
|||
|
|||
StateBehaviour<IndexType, ValueType> 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<IndexType, ValueType>& behaviour, StateSet& statesToExplore) { |
|||
{% for edge in nonSynchronizingEdges %}if ({$edge.guard}) { |
|||
Choice<IndexType, ValueType>& 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<IndexType>(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<IndexType, ValueType>& behaviour) { |
|||
if (behaviour.empty()) { |
|||
deadlockStates.push_back(stateId); |
|||
} |
|||
|
|||
JitModelBuilderInterface<IndexType, ValueType>::addStateBehaviour(stateId, behaviour); |
|||
} |
|||
|
|||
static JitModelBuilderInterface<IndexType, ValueType>* create(ModelComponentsBuilder<IndexType, ValueType>& modelComponentsBuilder) { |
|||
return new JitBuilder(modelComponentsBuilder); |
|||
} |
|||
|
|||
private: |
|||
spp::sparse_hash_map<StateType, IndexType> stateIds; |
|||
std::vector<StateType> initialStates; |
|||
std::vector<IndexType> 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 <typename ValueType, typename RewardModelType> |
|||
cpptempl::data_list ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateInitialStates() { |
|||
cpptempl::data_list initialStates; |
|||
|
|||
// Prepare an SMT solver to enumerate all initial states.
|
|||
storm::utility::solver::SmtSolverFactory factory; |
|||
std::unique_ptr<storm::solver::SmtSolver> solver = factory.create(model.getExpressionManager()); |
|||
|
|||
std::vector<storm::expressions::Expression> 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<storm::solver::SmtSolver::ModelReference> 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<std::set<uint64_t>::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 <typename ValueType, typename RewardModelType> |
|||
cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::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<uint64_t>(variable.getUpperBound().evaluateAsInt() - variable.getLowerBound().evaluateAsInt() + 1); |
|||
uint64_t numberOfBits = static_cast<uint64_t>(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<uint64_t>(variable.getUpperBound().evaluateAsInt() - variable.getLowerBound().evaluateAsInt()); |
|||
uint64_t numberOfBits = static_cast<uint64_t>(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<uint64_t>(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 <typename ValueType, typename RewardModelType> |
|||
cpptempl::data_list ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::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 <typename ValueType, typename RewardModelType> |
|||
cpptempl::data_list ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::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 <typename ValueType, typename RewardModelType> |
|||
cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::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 <typename ValueType, typename RewardModelType> |
|||
cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::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 <typename ValueType, typename RewardModelType> |
|||
template <typename ValueTypePrime> |
|||
cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::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 <typename ValueType, typename RewardModelType> |
|||
cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::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 <typename ValueType, typename RewardModelType> |
|||
cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::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 <typename ValueType, typename RewardModelType> |
|||
std::string const& ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::getVariableName(storm::expressions::Variable const& variable) const { |
|||
return variableToName.at(variable); |
|||
} |
|||
|
|||
template <typename ValueType, typename RewardModelType> |
|||
std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::getQualifiedVariableName(storm::jani::Variable const& variable) const { |
|||
return variable.getName(); |
|||
} |
|||
|
|||
template <typename ValueType, typename RewardModelType> |
|||
std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::getQualifiedVariableName(storm::jani::Automaton const& automaton, storm::jani::Variable const& variable) const { |
|||
return variable.getExpressionVariable().getName(); |
|||
} |
|||
|
|||
template <typename ValueType, typename RewardModelType> |
|||
std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::getQualifiedVariableName(storm::jani::Automaton const& automaton, storm::expressions::Variable const& variable) const { |
|||
return variable.getName(); |
|||
} |
|||
|
|||
template <typename ValueType, typename RewardModelType> |
|||
std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::getLocationVariableName(storm::jani::Automaton const& automaton) const { |
|||
return automaton.getName() + "_location"; |
|||
} |
|||
|
|||
template <typename ValueType, typename RewardModelType> |
|||
std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::asString(bool value) const { |
|||
std::stringstream out; |
|||
out << std::boolalpha << value; |
|||
return out.str(); |
|||
} |
|||
|
|||
template <typename ValueType, typename RewardModelType> |
|||
template <typename ValueTypePrime> |
|||
std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::asString(ValueTypePrime value) const { |
|||
return std::to_string(value); |
|||
} |
|||
|
|||
template <typename ValueType, typename RewardModelType> |
|||
boost::optional<std::string> ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::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<FILE> 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<std::chrono::milliseconds>(end - start).count() << "ms" << std::endl; |
|||
|
|||
if (WEXITSTATUS(result) == 0) { |
|||
return boost::none; |
|||
} else { |
|||
return "Executing command failed. Got response: " + output.str(); |
|||
} |
|||
} |
|||
|
|||
template <typename ValueType, typename RewardModelType> |
|||
void ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::createBuilder(boost::filesystem::path const& dynamicLibraryPath) { |
|||
jitBuilderGetFunction = boost::dll::import_alias<typename ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::CreateFunctionType>(dynamicLibraryPath, "create_builder"); |
|||
builder = std::unique_ptr<JitModelBuilderInterface<IndexType, ValueType>>(jitBuilderGetFunction(modelComponentsBuilder)); |
|||
} |
|||
|
|||
template <typename ValueType, typename RewardModelType> |
|||
boost::filesystem::path ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::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 <typename ValueType, typename RewardModelType> |
|||
boost::filesystem::path ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::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<std::string> 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 <typename ValueType, typename RewardModelType> |
|||
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::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<std::chrono::milliseconds>(end - start).count() << "ms." << std::endl; |
|||
|
|||
// (7) delete the shared library
|
|||
boost::filesystem::remove(dynamicLibraryPath); |
|||
|
|||
// Return the constructed model.
|
|||
return std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>>(sparseModel); |
|||
} |
|||
|
|||
template class ExplicitJitJaniModelBuilder<double, storm::models::sparse::StandardRewardModel<double>>; |
|||
template class ExplicitJitJaniModelBuilder<storm::RationalNumber, storm::models::sparse::StandardRewardModel<storm::RationalNumber>>; |
|||
template class ExplicitJitJaniModelBuilder<storm::RationalFunction, storm::models::sparse::StandardRewardModel<storm::RationalFunction>>; |
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,93 @@ |
|||
#pragma once |
|||
|
|||
#include <memory> |
|||
|
|||
#include <boost/filesystem.hpp> |
|||
#include <boost/dll/import.hpp> |
|||
#include <boost/function.hpp> |
|||
|
|||
#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 <typename ValueType, typename RewardModelType> |
|||
class Model; |
|||
|
|||
template <typename ValueType> |
|||
class StandardRewardModel; |
|||
} |
|||
} |
|||
|
|||
namespace builder { |
|||
namespace jit { |
|||
|
|||
typedef uint32_t IndexType; |
|||
|
|||
template <typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>> |
|||
class ExplicitJitJaniModelBuilder { |
|||
public: |
|||
typedef JitModelBuilderInterface<IndexType, ValueType>* (CreateFunctionType)(ModelComponentsBuilder<IndexType, ValueType>& modelComponentsBuilder); |
|||
typedef boost::function<CreateFunctionType> ImportFunctionType; |
|||
|
|||
ExplicitJitJaniModelBuilder(storm::jani::Model const& model, storm::builder::BuilderOptions const& options = storm::builder::BuilderOptions()); |
|||
|
|||
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> 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<std::string> 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 <typename ValueTypePrime> |
|||
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 <typename ValueTypePrime> |
|||
std::string asString(ValueTypePrime value) const; |
|||
|
|||
storm::builder::BuilderOptions options; |
|||
storm::jani::Model model; |
|||
std::map<std::string, storm::expressions::Variable> locationVariables; |
|||
|
|||
ModelComponentsBuilder<IndexType, ValueType> modelComponentsBuilder; |
|||
typename ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::ImportFunctionType jitBuilderGetFunction; |
|||
std::unique_ptr<JitModelBuilderInterface<IndexType, ValueType>> builder; |
|||
|
|||
std::unordered_map<storm::expressions::Variable, std::string> variableToName; |
|||
storm::expressions::ToCppVisitor expressionTranslator; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -1,64 +0,0 @@ |
|||
#include "src/builder/jit/ModelComponentBuilder.h"
|
|||
|
|||
#include "src/storage/SparseMatrix.h"
|
|||
|
|||
namespace storm { |
|||
namespace builder { |
|||
namespace jit { |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
ModelComponentsBuilder<IndexType, ValueType>::ModelComponentsBuilder(storm::jani::ModelType const& modelType) : modelType(modelType), isDeterministicModel(storm::jani::isDeterministicModel(modelType)), isDiscreteTimeModel(storm::jani::isDiscreteTimeModel(modelType)), transitionMatrixBuilder(std::make_unique<storm::storage::SparseMatrixBuilder<ValueType>>(0, 0, 0, true, !isDeterministicModel)) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
void ModelComponentsBuilder<IndexType, ValueType>::addStateBehaviour(StateBehaviour<IndexType, ValueType> 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 <typename IndexType, typename ValueType> |
|||
storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>* ModelComponentsBuilder<IndexType, ValueType>::build() { |
|||
// FIXME
|
|||
return nullptr; |
|||
} |
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -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 <typename IndexType, typename ValueType> |
|||
ModelComponentsBuilder<IndexType, ValueType>::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<storm::storage::SparseMatrixBuilder<ValueType>>(0, 0, 0, true, !isDeterministicModel)) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
ModelComponentsBuilder<IndexType, ValueType>::~ModelComponentsBuilder() { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
void ModelComponentsBuilder<IndexType, ValueType>::addStateBehaviour(IndexType const& stateId, StateBehaviour<IndexType, ValueType>& 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 <typename IndexType, typename ValueType> |
|||
storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>* ModelComponentsBuilder<IndexType, ValueType>::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<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>(this->transitionMatrixBuilder->build(), std::move(stateLabeling)); |
|||
} else { |
|||
return nullptr; |
|||
} |
|||
} |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
void ModelComponentsBuilder<IndexType, ValueType>::registerLabel(std::string const& name, IndexType const& stateCount) { |
|||
labels.emplace_back(name, storm::storage::BitVector(stateCount)); |
|||
} |
|||
|
|||
template <typename IndexType, typename ValueType> |
|||
void ModelComponentsBuilder<IndexType, ValueType>::addLabel(IndexType const& stateId, IndexType const& labelIndex) { |
|||
labels[labelIndex].second.set(stateId); |
|||
} |
|||
|
|||
template class ModelComponentsBuilder<uint32_t, double>; |
|||
template class ModelComponentsBuilder<uint32_t, storm::RationalNumber>; |
|||
template class ModelComponentsBuilder<uint32_t, storm::RationalFunction>; |
|||
|
|||
} |
|||
} |
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue