BigStep.h

Go to the documentation of this file.

#pragma once
 
#include <map>
#include <memory>
#include <set>
 
#include "storm/adapters/IntervalForward.h"
#include "storm/adapters/RationalFunctionAdapter.h"  // TODO: use forward header
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/StateLabeling.h"
 
namespace storm {
 
namespace logic {
class Formula;
}  // namespace logic
 
namespace modelchecker {
template<typename FormulaType, typename ValueType>
class CheckTask;
}  // namespace modelchecker
 
namespace storage {
template<typename ValueType>
class FlexibleSparseMatrix;
}  // namespace storage
 
namespace transformer {
 
using UniPoly = RawUnivariatePolynomial;
 
// optimization for the polynomial cache - built in comparison is slow
struct UniPolyCompare {
    bool operator()(const UniPoly& lhs, const UniPoly& rhs) const;
};
 
struct UniPolyDefaultCompare {
    bool operator()(UniPoly const& lhs, UniPoly const& rhs) const {
        return lhs.less(rhs);
    }
};
 
struct PolynomialCache : std::unordered_map<RationalFunctionVariable, std::pair<std::map<UniPoly, uint64_t, UniPolyCompare>, std::vector<UniPoly>>> {
    uint64_t lookUpInCache(UniPoly const& f, RationalFunctionVariable const& p);

    UniPoly polynomialFromFactorization(std::vector<uint64_t> const& factorization, RationalFunctionVariable const& p) const;
};
 
template<typename Container>
struct container_hash {
    std::size_t operator()(Container const& c) const {
        return boost::hash_range(c.begin(), c.end());
    }
};
 
class Annotation : public std::unordered_map<std::vector<uint64_t>, RationalFunctionCoefficient, container_hash<std::vector<uint64_t>>> {
   public:
    Annotation(RationalFunctionVariable parameter, std::shared_ptr<PolynomialCache> polynomialCache);

    void operator+=(const Annotation other);

    void operator*=(RationalFunctionCoefficient n);

    Annotation operator*(RationalFunctionCoefficient n) const;

    void addAnnotationTimesConstant(Annotation const& other, RationalFunctionCoefficient timesConstant);

    void addAnnotationTimesPolynomial(Annotation const& other, UniPoly&& polynomial);

    void addAnnotationTimesAnnotation(Annotation const& anno1, Annotation const& anno2);

    UniPoly getProbability() const;

    std::vector<UniPoly> getTerms() const;
 
    template<typename ConstantType>
    ConstantType evaluate(ConstantType input) const {
        ConstantType sumOfTerms = utility::zero<ConstantType>();
        for (auto const& [info, constant] : *this) {
            ConstantType outerMult = utility::one<ConstantType>();
            for (uint64_t i = 0; i < info.size(); i++) {
                auto polynomial = this->polynomialCache->at(parameter).second[i];
                // Evaluate the inner polynomial by its coefficients
                auto coefficients = polynomial.coefficients();
                ConstantType innerSum = utility::zero<ConstantType>();
                for (uint64_t exponent = 0; exponent < coefficients.size(); exponent++) {
                    if (exponent != 0) {
                        innerSum += storm::utility::pow(input, exponent) * storm::utility::convertNumber<ConstantType>(coefficients[exponent]);
                    } else {
                        innerSum += utility::convertNumber<ConstantType>(coefficients[exponent]);
                    }
                }
                // Inner polynomial ^ exponent
                outerMult *= storm::utility::pow(innerSum, info[i]);
            }
            sumOfTerms += outerMult * utility::convertNumber<ConstantType>(constant);
        }
        return sumOfTerms;
    }
 
    Interval evaluateOnIntervalMidpointTheorem(Interval input, bool higherOrderBounds = false) const;
 
    RationalFunctionVariable getParameter() const;
 
    void computeDerivative(uint64_t nth);
 
    uint64_t maxDegree() const;
 
    std::shared_ptr<Annotation> derivative();
 
    friend std::ostream& operator<<(std::ostream& os, const Annotation& annotation);
 
   private:
    const RationalFunctionVariable parameter;
    const std::shared_ptr<PolynomialCache> polynomialCache;
    std::shared_ptr<Annotation> derivativeOfThis;
};
 
std::ostream& operator<<(std::ostream& os, const Annotation& annotation);
 
using UniPolyAnnotationMap = std::map<UniPoly, Annotation, UniPolyDefaultCompare>;

class BigStep {
   public:
    BigStep() : polynomialCache(std::make_shared<PolynomialCache>()) {
        // Intentionally left empty
    }
 
    RationalFunction uniPolyToRationalFunction(UniPoly poly);

    std::pair<models::sparse::Dtmc<RationalFunction>, UniPolyAnnotationMap> bigStep(models::sparse::Dtmc<RationalFunction> const& model,
                                                                                    modelchecker::CheckTask<logic::Formula, RationalFunction> const& checkTask);
 
    static std::unordered_map<RationalFunction, Annotation> lastSavedAnnotations;
 
   private:
    std::pair<std::map<uint64_t, Annotation>, std::pair<std::vector<uint64_t>, std::map<uint64_t, std::set<uint64_t>>>> bigStepBFS(
        uint64_t start, const RationalFunctionVariable& parameter, const storage::FlexibleSparseMatrix<RationalFunction>& flexibleMatrix,
        const storage::FlexibleSparseMatrix<RationalFunction>& backwardsFlexibleMatrix,
        const std::map<RationalFunctionVariable, std::map<uint64_t, std::set<uint64_t>>>& treeStates,
        const boost::optional<std::vector<RationalFunction>>& stateRewardVector, const UniPolyAnnotationMap& storedAnnotations);

    std::vector<std::pair<uint64_t, Annotation>> findBigStep(const std::map<uint64_t, Annotation> bigStepAnnotations, const RationalFunctionVariable& parameter,
                                                             storage::FlexibleSparseMatrix<RationalFunction>& flexibleMatrix,
                                                             storage::FlexibleSparseMatrix<RationalFunction>& backwardsFlexibleMatrix,
                                                             std::map<RationalFunctionVariable, std::set<std::set<uint64_t>>>& alreadyTimeTravelledToThis,
                                                             std::map<RationalFunctionVariable, std::set<uint64_t>>& treeStatesNeedUpdate, uint64_t root,
                                                             uint64_t originalNumStates);

    UniPolyAnnotationMap replaceWithNewTransitions(uint64_t state, const std::vector<std::pair<uint64_t, Annotation>> transitions,
                                                   storage::FlexibleSparseMatrix<RationalFunction>& flexibleMatrix,
                                                   storage::FlexibleSparseMatrix<RationalFunction>& backwardsFlexibleMatrix,
                                                   storage::BitVector& reachableStates,
                                                   std::map<RationalFunctionVariable, std::set<uint64_t>>& treeStatesNeedUpdate);

    void updateUnreachableStates(storage::BitVector& reachableStates, std::vector<uint64_t> const& statesMaybeUnreachable,
                                 storage::FlexibleSparseMatrix<RationalFunction> const& backwardsFlexibleMatrix, uint64_t initialState);

    void updateTreeStates(std::map<RationalFunctionVariable, std::map<uint64_t, std::set<uint64_t>>>& treeStates,
                          std::map<RationalFunctionVariable, std::set<uint64_t>>& workingSets,
                          const storage::FlexibleSparseMatrix<RationalFunction>& flexibleMatrix,
                          const storage::FlexibleSparseMatrix<RationalFunction>& backwardsTransitions, const std::set<RationalFunctionVariable>& allParameters,
                          const boost::optional<std::vector<RationalFunction>>& stateRewardVector, const models::sparse::StateLabeling stateLabelling);

    models::sparse::StateLabeling extendStateLabeling(const models::sparse::StateLabeling& oldLabeling, uint64_t oldSize, uint64_t newSize,
                                                      uint64_t stateWithLabels, const std::set<std::string>& labelsInFormula);
    std::vector<storm::storage::MatrixEntry<uint64_t, RationalFunction>> joinDuplicateTransitions(
        std::vector<storm::storage::MatrixEntry<uint64_t, RationalFunction>> const& entries);
 
    std::shared_ptr<RawPolynomialCache> rawPolynomialCache;
 
    const std::shared_ptr<PolynomialCache> polynomialCache;
};
 
}  // namespace transformer
}  // namespace storm