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

add documentation

parent 61c3860e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 123 additions and 57 deletions
src/main.cpp
+ 123
− 57
View file @ 6653eff7
......@@ -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;
......
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