modified: CMakeLists.txt

	modified:   src/CommonSOG.h
	modified:   src/LDDGraph.cpp
	modified:   src/ModelCheckerTh.cpp
	modified:   src/ModelCheckerThV2.cpp
	modified:   src/SafeDequeue.cpp
	modified:   src/SafeDequeue.h
	modified:   src/stacksafe.cpp
	modified:   src/stacksafe.h
	modified:   third-party/sylvan

CMakeLists.txt

@@ -4,14 +4,16 @@ cmake_minimum_required(VERSION 3.8 FATAL_ERROR)
 # project name and language
 project(pmc-sog C CXX)
 
-# C++17 standard
-set(CMAKE_CXX_STANDARD 17)
+
+set(CMAKE_CXX_STANDARD 14)
 set(CMAKE_CXX_STANDARD_REQUIRED ON)
 set(CMAKE_CXX_EXTENSIONS OFF)
 
 # Add compiler flags
 if(CMAKE_COMPILER_IS_GNUCC)
-  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fpermissive")
+
+  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fpermissive -std=c++14")
+
 endif()
 
 # add pn parser

src/CommonSOG.h

@@ -41,9 +41,7 @@ class CommonSOG
         Set m_nonObservable;
         Set InterfaceTrans;
         set<uint16_t> m_place_proposition;
-
         vector<class Transition> m_transitions;
-
         MDD Accessible_epsilon(MDD From);
         Set firable_obs(MDD State);
         MDD get_successor(MDD From, int t);

src/LDDGraph.cpp

@@ -20,7 +20,7 @@ LDDState *LDDGraph::getInitialState() const {
 
 /*----------------------find()----------------*/
 LDDState *LDDGraph::find(LDDState *c) {
-    std::scoped_lock lock(m_mutex);
+    std::lock_guard<std::mutex>  lock(m_mutex);
     for (MetaLDDNodes::const_iterator i = m_GONodes.begin(); !(i == m_GONodes.end()); i++)
         if (c->m_lddstate == (*i)->m_lddstate)
             return *i;
@@ -29,7 +29,7 @@ LDDState *LDDGraph::find(LDDState *c) {
 
 LDDState *LDDGraph::insertFind(LDDState *c) {
     LDDState *res = nullptr;
-    std::scoped_lock lock(m_mutex);
+    std::lock_guard<std::mutex> lock(m_mutex);
     for (MetaLDDNodes::const_iterator i = m_GONodes.begin(); !(i == m_GONodes.end()) && res == nullptr; i++) {
         if (c->m_lddstate == (*i)->m_lddstate)
             res = *i;
@@ -49,7 +49,7 @@ bool LDDGraph::cmpSHA(const unsigned char *s1, const unsigned char *s2) {
 }
 
 LDDState *LDDGraph::findSHA(unsigned char *c) {
-    std::scoped_lock lock(m_mutex_sha);
+    std::lock_guard<std::mutex> lock(m_mutex_sha);
     for (MetaLDDNodes::const_iterator i = m_GONodes.begin(); !(i == m_GONodes.end()); i++)
         if ((*i)->isVirtual() == true)
             if ((cmpSHA(c, (unsigned char *) (*i)->m_SHA2) == 0))
@@ -60,7 +60,7 @@ LDDState *LDDGraph::findSHA(unsigned char *c) {
 /***   Try to find an aggregate by its md5 code, else it is inserted***/
 LDDState *LDDGraph::insertFindSha(unsigned char *c, LDDState *agg) {
     LDDState *res = nullptr;
-    std::scoped_lock lock(m_mutex_sha);
+    std::lock_guard<std::mutex> lock(m_mutex_sha);
     for (auto i = m_GONodes.begin(); !(i == m_GONodes.end()) && !res; i++) {
         if ((*i)->isVirtual() == true)
             if ((cmpSHA(c, (unsigned char *) (*i)->m_SHA2) == 0))
@@ -89,7 +89,7 @@ size_t LDDGraph::findSHAPos(unsigned char *c, bool &res) {
 
 /*----------------------insert() ------------*/
 void LDDGraph::insert(LDDState *c) {
-    std::scoped_lock lock(m_mutex);
+    std::lock_guard<std::mutex> lock(m_mutex);
     this->m_GONodes.push_back(c);
     m_nbStates++;
 }

src/ModelCheckerTh.cpp

@@ -23,7 +23,7 @@ void ModelCheckerTh::preConfigure() {
 	lace_startup(0, NULL, NULL);
 	size_t max = 16LL<<30;
 	if (max > getMaxMemory()) max = getMaxMemory()/10*9;
-	sylvan_set_limits(max, 8, 0);
+	sylvan_set_limits(16LL<<30, 8, 0);
 
 	sylvan_init_package();
 	sylvan_init_ldd();

src/ModelCheckerThV2.cpp

@@ -32,12 +32,9 @@ void ModelCheckerThV2::preConfigure()
 
     sylvan_init_package();
     sylvan_init_ldd();
+    init_gc_seq();
     displayMDDTableInfo();
-
     vector<Place>::const_iterator it_places;
-
-    init_gc_seq();
-
     m_transitions = m_net->transitions;
     m_observable = m_net->Observable;
     m_place_proposition = m_net->m_formula_place;
@@ -119,10 +116,10 @@ void ModelCheckerThV2::Compute_successors()
         c->m_lddstate = Complete_meta_state;
         c->setDeadLock ( Set_Bloc ( Complete_meta_state ) );
         c->setDiv ( Set_Div ( Complete_meta_state ) );
-        m_common_stack.push ( Pair ( couple ( c, Complete_meta_state ), fire ) );
-        m_condStack.notify_one();        
         m_graph->setInitialState ( c );
         m_graph->insert ( c );
+        m_common_stack.push ( Pair ( couple ( c, Complete_meta_state ), fire ) );
+        m_condStack.notify_one();
         m_finish_initial = true;
     }
 
@@ -139,8 +136,8 @@ void ModelCheckerThV2::Compute_successors()
                 while ( !e.second.empty() && !m_finish ) {
                     int t = *e.second.begin();
                     e.second.erase ( t );
-                   
                     MDD reduced_meta = Accessible_epsilon ( get_successor ( e.first.second, t ) );
+
                     ldd_refs_push ( reduced_meta );
                     reached_class = new LDDState();
                     reached_class->m_lddstate = reduced_meta;                    

src/SafeDequeue.cpp

@@ -27,7 +27,7 @@ SafeDequeue<T>::SafeDequeue()
 template<typename T>
 SafeDequeue<T>::SafeDequeue ( const SafeDequeue& other )
 {
-    std::scoped_lock lk ( other.mut );
+    std::lock_guard<std::mutex> lk ( other.mut );
     data_queue=other.data_queue;
 }
 
@@ -40,7 +40,7 @@ SafeDequeue<T>::~SafeDequeue()
 template<typename T>
 void SafeDequeue<T>::push ( T new_value )
 {
-    std::scoped_lock lk ( mut );
+    std::lock_guard<std::mutex> lk ( mut );
     data_queue.push ( new_value );
     data_cond.notify_one();
 
@@ -65,7 +65,7 @@ std::shared_ptr<T> SafeDequeue<T>::wait_and_pop()
 template<typename T>
 bool SafeDequeue<T>::try_pop ( T& value )
 {
-    std::scoped_lock lk ( mut );
+    std::lock_guard<std::mutex> lk ( mut );
     if ( data_queue.empty() ) {
         return false;
     }
@@ -78,7 +78,7 @@ bool SafeDequeue<T>::try_pop ( T& value )
 template<typename T>
 std::shared_ptr<T> SafeDequeue<T>::try_pop()
 {
-    std::scoped_lock lk ( mut );
+    std::lock_guard<std::mutex> lk ( mut );
     if ( data_queue.empty() ) {
         return std::shared_ptr<T>();
     }
@@ -90,7 +90,7 @@ std::shared_ptr<T> SafeDequeue<T>::try_pop()
 template<typename T>
 bool SafeDequeue<T>::empty() const
 {
-    std::scoped_lock lk ( mut );
+    std::lock_guard<std::mutex> lk ( mut );
     return data_queue.empty();
 }
 

src/SafeDequeue.h

@@ -38,7 +38,7 @@ struct empty_queue: std::exception {
 template<typename T>
 class SafeDequeue {
     private:
-        std::mutex mut;
+        mutable std::mutex mut;
         std::queue<T> data_queue;
         std::condition_variable data_cond;
 

src/stacksafe.cpp

@@ -22,19 +22,19 @@ StackSafe<T>::StackSafe() {}
 template<typename T>
 StackSafe<T>::StackSafe ( const StackSafe& other)
 {
-    std::scoped_lock lock ( other.m_mutex );
+    std::lock_guard<std::mutex> lock ( other.m_mutex );
     m_data=other.m_data;
 }
 
 template<typename T>
 void StackSafe<T>::push ( T new_value ){
-    std::scoped_lock lock ( m_mutex );
+    std::lock_guard<std::mutex> lock ( m_mutex );
     m_data.push ( std::move ( new_value ) );
 }
 template<typename T>
 std::shared_ptr<T> StackSafe<T>::pop()
 {
-    std::scoped_lock lock(m_mutex); 
+    std::lock_guard<std::mutex> lock(m_mutex);
     if(m_data.empty()) throw empty_stack();
     std::shared_ptr<T> const res(std::make_shared<T>(m_data.top()));
     m_data.pop();
@@ -43,7 +43,7 @@ std::shared_ptr<T> StackSafe<T>::pop()
 template<typename T>
 void StackSafe<T>::pop(T& value)
 {
-    std::scoped_lock lock(m_mutex);
+    std::lock_guard<std::mutex> lock(m_mutex);
     if(m_data.empty()) throw empty_stack();
     value=m_data.top();
     m_data.pop();
@@ -51,7 +51,7 @@ void StackSafe<T>::pop(T& value)
 template<typename T>
 bool StackSafe<T>::try_pop(T& value)
 {
-    std::scoped_lock lock(m_mutex);
+    std::lock_guard<std::mutex> lock(m_mutex);
     if(m_data.empty()) return false;
     value=m_data.top();
     m_data.pop();

src/stacksafe.h

@@ -46,7 +46,7 @@ template<typename T> class StackSafe {
         void pop ( T& value );
         bool try_pop ( T& value );
         bool empty() const {
-            std::scoped_lock lock(m_mutex);
+            std::lock_guard<std::mutex> lock(m_mutex);
             return m_data.empty();
         };
     };

sylvan @ a88d8802

-Subproject commit 97208c7f528f08a91afa99da0d43c6734d36cfa4
+Subproject commit a88d88020693b35b272800fe0ded4293a22720e2