ModelCheckerHelper.h

Go to the documentation of this file.

#pragma once
 
#include <boost/optional.hpp>
#include <type_traits>
 
#include "storm/models/ModelRepresentation.h"
#include "storm/storage/dd/Bdd.h"
 
#include "storm/storage/BitVector.h"
 
namespace storm {
namespace modelchecker {
namespace helper {
 
template<typename VT, storm::models::ModelRepresentation ModelRepresentation>
class ModelCheckerHelper {
   public:
    typedef VT ValueType;
 
    ModelCheckerHelper() = default;
    virtual ~ModelCheckerHelper() = default;
 
    using StateSet = typename std::conditional<ModelRepresentation == storm::models::ModelRepresentation::Sparse, storm::storage::BitVector,
                                               storm::dd::Bdd<storm::models::GetDdType<ModelRepresentation>::ddType>>::type;
 
    void setRelevantStates(StateSet const& relevantStates);
 
    void clearRelevantStates();
 
    bool hasRelevantStates() const;
 
    boost::optional<StateSet> const& getOptionalRelevantStates() const;
 
    StateSet const& getRelevantStates() const;
 
   private:
    boost::optional<StateSet> _relevantStates;
};
}  // namespace helper
}  // namespace modelchecker
}  // namespace storm