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;
    storm::RationalNumber const& 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& setInferObservationsFromActions(bool newValue = true);
 
    BuilderOptions& setScaleAndLiftTransitionRewards(bool newValue = true);
 
    BuilderOptions& setAddOutOfBoundsState(bool newValue = true);
 
    BuilderOptions& setAddOverlappingGuardsLabel(bool newValue = true);
 
    BuilderOptions& setReservedBitsForUnboundedVariables(uint64_t value);
 
    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;
 
    storm::RationalNumber stochasticTolerance;
};
 
}  // namespace builder
}  // namespace storm