diff --git a/CMakeLists.txt b/CMakeLists.txt
index f11cb076b140cfc115a6725bff79905019e9de7b..4636699fe4808f4a55ece8b37ae333d2eeb0a4ff 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -6,7 +6,7 @@ project(pmc-sog C CXX)
# compiler flags
if(CMAKE_COMPILER_IS_GNUCC)
- set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fpermissive -g3")
+ set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fpermissive -g3 -std=c++17")
endif()
# add pn parser
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index f8861e386b05948d48f75819e19a85b910a7e609..cbf7ecbe4c2dff51b7fd521589cd4de86c59af78 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -63,6 +63,10 @@ add_executable(mc-sog main.cpp
SogKripkeIteratorTh.h
ModelCheckerTh.cpp
ModelCheckerTh.h
+ stacksafe.cpp
+ stacksafe.h
+ ModelCheckerThV2.cpp
+ ModelCheckerThV2.h
MCHybridSOG.cpp
MCHybridSOG.h
HybridKripke.cpp
diff --git a/src/ModelCheckerTh.h b/src/ModelCheckerTh.h
index 58bce47f2fc6dc1782fcbb111118b87f82001af9..ae0ff73da642e964bc754a754d1a9c39770cbefe 100644
--- a/src/ModelCheckerTh.h
+++ b/src/ModelCheckerTh.h
@@ -30,7 +30,7 @@ private:
pthread_barrier_t m_barrier_builder;
unsigned int m_gc=0; //
- bool m_finish=false;
+ volatile bool m_finish=false;
bool m_finish_initial=false;
pthread_mutex_t m_mutex_stack[128];
pthread_t m_list_thread[128];
diff --git a/src/ModelCheckerThV2.cpp b/src/ModelCheckerThV2.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..f1f9c3d7918de075a11d76baab544737164cb9aa
--- /dev/null
+++ b/src/ModelCheckerThV2.cpp
@@ -0,0 +1,282 @@
+#include "ModelCheckerThV2.h"
+#include "sylvan.h"
+#include "sylvan_seq.h"
+#include <sylvan_sog.h>
+#include <sylvan_int.h>
+
+using namespace sylvan;
+using namespace std;
+
+ModelCheckerThV2::ModelCheckerThV2 ( const NewNet &R, int nbThread ) :
+ ModelCheckBaseMT ( R, nbThread )
+{
+}
+size_t
+getMaxMemoryV3()
+{
+ long pages = sysconf ( _SC_PHYS_PAGES );
+ long page_size = sysconf ( _SC_PAGE_SIZE );
+ return pages * page_size;
+}
+void ModelCheckerThV2::preConfigure()
+{
+
+ lace_init ( 1, 0 );
+ lace_startup ( 0, NULL, NULL );
+ size_t max = 16LL<<30;
+ if ( max > getMaxMemoryV3() ) {
+ max = getMaxMemoryV3() /10*9;
+ }
+ sylvan_set_limits ( max, 8, 0 );
+
+ sylvan_init_package();
+ sylvan_init_ldd();
+ displayMDDTableInfo();
+
+ vector<Place>::const_iterator it_places;
+
+ init_gc_seq();
+
+
+ transitions = m_net->transitions;
+ m_observable = m_net->Observable;
+ m_place_proposition = m_net->m_formula_place;
+ m_nonObservable = m_net->NonObservable;
+
+ m_transitionName = m_net->transitionName;
+ m_placeName = m_net->m_placePosName;
+
+ InterfaceTrans = m_net->InterfaceTrans;
+
+ cout << "Nombre de places : " << m_nbPlaces << endl;
+ cout << "Derniere place : " << m_net->places[m_nbPlaces - 1].name << endl;
+
+ uint32_t *liste_marques = new uint32_t[m_net->places.size()];
+ uint32_t i;
+ for ( i = 0, it_places = m_net->places.begin(); it_places != m_net->places.end(); i++, it_places++ ) {
+ liste_marques[i] = it_places->marking;
+ }
+
+ m_initialMarking = lddmc_cube ( liste_marques, m_net->places.size() );
+ ldd_refs_push ( m_initialMarking );
+ uint32_t *prec = new uint32_t[m_nbPlaces];
+ uint32_t *postc = new uint32_t[m_nbPlaces];
+ // Transition relation
+ for ( vector<Transition>::const_iterator t = m_net->transitions.begin(); t != m_net->transitions.end(); t++ ) {
+ // Initialisation
+ for ( i = 0; i < m_nbPlaces; i++ ) {
+ prec[i] = 0;
+ postc[i] = 0;
+ }
+ // Calculer les places adjacentes a la transition t
+ set<int> adjacentPlace;
+ for ( vector<pair<int, int> >::const_iterator it = t->pre.begin(); it != t->pre.end(); it++ ) {
+ adjacentPlace.insert ( it->first );
+ prec[it->first] = prec[it->first] + it->second;
+ //printf("It first %d \n",it->first);
+ //printf("In prec %d \n",prec[it->first]);
+ }
+ // arcs post
+ for ( vector<pair<int, int> >::const_iterator it = t->post.begin(); it != t->post.end(); it++ ) {
+ adjacentPlace.insert ( it->first );
+ postc[it->first] = postc[it->first] + it->second;
+
+ }
+ for ( set<int>::const_iterator it = adjacentPlace.begin(); it != adjacentPlace.end(); it++ ) {
+ MDD Precond = lddmc_true;
+ Precond = Precond & ( ( *it ) >= prec[*it] );
+ }
+
+ MDD _minus = lddmc_cube ( prec, m_nbPlaces );
+ ldd_refs_push ( _minus );
+ MDD _plus = lddmc_cube ( postc, m_nbPlaces );
+ ldd_refs_push ( _plus );
+ m_tb_relation.push_back ( TransSylvan ( _minus, _plus ) );
+ }
+ delete[] prec;
+ delete[] postc;
+ ComputeTh_Succ();
+
+}
+
+LDDState* ModelCheckerThV2::getInitialMetaState()
+{
+ while ( !m_finish_initial ) ;
+ LDDState *initial_metastate = m_graph->getInitialState();
+ if ( !initial_metastate->isVisited() ) {
+ initial_metastate->setVisited();
+ while ( !initial_metastate->isCompletedSucc() )
+ ;
+ }
+ return initial_metastate;
+}
+
+void ModelCheckerThV2::buildSucc ( LDDState *agregate )
+{
+ if ( !agregate->isVisited() ) {
+ agregate->setVisited();
+ while ( !agregate->isCompletedSucc() )
+ ;
+ }
+}
+
+void ModelCheckerThV2::Compute_successors()
+{
+ int id_thread;
+ {
+ std::scoped_lock guard ( m_mutex );
+ id_thread = m_id_thread++;
+ }
+ //cout<<" I'm here thread id " <<m_id_thread<<endl;
+ Set fire;
+ int min_charge = 0;
+ m_started=false;
+ if ( id_thread == 0 ) {
+ LDDState *c = new LDDState;
+ MDD Complete_meta_state=Accessible_epsilon ( m_initialMarking );
+ ldd_refs_push ( Complete_meta_state );
+
+ fire = firable_obs ( Complete_meta_state );
+ 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_started=true;
+ m_graph->setInitialState ( c );
+ m_graph->insert ( c );
+ m_finish_initial = true;
+
+ }
+
+ LDDState *reached_class;
+ //pthread_barrier_wait ( &m_barrier_builder );
+ do {
+ Pair e;
+ while ( !m_common_stack.empty() && !m_finish ) {
+ m_terminaison++;
+ bool advance=true;
+ try {
+ m_common_stack.pop ( e );
+ } catch ( ... ) {
+ advance=false;
+ }
+
+ if ( advance ) {
+ while ( !e.second.empty() && !m_finish ) {
+ int t = *e.second.begin();
+ e.second.erase ( t );
+ if ( id_thread ) {
+ std::scoped_lock supervise ( m_supervise_gc_mutex );
+ m_gc++;
+ if ( m_gc == 1 ) {
+ m_gc_mutex.lock();
+ }
+ }
+
+ //MDD reduced_meta = Complete_meta_state; //Canonize(Complete_meta_state,0);
+ /*ldd_refs_push(reduced_meta);*/
+ if ( id_thread == 0 ) {
+ std::scoped_lock guard ( m_gc_mutex );
+ // #ifdef DEBUG_GC
+ //displayMDDTableInfo();
+ // #endif // DEBUG_GC
+ sylvan_gc_seq();
+ // #ifdef DEBUG_GC
+ //displayMDDTableInfo();
+ // #endif // DEBUG_GC
+ }
+
+ //pthread_spin_lock(&m_accessible);
+
+ 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;
+ m_graph_mutex.lock();
+ LDDState *pos = m_graph->find ( reached_class );
+ if ( !pos ) {
+ // cout<<"not found"<<endl;
+
+ m_graph->addArc();
+ m_graph->insert ( reached_class );
+ m_graph_mutex.unlock();
+ //reached_class->setDiv(Set_Div(reduced_meta));
+ //reached_class->setDeadLock(Set_Bloc(reduced_meta));
+ fire = firable_obs ( reduced_meta );
+ reached_class->setDeadLock ( Set_Bloc ( reduced_meta ) );
+ reached_class->setDiv ( Set_Div ( reduced_meta ) );
+
+
+ m_common_stack.push ( Pair ( couple ( reached_class, reduced_meta ), fire ) );
+
+ e.first.first->Successors.insert ( e.first.first->Successors.begin(), LDDEdge ( reached_class, t ) );
+ reached_class->Predecessors.insert ( reached_class->Predecessors.begin(), LDDEdge ( e.first.first, t ) );
+
+ //pthread_mutex_lock(&m_mutex);
+
+
+ } else {
+ m_graph->addArc();
+ m_graph_mutex.unlock();
+ e.first.first->Successors.insert ( e.first.first->Successors.begin(), LDDEdge ( pos, t ) );
+ pos->Predecessors.insert ( pos->Predecessors.begin(), LDDEdge ( e.first.first, t ) );
+ delete reached_class;
+ }
+ if ( id_thread ) {
+ std::scoped_lock guard ( m_supervise_gc_mutex );
+ m_gc--;
+ if ( m_gc == 0 ) {
+ m_gc_mutex.unlock();
+ }
+
+ }
+ }
+ e.first.first->setCompletedSucc();
+ } //end advance
+ m_terminaison--;
+ }
+
+ } while ( !m_finish );
+ pthread_barrier_wait ( &m_barrier_builder );
+
+}
+
+void ModelCheckerThV2::threadHandler ( void *context )
+{
+ ( ( ModelCheckerThV2* ) context )->Compute_successors();
+}
+
+void ModelCheckerThV2::ComputeTh_Succ()
+{
+
+ m_id_thread = 0;
+
+
+
+ /* pthread_barrier_init(&m_barrier_threads, NULL, m_nb_thread+1);*/
+ pthread_barrier_init ( &m_barrier_builder, NULL, m_nb_thread + 1 );
+
+
+ m_gc=0;
+ m_terminaison=0;
+ m_finish=false;
+ for ( int i = 0; i < m_nb_thread; i++ ) {
+ int rc;
+ m_list_thread[i]= new thread ( threadHandler,this );
+ if ( m_list_thread==nullptr ) {
+ cout << "error: pthread_create, rc: " << rc << endl;
+ }
+ }
+}
+
+ModelCheckerThV2::~ModelCheckerThV2()
+{
+ m_finish = true;
+ pthread_barrier_wait ( &m_barrier_builder );
+ for ( int i = 0; i < m_nb_thread; i++ ) {
+ m_list_thread[i]->join();
+ delete m_list_thread[i];
+ }
+
+}
+
diff --git a/src/ModelCheckerThV2.h b/src/ModelCheckerThV2.h
new file mode 100644
index 0000000000000000000000000000000000000000..987b7de6839b784acd23b2f352655a6dae8fda60
--- /dev/null
+++ b/src/ModelCheckerThV2.h
@@ -0,0 +1,37 @@
+#ifndef MODELCHECKERTHV2_H
+#define MODELCHECKERTHV2_H
+#include "ModelCheckBaseMT.h"
+#include "stacksafe.h"
+#include <atomic>
+#include <thread>
+#include <mutex>
+typedef pair<LDDState *, int> couple_th;
+typedef stack<pair<LDDState *,int>> pile_t;
+
+class ModelCheckerThV2 : public ModelCheckBaseMT
+{
+public:
+ ModelCheckerThV2(const NewNet &R,int nbThread);
+ ~ModelCheckerThV2();
+ LDDState * getInitialMetaState();
+ void buildSucc(LDDState *agregate);
+ static void threadHandler(void *context);
+ void Compute_successors();
+ void ComputeTh_Succ();
+private:
+ void preConfigure();
+
+
+ StackSafe<Pair> m_common_stack;
+ bool m_started=false;
+
+ int m_id_thread;
+ std::mutex m_mutex,m_graph_mutex,m_gc_mutex,m_supervise_gc_mutex;
+ pthread_barrier_t m_barrier_builder;
+ atomic<uint32_t> m_gc,m_terminaison; //
+ volatile bool m_finish=false;
+ bool m_finish_initial=false;
+ pthread_mutex_t m_mutex_stack[128];
+ thread* m_list_thread[128];
+};
+#endif
diff --git a/src/main.cpp b/src/main.cpp
index 0f773efc82f9ba2c159f83413559b7dde77423bd..aa3f8247b37efade5a5cef9fc755b584d2602164 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -13,6 +13,7 @@
#include "LDDGraph.h"
#include "ModelCheckLace.h"
#include "ModelCheckerTh.h"
+#include "ModelCheckerThV2.h"
#include <spot/misc/version.hh>
#include <spot/twaalgos/dot.hh>
@@ -118,12 +119,14 @@ int main(int argc, char **argv) {
MPI_Comm_rank(MPI_COMM_WORLD, &task_id);
if (n_tasks == 1) {
- if (n_tasks == 1 && (!strcmp(argv[1], "otfL") || !strcmp(argv[1], "otfP"))) {
+ if (n_tasks == 1 && (!strcmp(argv[1], "otfL") || !strcmp(argv[1], "otfC") || !strcmp(argv[1], "otfP"))) {
cout << "Performing on the fly Model checking..." << endl;
if (!strcmp(argv[1], "otfP"))
cout << "Multi-threaded algorithm based on Pthread library!" << endl;
- else
+ else if (!strcmp(argv[1], "otfL"))
cout << "Multi-threaded algorithm based on Lace framework!" << endl;
+ else
+ cout << "Multi-threaded algorithm based on C++ Thread library!" << endl;
cout << "Building automata for not(formula)\n";
auto d = spot::make_bdd_dict();
@@ -144,8 +147,10 @@ int main(int argc, char **argv) {
ModelCheckBaseMT *mcl;
if (!strcmp(argv[1], "otfL"))
mcl = new ModelCheckLace(Rnewnet, nb_th);
- else
+ else if (!strcmp(argv[1], "otfP"))
mcl = new ModelCheckerTh(Rnewnet, nb_th);
+ else
+ mcl = new ModelCheckerThV2(Rnewnet, nb_th);
mcl->loadNet();
auto k = std::make_shared<SogKripkeTh>(d, mcl, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP());
cout << "Performing on the fly Modelchecking" << endl;
diff --git a/src/stacksafe.cpp b/src/stacksafe.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..de7f260f0ef86460ca808ac1f0e59367fd703f3f
--- /dev/null
+++ b/src/stacksafe.cpp
@@ -0,0 +1,64 @@
+/*
+ * Copyright 2020 chiheb <email>
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+#include "stacksafe.h"
+
+template<typename T>
+StackSafe<T>::StackSafe() {}
+
+template<typename T>
+StackSafe<T>::StackSafe ( const StackSafe& other)
+{
+ std::scoped_lock 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 );
+ m_data.push ( std::move ( new_value ) );
+}
+template<typename T>
+std::shared_ptr<T> StackSafe<T>::pop()
+{
+ std::scoped_lock 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();
+ return res;
+}
+template<typename T>
+void StackSafe<T>::pop(T& value)
+{
+ std::scoped_lock lock(m_mutex);
+ if(m_data.empty()) throw empty_stack();
+ value=m_data.top();
+ m_data.pop();
+}
+
+template<typename T>
+bool StackSafe<T>::empty() const
+{
+ std::scoped_lock lock(m_mutex);
+ return m_data.empty();
+}
+
+
+ template class StackSafe<Pair>;
+
+
+
+
diff --git a/src/stacksafe.h b/src/stacksafe.h
new file mode 100644
index 0000000000000000000000000000000000000000..af33910ec32b554ffb4e7b048a53562c5e6e1af8
--- /dev/null
+++ b/src/stacksafe.h
@@ -0,0 +1,49 @@
+/*
+ * Copyright 2020 chiheb <email>
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+#ifndef STACKSAFE_H
+#define STACKSAFE_H
+#include <mutex>
+/**
+ * @todo A thread safe stack
+ */
+#include "LDDState.h"
+#include <exception>
+#include <memory>
+#include <stack>
+#include <exception>
+typedef pair<LDDState *, MDD> couple;
+typedef pair<couple, Set> Pair;
+struct empty_stack: std::exception {
+ ~empty_stack() {};
+ const char* what() const noexcept {return "heloo";}
+
+ };
+template<typename T> class StackSafe {
+ private:
+ std::stack<T> m_data;
+ mutable std::mutex m_mutex;
+ public:
+ explicit StackSafe();
+ ~StackSafe() {};
+ StackSafe ( const StackSafe& other);
+ StackSafe& operator= ( const StackSafe& ) = delete;
+ void push ( T new_value );
+ std::shared_ptr<T> pop();
+ void pop ( T& value );
+ bool empty() const;
+ };
+#endif // STACKSAFE_H