From e30f269c182235519d1b7959ba86af016ec80c94 Mon Sep 17 00:00:00 2001
From: Ghofrane Amaimi <ghofraneeamaimi@gmail.com>
Date: Mon, 9 May 2022 16:37:22 +0200
Subject: [PATCH] 2 threads work safely
---
src/algorithm/CNDFS.cpp | 69 ++++++++++++++++++++++++++++++++---------
src/algorithm/CNDFS.h | 10 +++++-
src/main.cpp | 29 ++++++++++-------
3 files changed, 80 insertions(+), 28 deletions(-)
diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp
index 640d974..e4b188c 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -1,34 +1,73 @@
//
// Created by ghofrane on 5/4/22.
//
+
#include "CNDFS.h"
#include "ModelCheckBaseMT.h"
#include <iostream>
#include <spot/twa/twagraph.hh>
#include <thread>
#include <vector>
-
+#include <spot/twa/twaproduct.hh>
+#include <spot/twa/twa.hh>
using namespace std;
+
bool red=false;
bool blue=false;
thread_local bool cyan = false;
+struct product_node{
+
+};
+std::mutex mtx;
+
+//CNDFS::CNDFS(auto mK, const shared_ptr<spot::twa_graph> &mAa) : mK(mK), mAa(mAa) {}
CNDFS::~CNDFS()=default;
-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;
+//structure qui represente le produit de 2 états
+
+ void CNDFS::DfsBlue(ModelCheckBaseMT &mcl,shared_ptr<spot::twa_graph> a) {
+ // mMcl = &m;
+ //cout << "First state SOG from CNDFS " << mMcl->getInitialMetaState() << endl;
+ //cout << "First state SOG from CNDFS " << typeid(m.getGraph()->getInitialAggregate()->getSuccessors()).name() << endl;
+ //cout << "First state BA from CNDFS " << a->get_init_state()<<endl;
+
+
+ //iterate succ of BA initial state
+ //mtx.lock();
+ spot::twa_succ_iterator* i = a->succ_iter(a->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());
+ a->release_iter(i);
+ //mtx.unlock();
+
+ //iterate succ of SOG first state
+ vector<pair<LDDState*, int>> * edges =m.getGraph()->getInitialAggregate()->getSuccessors();
+ for (const auto& pair : *edges)
+ {
+ std::cout << "sog succ list "<< 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
+
+
+//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();
+//
+// }
+//}
+
diff --git a/src/algorithm/CNDFS.h b/src/algorithm/CNDFS.h
index 2591afc..edda143 100644
--- a/src/algorithm/CNDFS.h
+++ b/src/algorithm/CNDFS.h
@@ -5,12 +5,20 @@
#ifndef PMC_SOG_CNDFS_H
#define PMC_SOG_CNDFS_H
#include "ModelCheckBaseMT.h"
+#include "SogKripkeTh.h"
#include <spot/tl/apcollect.hh>
class CNDFS {
+
+private:
+ //ModelCheckBaseMT& mMcl;
+ //shared_ptr<spot::twa_graph> mAa;
public:
+ //CNDFS(auto mK, const shared_ptr<spot::twa_graph> &mAa);
+
virtual ~CNDFS();
+ //static void DfsBlue();
static void DfsBlue(ModelCheckBaseMT &mcl, shared_ptr<spot::twa_graph> af);
- static void spawnThreads(int n, 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 8a4abda..f26d17e 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -38,7 +38,8 @@
#include "algorithm/CNDFS.h"
#include <typeinfo>
#include <atomic>
-
+#include <thread>
+#include <vector>
using namespace std;
int n_tasks, task_id;
@@ -350,6 +351,7 @@ bool runOnTheFlyMC(const string &algorithm, auto k, spot::twa_graph_ptr af)
// set the synchronized product of the SOG and the negated formula
shared_ptr<spot::twa_product> product = make_shared<spot::twa_product>(k, af);
+
// set the emptiness check
const char *err;
spot::emptiness_check_instantiator_ptr echeck_inst = spot::make_emptiness_check_instantiator(algorithm.c_str(), &err);
@@ -391,7 +393,7 @@ bool runOnTheFlyMC(const string &algorithm, auto k, spot::twa_graph_ptr af)
*
* TODO: implement this
*/
-bool runOnTheFlyParallelMC(const string &algorithm) {}
+//bool runOnTheFlyParallelMC(const string &algorithm) {}
/******************************************************************************
* Main function
@@ -510,6 +512,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);
@@ -520,14 +523,17 @@ 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(aa).name() <<endl;
-
- //atomic<ModelCheckBaseMT> (*mcl);
- //shared_ptr< atomic<spot::twa_graph>> aa;
- CNDFS n;
- //n.DfsBlue(*mcl, aa);
- n.spawnThreads(4,*mcl,aa);
+
+// cout<<"pointeur sur sog "<< typeid(mcl).name() <<endl;
+// cout <<"pointeur sur BA "<< typeid(aa).name() <<endl;
+
+ CNDFS cndfs;
+ //cndfs.DfsBlue(*mcl, aa);
+ thread thread_1 (cndfs.DfsBlue,ref(*mcl),ref(aa));
+ thread thread_2 (cndfs.DfsBlue,ref(*mcl),ref(aa));
+ thread_1.join();
+ thread_2.join();
+ // n.spawnThreads(2,*mcl,aa);
return(0);
}
@@ -575,7 +581,6 @@ int main(int argc, char **argv)
// print SOG information
g.printCompleteInformation();
-
// run model checking process
if (!only_sog)
{
@@ -655,7 +660,7 @@ int main(int argc, char **argv)
// build the SOG
auto k = std::make_shared<HybridKripke>(d, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP(), Rnewnet);
- runOnTheFlyMC(algorithm, k, af);
+ // runOnTheFlyMC(algorithm, k, af);
}
}
else // build only the SOG
--
GitLab