diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp
index abc63f861e7576002d5ff32bc0017c16f012ff91..1e164a30fadd60eb2723bb4029ab6715ec884298 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -13,25 +13,10 @@
#include <bddx.h>
using namespace std;
-struct start_state{
- LDDState *left;
- const spot::twa_graph_state* right;
- bool isAcceptance;
-};
-struct end_state{
- LDDState *left;
- const spot::state* right;
- bool isAcceptance;
-};
-vector<pair<end_state, int> > new_successors;
-list<spot::formula> transitionNames;
-vector<bdd>temp;
CNDFS::CNDFS(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh) : mMcl(mcl), mAa(af), mNbTh(nbTh)
{
- sog_current_state = mcl->getInitialMetaState();
- ba_current_state = mAa->get_init_state();
spawnThreads();
}
@@ -53,16 +38,27 @@ void CNDFS::spawnThreads() {
}
void CNDFS::threadHandler(void *context) {
- ((CNDFS *) context)->computeProduct();
+ _state* state = ((CNDFS *) context)->getInitialState();
+ ((CNDFS *) context)->dfsBlue(state);
}
-//Compute the synchronized product
-void CNDFS::computeProduct() {
- uint16_t idThread = mIdThread++;
+//get initial state of the product automata
+CNDFS::_state* CNDFS::getInitialState(){
+ _state * initStatePtr = static_cast<_state *>(malloc(sizeof(_state)));
+ initStatePtr->left = mMcl->getInitialMetaState();
+ initStatePtr->right = mAa->get_init_state();
+ initStatePtr->isAcceptance = mAa->state_is_accepting(mAa->get_init_state());
+ initStatePtr->isConstructed = true;
+ return initStatePtr;
+}
+
+//compute new successors of a product state
+void CNDFS::computeSuccessors(LDDState *sog_current_state, const spot::twa_graph_state *ba_current_state)
+{
+
while (!sog_current_state);
- LDDState *initialAgg = sog_current_state;
- while (!initialAgg->isCompletedSucc());
- //fetch the state's atomic proposition
+ while (!sog_current_state->isCompletedSucc());
+ //fetch the state's atomic proposition
for (auto vv: sog_current_state->getMarkedPlaces(mMcl->getPlaceProposition()))
{
string name = string(mMcl->getPlace(vv));
@@ -72,189 +68,74 @@ void CNDFS::computeProduct() {
for (auto tn: transitionNames)
{
- cout << "AP in state " << tn << endl;
+ cout << " \n AP in state " << tn << endl;
}
-
+
//iterate over the successors of an aggregate
for (int i = 0; i < sog_current_state->Successors.size(); i++)
{
- cout <<"------"<< " SOG's successor " << i << " ------" << endl;
- int transition = sog_current_state->Successors.at(i).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_back(f); // push state'S AP to edge'S AP
- auto p = mAa->get_dict(); //avoir le dictionnaire bdd,proposition atomique
- //cout << p->bdd_map.size() << endl;
- for (auto v: p->var_map)
- {
- cout << v.first << "-----" << v.second << endl;
- }
+ cout <<"------"<< " SOG's successor " << i << " ------" << endl;
+ int transition = sog_current_state->Successors.at(i).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_back(f); // push state'S AP to edge'S AP
+ auto p = mAa->get_dict(); //avoir le dictionnaire bdd,proposition atomique
+ //cout << p->bdd_map.size() << endl;
+ for (auto v: p->var_map)
+ {
+ cout << v.first << "-----" << v.second << endl;
+ }
- for (auto it = transitionNames.begin(); it != transitionNames.end(); ++it)
- {
- if (p->var_map.find(*it) != p->var_map.end())
- { //fetch the transition of BA that have the same AP as the SOG transition
- const bdd result=bdd_ithvar((p->var_map.find(*it))->second);
- cout << "dbb result " << result << endl;
- //iterate over the successors of a BA state
- spot::twa_succ_iterator* ii = mAa->succ_iter(ba_current_state);
- if (ii->first())
- do
+ for (auto it = transitionNames.begin(); it != transitionNames.end(); ++it)
+ {
+ if (p->var_map.find(*it) != p->var_map.end())
+ { //fetch the transition of BA that have the same AP as the SOG transition
+ const bdd result=bdd_ithvar((p->var_map.find(*it))->second);
+ cout << "dbb result " << result << endl;
+ //iterate over the successors of a BA state
+ spot::twa_succ_iterator* ii = mAa->succ_iter(ba_current_state);
+ if (ii->first())
+ do
+ {
+ bdd matched = ii->cond()&result;
+ if (matched!=bddfalse)
{
- bdd matched = ii->cond()&result;
- if (matched!=bddfalse)
- {
- cout << "matched bdd " << matched << endl;
- //new starting state
- struct start_state ns = {sog_current_state, ba_current_state, mAa->state_is_accepting(ba_current_state)};
- //new terminal state
- struct end_state nd = {sog_current_state->Successors.at(i).first, ii->dst(), mAa->state_is_accepting(ii->dst())};
- new_successors.push_back(make_pair(nd,transition));
- cout << *it << " is a common transaction!" << endl; // p->var_map.find ( f )->second => donne la bdd
- }
+ cout << "matched bdd " << matched << endl;
+ //new terminal state
+ _state nd = {sog_current_state->Successors.at(i).first, dynamic_cast<const spot::twa_graph_state *> (ii->dst()), mAa->state_is_accepting(ii->dst()),true};
+ new_successors.push_back(make_pair(nd,transition));
+ cout << *it << " is a common transaction!" << endl; // p->var_map.find ( f )->second => donne la bdd
}
+ }
while (ii->next());
- mAa->release_iter(ii);
- } else cout << *it << " isn't a common transaction" << endl;
- }
- transitionNames.pop_back();
- }
-
- for (auto p: new_successors) {
- std::cout << "list of successors of current state " << "({ " << p.first.right << ", " << p.first.left << ", " << p.first.isAcceptance << " }" << ", " << p.second << ") ";
+ mAa->release_iter(ii);
+ } else cout << *it << " isn't a common transaction" << endl;
+ }
+ transitionNames.pop_back();
}
- for (auto k = new_successors.begin(); k != new_successors.end(); ++k)
- {
- sog_current_state= k->first.left;
- ba_current_state= dynamic_cast<const spot::twa_graph_state *>(k->first.right);
- }
}
-spot::bdd_dict_ptr *CNDFS::m_dict_ptr;
-////
-//// 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/twa.hh>
-//
-//using namespace std;
-//
-//
-//struct new_state{
-// LDDState *left;;
-// spot::state* right;
-//};
-//
-////temporary list to collect the successors of a BA state
-//vector<bdd>BA_succ_temp;
-//
-////temporary list to collect the successors of a SOG aggregate
-//vector<bdd> SOG_succ_temp;
-//
-////list of new successors of the product
-//vector<bdd> successors_new_node;
-//
-//
-//CNDFS::CNDFS(shared_ptr<SogKripkeTh> k, const spot::twa_graph_ptr &af, const uint16_t &nbTh) : mK(k), mAa(af),
-// mNbTh(nbTh) {
-// spawnThreads();
-//}
-//
-////CNDFS::CNDFS(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh) : mMcl(mcl), mAa(af),
-//// mNbTh(nbTh) {
-//// spawnThreads();
-////}
-//
-//CNDFS::~CNDFS() {
-// for (int i = 0; i < mNbTh; ++i) {
-// mlThread[i]->join();
-// delete mlThread[i];
-// }
-//}
-//
-///*
-// * @Brief Create threads
-// */
-//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::threadHandler(void *context) {
-// ((CNDFS *) context)->computeProduct();
-//}
-//
-///*
-// * @brief Compute the synchornized product
-// */
-//void CNDFS::computeProduct()
-//{
-// mIdThread++;
-// //list of successors of a BA state
-// spot::twa_succ_iterator* i = mAa->succ_iter(mAa->get_init_state());
-// if (i->first())
-// do
-// {
-// //std::lock_guard<std::mutex> lg(mMutex);
-// BA_succ_temp.push_back(i->cond());
-// }
-// while (i->next());
-// mAa->release_iter(i);
-//
-// for(bdd n : BA_succ_temp)
-// {
-// std::cout << "BA succ"<< n << endl;
-// }
-//
-//// //list of successors of a SOG aggregate
-// auto edges = mK->succ_iter(mK->get_init_state());
-// if (edges->first())
-// do
-// {
-// //std::lock_guard<std::mutex> lg(mMutex);
-// SOG_succ_temp.push_back(edges->cond());
-// }
-// while (edges->next());
-// mK->release_iter(edges);
-//
-// for(bdd m : SOG_succ_temp)
-// {
-// std::cout << "SOG succ"<< m << endl;
-// }
-//
-// for(bdd n : SOG_succ_temp)
-// {
-// for(bdd m : BA_succ_temp)
-// {
-// if (n==m)
-// {
-// successors_new_node.push_back(m);
-// }
-// }
-// }
-//
-// if (!successors_new_node.empty())
-// {
-// for(bdd k : successors_new_node)
+//Compute the synchronized product
+void CNDFS::dfsBlue(_state *state) {
+ uint16_t idThread = mIdThread++;
+
+ cout << state->isConstructed << endl;
+ computeSuccessors(state->left,state->right);
+ for (auto p: new_successors) {
+ std::cout << "list of successors of current state " << "({ " << p.first.right << ", " << p.first.left << ", " << p.first.isAcceptance << ", " << p.first.isConstructed << " }" << ", " << p.second << ") ";
+ }
+
+// for (auto k = new_successors.begin(); k != new_successors.end(); ++k)
// {
-//// new_state new_product_state(mK->get_init_state(),mAa->get_init_state());
-// cout << "common succ "<< k << endl;
+// sog_current_state= k->first.left;
+// ba_current_state= dynamic_cast<const spot::twa_graph_state *>(k->first.right);
+// //computeSuccessors(sog_current_state,ba_current_state);
+// if (! k->first.isConstructed)
+// dfsBlue();
// }
-//
-// } else{
-// cout << "no common succ" << endl;
-// }
-//
-//}
+
+
+}
+spot::bdd_dict_ptr *CNDFS::m_dict_ptr;
+
diff --git a/src/algorithm/CNDFS.h b/src/algorithm/CNDFS.h
index 588582f5d80bb316fa6d77887b231a4d71da1db7..a4d654e887ec54dec74ee3dbe58296720a49483e 100644
--- a/src/algorithm/CNDFS.h
+++ b/src/algorithm/CNDFS.h
@@ -16,18 +16,29 @@ private:
static constexpr uint8_t MAX_THREADS=64;
ModelCheckBaseMT * mMcl;
spot::twa_graph_ptr mAa;
- LDDState* sog_current_state;
- const spot::twa_graph_state* ba_current_state;
uint16_t mNbTh;
atomic<uint8_t> mIdThread;
static void threadHandler(void *context);
std::thread* mlThread[MAX_THREADS];
std::mutex mMutex;
void spawnThreads();
+
public:
+ typedef struct _state{
+ LDDState *left;
+ const spot::twa_graph_state* right;
+ bool isAcceptance;
+ bool isConstructed = false;
+ } _state;
+
+ vector<pair<_state , int>> new_successors;
+ list<spot::formula> transitionNames;
+ vector<bdd>temp;
CNDFS(ModelCheckBaseMT *mcl,const spot::twa_graph_ptr &af,const uint16_t& nbTh);
virtual ~CNDFS();
- void computeProduct();
+ void computeSuccessors(LDDState* sog_current_state,const spot::twa_graph_state* ba_current_state);
+ void dfsBlue(_state *state);
+ _state* getInitialState();
static spot::bdd_dict_ptr* m_dict_ptr;
};
diff --git a/src/main.cpp b/src/main.cpp
index 5c6337e1277f33e3a988d9c8bfc5417a8960e111..6847eda2a6cd12a948385803a867e4c7a4137b80 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -525,11 +525,7 @@ int main(int argc, char **argv)
{
std::cout<<"------------CNDFS-------------"<<std::endl;
-// threadSOG DR(Rnewnet, nb_th, uselace);
-// LDDGraph g(&DR);
-//
-// DR.computeSeqSOG(g);
-// g.printCompleteInformation();
+
CNDFS cndfs(mcl,af,1);
return(0);