From 02ca60282d2f250fdcd9ac74b93bce4bfc12ea37 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 26 Oct 2016 17:30:57 +0200 Subject: [PATCH] forgotten files Former-commit-id: 3d9bce824d8f8c1d57f93cc07cf22c1811e0f02a [formerly a347808794acd0edcb47d480ea85e27453397af0] Former-commit-id: a11fa0697206ffbe1faad2b91824ab376c92c0e4 --- src/builder/BuilderOptions.h | 129 +++++++++++++++++++++ src/builder/jit/JitModelBuilderInterface.h | 39 +++++++ 2 files changed, 168 insertions(+) create mode 100644 src/builder/BuilderOptions.h create mode 100644 src/builder/jit/JitModelBuilderInterface.h diff --git a/src/builder/BuilderOptions.h b/src/builder/BuilderOptions.h new file mode 100644 index 000000000..7a7dc4267 --- /dev/null +++ b/src/builder/BuilderOptions.h @@ -0,0 +1,129 @@ +#pragma once + +#include +#include +#include + +#include +#include + +#include "src/storage/expressions/Expression.h" + +namespace storm { + namespace expressions { + class ExpressionManager; + } + + namespace models { + namespace sparse { + class StateLabeling; + } + } + + namespace logic { + class Formula; + } + + namespace builder { + + 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 BuilderOptions { + public: + /*! + * Creates an object representing the default options. + */ + BuilderOptions(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. + */ + BuilderOptions(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. + */ + BuilderOptions(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; + + BuilderOptions& setBuildAllRewardModels(); + BuilderOptions& addRewardModel(std::string const& rewardModelName); + BuilderOptions& setBuildAllLabels(); + BuilderOptions& addLabel(storm::expressions::Expression const& expression); + BuilderOptions& addLabel(std::string const& labelName); + BuilderOptions& addTerminalExpression(storm::expressions::Expression const& expression, bool value); + BuilderOptions& addTerminalLabel(std::string const& label, bool value); + BuilderOptions& 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 builder can abort the exploration. + std::vector> terminalStates; + + /// A flag indicating whether or not to build choice labels. + bool buildChoiceLabels; + }; + + } +} diff --git a/src/builder/jit/JitModelBuilderInterface.h b/src/builder/jit/JitModelBuilderInterface.h new file mode 100644 index 000000000..e170e6355 --- /dev/null +++ b/src/builder/jit/JitModelBuilderInterface.h @@ -0,0 +1,39 @@ +#pragma once + +#include + +#include "src/builder/jit/ModelComponentsBuilder.h" + +namespace storm { + namespace models { + namespace sparse { + template + class StandardRewardModel; + + template + class Model; + } + } + + namespace builder { + namespace jit { + + template + class JitModelBuilderInterface { + public: + JitModelBuilderInterface(ModelComponentsBuilder& modelComponentsBuilder); + + virtual ~JitModelBuilderInterface(); + + virtual storm::models::sparse::Model>* build() = 0; + + void addStateBehaviour(IndexType const& stateId, StateBehaviour& behaviour); + + protected: + ModelComponentsBuilder& modelComponentsBuilder; + }; + + + } + } +}