BuilderOptions.h

Go to the documentation of this file.

#pragma once
 
#include <set>
#include <string>
#include <vector>
 
#include <boost/optional.hpp>
#include <boost/variant.hpp>
 
#include "storm/storage/SymbolicModelDescription.h"
#include "storm/storage/expressions/Expression.h"
 
namespace storm {
namespace expressions {
class ExpressionManager;
}
 
namespace models {
namespace sparse {
class StateLabeling;
}
}  // namespace models
 
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:
    boost::variant<std::string, storm::expressions::Expression> labelOrExpression;
};
 
class BuilderOptions {
   public:
    BuilderOptions(bool buildAllRewardModels = false, bool buildAllLabels = false);

    BuilderOptions(storm::logic::Formula const& formula,
                   storm::storage::SymbolicModelDescription const& modelDescription = storm::storage::SymbolicModelDescription());

    BuilderOptions(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas,
                   storm::storage::SymbolicModelDescription const& modelDescription = storm::storage::SymbolicModelDescription());

    void preserveFormula(storm::logic::Formula const& formula,
                         storm::storage::SymbolicModelDescription const& modelDescription = storm::storage::SymbolicModelDescription());

    void setTerminalStatesFromFormula(storm::logic::Formula const& formula);

    std::set<std::string> const& getRewardModelNames() const;

    std::set<std::string> const& getLabelNames() const;

    std::vector<std::pair<std::string, storm::expressions::Expression>> const& getExpressionLabels() const;
    std::vector<std::pair<LabelOrExpression, bool>> const& getTerminalStates() const;
    bool hasTerminalStates() const;
    void clearTerminalStates();
    bool isApplyMaximalProgressAssumptionSet() const;
    bool isBuildChoiceLabelsSet() const;
    bool isBuildStateValuationsSet() const;
    bool isBuildObservationValuationsSet() const;
    bool isBuildChoiceOriginsSet() const;
    bool isBuildAllRewardModelsSet() const;
    bool isBuildAllLabelsSet() const;
    bool isExplorationChecksSet() const;
    bool isInferObservationsFromActionsSet() const;
    bool isShowProgressSet() const;
    bool isScaleAndLiftTransitionRewardsSet() const;
    bool isAddOutOfBoundsStateSet() const;
    uint64_t getReservedBitsForUnboundedVariables() const;
    bool isAddOverlappingGuardLabelSet() const;
    uint64_t getShowProgressDelay() const;
    double getStochasticTolerance() const;

    BuilderOptions& setBuildAllRewardModels(bool newValue = true);
    BuilderOptions& addRewardModel(std::string const& rewardModelName);
    BuilderOptions& setBuildAllLabels(bool newValue = true);
    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& setApplyMaximalProgressAssumption(bool newValue = true);

    BuilderOptions& setBuildChoiceLabels(bool newValue = true);
    BuilderOptions& setBuildStateValuations(bool newValue = true);

    BuilderOptions& setBuildObservationValuations(bool newValue = true);

    BuilderOptions& setBuildChoiceOrigins(bool newValue = true);
    BuilderOptions& setExplorationChecks(bool newValue = true);

    BuilderOptions& setScaleAndLiftTransitionRewards(bool newValue = true);

    BuilderOptions& setAddOutOfBoundsState(bool newValue = true);

    BuilderOptions& setAddOverlappingGuardsLabel(bool newValue = true);

    BuilderOptions& setReservedBitsForUnboundedVariables(uint64_t value);

    BuilderOptions& setStochasticTolerance(double newValue);

    BuilderOptions& setShowProgress(bool newValue = true);

    BuilderOptions& setShowProgressDelay(uint64_t newValue);

    BuilderOptions& substituteExpressions(std::function<storm::expressions::Expression(storm::expressions::Expression const&)> const& substitutionFunction);
 
   private:
    bool buildAllRewardModels;

    std::set<std::string> rewardModelNames;

    bool buildAllLabels;

    std::set<std::string> labelNames;

    std::vector<std::pair<std::string, storm::expressions::Expression>> expressionLabels;

    std::vector<std::pair<LabelOrExpression, bool>> terminalStates;

    bool applyMaximalProgressAssumption;

    bool buildChoiceLabels;

    bool buildStateValuations;

    bool buildObservationValuations;
 
    // A flag that indicates whether or not to generate the information from which parts of the model specification
    // each choice originates.
    bool buildChoiceOrigins;

    bool scaleAndLiftTransitionRewards;

    bool explorationChecks;

    bool inferObservationsFromActions;

    bool addOverlappingGuardsLabel;

    bool addOutOfBoundsState;

    uint64_t reservedBitsForUnboundedVariables;

    bool showProgress;

    uint64_t showProgressDelay;

    double stochasticTolerance;
};
 
}  // namespace builder
}  // namespace storm