add SpawnThreads: not safe

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)

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

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);
 };
 
 

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