From 554c9765bf1c40135a0354ddd9155c05d9b90c52 Mon Sep 17 00:00:00 2001
From: chihebabid <chiheb.abid@fst.utm.tn>
Date: Sun, 3 Jul 2022 23:46:20 +0100
Subject: [PATCH] Refactoring to C++17
---
src/algorithm/CNDFS.cpp | 33 ++++++++++++++++-----------------
src/algorithm/CNDFS.h | 32 +++++++++++++++-----------------
src/misc/SafeDequeue.cpp | 4 ++--
src/misc/SafeDequeue.h | 2 +-
4 files changed, 34 insertions(+), 37 deletions(-)
diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp
index 6786df6..b093999 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -49,7 +49,7 @@ void CNDFS::threadHandler(void *context) {
//get initial state of the product automata
void CNDFS::getInitialState(){
- mInitStatePtr = new _state; //static_cast<_state *>(malloc(sizeof(_state)));
+ mInitStatePtr = new myState_t; //static_cast<_state *>(malloc(sizeof(_state)));
mInitStatePtr->left = mMcl->getInitialMetaState();
mInitStatePtr->right = mAa->get_init_state();
//mInitStatePtr->new_successors = nullptr;
@@ -59,14 +59,13 @@ void CNDFS::getInitialState(){
//this function is to build a state with list of successor initially null
-_state* CNDFS::buildState(LDDState* left, spot::state* right, bool acc, bool constructed, bool cyan){
+myState_t* CNDFS::buildState(LDDState* left, spot::state* right, bool acc, bool constructed, bool cyan){
bool _cyan{false};
mMutex.lock();
- _state * buildStatePtr = static_cast<_state *>(malloc(sizeof(_state)));
+ myState_t * buildStatePtr = static_cast<myState_t *>(malloc(sizeof(myState_t)));
_cyan = cyan;
buildStatePtr->left = left;
buildStatePtr->right = dynamic_cast<const spot::twa_graph_state *>(right);
- buildStatePtr->new_successors = static_cast<vector<pair<_state *, int>>>(NULL);
buildStatePtr->isAcceptance = acc;
buildStatePtr->isConstructed = constructed;
buildStatePtr->cyan= _cyan;
@@ -74,7 +73,7 @@ _state* CNDFS::buildState(LDDState* left, spot::state* right, bool acc, bool con
return buildStatePtr;
}
-std::ostream & operator<<(std::ostream & Str,_state* state) {
+std::ostream & operator<<(std::ostream & Str,myState_t* state) {
Str << "({ Sog state= " << state->left << ", BA state= " << state->right << ", acceptance= " << state->isAcceptance << ", constructed= " << state->isConstructed << ", cyan= " << state->cyan << ", red= " << state->red << ", blue= " << state->blue << " }" << endl;
int i = 0;
for (auto ii : state->new_successors)
@@ -86,7 +85,7 @@ std::ostream & operator<<(std::ostream & Str,_state* state) {
}
//all visited accepting nodes (non seed, non red) should be red
-atomic_bool CNDFS::awaitCondition(_state* state,deque<_state*> localDeque)
+atomic_bool CNDFS::awaitCondition(myState_t* state,deque<myState_t*> localDeque)
{
vector<bool> localList ;
for (auto qu: localDeque)
@@ -108,7 +107,7 @@ atomic_bool CNDFS::awaitCondition(_state* state,deque<_state*> localDeque)
// while ( awaitCondition(state) == false) ;
//}
-void CNDFS::dfsRed(_state* state,deque<_state*> localDeque)
+void CNDFS::dfsRed(myState_t* state,deque<myState_t*> localDeque)
{
cout << "dfsRed" << endl;
localDeque.push_back(state);
@@ -126,7 +125,7 @@ void CNDFS::dfsRed(_state* state,deque<_state*> localDeque)
}
//compute new successors of a product state
-void CNDFS::computeSuccessors(_state *state)
+void CNDFS::computeSuccessors(myState_t *state)
{
LDDState* sog_current_state = state->left;
const spot::twa_graph_state* ba_current_state = state->right;
@@ -134,7 +133,7 @@ void CNDFS::computeSuccessors(_state *state)
while (!sog_current_state->isCompletedSucc());
auto p = mAa->get_dict(); //avoir le dictionnaire bdd,proposition atomique
//fetch the state's atomic proposition
- for (auto vv: sog_current_state->getMarkedPlaces(mMcl->getPlaceProposition()))
+ for (const auto & vv: sog_current_state->getMarkedPlaces(mMcl->getPlaceProposition()))
{
string name = string(mMcl->getPlace(vv));
auto f = spot::formula::ap(name);
@@ -142,9 +141,9 @@ void CNDFS::computeSuccessors(_state *state)
cv.notify_one();
}
//iterate over the successors of a current aggregate
- for (int i = 0; i < sog_current_state->Successors.size(); i++)
+ for (const auto &elt : sog_current_state->Successors)
{
- int transition = sog_current_state->Successors.at(i).second; // je récupère le numéro du transition
+ int transition = elt.second; // je récupère le numéro du transition
auto name = string(mMcl->getTransition(transition)); // récuprer le nom de la transition
auto f = spot::formula::ap(name);// récuperer la proposition atomique qui correspond à la transition
transitionNames.push(f); // push state'S AP to edge'S AP
@@ -169,13 +168,13 @@ void CNDFS::computeSuccessors(_state *state)
{
//make a copy that we can iterate
// SafeDequeue<myCouple> tempSharedPool = sharedPool;
- SafeDequeue<_state*> tempSharedPool = sharedPoolTemp;
+ SafeDequeue<myState_t*> tempSharedPool = mSharedPoolTemp;
while (!tempSharedPool.empty())
{
std::lock_guard<std::mutex> guard(mMutex);
// if ((tempSharedPool.front().first == sog_current_state->Successors.at(i).first) &&
// (tempSharedPool.front().second == const_cast<spot::state *>(ii->dst())))
- if ((tempSharedPool.front()->left == sog_current_state->Successors.at(i).first) && (tempSharedPool.front()->right == const_cast<spot::state *>(ii->dst())))
+ if ((tempSharedPool.front()->left == elt.first) && (tempSharedPool.front()->right == const_cast<spot::state *>(ii->dst())))
{
// nd->cyan = true;
state->new_successors.push_back(make_pair(tempSharedPool.front(), transition));
@@ -183,7 +182,7 @@ void CNDFS::computeSuccessors(_state *state)
{
//new terminal state without successors
//state_is_accepting() should only be called on automata with state-based acceptance
- _state *nd = buildState(sog_current_state->Successors.at(i).first,
+ myState_t *nd = buildState(elt.first,
const_cast<spot::state *>(ii->dst()),
mAa->state_is_accepting(ii->dst()), true, false);
state->new_successors.push_back(make_pair(nd, transition));
@@ -206,14 +205,14 @@ void CNDFS::computeSuccessors(_state *state)
int i = 1;
//Perform the dfsBlue
-void CNDFS::dfsBlue(_state *state) {
- deque<_state*> localDeque;
+void CNDFS::dfsBlue(myState_t *state) {
+ deque<myState_t*> localDeque;
uint16_t idThread = mIdThread++;
cout<< "appel recursif " << i << endl;
i++;
state->cyan = true;
// sharedPool.push(myCouple (state->left,state->right));
- sharedPoolTemp.push(state);
+ mSharedPoolTemp.push(state);
cv.notify_one();
// new_successor.push(coupleSuccessor(state,2));
computeSuccessors(state);
diff --git a/src/algorithm/CNDFS.h b/src/algorithm/CNDFS.h
index f4b189c..32b5b22 100644
--- a/src/algorithm/CNDFS.h
+++ b/src/algorithm/CNDFS.h
@@ -14,19 +14,18 @@
#include "misc/SafeDequeue.h"
using namespace std ;
-typedef pair<struct myState*, int> coupleSuccessor;
+typedef pair<struct myState_t*, int> coupleSuccessor;
-struct myState{
+struct myState_t {
LDDState *left;
const spot::twa_graph_state* right;
- vector<pair<struct myState*, int>> new_successors;
- atomic<bool> isAcceptance {false};
- atomic<bool> isConstructed {false};
+ vector<pair<struct myState_t*, int>> new_successors;
+ bool isAcceptance {false};
+ bool isConstructed {false};
bool cyan {false};
atomic<bool> blue {false};
atomic<bool> red {false};
};
-typedef struct myState _state; // @alias
class CNDFS {
private:
@@ -39,25 +38,24 @@ private:
mutex mMutex;
condition_variable cv;
void spawnThreads();
- _state * mInitStatePtr;
+ myState_t * mInitStatePtr;
+ SafeDequeue<struct myState_t*> mSharedPoolTemp;
+ static spot::bdd_dict_ptr* m_dict_ptr;
void getInitialState();
static void threadHandler(void *context);
public:
-
-// typedef myState _state;
- SafeDequeue<struct myState*> sharedPoolTemp;
// SafeDequeue<myCouple> sharedPool;
SafeDequeue<spot::formula> transitionNames;
SafeDequeue<coupleSuccessor> new_successor;
CNDFS(ModelCheckBaseMT *mcl,const spot::twa_graph_ptr &af,const uint16_t& nbTh);
virtual ~CNDFS();
- void computeSuccessors(_state *state);
- void dfsBlue(_state *state);
- void dfsRed(_state* state, deque<_state*> mydeque);
- void WaitForTestCompleted(_state* state);
- atomic_bool awaitCondition(_state* state,deque<_state*> mydeque);
- _state* buildState(LDDState* left, spot::state* right, bool acc, bool constructed,bool cyan);
- static spot::bdd_dict_ptr* m_dict_ptr;
+ void computeSuccessors(myState_t *state);
+ void dfsBlue(myState_t *state);
+ void dfsRed(myState_t* state, deque<myState_t*> mydeque);
+ void WaitForTestCompleted(myState_t* state);
+ atomic_bool awaitCondition(myState_t* state,deque<myState_t*> mydeque);
+ myState_t* buildState(LDDState* left, spot::state* right, bool acc, bool constructed,bool cyan);
+
};
#endif //PMC_SOG_CNDFS_H
diff --git a/src/misc/SafeDequeue.cpp b/src/misc/SafeDequeue.cpp
index aca8c11..b158c05 100644
--- a/src/misc/SafeDequeue.cpp
+++ b/src/misc/SafeDequeue.cpp
@@ -107,5 +107,5 @@ template class SafeDequeue<couple_th>;
template class SafeDequeue<coupleSuccessor>;
template class SafeDequeue<spot::formula>;
-//typedef pair<struct myState*, int> coupleSuccessor;
-template class SafeDequeue<struct myState*>;
+//typedef pair<struct myState_t*, int> coupleSuccessor;
+template class SafeDequeue<struct myState_t*>;
diff --git a/src/misc/SafeDequeue.h b/src/misc/SafeDequeue.h
index b4ddbb2..749d563 100644
--- a/src/misc/SafeDequeue.h
+++ b/src/misc/SafeDequeue.h
@@ -31,7 +31,7 @@ typedef pair<LDDState*, MDD> couple;
typedef pair<couple, Set> Pair;
typedef pair<LDDState*, int> couple_th;
-typedef pair<struct myState*, int> coupleSuccessor;
+typedef pair<struct myState_t*, int> coupleSuccessor;
struct empty_queue: std::exception {
~empty_queue() {};
--
GitLab