aggregate.hpp 2.51 KiB
#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_