diff --git a/src/SogKripkeTh.h b/src/SogKripkeTh.h index f482a0ea57793331960b2ae6c24e0a1cbaefc20e..f079fd079fb2c3364b84bad652cd0553b78bc784 100644 --- a/src/SogKripkeTh.h +++ b/src/SogKripkeTh.h @@ -18,8 +18,6 @@ class SogKripkeTh: public spot::kripke { std::string format_state(const spot::state* s) const override; bdd state_condition(const spot::state* s) const override; ModelCheckBaseMT *m_builder; - - }; #endif // SOGKRIPKE_H_INCLUDED diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp index 125d8cde7c5b73abcc1e9ca80226f14962e69d30..abd423ac6ecaeabb15700e3dad9de99e89fd9615 100644 --- a/src/algorithm/CNDFS.cpp +++ b/src/algorithm/CNDFS.cpp @@ -18,6 +18,7 @@ struct new_state{ spot::state* right; }; +list<spot::formula> transitionNames; CNDFS::CNDFS(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh) : mMcl(mcl), mAa(af), mNbTh(nbTh) { @@ -43,7 +44,6 @@ void CNDFS::spawnThreads() { } } - void CNDFS::threadHandler(void *context) { ((CNDFS *) context)->computeProduct(); } @@ -52,36 +52,36 @@ void CNDFS::threadHandler(void *context) { * @brief Compute the synchornized product */ void CNDFS::computeProduct() { - uint16_t idThread=mIdThread++; - //cout<<"My id : "<<mMcl; + uint16_t idThread = mIdThread++; while (!mMcl->getInitialMetaState()); - LDDState * initialAgg=mMcl->getInitialMetaState(); + LDDState *initialAgg = mMcl->getInitialMetaState(); while (!initialAgg->isCompletedSucc()); - for (auto vv : mMcl->getInitialMetaState()->getMarkedPlaces(mMcl->getPlaceProposition())) + + //fetch the state's atomic proposition + for (auto vv: mMcl->getInitialMetaState()->getMarkedPlaces(mMcl->getPlaceProposition())) { - cout << mMcl->getPlace(vv)<< endl; + string name = string(mMcl->getPlace(vv)); + auto f = spot::formula::ap(name); + transitionNames.push_back(f); } - 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; + for (int i = 0; i < mMcl->getInitialMetaState()->Successors.size(); i++) { + cout <<"------"<< i << " SOG's successor ------" << endl; + 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 + transitionNames.push_back(f); // push state'S AP to edge'S AP + auto p = mAa->get_dict(); //avoir le dictionnaire bdd,proposition atomique + for (auto it = transitionNames.begin(); it != transitionNames.end(); ++it) { + if (p->var_map.find(*it) != p->var_map.end()) { // Chercher la transition + cout << *it << " is a common transaction!" << endl; // p->var_map.find ( f )->second => donne la bdd + } else cout << *it << " isn't a common transaction" << 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é"; } - } -spot::bdd_dict_ptr* CNDFS::m_dict_ptr; +spot::bdd_dict_ptr *CNDFS::m_dict_ptr; //// //// Created by ghofrane on 5/4/22. diff --git a/src/main.cpp b/src/main.cpp index 5cbad55f52a8503f0d9d5c6e3a00b103af61d5f8..80d45355b658f9030b11718a2de179cd6b083fc5 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -524,7 +524,7 @@ int main(int argc, char **argv) if (algorithm == "UFSCC" || algorithm == "CNDFS") { - std::cout<<"I'm here"<<std::endl; + std::cout<<"------------CNDFS-------------"<<std::endl; // auto k = std::make_shared<SogKripkeTh>(d, mcl, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP()); // CNDFS cndfs(k,af,1); CNDFS cndfs(mcl,af,1);