diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp
index c29ddcbbd872951b103a0ec1641ae34ed96aecc2..bc0d2918b856fbc5844655bc1fdc76ac749d228b 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -10,35 +10,42 @@
#include <vector>
#include <spot/twa/twaproduct.hh>
#include <spot/twa/twa.hh>
+
using namespace std;
-bool red=false;
-bool blue=false;
+bool red = false;
+bool blue = false;
thread_local bool cyan = false;
-struct new_state{
+struct new_state {
ModelCheckBaseMT &left;
shared_ptr<spot::twa_graph> right;
};
-struct new_state_succ{
+struct new_state_succ {
LDDState *succ_left;
spot::twa_succ_iterator *succ_right;
};
vector<new_state_succ> successors_new_node;
-std::mutex mtx;
-//j'ai un problème de passage des paramétres dans le constructeur(pointeur vs adresse)
-//CNDFS::CNDFS(ModelCheckBaseMT *mMcl, const shared_ptr<spot::twa_graph> &mAa) : mMcl(mMcl), mAa(mAa) {}
-CNDFS::~CNDFS()=default;
-//structure qui represente le produit de 2 états
+CNDFS::CNDFS(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh) : mMcl(mcl), mAa(af),
+ mNbTh(nbTh) {}
+
+CNDFS::~CNDFS() {
+ for (int i = 0; i < mNbTh; ++i) {
+ mlThread[i]->join();
+ delete mlThread[i];
+ }
+}
- void CNDFS::DfsBlue() {
+//structure qui represente le produit de 2 états
+/*
+void CNDFS::DfsBlue() {
//cout << "First state SOG from CNDFS " << mMcl->getInitialMetaState() << endl;
//cout << "First state SOG from CNDFS " << typeid(m.getGraph()->getInitialAggregate()->getSuccessors()).name() << endl;
@@ -47,38 +54,42 @@ CNDFS::~CNDFS()=default;
//iterate succ of BA initial state
//mtx.lock();
- spot::twa_succ_iterator* i = mAa->succ_iter(mAa->get_init_state());
+ spot::twa_succ_iterator *i = mAa->succ_iter(mAa->get_init_state());
if (i->first())
- do
- {
- const std::lock_guard<std::mutex> lock(mtx);
- cout << "BA succ "<< i->dst() << "; in thread "
- << std::this_thread::get_id()<< endl;
- }
- while (i->next());
- mAa->release_iter(i);
+ do {
+ const std::lock_guard<std::mutex> lock(mMutex);
+ cout << "BA succ " << i->dst() << "; in thread "
+ << std::this_thread::get_id() << endl;
+ } while (i->next());
+ mAa->release_iter(i);
//mtx.unlock();
- //iterate succ of SOG first state
- //error: segmentation fault here don't know how to fix it
- vector<pair<LDDState*, int>> * edges =mMcl->getGraph()->getInitialAggregate()->getSuccessors();
- for (const auto& pair : *edges)
- {
- std::cout << "sog succ list "<< endl;
- }
+ //iterate succ of SOG first state
+ //error: segmentation fault here don't know how to fix it
+ vector<pair<LDDState *, int>> *edges = mMcl->getGraph()->getInitialAggregate()->getSuccessors();
+ for (const auto &pair: *edges) {
+ std::cout << "sog succ list " << endl;
+ }
}
+*/
+void CNDFS::spawnThreads() {
+ for (int i = 0; i < mNbTh; ++i) {
+ mlThread[i] = new thread(threadHandler, this);
+ if (mlThread[i] == nullptr) {
+ cout << "error: pthread creation failed. " << 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();
-//
-// }
-//}
+void CNDFS::threadHandler(void *context) {
+ ((CNDFS *) context)->computeProduct();
+}
+
+/*
+ * Compute the synchornized product
+ */
+void CNDFS::computeProduct() {
+
+}
\ No newline at end of file
diff --git a/src/algorithm/CNDFS.h b/src/algorithm/CNDFS.h
index 8e18943a8995dc2bbae3e439a884f77252c292cb..13fd7767b23019f93ba7fe899047879586479f94 100644
--- a/src/algorithm/CNDFS.h
+++ b/src/algorithm/CNDFS.h
@@ -5,25 +5,26 @@
#ifndef PMC_SOG_CNDFS_H
#define PMC_SOG_CNDFS_H
#include "../ModelCheckBaseMT.h"
-
#include <spot/tl/apcollect.hh>
+#include <cstdint>
+#include <thread>
class CNDFS {
private:
- ModelCheckBaseMT *mMcl;
- shared_ptr<spot::twa_graph> mAa;
+ static constexpr uint8_t MAX_THREADS=64;
+ ModelCheckBaseMT * mMcl;
+ spot::twa_graph_ptr mAa;
uint16_t mNbTh;
+ atomic<uint8_t> mIdThread;
+ static void threadHandler(void *context);
+ std::thread* mlThread[MAX_THREADS];
+ std::mutex mMutex;
+ void spawnThreads();
public:
- //CNDFS(ModelCheckBaseMT *mMcl, const shared_ptr<spot::twa_graph> &mAa);
- CNDFS(ModelCheckBaseMT &mcl,shared_ptr<spot::twa_graph> af,const uint16_t& nbTh) {
- mMcl=&mcl;
- mAa=af;
- mNbTh=nbTh; // nulber of threads to be created
- }
+ CNDFS(ModelCheckBaseMT *mcl,const spot::twa_graph_ptr &af,const uint16_t& nbTh);
virtual ~CNDFS();
//static void DfsBlue();
- void DfsBlue();
- // static void spawnThreads(int n, ModelCheckBaseMT &mcl, shared_ptr<spot::twa_graph> af);
+ void computeProduct();
};
diff --git a/src/main.cpp b/src/main.cpp
index 74300569e96ca30e41f9d6d320f3b53b684b1a60..4354610abc0788019ed83042b6f34030b42898d8 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -206,8 +206,8 @@ ModelCheckBaseMT *getMultiCoreMC(NewNet &net, int nb_th, const string &thread_li
// select the right model-checking algorithm
if (thread_library == "posix")
- {
- if (progressive)
+ { if (progressive)
+
{
cout << "Multi-threaded algorithm (progressive) based on PThread!" << endl;
mcl = new ModelCheckThReq(net, nb_th);
@@ -513,10 +513,7 @@ int main(int argc, char **argv)
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
+ // create the SOG
mcl->loadNet();
// run on the fly parallel model-checking
@@ -527,7 +524,7 @@ int main(int argc, char **argv)
// cout<<"pointeur sur sog "<< typeid(mcl).name() <<endl;
// cout <<"pointeur sur BA "<< typeid(aa).name() <<endl;
- CNDFS cndfs(*mcl,aa,3);
+ CNDFS cndfs(mcl,af,3);
// You have now to call a non static method of object cndfs that will create threads and execute your dfs algorithm
// Your static method should be defined as private and called by a non static method