diff --git a/src/main.cpp b/src/main.cpp
index 5365cf2af69cf6cea2872fe23b7eeb40ed6a1714..ba249e0409ba634d855508c5ed11d2e9f0537ad9 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -16,25 +16,39 @@
using namespace std;
+// definition of type path
+typedef set<vector<int>> paths_t;
+
+/**
+ * @brief Return the current time in secods
+ * @return time in seconds
+ */
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";
+/**
+ * @brief Save in a file the information about observable paths
+ * @param output_file Path to the file where the output will be saved
+ * @param obs_paths Set of observable paths
+ */
+void save_observable_paths(const paths_t& obs_paths,
+ const string& output_file) {
cout << "Saving results in " << output_file << endl;
- ofstream monFlux(output_file);
- monFlux << "# paths: " << obs_paths.size() << endl;
+ ofstream my_file(output_file);
+ my_file << "# paths: " << obs_paths.size() << endl;
int n = 1;
for (auto path : obs_paths) {
- monFlux << "path #" << n << ": " << path.size() << " transitions" << endl;
+ my_file << "path #" << n << ": " << path.size() << " transitions" << endl;
n++;
}
}
-void print_stats(const set<vector<int>> abstract_paths) {
+/**
+ * @brief Print statistics about the generated abstract paths
+ * @param abstract_paths Set of abstract paths
+ */
+void print_stats(const paths_t& abstract_paths) {
int sum_transtions = 0;
set<int> transitions;
@@ -60,13 +74,22 @@ void print_stats(const set<vector<int>> abstract_paths) {
cout << "# covered transitions: " << transitions.size() << endl;
}
+/**
+ * @brief Prints the output of the tool
+ * @param model Petri net model
+ * @param g SOG graph
+ * @param obs_transitions observable transitions
+ * @param obs_paths set of observable paths
+ * @param abstract_paths set of abstract paths
+ * @param elapsed_time time consumed by the computation
+ * @param output_file file where the information will be saved
+ */
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) {
+ const paths_t& obs_paths, const paths_t& abstract_paths,
+ float elapsed_time, const string& output_file) {
// save observable paths in the folder
- save_observable_paths(model_name, output_folder, obs_paths);
+ save_observable_paths(obs_paths, output_file);
// print SOG information
g.printCompleteInformation();
@@ -78,11 +101,16 @@ void print_output(const net& model, MDGraph& g,
// print stats
print_stats(abstract_paths);
- // print time
+ // print consumed time
cout << "\nTime for computing all the paths: " << elapsed_time << " seconds"
<< endl;
}
+/**
+ * @brief Returns the name of the model from the filename
+ * @param filename Path to the petri net model
+ * @return name of the model
+ */
string get_model_name(const string& filename) {
int pp = filename.find(".n") + 1;
int ps = filename.rfind("/") + 1;
@@ -90,106 +118,142 @@ string get_model_name(const string& filename) {
return name;
}
+/**
+ * @brief Load a petri net from a .net file
+ * @param filename Path to the petri net model
+ * @return Petri net model
+ */
net load_net(const string& filename) {
cout << "Parsing net: " << filename << " ... ";
- net R(filename.c_str());
+ net model(filename.c_str());
cout << "done" << endl;
- return R;
+ return model;
}
-void compute_abstract_paths(const net& model, MDGraph& g,
+/**
+ * @brief Compute the set of abstract path from a Petri net model
+ * @param model Petri net model
+ * @param bound SOG bound
+ * @param obs observable transition
+ * @param unobs unobservable transitions
+ * @param g SOG graph
+ * @param obs_paths observable paths
+ * @param abstract_paths abstract paths
+ */
+void compute_abstract_paths(const net& model, int bound,
const map<int, int>& obs, const set<int>& unobs,
- set<vector<int>>& obs_paths,
- set<vector<int>>& abstract_path, int bound) {
+ MDGraph& g, paths_t& obs_paths,
+ paths_t& abstract_paths) {
// build the SOG
cout << "Building SOG ...";
- RdPBDD DR(model, obs, unobs, bound);
- cout << "done";
+ RdPBDD SOG(model, obs, unobs, bound);
+ cout << " done" << endl;
// compute the observable paths
- obs_paths = DR.chem_obs(g, obs);
+ obs_paths = SOG.chem_obs(g, obs);
// add abstract paths
for (auto path : obs_paths) {
- abstract_path.insert(DR.chem_abs(path, g));
+ abstract_paths.insert(SOG.chem_abs(path, g));
}
}
-void generate_paths_from_file(const string& net_file,
+/**
+ * @brief Generates abstract paths of a Petri net covering transitions specified
+ * in a file
+ * @param net_file Path to file of the petri net model
+ * @param bound SOG bound
+ * @param transitions_file Path to file of observable transitions
+ * @param output_folder Path to folder where output files will be saved
+ */
+void generate_paths_from_file(const string& net_file, int bound,
const string& transitions_file,
- const string& output_folder, int bound = 32) {
+ const string& output_folder) {
net model = load_net(net_file);
string model_name = get_model_name(net_file);
+ // TODO: should we take into account reading the file ?
double d = getTime();
// get observable transitions from file
- map<int, int> obs;
- ifstream flux(transitions_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});
+ string line;
+ ifstream my_file(transitions_file);
+ map<int, int> obs_trans; // TODO: <transition_id, _>
+ if (my_file) {
+ while (getline(my_file, line)) {
+ // TODO: catch error when the file has transition different to t
+ int tr = stoi(line.substr(1)); // for a transition t1, we take the id 1
+ obs_trans.insert({tr, 1});
}
}
+ // TODO: What happens if the transition started in t1 instead of t0 ?
// compute the unobservable transitions
- set<int> unobs;
+ set<int> unobs_trans;
for (long unsigned int i = 0; i < model.transitions.size(); i++) {
- if ((obs.find(i)) == obs.end()) {
- unobs.insert(i);
+ if ((obs_trans.find(i)) == obs_trans.end()) {
+ unobs_trans.insert(i);
}
}
// 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);
+ paths_t obs_paths;
+ paths_t abstract_paths;
+ compute_abstract_paths(model, bound, obs_trans, unobs_trans, g, obs_paths,
+ abstract_paths);
// time for generating the paths
- double tps = getTime() - d;
+ float tps = getTime() - d;
// print output
- print_output(model, g, obs, obs_paths, abstract_paths, tps, model_name,
- output_folder);
+ string output_file = output_folder + "/no_optimal_" + model_name + ".txt";
+ print_output(model, g, obs_trans, obs_paths, abstract_paths, tps,
+ output_file);
}
-void generate_all_paths(const string& net_file, const string& output_folder,
- int bound = 32) {
+/**
+ * @brief Generate abstract paths of a Petri net covering all the observable
+ * transitions
+ * @param net_file Path to file of the petri net model
+ * @param bound SOG bound
+ * @param output_folder Path to folder where output files will be saved
+ */
+void generate_all_paths(const string& net_file, int bound,
+ const string& output_folder) {
net model = load_net(net_file);
string model_name = get_model_name(net_file);
double d = getTime();
// compute the unobservable transitions of the model using the pattern
- set<int> unobs = model.calcul1();
+ set<int> unobs_trans = model.calcul1();
// compute the observable transitions
- map<int, int> obs;
+ map<int, int> obs_trans;
for (long unsigned int i = 0; i < model.transitions.size(); i++) {
- if ((unobs.find(i)) == unobs.end()) {
- obs.insert({i, 1});
+ if ((unobs_trans.find(i)) == unobs_trans.end()) {
+ obs_trans.insert({i, 1});
}
}
// 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);
+ paths_t obs_paths;
+ paths_t abstract_paths;
+ compute_abstract_paths(model, bound, obs_trans, unobs_trans, g, obs_paths,
+ abstract_paths);
// time for generating the paths
- double tps = getTime() - d;
+ float tps = getTime() - d;
// print output
- print_output(model, g, obs, obs_paths, abstract_paths, tps, model_name,
- output_folder);
+ string output_file = output_folder + "/no_optimal_" + model_name + ".txt";
+ print_output(model, g, obs_trans, obs_paths, abstract_paths, tps,
+ output_file);
}
+
/******************************************************************************
* Main function
******************************************************************************/
@@ -212,17 +276,19 @@ int main(int argc, char** argv) {
std::string obs_file;
CLI::Option* opt_transitions =
app.add_option("--obs-file", obs_file,
- "Cover transitions from file [default: all transitions]")
+ "Cover observable transitions from file [default: all "
+ "transitions]")
->type_name("Path")
->check(CLI::ExistingFile);
// parse arguments
CLI11_PARSE(app, argc, argv);
+ int bound = 32;
if (*opt_transitions) {
- generate_paths_from_file(input_file, obs_file, output_folder);
+ generate_paths_from_file(input_file, bound, obs_file, output_folder);
} else {
- generate_all_paths(input_file, output_folder);
+ generate_all_paths(input_file, bound, output_folder);
}
return 0;