SparsePropositionalModelChecker.h

Go to the documentation of this file.

#ifndef STORM_MODELCHECKER_SPARSEPROPOSITIONALMODELCHECKER_H_
#define STORM_MODELCHECKER_SPARSEPROPOSITIONALMODELCHECKER_H_
 
#include "storm/modelchecker/AbstractModelChecker.h"
 
namespace storm {
namespace modelchecker {
 
template<typename SparseModelType>
class SparsePropositionalModelChecker : public AbstractModelChecker<SparseModelType> {
   public:
    typedef typename SparseModelType::ValueType ValueType;
    typedef typename SparseModelType::RewardModelType RewardModelType;
    using SolutionType = typename std::conditional<std::is_same_v<ValueType, storm::Interval>, double, ValueType>::type;
 
    explicit SparsePropositionalModelChecker(SparseModelType const& model);
 
    // The implemented methods of the AbstractModelChecker interface.
    virtual bool canHandle(CheckTask<storm::logic::Formula, SolutionType> const& checkTask) const override;
    virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(Environment const& env,
                                                                    CheckTask<storm::logic::BooleanLiteralFormula, SolutionType> const& checkTask) override;
    virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(Environment const& env,
                                                                 CheckTask<storm::logic::AtomicLabelFormula, SolutionType> const& checkTask) override;
 
   protected:
    SparseModelType const& getModel() const;
 
   private:
    // The model that is to be analyzed by the model checker.
    SparseModelType const& model;
};
}  // namespace modelchecker
}  // namespace storm
 
#endif /* STORM_MODELCHECKER_SPARSEPROPOSITIONALMODELCHECKER_H_ */