diff --git a/CMakeLists.txt b/CMakeLists.txt
index 746dbc4eeba539a988e4850723cbdb8426f535ca..990d917d17ed365c14997ae7a4ef3f69d930e1f5 100644
--- a/CMakeLists.txt
+++ b/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
diff --git a/src/CommonSOG.h b/src/CommonSOG.h
index a7b10033866af9fa9b53906f551fcedfec711fe6..1b59950b5c9c0b7399abaabc4da7279f140369f3 100644
--- a/src/CommonSOG.h
+++ b/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);
diff --git a/src/LDDGraph.cpp b/src/LDDGraph.cpp
index e75a437300a4a53d42dcd9ae22ec08976e2b3602..21e6d65df06740424dd73a4853925ad98f4c67bc 100644
--- a/src/LDDGraph.cpp
+++ b/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++;
}
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index 52ccf04ec5ca3b1f9b73a52dc1abffd434ea5c15..de81add4746e64f0d75ef894d5107b31dae8a7b3 100644
--- a/src/ModelCheckerTh.cpp
+++ b/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();
diff --git a/src/ModelCheckerThV2.cpp b/src/ModelCheckerThV2.cpp
index 4729ae8373b055f29e625166df372962e4a2ef95..12b4efa71498cc5d06f65a46afea0b31f6d972ad 100644
--- a/src/ModelCheckerThV2.cpp
+++ b/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;
diff --git a/src/SafeDequeue.cpp b/src/SafeDequeue.cpp
index fd4b282f2c7cc907dda5cb656d283b130c51e844..429c78fe2027bc326b8269105566be80c769eeea 100644
--- a/src/SafeDequeue.cpp
+++ b/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();
}
diff --git a/src/SafeDequeue.h b/src/SafeDequeue.h
index 22b983b5f1b410ffaa335c90b2a209ab8933f397..607f0851d35d32f32a28e54ace7aeaf09d892248 100644
--- a/src/SafeDequeue.h
+++ b/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;
diff --git a/src/stacksafe.cpp b/src/stacksafe.cpp
index 6b381d20ab35c959886f279b974c85c50247b55b..9b642a4a4c75f96431f24715bb97efc64525854a 100644
--- a/src/stacksafe.cpp
+++ b/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();
diff --git a/src/stacksafe.h b/src/stacksafe.h
index 723cf901259c03bfeebcb79346a8e1d666ead5a8..dd5318c4788ef727da4b4cf31ccd2a311d3a59df 100644
--- a/src/stacksafe.h
+++ b/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();
};
};
diff --git a/third-party/sylvan b/third-party/sylvan
index 97208c7f528f08a91afa99da0d43c6734d36cfa4..a88d88020693b35b272800fe0ded4293a22720e2 160000
--- a/third-party/sylvan
+++ b/third-party/sylvan
@@ -1 +1 @@
-Subproject commit 97208c7f528f08a91afa99da0d43c6734d36cfa4
+Subproject commit a88d88020693b35b272800fe0ded4293a22720e2