ExplicitQuantitativeCheckResult.h

Go to the documentation of this file.

#pragma once
#include <optional>
#include <vector>
 
#include "storm/adapters/JsonForward.h"
#include "storm/modelchecker/results/QuantitativeCheckResult.h"
#include "storm/models/sparse/StateLabeling.h"
#include "storm/solver/SolutionBounds.h"
#include "storm/storage/BitVector.h"
#include "storm/storage/Scheduler.h"
#include "storm/storage/sparse/StateType.h"
#include "storm/storage/valuations/Valuations.h"
#include "storm/utility/ExtendedNumber.h"
 
namespace storm {
 
namespace modelchecker {
// Forward declaration
template<typename ValueType>
class ExplicitQualitativeCheckResult;

template<typename ValueType>
class ExplicitQuantitativeCheckResult : public QuantitativeCheckResult<ValueType> {
   public:
    typedef typename QuantitativeCheckResult<ValueType>::ExtendedValueType ExtendedValueType;
    typedef std::vector<ExtendedValueType> vector_type;

    ExplicitQuantitativeCheckResult(storm::storage::sparse::state_type const& state, ExtendedValueType const& value);

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

    ExplicitQuantitativeCheckResult(storm::storage::BitVector states, vector_type&& values,
                                    std::optional<std::shared_ptr<storm::storage::Scheduler<ValueType>>> scheduler = {});

    ExplicitQuantitativeCheckResult(std::vector<ValueType> const& values)
        requires(!std::is_same_v<storm::utility::ExtendedValueType<ValueType>, ValueType>);
    ExplicitQuantitativeCheckResult(std::vector<ValueType>&& values)
        requires(!std::is_same_v<storm::utility::ExtendedValueType<ValueType>, ValueType>);
    ExplicitQuantitativeCheckResult(storm::storage::BitVector states, std::vector<ValueType>&& values)
        requires(!std::is_same_v<storm::utility::ExtendedValueType<ValueType>, ValueType>);
 
    ExplicitQuantitativeCheckResult(ExplicitQuantitativeCheckResult const& other) = default;
    ExplicitQuantitativeCheckResult& operator=(ExplicitQuantitativeCheckResult const& other) = default;
    ExplicitQuantitativeCheckResult(ExplicitQuantitativeCheckResult&& other) = default;
    ExplicitQuantitativeCheckResult& operator=(ExplicitQuantitativeCheckResult&& other) = default;
    explicit ExplicitQuantitativeCheckResult(ExplicitQualitativeCheckResult<ValueType> const& other);
 
    virtual ~ExplicitQuantitativeCheckResult() = default;
 
    virtual std::unique_ptr<CheckResult> clone() const override;

    ExtendedValueType& operator[](storm::storage::sparse::state_type state);
    ExtendedValueType const& operator[](storm::storage::sparse::state_type state) const;
 
    virtual std::unique_ptr<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, ValueType const& bound) const override;
 
    virtual bool isExplicit() const override;
    virtual bool isResultForAllStates() const override;
 
    virtual bool isExplicitQuantitativeCheckResult() const override;

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

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

    vector_type const& getValueVector() const;
    vector_type& getValueVector();

    std::vector<ValueType> getFiniteValueVector() const;

    std::vector<ValueType> getSentinelValueVector() const;

    bool hasLowerBounds() const;
    bool hasUpperBounds() const;

    vector_type const& getLowerBoundVector() const;
    vector_type const& getUpperBoundVector() const;

    storm::solver::SolutionBounds<ExtendedValueType> const& getSolutionBounds() const;

    void setLowerBounds(vector_type lowerBounds);
    void setUpperBounds(vector_type upperBounds);
    void setBounds(storm::solver::SolutionBounds<ExtendedValueType> bounds);

    void setBounds(storm::solver::SolutionBounds<ValueType> bounds)
        requires(!std::is_same_v<storm::utility::ExtendedValueType<ValueType>, ValueType>);

    void setValuesExact();

    void clearBounds();
 
    virtual std::ostream& writeToStream(std::ostream& out) const override;
 
    virtual void filter(QualitativeCheckResult const& filter) override;
 
    virtual void oneMinus() override;
 
    virtual ExtendedValueType getMin() const override;
    virtual ExtendedValueType getMax() const override;
    virtual std::pair<ExtendedValueType, ExtendedValueType> getMinMax() const;
    virtual ExtendedValueType average() const override;
    virtual ExtendedValueType sum() const override;
 
    virtual AggregatedValue<ExtendedValueType> aggregate(FilterType filter) const 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();
 
    storm::json<ValueType> 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 ExtendedValueType aggregateVector(vector_type const& vector, FilterType filter);

    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, values[offset]);
            ++offset;
        }
    }

    void printValue(std::ostream& out, uint64_t offset) const;
 
    // The states this result holds values for, which are all states of the model unless it was narrowed down.
    storm::storage::BitVector states;
 
    // The values of the quantitative check result, one per state this result is for. These are estimates that
    // lie within the bounds below but carry no further guarantee.
    vector_type values;
 
    // Sound bounds on the actual values, if an algorithm provided them.
    storm::solver::SolutionBounds<ExtendedValueType> bounds;
 
    // An optional scheduler that accompanies the values.
    std::optional<std::shared_ptr<storm::storage::Scheduler<ValueType>>> scheduler;
};
}  // namespace modelchecker
}  // namespace storm