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

refactor: set attributes to private

parent 03993c62
No related branches found
No related tags found
No related merge requests found
......@@ -5,7 +5,6 @@
#include <set>
#include <stack>
#include <string>
#include <utility>
#include <vector>
#include "Net.hpp"
......@@ -18,12 +17,14 @@ constexpr int BDD_INITIAL_NUM_NODES_ = 1000000;
constexpr int BDD_SIZE_CACHES = 1000000;
// TODO: why these global variables ?
bdd *tab_meta;
int nb_iter;
int it_ext, it_int;
int max_bdd_nodes;
bdd *tab_meta;
int nb_meta_state;
double old_size;
// vector of model's places for the print handler
const vector<Place> *v_places = nullptr;
/**
......@@ -93,14 +94,17 @@ bdd Trans::operator[](const bdd &op) const {
PetriNetSOG::PetriNetSOG(const net &petri_net, const map<int, int> &obs_trans,
Set non_obs_trans, const int bound, const bool init)
: nb_places(petri_net.places.size()) {
bvec *v = new bvec[nb_places];
bvec *vp = new bvec[nb_places];
bvec *prec = new bvec[nb_places];
bvec *postc = new bvec[nb_places];
auto v = new bvec[nb_places];
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 idv = new int[nb_places];
auto idvp = new int[nb_places];
int *idv = new int[nb_places];
int *idvp = new int[nb_places];
int *nbbit = new int[nb_places];
auto nbbit = new int[nb_places];
if (!init) {
bdd_init(BDD_INITIAL_NUM_NODES_, BDD_SIZE_CACHES);
......@@ -120,6 +124,7 @@ PetriNetSOG::PetriNetSOG(const net &petri_net, const map<int, int> &obs_trans,
transitions_names = petri_net.transitionName;
// create bdd variables for each model's place
int domain = 0;
for (const auto &place : petri_net.places) {
if (place.hasCapacity()) {
......@@ -134,7 +139,7 @@ PetriNetSOG::PetriNetSOG(const net &petri_net, const map<int, int> &obs_trans,
}
// bvec
current_var = bdd_true();
bdd current_var = bdd_true();
for (int i = 0; i < nb_places; i++) {
nbbit[i] = fdd_varnum(2 * i);
v[i] = bvec_varfdd(2 * i);
......
......@@ -10,8 +10,6 @@
// type definitions
typedef std::vector<int> Path;
// structures useful for the synchronised product of n observation graphs.
typedef pair<Aggregate*, bdd> Couple;
typedef pair<Couple, Set> StackElt;
typedef stack<StackElt> Stack;
......@@ -45,18 +43,38 @@ class Trans {
class PetriNetSOG {
private:
// number of places of the petri net model
size_t nb_places;
// transitions of the petri net model
std::vector<Transition> transitions;
// Set of observable transitions of the petri net model
Set observables;
// Set of non observable transitions of the petri net model
Set non_observables;
// Mapping from transition names to their identifiers
std::map<std::string, int> transitions_names;
size_t nb_places;
public:
// initial marking
bdd m0;
bdd current_var;
// SOG transitions
std::vector<Trans> relation;
public:
/**
*
* @param obs_trans observable transitions
* @param non_obs_trans non observable transitions
* @param bound bound of the model's places (i.e., max number of tokens)
* @param init
*
* TODO: why observable transitions is a map and non observable transitions is
* a set?
*/
PetriNetSOG(const net&, const map<int, int>& obs_trans, Set non_obs_trans,
int bound = 32, bool init = false);
~PetriNetSOG() = default;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment