From 2d4749426c4fa610fc3b7c2f5aff0bf7d2010e41 Mon Sep 17 00:00:00 2001
From: Ghofrane Amaimi <ghofraneeamaimi@gmail.com>
Date: Fri, 6 May 2022 12:26:22 +0200
Subject: [PATCH] add SpawnThreads: not safe
---
CMakeLists.txt | 2 ++
src/algorithm/CNDFS.cpp | 26 ++++++++++++++++++++++----
src/algorithm/CNDFS.h | 3 ++-
src/main.cpp | 14 ++++++++------
4 files changed, 34 insertions(+), 11 deletions(-)
diff --git a/CMakeLists.txt b/CMakeLists.txt
index cc9ffb2..4269e84 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -68,6 +68,8 @@ target_include_directories(cli11 INTERFACE "${THIRD_PARTY_INCLUDE_DIR}/cli11")
include_directories(src)
add_subdirectory(src)
+set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -pthread")
+
# add tests
# enable_testing()
# add_subdirectory(tests)
diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp
index 6c2c0a7..640d974 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -4,13 +4,31 @@
#include "CNDFS.h"
#include "ModelCheckBaseMT.h"
#include <iostream>
-#include <spot/tl/apcollect.hh>
#include <spot/twa/twagraph.hh>
+#include <thread>
+#include <vector>
+
using namespace std;
+bool red=false;
+bool blue=false;
+thread_local bool cyan = false;
+
CNDFS::~CNDFS()=default;
-void CNDFS::DfsBlue( ModelCheckBaseMT &mcl, shared_ptr<spot::twa_graph> af) {
- cout << "First state SOG from CNDFS " << mcl.getInitialMetaState() << endl;
- cout << "First state BA from CNDFS " << af->acc() <<endl;
+void CNDFS::DfsBlue(ModelCheckBaseMT &m,shared_ptr<spot::twa_graph> a) {
+ cout << "First state SOG from CNDFS " << m.getInitialMetaState() << endl;
+ cout << "First state BA from CNDFS " << a->get_init_state()<<endl;
+}
+
+void CNDFS::spawnThreads(int n, ModelCheckBaseMT &mcl, shared_ptr<spot::twa_graph> af )
+{
+ std::vector<thread> threads(n);
+ // spawn n threads:
+ for (int i = 0; i < n; i++) {
+ threads.push_back(thread(DfsBlue,ref(mcl),af));
+ }
+ for (auto& th : threads) {
+ th.join();
+ }
}
\ No newline at end of file
diff --git a/src/algorithm/CNDFS.h b/src/algorithm/CNDFS.h
index 81011a6..2591afc 100644
--- a/src/algorithm/CNDFS.h
+++ b/src/algorithm/CNDFS.h
@@ -9,7 +9,8 @@
class CNDFS {
public:
virtual ~CNDFS();
- void DfsBlue(ModelCheckBaseMT &mcl, shared_ptr<spot::twa_graph> af);
+ static void DfsBlue(ModelCheckBaseMT &mcl, shared_ptr<spot::twa_graph> af);
+ static void spawnThreads(int n, ModelCheckBaseMT &mcl, shared_ptr<spot::twa_graph> af);
};
diff --git a/src/main.cpp b/src/main.cpp
index 01fb415..8a4abda 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -37,6 +37,7 @@
#include "Hybrid/MCHybridPOR/MCHybridSOGPOR.h"
#include "algorithm/CNDFS.h"
#include <typeinfo>
+#include <atomic>
using namespace std;
@@ -509,6 +510,7 @@ int main(int argc, char **argv)
// build automata of the negation of the formula
auto d = spot::make_bdd_dict();
spot::twa_graph_ptr af = formula2Automaton(negate_formula.f, d, dot_formula);
+ // twa_graph class
shared_ptr<spot::twa_graph> aa = formula2Automaton(negate_formula.f, d, dot_formula);
// create the SOG
@@ -519,14 +521,14 @@ int main(int argc, char **argv)
if (algorithm == "UFSCC" || algorithm == "CNDFS")
{
cout<<"pointeur sur le sog "<< typeid(mcl).name() <<endl;
- //cout << "pointeur sur le BA "<< typeid(af).name() <<endl;
- cout << "pointeur sur le BA "<< typeid(aa).name() <<endl;
+ cout <<"pointeur sur le BA "<< typeid(aa).name() <<endl;
+ //atomic<ModelCheckBaseMT> (*mcl);
+ //shared_ptr< atomic<spot::twa_graph>> aa;
CNDFS n;
- //n.DfsBlue();
- n.DfsBlue(*mcl, aa);
- return(0);
- //exit(0);
+ //n.DfsBlue(*mcl, aa);
+ n.spawnThreads(4,*mcl,aa);
+ return(0);
}
else // run on the fly sequential model-checking
--
GitLab