ExplicitQualitativeCheckResult.h

Go to the documentation of this file.

#pragma once
 
#include <optional>
 
#include "storm/adapters/JsonForward.h"
#include "storm/modelchecker/results/QualitativeCheckResult.h"
#include "storm/models/sparse/StateLabeling.h"
#include "storm/storage/BitVector.h"
#include "storm/storage/Scheduler.h"
#include "storm/storage/sparse/StateType.h"
#include "storm/storage/valuations/Valuations.h"
 
namespace storm {
 
namespace modelchecker {

template<typename ValueType>
class ExplicitQualitativeCheckResult : public QualitativeCheckResult {
   public:
    typedef storm::storage::BitVector vector_type;

    ExplicitQualitativeCheckResult(storm::storage::sparse::state_type state, bool value);

    ExplicitQualitativeCheckResult(vector_type const& truthValues, std::optional<std::shared_ptr<storm::storage::Scheduler<ValueType>>> scheduler = {});
    ExplicitQualitativeCheckResult(vector_type&& truthValues, std::optional<std::shared_ptr<storm::storage::Scheduler<ValueType>>> scheduler = {});

    ExplicitQualitativeCheckResult(storm::storage::BitVector states, vector_type&& truthValues,
                                   std::optional<std::shared_ptr<storm::storage::Scheduler<ValueType>>> scheduler = {});
 
    virtual ~ExplicitQualitativeCheckResult() = default;
    ExplicitQualitativeCheckResult(ExplicitQualitativeCheckResult const& other) = default;
    ExplicitQualitativeCheckResult& operator=(ExplicitQualitativeCheckResult const& other) = default;
    ExplicitQualitativeCheckResult(ExplicitQualitativeCheckResult&& other) = default;
    ExplicitQualitativeCheckResult& operator=(ExplicitQualitativeCheckResult&& other) = default;
 
    virtual std::unique_ptr<CheckResult> clone() const override;

    bool operator[](storm::storage::sparse::state_type state) const;
 
    virtual bool isExplicit() const override;
    virtual bool isResultForAllStates() const override;
 
    virtual bool isExplicitQualitativeCheckResult() const override;
 
    virtual QualitativeCheckResult& operator&=(QualitativeCheckResult const& other) override;
    virtual QualitativeCheckResult& operator|=(QualitativeCheckResult const& other) override;
    virtual void complement() override;

    bool hasValueForState(storm::storage::sparse::state_type state) const;

    storm::storage::BitVector const& getStates() const;

    vector_type const& getTruthValuesVector() const;
 
    virtual bool existsTrue() const override;
    virtual bool forallTrue() const override;
    virtual uint64_t count() const override;
 
    virtual std::ostream& writeToStream(std::ostream& out) const override;
 
    virtual void filter(QualitativeCheckResult const& filter) override;
 
    virtual bool hasScheduler() const override;
    void setScheduler(std::unique_ptr<storm::storage::Scheduler<ValueType>>&& scheduler);
    storm::storage::Scheduler<ValueType> const& getScheduler() const;
    storm::storage::Scheduler<ValueType>& getScheduler();
 
    template<typename JsonRationalType>
    storm::json<JsonRationalType> toJson(std::optional<storm::storage::sparse::Valuations> const& stateValuations = std::nullopt,
                                         std::optional<storm::models::sparse::StateLabeling> const& stateLabels = std::nullopt) const;
 
   private:
    bool hasValueType(std::type_info const& t) const override {
        return t == typeid(ValueType);
    }
 
    static void performLogicalOperation(ExplicitQualitativeCheckResult& first, QualitativeCheckResult const& second, bool logicalAnd);

    uint64_t getOffset(storm::storage::sparse::state_type state) const;

    template<typename Function>
    void forEachState(Function const& f) const {
        uint64_t offset = 0;
        for (uint64_t state : states) {
            f(state, truthValues.get(offset));
            ++offset;
        }
    }
 
    // The states this result holds truth values for, which are all states of the model unless it was narrowed down.
    storm::storage::BitVector states;
 
    // The truth values of the qualitative check result, one per state this result is for.
    vector_type truthValues;
 
    // An optional scheduler that accompanies the values.
    std::optional<std::shared_ptr<storm::storage::Scheduler<ValueType>>> scheduler;
};
}  // namespace modelchecker
}  // namespace storm