OrderedAssignments.h

Go to the documentation of this file.

#pragma once
 
#include "storm/adapters/DereferenceIteratorAdapter.h"
 
#include "storm/storage/jani/Assignment.h"
 
namespace storm {
namespace jani {
 
class VariableSet;
 
namespace detail {
using Assignments = storm::adapters::DereferenceIteratorAdapter<std::vector<std::shared_ptr<Assignment>>>;
using ConstAssignments = storm::adapters::DereferenceIteratorAdapter<std::vector<std::shared_ptr<Assignment>> const>;
}  // namespace detail
 
class OrderedAssignments {
   public:
    OrderedAssignments(std::vector<Assignment> const& assignments = std::vector<Assignment>());
 
    explicit OrderedAssignments(Assignment const& assignment);
 
    bool add(Assignment const& assignment, bool addToExisting = false);
 
    bool remove(Assignment const& assignment);
 
    bool hasMultipleLevels(bool onlyTransient = false) const;
 
    OrderedAssignments simplifyLevels(bool synchronous, VariableSet const& localVars, bool first = true) const;
 
    bool empty(bool onlyTransient = false) const;
 
    void clear();
 
    std::size_t getNumberOfAssignments() const;
 
    int64_t getLowestLevel(bool onlyTransient = false) const;
 
    int64_t getHighestLevel(bool onlyTransient = false) const;
 
    bool contains(Assignment const& assignment) const;
 
    detail::ConstAssignments getAllAssignments() const;
 
    detail::ConstAssignments getTransientAssignments() const;
 
    detail::ConstAssignments getTransientAssignments(int64_t assignmentLevel) const;
 
    detail::ConstAssignments getNonTransientAssignments() const;
 
    detail::ConstAssignments getNonTransientAssignments(int64_t assignmentLevel) const;
 
    bool hasTransientAssignment() const;
 
    detail::Assignments::iterator begin();
 
    detail::ConstAssignments::iterator begin() const;
 
    detail::Assignments::iterator end();
 
    detail::ConstAssignments::iterator end() const;
 
    void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution, bool const substituteTranscendentalNumbers);
 
    void changeAssignmentVariables(std::map<Variable const*, std::reference_wrapper<Variable const>> const& remapping);
 
    bool areLinear() const;
 
    friend std::ostream& operator<<(std::ostream& stream, OrderedAssignments const& assignments);
 
    OrderedAssignments clone() const;
 
    bool checkOrder() const;
 
   private:
    uint64_t isReadBeforeAssignment(LValue const& lValue, uint64_t assignmentNumber, uint64_t start = 0) const;
    uint64_t isWrittenBeforeAssignment(LValue const& LValue, uint64_t assignmentNumber, uint64_t start = 0) const;
 
    uint64_t upperBound(int64_t index) const;
 
    static std::vector<std::shared_ptr<Assignment>>::const_iterator lowerBound(Assignment const& assignment,
                                                                               std::vector<std::shared_ptr<Assignment>> const& assignments);
 
    // The vectors to store the assignments. These need to be ordered at all times.
    std::vector<std::shared_ptr<Assignment>> allAssignments;
    std::vector<std::shared_ptr<Assignment>> transientAssignments;
    std::vector<std::shared_ptr<Assignment>> nonTransientAssignments;
};
 
}  // namespace jani
}  // namespace storm