From 4243537fd39923665f0db1354a1c5c2404a7e7cd Mon Sep 17 00:00:00 2001
From: Jaime Arias <arias@lipn.univ-paris13.fr>
Date: Mon, 30 Dec 2024 20:39:01 +0100
Subject: [PATCH] refactor: petri_net_sog
---
src/aggregate.hpp | 14 ++++++++++++-
src/petri_net_sog.cpp | 49 +++++++++++++++++++++----------------------
src/petri_net_sog.hpp | 26 +++++++++++++++++------
src/sog.cpp | 18 ++++++++--------
4 files changed, 66 insertions(+), 41 deletions(-)
diff --git a/src/aggregate.hpp b/src/aggregate.hpp
index a1a4076..123a258 100644
--- a/src/aggregate.hpp
+++ b/src/aggregate.hpp
@@ -30,7 +30,7 @@ class Aggregate {
/**
* BDD of the aggregate
*/
- bdd state;
+ bdd bdd_state;
/*
* Input transitions of the aggregate
*/
@@ -48,32 +48,44 @@ class Aggregate {
/**
* 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;
diff --git a/src/petri_net_sog.cpp b/src/petri_net_sog.cpp
index 62fd8f7..966026b 100644
--- a/src/petri_net_sog.cpp
+++ b/src/petri_net_sog.cpp
@@ -257,14 +257,12 @@ bdd PetriNetSOG::AccessibleEpsilon(const bdd &from) const {
return m2;
}
-/* Computes the bdd obtaine by one step backward in the aggregate from a subset
- * 'from'*/
bdd PetriNetSOG::OneStepBackUnobs(const bdd &from,
const Aggregate *aggr) const {
bdd res = bdd_false();
for (const auto t : non_observables) {
- bdd pred = relation[t][from] & aggr->state;
+ bdd pred = relation[t][from] & aggr->bdd_state;
res = res | pred;
}
@@ -279,7 +277,7 @@ pair<int, bdd> PetriNetSOG::StepBackward(const bdd &from,
bdd succ = relation[t][from];
// function that returns the preceding bdd with the transition t
- if ((succ != bdd_false()) & ((succ &= aggr->state) != bdd_false())) {
+ if ((succ != bdd_false()) & ((succ &= aggr->bdd_state) != bdd_false())) {
res.first = t;
res.second = succ;
break;
@@ -305,12 +303,10 @@ Set PetriNetSOG::FirableObservableTrans(const bdd &from) const {
return res;
}
-// computes the weight (lengthtof ihe shortest path) f we enter the aggregate
-// with the input transition in and we leave it by output transition out
-int PetriNetSOG::ComputeSingleWeight(Aggregate *aggr, const int in,
+int PetriNetSOG::ComputeSingleWeight(const Aggregate *aggr, const int in,
const int out) const {
- bdd source = SearchExitPoints(aggr->state, out);
- const bdd dest = relation[in][(aggr->GetPredecessorsOfTrans(in))->state];
+ bdd source = SearchExitPoints(aggr->bdd_state, out);
+ const bdd dest = relation[in][(aggr->GetPredecessorsOfTrans(in))->bdd_state];
// backtracking from t_target until t_source
int counter = 0;
@@ -318,25 +314,28 @@ int PetriNetSOG::ComputeSingleWeight(Aggregate *aggr, const int in,
source = OneStepBackUnobs(source, aggr);
counter++;
}
+
return counter;
}
-/* 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->columns;
- for (int out : col) {
- r.push_back(ComputeSingleWeight(a, in, out));
+void PetriNetSOG::ComputeRowWeight(const int in, Aggregate *a) const {
+ std::vector<int> row;
+ row.reserve(a->columns.size()); // Preallocates memory for n elements
+
+ for (const int out : a->columns) {
+ row.push_back(ComputeSingleWeight(a, in, out));
}
- a->AddWeightRow(in, r);
+
+ a->AddWeightRow(in, row);
}
-void PetriNetSOG::GenerateSOG(SOG &sog) {
+
+void PetriNetSOG::GenerateSOG(SOG &sog) const {
Stack st;
// construction of the first aggregate
auto *new_aggregate = new Aggregate;
const bdd complete_aggr = AccessibleEpsilon(m0);
- new_aggregate->state = complete_aggr;
+ new_aggregate->bdd_state = complete_aggr;
sog.set_initial_state(new_aggregate);
sog.AddState(new_aggregate);
@@ -361,8 +360,8 @@ void PetriNetSOG::GenerateSOG(SOG &sog) {
auto *succ_aggr = new Aggregate;
const bdd complete_succ_aggr =
- AccessibleEpsilon(GetSuccessor(curr_aggr.aggregate->state, t));
- succ_aggr->state = complete_succ_aggr;
+ AccessibleEpsilon(GetSuccessor(curr_aggr.aggregate->bdd_state, t));
+ succ_aggr->bdd_state = complete_succ_aggr;
Aggregate *pos = sog.FindState(succ_aggr);
@@ -405,7 +404,7 @@ Paths PetriNetSOG::ObservablePaths(SOG &sog, map<int, int> trans_obs) const {
auto *c = new Aggregate;
{
const bdd complete_aggr = AccessibleEpsilon(m0);
- c->state = complete_aggr;
+ c->bdd_state = complete_aggr;
firable_trans = FirableObservableTrans(complete_aggr);
st.emplace(c, firable_trans);
@@ -453,8 +452,8 @@ Paths PetriNetSOG::ObservablePaths(SOG &sog, map<int, int> trans_obs) const {
{
auto *reached_aggr = new Aggregate;
bdd complete_aggr =
- AccessibleEpsilon(GetSuccessor(elt.aggregate->state, t));
- reached_aggr->state = complete_aggr;
+ AccessibleEpsilon(GetSuccessor(elt.aggregate->bdd_state, t));
+ reached_aggr->bdd_state = complete_aggr;
Aggregate *pos = sog.FindState(reached_aggr);
// if aggregate does not exist in the sog
@@ -511,7 +510,7 @@ stack<AggrPair> PetriNetSOG::SearchEntryPoints(Path path,
for (auto k = path.begin(); k != path.end() - 1; ++k) {
const int t = *k;
- entree = relation[t](p.first->state);
+ entree = relation[t](p.first->bdd_state);
p.second = entree;
for (const auto &succ : agr->successors) {
@@ -547,7 +546,7 @@ Path PetriNetSOG::AbstractPath(Path path, const SOG &sog) const {
const bdd target = entry_aggr.second;
source =
- flag ? relation[trans][source] : SearchExitPoints(aggr->state, trans);
+ flag ? relation[trans][source] : SearchExitPoints(aggr->bdd_state, trans);
Path path_aggregate = SubPathAggregate(&source, target, aggr);
abstract_paths.insert(abstract_paths.begin(), trans);
diff --git a/src/petri_net_sog.hpp b/src/petri_net_sog.hpp
index 3be78ab..7731fbe 100644
--- a/src/petri_net_sog.hpp
+++ b/src/petri_net_sog.hpp
@@ -89,16 +89,30 @@ class PetriNetSOG {
~PetriNetSOG() = default;
/**
- * Compute the bdd obtained by a single bacward step inside the aggregate
- * @param from : starting subset oif state
- * @param t transition identifier
+ * Compute the bdd obtained by a single backward step inside the aggregate
+ * @param from starting subset oif state
+ * @param aggr transition identifier
* @return the set of reached states by a step backward
*/
bdd OneStepBackUnobs(const bdd& from, const Aggregate* aggr) const;
- void computeRowWeight(const int in, Aggregate* a);
+ /**
+ * Compute one row of the weight matrix corresponding to the input transition
+ * @param in input transition
+ * @param a aggregate
+ */
+ void ComputeRowWeight(int in, Aggregate* a) const;
+
+ /**
+ * Computes the weight (length of the shortest path) if we enter the aggregate
+ * with the input transition in and we leave it by output transition out
+ * @param aggr aggregate
+ * @param in input transition
+ * @param out output transition
+ * @return the weight
+ */
+ int ComputeSingleWeight(const Aggregate* aggr, int in, int out) const;
- int ComputeSingleWeight(Aggregate* aggr, const int in, const int out) const;
/**
* Transitive closure on unobserved transitions
* @param from marking from which the closure is computed
@@ -134,7 +148,7 @@ class PetriNetSOG {
* Generate the SOG graph
* @param [out] sog SOG graph
*/
- void GenerateSOG(SOG& sog);
+ void GenerateSOG(SOG& sog) const;
/**
* Compute the aggregates traversed along the observable path, each
diff --git a/src/sog.cpp b/src/sog.cpp
index 7af34fa..a50d032 100644
--- a/src/sog.cpp
+++ b/src/sog.cpp
@@ -12,7 +12,7 @@ void SOG::set_initial_state(Aggregate *state) {
Aggregate *SOG::FindState(const Aggregate *state) const {
for (auto *aggr : states) {
- if (state->state.id() == aggr->state.id()) {
+ if (state->bdd_state.id() == aggr->bdd_state.id()) {
return aggr;
}
}
@@ -27,9 +27,9 @@ void SOG::AddState(Aggregate *state) {
int SOG::NbBddNode(Aggregate *state, size_t counter) {
if (!state->visited) {
- bdd_tab[counter - 1] = state->state;
+ bdd_tab[counter - 1] = state->bdd_state;
state->visited = true;
- int nb_bdd = bdd_nodecount(state->state);
+ int nb_bdd = bdd_nodecount(state->bdd_state);
for (const auto &successor : state->successors) {
if (!successor.state->visited) {
counter++;
@@ -99,12 +99,12 @@ void SOG::ExportGraphToDotFile(const std::string &filename) const {
// Add the initial node (start point)
file << " start [shape=point, width=0];\n\n";
- file << " start -> ag_" << initial_state->state.id() << ";\n";
+ file << " start -> ag_" << initial_state->bdd_state.id() << ";\n";
for (const auto *aggr : states) {
for (const auto &edge : aggr->successors) {
- file << " ag_" << aggr->state.id() << " -> "
- << "ag_" << edge.state->state.id() << " [ label = \"t"
+ file << " ag_" << aggr->bdd_state.id() << " -> "
+ << "ag_" << edge.state->bdd_state.id() << " [ label = \"t"
<< edge.transition + 1 << "\"];" << '\n';
}
}
@@ -114,7 +114,7 @@ void SOG::ExportGraphToDotFile(const std::string &filename) const {
}
void SOG::PrintSuccessors(const Aggregate *state) const {
- std::cout << bddtable << state->state << '\n';
+ std::cout << bddtable << state->bdd_state << '\n';
std::cout << "\n\tIts successors are ( " << state->successors.size()
<< " ):\n\n";
@@ -122,7 +122,7 @@ void SOG::PrintSuccessors(const Aggregate *state) const {
for (const auto &successor : state->successors) {
std::cout << " \t- t" << successor.transition << " -> " << bddtable
- << successor.state->state << '\n';
+ << successor.state->bdd_state << '\n';
getchar();
}
}
@@ -140,7 +140,7 @@ void SOG::PrintPredecessors(const Aggregate *state) const {
for (const auto &predecessor : state->predecessors) {
std::cout << " \t- t" << predecessor.transition << " ->" << bddtable
- << predecessor.state->state << '\n';
+ << predecessor.state->bdd_state << '\n';
getchar();
}
}
--
GitLab