diff --git a/README.md b/README.md
index 3b7311f948aa3515380564687956aabeb0904b37..cda810a7845bbfc5dd436ec1b632e21c527d9533 100644
--- a/README.md
+++ b/README.md
@@ -53,11 +53,22 @@ arg1: specifies method of creating threads or/and specifies if modelchecking sho
      * lc : using lace framework and applying canonization on nodes
      * otfL : perform modelchecking on the fly using laceframework
      * otfP : perform modelchecking on the fly using pthread
-arg2: specifies the number of threads/workers to be created
-arg3: specifies the net to build its SOG
-arg4: specifies the LTL formula file
-arg5: (Optional)
-     * couv : Couvreur99 emptiness check algorithm provided by spot
+arg2: specify the number of threads/workers to be created
+arg3: specify the net to build its SOG
+arg4: specify the LTL formula file
+arg5: (Optional) select an algorithm for the emptiness check provided by spot, see https://spot.lrde.epita.fr/doxygen/group__emptiness__check.html 
+     * Cou99 
+	+ shy
+	+ poprem
+	+ group 
+     * GC04
+     * CVWY90
+	+ bsh : set the size of a hash-table
+     * SE05
+	+ bsh : set the size of a hash-table
+     * Tau03
+     * Tau03_opt
+      
 
 Distributed execution
 mpirun -n arg0 hybrid-sog arg1 arg 2 arg3 arg4
@@ -68,6 +79,18 @@ arg1: specifies whether modelchecking should be performed on the fly. It can be
 arg2: specifies the number of threads/workers to be created
 arg3: specifies the net to build its SOG
 arg4: specifies the LTL formula file
+arg5: (Optional) select an algorithm for the emptiness check provided by spot, see https://spot.lrde.epita.fr/doxygen/group__emptiness__check>
+     * Cou99 
+        + shy
+        + poprem
+        + group
+     * GC04
+     * CVWY90
+        + bsh : set the size of a hash-table
+     * SE05
+        + bsh : set the size of a hash-table
+     * Tau03
+     * Tau03_opt
 
 ```
 ## Publications
diff --git a/src/main.cpp b/src/main.cpp
index 800d3b4abd1f329668c21ced3944391c16aa8048..9facf97ff683f1a981f8e9cc9e2a70a5d5f4d59f 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -149,15 +149,32 @@ int main(int argc, char **argv) {
 			mcl->loadNet();
 			auto k = std::make_shared<SogKripkeTh>(d, mcl, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP());
 			cout << "Performing on the fly Modelchecking" << endl;
-			if (!strcmp(algorithm, "couv")) {
+			if (strcmp(algorithm, "")) {
 				cout << "Couvreur99 algorithm..." << endl;
-				std::shared_ptr < spot::twa_product > product = make_shared<spot::twa_product>(af, k);
-				spot::couvreur99_check_shy check = spot::couvreur99_check_shy(product);
+				shared_ptr < spot::twa_product > product = make_shared<spot::twa_product>(af, k);
+				//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);
+				}
+				spot::emptiness_check_ptr echptr = echeck_inst->instantiate(product);
 				auto startTime = std::chrono::steady_clock::now();
-				bool res = (check.check() == 0);
+				bool res = (echptr->check() == 0);
 				auto finalTime = std::chrono::steady_clock::now();
 				displayTime(startTime, finalTime);
 				displayCheckResult(res);
+				/****************************/
+
+				/*auto startTime = std::chrono::steady_clock::now();
+				 bool res = (check.check() == 0);
+				 auto finalTime = std::chrono::steady_clock::now();
+				 displayTime(startTime, finalTime);
+				 displayCheckResult(res);*/
 
 			} else {
 				auto startTime = std::chrono::steady_clock::now();
@@ -303,17 +320,31 @@ int main(int argc, char **argv) {
 					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,"couv")) {
+					if (strcmp(algorithm, "")) {
 						std::shared_ptr < spot::twa_product > product = make_shared<spot::twa_product>(af, k);
-						spot::couvreur99_check check = spot::couvreur99_check(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);
+						}
+						spot::emptiness_check_ptr echptr = echeck_inst->instantiate(product);
 						auto startTime = std::chrono::steady_clock::now();
-						bool res = (check.check() == 0);
+						bool res = (echptr->check() == 0);
 						auto finalTime = std::chrono::steady_clock::now();
 						displayTime(startTime, finalTime);
 						displayCheckResult(res);
+						/*spot::couvreur99_check check = spot::couvreur99_check(product);
+						 auto startTime = std::chrono::steady_clock::now();
+						 bool res = (check.check() == 0);
+						 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)==0);
+						bool res = (k->intersecting_run(af) == 0);
 						auto finalTime = std::chrono::steady_clock::now();
 						displayTime(startTime, finalTime);
 						displayCheckResult(res);