AbstractionSettings.h

Go to the documentation of this file.

#pragma once
 
#include "storm/settings/modules/ModuleSettings.h"
 
namespace storm {
namespace settings {
namespace modules {
 
class AbstractionSettings : public ModuleSettings {
   public:
    enum class Method { Games, Bisimulation };
 
    enum class PivotSelectionHeuristic { NearestMaximalDeviation, MostProbablePath, MaxWeightedDeviation };
 
    enum class SplitMode { All, None, NonGuard };
 
    enum class ReuseMode { All, None, Qualitative, Quantitative };
 
    enum class SolveMode { Dd, Sparse };
 
    enum class ValidBlockMode { MorePredicates, BlockEnumeration };
 
    AbstractionSettings();
 
    Method getAbstractionRefinementMethod() const;
 
    bool isUseDecompositionSet() const;
 
    SplitMode getSplitMode() const;
 
    bool isAddAllGuardsSet() const;
 
    bool isAddAllInitialExpressionsSet() const;
 
    void setAddAllGuards(bool value);
 
    void setAddAllInitialExpressions(bool value);
 
    bool isUseInterpolationSet() const;
 
    double getPrecision() const;
 
    bool getRelativeTerminationCriterion() const;
 
    PivotSelectionHeuristic getPivotSelectionHeuristic() const;
 
    ReuseMode getReuseMode() const;
 
    bool isRestrictToRelevantStatesSet() const;
 
    SolveMode getSolveMode() const;
 
    uint_fast64_t getMaximalAbstractionCount() const;
 
    /*
     * Determines whether refinement predicates are to be ranked.
     *
     * @return True iff the refinement predicates are to be ranked.
     */
    bool isRankRefinementPredicatesSet() const;
 
    bool isConstraintsSet() const;
 
    std::string getConstraintString() const;
 
    bool isUseEagerRefinementSet() const;
 
    bool isDebugSet() const;
 
    bool isInjectRefinementPredicatesSet() const;
 
    std::string getInjectedRefinementPredicates() const;
 
    bool isFixPlayer1StrategySet() const;
 
    bool isFixPlayer2StrategySet() const;
 
    ValidBlockMode getValidBlockMode() const;
 
    const static std::string moduleName;
 
   private:
    const static std::string methodOptionName;
    const static std::string useDecompositionOptionName;
    const static std::string splitModeOptionName;
    const static std::string addAllGuardsOptionName;
    const static std::string addInitialExpressionsOptionName;
    const static std::string useInterpolationOptionName;
    const static std::string precisionOptionName;
    const static std::string relativeOptionName;
    const static std::string pivotHeuristicOptionName;
    const static std::string reuseResultsOptionName;
    const static std::string restrictToRelevantStatesOptionName;
    const static std::string solveModeOptionName;
    const static std::string maximalAbstractionOptionName;
    const static std::string rankRefinementPredicatesOptionName;
    const static std::string constraintsOptionName;
    const static std::string useEagerRefinementOptionName;
    const static std::string debugOptionName;
    const static std::string injectRefinementPredicatesOptionName;
    const static std::string fixPlayer1StrategyOptionName;
    const static std::string fixPlayer2StrategyOptionName;
    const static std::string validBlockModeOptionName;
};
 
}  // namespace modules
}  // namespace settings
}  // namespace storm