GraphConditions.h

Go to the documentation of this file.

#pragma once
 
#include <cstddef>
#include <memory>
#include <set>
#include <unordered_map>
#include <vector>
 
#include "storm/adapters/RationalFunctionAdapter.h"
#include "storm/models/sparse/ModelForward.h"
#include "storm/storage/expressions/BinaryRelationType.h"
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/expressions/HashVisitor.h"
 
namespace storm {
namespace expressions {
class ExpressionManager;
}
namespace analysis {

class ConstraintCollector {
   public:
    using ConstraintSet = std::vector<storm::expressions::Expression>;
 
   private:
    using ConstraintIndex = std::unordered_map<std::size_t, ConstraintSet>;
 
    // The expression manager owning the collected constraints.
    std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
 
    // Hashes expressions by their structure, so that they can be deduplicated and looked up.
    storm::expressions::HashVisitor hashVisitor;
 
    // A set of constraints that says that the DTMC actually has valid probability distributions in all states.
    ConstraintSet wellformedConstraintSet;
 
    // An index over the wellformed constraints. It mirrors wellformedConstraintSet.
    ConstraintIndex wellformedConstraintIndex;
 
    // A set of constraints that makes sure that the underlying graph of the model does not change depending
    // on the parameter values.
    ConstraintSet graphPreservingConstraintSet;
 
    // An index over the graph preserving constraints. It mirrors graphPreservingConstraintSet.
    ConstraintIndex graphPreservingConstraintIndex;
 
    // A set of variables
    std::set<storm::RationalFunctionVariable> variableSet;

    storm::expressions::Expression relateToZero(storm::RawPolynomial const& polynomial, storm::expressions::RelationType relation) const;

    bool addConstraint(ConstraintSet& constraintSet, ConstraintIndex& constraintIndex, storm::expressions::Expression const& constraint);

    void wellformedRequiresNonNegativeEntries(storm::RationalFunction const& value);

    void wellformedRequiresAtMostOne(storm::RationalFunction const& value);

    void graphPreservingRequiresNonZero(storm::RationalFunction const& value);

    void process(storm::models::sparse::Model<storm::RationalFunction> const& model);
 
   public:
    explicit ConstraintCollector(storm::models::sparse::Model<storm::RationalFunction> const& model);

    ConstraintSet const& getWellformedConstraints() const;

    ConstraintSet const& getGraphPreservingConstraints() const;

    std::set<storm::RationalFunctionVariable> const& getVariables() const;

    void operator()(storm::models::sparse::Model<storm::RationalFunction> const& model);
};
 
}  // namespace analysis
}  // namespace storm