AbstractAbstractionRefinementModelChecker.h

Go to the documentation of this file.

#pragma once
 
#include "storm/modelchecker/AbstractModelChecker.h"
#include "storm/storage/dd/DdType.h"
 
#include "storm-gamebased-ar/abstraction/AbstractionOptions.h"
 
namespace storm {
 
class Environment;
 
namespace dd {
template<storm::dd::DdType DdType>
class Bdd;
 
template<storm::dd::DdType DdType, typename ValueType>
class Add;
}  // namespace dd
 
namespace models {
template<typename ValueType>
class Model;
 
namespace symbolic {
template<storm::dd::DdType DdType, typename ValueType>
class Model;
 
template<storm::dd::DdType DdType, typename ValueType>
class Dtmc;
 
template<storm::dd::DdType DdType, typename ValueType>
class Mdp;
 
template<storm::dd::DdType DdType, typename ValueType>
class StochasticTwoPlayerGame;
}  // namespace symbolic
}  // namespace models
 
namespace modelchecker {
template<typename ModelType>
class SymbolicMdpPrctlModelChecker;
 
template<typename ValueType>
class QuantitativeCheckResult;
 
template<storm::dd::DdType DdType, typename ValueType>
class SymbolicQuantitativeCheckResult;
}  // namespace modelchecker
}  // namespace storm
 
namespace storm::gbar {
namespace abstraction {
class QualitativeResultMinMax;
 
template<storm::dd::DdType DdType>
class SymbolicQualitativeResultMinMax;
 
template<storm::dd::DdType DdType>
class SymbolicQualitativeMdpResultMinMax;
 
template<storm::dd::DdType DdType>
class SymbolicQualitativeGameResultMinMax;
 
class StateSet;
 
template<storm::dd::DdType DdType>
class SymbolicStateSet;
}  // namespace abstraction
 
namespace modelchecker {
 
template<typename ModelType>
class AbstractAbstractionRefinementModelChecker : public storm::modelchecker::AbstractModelChecker<ModelType> {
   public:
    typedef typename ModelType::ValueType ValueType;
    static const storm::dd::DdType DdType = ModelType::DdType;

    explicit AbstractAbstractionRefinementModelChecker(abstraction::AbstractionOptions const& options = abstraction::AbstractionOptions());
 
    virtual ~AbstractAbstractionRefinementModelChecker();

    virtual bool canHandle(storm::modelchecker::CheckTask<storm::logic::Formula> const& checkTask) const override;
    virtual std::unique_ptr<storm::modelchecker::CheckResult> computeUntilProbabilities(
        Environment const& env, storm::modelchecker::CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) override;
    virtual std::unique_ptr<storm::modelchecker::CheckResult> computeReachabilityProbabilities(
        Environment const& env, storm::modelchecker::CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
    virtual std::unique_ptr<storm::modelchecker::CheckResult> computeReachabilityRewards(
        Environment const& env, storm::modelchecker::CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
 
   protected:

    virtual bool supportsReachabilityRewards() const;

    virtual std::string const& getName() const = 0;

    virtual void initializeAbstractionRefinement() = 0;

    virtual std::shared_ptr<storm::models::Model<ValueType>> getAbstractModel() = 0;

    virtual std::pair<std::unique_ptr<storm::gbar::abstraction::StateSet>, std::unique_ptr<storm::gbar::abstraction::StateSet>> getConstraintAndTargetStates(
        storm::models::Model<ValueType> const& abstractModel) = 0;

    virtual uint64_t getAbstractionPlayer() const = 0;

    virtual bool requiresSchedulerSynthesis() const = 0;

    virtual void refineAbstractModel() = 0;


    std::unique_ptr<storm::modelchecker::CheckResult> performAbstractionRefinement(Environment const& env);

    std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>> computeBounds(
        Environment const& env, storm::models::Model<ValueType> const& abstractModel);

    std::unique_ptr<storm::gbar::abstraction::QualitativeResultMinMax> computeQualitativeResult(Environment const& env,
                                                                                                storm::models::Model<ValueType> const& abstractModel,
                                                                                                storm::gbar::abstraction::StateSet const& constraintStates,
                                                                                                storm::gbar::abstraction::StateSet const& targetStates);
    std::unique_ptr<storm::gbar::abstraction::QualitativeResultMinMax> computeQualitativeResult(
        Environment const& env, storm::models::symbolic::Model<DdType, ValueType> const& abstractModel,
        storm::gbar::abstraction::SymbolicStateSet<DdType> const& constraintStates, storm::gbar::abstraction::SymbolicStateSet<DdType> const& targetStates);
    std::unique_ptr<storm::gbar::abstraction::QualitativeResultMinMax> computeQualitativeResult(
        Environment const& env, storm::models::symbolic::Dtmc<DdType, ValueType> const& abstractModel,
        storm::gbar::abstraction::SymbolicStateSet<DdType> const& constraintStates, storm::gbar::abstraction::SymbolicStateSet<DdType> const& targetStates);
    std::unique_ptr<storm::gbar::abstraction::QualitativeResultMinMax> computeQualitativeResult(
        Environment const& env, storm::models::symbolic::Mdp<DdType, ValueType> const& abstractModel,
        storm::gbar::abstraction::SymbolicStateSet<DdType> const& constraintStates, storm::gbar::abstraction::SymbolicStateSet<DdType> const& targetStates);
    std::unique_ptr<storm::gbar::abstraction::QualitativeResultMinMax> computeQualitativeResult(
        Environment const& env, storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType> const& abstractModel,
        storm::gbar::abstraction::SymbolicStateSet<DdType> const& constraintStates, storm::gbar::abstraction::SymbolicStateSet<DdType> const& targetStates);
    std::unique_ptr<storm::gbar::abstraction::SymbolicQualitativeGameResultMinMax<DdType>> computeQualitativeResultReuse(
        storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType> const& abstractModel, storm::dd::Bdd<DdType> const& transitionMatrixBdd,
        storm::gbar::abstraction::SymbolicStateSet<DdType> const& constraintStates, storm::gbar::abstraction::SymbolicStateSet<DdType> const& targetStates,
        uint64_t abstractionPlayer, storm::OptimizationDirection const& modelNondeterminismDirection, bool requiresSchedulers);
    std::unique_ptr<storm::modelchecker::CheckResult> checkForResultAfterQualitativeCheck(storm::models::Model<ValueType> const& abstractModel);
    std::unique_ptr<storm::modelchecker::CheckResult> checkForResultAfterQualitativeCheck(
        storm::models::symbolic::Model<DdType, ValueType> const& abstractModel);
 
    // Methods related to the quantitative solution.
    bool skipQuantitativeSolution(storm::models::Model<ValueType> const& abstractModel,
                                  storm::gbar::abstraction::QualitativeResultMinMax const& qualitativeResults);
    bool skipQuantitativeSolution(storm::models::symbolic::Model<DdType, ValueType> const& abstractModel,
                                  storm::gbar::abstraction::SymbolicQualitativeResultMinMax<DdType> const& qualitativeResults);
    std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>> computeQuantitativeResult(
        Environment const& env, storm::models::Model<ValueType> const& abstractModel, storm::gbar::abstraction::StateSet const& constraintStates,
        storm::gbar::abstraction::StateSet const& targetStates, storm::gbar::abstraction::QualitativeResultMinMax const& qualitativeResults);
    std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>> computeQuantitativeResult(
        Environment const& env, storm::models::symbolic::Model<DdType, ValueType> const& abstractModel,
        storm::gbar::abstraction::SymbolicStateSet<DdType> const& constraintStates, storm::gbar::abstraction::SymbolicStateSet<DdType> const& targetStates,
        storm::gbar::abstraction::SymbolicQualitativeResultMinMax<DdType> const& qualitativeResults);
    std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>> computeQuantitativeResult(
        Environment const& env, storm::models::symbolic::Dtmc<DdType, ValueType> const& abstractModel,
        storm::gbar::abstraction::SymbolicStateSet<DdType> const& constraintStates, storm::gbar::abstraction::SymbolicStateSet<DdType> const& targetStates,
        storm::gbar::abstraction::SymbolicQualitativeResultMinMax<DdType> const& qualitativeResults);
    std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>> computeQuantitativeResult(
        Environment const& env, storm::models::symbolic::Mdp<DdType, ValueType> const& abstractModel,
        storm::gbar::abstraction::SymbolicStateSet<DdType> const& constraintStates, storm::gbar::abstraction::SymbolicStateSet<DdType> const& targetStates,
        storm::gbar::abstraction::SymbolicQualitativeResultMinMax<DdType> const& qualitativeResults);
    std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>> computeQuantitativeResult(
        Environment const& env, storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType> const& abstractModel,
        storm::gbar::abstraction::SymbolicStateSet<DdType> const& constraintStates, storm::gbar::abstraction::SymbolicStateSet<DdType> const& targetStates,
        storm::gbar::abstraction::SymbolicQualitativeResultMinMax<DdType> const& qualitativeResults);
    void filterInitialStates(storm::models::Model<ValueType> const& abstractModel,
                             std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>>& bounds);
    void filterInitialStates(storm::models::symbolic::Model<DdType, ValueType> const& abstractModel,
                             std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>>& bounds);
    void printBoundsInformation(std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>>& bounds);
    void printBoundsInformation(storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType> const& lowerBounds,
                                storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType> const& upperBounds);
    bool checkForResultAfterQuantitativeCheck(storm::models::Model<ValueType> const& abstractModel, bool lowerBounds,
                                              storm::modelchecker::QuantitativeCheckResult<ValueType> const& result);
    std::unique_ptr<storm::modelchecker::CheckResult> computeReachabilityProbabilitiesHelper(
        Environment const& env, storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType> const& abstractModel,
        storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::dd::Bdd<DdType> const& maybeStates,
        storm::dd::Bdd<DdType> const& prob1States, storm::dd::Add<DdType, ValueType> const& startValues);

    std::unique_ptr<storm::modelchecker::CheckResult> tryToObtainResultFromBounds(
        storm::models::Model<ValueType> const& model,
        std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>>& bounds);
    bool boundsAreSufficientlyClose(
        std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>> const& bounds);
    std::unique_ptr<storm::modelchecker::CheckResult> getAverageOfBounds(
        std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>> const& bounds);

    void setCheckTask(storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& checkTask);
    storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& getCheckTask() const;

    bool getReuseQualitativeResults() const;
    bool getReuseQuantitativeResults() const;
 
   private:
    std::unique_ptr<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const> checkTask;

    bool reuseQualitativeResults;

    bool reuseQuantitativeResults;

    double precision;

    std::unique_ptr<storm::gbar::abstraction::QualitativeResultMinMax> lastQualitativeResults;

    std::pair<std::unique_ptr<storm::modelchecker::CheckResult>, std::unique_ptr<storm::modelchecker::CheckResult>> lastBounds;
};
}  // namespace modelchecker
}  // namespace storm::gbar