Skip to content
Snippets Groups Projects
Commit edcc0c0d authored by Jaime Arias's avatar Jaime Arias
Browse files

refactor: some refactorings

parent c63df5be
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/petri_net_sog.cpp
+ 70
− 64
View file @ edcc0c0d
......@@ -68,20 +68,23 @@ void ReinitCycle(const vector<int> &sw, map<int, int> &trans_obs) {
/*****************************************************************************/
/* Class Trans */
/*****************************************************************************/
Trans::Trans(const bdd &v, bddPair *p, const bdd &r, const bdd &pr,
const bdd &pre, const bdd &post)
: var(v), pair(p), precond(pre), postcond(post), rel(r), prerel(pr) {}
Trans::Trans(const bdd &var, bddPair *pairs_table, const bdd &postrel,
const bdd &prerel, const bdd &precond, const bdd &postcond)
: var(var),
pairs_table(pairs_table),
precond(precond),
postcond(postcond),
postrel(postrel),
prerel(prerel) {}
bdd Trans::operator()(const bdd &op) const {
bdd res = bdd_relprod(op, rel, var);
res = bdd_replace(res, pair);
return res;
const bdd res = bdd_relprod(op, postrel, var);
return bdd_replace(res, pairs_table);
}
bdd Trans::operator[](const bdd &op) const {
bdd res = bdd_relprod(op, prerel, var);
res = bdd_replace(res, pair);
return res;
const bdd res = bdd_relprod(op, prerel, var);
return bdd_replace(res, pairs_table);
}
/*****************************************************************************/
......@@ -94,10 +97,10 @@ PetriNetSOG::PetriNetSOG(const net &petri_net, const map<int, int> &obs_trans,
auto vp = new bvec[nb_places];
// pre and post conditions of the transitions
auto prec = new bvec[nb_places];
auto postc = new bvec[nb_places];
auto pre_arc = new bvec[nb_places];
auto post_arc = new bvec[nb_places];
auto idv = new int[nb_places];
auto id_var = new int[nb_places];
auto idvp = new int[nb_places];
// number of bdd variables used for each place
......@@ -143,11 +146,11 @@ PetriNetSOG::PetriNetSOG(const net &petri_net, const map<int, int> &obs_trans,
}
// initialize the bdd variables
for (int i = 0; i < nb_places; i++) {
int var = 2 * i;
nb_bdd_vars[i] = fdd_varnum(var);
bvec_vars[i] = bvec_varfdd(var);
vp[i] = bvec_varfdd(var + 1);
for (int p = 0; p < nb_places; p++) {
int var = 2 * p;
nb_bdd_vars[p] = fdd_varnum(var);
bvec_vars[p] = bvec_varfdd(var);
vp[p] = bvec_varfdd(var + 1);
}
// initial marking
......@@ -161,85 +164,88 @@ PetriNetSOG::PetriNetSOG(const net &petri_net, const map<int, int> &obs_trans,
/* Transition relation */
for (auto t = petri_net.transitions.begin(); t != petri_net.transitions.end();
++t) {
bdd rel = bdd_true();
bdd postrel = bdd_true();
bdd var = bdd_true();
bdd prerel = bdd_true();
bdd precond = bdd_true();
bdd postcond = bdd_true();
bddPair *p = bdd_newpair();
for (int i = 0; i < nb_places; i++) {
prec[i] = bvec_con(nb_bdd_vars[i], 0);
postc[i] = bvec_con(nb_bdd_vars[i], 0);
// initialize the pre adn post arcs vectors with 0
for (int p = 0; p < nb_places; p++) {
pre_arc[p] = bvec_con(nb_bdd_vars[p], 0);
post_arc[p] = bvec_con(nb_bdd_vars[p], 0);
}
// arcs pre
set<int> adjacent_places;
// pre arcs
Set adjacent_places;
for (auto it = t->pre.begin(); it != t->pre.end(); ++it) {
adjacent_places.insert(it->first);
prec[it->first] =
prec[it->first] + bvec_con(nb_bdd_vars[it->first], it->second);
int place = it->first;
adjacent_places.insert(place);
pre_arc[place] =
pre_arc[place] + bvec_con(nb_bdd_vars[place], it->second);
}
// arcs post
// post arcs
for (auto it = t->post.begin(); it != t->post.end(); ++it) {
adjacent_places.insert(it->first);
postc[it->first] =
postc[it->first] + bvec_con(nb_bdd_vars[it->first], it->second);
int place = it->first;
adjacent_places.insert(place);
post_arc[place] =
post_arc[place] + bvec_con(nb_bdd_vars[place], it->second);
}
int np = 0;
for (const auto adjacent_place : adjacent_places) {
idv[np] = 2 * adjacent_place;
idvp[np] = 2 * adjacent_place + 1;
var = var & fdd_ithset(2 * adjacent_place);
int nb_pairs = 0;
for (const auto place : adjacent_places) {
id_var[nb_pairs] = 2 * place;
idvp[nb_pairs] = 2 * place + 1;
var = var & fdd_ithset(2 * place);
// image
// precondition
rel = rel & (bvec_vars[adjacent_place] >= prec[adjacent_place]);
precond = precond & (bvec_vars[adjacent_place] >= prec[adjacent_place]);
postrel = postrel & (bvec_vars[place] >= pre_arc[place]);
precond = precond & (bvec_vars[place] >= pre_arc[place]);
// postcondition
rel = rel & (vp[adjacent_place] ==
(bvec_vars[adjacent_place] - prec[adjacent_place] +
postc[adjacent_place]));
postrel =
postrel &
(vp[place] == (bvec_vars[place] - pre_arc[place] + post_arc[place]));
// pre-image
// precondition
prerel = prerel & (bvec_vars[adjacent_place] >= postc[adjacent_place]);
prerel = prerel & (bvec_vars[place] >= post_arc[place]);
// postcondition
postcond =
postcond & (bvec_vars[adjacent_place] >= postc[adjacent_place]);
prerel = prerel & (vp[adjacent_place] ==
(bvec_vars[adjacent_place] - postc[adjacent_place] +
prec[adjacent_place]));
postcond = postcond & (bvec_vars[place] >= post_arc[place]);
prerel = prerel & (vp[place] ==
(bvec_vars[place] - post_arc[place] + pre_arc[place]));
// capacity
if (petri_net.places[adjacent_place].hasCapacity()) {
rel = rel & (vp[adjacent_place] <=
bvec_con(nb_bdd_vars[adjacent_place],
petri_net.places[adjacent_place].capacity));
if (petri_net.places[place].hasCapacity()) {
postrel =
postrel & (vp[place] <= bvec_con(nb_bdd_vars[place],
petri_net.places[place].capacity));
}
np++;
nb_pairs++;
}
fdd_setpairs(p, idvp, idv, np);
relation.emplace_back(var, p, rel, prerel, precond, postcond);
// variable pairs are used in bdd_replace to define which variables to
// replace with other variables.
bddPair *vars_pair_table = bdd_newpair();
fdd_setpairs(vars_pair_table, idvp, id_var, nb_pairs);
relation.emplace_back(var, vars_pair_table, postrel, prerel, precond,
postcond);
}
// remove vectors
delete[] bvec_vars;
delete[] vp;
delete[] prec;
delete[] postc;
delete[] idv;
delete[] pre_arc;
delete[] post_arc;
delete[] id_var;
delete[] idvp;
delete[] nb_bdd_vars;
}
bdd PetriNetSOG::AccessibleEpsilon(const bdd &from_s) const {
bdd PetriNetSOG::AccessibleEpsilon(const bdd &from) const {
bdd m1;
bdd m2 = from_s;
bdd m2 = from;
do {
m1 = m2;
......@@ -273,12 +279,12 @@ bdd PetriNetSOG::GetSuccessor(const bdd &from, const int t) const {
return relation[t](from);
}
Set PetriNetSOG::FirableObservableTrans(const bdd &state) const {
Set PetriNetSOG::FirableObservableTrans(const bdd &from) const {
Set res;
for (int i : observables) {
if (relation[i](state) != bddfalse) {
res.insert(i);
for (int t : observables) {
if (relation[t](from) != bddfalse) {
res.insert(t);
}
}
......
src/petri_net_sog.hpp
+ 12
− 7
View file @ edcc0c0d
......@@ -41,10 +41,10 @@ class Trans {
bdd operator[](const bdd& op) const;
bdd var;
bddPair* pair;
bddPair* pairs_table;
bdd precond;
bdd postcond;
bdd rel;
bdd postrel;
bdd prerel;
};
......@@ -90,12 +90,17 @@ class PetriNetSOG {
/**
* Transitive closure on unobserved transitions
* @param from_s state from which the closure is computed
* @param from marking from which the closure is computed
* @return the set of reached states
*/
bdd AccessibleEpsilon(const bdd& from_s) const;
bdd AccessibleEpsilon(const bdd& from) const;
// step backward
/**
*
* @param from marking from which the backward step is computed
* @param aggr aggregate from which the backward step is computed
* @return
*/
std::pair<int, bdd> StepBackward(const bdd& from,
const Aggregate* aggr) const;
......@@ -109,10 +114,10 @@ class PetriNetSOG {
/**
* Return the set of observable transitions that are firable from a state
* @param state state from which the firable transitions are computed
* @param from state from which the firable transitions are computed
* @return the set of firable transitions
*/
Set FirableObservableTrans(const bdd& state) const;
Set FirableObservableTrans(const bdd& from) const;
/**
* Extract observable paths. It constructs the SOG of the petri net model
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment