diff --git a/src/aggregate.cpp b/src/aggregate.cpp
index 2609eec106467b465bb86bfaa5d2cb38f4d36705..c0a8ff5f0ab94683c9c35c7238a073b5abc2ce66 100644
--- a/src/aggregate.cpp
+++ b/src/aggregate.cpp
@@ -1,44 +1,48 @@
#include "aggregate.hpp"
-#include <iostream>
#include <map>
#include <set>
-#include <stack>
-#include <string>
#include <vector>
-void Aggregate::initWeightColumns(std::set<int> outputTrans) {
- for (int t : outputTrans) {
+
+void Aggregate::InitWeightColumns(const std::set<int>& output_trans) {
+ for (int t : output_trans) {
columns.push_back(t);
}
}
-void Aggregate::addRowWeight(const int in, const std::vector<int> weightRow) {
+
+void Aggregate::AddWeightRow(const int in, const std::vector<int>& weight_row) {
rows.push_back(in);
- weight.push_back(weightRow);
+ weight.push_back(weight_row);
}
-int Aggregate::posTransOutWeight(int t) {
- for (int i = 0; i < columns.size(); i++)
- if (columns[i] == t)
+int Aggregate::PosTransOutWeight(const int t) const {
+ for (int i = 0; i < columns.size(); i++) {
+ if (columns[i] == t) {
return i;
+ }
+ }
return -1;
}
-int Aggregate::posTransInWeight(int t) {
- for (int i = 0; i < rows.size(); i++)
- if (rows[i] == t)
+int Aggregate::PosTransInWeight(const int t) const {
+ for (int i = 0; i < rows.size(); i++) {
+ if (rows[i] == t) {
return i;
+ }
+ }
return -1;
}
-int Aggregate::weightInOut(int in, int out) {
- return weight[posTransInWeight(in)][posTransOutWeight(out)];
+int Aggregate::WeightInOut(const int in, const int out) const {
+ return weight[PosTransInWeight(in)][PosTransOutWeight(out)];
}
-Aggregate* Aggregate::predbytrans(const int t) const {
- for (Edge p : predecessors) {
+
+Aggregate* Aggregate::GetPredecessorsOfTrans(const int t) const {
+ for (const Edge p : predecessors) {
if (p.transition == t) {
return p.state;
}
}
return nullptr;
-}
\ No newline at end of file
+}
diff --git a/src/aggregate.hpp b/src/aggregate.hpp
index 6151a82d5f25aa126df2dd337fe95c59e2f3920f..a1a407621c06ea6be5d444e4afbda2026fa33800 100644
--- a/src/aggregate.hpp
+++ b/src/aggregate.hpp
@@ -31,49 +31,51 @@ class Aggregate {
* BDD of the aggregate
*/
bdd state;
+ /*
+ * Input transitions of the aggregate
+ */
+ std::vector<int> rows;
+
+ /**
+ * Output transitions of the aggregate
+ */
+ std::vector<int> columns;
- /* returns the bdd representing the aggregate */
- bdd getbddstate() const {
- return state;
- }
/*
* Matrix representing the weights of the shortest paths inside the aggregate
*/
- std::vector<int> rows; // input transitions of the aggregate
- std::vector<int> columns; // output transitions of the aggregate
std::vector<std::vector<int>> weight;
- /* returns the column of the output transitions */
- std::vector<int> getColumnsWeight() const {
- return columns;
- }
- /*initializes the columns with the output transitions*/
- void initWeightColumns(std::set<int>);
-
- /* adds a row corresponding to a given input transition (in) to the matrix of
- * weight*/
- /* rerns the tu*/ void addRowWeight(const int in, const std::vector<int> r);
- /* gives (int in, int out);the position of transition t in output
- * transitions vector
+
+ /**
+ * Initialize the columns with the output transitions
*/
- int posTransOutWeight(int t);
- /* gives the weight for a given pair of input and output transition */
- int weightInOut(int in, int out);
- /* gives the position of transition t in input transitions vector */
+ void InitWeightColumns(const std::set<int>& output_trans);
- int posTransInWeight(int t);
+ /**
+ * Add a row corresponding to a given input transition (in) to the matrix of
+ * weight
+ * */
+ void AddWeightRow(int in, const std::vector<int>& weight_row);
+
+ /**
+ * Return the position of transition t in output transitions vector
+ */
+ int PosTransOutWeight(int t) const;
- /*returns the predecessor of the aggregate by a given transition*/
- Aggregate* predbytrans(const int t) const;
+ /**
+ * Gives the position of transition t in input transitions vector
+ */
+ int PosTransInWeight(int t) const;
/**
- * Flag to indicate if the state loops using epsilon transitions
+ * Gives the weight for a given pair of input and output transition
*/
- bool loop{false};
+ int WeightInOut(int in, int out) const;
/**
- * Flag to indicate if there exists a blocking state
+ * Return the predecessor of the aggregate by a given transition
*/
- bool blocking{false};
+ Aggregate* GetPredecessorsOfTrans(int t) const;
/**
* Flag to indicate if the state was visited
diff --git a/src/petri_net_sog.cpp b/src/petri_net_sog.cpp
index ffbd644a39eb040237ddb2d0b6147dd91c03f8a2..62fd8f77c14c68f54f571b3a9bd37517611f2be0 100644
--- a/src/petri_net_sog.cpp
+++ b/src/petri_net_sog.cpp
@@ -310,7 +310,7 @@ Set PetriNetSOG::FirableObservableTrans(const bdd &from) const {
int PetriNetSOG::ComputeSingleWeight(Aggregate *aggr, const int in,
const int out) const {
bdd source = SearchExitPoints(aggr->state, out);
- const bdd dest = relation[in][(aggr->predbytrans(in))->getbddstate()];
+ const bdd dest = relation[in][(aggr->GetPredecessorsOfTrans(in))->state];
// backtracking from t_target until t_source
int counter = 0;
@@ -324,11 +324,11 @@ int PetriNetSOG::ComputeSingleWeight(Aggregate *aggr, const int in,
/* compute one raw of the weight matrix corresponding to the input transition */
void PetriNetSOG::computeRowWeight(const int in, Aggregate *a) {
std::vector<int> r;
- std::vector<int> col = a->getColumnsWeight();
+ std::vector<int> col = a->columns;
for (int out : col) {
r.push_back(ComputeSingleWeight(a, in, out));
}
- a->addRowWeight(in, r);
+ a->AddWeightRow(in, r);
}
void PetriNetSOG::GenerateSOG(SOG &sog) {
Stack st;
@@ -345,7 +345,7 @@ void PetriNetSOG::GenerateSOG(SOG &sog) {
Set firable_trans = FirableObservableTrans(complete_aggr);
// initialize the raws of Weight
- new_aggregate->initWeightColumns(firable_trans);
+ new_aggregate->InitWeightColumns(firable_trans);
st.emplace(new_aggregate, firable_trans);
while (!st.empty()) {
@@ -378,14 +378,16 @@ void PetriNetSOG::GenerateSOG(SOG &sog) {
st.emplace(succ_aggr, firable_trans);
// initialize the raws of Weight
- succ_aggr->initWeightColumns(firable_trans);
+ // succ_aggr->initWeightColumns(firable_trans);
+
// compute a row weight for the input transition t and add it to the
// succ aggregate
- computeRowWeight(t, succ_aggr);
+ // computeRowWeight(t, succ_aggr);
}
} else {
sog.AddArc(curr_aggr.aggregate, pos, t);
+ // computeRowWeight(t, pos);
delete succ_aggr;
}
}
diff --git a/src/sog.cpp b/src/sog.cpp
index 7e1f646cb9d8792f2eeae4ddce171542d4dd772c..7af34fa40ddbe825b540524e9243142bc3a35107 100644
--- a/src/sog.cpp
+++ b/src/sog.cpp
@@ -115,13 +115,6 @@ void SOG::ExportGraphToDotFile(const std::string &filename) const {
void SOG::PrintSuccessors(const Aggregate *state) const {
std::cout << bddtable << state->state << '\n';
- if (state->loop) {
- std::cout << "\n\tLooping with epsilon transitions\n";
- }
-
- if (state->blocking) {
- std::cout << "\n\tExisting a blocking state\n";
- }
std::cout << "\n\tIts successors are ( " << state->successors.size()
<< " ):\n\n";