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* topStates, storm::storage::BitVector* 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();
 
    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 setDoneBuilding(bool done = true);
 
    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;
 
   protected:
    storage::Decomposition<storage::StronglyConnectedComponent> getDecomposition() const;
 
   private:
    bool above(Node* node1, Node* node2);
 
    bool above(Node* node1, Node* node2, storm::analysis::Order::Node* nodePrev, storm::storage::BitVector* statesSeen);
 
    bool aboveFast(Node* node1, Node* node2) const;
 
    void init(uint_fast64_t numberOfStates, storage::Decomposition<storage::StronglyConnectedComponent>, bool doneBuilding = false);
 
    std::string nodeName(Node n) const;
 
    std::string nodeLabel(Node n) const;
 
    bool invalid;
 
    void nodeOutput();
 
    bool doneBuilding;
 
    bool onlyBottomTopOrder;
 
    storm::storage::BitVector doneStates;
    storm::storage::BitVector trivialStates;
 
    std::vector<Node*> nodes;
 
    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