diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index ec66b0a03cf2741e6babd9f332f497a25c4ace4c..3a31882230faef5bb8842329f107e46380b6a26d 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -49,7 +49,8 @@ add_executable(pmc-sog main.cpp
   LDDState.cpp
   LDDState.h
   TransSylvan.cpp
-
+  algorithm/CNDFS.h
+  algorithm/CNDFS.cpp
   SpotSogState.cpp
   SpotSogState.h
   SpotSogIterator.cpp
diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp
index 7fbbe510552b271fb9d3aacb8f75c04bfd2f9522..6c2c0a72206de74860c5620a12765a1a7e7cdf12 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -2,11 +2,15 @@
 // Created by ghofrane on 5/4/22.
 //
 #include "CNDFS.h"
+#include "ModelCheckBaseMT.h"
 #include <iostream>
+#include <spot/tl/apcollect.hh>
+#include <spot/twa/twagraph.hh>
 using namespace std;
 
 CNDFS::~CNDFS()=default;
 
-void CNDFS::DfsBlue() {
-    cout << "hello from cndfs class" << endl;
+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;
 }
\ No newline at end of file
diff --git a/src/algorithm/CNDFS.h b/src/algorithm/CNDFS.h
index f7a0484796860742448b27838bad57791abc6c52..81011a6e6e314076c63506f6b90aab1204fde0a5 100644
--- a/src/algorithm/CNDFS.h
+++ b/src/algorithm/CNDFS.h
@@ -4,12 +4,12 @@
 
 #ifndef PMC_SOG_CNDFS_H
 #define PMC_SOG_CNDFS_H
-
+#include "ModelCheckBaseMT.h"
+#include <spot/tl/apcollect.hh>
 class CNDFS {
 public:
-
     virtual ~CNDFS();
-    void DfsBlue();
+    void DfsBlue(ModelCheckBaseMT &mcl, shared_ptr<spot::twa_graph> af);
 };
 
 
diff --git a/src/main.cpp b/src/main.cpp
index b4b79478f61c8ed3ecc461e6d8d4917c2e7faa6b..01fb4152540b43211724769e1afa3270cdbd32d3 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -36,7 +36,7 @@
 #include "Hybrid/MCHybridReqPOR/MCHybridSOGReqPOR.h"
 #include "Hybrid/MCHybridPOR/MCHybridSOGPOR.h"
 #include "algorithm/CNDFS.h"
-
+#include <typeinfo>
 
 using namespace std;
 
@@ -509,6 +509,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);
+            shared_ptr<spot::twa_graph> aa = formula2Automaton(negate_formula.f, d, dot_formula);
 
             // create the SOG
             mcl->loadNet();
@@ -517,10 +518,13 @@ int main(int argc, char **argv)
             // TODO: Implement here Ghofrane's algorithms
             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 << "HELLO" << endl;
-                 CNDFS n;
-                 n.DfsBlue();
+                CNDFS n;
+                 //n.DfsBlue();
+                 n.DfsBlue(*mcl, aa);
                  return(0);
                 //exit(0);
 
@@ -528,7 +532,7 @@ int main(int argc, char **argv)
             else // run on the fly sequential model-checking
             {
                 auto k = std::make_shared<SogKripkeTh>(d, mcl, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP());
-                runOnTheFlyMC(algorithm, k, af);
+                //runOnTheFlyMC(algorithm, k, af);
             }
 
             // stop model checker process
diff --git a/src/threadSOG.cpp b/src/threadSOG.cpp
index 303bb7092973b097343d6468f6735fb1fe3dc53a..dab83310167345d5b6424c64e7748243112334c8 100644
--- a/src/threadSOG.cpp
+++ b/src/threadSOG.cpp
@@ -6,8 +6,6 @@
 #include "threadSOG.h"
 
 
-
-
 /*
 void write_to_dot(const char *ch,MDD m)
 {