add CNDFS Version2 and UFSCC files

src/CMakeLists.txt

@@ -27,7 +27,7 @@ include_directories(${MPI_INCLUDE_PATH})
 
 # include spot and bddx library
 add_library(spot SHARED IMPORTED)
-add_library(bddx SHARED IMPORTED algorithm/CNDFS.cpp algorithm/CNDFS.h)
+add_library(bddx SHARED IMPORTED algorithm/CNDFS.cpp algorithm/CNDFS.h algorithm/CndfsV2.h algorithm/CndfsV2.cpp)
 
 if(NOT SPOT_LIBRARY)
   set_target_properties(spot PROPERTIES IMPORTED_LOCATION "${SPOT_DIR}/lib/libspot.so")
@@ -100,6 +100,10 @@ add_executable(pmc-sog main.cpp
     misc/md5_hash.h Hybrid/MCHybridPOR/MCHybridSOGPOR.cpp Hybrid/MCHybridPOR/MCHybridSOGPOR.h
         algorithm/CNDFS.h
         algorithm/CNDFS.cpp
+        algorithm/CndfsV2.h
+        algorithm/CndfsV2.cpp
+        algorithm/UFSCC.h
+        algorithm/UFSCC.cpp
         )
 
 

src/algorithm/CNDFS.cpp

@@ -173,18 +173,8 @@ void CNDFS::computeSuccessors(myState_t *state, vector<spot::formula> ap_sog) {
          if (ii->first())
                 do {
                    auto pa_ba_result = spot::bdd_to_formula(ii->cond(), p); // from bdd to formula
-//                   cout << "formula ba: " << pa_ba_result << endl;
-//                    std::cout << (spot::are_equivalent(pa_ba_result, pa_sog_result) ?
-//                                  "Equivalent\n" : "Not equivalent\n");
-//                    std::cout << "match " << c.contained(pa_sog_result, pa_ba_result) << endl;
-//                    auto form= p->var_map.find(bdd_var(ii->cond()))->second.id();
-//                   cout <<  "here " << form << endl;
-//                    if (p->var_map.find(pa_sog_result) != p->var_map.end()) {   //extra text
-//                        cout << "yes " << endl;
-//                        //fetch the transition of BA that have the same AP as the SOG transition
-//                       cout << "dbb  "<<  mAa->register_ap(pa_sog_result) << endl;  //The BDD variable number assigned for this atomic proposition.
-//                        const bdd result = bdd_ithvar((p->var_map.find(pa_sog_result))->second);
-                        if (c.contained(pa_sog_result, pa_ba_result) || c.contained(pa_ba_result, pa_sog_result)) {
+                   if (c.contained(pa_sog_result, pa_ba_result) || c.contained(pa_ba_result, pa_sog_result))
+                   {
                             std::unique_lock lk(mMutex);
                             auto result = isStateBuilt(elt.first, (spot::twa_graph_state *) ii->dst());
                             if (result) {
@@ -195,7 +185,7 @@ void CNDFS::computeSuccessors(myState_t *state, vector<spot::formula> ap_sog) {
                                                            mAa->state_is_accepting(ii->dst()), true, false);
                                 state->new_successors.push_back(make_pair(nd, transition));
                             }
-                        }
+                   }
                 } while (ii->next());
          mAa->release_iter(ii);
         }

src/algorithm/CNDFS.h

@@ -65,16 +65,10 @@ public:
 
     virtual ~CNDFS();
 
-
-
     void dfsBlue(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread,vector<spot::formula> ap_sog);
 
     void dfsRed(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread);
 
-
-
-
-
 };
 
 #endif //PMC_SOG_CNDFS_H

src/algorithm/CndfsV2.cpp

+//
+// Created by ghofrane on 5/4/22.
+//
+
+#include "CndfsV2.h"
+#include "ModelCheckBaseMT.h"
+#include <iostream>
+#include <spot/twa/twagraph.hh>
+#include <thread>
+#include <vector>
+#include <utility>
+#include <spot/twa/twa.hh>
+#include <bddx.h>
+#include <deque>
+#include <atomic>
+#include <condition_variable>
+#include <algorithm>
+#include "misc/stacksafe.h"
+#include <spot/twa/formula2bdd.hh>
+#include <spot/tl/formula.hh>
+#include <spot/misc/minato.hh>
+#include <spot/twaalgos/contains.hh>
+#include <spot/tl/contain.hh>
+#include  <random>
+
+
+using namespace std;
+
+CndfsV2::CndfsV2(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh) : mMcl(mcl), mAa(af),
+                                                                                           mNbTh(nbTh) {
+    getInitialState();
+    spawnThreads();
+}
+
+CndfsV2::~CndfsV2() {
+    for (int i = 0; i < mNbTh; ++i) {
+        mlThread[i]->join();
+        delete mlThread[i];
+    }
+    // Liberate dynamic allocated memory for synchropnized product
+    for (const auto & elt : mlBuiltStates)
+        delete elt;
+}
+
+// Create threads
+void CndfsV2::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 CndfsV2::threadHandler(void *context) {
+    ((CndfsV2 *) context)->threadRun();
+}
+
+void CndfsV2::threadRun() {
+    uint16_t idThread = mIdThread++;
+    vector<myState_t *> Rp;
+    vector<spot::formula> ap_sog;
+    vector <spot::formula> communTr;
+    dfsBlue(mInitStatePtr, Rp, idThread, ap_sog, communTr);
+}
+
+/*
+ * Build initial state of the product automata
+ */
+void CndfsV2::getInitialState() {
+    mInitStatePtr = new myState_t;
+    mInitStatePtr->left = mMcl->getInitialMetaState();
+    mInitStatePtr->right = mAa->get_init_state();
+    mInitStatePtr->isAcceptance = mAa->state_is_accepting(mAa->get_init_state());
+    mInitStatePtr->isConstructed = true;
+    mlBuiltStates.push_back(mInitStatePtr);
+}
+
+
+//this function is to build a state with list of successor initially null
+myState_t *CndfsV2::buildState(myState_t *state, spot::formula tr) {
+    myState_t *buildStatePtr = new myState_t;
+//    buildStatePtr->left = getSuccessorFromSOG(state->left,tr);
+//    buildStatePtr->right = getSuccessorFromBA(state->right,tr);
+//    buildStatePtr->isAcceptance = state->right;
+//    buildStatePtr->isConstructed = constructed;
+
+    return buildStatePtr;
+}
+
+//std::ostream &operator<<(std::ostream &Str, myState_t *state) {
+//    Str << "({ Sog state= " << state->left << ", BA state= " << state->right << ", acceptance= " << state->isAcceptance
+//        << ", constructed= " << state->isConstructed << ", red= " << state->red << ", blue= " << state->blue << " }"
+//        << endl;
+//    int i = 0;
+//    for (const auto &ii: state->new_successors) {
+//        Str << "succ num " << i << ii.first << " with transition " << ii.second << endl;
+//        i++;
+//    }
+//    return Str;
+//}
+
+void CndfsV2::dfsRed(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread) {
+//    cout << "dfsRed" << endl;
+    Rp.push_back(state);
+//    computeSuccessors(state);
+    for (const auto &succ: state->new_successors) {
+//        cout << "dfs red 1 "  << succ.first->cyan[idThread]<< endl;
+        if (succ.first->cyan[idThread]) {
+            cout << "cycle detected with the thread " << unsigned(idThread) << endl;
+            exit(0);
+        }
+        // unvisited and not red state
+        if ((find(Rp.begin(), Rp.end(), state) != Rp.end()) && !succ.first->red)
+            dfsRed(succ.first, Rp, idThread);
+    }
+}
+
+/*
+ * Check whether a product state exists or not
+ */
+myState_t *CndfsV2::isStateBuilt(LDDState *sogState, const spot::twa_graph_state *spotState) {
+    auto compare = [sogState, spotState](myState_t *state) {
+        return (state->left == sogState && state->right == spotState);
+    };
+    auto result = find_if(begin(mlBuiltStates), end(mlBuiltStates), compare);
+    return result == end(mlBuiltStates) ? nullptr : *result;
+}
+
+
+//compute new successors of a product state
+vector<spot::formula> CndfsV2::fireable(myState_t *state, vector<spot::formula> ap_sog, vector <spot::formula> communTr) {
+    auto sog_current_state = state->left;
+    const spot::twa_graph_state *ba_current_state = state->right;
+    while (!sog_current_state->isCompletedSucc());
+    auto p = mAa->get_dict();//avoir le dictionnaire bdd,proposition atomique
+    //fetch the state's atomic proposition
+    for (const auto & vv: sog_current_state->getMarkedPlaces(mMcl->getPlaceProposition()))
+    {
+        auto name = string(mMcl->getPlace(vv));
+        auto ap_state = spot::formula::ap(name);
+        if (p->var_map.find(ap_state) != p->var_map.end()) {
+            ap_sog.push_back(ap_state);
+            for( auto n: p->var_map)
+            {
+                if (n.first != ap_state)
+                {
+                    ap_sog.push_back(spot::formula::Not(n.first));
+                }
+            }
+        }
+    }
+    //iterate over the successors of a current aggregate
+    for (const auto &elt: sog_current_state->Successors) {
+        auto 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 ap_edge = spot::formula::ap(name);// récuperer la proposition atomique qui correspond à la transition
+        if (p->var_map.find(ap_edge) != p->var_map.end()) {
+            ap_sog.push_back(ap_edge);
+        }
+        spot::formula pa_sog_result = spot::formula::And(ap_sog);
+//        cout << "formula sog: " << pa_sog_result << endl;
+        //iterate over the successors of a BA state
+        auto ii = mAa->succ_iter(ba_current_state);
+        if (ii->first())
+            do {
+                auto pa_ba_result = spot::bdd_to_formula(ii->cond(), p); // from bdd to formula
+                if (c.contained(pa_sog_result, pa_ba_result) || c.contained(pa_ba_result, pa_sog_result)) {
+                  communTr.push_back(pa_sog_result);
+                }
+            } while (ii->next());
+        mAa->release_iter(ii);
+    }
+    return communTr;
+}
+
+int i = 0 ;
+//Perform the dfsBlue
+void CndfsV2::dfsBlue(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread, vector<spot::formula> ap_sog, vector <spot::formula> communTr) {
+
+    state->cyan[idThread] = true;
+    communTr = fireable(state, ap_sog, communTr);
+//    std::mt19937 g(rd());
+//    std::shuffle(communTr.begin(), communTr.end(), g);
+    mMutexStatus.lock();
+    spot::formula sel_elem = communTr[communTr.size()-1];
+    cout << "hello from thread " << unsigned(idThread) << " transition " << sel_elem << endl;
+    communTr.pop_back();
+    mMutexStatus.unlock();
+
+//        myState_t* st = buildState(state,tr);
+//        myState_t* s = isStateBuilt(st->left,st->right);
+//        if(s)
+//        {
+//            free(st);
+//            state->new_successors.push_back(make_pair(s,0));
+//        }else
+//        {
+//            mlBuiltStates.push_back(st);
+//            state->new_successors.push_back(make_pair(st,0));
+//        }
+
+//    for (const auto &succ: state->new_successors) {
+//        if (!succ.first->blue && !succ.first->cyan[idThread]) {
+//            dfsBlue(succ.first, Rp, idThread, ap_sog, communTr);
+//        }
+//    }
+//    state->blue = true;
+//    if (state->isAcceptance) {
+////        cout << "Acceptance state detected " << endl;
+//        if (state->left->isDeadLock() || state->left->isDiv()) {
+//            cout << "cycle detected: an aggregate with deal_lock or live_lock" << endl;
+//            exit(0);
+//        } else {
+//            Rp.clear();
+//            dfsRed(state, Rp, idThread); //looking for an accepting cycle
+//            bool cond;
+//            do {
+//                cond = true;
+//                for (auto iter = Rp.begin(); iter != Rp.end() && cond; ++iter) {
+//                    if ((*iter)->isAcceptance && (*iter != state)) {
+//                        if (!(*iter)->red) cond = false;
+//                    }
+//                }
+//            } while (!cond);
+//
+//            for (const auto &qu: Rp) // prune other dfsRed
+//            {
+//                qu->red = true;
+//            }
+//        }
+//        cout << "no cycle detected" << endl;
+//    }
+//    state->cyan[idThread] = false;
+}
+
+
+spot::bdd_dict_ptr *CndfsV2::m_dict_ptr;
+

src/algorithm/CndfsV2.h

+//
+// Created by ghofrane on 7/21/22.
+//
+
+#ifndef PMC_SOG_CNDFSV2_H
+#define PMC_SOG_CNDFSV2_H
+
+#include "../ModelCheckBaseMT.h"
+#include "CNDFS.h"
+#include <spot/tl/apcollect.hh>
+#include <cstdint>
+#include <spot/twa/twagraph.hh>
+#include <atomic>
+#include <thread>
+#include <mutex>
+#include <condition_variable>
+#include "misc/SafeDequeue.h"
+#include <spot/tl/contain.hh>
+#include <random>
+#include <algorithm>
+
+using namespace std;
+typedef pair<struct myState_t *, int> coupleSuccessor;
+
+using namespace std;
+
+
+class CndfsV2 {
+
+private:
+    ModelCheckBaseMT *mMcl;
+    spot::twa_graph_ptr mAa;
+    uint16_t mNbTh;
+    atomic<uint8_t> mIdThread;
+    std::thread *mlThread[MAX_THREADS];
+    mutex mMutex,mMutexStatus;
+    std::condition_variable mDataCondWait;
+    condition_variable cv;
+    myState_t *mInitStatePtr;
+    vector<myState_t *> mlBuiltStates;
+    SafeDequeue<struct myState_t *> mSharedPoolTemp;
+    static spot::bdd_dict_ptr *m_dict_ptr;
+    spot::language_containment_checker c;
+    std::random_device rd;
+
+    void getInitialState();
+
+    void spawnThreads();
+
+    static void threadHandler(void *context);
+
+    void threadRun();
+
+//    void computeSuccessors(myState_t *state, vector<spot::formula> ap_sog);
+    vector<spot::formula> fireable(myState_t *state, vector<spot::formula> ap_sog, vector <spot::formula> transition);
+
+    myState_t *buildState(myState_t *state, spot::formula tr);
+    myState_t* isStateBuilt(LDDState *sogState,const spot::twa_graph_state *spotState);
+public:
+    CndfsV2(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh);
+
+    virtual ~CndfsV2();
+
+    void dfsBlue(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread,vector<spot::formula> ap_sog, vector <spot::formula> transition);
+
+    void dfsRed(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread);
+
+};
+
+#endif //PMC_SOG_CNDFSV2_H

src/algorithm/UFSCC.cpp

+//
+// Created by ghofrane on 7/21/22.
+//
+
+#include "UFSCC.h"

src/algorithm/UFSCC.h

+//
+// Created by ghofrane on 7/21/22.
+//
+
+#ifndef PMC_SOG_UFSCC_H
+#define PMC_SOG_UFSCC_H
+
+
+class UFSCC {
+
+};
+
+
+#endif //PMC_SOG_UFSCC_H

src/main.cpp

@@ -36,6 +36,8 @@
 #include "Hybrid/MCHybridReqPOR/MCHybridSOGReqPOR.h"
 #include "Hybrid/MCHybridPOR/MCHybridSOGPOR.h"
 #include "algorithm/CNDFS.h"
+#include "algorithm/CndfsV2.h"
+#include "algorithm/UFSCC.h"
 #include <typeinfo>
 #include <atomic>
 #include <thread>
@@ -523,13 +525,24 @@ int main(int argc, char **argv)
 
             // run on the fly parallel model-checking
             // TODO: Implement here Ghofrane's algorithms
-            if (algorithm == "UFSCC" || algorithm == "CNDFS")
+            if (algorithm == "CndfsV1")
             {
-                std::cout<<"------------CNDFS-------------"<<std::endl;
+                cout<<"------------MC-CNDFS-VERSION1-------------"<<endl;
                 CNDFS cndfs(mcl,af,2); // If I increase the number of threads, a segmentation fault appears.
                 return(0);
             }
-            else // run on the fly sequential model-checking
+            else if (algorithm == "CndfsV2")// run on the fly sequential model-checking
+            {
+                cout<<"------------MC-CNDFS-VERSION2-------------"<<endl;
+                CndfsV2 cndfs2(mcl,af,2);
+                return(0);
+
+            } else if (algorithm == "UFSCC")
+            {
+                cout<<"------------MC-UFSCC-------------"<<endl;
+                return(0);
+
+            }else
             {
                 auto k = std::make_shared<SogKripkeTh>(d, mcl, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP());
                 runOnTheFlyMC(algorithm, k, af);