From 41e36c9a20c9ee9788ed9737b2cf6fd2ef74cce7 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Thu, 6 Jun 2019 00:23:35 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/ModelCheckerTh.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20?=
=?UTF-8?q?=20=20=20=20=20src/ModelCheckerTh.h=20=09modifi=C3=A9=C2=A0:=20?=
=?UTF-8?q?=20=20=20=20=20=20=20=20src/main.cpp?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/ModelCheckerTh.cpp | 47 +++++++++++++++++-------------------------
src/ModelCheckerTh.h | 10 ++++-----
src/main.cpp | 21 +------------------
3 files changed, 25 insertions(+), 53 deletions(-)
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index 7e76293..bcffda8 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -36,22 +36,14 @@ ModelCheckerTh::ModelCheckerTh(const NewNet &R, int BOUND,int nbThread)
m_transitionName=R.transitionName;
m_placeName=R.m_placePosName;
- cout<<"Toutes les Transitions:"<<endl;
+ /* cout<<"Toutes les Transitions:"<<endl;
map<string,int>::iterator it2=m_transitionName.begin();
for (; it2!=m_transitionName.end(); it2++)
{
cout<<(*it2).first<<" : "<<(*it2).second<<endl;
- }
-
+ }*/
- cout<<"Transitions observables :"<<endl;
- Set::iterator it=m_observable.begin();
- for (; it!=m_observable.end(); it++)
- {
- cout<<*it<<" ";
- }
- cout<<endl;
InterfaceTrans=R.InterfaceTrans;
m_nbPlaces=R.places.size();
cout<<"Nombre de places : "<<m_nbPlaces<<endl;
@@ -65,10 +57,6 @@ ModelCheckerTh::ModelCheckerTh(const NewNet &R, int BOUND,int nbThread)
m_initalMarking=lddmc_cube(liste_marques,R.places.size());
-
-
-
-
uint32_t *prec = new uint32_t[m_nbPlaces];
uint32_t *postc= new uint32_t [m_nbPlaces];
// Transition relation
@@ -132,7 +120,6 @@ LDDState * ModelCheckerTh::buildInitialMetaState()
{
ComputeTh_Succ();
LDDState *c=new LDDState;
- cout<<"Initial marking : "<<m_initalMarking<<endl;
MDD initial_meta_state=Accessible_epsilon(m_initalMarking);
ldd_refs_push(initial_meta_state);
c->m_lddstate=initial_meta_state;
@@ -171,11 +158,8 @@ void * ModelCheckerTh::Compute_successors()
pthread_mutex_lock(&m_mutex);
id_thread=m_id_thread++;
pthread_mutex_unlock(&m_mutex);
-
LDDState* reached_class=nullptr;
- // size_t max_meta_state_size;
- // int min_charge;
- cout<<"Thread id : "<<id_thread<<endl;
+
do
{
pthread_barrier_wait(&m_barrier_threads);
@@ -211,8 +195,7 @@ void * ModelCheckerTh::Compute_successors()
}
pthread_barrier_wait(&m_barrier_builder);
}
- while (1);
-
+ while (!m_finish);
}
@@ -233,15 +216,13 @@ void ModelCheckerTh::ComputeTh_Succ()
m_id_thread=0;
pthread_mutex_init(&m_mutex, NULL);
- pthread_mutex_init(&m_gc_mutex,NULL);
+ //pthread_mutex_init(&m_gc_mutex,NULL);
pthread_mutex_init(&m_graph_mutex,NULL);
- pthread_mutex_init(&m_supervise_gc_mutex,NULL);
- m_gc=0;
+ //pthread_mutex_init(&m_supervise_gc_mutex,NULL);
+ pthread_barrier_init(&m_barrier_threads, NULL, m_nb_thread+1);
+ pthread_barrier_init(&m_barrier_builder, NULL, m_nb_thread+1);
- pthread_barrier_init(&m_barrier_threads, NULL, m_nb_thread);
- pthread_barrier_init(&m_barrier_builder, NULL, m_nb_thread);
-
- for (int i=0; i<m_nb_thread-1; i++)
+ for (int i=0; i<m_nb_thread; i++)
{
if ((rc = pthread_create(&m_list_thread[i], NULL,threadHandler,this)))
{
@@ -256,3 +237,13 @@ void ModelCheckerTh::ComputeTh_Succ()
}
+ModelCheckerTh::~ModelCheckerTh() {
+ m_finish=true;
+ pthread_barrier_wait(&m_barrier_threads);
+ pthread_barrier_wait(&m_barrier_builder);
+ for (int i = 0; i < m_nb_thread-1; i++)
+ {
+ pthread_join(m_list_thread[i], NULL);
+ }
+ cout<<"Destructor "<<endl;
+}
diff --git a/src/ModelCheckerTh.h b/src/ModelCheckerTh.h
index e92aea8..b271d6c 100644
--- a/src/ModelCheckerTh.h
+++ b/src/ModelCheckerTh.h
@@ -8,6 +8,7 @@ class ModelCheckerTh : public CommonSOG
{
public:
ModelCheckerTh(const NewNet &R, int BOUND,int nbThread);
+ ~ModelCheckerTh();
LDDState * buildInitialMetaState();
string getTransition(int pos);
string getPlace(int pos);
@@ -18,17 +19,16 @@ public:
private:
int m_nb_thread;
MDD m_initalMarking;
- int m_min_charge;
pile_t m_st[128];
- int m_charge[128];
int m_id_thread;
pthread_mutex_t m_mutex;
pthread_mutex_t m_graph_mutex;
- pthread_mutex_t m_gc_mutex;
- pthread_mutex_t m_supervise_gc_mutex;
+ //pthread_mutex_t m_gc_mutex;
+ //pthread_mutex_t m_supervise_gc_mutex;
pthread_barrier_t m_barrier_threads,m_barrier_builder;
- unsigned int m_gc;
+ //unsigned int m_gc;
+ bool m_finish=false;
pthread_mutex_t m_mutex_stack[128];
pthread_t m_list_thread[128];
diff --git a/src/main.cpp b/src/main.cpp
index e1b435a..9c41fdb 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -204,28 +204,8 @@ int main(int argc, char** argv)
}
// Initialize SOG builder
ModelCheckerTh* mcl=new ModelCheckerTh(R,bound,nb_th);
- cout<<"Created"<<endl;
- /********************************************************************/
- spot::twa_graph_ptr kk =
- spot::make_twa_graph(std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()),
- spot::twa::prop_set::all(), true);
- cout<<"SOG translated to SPOT succeeded.."<<endl;
- cout<<"Want to save the graph in a dot file ?";
- cin>>c;
- if (c=='y')
- {
- fstream file;
-
- string st(argv[3]);
- st+=".dot";
- file.open(st.c_str(),fstream::out);
- spot::print_dot(file, kk,"ka");
- file.close();
- }
-
- /********************************************************************/
auto k =
@@ -259,6 +239,7 @@ int main(int argc, char** argv)
}
else
std::cout << "formula is verified\n";
+ delete mcl;
}
--
GitLab