diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp
index df555f5aff9d1cdc1dee48d6d52afccc1aca2b4d..125d8cde7c5b73abcc1e9ca80226f14962e69d30 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -13,25 +13,11 @@
using namespace std;
-
-bool red = false;
-bool blue = false;
-thread_local bool cyan = false;
-
-struct new_state {
- ModelCheckBaseMT &left;
- shared_ptr<spot::twa_graph> right;
-};
-
-struct new_state_succ {
- LDDState *succ_left;
- spot::twa_succ_iterator *succ_right;
+struct new_state{
+ LDDState *left;;
+ spot::state* right;
};
-vector<new_state_succ> successors_new_node;
-
-
-
CNDFS::CNDFS(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh) : mMcl(mcl), mAa(af),
mNbTh(nbTh) {
@@ -45,36 +31,6 @@ CNDFS::~CNDFS() {
}
}
-//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;
- //cout << "First state BA from CNDFS " << a->get_init_state()<<endl;
-
-
- //iterate succ of BA initial state
- //mtx.lock();
- spot::twa_succ_iterator *i = mAa->succ_iter(mAa->get_init_state());
- if (i->first())
- 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;
- }
-}
-*/
-
/*
* @Brief Create threads
*/
@@ -101,16 +57,155 @@ void CNDFS::computeProduct() {
while (!mMcl->getInitialMetaState());
LDDState * initialAgg=mMcl->getInitialMetaState();
while (!initialAgg->isCompletedSucc());
- int transition=mMcl->getInitialMetaState()->Successors.at(0).second; // je récupère le numéro de la première 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 transiition
- auto p=mAa->get_dict(); // avoir le dictionnaire bdd,proposition atomique
- if (p->var_map.find ( f )==p->var_map.end()) { // Chercher la transition
- cout<<"trouvé!"; // p->var_map.find ( f )->second => donne la bdd
- } else cout<<"trouvé";
- //bdd result=bdd_ithvar ( ( p->var_map.find ( f ) )->second );
+ for (auto vv : mMcl->getInitialMetaState()->getMarkedPlaces(mMcl->getPlaceProposition()))
+ {
+ cout << mMcl->getPlace(vv)<< endl;
+ }
+
+ for (int i=0 ; i < mMcl->getInitialMetaState()->Successors.size(); i++)
+ {
+ int transition=mMcl->getInitialMetaState()->Successors.at(i).second; // je récupère le numéro de la première 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 transiition
+ // cout << f << endl;
+ auto p=mAa->get_dict(); // avoir le dictionnaire bdd,proposition atomique
+ for (auto v : p->var_map)
+ {
+ cout << f << "-->" << v.first << endl;
+ }
+
+ if (p->var_map.find ( f )==p->var_map.end()) { // Chercher la transition
+ cout<<"non trouvé!" <<endl; // p->var_map.find ( f )->second => donne la bdd
+ } else cout<<"trouvé";
+ }
- //mAa->edge_data(0)
}
-spot::bdd_dict_ptr* CNDFS::m_dict_ptr;
\ No newline at end of file
+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)
+// {
+//// new_state new_product_state(mK->get_init_state(),mAa->get_init_state());
+// cout << "common succ "<< k << endl;
+// }
+//
+// } else{
+// cout << "no common succ" << endl;
+// }
+//
+//}
diff --git a/src/algorithm/CNDFS.h b/src/algorithm/CNDFS.h
index 185520e9b7e4122b207193a634a60d5856bd25ea..d367f6a565c61be7e4245c7b97e8f35c1927d043 100644
--- a/src/algorithm/CNDFS.h
+++ b/src/algorithm/CNDFS.h
@@ -5,6 +5,7 @@
#ifndef PMC_SOG_CNDFS_H
#define PMC_SOG_CNDFS_H
#include "../ModelCheckBaseMT.h"
+//#include "../SogKripkeTh.h"
#include <spot/tl/apcollect.hh>
#include <cstdint>
#include <thread>
@@ -22,6 +23,7 @@ private:
void spawnThreads();
public:
CNDFS(ModelCheckBaseMT *mcl,const spot::twa_graph_ptr &af,const uint16_t& nbTh);
+// CNDFS(shared_ptr<SogKripkeTh> k,const spot::twa_graph_ptr &af,const uint16_t& nbTh);
virtual ~CNDFS();
//static void DfsBlue();
void computeProduct();
diff --git a/src/main.cpp b/src/main.cpp
index 294a73c154ec39a38fac5186a4c9d8e473e9c42e..5cbad55f52a8503f0d9d5c6e3a00b103af61d5f8 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -200,7 +200,8 @@ void displayToolInformation(const string &net, const string &formula, const stri
* @param por Flag for partial order reduction
* @return ModelCheckBaseMT*
*/
-ModelCheckBaseMT *getMultiCoreMC(NewNet &net, int nb_th, const string &thread_library, bool progressive, bool por)
+ModelCheckBaseMT *
+getMultiCoreMC(NewNet &net, int nb_th, const string &thread_library, bool progressive, bool por)
{
ModelCheckBaseMT *mcl = nullptr;
@@ -524,23 +525,17 @@ int main(int argc, char **argv)
{
std::cout<<"I'm here"<<std::endl;
+// auto k = std::make_shared<SogKripkeTh>(d, mcl, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP());
+// CNDFS cndfs(k,af,1);
+ CNDFS cndfs(mcl,af,1);
- 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
- // try else you send me a request tomorrw if you have pbs
- //CNDFS cndfs(*mcl, aa);
- //cndfs.DfsBlue(*mcl, aa);
-
- // n.spawnThreads(2,*mcl,aa);
return(0);
}
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