diff --git a/README.md b/README.md index 7e648388447c9997e83d55dcd27954a40f645b66..3b7311f948aa3515380564687956aabeb0904b37 100644 --- a/README.md +++ b/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 diff --git a/src/main.cpp b/src/main.cpp index d9d482e7d632683e489122f11a5de40a1818f35f..800d3b4abd1f329668c21ced3944391c16aa8048 100644 --- a/src/main.cpp +++ b/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); }