diff --git a/src/MDGraph.hpp b/src/MDGraph.hpp
index 34850f1fa28736def422cfca666ff44030fb1fb0..7be028bf66a138080d6cb2c9561a79c40994d218 100644
--- a/src/MDGraph.hpp
+++ b/src/MDGraph.hpp
@@ -5,12 +5,13 @@
#ifndef _MDGRAPH_
#define _MDGRAPH_
-using namespace std;
#include <iostream>
#include <list>
#include <string>
#include <vector>
+using namespace std;
+
#include "Class_of_state.hpp"
typedef set<int> Set;
typedef vector<Class_Of_State *> MetaGrapheNodes;
diff --git a/src/main.cpp b/src/main.cpp
index 2266fa709bf5d987ae2bce771d16030ceb041165..04e603c64a0a41d91906a084f4392f39964c69e7 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -18,6 +18,22 @@ using namespace std;
double getTime() { return (double)clock() / (double)CLOCKS_PER_SEC; }
+void save_observable_paths(const string& model_name,
+ const string& output_folder,
+ const set<vector<int>>& obs_paths) {
+ string output_file = output_folder + "/no_optimal_" + model_name + ".txt";
+ cout << "Saving results in " << output_file << endl;
+
+ ofstream monFlux(output_file);
+ monFlux << "# observable paths: " << obs_paths.size() << endl;
+
+ int n = 1;
+ for (auto path : obs_paths) {
+ monFlux << "path #" << n << ": " << path.size() << " transitions" << endl;
+ n++;
+ }
+}
+
void print_stats(const set<vector<int>> abstract_paths) {
int sum_transtions = 0;
set<int> transitions;
@@ -44,6 +60,29 @@ void print_stats(const set<vector<int>> abstract_paths) {
cout << "# covered transitions: " << transitions.size() << endl;
}
+void print_output(const net& model, MDGraph& g,
+ const map<int, int>& obs_transitions,
+ const set<vector<int>>& obs_paths,
+ const set<vector<int>>& abstract_paths, float elapsed_time,
+ const string& model_name, const string& output_folder) {
+ // save observable paths in the folder
+ save_observable_paths(model_name, output_folder, obs_paths);
+
+ // print SOG information
+ g.printCompleteInformation();
+ cout << "\n# transition: " << model.transitions.size() << endl;
+ cout << "# places: " << model.places.size() << endl;
+ cout << "# observable transitions: " << obs_transitions.size() << endl
+ << endl;
+
+ // print stats
+ print_stats(abstract_paths);
+
+ // print time
+ cout << "\nTime for computing all the paths: " << elapsed_time << " seconds"
+ << endl;
+}
+
string get_model_name(const string& filename) {
int pp = filename.find(".n") + 1;
int ps = filename.rfind("/") + 1;
@@ -59,14 +98,45 @@ net load_net(const string& filename) {
return R;
}
-void generate_paths(const string& file, const string& output_folder,
- int bound = 32) {
- net model = load_net(file);
- string model_name = get_model_name(file);
+void compute_abstract_paths(const net& model, MDGraph& g,
+ const map<int, int>& obs, const set<int>& unobs,
+ set<vector<int>>& obs_paths,
+ set<vector<int>>& abstract_path, int bound) {
+ // build the SOG
+ cout << "Building SOG ...";
+ RdPBDD DR(model, obs, unobs, bound);
+ cout << "done";
+
+ // compute the observable paths
+ obs_paths = DR.chem_obs(g, obs);
- map<int, int> obs;
- set<vector<int>> abstrait;
- MDGraph g;
+ // add abstract paths
+ for (auto path : obs_paths) {
+ abstract_path.insert(DR.chem_abs(path, g));
+ }
+}
+
+void get_transitions_from_file(const net& model, const string& file,
+ map<int, int>& obs, set<int>& unobs) {
+ ifstream flux(file);
+ string ligne;
+ if (flux) {
+ while (getline(flux, ligne)) {
+ int tr = stoi(ligne.substr(1)); // le ligne sous forme de t1 prendre le1
+ obs.insert({tr, 1});
+ }
+ }
+ for (long unsigned int i = 0; i < model.transitions.size(); i++) {
+ if ((obs.find(i)) == obs.end()) {
+ unobs.insert(i);
+ }
+ }
+}
+
+void generate_all_paths(const string& net_file, const string& output_folder,
+ int bound = 32) {
+ net model = load_net(net_file);
+ string model_name = get_model_name(net_file);
double d = getTime();
@@ -74,48 +144,26 @@ void generate_paths(const string& file, const string& output_folder,
set<int> unobs = model.calcul1();
// compute the observable transitions
+ map<int, int> obs;
for (long unsigned int i = 0; i < model.transitions.size(); i++) {
if ((unobs.find(i)) == unobs.end()) {
obs.insert({i, 1});
}
}
- // build the SOG
- cout << "Building SOG ...";
- RdPBDD DR(model, obs, unobs, bound);
- cout << "done";
-
- // compute the observable paths
- set<vector<int>> chemins = DR.chem_obs(g, obs);
-
- string output_file = output_folder + "/no_optimal_" + model_name + ".txt";
- ofstream monFlux(output_file);
- monFlux << "le nombre de chemins observés: " << chemins.size() << endl;
-
- int n = 1;
- for (auto i : chemins) {
- monFlux << "le " << n << " ch: " << i.size() << " tr." << endl;
-
- // add abstract paths
- abstrait.insert(DR.chem_abs(i, g));
- n++;
- }
+ // compute abstract paths
+ MDGraph g;
+ set<vector<int>> obs_paths;
+ set<vector<int>> abstract_paths;
+ compute_abstract_paths(model, g, obs, unobs, obs_paths, abstract_paths,
+ bound);
// time for generating the paths
double tps = getTime() - d;
- // print SOG information
- g.printCompleteInformation();
- cout << "\n# transition: " << model.transitions.size() << endl;
- cout << "# places: " << model.places.size() << endl;
- cout << "# observable transitions: " << obs.size() << endl << endl;
-
- // print stats
- print_stats(abstrait);
-
- // print time
- cout << "\nTime for computing all the paths: " << tps << " seconds" << endl;
- cout << "Saving results in " << output_file << endl;
+ // print output
+ print_output(model, g, obs, obs_paths, abstract_paths, tps, model_name,
+ output_folder);
}
/******************************************************************************
* Main function
@@ -165,7 +213,11 @@ int main(int argc, char** argv) {
// reach->callback([&]() {});
// sog->callback([&]() {});
- generate->callback([&]() { generate_paths(input_file, output_folder); });
+ generate->callback([&]() {
+ // if (all) {
+ generate_all_paths(input_file, output_folder);
+ // }
+ });
// parse arguments
CLI11_PARSE(app, argc, argv);