aggregate.hpp

#ifndef AGGREGATE_H_
#define AGGREGATE_H_

#include <set>
#include <vector>

#include "bdd.h"

// definition of types
class Aggregate;
struct Edge {
  Aggregate* state;  // pointer to an state
  int transition;    // identifier of the transition
  Edge(Aggregate* s, int t) : state(s), transition(t) {}  // constructor
};
typedef std::vector<Edge> Edges;

class Aggregate {
 public:
  /**
   * Constructor
   */
  Aggregate() = default;

  /**
   * Destructor
   */
  ~Aggregate() = default;

  /**
   * BDD of the aggregate
   */
  bdd bdd_state;
  /*
   * Input transitions of the aggregate
   */
  std::vector<int> rows;

  /**
   * Output transitions of the aggregate
   */
  std::vector<int> columns;

  /*
   * Matrix representing the weights of the shortest paths inside the aggregate
   */
  std::vector<std::vector<int>> weight;

  /**
   * Initialize the columns with the output transitions
   * @param  output_trans set of output transitions
   */
  void InitWeightColumns(const std::set<int>& output_trans);

  /**
   * Add a row corresponding to a given input transition (in) to the matrix of
   * weight
   * @param in input transition
   * @param weight_row row of weights
   * */
  void AddWeightRow(int in, const std::vector<int>& weight_row);

  /**
   * Return the position of transition t in output transitions vector
   * @param t transition identifier
   * @return the position of the transition
   */
  int PosTransOutWeight(int t) const;

  /**
   * Gives the position of transition t in input transitions vector
   * @param t transition identifier
   * @return the position of the transition
   */
  int PosTransInWeight(int t) const;

  /**
   * Gives the weight for a given pair of input and output transition
   * @param in input transition
   * @param out output transition
   * @return the weight of the pair of transitions
   */
  int WeightInOut(int in, int out) const;

  /**
   * Return the predecessor of the aggregate by a given transition
   * @param t transition identifier
   * @return the predecessor of the aggregate
   */
  Aggregate* GetPredecessorsOfTrans(int t) const;

    /**
     * Return the successor of the aggregate by a given transition
     * @param t transition identifier
     * @return the predecessor of the aggregate
     */
    Aggregate* GetsuccessorsOfTrans(int t) const;

  /**
   * Flag to indicate if the state was visited
   */
  bool visited{false};

  /**
   * Set of predecessors edges
   */
  Edges predecessors;

  /**
   * Set of successors edges
   */
  Edges successors;
};

#endif  // AGGREGATE_H_