AbstractionSettings.h

Go to the documentation of this file.

#pragma once
 
#include "storm-gamebased-ar/abstraction/AbstractionOptions.h"
#include "storm/settings/modules/ModuleSettings.h"
 
namespace storm {
namespace settings {
namespace modules {

class AbstractionSettings : public ModuleSettings {
   public:
    enum class Method { Games, Bisimulation };
 
    // The remaining enums are defined by the game-based abstraction library (see AbstractionOptions.h) and are merely
    // aliased here so that the settings module stays consistent with the library's option types.
    using PivotSelectionHeuristic = storm::gbar::abstraction::PivotSelectionHeuristic;
 
    using SplitMode = storm::gbar::abstraction::SplitMode;
 
    using ReuseMode = storm::gbar::abstraction::ReuseMode;
 
    using SolveMode = storm::gbar::abstraction::SolveMode;
 
    using ValidBlockMode = storm::gbar::abstraction::ValidBlockMode;

    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