From 60ce3c2261219aaf6fc0fb5f00490e313b57ebe4 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Sun, 22 Mar 2020 01:44:28 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20README.md=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/main.cpp?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
README.md | 4 +++-
src/main.cpp | 19 ++++++++++---------
2 files changed, 13 insertions(+), 10 deletions(-)
diff --git a/README.md b/README.md
index 7e64838..3b7311f 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 d9d482e..800d3b4 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);
}
--
GitLab