Implementation of a CLI for the tool

CMakeLists.txt

@@ -53,6 +53,13 @@ else ()
  include_directories("${SPOT_INCLUDE_PATH}")
 endif()
 
+# Third-party libraries PATH
+set(THIRD_PARTY_INCLUDE_DIR ${CMAKE_SOURCE_DIR}/third-party)
+
+# CLI library
+add_library(cli11 INTERFACE)
+target_include_directories(cli11 INTERFACE "${THIRD_PARTY_INCLUDE_DIR}/cli11")
+
 # add source folder
 include_directories(src)
 add_subdirectory(src)

src/CMakeLists.txt

@@ -38,7 +38,7 @@ else()
 endif()
 
 # Hybrid SOG executable
-add_executable(mc-sog main.cpp
+add_executable(pmc-sog main.cpp
   PMCSOGConfig.h
   NewNet.cpp
   NewNet.h
@@ -100,12 +100,13 @@ add_executable(mc-sog main.cpp
         misc/md5_hash.h Hybrid/MCHybridPOR/MCHybridSOGPOR.cpp Hybrid/MCHybridPOR/MCHybridSOGPOR.h)
 
 
-target_include_directories(mc-sog PUBLIC  "${PROJECT_BINARY_DIR}/src")
+target_include_directories(pmc-sog PUBLIC  "${PROJECT_BINARY_DIR}/src")
 
-target_link_libraries(mc-sog
+target_link_libraries(pmc-sog
   bddx
   spot
   RdP
   ${MPI_LIBRARIES}
   ${OPENSSL_LIBRARIES}
+  cli11
 )

src/main.cpp

@@ -4,7 +4,7 @@
 #include <string>
 #include <fstream>
 #include <mpi.h>
-
+#include <CLI11.hpp>
 
 #include "LDDGraph.h"
 #include "MCMultiCore/ModelCheckerCPPThread.h"
@@ -35,309 +35,570 @@
 #include "PMCSOGConfig.h"
 #include "Hybrid/MCHybridReqPOR/MCHybridSOGReqPOR.h"
 #include "Hybrid/MCHybridPOR/MCHybridSOGPOR.h"
-// #include "RdPBDD.h"
 
 using namespace std;
 
-
-unsigned int nb_th;
 int n_tasks, task_id;
-spot::formula not_f;
-set<string> buildPropositions(const string &fileName) {
-	string input;
-	set<string> transitionSet;
-	ifstream file(fileName);
-	if (file.is_open()) {
-		getline(file, input);
-		cout << "Loaded formula : " << input << endl;
-		file.close();
-
-	} else {
-		cout << "Can not open formula file" << endl;
-		exit(0);
-	}
-
-	spot::parsed_formula pf = spot::parse_infix_psl(input);
-	if (pf.format_errors(std::cerr))
-		return transitionSet;
-	spot::formula fo = pf.f;
-	if (!fo.is_ltl_formula()) {
-		std::cerr << "Only LTL formulas are supported.\n";
-		return transitionSet;
-	}
-	spot::atomic_prop_set *p_list = spot::atomic_prop_collect(fo, nullptr);
-	for (const auto & i : *p_list) {
-		transitionSet.insert(i.ap_name());
-	}
-	print_spin_ltl(std::cout, fo) << '\n';
-	cout << "Building formula negation\n";
-	not_f = spot::formula::Not(pf.f);
-	return transitionSet;
+unsigned int nb_th; // used by the distributed model checker
+
+struct Formula
+{
+    spot::formula f;
+    set<string> propositions;
+};
+
+/**
+ * Parse a file  containing a LTL formula and return its negation
+ *
+ * @param fileName Path to LTL formula
+ * @return Formula
+ */
+Formula negateFormula(const string &fileName)
+{
+    string input;
+    set<string> transitionSet;
+    ifstream file(fileName);
+
+    cout << "______________________________________" << endl;
+    cout << "Fetching formula ... " << endl;
+
+    if (!file.is_open())
+    {
+        cout << "Cannot open formula file" << endl;
+        exit(0);
+    }
+
+    getline(file, input);
+    cout << "        Loaded formula: " << input << endl;
+    file.close();
 
+    spot::parsed_formula pf = spot::parse_infix_psl(input);
+    if (pf.format_errors(std::cerr))
+        exit(0);
+
+    spot::formula fo = pf.f;
+    if (!fo.is_ltl_formula())
+    {
+        std::cerr << "Only LTL formulas are supported.\n";
+        exit(0);
+    }
+
+    spot::atomic_prop_set *p_list = spot::atomic_prop_collect(fo, nullptr);
+    for (const auto &i : *p_list)
+    {
+        transitionSet.insert(i.ap_name());
+    }
+    cout << "Formula in SPIN format: ";
+    print_spin_ltl(std::cout, fo) << endl;
+
+    cout << "Building negation of the formula ... ";
+    spot::formula not_f = spot::formula::Not(pf.f);
+    cout << "done\n"
+         << endl;
+
+    return {not_f, transitionSet};
 }
-void displayCheckResult(bool res) {
-	if (res)
-		cout << "Property is verified..." << endl;
-	else
-		cout << "Property is violated..." << endl;
+
+/**
+ * Convert a formula inton an automaton
+ *
+ * @param f  Formula to be converted
+ * @param bdd  BDD structure
+ * @return spot::twa_graph_ptr
+ */
+spot::twa_graph_ptr formula2Automaton(const spot::formula &f, spot::bdd_dict_ptr bdd)
+{
+    cout << "\nBuilding automata for not(formula)\n";
+    spot::twa_graph_ptr af = spot::translator(bdd).run(f);
+    cout << "Formula automata built.\n"
+         << endl;
+    return af;
 }
 
-void displayTime(auto startTime,auto finalTime) {
-	cout << "Verification duration : " << std::chrono::duration_cast < std::chrono::milliseconds> (finalTime - startTime).count() << " milliseconds\n";
+/**
+ * Print the result of the verification
+ *
+ * @param res flag indicating if the property is true or false
+ */
+void displayCheckResult(bool res)
+{
+    if (res)
+        cout << "Property is verified..." << endl;
+    else
+        cout << "Property is violated..." << endl;
 }
-/***********************************************/
-int main(int argc, char **argv) {
-
-	if (argc < 3)
-		return 0;
-	char formula[100] = "";
-	char algorithm[100] = "";
-	strcpy(formula, argv[4]);
-	if (argc > 5) {
-		strcpy(algorithm, argv[5]);
-	}
-
-	nb_th = atoi(argv[2]) == 0 ? 1 : atoi(argv[2]);
+
+/**
+ * Display the elapsed time between two times
+ *
+ * @param startTime initial time
+ * @param finalTime final time
+ */
+void displayTime(auto startTime, auto finalTime)
+{
+    cout << "Verification duration : " << std::chrono::duration_cast<std::chrono::milliseconds>(finalTime - startTime).count() << " milliseconds\n";
+}
+
+/**
+ * Checks if the options are valid to run the multi-core version
+ *
+ * @param nb_threads Number of threads
+ * @param method  Method to build the threads
+ * @return bool
+ */
+bool isValidMultiCoreMCOption(int nb_threads, const string &method)
+{
+    set<string> options = {"otfPR",
+                           "otfC",
+                           "otfP",
+                           "otfCPOR"};
+
+    return (nb_threads == 1 && (options.find(method) != options.end()));
+}
+
+/**
+ * Checks if the options are valid to run the hybrid version
+ *
+ * @param nb_threads Number of threads
+ * @param method  Method to build the distributed SOG
+ * @return bool
+ */
+bool isValidHybridMCOption(int nb_threads, const string &method)
+{
+    set<string> options = {"otf",
+                           "otfPR",
+                           "otfPOR",
+                           "otfPRPOR"};
+
+    return (nb_threads > 1 && (options.find(method) != options.end()));
+}
+
+/**
+ * Print information of the execution
+ *
+ * @param net Net to be verified
+ * @param formula  Formula to be verified
+ * @param algorithm Emptiness check algorithm to be used
+ * @param nb_th  Number of threads of the execution
+ */
+void displayToolInformation(const string &net, const string &formula, const string &algorithm, int nb_th)
+{
+    // computes the current year
+    time_t t = std::time(nullptr);
+    tm *const pTInfo = std::localtime(&t);
+    int year = 1900 + pTInfo->tm_year;
+
+    cout << "PMC-SOG: Parallel Model Checking tool based on Symbolic Observation Graphs" << endl;
+    cout << "Version " << PMCSOG_VERSION_MAJOR << "." << PMCSOG_VERSION_MINOR << "." << PMCSOG_VERSION_PATCH << endl;
+    cout << "(c) 2018 - " << year << endl;
+    cout << endl;
+    cout << "          Net file: " << net << endl;
+    cout << "      Formula file: " << formula << endl;
+    cout << "Checking algorithm: " << algorithm << endl;
+    cout << "         # threads: " << nb_th << endl;
+}
+
+/**
+ * Get the multi-core model-checker
+ *
+ * @param net Net to be verified
+ * @param method Multi-core implementation
+ * @param nb_th Number of threads
+ * @return ModelCheckBaseMT*
+ */
+ModelCheckBaseMT *getMultiCoreMC(NewNet &net, const string &method, int nb_th)
+{
+    ModelCheckBaseMT *mcl = nullptr;
+
+    // select the right model-checking algorithm
+    if (method == "otfP")
+    {
+        cout << "Multi-threaded algorithm based on Pthread library!" << endl;
+        mcl = new ModelCheckerTh(net, nb_th);
+    }
+    else if (method == "otfPR")
+    {
+        cout << "Multi-threaded algorithm (progressive) based on PThread!" << endl;
+        mcl = new ModelCheckThReq(net, nb_th);
+    }
+    else if (method == "otfC")
+    {
+        cout << "Multi-threaded algorithm based on C++ Thread library!" << endl;
+        mcl = new ModelCheckerCPPThread(net, nb_th);
+    }
+    else if (method == "otfCPOR")
+    {
+        cout << "Multi-threaded algorithm with POR!" << endl;
+        mcl = new MCCPPThPor(net, nb_th);
+    }
+    else
+    {
+        cout << method << " is not valid for the multi-core version" << endl;
+        exit(-1);
+    }
+
+    return mcl;
+}
+
+/**
+ * Get the Hybrid model-checker
+ *
+ * @param net Net to be verified
+ * @param method  Hybrid implementation
+ * @param communicator MPI communicator
+ * @return CommonSOG*
+ */
+CommonSOG *getHybridMC(NewNet &net, const string &method, MPI_Comm &communicator)
+{
+
+    CommonSOG *DR;
+    if (method == "otf")
+    {
+        cout << " Normal construction..." << endl;
+        DR = new MCHybridSOG(net, communicator, false);
+    }
+    else if (method == "otfPOR")
+    {
+        cout << " Normal construction with POR" << endl;
+        DR = new MCHybridSOGPOR(net, communicator, false);
+    }
+    else if (method == "otfPR")
+    {
+        cout << " Progressive construction..." << endl;
+        DR = new MCHybridSOGReq(net, communicator, false);
+    }
+    else if (method == "otfPRPOR")
+    {
+        cout << " Progressive construction with POR..." << endl;
+        DR = new MCHybridSOGReqPOR(net, communicator, false);
+    }
+    else
+    {
+        cout << " " << method << " is not valid for the hybrid version" << endl;
+        exit(0);
+    }
+    return DR;
+}
+
+/**
+ * Save a graph in a dot file
+ *
+ * @param graph Graph to be saved
+ * @param filename Output filename
+ * @param options Options to customized the print
+ */
+void saveGraph(spot::twa_graph_ptr graph, const string &filename, const char *options = nullptr)
+{
+    fstream file;
+    file.open(filename.c_str(), fstream::out);
+    spot::print_dot(file, graph, options);
+    file.close();
+}
+
+void runOnTheFlyMC(const string &algorithm, auto k, spot::twa_graph_ptr af)
+{
+    bool res = false;
+    std::chrono::steady_clock::time_point startTime, finalTime;
+
+    cout << "\nPerforming on the fly Model-Checking..." << endl;
+
+    if (algorithm != "")
+    {
+        // set the synchronized product of the SOG and the negated formula
+        shared_ptr<spot::twa_product> product = make_shared<spot::twa_product>(k, af);
+
+        // set the emptiness check
+        const char *err;
+        spot::emptiness_check_instantiator_ptr echeck_inst = spot::make_emptiness_check_instantiator(algorithm.c_str(), &err);
+
+        if (!echeck_inst)
+        {
+            cerr << "Failed to parse argument near '" << err << "'" << endl;
+            cerr << "Spot unknown emptiness algorithm" << endl;
+            exit(2);
+        }
+        else
+            cout << "Spot emptiness check algorithm: " << algorithm << endl;
+
+        // computes the on-the-fly emptiness check of the synchronized product
+        startTime = std::chrono::steady_clock::now();
+        spot::emptiness_check_ptr echptr = echeck_inst->instantiate(product);
+        res = (echptr->check() == nullptr);
+        finalTime = std::chrono::steady_clock::now();
+    }
+    else
+    {
+        // computes the intersection between the SOG and the negated formula
+        startTime = std::chrono::steady_clock::now();
+        res = (k->intersecting_run(af) == nullptr);
+        finalTime = std::chrono::steady_clock::now();
+    }
+
+    // display results
+    displayTime(startTime, finalTime);
+    displayCheckResult(res);
+}
+
+/******************************************************************************
+ * Main function
+ ******************************************************************************/
+int main(int argc, char **argv)
+{
+
+    CLI::App app{"PMC-SOG : Parallel Model Checking tool based on Symbolic Observation Graphs"};
+
+    app.add_option("--n", nb_th, "Number of threads/workers to be created (default: 1)")
+        ->default_val(1)
+        ->check(CLI::PositiveNumber);
+
+    string net = "";
+    app.add_option("--net", net, "Petri net file")
+        ->required()
+        ->check(CLI::ExistingFile);
+
+    string formula = "";
+    app.add_option("--ltl", formula, "LTL property file")
+        ->required()
+        ->check(CLI::ExistingFile);
+
+    string method = "";
+    app.add_option("--method", method, "Method to create threads or/and set if model-checking should be performed on the fly")
+        ->required();
+
+    string algorithm = "";
+    app.add_option("--emptiness-check", algorithm, "Number of threads/workers to be created");
+
+    CLI11_PARSE(app, argc, argv);
+
+    // MPI arguments
     MPI_Init(&argc, &argv);
     MPI_Comm_size(MPI_COMM_WORLD, &n_tasks);
     MPI_Comm_rank(MPI_COMM_WORLD, &task_id);
-   // n_tasks=1;
-    if (!task_id) {
-        cout << "PMC-SOG : Parallel Model Checking tool based on Symbolic Observation Graphs " << endl;
-        cout << "Version " <<PMCSOG_VERSION_MAJOR<<"."<<PMCSOG_VERSION_MINOR<<"."<<PMCSOG_VERSION_PATCH<<endl;
-        cout << "(c) 2018 - 2020"<<endl;
-        cout << "Net file : " << argv[3] << endl;
-        cout << "Formula file : " << formula << endl;
-        cout << "Checking algorithm : " << algorithm << endl;
-        cout << "#threads : " << nb_th << endl;
+
+    // Display information of the tool
+    if (!task_id)
+    {
+        displayToolInformation(net, formula, algorithm, nb_th);
+    }
+
+    // Check the number of processes
+    if (n_tasks <= 0)
+    {
+        cout << "Number of tasks <= 0 " << endl;
+        exit(0);
+    }
+
+    // Check the number of threads
+    if (nb_th <= 0)
+    {
+        cout << "Number of thread <= 0 " << endl;
+        exit(0);
+    }
+
+    // hybrid version requires two or more threads
+    if (n_tasks > 1 && nb_th < 2)
+    {
+        if (task_id == 0)
+            cout << "The hybrid version requires more than 1 threads\n"
+                 << endl;
+        exit(0);
     }
-	if (nb_th == 0) {
-		cout << "number of thread <= 0 " << endl;
-		exit(0);
-	}
-
-	cout << "______________________________________\n";
-	cout << "Fetching formula..." << endl;
-	set<string> list_propositions = buildPropositions(formula);
-	NewNet Rnewnet(argv[3], list_propositions);
-
-
-    if (n_tasks == 1) {
-        if (n_tasks == 1 && (!strcmp(argv[1], "otfPR") || !strcmp(argv[1], "otfC") || !strcmp(argv[1], "otfP") || !strcmp(argv[1], "otfCPOR"))) {
-            cout << "Performing on the fly Model checking..." << endl;
-            if (!strcmp(argv[1], "otfP"))
-                cout << "Multi-threaded algorithm based on Pthread library!" << endl;
-            else if (!strcmp(argv[1], "otfPR"))
-                cout << "Multi-threaded algorithm (progressive) based on PThread!" << endl;
-            else if (!strcmp(argv[1], "otfC"))
-                cout << "Multi-threaded algorithm based on C++ Thread library!" << endl;
-            else
-                cout<<"Multi-threaded algorithm with POR!"<<endl;
-            cout << "Building automata for not(formula)\n";
+
+    // Get the negation of the LTL formula
+    Formula negate_formula = negateFormula(formula);
+    NewNet Rnewnet(net.c_str(), negate_formula.propositions);
+    cout << endl;
+
+    /**************************************************************************
+     * Multi-core version
+     **************************************************************************/
+    if (n_tasks == 1)
+    {
+        // On-the-fly multi-core model checking
+        if (isValidMultiCoreMCOption(n_tasks, method))
+        {
+            // get the corresponding multi-core model-checker
+            ModelCheckBaseMT *mcl = getMultiCoreMC(Rnewnet, method, nb_th);
+
+            // build automata of the negation of the formula
             auto d = spot::make_bdd_dict();
-            spot::translator obj=spot::translator(d);
-
-            spot::twa_graph_ptr af = obj.run(not_f);
-            cout << "Formula automata built.\n";
-            ModelCheckBaseMT *mcl;
-
-            if (!strcmp(argv[1], "otfP"))
-                mcl = new ModelCheckerTh(Rnewnet, nb_th);
-            else if (!strcmp(argv[1], "otfC"))
-                mcl = new ModelCheckerCPPThread(Rnewnet, nb_th);
-            else if (!strcmp(argv[1], "otfPR"))
-                mcl=new ModelCheckThReq(Rnewnet, nb_th);
-            else mcl=new MCCPPThPor(Rnewnet, nb_th);
+            spot::twa_graph_ptr af = formula2Automaton(negate_formula.f, d);
+
+            // create the SOG
             mcl->loadNet();
             auto k = std::make_shared<SogKripkeTh>(d, mcl, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP());
-            cout << "Performing on the fly Modelchecking" << endl;
-            if (strcmp(algorithm, "")) {
-                cout << "Spot emptiness check algorithm : "<<algorithm<< endl;
-                shared_ptr < spot::twa_product > product = make_shared<spot::twa_product>(k,af);
-                //spot::couvreur99_check_shy check = spot::couvreur99_check_shy(product);
-                /****************************/
-                const char *err;
-                spot::emptiness_check_instantiator_ptr echeck_inst = spot::make_emptiness_check_instantiator(algorithm, &err);
-
-                if (!echeck_inst) {
-                    cerr << "Failed to parse argument near `" << err << "'" << endl;
-                    cerr << "Spot unknown emptiness algorithm" << endl;
-                    exit(2);
-                }
-                auto startTime = std::chrono::steady_clock::now();
-                spot::emptiness_check_ptr echptr = echeck_inst->instantiate(product);
-                bool res = (echptr->check() == nullptr);
-                auto finalTime = std::chrono::steady_clock::now();
-                displayTime(startTime, finalTime);
-                displayCheckResult(res);
-
-            } else {
-                auto startTime = std::chrono::steady_clock::now();
-                bool res = (k->intersecting_run(af) == nullptr);
-                auto finalTime = std::chrono::steady_clock::now();
-                displayTime(startTime, finalTime);
-                displayCheckResult(res);
-            }
+
+            // run on the fly model-checking
+            runOnTheFlyMC(algorithm, k, af);
+
+            // stop model checker process
             mcl->finish();
+
+            // print SOG information
             mcl->getGraph()->printCompleteInformation();
             delete mcl;
         }
-
-        else {
-            cout << "number of task = 1 \n " << endl;
-            bool uselace = (!strcmp(argv[1], "lc")) || (!strcmp(argv[1], "l"));
+        else // build only SOG
+        {
+            bool uselace = ((method == "lc") || (method == "l"));
             threadSOG DR(Rnewnet, nb_th, uselace);
             LDDGraph g(&DR);
 
-            if (nb_th == 1) {
-                cout << "******************Sequential version******************* \n" << endl;
+            // Sequential  construction of the SOG
+            // TODO: There is no way to run Model-checking when the SOG is built sequentially?
+            if (nb_th == 1)
+            {
+                cout << "\n****************** Sequential version ******************* \n"
+                     << endl;
+
+                // build sequential SOG
                 DR.computeSeqSOG(g);
+
+                // print SOG information
                 g.printCompleteInformation();
-            } else {
-                cout << "*******************Multithread version****************** \n" << endl;
-                cout << "Count of threads to be created: " << nb_th << endl;
-                if (!strcmp(argv[1], "p")) {
+            }
+            else // Multi-thread construction of the SOG
+            {
+                cout << "\n******************* Multi-thread version ****************** \n"
+                     << endl;
+                cout << "# of threads to be created: " << nb_th << endl;
+
+                // select a method to construct the SOG
+                unsigned int constructionOption;
+                if (method == "p")
+                {
                     cout << "Construction with pthread library." << endl;
-                    DR.computeDSOG(g, 0);
-                    g.printCompleteInformation();
-                } else if (!strcmp(argv[1], "pc")) {
+                    constructionOption = 0;
+                }
+                else if (method == "pc")
+                {
                     cout << "Canonized construction with pthread library." << endl;
-                    DR.computeDSOG(g, 1);
-                    g.printCompleteInformation();
-                } else {
+                    constructionOption = 1;
+                }
+                else
+                {
                     cout << "Partial Order Reduction with pthread library." << endl;
-                    DR.computeDSOG(g, 2);
-                    g.printCompleteInformation();
+                    constructionOption = 2;
                 }
 
-                cout << "Perform Model checking ?";
+                // build the distributed SOG
+                DR.computeDSOG(g, constructionOption);
+
+                // print SOG information
+                g.printCompleteInformation();
+
+                cout << "\nPerform Model checking? ";
                 char c;
                 cin >> c;
-                if (c == 'y') {
-                    cout << "Building automata for not(formula)\n";
+                if (c == 'y')
+                {
                     auto d = spot::make_bdd_dict();
 
-                    spot::twa_graph_ptr af = spot::translator(d).run(not_f);
-                    cout << "Formula automata built.\n";
-                    cout << "Want to save the graph in a dot file ?";
+                    // build the negation of the formula
+                    spot::twa_graph_ptr af = formula2Automaton(negate_formula.f, d);
+                    cout << "Want to save the automata of the formula in a dot file? ";
                     cin >> c;
-                    if (c == 'y') {
-                        fstream file;
-                        string st(formula);
-                        st += ".dot";
-                        file.open(st.c_str(), fstream::out);
-                        spot::print_dot(file, af);
-                        file.close();
+                    if (c == 'y')
+                    {
+                        saveGraph(af, formula + ".dot");
                     }
-                    //auto k = std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP(),R.getListPlaceAP());
 
+                    // build a twa graph of the SOG
+                    // TODO: Why do we translate the SOG into twa ?
+                    cout << "\n\nTranslating SOG to SPOT ..." << endl;
                     spot::twa_graph_ptr k = spot::make_twa_graph(
-                            std::make_shared<SogKripke>(d, DR.getGraph(), Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP()),
-                            spot::twa::prop_set::all(), true);
-
-                    cout << "SOG translated to SPOT succeeded.." << endl;
-                    cout << "Want to save the graph in a dot file ?";
+                        std::make_shared<SogKripke>(d, DR.getGraph(), Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP()),
+                        spot::twa::prop_set::all(), true);
+                    cout << "\nWant to save the SOG in a dot file? ";
                     cin >> c;
-                    if (c == 'y') {
-                        fstream file;
-                        string st(argv[3]);
-                        st += ".dot";
-                        file.open(st.c_str(), fstream::out);
-                        spot::print_dot(file, k, "ka");
-                        file.close();
+                    if (c == 'y')
+                    {
+                        saveGraph(af, net + ".dot", "ka");
                     }
-                    if (auto run = k->intersecting_run(af)) {
+                    cout << endl;
+
+                    // computes the explicit synchronization product
+                    auto run = k->intersecting_run(af);
+                    displayCheckResult(run == nullptr);
+
+                    // display a counter-example if it exists
+                    if (run)
+                    {
                         run->highlight(5);
-                        fstream file;
-                        file.open("violated.dot", fstream::out);
-                        cout << "Property is violated" << endl;
-                        cout << "Check the dot file to get a violation run" << endl;
-                        spot::print_dot(file, k, ".kA");
-                        file.close();
-                    } else
-                        std::cout << "formula is verified\n";
+                        saveGraph(k, "counter-example.dot", ".kA");
+                        cout << "Check the dot file to get a counter-example" << endl;
+                    }
                 }
-
             }
         }
     }
+    /**************************************************************************
+     * Hybrid version
+     **************************************************************************/
+    else
+    {
+        if (task_id == 0)
+            cout << "\n************** Hybrid version ****************\n"
+                 << endl;
 
-    if (n_tasks > 1) {
-        if (nb_th > 1) {
-            if (task_id == 0)
-                cout << "**************Hybrid version**************** \n" << endl;
-            if (strcmp(argv[1], "otf") && strcmp(argv[1], "otfPR") && strcmp(argv[1], "otfPOR") && strcmp(argv[1], "otfPRPOR")  ) {
-                HybridSOG DR(Rnewnet);
-                LDDGraph g(&DR);
-                if (task_id == 0)
-                    cout << "Building the Distributed SOG by " << n_tasks << " processes..." << endl;
-                DR.computeDSOG(g);
-            } else {
-                n_tasks--;
-                if (task_id == n_tasks) {
-                    cout << "Model checking on the fly..." << endl;
-                    cout << " One process will perform Model checking" << endl;
-                    cout << n_tasks << " process will build the Distributed SOG" << endl;
-                }
-                MPI_Comm gprocess;
-                MPI_Comm_split(MPI_COMM_WORLD, task_id == n_tasks ? 0 : 1, task_id, &gprocess);
-                //cout<<" Task id "<<task_id<<"/"<<n_tasks<<endl;
-                if (task_id != n_tasks) {
-                    cout << "N task :" << n_tasks << endl;
-                    CommonSOG* DR;
-                    if (strcmp(argv[1], "otf")==0) {
-                        cout<<"Normal construction..."<<endl;
-                        DR= new MCHybridSOG(Rnewnet, gprocess, false);
-                    }
-                    else if (strcmp(argv[1], "otfPOR")==0) {
-                        cout<<"Normal construction with POR"<<endl;
-                        DR= new MCHybridSOGPOR(Rnewnet, gprocess, false);
-                    }
-                    else if (strcmp(argv[1], "otfPR")==0) {
-                        cout<<"Progressive construction..."<<endl;
-                        DR= new MCHybridSOGReq(Rnewnet, gprocess, false);
-                    }
-                    else {
-                        cout<<"Progressive construction with POR..."<<endl;
-                        DR= new MCHybridSOGReqPOR(Rnewnet, gprocess, false);
-                    }
-                    LDDGraph g(DR);
-                    DR->computeDSOG(g);
-                } else {
-                    cout << "************************************" << endl;
-                    cout << "On the fly Model checker by process " << task_id << endl;
-                    auto d = spot::make_bdd_dict();
-                    spot::twa_graph_ptr af = spot::translator(d).run(not_f);
-                    auto k = std::make_shared<HybridKripke>(d, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP(), Rnewnet);
-                    if (strcmp(algorithm, "")) {
-                        std::shared_ptr < spot::twa_product > product = make_shared<spot::twa_product>(af, k);
-                        const char *err;
-                        spot::emptiness_check_instantiator_ptr echeck_inst = spot::make_emptiness_check_instantiator(algorithm, &err);
-
-                        if (!echeck_inst) {
-                            cerr << "Failed to parse argument near `" << err << "'" << endl;
-                            cerr << "Spot unknown emptiness algorithm" << endl;
-                            exit(2);
-                        }
-                        else
-                            cout<<"Spot emptiness check algorithm : "<<algorithm<<endl;
-                        auto startTime = std::chrono::high_resolution_clock::now();
-                        spot::emptiness_check_ptr echptr = echeck_inst->instantiate(product);
-                        bool res = (echptr->check() == nullptr);
-                        auto finalTime = std::chrono::high_resolution_clock::now();
-                        displayTime(startTime, finalTime);
-                        displayCheckResult(res);
-                    } else {
-                        auto startTime = std::chrono::steady_clock::now();
-                        bool res = (k->intersecting_run(af) == nullptr);
-                        auto finalTime = std::chrono::steady_clock::now();
-                        displayTime(startTime, finalTime);
-                        displayCheckResult(res);
-                    }
-                }
+        // On-the-fly hybrid model checking
+        if (isValidHybridMCOption(nb_th, method))
+        {
+            n_tasks--;
+
+            // ID of the task performing the model checking
+            int mc_task = n_tasks;
+
+            // display information about model checking processes
+            if (task_id == mc_task)
+            {
+                cout << "Model checking on the fly..." << endl;
+                cout << " 1 process will perform Model checking" << endl;
+                cout << " " << n_tasks << " process(es) will build the Distributed SOG" << endl;
+            }
+
+            // creates model-checking process
+            MPI_Comm gprocess;
+            MPI_Comm_split(MPI_COMM_WORLD, task_id == mc_task ? 0 : 1, task_id, &gprocess);
+
+            // computes the SOG in processes different to the model-checker one
+            if (task_id != mc_task)
+            {
+                CommonSOG *DR = getHybridMC(Rnewnet, method, gprocess);
+                cout << "# tasks: " << n_tasks << endl;
+
+                // compute the distributed SOG
+                LDDGraph g(DR);
+                DR->computeDSOG(g);
+            }
+            else // computes the on-the-fly model-checking in the mc process
+            {
+                cout << "On the fly Model checker by process " << task_id << endl;
+
+                // build the negation of the formula
+                auto d = spot::make_bdd_dict();
+                spot::twa_graph_ptr af = formula2Automaton(negate_formula.f, d);
+
+                // build the SOG
+                auto k = std::make_shared<HybridKripke>(d, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP(), Rnewnet);
+
+                runOnTheFlyMC(algorithm, k, af);
             }
         }
+        else // build only the SOG
+        {
+            HybridSOG DR(Rnewnet);
+            LDDGraph g(&DR);
+            cout << endl;
+
+            if (task_id == 0)
+                cout << "Building the Distributed SOG by " << n_tasks << " processes..." << endl;
+
+            // computes the distributed SOG
+            DR.computeDSOG(g);
+        }
     }
+
     MPI_Finalize();
-	return (EXIT_SUCCESS);
-}
+    return (EXIT_SUCCESS);
+}
\ No newline at end of file