Order.h

Go to the documentation of this file.

#pragma once
 
#include <boost/container/flat_set.hpp>
#include <iostream>
#include <memory>
#include <vector>
 
#include "storm/storage/BitVector.h"
#include "storm/storage/StronglyConnectedComponent.h"
 
namespace storm {
namespace analysis {
class Order {
   public:
    enum NodeComparison {
        UNKNOWN,
        BELOW,
        ABOVE,
        SAME,
    };

    struct Node {
        boost::container::flat_set<uint_fast64_t> states;
        storm::storage::BitVector statesAbove;
    };

    Order(storm::storage::BitVector const& topStates, storm::storage::BitVector const& bottomStates, uint_fast64_t numberOfStates,
          storage::Decomposition<storage::StronglyConnectedComponent> sccsSorted, std::vector<uint_fast64_t> statesSorted);

    Order(uint_fast64_t top, uint_fast64_t bottom, uint_fast64_t numberOfStates, storage::Decomposition<storage::StronglyConnectedComponent> sccsSorted,
          std::vector<uint_fast64_t> statesSorted);

    Order();

    Order(Order const& other);
 
    Order(Order&&) noexcept = default;
 
    Order& operator=(Order other);
 
    friend void swap(Order& first, Order& second) noexcept;

    void add(uint_fast64_t state);

    void addAbove(uint_fast64_t state, Node* node);

    void addBelow(uint_fast64_t state, Node* node);

    void addBetween(uint_fast64_t state, Node* node1, Node* node2);

    void addBetween(uint_fast64_t state, uint_fast64_t above, uint_fast64_t below);

    void addRelationNodes(storm::analysis::Order::Node* above, storm::analysis::Order::Node* below, bool allowMerge = false);

    void addRelation(uint_fast64_t above, uint_fast64_t below, bool allowMerge = false);

    void addToNode(uint_fast64_t state, Node* node);

    bool mergeNodes(Node* node1, Node* node2);

    bool merge(uint_fast64_t var1, uint_fast64_t var2);

    Order::NodeComparison compare(uint_fast64_t state1, uint_fast64_t state2, NodeComparison hypothesis = UNKNOWN);
    Order::NodeComparison compareFast(uint_fast64_t state1, uint_fast64_t state2, NodeComparison hypothesis = UNKNOWN) const;

    NodeComparison compare(Node* node1, Node* node2, NodeComparison hypothesis = UNKNOWN);
    NodeComparison compareFast(Node* node1, Node* node2, NodeComparison hypothesis = UNKNOWN) const;

    bool contains(uint_fast64_t state) const;

    Node* getBottom() const;

    bool getDoneBuilding() const;

    uint_fast64_t getNextDoneState(uint_fast64_t state) const;
 
    uint_fast64_t getNumberOfDoneStates() const;

    Node* getNode(uint_fast64_t state) const;

    std::vector<Node*> getNodes() const;
 
    std::vector<uint_fast64_t>& getStatesSorted();
    Node* getTop() const;

    uint_fast64_t getNumberOfAddedStates() const;

    uint_fast64_t getNumberOfStates() const;

    bool isBottomState(uint_fast64_t) const;

    bool isTopState(uint_fast64_t) const;

    bool isOnlyBottomTopOrder() const;

    std::vector<uint_fast64_t> sortStates(std::vector<uint_fast64_t>* states);
    std::pair<bool, bool> allAboveBelow(std::vector<uint_fast64_t> const states, uint_fast64_t state);

    std::pair<std::pair<uint_fast64_t, uint_fast64_t>, std::vector<uint_fast64_t>> sortStatesForForward(uint_fast64_t currentState,
                                                                                                        std::vector<uint_fast64_t> const& successors);

    std::pair<std::pair<uint_fast64_t, uint_fast64_t>, std::vector<uint_fast64_t>> sortStatesUnorderedPair(const std::vector<uint_fast64_t>* states);

    std::vector<uint_fast64_t> sortStates(storm::storage::BitVector* states);
 
    bool isTrivial(uint_fast64_t state);
    std::pair<uint_fast64_t, bool> getNextStateNumber();
 
    //                    bool existsNextSCC();
    bool existsNextState();
    bool existsStateToHandle();
 
    std::pair<uint_fast64_t, bool> getStateToHandle();
 
    void addStateToHandle(uint_fast64_t state);
    void addStateSorted(uint_fast64_t state);

    void toDotOutput() const;

    void dotOutputToFile(std::ofstream& dotOutfile) const;

    std::shared_ptr<Order> copy() const;
    //                    void setAddedSCC(uint_fast64_t sccNumber);
    void setDoneState(uint_fast64_t sccNumber);
 
    bool isInvalid() const;
 
   private:
    bool above(Node* node1, Node* node2);
 
    bool aboveFast(Node* node1, Node* node2) const;
 
    void init(uint_fast64_t numberOfStates, storage::Decomposition<storage::StronglyConnectedComponent>, bool doneBuilding = false);

    Node* allocateNode();
 
    std::string nodeName(Node n) const;
 
    std::string nodeLabel(Node n) const;
 
    bool invalid;
 
    bool doneBuilding;
 
    bool onlyBottomTopOrder;
 
    storm::storage::BitVector doneStates;
    storm::storage::BitVector trivialStates;
 
    std::vector<Node*> nodes;
 
    // Sole owner of every Node allocated for this Order; `nodes`, `top` and `bottom` are
    // non-owning observer pointers into this storage.
    std::vector<std::unique_ptr<Node>> nodeStorage;
 
    std::vector<uint_fast64_t> statesToHandle;
 
    Node* top;
 
    Node* bottom;
 
    uint_fast64_t numberOfStates;
 
    uint_fast64_t numberOfAddedStates;
 
    std::vector<uint_fast64_t> statesSorted;
};
}  // namespace analysis
}  // namespace storm