modifié : README.md

	modifié :         src/main.cpp

README.md

@@ -45,7 +45,7 @@ SOG building from an LTL formula (philo3.net example)
 ```
 Multi-threading execution
 
-mpirun -n 1 hybrid-sog arg1 arg 2 arg3 arg4
+mpirun -n 1 hybrid-sog arg1 arg2 arg3 arg4 [arg5]
 arg1: specifies method of creating threads or/and specifies if modelchecking should be performed on the fly. It can be set with one of the following values:
      * p : using pthread library
      * pc : using pthread library and applying canonization on nodes
@@ -56,6 +56,8 @@ arg1: specifies method of creating threads or/and specifies if modelchecking sho
 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
 
 Distributed execution
 mpirun -n arg0 hybrid-sog arg1 arg 2 arg3 arg4

src/main.cpp

@@ -80,6 +80,7 @@ void displayCheckResult(bool res) {
 void displayTime(auto startTime, auto finalTime) {
 	cout << "Verification duration : " << std::chrono::duration_cast < std::chrono::milliseconds
 			> (finalTime - startTime).count() << " milliseconds\n";
+
 }
 /***********************************************/
 int main(int argc, char **argv) {
@@ -151,17 +152,17 @@ int main(int argc, char **argv) {
 			if (!strcmp(algorithm, "couv")) {
 				cout << "Couvreur99 algorithm..." << endl;
 				std::shared_ptr < spot::twa_product > product = make_shared<spot::twa_product>(af, k);
-				spot::couvreur99_check check = spot::couvreur99_check(product);
-				auto startTime = std::chrono::high_resolution_clock::now();
+				spot::couvreur99_check_shy check = spot::couvreur99_check_shy(product);
+				auto startTime = std::chrono::steady_clock::now();
 				bool res = (check.check() == 0);
-				auto finalTime = std::chrono::high_resolution_clock::now();
+				auto finalTime = std::chrono::steady_clock::now();
 				displayTime(startTime, finalTime);
 				displayCheckResult(res);
 
 			} else {
-				auto startTime = std::chrono::high_resolution_clock::now();
+				auto startTime = std::chrono::steady_clock::now();
 				bool res = (k->intersecting_run(af) == 0);
-				auto finalTime = std::chrono::high_resolution_clock::now();
+				auto finalTime = std::chrono::steady_clock::now();
 				displayTime(startTime, finalTime);
 				displayCheckResult(res);
 				/*
@@ -305,15 +306,15 @@ int main(int argc, char **argv) {
 					if (!strcmp(algorithm,"couv")) {
 						std::shared_ptr < spot::twa_product > product = make_shared<spot::twa_product>(af, k);
 						spot::couvreur99_check check = spot::couvreur99_check(product);
-						auto startTime = std::chrono::high_resolution_clock::now();
+						auto startTime = std::chrono::steady_clock::now();
 						bool res = (check.check() == 0);
-						auto finalTime = std::chrono::high_resolution_clock::now();
+						auto finalTime = std::chrono::steady_clock::now();
 						displayTime(startTime, finalTime);
 						displayCheckResult(res);
 					} else {
-						auto startTime = std::chrono::high_resolution_clock::now();
+						auto startTime = std::chrono::steady_clock::now();
 						bool res= (k->intersecting_run(af)==0);
-						auto finalTime = std::chrono::high_resolution_clock::now();
+						auto finalTime = std::chrono::steady_clock::now();
 						displayTime(startTime, finalTime);
 						displayCheckResult(res);
 					}