AbstractionOptions.h

Go to the documentation of this file.

#pragma once
 
#include <cstdint>
#include <vector>
 
#include "storm/storage/expressions/Expression.h"
 
namespace storm::gbar {
namespace abstraction {
 
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 };

struct AbstractionOptions {
    AbstractionOptions() = default;
 
    AbstractionOptions(std::vector<storm::expressions::Expression>&& constraints,
                       std::vector<std::vector<storm::expressions::Expression>>&& injectedRefinementPredicates)
        : constraints(std::move(constraints)), injectedRefinementPredicates(std::move(injectedRefinementPredicates)) {
        // Intentionally left empty.
    }
 
    // Options for the abstractor.
    bool restrictToRelevantStates = true;

    bool restrictToValidBlocks = false;

    bool useDecomposition = true;
 
    // Options for the refiner.
    bool useInterpolation = true;

    SplitMode splitMode = SplitMode::All;

    PivotSelectionHeuristic pivotSelectionHeuristic = PivotSelectionHeuristic::NearestMaximalDeviation;

    bool rankRefinementPredicates = false;

    bool useEagerRefinement = false;

    bool addAllGuards = true;

    bool addAllInitialExpressions = true;
 
    // Options for the model checking procedure.
    double precision = 1e-03;

    bool relativeTerminationCriterion = false;

    SolveMode solveMode = SolveMode::Sparse;

    ReuseMode reuseMode = ReuseMode::All;

    uint_fast64_t maximalNumberOfAbstractions = 20000;

    bool fixPlayer1Strategy = true;

    bool fixPlayer2Strategy = true;

    bool debug = false;
 
    // Predicates.
    std::vector<storm::expressions::Expression> constraints;

    std::vector<std::vector<storm::expressions::Expression>> injectedRefinementPredicates;
};
 
}  // namespace abstraction
}  // namespace storm::gbar