Merge branch 'feature/ufscc-emptiness-check' into 'master'

Feature/ufscc emptiness check

See merge request !6

.devcontainer/Dockerfile

@@ -6,7 +6,7 @@ FROM mcr.microsoft.com/vscode/devcontainers/cpp:0-${VARIANT}
 
 # [Optional] Uncomment this section to install additional packages.
 RUN apt-get update && export DEBIAN_FRONTEND=noninteractive \
-    && apt-get -y install --no-install-recommends wget cmake bison flex \
+    && apt-get -y install --no-install-recommends wget cmake bison flex graphviz \
     openmpi-bin libopenmpi-dev && \
     wget http://www.lrde.epita.fr/dload/spot/spot-2.10.4.tar.gz && \
     tar xzf spot-2.10.4.tar.gz && cd spot-2.10.4 && \

CMakeLists.txt

@@ -68,6 +68,11 @@ target_include_directories(cli11 INTERFACE "${THIRD_PARTY_INCLUDE_DIR}/cli11")
 include_directories(src)
 add_subdirectory(src)
 
+set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -pthread")
+
+
+
 # add tests
 # enable_testing()
 # add_subdirectory(tests)
+

README.md

@@ -164,6 +164,9 @@ mpirun -n 2 ./pmc-sog \
 
 ## Publications
 
+- K. Klai, C. A. Abid, J. Arias, and S. Evangelista, "[Hybrid Parallel Model Checking of Hybrid LTL on Hybrid State Space Representation](https://link.springer.com/chapter/10.1007/978-3-030-98850-0_3)", in 14th International Conference on Verification and Evaluation of Computer and Communication Systems, VECoS 2021, Beijing, China, November 22-23, 2021, 2022, vol. 13187, pp. 27–42. doi: 10.1007/978-3-030-98850-0_3.
+
+
 - C. A. Abid, K. Klai, J. Arias, and H. Ouni, “[SOG-Based Multi-Core LTL Model Checking](https://ieeexplore.ieee.org/document/9443795),” in IEEE International Conference on Parallel & Distributed Processing with Applications, Big Data & Cloud Computing, Sustainable Computing & Communications, Social Computing & Networking, ISPA/BDCloud/SocialCom/SustainCom 2020, Exeter, United Kingdom, December 17-19, 2020, 2020, pp. 9–17. doi: 10.1109/ISPA-BDCloud-SocialCom-SustainCom51426.2020.00028.
 
 - H. Ouni, K. Klai, C. A. Abid, and B. Zouari, “[Towards Parallel Verification of Concurrent Systems using the Symbolic Observation Graph](https://ieeexplore.ieee.org/document/8843636),” in 19th International Conference on Application of Concurrency to System Design, ACSD 2019, Aachen, Germany, June 23-28, 2019, 2019, pp. 23–32. doi: 10.1109/ACSD.2019.00007.

examples/Test_example/exemple.net

+#place p1 mk(<..>)
+#place p2
+#place p3
+#place p4
+#place p5
+#place p6
+#place p7
+#place p8
+#place p9
+#place p10
+#trans t1
+in {p1:<..>;}
+out {p2:<..>;}
+#endtr
+#trans t2
+in {p2:<..>;}
+out {p3:<..>;p4:<..>;}
+#endtr
+#trans t3
+in {p3:<..>;}
+out {p5:<..>;}
+#endtr
+#trans t4
+in {p5:<..>;}
+out {p7:<..>;}
+#endtr
+#trans t5
+in {p4:<..>;}
+out {p6:<..>;}
+#endtr
+#trans t6
+in {p4:<..>;}
+out {p8:<..>;}
+#endtr
+#trans t7
+in {p6:<..>;}
+out {p9:<..>;}
+#endtr
+
+#trans t8
+in {p8:<..>;}
+out {p9:<..>;}
+#endtr
+
+#trans t9
+in {p7:<..>;p9:<..>;}
+out {p10:<..>;}
+#endtr
+#trans t10
+in {p9:<..>;}
+out {p4:<..>;}
+#endtr
+#trans t11
+in {p10:<..>;}
+out {p1:<..>;}
+#endtr

examples/Test_example/ltl-ex-false.reduced

+(("p1") -> <> (("p2") && ("p4"))) 

examples/Test_example/ltl-ex-true.reduced

+(("p1") -> <> ("p2"))

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)
+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")
@@ -49,7 +49,6 @@ add_executable(pmc-sog main.cpp
   LDDState.cpp
   LDDState.h
   TransSylvan.cpp
-
   SpotSogState.cpp
   SpotSogState.h
   SpotSogIterator.cpp
@@ -72,32 +71,40 @@ add_executable(pmc-sog main.cpp
   SogKripkeIteratorTh.cpp
   SogKripkeIteratorTh.h
 
-        misc/stacksafe.cpp
-        misc/stacksafe.h
-        misc/SafeDequeue.cpp
-        misc/SafeDequeue.h
-        Hybrid/HybridKripke.cpp
-        Hybrid/HybridKripke.h
-        Hybrid/HybridKripkeIterator.cpp
-        Hybrid/HybridKripkeIterator.h
-        Hybrid/HybridKripkeState.cpp
-        Hybrid/HybridKripkeState.h
-        SylvanWrapper.cpp
-        SylvanWrapper.h
-        SylvanCacheWrapper.cpp SylvanCacheWrapper.h
-        MCMultiCore/ModelCheckerCPPThread.cpp MCMultiCore/ModelCheckerCPPThread.h
-        MCMultiCore/ModelCheckerTh.cpp MCMultiCore/ModelCheckerTh.h
-        MCMultiCore/MCThReqPor.cpp MCMultiCore/MCThReqPor.h
-        MCMultiCore/MCCPPThPor.cpp MCMultiCore/MCCPPThPor.h
-        threadSOG.cpp threadSOG.h
-        HybridSOG.cpp HybridSOG.h
-        Hybrid/MCHybrid/MCHybridSOG.cpp Hybrid/MCHybrid/MCHybridSOG.h
-        MCMultiCore/ModelCheckThReq.cpp MCMultiCore/ModelCheckThReq.h
-        Hybrid/MCHybridReq/MCHybridSOGReq.cpp
-        Hybrid/MCHybridReq/MCHybridSOGReq.h
-        Hybrid/MCHybridReqPOR/MCHybridSOGReqPOR.cpp
-        Hybrid/MCHybridReqPOR/MCHybridSOGReqPOR.h
-        misc/md5_hash.h Hybrid/MCHybridPOR/MCHybridSOGPOR.cpp Hybrid/MCHybridPOR/MCHybridSOGPOR.h)
+
+    Hybrid/HybridKripke.cpp
+    Hybrid/HybridKripke.h
+    Hybrid/HybridKripkeIterator.cpp
+    Hybrid/HybridKripkeIterator.h
+    Hybrid/HybridKripkeState.cpp
+    Hybrid/HybridKripkeState.h
+    misc/SafeDequeue.cpp
+    misc/SafeDequeue.h
+    misc/stacksafe.cpp
+    misc/stacksafe.h
+    SylvanWrapper.cpp
+    SylvanWrapper.h
+    SylvanCacheWrapper.cpp SylvanCacheWrapper.h
+    MCMultiCore/ModelCheckerCPPThread.cpp MCMultiCore/ModelCheckerCPPThread.h
+    MCMultiCore/ModelCheckerTh.cpp MCMultiCore/ModelCheckerTh.h
+    MCMultiCore/MCThReqPor.cpp MCMultiCore/MCThReqPor.h
+    MCMultiCore/MCCPPThPor.cpp MCMultiCore/MCCPPThPor.h
+    threadSOG.cpp threadSOG.h
+    HybridSOG.cpp HybridSOG.h
+    Hybrid/MCHybrid/MCHybridSOG.cpp Hybrid/MCHybrid/MCHybridSOG.h
+    MCMultiCore/ModelCheckThReq.cpp MCMultiCore/ModelCheckThReq.h
+    Hybrid/MCHybridReq/MCHybridSOGReq.cpp
+    Hybrid/MCHybridReq/MCHybridSOGReq.h
+    Hybrid/MCHybridReqPOR/MCHybridSOGReqPOR.cpp
+    Hybrid/MCHybridReqPOR/MCHybridSOGReqPOR.h
+    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
+        )
 
 
 target_include_directories(pmc-sog PUBLIC  "${PROJECT_BINARY_DIR}/src")

src/CommonSOG.cpp

@@ -127,8 +127,8 @@ bool CommonSOG::Set_Div(const MDD &M) const {
     do {
         Reached = lddmc_false;
         for (const auto&  i: m_nonObservable) {
-            MDD To = SylvanWrapper::lddmc_firing_mono(From, m_tb_relation[(i)].getMinus(),
-                                                      m_tb_relation[(i)].getPlus());
+            MDD To = SylvanWrapper::lddmc_firing_mono(From, m_tb_relation[i].getMinus(),
+                                                      m_tb_relation[i].getPlus());
             Reached = SylvanWrapper::lddmc_union_mono(Reached, To);
         }
 

src/Hybrid/HybridKripkeIterator.cpp

@@ -6,7 +6,7 @@
 
 HybridKripkeIterator::HybridKripkeIterator(HybridKripkeState &st, bdd cnd): kripke_succ_iterator(cnd)
 {
-   
+
     m_current_state=&st;
     
 }

src/LDDGraph.cpp

@@ -32,7 +32,7 @@ LDDState *LDDGraph::insertFindByMDD(MDD md, bool &found) {
             }
         }
 
-    LDDState *n = new LDDState;
+    auto *n = new LDDState;
     n->m_lddstate = md;
     found = false;
     m_GONodes.push_back(n);
@@ -106,7 +106,7 @@ void LDDGraph::insertSHA(LDDState *c) {
 
 /*----------------------Visualisation du graphe------------------------*/
 void LDDGraph::printCompleteInformation() {
-    long count_ldd = 0L;
+    size_t count_ldd = 0L;
     for (const auto & i : m_GONodes) {
         count_ldd += SylvanWrapper::lddmc_nodecount(i->m_lddstate);
         m_nbMarking += SylvanWrapper::getMarksCount(i->m_lddstate);
@@ -141,9 +141,9 @@ void LDDGraph::printGraph(LDDState *s, size_t &nb) {
         cout << "\nSTATE NUMBER " << nb << " sha : " << s->getSHAValue() << " LDD v :" << s->getLDDValue() << endl;
 
         s->setVisited();
-        LDDEdges::const_iterator i;
+
         for (const auto & i:  s->Successors) {
-            if (i.first->isVisited() == false) {
+            if (!i.first->isVisited()) {
                 ++nb;
                 printGraph(i.first, nb);
             }

src/LDDState.cpp

@@ -8,7 +8,7 @@ LDDState::~LDDState()=default;
 void LDDState::setLDDValue(const MDD & m) {
     m_lddstate=m;
 }
-MDD  LDDState::getLDDValue() {
+MDD  LDDState::getLDDValue() const {
     return m_lddstate;
 }
 
@@ -23,7 +23,7 @@ vector<pair<LDDState*, int>>* LDDState::getSuccessors() {
     return &Successors;
 }
 
-vector<uint16_t> LDDState::getMarkedPlaces(set<uint16_t>& lplacesAP) {
+vector<uint16_t> LDDState::getMarkedPlaces(set<uint16_t>& lplacesAP) const {
     vector<uint16_t> result;
     MDD mdd=m_lddstate;
     int depth=0;
@@ -40,7 +40,7 @@ vector<uint16_t> LDDState::getMarkedPlaces(set<uint16_t>& lplacesAP) {
     return result;
 }
 
-vector<uint16_t> LDDState::getUnmarkedPlaces(set<uint16_t>& lplacesAP) {
+vector<uint16_t> LDDState::getUnmarkedPlaces(set<uint16_t>& lplacesAP) const {
     vector<uint16_t> result;
     MDD mdd=m_lddstate;
     int depth=0;

src/LDDState.h

@@ -23,7 +23,7 @@ class LDDState {
   vector<pair<LDDState*, int> > Predecessors, Successors;
 
   void setLDDValue(const MDD& m);
-  MDD getLDDValue();
+  MDD getLDDValue() const;
   MDD m_lddstate=0;
   unsigned char m_SHA2[81];
   unsigned char* getSHAValue();
@@ -39,8 +39,8 @@ class LDDState {
   [[nodiscard]] inline bool isVisited() const {return m_visited;}
   void setCompletedSucc() {m_completed=true;}
   bool isCompletedSucc() {return m_completed;}
-  vector<uint16_t> getMarkedPlaces(set<uint16_t>& lplacesAP);
-  vector<uint16_t> getUnmarkedPlaces(set<uint16_t>& lplacesAP);
+  vector<uint16_t> getMarkedPlaces(set<uint16_t>& lplacesAP) const;
+  vector<uint16_t> getUnmarkedPlaces(set<uint16_t>& lplacesAP) const;
   void setProcess(const uint16_t& v) {m_process=v;}
   [[nodiscard]] uint16_t getProcess() const {return m_process;}
   inline void decNbSuccessors() {m_nbSuccessorsToBeProcessed--;}

src/MCMultiCore/ModelCheckerCPPThread.cpp

@@ -36,7 +36,7 @@ void ModelCheckerCPPThread::Compute_successors() {
 
     id_thread = m_id_thread++;
 
-    //cout<<" I'm here thread id " <<m_id_thread<<endl;
+
     Set fire;
 
     if (id_thread == 0) {
@@ -59,7 +59,8 @@ void ModelCheckerCPPThread::Compute_successors() {
     Pair e;
     do {
         std::unique_lock<std::mutex> lk(m_mutexStack);
-        m_condStack.wait(lk, std::bind(&ModelCheckerCPPThread::hasToProcess, this));
+        //m_condStack.wait(lk, std::bind(&ModelCheckerCPPThread::hasToProcess, this));
+        m_condStack.wait(lk, [this](){return  this->hasToProcess();});
         lk.unlock();
 
         if (m_common_stack.try_pop(e) && !m_finish) {
@@ -88,6 +89,8 @@ void ModelCheckerCPPThread::Compute_successors() {
         } //end advance
 
     } while (!m_finish);
+
+
 }
 
 void ModelCheckerCPPThread::threadHandler(void *context) {

src/MCMultiCore/ModelCheckerCPPThread.h

@@ -8,7 +8,7 @@
 #include <mutex>
 #include <condition_variable>
 typedef pair<LDDState *, int> couple_th;
-typedef stack<pair<LDDState *,int>> pile_t;
+
 /*
  * Multi-threading with C++14 Library
  */
@@ -20,6 +20,7 @@ public:
     static void threadHandler(void *context);
     void Compute_successors();
     void ComputeTh_Succ();
+    //LDDState * getInitialMetaState() override;
 private:
     void preConfigure();
     bool hasToProcess() const;

src/SogKripke.cpp

@@ -14,6 +14,7 @@ SogKripke::SogKripke(const bdd_dict_ptr &dict_ptr,LDDGraph *sog): spot::kripke(d
 {
     SogKripkeIterator::m_graph=sog;
     SogKripkeIterator::m_dict_ptr=&dict_ptr;
+    SogKripkeIterator::m_deadlock.setLDDValue(1);
 }
 
 SogKripke::SogKripke(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog,set<string> &l_transap,set<string> &l_placeap):SogKripke(dict_ptr,sog) {

src/SogKripkeIterator.cpp

@@ -6,15 +6,17 @@
 
 SogKripkeIterator::SogKripkeIterator(const LDDState* lddstate, bdd cond):kripke_succ_iterator(cond),m_lddstate(lddstate)
 {
-    //vector<pair<LDDState*, int>>
-    m_lddstate->setDiv(true);
+
+   // m_lddstate->setDeadLock(true);
     for (const auto & elt : *(m_lddstate->getSuccessors())) {
         m_lsucc.push_back(elt);
     }
-   /* if (lddstate->isDeadLock()) {
-        m_lsucc.push_back(pair(,-1));
-    }*/
+    if ( lddstate->isDeadLock() ) {
+
+        m_lsucc.emplace_back( m_lddstate,-1 );
+   }
     if (lddstate->isDiv()) {
+
         m_lsucc.push_back(pair<LDDState*,int>(m_lddstate,-1));
     }
 }
@@ -68,3 +70,4 @@ SogKripkeIterator::~SogKripkeIterator()
 
 static LDDGraph * SogKripkeIterator::m_graph;
 static spot::bdd_dict_ptr* SogKripkeIterator::m_dict_ptr;
+LDDState SogKripkeIterator::m_deadlock;

src/SogKripkeIterator.h

@@ -7,7 +7,7 @@
 class SogKripkeIterator : public spot::kripke_succ_iterator
 {
     public:
-
+        static LDDState m_deadlock;
         static LDDGraph * m_graph;
         static spot::bdd_dict_ptr* m_dict_ptr;
         SogKripkeIterator(const LDDState *lddstate,bdd cond);

src/SogKripkeIteratorTh.cpp

@@ -8,15 +8,15 @@ SogKripkeIteratorTh::SogKripkeIteratorTh ( LDDState* lddstate, bdd cnd ) :m_ldds
 {
     m_lsucc.reserve(m_lddstate->getSuccessors()->size()+ 2);
     if ( lddstate->isDeadLock() ) {
-        m_lsucc.push_back ( pair<LDDState*,int> ( &m_deadlock,-1 ) );
+        // cout<<"deadlock"<<endl;
+        m_lsucc.emplace_back(make_pair( &m_deadlock,-1) );
     }
     if ( lddstate->isDiv() ) {
-        m_lsucc.push_back ( pair<LDDState*,int> ( (LDDState*)lddstate,-1 ) );
+        m_lsucc.emplace_back( lddstate,-1 );
     }
 
-    for ( int i=0; i<m_lddstate->getSuccessors()->size(); i++ ) {
-        m_lsucc.push_back ( m_lddstate->getSuccessors()->at ( i ) );
-    }
+    for (const auto & elt : *(m_lddstate->getSuccessors()))
+        m_lsucc.emplace_back(elt);
 
 
 }
@@ -26,7 +26,7 @@ bool SogKripkeIteratorTh::first()
     // cout<<"entering "<<__func__<<endl;
     m_current_edge=0;
     //cout<<"exciting "<<__func__<<endl;
-    return m_lsucc.size() !=0;
+    return !m_lsucc.empty();
 
 }
 
@@ -53,6 +53,7 @@ SogKripkeStateTh* SogKripkeIteratorTh::dst() const
 
 bdd SogKripkeIteratorTh::cond()  const
 {
+
     if ( m_lsucc.at ( m_current_edge ).second==-1 ) {
         return bddtrue;
     }
@@ -68,13 +69,9 @@ SogKripkeIteratorTh::~SogKripkeIteratorTh()
     //dtor
 }
 
-void SogKripkeIteratorTh::recycle ( LDDState* aggregate, bdd cond )
-{
-    m_lddstate=aggregate;
-    spot::kripke_succ_iterator::recycle ( cond );
-}
+
 
 ModelCheckBaseMT * SogKripkeIteratorTh::m_builder;
 spot::bdd_dict_ptr* SogKripkeIteratorTh::m_dict_ptr;
 LDDState SogKripkeIteratorTh::m_deadlock;
-//LDDState SogKripkeIteratorTh::m_div;
+LDDState SogKripkeIteratorTh::m_div;