diff --git a/src/main.cpp b/src/main.cpp index 04e603c64a0a41d91906a084f4392f39964c69e7..68e63a0b8da542a2b809f23b955fb4f2b797a06b 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -25,7 +25,7 @@ void save_observable_paths(const string& model_name, cout << "Saving results in " << output_file << endl; ofstream monFlux(output_file); - monFlux << "# observable paths: " << obs_paths.size() << endl; + monFlux << "# paths: " << obs_paths.size() << endl; int n = 1; for (auto path : obs_paths) { @@ -116,9 +116,17 @@ void compute_abstract_paths(const net& model, MDGraph& g, } } -void get_transitions_from_file(const net& model, const string& file, - map<int, int>& obs, set<int>& unobs) { - ifstream flux(file); +void generate_paths_from_file(const string& net_file, + const string& transitions_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(); + + // get observable transitions from file + map<int, int> obs; + ifstream flux(transitions_file); string ligne; if (flux) { while (getline(flux, ligne)) { @@ -126,11 +134,28 @@ void get_transitions_from_file(const net& model, const string& file, obs.insert({tr, 1}); } } + + // compute the unobservable transitions + set<int> unobs; for (long unsigned int i = 0; i < model.transitions.size(); i++) { if ((obs.find(i)) == obs.end()) { unobs.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); + + // time for generating the paths + double tps = getTime() - d; + + // print output + print_output(model, g, obs, obs_paths, abstract_paths, tps, model_name, + output_folder); } void generate_all_paths(const string& net_file, const string& output_folder, @@ -203,7 +228,7 @@ int main(int argc, char** argv) { ->fallthrough(); std::string obs_file; - generate->add_option("--transitions", obs_file, "Observable transitions") + generate->add_option("--obs-file", obs_file, "Observable transitions") ->type_name("Path") ->check(CLI::ExistingFile); @@ -214,9 +239,11 @@ int main(int argc, char** argv) { // reach->callback([&]() {}); // sog->callback([&]() {}); generate->callback([&]() { - // if (all) { - generate_all_paths(input_file, output_folder); - // } + if (all) { + generate_all_paths(input_file, output_folder); + } else { + generate_paths_from_file(input_file, obs_file, output_folder); + } }); // parse arguments