MonotonicityResult.h

Go to the documentation of this file.

#pragma once
 
#include <map>
#include <memory>
#include <ostream>
#include <set>
 
#include "storm-pars/modelchecker/region/monotonicity/MonotonicityKind.h"
#include "storm/storage/BitVector.h"
 
namespace storm {
namespace analysis {
template<typename VariableType>
class MonotonicityResult {
   public:
    using Monotonicity = storm::analysis::MonotonicityKind;
 
    MonotonicityResult();
 
    void addMonotonicityResult(VariableType var, Monotonicity mon);
 
    void updateMonotonicityResult(VariableType var, Monotonicity mon, bool force = false);
 
    Monotonicity getMonotonicity(VariableType var) const;
    bool isMonotone(VariableType var) const;
 
    std::map<VariableType, Monotonicity> const& getMonotonicityResult() const;
 
    void splitBasedOnMonotonicity(std::set<VariableType> const& consideredVariables, std::set<VariableType>& monotoneIncr, std::set<VariableType>& monotoneDecr,
                                  std::set<VariableType>& notMontone) const;
 
    std::pair<std::set<VariableType>, std::set<VariableType>> splitVariables(std::set<VariableType> const& consideredVariables) const;
    std::string toString() const;
 
    bool isDone() const;
 
    bool isDoneForVar(VariableType) const;
 
    bool existsMonotonicity();
 
    bool isAllMonotonicity() const;
 
    void setDone(bool done = true);
 
    void setSomewhereMonotonicity(bool done = true);
 
    void setAllMonotonicity(bool done = true);
 
    void setDoneForVar(VariableType);
 
    void setDoneVariables(std::set<VariableType> doneVariables);
 
    std::shared_ptr<MonotonicityResult<VariableType>> copy() const;
 
   private:
    std::map<VariableType, Monotonicity> monotonicityResult;
    std::set<VariableType> doneVariables;
    bool done;
    bool somewhereMonotonicity;
    bool allMonotonicity;
};
 
}  // namespace analysis
}  // namespace storm