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

refactor: remove modular_sog files

parent 74aafb1b
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/CMakeLists.txt
+ 0
− 1
View file @ b5f2eb40
......@@ -5,7 +5,6 @@ cmake_minimum_required(VERSION 3.5 FATAL_ERROR)
add_executable(sogMBT main.cpp
sog.cpp
petri_net_sog.cpp
modular_sog.cpp
)
# link libraries
......
src/modular_aggregate.hpp deleted 100644 → 0
+ 0
− 49
View file @ 74aafb1b
#ifndef MODULAR_AGGREGATE_H_
#define MODULAR_AGGREGATE_H_
#include <set>
#include <vector>
#include "bdd.h"
class ModularAggregate;
typedef std::pair<ModularAggregate *, std::string> ModularEdge;
// TODO: check this
struct LessModularEdge {
bool operator()(const ModularEdge &a1, const ModularEdge &a2) const {
return (a1.first < a2.first);
}
};
typedef std::set<ModularEdge, LessModularEdge> ModularEdges;
class ModularAggregate {
public:
ModularAggregate() = default;
std::vector<bdd> state;
bool boucle{false};
bool blocage{false};
bool visited{false};
std::set<ModularEdge> predecessors;
std::set<ModularEdge> successors;
/**
* Operator << overload
* @param os
* @param c
* @return
*/
friend std::ostream &operator<<(std::ostream &os, const ModularAggregate &c) {
os << "{";
for (const auto &k : c.state) {
os << k.id() << ", ";
}
os << "}";
return (os);
}
};
#endif // MODULAR_AGGREGATE_H_
src/modular_sog.cpp deleted 100644 → 0
+ 0
− 173
View file @ 74aafb1b
#include "modular_sog.hpp"
// intermediate table to calculate the size (nb bdd) of the graph
bdd *tmp_table;
void ModularSOG::set_initial_state(ModularAggregate *s) {
current_state = initial_state = s;
}
ModularAggregate *ModularSOG::FindState(const ModularAggregate *s) const {
for (auto *GONode : GONodes) {
bool arret = false;
for (auto k = 0; ((k < (s->state).size()) && (!arret)); k++) {
if ((s->state[k] == GONode->state[k]) == 0) {
arret = true;
}
}
if (!arret) {
return GONode;
}
}
return nullptr;
}
ModularAggregate *ModularSOG::FindState2(const ModularAggregate *s,
Set states_involved) const {
for (auto *GONode : GONodes) {
bool arret = false;
for (auto k = 0; ((k < (s->state).size()) && (!arret)); k++) {
if (states_involved.find(k) != states_involved.end()) {
if ((s->state[k] == GONode->state[k]) == 0) {
arret = true;
}
}
}
if (!arret && (s->blocage == GONode->blocage) &&
(s->boucle == GONode->boucle)) {
return GONode;
}
}
return nullptr;
}
void ModularSOG::AddArc(ModularAggregate *pred, ModularAggregate *succ,
const char *trans) {
const auto arc = ModularEdge(succ, trans);
const auto cra = ModularEdge(pred, trans);
if (pred->successors.find(arc) == pred->successors.end()) {
pred->successors.insert(pred->successors.begin(), arc);
succ->predecessors.insert(succ->predecessors.begin(), cra);
nb_arcs++;
}
}
void ModularSOG::InsertState(ModularAggregate *s) {
s->visited = false;
this->GONodes.push_back(s);
nb_states++;
}
void ModularSOG::InitVisit(ModularAggregate *s, size_t nb) {
if (nb <= nb_states) {
s->visited = false;
for (const auto &successor : s->successors) {
if (successor.first->visited) {
nb++;
InitVisit(successor.first, nb);
}
}
}
}
void ModularSOG::TabBDDNodes(ModularAggregate *s, size_t &nb) {
if (!s->visited) {
for (unsigned int k = 0; k < s->state.size(); k++, nb++) {
tmp_table[nb - 1] = s->state[k];
}
nb--;
s->visited = true;
for (const auto &successor : s->successors) {
if (!successor.first->visited) {
nb++;
TabBDDNodes(successor.first, nb);
}
}
}
}
void ModularSOG::PrintFullInformation(int nb_subnets) {
std::cout << "\n\nGRAPH SIZE : \n";
std::cout << "\n\tNB MARKING : " << nb_marking;
std::cout << "\n\tNB NODES : " << nb_states;
std::cout << "\n\tNB ARCS : " << nb_arcs << '\n';
std::cout << " \n\nCOMPLETE INFORMATION ?(y/n)\n";
char c = 0;
std::cin >> c;
tmp_table = new bdd[nb_states * nb_subnets];
size_t bdd_node = 1;
TabBDDNodes(initial_state, bdd_node);
std::cout << "NB BDD NODES : "
<< bdd_anodecount(tmp_table, nb_states * nb_subnets) << '\n';
InitVisit(initial_state, 1);
if (c == 'y' || c == 'Y') {
size_t node = 1;
PrintGraph(initial_state, node);
}
}
void ModularSOG::PrintGraph(ModularAggregate *s, size_t &nb) const {
if (nb <= nb_states) {
std::cout << "\nSTATE NUMBER " << nb << " : \n";
s->visited = true;
PrintSuccessors(s);
getchar();
PrintPredecessors(s);
getchar();
for (const auto &successor : s->successors) {
if (!successor.first->visited) {
nb++;
PrintGraph(successor.first, nb);
}
}
}
}
void ModularSOG::Reset() {
current_state = nullptr;
nb_arcs = nb_marking = nb_states = 0;
}
void ModularSOG::PrintSuccessors(const ModularAggregate *s) const {
std::cout << *s << '\n';
if (s->boucle) {
std::cout << "\n\tON BOUCLE DESSUS AVEC EPSILON\n";
}
if (s->blocage) {
std::cout << "\n\tEXISTENCE D'UN ETAT BLOCANT\n";
}
std::cout << "\n\tSES SUCCESSEURS SONT ( " << s->successors.size()
<< " ) :\n\n";
getchar();
for (const auto &successor : s->successors) {
std::cout << " \t---" << successor.second << " -->";
std::cout << *(successor.first) << '\n';
getchar();
}
}
void ModularSOG::PrintPredecessors(const ModularAggregate *s) const {
std::cout << "\n\tSES PREDESCESSEURS SONT ( " << s->predecessors.size()
<< " ) :\n\n";
getchar();
for (const auto &predecessor : s->predecessors) {
std::cout << " \t---" << predecessor.second << " -->";
std::cout << *predecessor.first << '\n';
getchar();
}
}
void ModularSOG::IncrementNbArcs() {
nb_arcs++;
}
src/modular_sog.hpp deleted 100644 → 0
+ 0
− 107
View file @ 74aafb1b
#ifndef MODULAR_SOG_H_
#define MODULAR_SOG_H_
#include <set>
#include <vector>
#include "modular_aggregate.hpp"
// define types
typedef std::set<int> Set;
typedef std::vector<ModularAggregate *> ModularAggregates;
class ModularSOG {
public:
ModularSOG() = default;
ModularAggregates GONodes;
ModularAggregate *initial_state{nullptr};
ModularAggregate *current_state{nullptr};
size_t nb_states{0};
size_t nb_marking{0};
size_t nb_arcs{0};
/**
* Reset the graph
*/
void Reset();
/**
* Find a state
* @return
*/
ModularAggregate *FindState(const ModularAggregate *s) const;
/**
* Find a modular state
* @return
*/
ModularAggregate *FindState2(const ModularAggregate *s,
Set states_involved) const;
/**
* Print successors of an state
*/
void PrintSuccessors(const ModularAggregate *s) const;
/**
* Print predecessors of an state
*/
void PrintPredecessors(const ModularAggregate *s) const;
/**
* Reset the visit flag of all states
* @param s
* @param nb
*/
void InitVisit(ModularAggregate *s, size_t nb);
/**
* Fill the intermediate table to calculate the size of the graph
* @param s
* @param nb
*/
void TabBDDNodes(ModularAggregate *s, size_t &nb);
/**
* Insert a state
* @param s
*/
void InsertState(ModularAggregate *s);
/**
* Add an arc
* TODO: check the implementation of this
*/
void IncrementNbArcs();
/**
* Add arcs to the graph
* @param pred
* @param succ
* @param trans
*/
void AddArc(ModularAggregate *pred, ModularAggregate *succ,
const char *trans);
/**
* Print the graph
* @param s
* @param nb
*/
void PrintGraph(ModularAggregate *s, size_t &nb) const;
/**
* Set the initial state of this graph
* @param s
*/
void set_initial_state(ModularAggregate *s);
/**
* Print full information of the graph
* @param nb_subnets
*/
void PrintFullInformation(int nb_subnets);
};
#endif // MODULAR_SOG_H_
src/petri_net_sog.cpp
+ 14
− 14
View file @ b5f2eb40
......@@ -48,7 +48,7 @@ void PrintHandler(ostream &o, int var) {
}
}
int choisir(Set cov, Set fire) {
int Choisir(Set cov, Set fire) {
auto it = fire.begin();
while (it != fire.end()) {
if (cov.find(*it) == cov.end()) {
......@@ -60,7 +60,7 @@ int choisir(Set cov, Set fire) {
return -1;
}
void reinit_cycle(const vector<int> &sw, map<int, int> &trans_obs) {
void ReinitCycle(const vector<int> &sw, map<int, int> &trans_obs) {
for (auto i : sw) {
if (trans_obs[i] > 0) {
trans_obs[i] = 2;
......@@ -87,9 +87,9 @@ bdd Trans::operator[](const bdd &op) const {
return res;
}
/*****************************************************************/
/* Class RdPBDD */
/*****************************************************************/
/*****************************************************************************/
/* Class PetriNetSOG */
/*****************************************************************************/
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()) {
......@@ -247,8 +247,8 @@ bdd PetriNetSOG::AccessibleEpsilon(const bdd &from_s) const {
return m2;
}
pair<int, bdd> PetriNetSOG::StepBackward1(const bdd &from,
const Aggregate *aggr) const {
pair<int, bdd> PetriNetSOG::StepBackward(const bdd &from,
const Aggregate *aggr) const {
pair<int, bdd> res;
for (const auto t : non_observables) {
......@@ -320,7 +320,7 @@ set<chem> PetriNetSOG::ObservablePaths(SOG &g, map<int, int> trans_obs) const {
// if there are firable transitions
if (!e.second.empty()) {
// choose a transition from the firable transitions
int t = choisir(cov, e.second);
int t = Choisir(cov, e.second);
if (t != -1) {
ancien = false;
trans_obs[t]--;
......@@ -367,7 +367,7 @@ set<chem> PetriNetSOG::ObservablePaths(SOG &g, map<int, int> trans_obs) const {
if (!ancien) {
cto.insert(sw);
}
reinit_cycle(sw, trans_obs);
ReinitCycle(sw, trans_obs);
sw.pop_back();
} else {
......@@ -377,7 +377,7 @@ set<chem> PetriNetSOG::ObservablePaths(SOG &g, map<int, int> trans_obs) const {
if (!ancien) {
cto.insert(sw);
}
reinit_cycle(sw, trans_obs);
ReinitCycle(sw, trans_obs);
sw.pop_back();
ancien = true;
......@@ -440,11 +440,11 @@ chem PetriNetSOG::AbstractPaths(chem path, const SOG &g) const {
const Couple agr_entree = point_entree.top();
point_entree.pop();
Aggregate *agr = agr_entree.first;
const Aggregate *agr = agr_entree.first;
const bdd target = agr_entree.second;
if (i == 0) {
source = FrontiereNodes1(agr->state, trans);
source = FrontiereNodes(agr->state, trans);
}
if (i == 1) {
......@@ -468,7 +468,7 @@ vector<int> PetriNetSOG::SubPathAggregate(bdd *source, const bdd &target,
bdd current_state = *source;
while ((target & current_state) == bdd_false()) {
pair<int, bdd> couple = StepBackward1(current_state, aggr);
pair<int, bdd> couple = StepBackward(current_state, aggr);
path.insert(path.begin(), couple.first);
current_state = couple.second;
}
......@@ -477,6 +477,6 @@ vector<int> PetriNetSOG::SubPathAggregate(bdd *source, const bdd &target,
return path;
}
bdd PetriNetSOG::FrontiereNodes1(const bdd &from, const int t) const {
bdd PetriNetSOG::FrontiereNodes(const bdd &from, const int t) const {
return bddfalse | (from & relation[t].precond);
}
src/petri_net_sog.hpp
+ 3
− 3
View file @ b5f2eb40
......@@ -65,8 +65,8 @@ class PetriNetSOG {
bdd AccessibleEpsilon(const bdd& from_s) const;
// step backward
std::pair<int, bdd> StepBackward1(const bdd& from,
const Aggregate* aggr) const;
std::pair<int, bdd> StepBackward(const bdd& from,
const Aggregate* aggr) const;
/**
* Returns the successor of a state from a transition
......@@ -96,7 +96,7 @@ class PetriNetSOG {
std::vector<int> SubPathAggregate(bdd* source, const bdd& target,
const Aggregate* aggr) const;
bdd FrontiereNodes1(const bdd& from, int t) const;
bdd FrontiereNodes(const bdd& from, int t) const;
};
#endif // PETRI_NET_SOG_H_
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