RobustParameterLifter.h

Go to the documentation of this file.

#pragma once
 
#include <memory>
#include <set>
#include <unordered_map>
#include <vector>
 
#include "storm-pars/modelchecker/region/monotonicity/LocalMonotonicityResult.h"
#include "storm-pars/transformer/BigStep.h"
#include "storm-pars/utility/parametric.h"
#include "storm/adapters/RationalFunctionForward.h"
#include "storm/solver/OptimizationDirection.h"
#include "storm/storage/BitVector.h"
#include "storm/storage/SparseMatrix.h"
 
namespace storm {
 
namespace analysis {
class Order;
}  // namespace analysis
 
namespace storage {
template<typename ParametricType>
class ParameterRegion;
}  // namespace storage
 
namespace transformer {
 
template<typename ParametricType, typename ConstantType>
class RobustParameterLifter {
   public:
    typedef typename storm::utility::parametric::VariableType<ParametricType>::type VariableType;
    typedef typename storm::utility::parametric::CoefficientType<ParametricType>::type CoefficientType;
    typedef typename storm::analysis::MonotonicityResult<VariableType>::Monotonicity Monotonicity;
 
    RobustParameterLifter(storm::storage::SparseMatrix<ParametricType> const& pMatrix, std::vector<ParametricType> const& pVector,
                          storm::storage::BitVector const& selectedRows, storm::storage::BitVector const& selectedColumns, bool generateRowLabels = false,
                          bool useMonotonicity = false);
 
    void specifyRegion(storm::storage::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
 
    void specifyRegion(storm::storage::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForParameters,
                       storm::storage::BitVector const& selectedRows);
 
    void specifyRegion(storm::storage::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForParameters,
                       std::shared_ptr<storm::analysis::Order> reachabilityOrder,
                       std::shared_ptr<storm::analysis::LocalMonotonicityResult<VariableType>> localMonotonicityResult);
 
    // Returns the resulting matrix. Should only be called AFTER specifying a region
    storm::storage::SparseMatrix<Interval> const& getMatrix() const;
 
    // Returns the resulting vector. Should only be called AFTER specifying a region
    std::vector<Interval> const& getVector() const;
 
    std::vector<std::set<VariableType>> const& getOccurringVariablesAtState() const;
 
    std::map<VariableType, std::set<uint_fast64_t>> const& getOccuringStatesAtVariable() const;
 
    // Returns whether the curent region is all ill-defined.
    bool isCurrentRegionAllIllDefined() const;
 
    /*
     * We minimize the number of function evaluations by only calling evaluate() once for each unique pair of function and valuation.
     * The result of each evaluation is then written to all positions in the matrix (and the vector) where the corresponding (function,valuation) occurred.
     */
    class RobustAbstractValuation {
       public:
        RobustAbstractValuation(storm::RationalFunction transition);
        RobustAbstractValuation(RobustAbstractValuation const& other) = default;
        bool operator==(RobustAbstractValuation const& other) const;
 
        std::size_t getHashValue() const;
 
        std::set<VariableType> const& getParameters() const;
 
        uint64_t getNumTransitions() const;
 
        storm::RationalFunction const& getTransition() const;
 
        void initialize();
 
        std::optional<std::map<VariableType, std::set<CoefficientType>>> const& getExtrema() const;
 
        std::optional<Annotation> const& getAnnotation() const;
 
       private:
        std::set<CoefficientType> cubicEquationZeroes(RawPolynomial polynomial, VariableType parameter);
 
        std::optional<std::set<CoefficientType>> zeroesSMT(RationalFunction function, VariableType parameter);
 
        std::optional<std::set<CoefficientType>> zeroesCarl(UniPoly polynomial, VariableType parameter);
 
        std::set<VariableType> parameters;
 
        storm::RationalFunction const transition;
 
        // position and value of the extrema of each of the functions (if computable)
        std::optional<std::map<VariableType, std::set<CoefficientType>>> extrema;
 
        // extrema could not be computed => use interval arithmetic
        std::optional<Annotation> annotation;
    };
 
   private:
    class FunctionValuationCollector {
       public:
        FunctionValuationCollector() = default;
 
        Interval& add(RobustAbstractValuation& valuation);
 
        bool evaluateCollectedFunctions(storm::storage::ParameterRegion<ParametricType> const& region,
                                        storm::solver::OptimizationDirection const& dirForUnspecifiedParameters);
 
       private:
        class RobustAbstractValuationHash {
           public:
            std::size_t operator()(RobustAbstractValuation const& valuation) const {
                return valuation.getHashValue();
            }
        };
 
        // Stores the collected functions with the valuations together with a placeholder for the result.
        std::unordered_map<RobustAbstractValuation, Interval, RobustAbstractValuationHash> collectedValuations;
        // Stores regions and bounds for abstract evaluations that use them
        // We store this here because we cannot change the existing robustabstractvaluations in collectedValuations
        std::unordered_map<RobustAbstractValuation, std::vector<std::pair<Interval, Interval>>, RobustAbstractValuationHash> regionsAndBounds;
    };
 
    FunctionValuationCollector functionValuationCollector;
 
    storm::storage::SparseMatrix<Interval> matrix;  // The resulting matrix;
    std::vector<std::pair<typename storm::storage::SparseMatrix<Interval>::iterator, Interval&>>
        matrixAssignment;  // Connection of matrix entries with placeholders
 
    std::vector<uint64_t> oldToNewColumnIndexMapping;  // Mapping from old to new columnIndex
    std::vector<uint64_t> oldToNewRowIndexMapping;     // Mapping from old to new columnIndex
    std::vector<uint64_t> rowGroupToStateNumber;       // Mapping from new to old columnIndex
 
    bool currentRegionAllIllDefined = false;
 
    std::vector<Interval> vector;
    std::vector<std::pair<typename std::vector<Interval>::iterator, Interval&>> vectorAssignment;  // Connection of vector entries with placeholders
 
    std::vector<std::set<VariableType>> occurringVariablesAtState;
    std::map<VariableType, std::set<uint_fast64_t>> occuringStatesAtVariable;
};
 
}  // namespace transformer
}  // namespace storm