LocalMonotonicityResult.h

Go to the documentation of this file.

#pragma once
 
#include <vector>
 
#include "storm-pars/modelchecker/region/monotonicity/MonotonicityResult.h"
#include "storm/storage/BitVector.h"
 
namespace storm {
namespace analysis {
template<typename VariableType>
class LocalMonotonicityResult {
   public:
    typedef typename MonotonicityResult<VariableType>::Monotonicity Monotonicity;
 
    LocalMonotonicityResult(uint_fast64_t numberOfStates);
 
    LocalMonotonicityResult(std::shared_ptr<MonotonicityResult<VariableType>> globalResult, uint_fast64_t numberOfStates);
 
    Monotonicity getMonotonicity(uint_fast64_t state, VariableType var) const;
    std::shared_ptr<MonotonicityResult<VariableType>> getMonotonicity(uint_fast64_t state) const;
 
    void setMonotonicity(uint_fast64_t state, VariableType var, Monotonicity mon);
 
    std::shared_ptr<MonotonicityResult<VariableType>> getGlobalMonotonicityResult() const;
 
    std::shared_ptr<LocalMonotonicityResult<VariableType>> copy();
 
    bool isDone() const;
    void setDone(bool done = true);
 
    bool isNoMonotonicity() const;
 
    void setConstant(uint_fast64_t state);
 
    void setIndexMinimize(int index);
    void setIndexMaximize(int index);
    int getIndexMinimize() const;
    int getIndexMaximize() const;
 
    std::string toString() const;
 
    void setMonotoneIncreasing(VariableType var);
    void setMonotoneDecreasing(VariableType var);
 
    bool isFixedParametersSet() const;
 
   private:
    std::vector<std::shared_ptr<MonotonicityResult<VariableType>>> stateMonRes;
 
    std::shared_ptr<MonotonicityResult<VariableType>> globalMonotonicityResult;
 
    void setMonotonicityResult(uint_fast64_t state, std::shared_ptr<MonotonicityResult<VariableType>> monRes);
 
    void setGlobalMonotonicityResult(std::shared_ptr<MonotonicityResult<VariableType>> monRes);
 
    void setStatesMonotone(storm::storage::BitVector statesMonotone);
 
    storm::storage::BitVector statesMonotone;
    bool done;
 
    int indexMinimize = -1;
    int indexMaximize = -1;
    std::shared_ptr<MonotonicityResult<VariableType>> dummyPointer;
 
    bool setFixedParameters = false;
};
}  // namespace analysis
}  // namespace storm