diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp
index 8200ca6ca70812e98c740bb8eb981076c3b217c2..0bdc5abef6cb5e698d16b626247471ea3cce8b68 100644
--- a/src/CommonSOG.cpp
+++ b/src/CommonSOG.cpp
@@ -12,136 +12,125 @@ CommonSOG::~CommonSOG()
//dtor
}
-LDDGraph *CommonSOG::getGraph() const {
+LDDGraph *CommonSOG::getGraph() const
+{
return m_graph;
}
-MDD CommonSOG::Accessible_epsilon(MDD From)
+MDD CommonSOG::Accessible_epsilon ( MDD From )
{
MDD M1;
MDD M2=From;
- do
- {
+ do {
M1=M2;
- for(Set::const_iterator i=m_nonObservable.begin(); !(i==m_nonObservable.end()); i++)
- {
+ for ( Set::const_iterator i=m_nonObservable.begin(); ! ( i==m_nonObservable.end() ); i++ ) {
- MDD succ= lddmc_firing_mono(M2,m_tb_relation[(*i)].getMinus(),m_tb_relation[(*i)].getPlus());
- M2=lddmc_union_mono(M2,succ);
+ MDD succ= lddmc_firing_mono ( M2,m_tb_relation[ ( *i )].getMinus(),m_tb_relation[ ( *i )].getPlus() );
+ M2=lddmc_union_mono ( M2,succ );
//M2=succ|M2;
}
- }
- while(M1!=M2);
+ } while ( M1!=M2 );
return M2;
}
// Return the set of firable observable transitions from an agregate
-Set CommonSOG::firable_obs(MDD State)
+Set CommonSOG::firable_obs ( MDD State )
{
Set res;
- for(Set::const_iterator i=m_observable.begin(); !(i==m_observable.end()); i++)
- {
+ for ( Set::const_iterator i=m_observable.begin(); ! ( i==m_observable.end() ); i++ ) {
//cout<<"firable..."<<endl;
- MDD succ = lddmc_firing_mono(State,m_tb_relation[(*i)].getMinus(),m_tb_relation[(*i)].getPlus());
- if(succ!=lddmc_false)
- {
- res.insert(*i);
+ MDD succ = lddmc_firing_mono ( State,m_tb_relation[ ( *i )].getMinus(),m_tb_relation[ ( *i )].getPlus() );
+ if ( succ!=lddmc_false ) {
+ res.insert ( *i );
}
}
return res;
}
-MDD CommonSOG::get_successor(MDD From,int t)
+MDD CommonSOG::get_successor ( MDD From,int t )
{
- return lddmc_firing_mono(From,m_tb_relation[(t)].getMinus(),m_tb_relation[(t)].getPlus());
+ return lddmc_firing_mono ( From,m_tb_relation[ ( t )].getMinus(),m_tb_relation[ ( t )].getPlus() );
}
-MDD CommonSOG::ImageForward(MDD From)
+MDD CommonSOG::ImageForward ( MDD From )
{
MDD Res=lddmc_false;
- for(Set::const_iterator i=m_nonObservable.begin(); !(i==m_nonObservable.end()); i++)
- {
- MDD succ= lddmc_firing_mono(From,m_tb_relation[(*i)].getMinus(),m_tb_relation[(*i)].getPlus());
- Res=lddmc_union_mono(Res,succ);
+ for ( Set::const_iterator i=m_nonObservable.begin(); ! ( i==m_nonObservable.end() ); i++ ) {
+ MDD succ= lddmc_firing_mono ( From,m_tb_relation[ ( *i )].getMinus(),m_tb_relation[ ( *i )].getPlus() );
+ Res=lddmc_union_mono ( Res,succ );
}
return Res;
}
/*----------------------------------------------CanonizeR()------------------------------------*/
-MDD CommonSOG::Canonize(MDD s,unsigned int level)
+MDD CommonSOG::Canonize ( MDD s,unsigned int level )
{
- if (level>m_nbPlaces || s==lddmc_false) return lddmc_false;
- if(isSingleMDD(s)) return s;
+ if ( level>m_nbPlaces || s==lddmc_false ) {
+ return lddmc_false;
+ }
+ if ( isSingleMDD ( s ) ) {
+ return s;
+ }
MDD s0=lddmc_false,s1=lddmc_false;
bool res=false;
- do
- {
- if (get_mddnbr(s,level)>1)
- {
- s0=ldd_divide_rec(s,level);
- s1=ldd_minus(s,s0);
+ do {
+ if ( get_mddnbr ( s,level ) >1 ) {
+ s0=ldd_divide_rec ( s,level );
+ s1=ldd_minus ( s,s0 );
res=true;
- }
- else
+ } else {
level++;
- }
- while(level<m_nbPlaces && !res);
+ }
+ } while ( level<m_nbPlaces && !res );
- if (s0==lddmc_false && s1==lddmc_false)
+ if ( s0==lddmc_false && s1==lddmc_false ) {
return lddmc_false;
+ }
// if (level==nbPlaces) return lddmc_false;
MDD Front,Reach;
- if (s0!=lddmc_false && s1!=lddmc_false)
- {
+ if ( s0!=lddmc_false && s1!=lddmc_false ) {
Front=s1;
Reach=s1;
- do
- {
+ do {
// cout<<"premiere boucle interne \n";
- Front=ldd_minus(ImageForward(Front),Reach);
- Reach = lddmc_union_mono(Reach,Front);
- s0 = ldd_minus(s0,Front);
- }
- while((Front!=lddmc_false)&&(s0!=lddmc_false));
+ Front=ldd_minus ( ImageForward ( Front ),Reach );
+ Reach = lddmc_union_mono ( Reach,Front );
+ s0 = ldd_minus ( s0,Front );
+ } while ( ( Front!=lddmc_false ) && ( s0!=lddmc_false ) );
}
- if((s0!=lddmc_false)&&(s1!=lddmc_false))
- {
+ if ( ( s0!=lddmc_false ) && ( s1!=lddmc_false ) ) {
Front=s0;
Reach = s0;
- do
- {
+ do {
// cout<<"deuxieme boucle interne \n";
- Front=ldd_minus(ImageForward(Front),Reach);
- Reach = lddmc_union_mono(Reach,Front);
- s1 = ldd_minus(s1,Front);
- }
- while( Front!=lddmc_false && s1!=lddmc_false );
+ Front=ldd_minus ( ImageForward ( Front ),Reach );
+ Reach = lddmc_union_mono ( Reach,Front );
+ s1 = ldd_minus ( s1,Front );
+ } while ( Front!=lddmc_false && s1!=lddmc_false );
}
MDD Repr=lddmc_false;
- if (isSingleMDD(s0))
- {
+ if ( isSingleMDD ( s0 ) ) {
Repr=s0;
- }
- else
- {
+ } else {
- Repr=Canonize(s0,level);
+ Repr=Canonize ( s0,level );
}
- if (isSingleMDD(s1))
- Repr=lddmc_union_mono(Repr,s1);
- else
- Repr=lddmc_union_mono(Repr,Canonize(s1,level));
+ if ( isSingleMDD ( s1 ) ) {
+ Repr=lddmc_union_mono ( Repr,s1 );
+ } else {
+ Repr=lddmc_union_mono ( Repr,Canonize ( s1,level ) );
+ }
return Repr;
@@ -149,81 +138,85 @@ MDD CommonSOG::Canonize(MDD s,unsigned int level)
}
-void CommonSOG::printhandler(ostream &o, int var)
+void CommonSOG::printhandler ( ostream &o, int var )
{
- o << (*_places)[var/2].name;
- if (var%2)
+ o << ( *_places ) [var/2].name;
+ if ( var%2 ) {
o << "_p";
+ }
}
-vector<TransSylvan>* CommonSOG::getTBRelation() {
+vector<TransSylvan>* CommonSOG::getTBRelation()
+{
return &m_tb_relation;
}
-Set * CommonSOG::getNonObservable() {
+Set * CommonSOG::getNonObservable()
+{
return &m_nonObservable;
}
/*********Returns the count of places******************************************/
-unsigned int CommonSOG::getPlacesCount() {
+unsigned int CommonSOG::getPlacesCount()
+{
return m_nbPlaces;
}
/**** Detect divergence in an agregate ****/
-bool CommonSOG::Set_Div(MDD &M) const
+bool CommonSOG::Set_Div ( MDD &M ) const
{
-
- if (m_nonObservable.empty())
- return false;
- Set::const_iterator i;
- MDD Reached,From;
- //cout<<"Ici detect divergence \n";
- Reached=lddmc_false;
+
+ if ( m_nonObservable.empty() ) {
+ return false;
+ }
+ Set::const_iterator i;
+ MDD Reached,From;
+ //cout<<"Ici detect divergence \n";
+ Reached=lddmc_false;
From=M;
- do
- {
-
- for(i=m_nonObservable.begin();!(i==m_nonObservable.end());i++)
- {
-
- MDD To= lddmc_firing_mono(From,m_tb_relation[(*i)].getMinus(),m_tb_relation[(*i)].getPlus());
- Reached=lddmc_union_mono(Reached,To);
- //Reached=To;
- }
-
- if(Reached==From) return true;
+ do {
+
+ for ( i=m_nonObservable.begin(); ! ( i==m_nonObservable.end() ); i++ ) {
+
+ MDD To= lddmc_firing_mono ( From,m_tb_relation[ ( *i )].getMinus(),m_tb_relation[ ( *i )].getPlus() );
+ Reached=lddmc_union_mono ( Reached,To );
+ //Reached=To;
+ }
+
+ if ( Reached==From ) {
+ return true;
+ }
From=Reached;
Reached=lddmc_false;
- } while(Reached!=lddmc_false && Reached != lddmc_true);
-
- return false;
+ } while ( Reached!=lddmc_false && Reached != lddmc_true );
+
+ return false;
}
/**** Detetc deadlocks ****/
-bool CommonSOG::Set_Bloc(MDD &M) const
+bool CommonSOG::Set_Bloc ( MDD &M ) const
{
- MDD cur=lddmc_true;
- for(vector<TransSylvan>::const_iterator i = m_tb_relation.begin(); i!=m_tb_relation.end();i++)
- {
+ MDD cur=lddmc_true;
+ for ( vector<TransSylvan>::const_iterator i = m_tb_relation.begin(); i!=m_tb_relation.end(); i++ ) {
- cur=cur&(TransSylvan(*i).getMinus());
+ cur=cur& ( TransSylvan ( *i ).getMinus() );
- }
-return ((M&cur)!=lddmc_false);
- //BLOCAGE
+ }
+ return ( ( M&cur ) !=lddmc_false );
+ //BLOCAGE
}
-string CommonSOG::getTransition(int pos)
+string CommonSOG::getTransition ( int pos )
{
- return m_graph->getTransition(pos);
+ return m_graph->getTransition ( pos );
}
-string CommonSOG::getPlace(int pos)
+string CommonSOG::getPlace ( int pos )
{
- return m_graph->getPlace(pos);
+ return m_graph->getPlace ( pos );
}
static LDDGraph *CommonSOG::m_graph;
diff --git a/src/HybridKripke.cpp b/src/HybridKripke.cpp
index 55bb4ed8cb7501460b61a95718b816ffa043a932..e7eb9e37e9d443d6c1c7017e13157bdc6054037e 100644
--- a/src/HybridKripke.cpp
+++ b/src/HybridKripke.cpp
@@ -100,7 +100,6 @@ bdd HybridKripke::state_condition(const spot::state* s) const
spot::formula f=spot::formula::ap(name);
result&=!bdd_ithvar((dict_->var_map.find(f))->second);
}
-
return result;
}
diff --git a/src/MCHybridSOG.cpp b/src/MCHybridSOG.cpp
index ab2a151b4c9c0f34fcb1fa94665de846a45c9156..83c235be5cc7ea52273993026ae53d157ec56658 100644
--- a/src/MCHybridSOG.cpp
+++ b/src/MCHybridSOG.cpp
@@ -26,15 +26,15 @@
#define TAG_NOTCOMPLETED 20
using namespace sylvan;
using namespace std;
-MCHybridSOG::MCHybridSOG(const NewNet &R,MPI_Comm &comm_world,bool init)
+MCHybridSOG::MCHybridSOG ( const NewNet &R,MPI_Comm &comm_world,bool init )
{
m_comm_world=comm_world;
- lace_init(1, 0);
- lace_startup(0, NULL, NULL);
+ lace_init ( 1, 0 );
+ lace_startup ( 0, NULL, NULL );
// Simple Sylvan initialization, also initialize MDD support
- sylvan_set_limits(2LL<<31, 2, 1); // sylvan_set_limits(2LL<<31, 2, 1);
+ sylvan_set_limits ( 2LL<<31, 2, 1 ); // sylvan_set_limits(2LL<<31, 2, 1);
//sylvan_set_sizes(1LL<<27, 1LL<<31, 1LL<<20, 1LL<<22);
sylvan_init_package();
@@ -63,12 +63,11 @@ MCHybridSOG::MCHybridSOG(const NewNet &R,MPI_Comm &comm_world,bool init)
// place domain, place bvect, place initial marking and place name
uint32_t * liste_marques=new uint32_t[R.places.size()];
- for(i=0,it_places=R.places.begin(); it_places!=R.places.end(); i++,it_places++)
- {
+ for ( i=0,it_places=R.places.begin(); it_places!=R.places.end(); i++,it_places++ ) {
liste_marques[i] =it_places->marking;
}
- M0=lddmc_cube(liste_marques,R.places.size());
- ldd_refs_push(M0);
+ M0=lddmc_cube ( liste_marques,R.places.size() );
+ ldd_refs_push ( M0 );
delete []liste_marques;
// place names
@@ -79,36 +78,32 @@ MCHybridSOG::MCHybridSOG(const NewNet &R,MPI_Comm &comm_world,bool init)
uint32_t *postc= new uint32_t [m_nbPlaces];
// Transition relation
- for(vector<Transition>::const_iterator t=R.transitions.begin();
- t!=R.transitions.end(); t++)
- {
+ for ( vector<Transition>::const_iterator t=R.transitions.begin();
+ t!=R.transitions.end(); t++ ) {
// Initialisation
- for(i=0; i<m_nbPlaces; i++)
- {
+ 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);
+ 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;
-
+
}
// arcs post
- for(vector< pair<int,int> >::const_iterator it=t->post.begin(); it!=t->post.end(); it++)
- {
- adjacentPlace.insert(it->first);
+ 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;
}
- MDD _minus=lddmc_cube(prec,m_nbPlaces);
- ldd_refs_push(_minus);
+ 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));
+ MDD _plus=lddmc_cube ( postc,m_nbPlaces );
+ ldd_refs_push ( _plus );
+ m_tb_relation.push_back ( TransSylvan ( _minus,_plus ) );
}
//sylvan_gc_seq();
delete [] prec;
@@ -128,48 +123,44 @@ void *MCHybridSOG::doCompute()
int min_charge=1;
int id_thread;
- pthread_mutex_lock(&m_mutex);
+ pthread_mutex_lock ( &m_mutex );
id_thread=m_id_thread++;
- pthread_mutex_unlock(&m_mutex);
+ pthread_mutex_unlock ( &m_mutex );
unsigned char Identif[20];
m_Terminated=false;
-
+
/****************************************** initial state ********************************************/
- if (task_id==0 && id_thread==0)
- {
+ if ( task_id==0 && id_thread==0 ) {
string* chaine=new string();
LDDState *c=new LDDState;
- MDD Complete_meta_state=Accessible_epsilon(M0);
+ MDD Complete_meta_state=Accessible_epsilon ( M0 );
c->m_lddstate=Complete_meta_state;
- ldd_refs_push(Complete_meta_state);
- // MDD reduced_initialstate=Canonize(Complete_meta_state,0);
+ ldd_refs_push ( Complete_meta_state );
+ // MDD reduced_initialstate=Canonize(Complete_meta_state,0);
- convert_wholemdd_stringcpp(Complete_meta_state,*chaine);
- get_md5(*chaine,Identif);
+ convert_wholemdd_stringcpp ( Complete_meta_state,*chaine );
+ get_md5 ( *chaine,Identif );
//lddmc_getsha(Complete_meta_state, Identif);
- uint16_t destination=(uint16_t)(Identif[0]%n_tasks);
- c->setProcess(destination);
- if(destination==0)
- {
+ uint16_t destination= ( uint16_t ) ( Identif[0]%n_tasks );
+ c->setProcess ( destination );
+ if ( destination==0 ) {
m_nbmetastate++;
- Set fire=firable_obs(Complete_meta_state);
- m_st[1].push(Pair(couple(c,Complete_meta_state),fire));
- m_graph->setInitialState(c);
- m_graph->insert(c);
+ Set fire=firable_obs ( Complete_meta_state );
+ m_st[1].push ( Pair ( couple ( c,Complete_meta_state ),fire ) );
+ m_graph->setInitialState ( c );
+ m_graph->insert ( c );
m_charge[1]++;
- memcpy(c->m_SHA2,Identif,16);
- }
- else
- {
+ memcpy ( c->m_SHA2,Identif,16 );
+ } else {
MDD initialstate=Complete_meta_state;
//cout<<"Initial marking is sent"<<endl;
- m_graph->insertSHA(c);
- memcpy(c->m_SHA2,Identif,16);
- // MDD initialstate=Complete_meta_state;
+ m_graph->insertSHA ( c );
+ memcpy ( c->m_SHA2,Identif,16 );
+ // MDD initialstate=Complete_meta_state;
//pthread_spin_lock(&m_spin_md5);
//pthread_spin_unlock(&m_spin_md5);
@@ -177,321 +168,302 @@ void *MCHybridSOG::doCompute()
//pthread_spin_unlock(&m_spin_md5);
//#ifndef
// if (strcmp(red,'C')==0)
-
- initialstate=Canonize(Complete_meta_state,0);
-
+
+ initialstate=Canonize ( Complete_meta_state,0 );
+
//#endif // REDUCE
- convert_wholemdd_stringcpp(initialstate,*chaine);
+ convert_wholemdd_stringcpp ( initialstate,*chaine );
- pthread_mutex_lock(&m_spin_msg[0]);
- m_msg[0].push(MSG(chaine,destination));
- pthread_mutex_unlock(&m_spin_msg[0]);
+ pthread_mutex_lock ( &m_spin_msg[0] );
+ m_msg[0].push ( MSG ( chaine,destination ) );
+ pthread_mutex_unlock ( &m_spin_msg[0] );
delete c;
}
}
- while (m_Terminated==false)
- {
+ while ( m_Terminated==false ) {
/******************************* envoie et reception des aggregats ************************************/
- if (id_thread==0)
- {
+ if ( id_thread==0 ) {
- do
- {
+ do {
send_state_message();
read_message();
- if (m_waitingBuild) {
- bool res;
- size_t pos=m_graph->findSHAPos(m_id_md5,res);
- if (res) {
- m_waitingBuild=false;
- m_aggWaiting=m_graph->getLDDStateById(pos);
- m_waitingSucc=true;
- // cout<<"Get build..."<<endl;
- }
-
- }
- if (m_waitingSucc) {
-
- if (m_aggWaiting->isCompletedSucc()) {
- //cout<<"Get succ..."<<endl;
- m_waitingSucc=false;
- sendSuccToMC();
- }
- }
- if (m_waitingAgregate) {
- bool res=false;
- size_t pos=m_graph->findSHAPos(m_id_md5,res);
- //cout<<"Not found..."<<endl;
- if (res) {
- m_waitingAgregate=false;
- sendPropToMC(pos);
- }
- }
- }
- while (!m_Terminated);
+ if ( m_waitingBuild ) {
+ bool res;
+ size_t pos=m_graph->findSHAPos ( m_id_md5,res );
+ if ( res ) {
+ m_waitingBuild=false;
+ m_aggWaiting=m_graph->getLDDStateById ( pos );
+ m_waitingSucc=true;
+ // cout<<"Get build..."<<endl;
+ }
+
+ }
+ if ( m_waitingSucc ) {
+
+ if ( m_aggWaiting->isCompletedSucc() ) {
+ //cout<<"Get succ..."<<endl;
+ m_waitingSucc=false;
+ sendSuccToMC();
+ }
+ }
+ if ( m_waitingAgregate ) {
+ bool res=false;
+ size_t pos=m_graph->findSHAPos ( m_id_md5,res );
+ //cout<<"Not found..."<<endl;
+ if ( res ) {
+ m_waitingAgregate=false;
+ sendPropToMC ( pos );
+ }
+ }
+ } while ( !m_Terminated );
+
-
}
/******************************* Construction des aggregats ************************************/
- else
- {
+ else {
- if (!m_st[id_thread].empty() || !m_msg[id_thread].empty())
- {
- pthread_mutex_lock(&m_spin_working);
+ if ( !m_st[id_thread].empty() || !m_msg[id_thread].empty() ) {
+ pthread_mutex_lock ( &m_spin_working );
m_working++;
- pthread_mutex_unlock(&m_spin_working);
-
- if (id_thread>1)
- {
- pthread_mutex_lock(&m_supervise_gc_mutex);
- m_gc++;
- if (m_gc==1) pthread_mutex_lock(&m_gc_mutex);
- pthread_mutex_unlock(&m_supervise_gc_mutex);
+ pthread_mutex_unlock ( &m_spin_working );
+
+ if ( id_thread>1 ) {
+ pthread_mutex_lock ( &m_supervise_gc_mutex );
+ m_gc++;
+ if ( m_gc==1 ) {
+ pthread_mutex_lock ( &m_gc_mutex );
}
+ pthread_mutex_unlock ( &m_supervise_gc_mutex );
+ }
- if (!m_st[id_thread].empty())
- {
+ if ( !m_st[id_thread].empty() ) {
- Pair e;
- pthread_mutex_lock(&m_spin_stack[id_thread]);
- e=m_st[id_thread].top();
- m_st[id_thread].pop();
- pthread_mutex_unlock(&m_spin_stack[id_thread]);
- m_charge[id_thread]--;
+ Pair e;
+ pthread_mutex_lock ( &m_spin_stack[id_thread] );
+ e=m_st[id_thread].top();
+ m_st[id_thread].pop();
+ pthread_mutex_unlock ( &m_spin_stack[id_thread] );
+ m_charge[id_thread]--;
- LDDState *reached_class=NULL;
-
+ LDDState *reached_class=NULL;
- while(!e.second.empty())
- {
- /*#ifdef DEBUG_GC
- displayMDDTableInfo();
- #endif // DEBUG_GC*/
- int t = *(e.second.begin());
- e.second.erase(t);
- reached_class=new LDDState();
+ while ( !e.second.empty() ) {
+ /*#ifdef DEBUG_GC
+ displayMDDTableInfo();
+ #endif // DEBUG_GC*/
+ int t = * ( e.second.begin() );
+ e.second.erase ( t );
+ reached_class=new LDDState();
- MDD ldd_reachedclass=Accessible_epsilon(get_successor(e.first.second,t));
- ldd_refs_push(ldd_reachedclass);
+ MDD ldd_reachedclass=Accessible_epsilon ( get_successor ( e.first.second,t ) );
+ ldd_refs_push ( ldd_reachedclass );
- if (id_thread==1)
- if (isGCRequired())
- {
- pthread_mutex_lock(&m_gc_mutex);
+ if ( id_thread==1 )
+ if ( isGCRequired() ) {
+ pthread_mutex_lock ( &m_gc_mutex );
#ifdef DEBUG_GC
- displayMDDTableInfo();
+ displayMDDTableInfo();
#endif // DEBUG_GC
- sylvan_gc_seq();
+ sylvan_gc_seq();
#ifdef DEBUG_GC
- displayMDDTableInfo();
+ displayMDDTableInfo();
#endif // DEBUG_GC
- pthread_mutex_unlock(&m_gc_mutex);
- }
+ pthread_mutex_unlock ( &m_gc_mutex );
+ }
- //pthread_spin_unlock(&m_spin_md5);
+ //pthread_spin_unlock(&m_spin_md5);
- reached_class->m_lddstate=ldd_reachedclass;
+ reached_class->m_lddstate=ldd_reachedclass;
- //MDD Reduced=Canonize(ldd_reachedclass,0);
- // ldd_refs_push(Reduced);
+ //MDD Reduced=Canonize(ldd_reachedclass,0);
+ // ldd_refs_push(Reduced);
- //MDD Reduced=ldd_reachedclass;
- string* message_to_send1=new string();
- convert_wholemdd_stringcpp(ldd_reachedclass,*message_to_send1);
- get_md5(*message_to_send1,Identif);
+ //MDD Reduced=ldd_reachedclass;
+ string* message_to_send1=new string();
+ convert_wholemdd_stringcpp ( ldd_reachedclass,*message_to_send1 );
+ get_md5 ( *message_to_send1,Identif );
- //lddmc_getsha(ldd_reachedclass, Identif);
+ //lddmc_getsha(ldd_reachedclass, Identif);
- unsigned int destination=(unsigned int)(Identif[0]%n_tasks);
+ unsigned int destination= ( unsigned int ) ( Identif[0]%n_tasks );
- /**************** construction local ******/
- // cout<<"debut boucle pile process "<<task_id<< " thread "<< id_thread<<endl;
- reached_class->setProcess(destination);
- if(destination==task_id)
- {
- // cout << " construction local de l'aggregat " <<endl;
- pthread_mutex_lock(&m_graph_mutex);
- LDDState* pos=m_graph->find(reached_class);
- if(!pos)
- {
- reached_class->setDiv(Set_Div(ldd_reachedclass));
- reached_class->setDeadLock(Set_Bloc(ldd_reachedclass));
- m_graph->insert(reached_class);
- memcpy(reached_class->m_SHA2,Identif,16);
- pthread_mutex_unlock(&m_graph_mutex);
- m_graph->addArc();
- 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));
+ /**************** construction local ******/
+ // cout<<"debut boucle pile process "<<task_id<< " thread "<< id_thread<<endl;
+ reached_class->setProcess ( destination );
+ if ( destination==task_id ) {
+ // cout << " construction local de l'aggregat " <<endl;
+ pthread_mutex_lock ( &m_graph_mutex );
+ LDDState* pos=m_graph->find ( reached_class );
+ if ( !pos ) {
+ reached_class->setDiv ( Set_Div ( ldd_reachedclass ) );
+ reached_class->setDeadLock ( Set_Bloc ( ldd_reachedclass ) );
+ m_graph->insert ( reached_class );
+ memcpy ( reached_class->m_SHA2,Identif,16 );
+ pthread_mutex_unlock ( &m_graph_mutex );
+ m_graph->addArc();
+ 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 ) );
- Set fire=firable_obs(ldd_reachedclass);
- min_charge=minCharge();
+ Set fire=firable_obs ( ldd_reachedclass );
+ min_charge=minCharge();
- pthread_mutex_lock(&m_spin_stack[min_charge]);
- m_st[min_charge].push(Pair(couple(reached_class,ldd_reachedclass),fire));
- pthread_mutex_unlock(&m_spin_stack[min_charge]);
- //pthread_mutex_lock(&m_spin_charge);
- m_charge[min_charge]++;
- //pthread_mutex_unlock(&m_spin_charge);
- // cout<<" I'm local destination "<<task_id<< " thread "<< id_thread<< " msg "<< msg<<endl;
- }
- else
- {
- pthread_mutex_unlock(&m_graph_mutex);
- m_graph->addArc();
- 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;
+ pthread_mutex_lock ( &m_spin_stack[min_charge] );
+ m_st[min_charge].push ( Pair ( couple ( reached_class,ldd_reachedclass ),fire ) );
+ pthread_mutex_unlock ( &m_spin_stack[min_charge] );
+ //pthread_mutex_lock(&m_spin_charge);
+ m_charge[min_charge]++;
+ //pthread_mutex_unlock(&m_spin_charge);
+ // cout<<" I'm local destination "<<task_id<< " thread "<< id_thread<< " msg "<< msg<<endl;
+ } else {
+ pthread_mutex_unlock ( &m_graph_mutex );
+ m_graph->addArc();
+ 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;
- }
+ }
- }
- /**************** construction externe ******/
- else // send to another process
- {
- pthread_mutex_lock(&m_graph_mutex);
- LDDState* posV=m_graph->findSHA(Identif);
- if(!posV)
- {
-
- MDD reached=ldd_reachedclass;
-
- m_graph->insertSHA(reached_class);
- memcpy(reached_class->m_SHA2,Identif,16);
- pthread_mutex_unlock(&m_graph_mutex);
- #ifndef REDUCE
- reached=Canonize(ldd_reachedclass,0);
- ldd_refs_push(ldd_reachedclass);
- #endif
- //MDD Reduced=ldd_reachedclass;
- string* message_to_send2=new string();
- convert_wholemdd_stringcpp(reached,*message_to_send2);
+ }
+ /**************** construction externe ******/
+ else { // send to another process
+ pthread_mutex_lock ( &m_graph_mutex );
+ LDDState* posV=m_graph->findSHA ( Identif );
+ if ( !posV ) {
+
+ MDD reached=ldd_reachedclass;
+
+ m_graph->insertSHA ( reached_class );
+ memcpy ( reached_class->m_SHA2,Identif,16 );
+ pthread_mutex_unlock ( &m_graph_mutex );
+#ifndef REDUCE
+ reached=Canonize ( ldd_reachedclass,0 );
+ ldd_refs_push ( ldd_reachedclass );
+#endif
+ //MDD Reduced=ldd_reachedclass;
+ string* message_to_send2=new string();
+ convert_wholemdd_stringcpp ( reached,*message_to_send2 );
// get_md5(*message_to_send2,Identif);
- m_graph->addArc();
- 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));
+ m_graph->addArc();
+ 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_spin_msg[0]);
- m_msg[0].push(MSG(message_to_send2,destination));
- pthread_mutex_unlock(&m_spin_msg[0]);
+ pthread_mutex_lock ( &m_spin_msg[0] );
+ m_msg[0].push ( MSG ( message_to_send2,destination ) );
+ pthread_mutex_unlock ( &m_spin_msg[0] );
- }
- else
- {
- pthread_mutex_unlock(&m_graph_mutex);
- m_graph->addArc();
- e.first.first->Successors.insert(e.first.first->Successors.begin(),LDDEdge(posV,t));
- posV->Predecessors.insert(posV->Predecessors.begin(),LDDEdge(e.first.first,t));
- delete reached_class;
- // read_state_message();
+ } else {
+ pthread_mutex_unlock ( &m_graph_mutex );
+ m_graph->addArc();
+ e.first.first->Successors.insert ( e.first.first->Successors.begin(),LDDEdge ( posV,t ) );
+ posV->Predecessors.insert ( posV->Predecessors.begin(),LDDEdge ( e.first.first,t ) );
+ delete reached_class;
+ // read_state_message();
- }
+ }
- }
+ }
- }
- e.first.first->setCompletedSucc();
-
+ }
+ e.first.first->setCompletedSucc();
- }
+ }
- /******************************* Construction des aggregats � partir de pile de messages ************************************/
-
- if (!m_msg[id_thread].empty())
- {
-
- MSG popped_msg;
- pthread_mutex_lock(&m_spin_msg[id_thread]);
- popped_msg=m_msg[id_thread].top();
- m_msg[id_thread].pop();
- pthread_mutex_unlock(&m_spin_msg[id_thread]);
-
- m_charge[id_thread]--;
- MDD receivedLDD=decodage_message(popped_msg.first->c_str());
- delete popped_msg.first;
- // ldd_refs_push(receivedLDD);
-
- LDDState* Agregate=new LDDState();
- MDD MState=Accessible_epsilon(receivedLDD);
-
- //cout<<"executed3..."<<endl;
- Agregate->m_lddstate=MState;
- pthread_mutex_lock(&m_graph_mutex);
- if (!m_graph->find(Agregate))
- {
- ldd_refs_push(MState);
- Agregate->setDiv(Set_Div(MState));
- Agregate->setDeadLock(Set_Bloc(MState));
- Agregate->setProcess(task_id);
- m_graph->insert(Agregate);
- string* chaine=new string();
- convert_wholemdd_stringcpp(MState,*chaine);
- get_md5(*chaine,Identif);
- delete chaine;
- memcpy(Agregate->m_SHA2,Identif,16);
- pthread_mutex_unlock(&m_graph_mutex);
- Set fire=firable_obs(MState);
- min_charge=minCharge();
- pthread_mutex_lock(&m_spin_stack[min_charge]);
- m_st[min_charge].push(Pair(couple(Agregate,MState),fire));
- pthread_mutex_unlock(&m_spin_stack[min_charge]);
- m_charge[min_charge]++;
- }
- else
- {
- pthread_mutex_unlock(&m_graph_mutex);
- delete Agregate;
- }
+ /******************************* Construction des aggregats � partir de pile de messages ************************************/
+
+ if ( !m_msg[id_thread].empty() ) {
+
+ MSG popped_msg;
+ pthread_mutex_lock ( &m_spin_msg[id_thread] );
+ popped_msg=m_msg[id_thread].top();
+ m_msg[id_thread].pop();
+ pthread_mutex_unlock ( &m_spin_msg[id_thread] );
+
+ m_charge[id_thread]--;
+ MDD receivedLDD=decodage_message ( popped_msg.first->c_str() );
+ delete popped_msg.first;
+ // ldd_refs_push(receivedLDD);
+
+ LDDState* Agregate=new LDDState();
+ MDD MState=Accessible_epsilon ( receivedLDD );
+
+ //cout<<"executed3..."<<endl;
+ Agregate->m_lddstate=MState;
+ pthread_mutex_lock ( &m_graph_mutex );
+ if ( !m_graph->find ( Agregate ) ) {
+ ldd_refs_push ( MState );
+ Agregate->setDiv ( Set_Div ( MState ) );
+ Agregate->setDeadLock ( Set_Bloc ( MState ) );
+ Agregate->setProcess ( task_id );
+ m_graph->insert ( Agregate );
+ string* chaine=new string();
+ convert_wholemdd_stringcpp ( MState,*chaine );
+ get_md5 ( *chaine,Identif );
+ delete chaine;
+ memcpy ( Agregate->m_SHA2,Identif,16 );
+ pthread_mutex_unlock ( &m_graph_mutex );
+ Set fire=firable_obs ( MState );
+ min_charge=minCharge();
+ pthread_mutex_lock ( &m_spin_stack[min_charge] );
+ m_st[min_charge].push ( Pair ( couple ( Agregate,MState ),fire ) );
+ pthread_mutex_unlock ( &m_spin_stack[min_charge] );
+ m_charge[min_charge]++;
}
- if (id_thread>1)
- {
- pthread_mutex_lock(&m_supervise_gc_mutex);
- m_gc--;
- if (m_gc==0) pthread_mutex_unlock(&m_gc_mutex);
- pthread_mutex_unlock(&m_supervise_gc_mutex);
+ else {
+ pthread_mutex_unlock ( &m_graph_mutex );
+ delete Agregate;
+ }
+ }
+
+ if ( id_thread>1 ) {
+ pthread_mutex_lock ( &m_supervise_gc_mutex );
+ m_gc--;
+ if ( m_gc==0 ) {
+ pthread_mutex_unlock ( &m_gc_mutex );
}
- pthread_mutex_lock(&m_spin_working);
+ pthread_mutex_unlock ( &m_supervise_gc_mutex );
+ }
+ pthread_mutex_lock ( &m_spin_working );
m_working--;
- pthread_mutex_unlock(&m_spin_working);
+ pthread_mutex_unlock ( &m_spin_working );
- } // End while (m_msg[id_thread].size()>0 || m_st[id_thread].size()>0);
+ } // End while (m_msg[id_thread].size()>0 || m_st[id_thread].size()>0);
- // }
+ // }
} /// End else
//cout<<"Working process "<<task_id<<" leaved...thread "<<id_thread<<endl;
-
+
}
@@ -503,78 +475,78 @@ void *MCHybridSOG::doCompute()
void MCHybridSOG::read_message()
{
int flag=0;
- MPI_Iprobe(MPI_ANY_SOURCE,MPI_ANY_TAG,MPI_COMM_WORLD,&flag,&m_status); // exist a msg to receiv?
- while (flag!=0)
- {
- //cout<<"message tag :"<<m_status.MPI_TAG<<" by task "<<task_id<<endl;
- if (m_status.MPI_TAG==TAG_ASK_STATE) {
+ MPI_Iprobe ( MPI_ANY_SOURCE,MPI_ANY_TAG,MPI_COMM_WORLD,&flag,&m_status ); // exist a msg to receiv?
+ while ( flag!=0 ) {
+ //cout<<"message tag :"<<m_status.MPI_TAG<<" by task "<<task_id<<endl;
+ if ( m_status.MPI_TAG==TAG_ASK_STATE ) {
//cout<<"TAG ASKSTATE received by task "<<task_id<<" from "<<m_status.MPI_SOURCE<<endl;
char mess[17];
- MPI_Recv(mess,16,MPI_BYTE,m_status.MPI_SOURCE,m_status.MPI_TAG,MPI_COMM_WORLD,&m_status);
- bool res;m_waitingAgregate=false;
- size_t pos=m_graph->findSHAPos(mess,res);
- if (!res) {
+ MPI_Recv ( mess,16,MPI_BYTE,m_status.MPI_SOURCE,m_status.MPI_TAG,MPI_COMM_WORLD,&m_status );
+ bool res;
+ m_waitingAgregate=false;
+ size_t pos=m_graph->findSHAPos ( mess,res );
+ if ( !res ) {
//cout<<"Not found"<<endl;
m_waitingAgregate=true;
- memcpy(m_id_md5,mess,16);
+ memcpy ( m_id_md5,mess,16 );
+ } else {
+ sendPropToMC ( pos );
}
- else sendPropToMC(pos);
-
-
- }
- else if (m_status.MPI_TAG==TAG_ASK_SUCC) {
-
- char mess[17];
- MPI_Recv(mess,16,MPI_BYTE,m_status.MPI_SOURCE,m_status.MPI_TAG,MPI_COMM_WORLD,&m_status);
- m_waitingBuild=false;m_waitingSucc=false;
+
+
+ } else if ( m_status.MPI_TAG==TAG_ASK_SUCC ) {
+
+ char mess[17];
+ MPI_Recv ( mess,16,MPI_BYTE,m_status.MPI_SOURCE,m_status.MPI_TAG,MPI_COMM_WORLD,&m_status );
+ m_waitingBuild=false;
+ m_waitingSucc=false;
bool res;
//cout<<"Before "<<res<<endl;
- size_t pos=m_graph->findSHAPos(mess,res);
+ size_t pos=m_graph->findSHAPos ( mess,res );
//cout<<"After "<<res<<endl;
- if (res) {
- LDDState *aggregate=m_graph->getLDDStateById(pos);
+ if ( res ) {
+ LDDState *aggregate=m_graph->getLDDStateById ( pos );
m_aggWaiting=aggregate;
- if (aggregate->isCompletedSucc()) sendSuccToMC();
- else {
- m_waitingSucc=true;
+ if ( aggregate->isCompletedSucc() ) {
+ sendSuccToMC();
+ } else {
+ m_waitingSucc=true;
//cout<<"Waiting for succ..."<<endl;
}
- }
- else {
+ } else {
m_waitingBuild=true;
//cout<<"Waiting for build..."<<endl;
- memcpy(m_id_md5,mess,16);
+ memcpy ( m_id_md5,mess,16 );
}
-
- }
- int v;
- switch (m_status.MPI_TAG)
- {
+
+ }
+ int v;
+ switch ( m_status.MPI_TAG ) {
case TAG_STATE:
//cout<<"=============================TAG STATE received by task "<<task_id<<endl;
read_state_message();
break;
- case TAG_FINISH:
- //cout<<"TAG FINISH received by task "<<task_id<<endl;
- MPI_Recv(&v, 1, MPI_INT, m_status.MPI_SOURCE, m_status.MPI_TAG, MPI_COMM_WORLD, &m_status);
+ case TAG_FINISH:
+ //cout<<"TAG FINISH received by task "<<task_id<<endl;
+ MPI_Recv ( &v, 1, MPI_INT, m_status.MPI_SOURCE, m_status.MPI_TAG, MPI_COMM_WORLD, &m_status );
m_Terminated=true;
break;
- case TAG_INITIAL:
- // cout<<"TAG INITIAL received by task "<<task_id<<endl;
- MPI_Recv(&v, 1, MPI_INT, m_status.MPI_SOURCE, m_status.MPI_TAG, MPI_COMM_WORLD, &m_status);
- LDDState *i_agregate=m_graph->getInitialState();
- char message[22];
- memcpy(message,i_agregate->getSHAValue(),16);
- uint16_t id_p=i_agregate->getProcess();
- memcpy(message+16,&id_p,2);
- MPI_Send(message,22,MPI_BYTE,m_status.MPI_SOURCE, TAG_ACK_INITIAL, MPI_COMM_WORLD);
- break;
- /*default: cout<<"unknown received "<<m_status.MPI_TAG<<" by task "<<task_id<<endl;
- //AbortTerm();
- //break; */
+ case TAG_INITIAL:
+ // cout<<"TAG INITIAL received by task "<<task_id<<endl;
+ MPI_Recv ( &v, 1, MPI_INT, m_status.MPI_SOURCE, m_status.MPI_TAG, MPI_COMM_WORLD, &m_status );
+ LDDState *i_agregate=m_graph->getInitialState();
+ char message[22];
+ memcpy ( message,i_agregate->getSHAValue(),16 );
+ uint16_t id_p=i_agregate->getProcess();
+ memcpy ( message+16,&id_p,2 );
+ MPI_Send ( message,22,MPI_BYTE,m_status.MPI_SOURCE, TAG_ACK_INITIAL, MPI_COMM_WORLD );
+ break;
+ /*default: cout<<"unknown received "<<m_status.MPI_TAG<<" by task "<<task_id<<endl;
+ //AbortTerm();
+ //break; */
}
-
- MPI_Iprobe(MPI_ANY_SOURCE,MPI_ANY_TAG,MPI_COMM_WORLD,&flag,&m_status);
+
+ MPI_Iprobe ( MPI_ANY_SOURCE,MPI_ANY_TAG,MPI_COMM_WORLD,&flag,&m_status );
}
}
@@ -586,38 +558,37 @@ void MCHybridSOG::read_state_message()
int min_charge;
/****************************************** debut reception state ********************************************/
int nbytes;
- MPI_Get_count(&m_status, MPI_CHAR, &nbytes);
+ MPI_Get_count ( &m_status, MPI_CHAR, &nbytes );
char inmsg[nbytes+1];
- MPI_Recv(inmsg, nbytes, MPI_CHAR,m_status.MPI_SOURCE,TAG_STATE,MPI_COMM_WORLD, &m_status);
+ MPI_Recv ( inmsg, nbytes, MPI_CHAR,m_status.MPI_SOURCE,TAG_STATE,MPI_COMM_WORLD, &m_status );
m_nbrecv++;
- string *msg_receiv =new string(inmsg,nbytes);
+ string *msg_receiv =new string ( inmsg,nbytes );
min_charge=minCharge();
m_charge[min_charge]++;
- pthread_mutex_lock(&m_spin_msg[min_charge]);
- m_msg[min_charge].push(MSG(msg_receiv,0));
- pthread_mutex_unlock(&m_spin_msg[min_charge]);
+ pthread_mutex_lock ( &m_spin_msg[min_charge] );
+ m_msg[min_charge].push ( MSG ( msg_receiv,0 ) );
+ pthread_mutex_unlock ( &m_spin_msg[min_charge] );
}
void MCHybridSOG::send_state_message()
{
- while (!m_msg[0].empty())
- {
- pthread_mutex_lock(&m_spin_msg[0]);
+ while ( !m_msg[0].empty() ) {
+ pthread_mutex_lock ( &m_spin_msg[0] );
MSG s=m_msg[0].top();
m_msg[0].pop();
- pthread_mutex_unlock(&m_spin_msg[0]);
+ pthread_mutex_unlock ( &m_spin_msg[0] );
unsigned int message_size;
message_size=s.first->size()+1;
int destination=s.second;
read_message();
- MPI_Send(s.first->c_str(), message_size, MPI_CHAR, destination, TAG_STATE, MPI_COMM_WORLD);
+ MPI_Send ( s.first->c_str(), message_size, MPI_CHAR, destination, TAG_STATE, MPI_COMM_WORLD );
m_nbsend++;
m_size_mess+=message_size;
delete s.first;
}
}
-void MCHybridSOG::computeDSOG(LDDGraph &g)
+void MCHybridSOG::computeDSOG ( LDDGraph &g )
{
m_graph=&g;
@@ -625,58 +596,54 @@ void MCHybridSOG::computeDSOG(LDDGraph &g)
// double t1=(double)clock() / (double)CLOCKS_PER_SEC;
//cout<<"process with id "<<task_id<<" / "<<n_tasks<<endl;
- MPI_Barrier(m_comm_world);
- // cout<<"After!!!!process with id "<<task_id<<endl;
- // int nb_th;
+ MPI_Barrier ( m_comm_world );
+ // cout<<"After!!!!process with id "<<task_id<<endl;
+ // int nb_th;
m_nb_thread=nb_th;
//cout<<"nb de thread"<<nb_th<<endl;
int rc;
m_id_thread=0;
m_nbrecv=0;
m_nbsend=0;
- for (int i=1; i<m_nb_thread; i++)
- {
+ for ( int i=1; i<m_nb_thread; i++ ) {
m_charge[i]=0;
}
//pthread_barrier_init(&m_barrier1, 0, m_nb_thread);
//pthread_barrier_init(&m_barrier2, 0, m_nb_thread);
- pthread_mutex_init(&m_mutex, NULL);
- pthread_mutex_init(&m_graph_mutex,NULL);
- pthread_mutex_init(&m_gc_mutex,NULL);
- pthread_mutex_init(&m_supervise_gc_mutex,NULL);
+ pthread_mutex_init ( &m_mutex, NULL );
+ pthread_mutex_init ( &m_graph_mutex,NULL );
+ pthread_mutex_init ( &m_gc_mutex,NULL );
+ pthread_mutex_init ( &m_supervise_gc_mutex,NULL );
m_gc=0;
- pthread_spin_init(&m_spin_md5,0);
- pthread_mutex_init(&m_spin_working,0);
+ pthread_spin_init ( &m_spin_md5,0 );
+ pthread_mutex_init ( &m_spin_working,0 );
m_working=0;
- for (int i=0; i<m_nb_thread; i++)
- {
- pthread_mutex_init(&m_spin_stack[i], 0);
- pthread_mutex_init(&m_spin_msg[i], 0);
+ for ( int i=0; i<m_nb_thread; i++ ) {
+ pthread_mutex_init ( &m_spin_stack[i], 0 );
+ pthread_mutex_init ( &m_spin_msg[i], 0 );
}
timespec start, finish;
- if (task_id==0)
- clock_gettime(CLOCK_REALTIME, &start);
+ if ( task_id==0 ) {
+ clock_gettime ( CLOCK_REALTIME, &start );
+ }
- for (int i=0; i<m_nb_thread-1; i++)
- {
- if ((rc = pthread_create(&m_list_thread[i], NULL,threadHandler,this)))
- {
+ for ( int i=0; i<m_nb_thread-1; i++ ) {
+ if ( ( rc = pthread_create ( &m_list_thread[i], NULL,threadHandler,this ) ) ) {
cout<<"error: pthread_create, rc: "<<rc<<endl;
}
}
doCompute();
- for (int i = 0; i < m_nb_thread-1; i++)
- {
- pthread_join(m_list_thread[i], NULL);
+ for ( int i = 0; i < m_nb_thread-1; i++ ) {
+ pthread_join ( m_list_thread[i], NULL );
}
@@ -687,16 +654,15 @@ void MCHybridSOG::computeDSOG(LDDGraph &g)
int nbarcs=g.m_nbArcs;
unsigned long total_size_mess=0;
- MPI_Reduce(&nbstate, &sum_nbStates, 1, MPI_INT, MPI_SUM, 0, m_comm_world);
- MPI_Reduce(&nbarcs, &sum_nbArcs, 1, MPI_INT, MPI_SUM, 0, m_comm_world);
- MPI_Reduce(&m_size_mess, &total_size_mess, 1, MPI_INT, MPI_SUM, 0, m_comm_world);
+ MPI_Reduce ( &nbstate, &sum_nbStates, 1, MPI_INT, MPI_SUM, 0, m_comm_world );
+ MPI_Reduce ( &nbarcs, &sum_nbArcs, 1, MPI_INT, MPI_SUM, 0, m_comm_world );
+ MPI_Reduce ( &m_size_mess, &total_size_mess, 1, MPI_INT, MPI_SUM, 0, m_comm_world );
- if(task_id==0)
- {
- clock_gettime(CLOCK_REALTIME, &finish);
+ if ( task_id==0 ) {
+ clock_gettime ( CLOCK_REALTIME, &finish );
- tps = (finish.tv_sec - start.tv_sec);
- tps += (finish.tv_nsec - start.tv_nsec) / 1000000000.0;
+ tps = ( finish.tv_sec - start.tv_sec );
+ tps += ( finish.tv_nsec - start.tv_nsec ) / 1000000000.0;
std::cout << " TIME OF CONSTRUCTION OF THE SOG "
<< tps
<< " seconds\n";
@@ -715,10 +681,8 @@ int MCHybridSOG::minCharge()
{
int pos=1;
int min_charge=m_charge[1];
- for (int i=1; i<m_nb_thread; i++)
- {
- if (m_charge[i]<min_charge)
- {
+ for ( int i=1; i<m_nb_thread; i++ ) {
+ if ( m_charge[i]<min_charge ) {
min_charge=m_charge[i];
pos=i;
}
@@ -737,34 +701,32 @@ MCHybridSOG::~MCHybridSOG()
/******************************************convert char ---> MDD ********************************************/
-MDD MCHybridSOG::decodage_message(const char *chaine)
+MDD MCHybridSOG::decodage_message ( const char *chaine )
{
MDD M=lddmc_false;
- unsigned int nb_marq=((unsigned char)chaine[1]-1);
- nb_marq=(nb_marq<<7) | ((unsigned char)chaine[0]>>1);
+ unsigned int nb_marq= ( ( unsigned char ) chaine[1]-1 );
+ nb_marq= ( nb_marq<<7 ) | ( ( unsigned char ) chaine[0]>>1 );
unsigned int index=2;
uint32_t list_marq[m_nbPlaces];
- for (unsigned int i=0; i<nb_marq; i++)
- {
- for (unsigned int j=0; j<m_nbPlaces; j++)
- {
- list_marq[j]=(uint32_t)((unsigned char)chaine[index]-1);
+ for ( unsigned int i=0; i<nb_marq; i++ ) {
+ for ( unsigned int j=0; j<m_nbPlaces; j++ ) {
+ list_marq[j]= ( uint32_t ) ( ( unsigned char ) chaine[index]-1 );
index++;
}
- MDD N=lddmc_cube(list_marq,m_nbPlaces);
- M=lddmc_union_mono(M,N);
+ MDD N=lddmc_cube ( list_marq,m_nbPlaces );
+ M=lddmc_union_mono ( M,N );
}
return M;
}
-void * MCHybridSOG::threadHandler(void *context)
+void * MCHybridSOG::threadHandler ( void *context )
{
- return ((MCHybridSOG*)context)->doCompute();
+ return ( ( MCHybridSOG* ) context )->doCompute();
}
-void MCHybridSOG::convert_wholemdd_stringcpp(MDD cmark,string &res)
+void MCHybridSOG::convert_wholemdd_stringcpp ( MDD cmark,string &res )
{
typedef pair<string,MDD> Pair_stack;
vector<Pair_stack> local_stack;
@@ -775,140 +737,138 @@ void MCHybridSOG::convert_wholemdd_stringcpp(MDD cmark,string &res)
string chaine;
res=" ";
- local_stack.push_back(Pair_stack(chaine,cmark));
- do
- {
+ local_stack.push_back ( Pair_stack ( chaine,cmark ) );
+ do {
Pair_stack element=local_stack.back();
chaine=element.first;
explore_mdd=element.second;
local_stack.pop_back();
compteur++;
- while ( explore_mdd!= lddmc_false && explore_mdd!=lddmc_true)
- {
- mddnode_t n_val = GETNODE(explore_mdd);
- if (mddnode_getright(n_val)!=lddmc_false)
- {
- local_stack.push_back(Pair_stack(chaine,mddnode_getright(n_val)));
+ while ( explore_mdd!= lddmc_false && explore_mdd!=lddmc_true ) {
+ mddnode_t n_val = GETNODE ( explore_mdd );
+ if ( mddnode_getright ( n_val ) !=lddmc_false ) {
+ local_stack.push_back ( Pair_stack ( chaine,mddnode_getright ( n_val ) ) );
}
- unsigned int val = mddnode_getvalue(n_val);
+ unsigned int val = mddnode_getvalue ( n_val );
- chaine.push_back((unsigned char)(val)+1);
- explore_mdd=mddnode_getdown(n_val);
+ chaine.push_back ( ( unsigned char ) ( val )+1 );
+ explore_mdd=mddnode_getdown ( n_val );
}
/*printchaine(&chaine);printf("\n");*/
res+=chaine;
- }
- while (local_stack.size()!=0);
+ } while ( local_stack.size() !=0 );
//delete chaine;
- compteur=(compteur<<1) | 1;
- res[1]=(unsigned char)((compteur>>8)+1);
- res[0]=(unsigned char)(compteur & 255);
+ compteur= ( compteur<<1 ) | 1;
+ res[1]= ( unsigned char ) ( ( compteur>>8 )+1 );
+ res[0]= ( unsigned char ) ( compteur & 255 );
}
-void MCHybridSOG::get_md5(const string& chaine,unsigned char *md_chaine)
+void MCHybridSOG::get_md5 ( const string& chaine,unsigned char *md_chaine )
{
- pthread_spin_lock(&m_spin_md5);
- MD5(chaine.c_str(), chaine.size(),md_chaine);
- pthread_spin_unlock(&m_spin_md5);
+ pthread_spin_lock ( &m_spin_md5 );
+ MD5 ( chaine.c_str(), chaine.size(),md_chaine );
+ pthread_spin_unlock ( &m_spin_md5 );
//md_chaine[16]='\0';
}
-void MCHybridSOG::sendSuccToMC() {
+void MCHybridSOG::sendSuccToMC()
+{
uint32_t nb_succ=m_aggWaiting->getSuccessors()->size();
uint32_t message_size=nb_succ*20+4;
-
+
char mess_tosend[message_size];
- memcpy(mess_tosend,&nb_succ,4);
+ memcpy ( mess_tosend,&nb_succ,4 );
uint32_t i_message=4;
//cout<<"***************************Number of succesors to send :"<<nb_succ<<endl;
- for (uint32_t i=0;i<nb_succ;i++) {
-
- pair<LDDState*,int> elt;
- elt=m_aggWaiting->getSuccessors()->at(i);
- memcpy(mess_tosend+i_message,elt.first->getSHAValue(),16);
- i_message+=16;
- uint16_t pcontainer=elt.first->getProcess();
- //cout<<" pcontainer "<<pcontainer<<endl;
- memcpy(mess_tosend+i_message,&pcontainer,2);
- i_message+=2;
- memcpy(mess_tosend+i_message,&(elt.second),2);
- i_message+=2;
- }
-
- MPI_Send(mess_tosend,message_size,MPI_BYTE,n_tasks, TAG_ACK_SUCC,MPI_COMM_WORLD);
-
+ for ( uint32_t i=0; i<nb_succ; i++ ) {
+
+ pair<LDDState*,int> elt;
+ elt=m_aggWaiting->getSuccessors()->at ( i );
+ memcpy ( mess_tosend+i_message,elt.first->getSHAValue(),16 );
+ i_message+=16;
+ uint16_t pcontainer=elt.first->getProcess();
+ //cout<<" pcontainer "<<pcontainer<<endl;
+ memcpy ( mess_tosend+i_message,&pcontainer,2 );
+ i_message+=2;
+ memcpy ( mess_tosend+i_message,& ( elt.second ),2 );
+ i_message+=2;
+ }
+
+ MPI_Send ( mess_tosend,message_size,MPI_BYTE,n_tasks, TAG_ACK_SUCC,MPI_COMM_WORLD );
+
}
-set<uint16_t> MCHybridSOG::getMarkedPlaces(LDDState *agg) {
+set<uint16_t> MCHybridSOG::getMarkedPlaces ( LDDState *agg )
+{
set<uint16_t> result;
MDD mdd=agg->getLDDValue();
uint16_t depth=0;
- while (mdd>lddmc_true)
- {
+ while ( mdd>lddmc_true ) {
//printf("mddd : %d \n",mdd);
- mddnode_t node=GETNODE(mdd);
- if (m_place_proposition.find(depth)!=m_place_proposition.end())
- if (mddnode_getvalue(node)==1) {
- result.insert(depth);
- }
+ mddnode_t node=GETNODE ( mdd );
+ if ( m_place_proposition.find ( depth ) !=m_place_proposition.end() )
+ if ( mddnode_getvalue ( node ) ==1 ) {
+ result.insert ( depth );
+ }
- mdd=mddnode_getdown(node);
+ mdd=mddnode_getdown ( node );
depth++;
}
return result;
}
-set<uint16_t> MCHybridSOG::getUnmarkedPlaces(LDDState *agg) {
+set<uint16_t> MCHybridSOG::getUnmarkedPlaces ( LDDState *agg )
+{
set<uint16_t> result;
MDD mdd=agg->getLDDValue();
uint16_t depth=0;
- while (mdd>lddmc_true)
- {
+ while ( mdd>lddmc_true ) {
//printf("mddd : %d \n",mdd);
- mddnode_t node=GETNODE(mdd);
- if (m_place_proposition.find(depth)!=m_place_proposition.end())
- if (mddnode_getvalue(node)==0) {
- result.insert(depth);
+ mddnode_t node=GETNODE ( mdd );
+ if ( m_place_proposition.find ( depth ) !=m_place_proposition.end() )
+ if ( mddnode_getvalue ( node ) ==0 ) {
+ result.insert ( depth );
- }
+ }
- mdd=mddnode_getdown(node);
+ mdd=mddnode_getdown ( node );
depth++;
}
return result;
}
// Send propositions to Model checker
-void MCHybridSOG::sendPropToMC(size_t pos) {
- LDDState *agg=m_graph->getLDDStateById(pos);
- set<uint16_t> marked_places=getMarkedPlaces(agg);
- set<uint16_t> unmarked_places=getUnmarkedPlaces(agg);
- uint16_t s_mp=marked_places.size();
- uint16_t s_up=unmarked_places.size();
- char mess_to_send[8+s_mp*2+s_up*2+5];
- memcpy(mess_to_send,&pos,8);
- //cout<<"************* Pos to send :"<<pos<<endl;
- size_t indice=8;
- memcpy(mess_to_send+indice,&s_mp,2);
- indice+=2;
- for (auto it=marked_places.begin();it!=marked_places.end();it++) {
- memcpy(mess_to_send+indice,&(*it),2);
+void MCHybridSOG::sendPropToMC ( size_t pos )
+{
+ LDDState *agg=m_graph->getLDDStateById ( pos );
+ set<uint16_t> marked_places=getMarkedPlaces ( agg );
+ set<uint16_t> unmarked_places=getUnmarkedPlaces ( agg );
+ uint16_t s_mp=marked_places.size();
+ uint16_t s_up=unmarked_places.size();
+ char mess_to_send[8+s_mp*2+s_up*2+5];
+ memcpy ( mess_to_send,&pos,8 );
+ //cout<<"************* Pos to send :"<<pos<<endl;
+ size_t indice=8;
+ memcpy ( mess_to_send+indice,&s_mp,2 );
+ indice+=2;
+ for ( auto it=marked_places.begin(); it!=marked_places.end(); it++ ) {
+ memcpy ( mess_to_send+indice,& ( *it ),2 );
indice+=2;
}
- memcpy(mess_to_send+indice,&s_up,2);
+ memcpy ( mess_to_send+indice,&s_up,2 );
indice+=2;
- for (auto it=unmarked_places.begin();it!=unmarked_places.end();it++) {
- memcpy(mess_to_send+indice,&(*it),2);
+ for ( auto it=unmarked_places.begin(); it!=unmarked_places.end(); it++ ) {
+ memcpy ( mess_to_send+indice,& ( *it ),2 );
indice+=2;
}
uint8_t divblock=agg->isDiv();
- divblock=divblock | (agg->isDeadLock()<<1);
- memcpy(mess_to_send+indice,&divblock,1);
+ divblock=divblock | ( agg->isDeadLock() <<1 );
+ memcpy ( mess_to_send+indice,&divblock,1 );
indice++;
- MPI_Send(mess_to_send,indice,MPI_BYTE,n_tasks, TAG_ACK_STATE, MPI_COMM_WORLD);
+ MPI_Send ( mess_to_send,indice,MPI_BYTE,n_tasks, TAG_ACK_STATE, MPI_COMM_WORLD );
}
diff --git a/src/MDGraph.cpp b/src/MDGraph.cpp
index d6199310e8b5ac73fa02990c3514d816d82f5ced..7236995dbf5f119bf0522e848a40fb57483a77fe 100644
--- a/src/MDGraph.cpp
+++ b/src/MDGraph.cpp
@@ -1,59 +1,55 @@
-
-/******** Graph.cpp *******/
#include "MDGraph.h"
-/*#include <conio>*/
+
bdd * Tab;
/********* setInitialState *****/
-void MDGraph::setInitialState(Class_Of_State *c)
+void MDGraph::setInitialState ( Class_Of_State *c )
{
- currentstate=initialstate=c;
+ currentstate=initialstate=c;
}
/*----------------------find()----------------*/
-Class_Of_State * MDGraph::find(Class_Of_State* c)
+Class_Of_State * MDGraph::find ( Class_Of_State* c )
{
- for(MetaGrapheNodes::const_iterator i=GONodes.begin();!(i==GONodes.end());i++)
- //if((c->class_state.id()==(*i)->class_state.id())&&(c->blocage==(*i)->blocage)&&(c->boucle==(*i)->boucle))
-if(c->class_state.id()==(*i)->class_state.id())
- return *i;
- return NULL;
+ for ( MetaGrapheNodes::const_iterator i=GONodes.begin(); ! ( i==GONodes.end() ); i++ )
+ //if((c->class_state.id()==(*i)->class_state.id())&&(c->blocage==(*i)->blocage)&&(c->boucle==(*i)->boucle))
+ if ( c->class_state.id() == ( *i )->class_state.id() ) {
+ return *i;
+ }
+ return NULL;
}
/*----------------------insert() ------------*/
-void MDGraph::insert(Class_Of_State *c)
+void MDGraph::insert ( Class_Of_State *c )
{
- c->Visited=false;
- this->GONodes.push_back(c);
- nbStates++;
+ c->Visited=false;
+ this->GONodes.push_back ( c );
+ nbStates++;
}
/*----------------------NbBddNod()------------------------*/
-int MDGraph::NbBddNode(Class_Of_State * S, size_t& nb)
+int MDGraph::NbBddNode ( Class_Of_State * S, size_t& nb )
{
- if(S->Visited==false)
- {
- //cout<<"insertion du meta etat numero :"<<nb<<"son id est :"<<S->class_state.id()<<endl;
- //cout<<"sa taille est :"<<bdd_nodecount(S->class_state)<<" noeuds \n";
- Tab[nb-1]=S->class_state;
- S->Visited=true;
- int bddnode=bdd_nodecount(S->class_state);
- int size_succ=0;
- for(Edges::const_iterator i=S->Successors.begin();!(i==S->Successors.end());i++)
- {
- if((*i).first->Visited==false)
- {
- nb++;
- size_succ+=NbBddNode((*i).first,nb);
- }
- }
- return size_succ+bddnode;
-
- }
- else
- return 0;
+ if ( S->Visited==false ) {
+ //cout<<"insertion du meta etat numero :"<<nb<<"son id est :"<<S->class_state.id()<<endl;
+ //cout<<"sa taille est :"<<bdd_nodecount(S->class_state)<<" noeuds \n";
+ Tab[nb-1]=S->class_state;
+ S->Visited=true;
+ int bddnode=bdd_nodecount ( S->class_state );
+ int size_succ=0;
+ for ( Edges::const_iterator i=S->Successors.begin(); ! ( i==S->Successors.end() ); i++ ) {
+ if ( ( *i ).first->Visited==false ) {
+ nb++;
+ size_succ+=NbBddNode ( ( *i ).first,nb );
+ }
+ }
+ return size_succ+bddnode;
+
+ } else {
+ return 0;
+ }
}
/*----------------------Visualisation du graphe------------------------*/
@@ -61,107 +57,100 @@ void MDGraph::printCompleteInformation()
{
- cout << "\n\nGRAPH SIZE : \n";
- cout<< "\n\tNB MARKING : "<< nbMarking;
- cout<< "\n\tNB NODES : "<< nbStates;
- cout<<"\n\tNB ARCS : " <<nbArcs<<endl;
- cout<<" \n\nCOMPLETE INFORMATION ?(y/n)\n";
- char c;
- cin>>c;
- //InitVisit(initialstate,n);
- Tab=new bdd[(int)nbStates];
- size_t n=1;
- //cout<<"NB BDD NODE : "<<NbBddNode(initialstate,n)<<endl;
- NbBddNode(initialstate,n);
- cout<<"NB BDD NODE : "<<bdd_anodecount(Tab,(int)nbStates)<<endl;
- //cout<<"Shared Nodes : "<<bdd_anodecount(Tab,nbStates)<<endl;
- InitVisit(initialstate,1);
- //int toto;cin>>toto;
- //bdd Union=UnionMetaState(initialstate,1);
- //cout<<"a titre indicatif taille de l'union : "<<bdd_nodecount(Union)<<endl;
- if(c=='y'||c=='Y')
- {
- size_t n=1;
- printGraph(initialstate,n);
- }
+ cout << "\n\nGRAPH SIZE : \n";
+ cout<< "\n\tNB MARKING : "<< nbMarking;
+ cout<< "\n\tNB NODES : "<< nbStates;
+ cout<<"\n\tNB ARCS : " <<nbArcs<<endl;
+ cout<<" \n\nCOMPLETE INFORMATION ?(y/n)\n";
+ char c;
+ cin>>c;
+ //InitVisit(initialstate,n);
+ Tab=new bdd[ ( int ) nbStates];
+ size_t n=1;
+ //cout<<"NB BDD NODE : "<<NbBddNode(initialstate,n)<<endl;
+ NbBddNode ( initialstate,n );
+ cout<<"NB BDD NODE : "<<bdd_anodecount ( Tab, ( int ) nbStates ) <<endl;
+ //cout<<"Shared Nodes : "<<bdd_anodecount(Tab,nbStates)<<endl;
+ InitVisit ( initialstate,1 );
+ //int toto;cin>>toto;
+ //bdd Union=UnionMetaState(initialstate,1);
+ //cout<<"a titre indicatif taille de l'union : "<<bdd_nodecount(Union)<<endl;
+ if ( c=='y'||c=='Y' ) {
+ size_t n=1;
+ printGraph ( initialstate,n );
+ }
}
/*----------------------InitVisit()------------------------*/
-void MDGraph::InitVisit(Class_Of_State * S,size_t nb)
+void MDGraph::InitVisit ( Class_Of_State * S,size_t nb )
{
- if(nb<=nbStates)
- {
- S->Visited=false;
- for(Edges::const_iterator i=S->Successors.begin();!(i==S->Successors.end());i++)
- {
+ if ( nb<=nbStates ) {
+ S->Visited=false;
+ for ( Edges::const_iterator i=S->Successors.begin(); ! ( i==S->Successors.end() ); i++ ) {
- if((*i).first->Visited==true)
- {
- nb++;
- InitVisit((*i).first,nb);
- }
- }
+ if ( ( *i ).first->Visited==true ) {
+ nb++;
+ InitVisit ( ( *i ).first,nb );
+ }
+ }
- }
+ }
}
/********* printGraph *****/
-void MDGraph::printGraph(Class_Of_State *s,size_t &nb)
+void MDGraph::printGraph ( Class_Of_State *s,size_t &nb )
{
- if(nb<=nbStates)
- {
- cout<<"\nSTATE NUMBER "<<nb<<" : \n";
- s->Visited=true;
- printsuccessors(s);
- getchar();
- printpredecessors(s);
- getchar();
- Edges::const_iterator i;
- for(i=s->Successors.begin();!(i==s->Successors.end());i++)
- {
- if((*i).first->Visited==false)
- {
- nb++;
- printGraph((*i).first, nb);
- }
- }
-
- }
+ if ( nb<=nbStates ) {
+ cout<<"\nSTATE NUMBER "<<nb<<" : \n";
+ s->Visited=true;
+ printsuccessors ( s );
+ getchar();
+ printpredecessors ( s );
+ getchar();
+ Edges::const_iterator i;
+ for ( i=s->Successors.begin(); ! ( i==s->Successors.end() ); i++ ) {
+ if ( ( *i ).first->Visited==false ) {
+ nb++;
+ printGraph ( ( *i ).first, nb );
+ }
+ }
+
+ }
}
/*---------void print_successors_class(Class_Of_State *)------------*/
-void MDGraph::printsuccessors(Class_Of_State *s)
+void MDGraph::printsuccessors ( Class_Of_State *s )
{
- Edges::const_iterator i;
- cout<<bddtable<<s->class_state<<endl;
- if(s->boucle)
- cout<<"\n\tON BOUCLE DESSUS AVEC EPSILON\n";
- if(s->blocage)
- cout<<"\n\tEXISTENCE D'UN ETAT BLOCANT\n";
- cout<<"\n\tSES SUCCESSEURS SONT ( "<<s->Successors.size()<<" ) :\n\n";
- getchar();
- for(i =s->Successors.begin();!(i==s->Successors.end());i++)
- {
- cout<<" \t- t"<<(*i).second<<" ->";
- cout<<bddtable<<(*i).first->class_state<<endl;
- getchar();
- }
+ Edges::const_iterator i;
+ cout<<bddtable<<s->class_state<<endl;
+ if ( s->boucle ) {
+ cout<<"\n\tON BOUCLE DESSUS AVEC EPSILON\n";
+ }
+ if ( s->blocage ) {
+ cout<<"\n\tEXISTENCE D'UN ETAT BLOCANT\n";
+ }
+ cout<<"\n\tSES SUCCESSEURS SONT ( "<<s->Successors.size() <<" ) :\n\n";
+ getchar();
+ for ( i =s->Successors.begin(); ! ( i==s->Successors.end() ); i++ ) {
+ cout<<" \t- t"<< ( *i ).second<<" ->";
+ cout<<bddtable<< ( *i ).first->class_state<<endl;
+ getchar();
+ }
}
/*---------void printpredescessors(Class_Of_State *)------------*/
-void MDGraph::printpredecessors(Class_Of_State *s)
+void MDGraph::printpredecessors ( Class_Of_State *s )
{
- Edges::const_iterator i;
- cout<<"\n\tSES PREDESCESSEURS SONT ( "<<s->Predecessors.size()<<" ) :\n\n";
- getchar();
- for(i =s->Predecessors.begin();!(i==s->Predecessors.end());i++)
- {
- cout<<" \t- t"<<(*i).second<<" ->";
- cout<<bddtable<<(*i).first->class_state<<endl;
- getchar();
- }
+ Edges::const_iterator i;
+ cout<<"\n\tSES PREDESCESSEURS SONT ( "<<s->Predecessors.size() <<" ) :\n\n";
+ getchar();
+ for ( i =s->Predecessors.begin(); ! ( i==s->Predecessors.end() ); i++ ) {
+ cout<<" \t- t"<< ( *i ).second<<" ->";
+ cout<<bddtable<< ( *i ).first->class_state<<endl;
+ getchar();
+ }
}
diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp
index d1b984c8f81d2ddadda64ed75b568b58ffd54f48..c93f3fc279b0ddccc88e026301d5cb0cb32d6f83 100644
--- a/src/ModelCheckLace.cpp
+++ b/src/ModelCheckLace.cpp
@@ -64,11 +64,8 @@ void ModelCheckLace::preConfigure() {
}
m_initialMarking=lddmc_cube(liste_marques,m_net->places.size());
- delete []liste_marques;
lddmc_refs_push(m_initialMarking);
-
-
-
+ delete []liste_marques;
uint32_t *prec = new uint32_t[m_nbPlaces];
uint32_t *postc= new uint32_t [m_nbPlaces];
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index d6dac10c374128f59899b65b025a9da1f0dda64d..85ae0a3dd3cc9e74a391b514215a5b695461fd51 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -54,7 +54,7 @@ void ModelCheckerTh::preConfigure() {
}
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
@@ -124,14 +124,13 @@ void* ModelCheckerTh::Compute_successors() {
if (id_thread == 0) {
LDDState *c = new LDDState;
- MDD Complete_meta_state(Accessible_epsilon(m_initialMarking));
+ MDD Complete_meta_state=Accessible_epsilon(m_initialMarking);
ldd_refs_push(Complete_meta_state);
- MDD canonised_initial = Complete_meta_state; //Canonize(Complete_meta_state,0);
- /*ldd_refs_push(canonised_initial);*/
+
fire = firable_obs(Complete_meta_state);
- c->m_lddstate = canonised_initial;
- c->setDeadLock(Set_Bloc(Complete_meta_state));
- c->setDiv(Set_Div(Complete_meta_state));
+ c->m_lddstate = Complete_meta_state;
+ //c->setDeadLock(Set_Bloc(Complete_meta_state));
+ //c->setDiv(Set_Div(Complete_meta_state));
m_st[0].push(Pair(couple(c, Complete_meta_state), fire));
m_graph->setInitialState(c);
m_graph->insert(c);
@@ -153,6 +152,7 @@ void* ModelCheckerTh::Compute_successors() {
int t = *e.second.begin();
e.second.erase(t);
+
if (id_thread) {
pthread_mutex_lock(&m_supervise_gc_mutex);
m_gc++;
@@ -162,27 +162,27 @@ void* ModelCheckerTh::Compute_successors() {
pthread_mutex_unlock(&m_supervise_gc_mutex);
}
- MDD Complete_meta_state = Accessible_epsilon(get_successor(e.first.second, t));
- ldd_refs_push(Complete_meta_state);
- MDD reduced_meta = Complete_meta_state; //Canonize(Complete_meta_state,0);
+
+ //MDD reduced_meta = Complete_meta_state; //Canonize(Complete_meta_state,0);
/*ldd_refs_push(reduced_meta);*/
if (id_thread == 0) {
pthread_mutex_lock(&m_gc_mutex);
// #ifdef DEBUG_GC
- // displayMDDTableInfo();
+ //displayMDDTableInfo();
// #endif // DEBUG_GC
sylvan_gc_seq();
// #ifdef DEBUG_GC
- // displayMDDTableInfo();
+ //displayMDDTableInfo();
// #endif // DEBUG_GC
pthread_mutex_unlock(&m_gc_mutex);
}
+ 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;
- //reached_class->m_lddstate=reduced_meta;
- //nbnode=bdd_pathcount(reached_class->m_lddstate);
+
//pthread_spin_lock(&m_accessible);
pthread_mutex_lock(&m_graph_mutex);
@@ -196,20 +196,20 @@ void* ModelCheckerTh::Compute_successors() {
m_graph->addArc();
m_graph->insert(reached_class);
- reached_class->setDiv(Set_Div(Complete_meta_state));
- reached_class->setDeadLock(Set_Bloc(Complete_meta_state));
+
+ //reached_class->setDiv(Set_Div(reduced_meta));
+ //reached_class->setDeadLock(Set_Bloc(reduced_meta));
pthread_mutex_unlock(&m_graph_mutex);
-
- e.first.first->Successors.insert(e.first.first->Successors.begin(), LDDEdge(reached_class, t));
+ 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);
- fire = firable_obs(Complete_meta_state);
+ fire = firable_obs(reduced_meta);
//if (max_succ<fire.size()) max_succ=fire.size();
//pthread_mutex_unlock(&m_mutex);
min_charge = minCharge();
//m_min_charge=(m_min_charge+1) % m_nb_thread;
pthread_spin_lock(&m_spin_stack[min_charge]);
- m_st[min_charge].push(Pair(couple(reached_class, Complete_meta_state), fire));
+ m_st[min_charge].push(Pair(couple(reached_class, reduced_meta), fire));
pthread_spin_unlock(&m_spin_stack[min_charge]);
m_charge[min_charge]++;
} else {
@@ -243,7 +243,7 @@ void* ModelCheckerTh::threadHandler(void *context) {
void ModelCheckerTh::ComputeTh_Succ() {
m_id_thread = 0;
-
+ m_gc==0;
pthread_mutex_init(&m_mutex, NULL);
pthread_mutex_init(&m_gc_mutex, NULL);
pthread_mutex_init(&m_graph_mutex, NULL);
diff --git a/src/ModelCheckerTh.h b/src/ModelCheckerTh.h
index c274d1968ed9354223096432968443bbcfcb6e7a..58bce47f2fc6dc1782fcbb111118b87f82001af9 100644
--- a/src/ModelCheckerTh.h
+++ b/src/ModelCheckerTh.h
@@ -1,6 +1,7 @@
#ifndef MODELCHECKERTH_H
#define MODELCHECKERTH_H
#include "ModelCheckBaseMT.h"
+#include <atomic>
typedef pair<LDDState *, int> couple_th;
typedef stack<pair<LDDState *,int>> pile_t;
@@ -28,7 +29,7 @@ private:
pthread_mutex_t m_supervise_gc_mutex;
pthread_barrier_t m_barrier_builder;
- unsigned int m_gc;
+ unsigned int m_gc=0; //
bool m_finish=false;
bool m_finish_initial=false;
pthread_mutex_t m_mutex_stack[128];
diff --git a/src/SogKripke.h b/src/SogKripke.h
index d4b13c849a53ba1be2a84fa620ee7f5f36fd55e1..60f7e28dbf87d7f38df1d2c6253b1d06841486ae 100644
--- a/src/SogKripke.h
+++ b/src/SogKripke.h
@@ -5,23 +5,20 @@
#include <spot/kripke/kripke.hh>
class SogKripke: public spot::kripke {
public:
-
-
-
- SogKripke(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog);
- SogKripke(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog,set<string> &l_transap,set<string> &l_placeap);
+ SogKripke ( const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog );
+ SogKripke ( const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog,set<string> &l_transap,set<string> &l_placeap );
virtual ~SogKripke();
spot::state* get_init_state() const;
- SogKripkeIterator* succ_iter(const spot::state* s) const override;
- std::string format_state(const spot::state* s) const override;
- bdd state_condition(const spot::state* s) const override;
+ SogKripkeIterator* succ_iter ( const spot::state* s ) const override;
+ std::string format_state ( const spot::state* s ) const override;
+ bdd state_condition ( const spot::state* s ) const override;
protected:
private:
- std::map<int, int> place_prop;
- LDDGraph* m_sog;
-};
+ std::map<int, int> place_prop;
+ LDDGraph* m_sog;
+ };
#endif // SOGKRIPKE_H_INCLUDED
diff --git a/src/SogKripkeIteratorTh.cpp b/src/SogKripkeIteratorTh.cpp
index 4862d6095e2c762e1cdcd3309099c0ecd265be5a..638840e4a2d5254af15fd4d5e492db8f65c5a129 100644
--- a/src/SogKripkeIteratorTh.cpp
+++ b/src/SogKripkeIteratorTh.cpp
@@ -4,57 +4,63 @@
#include "SogKripkeIteratorTh.h"
-SogKripkeIteratorTh::SogKripkeIteratorTh(const LDDState* lddstate, bdd cnd):m_lddstate(lddstate), kripke_succ_iterator(cnd)
+SogKripkeIteratorTh::SogKripkeIteratorTh ( const LDDState* lddstate, bdd cnd ) :m_lddstate ( lddstate ), kripke_succ_iterator ( cnd )
{
- for (int i=0;i<m_lddstate->getSuccessors()->size();i++) {
- m_lsucc.push_back(m_lddstate->getSuccessors()->at(i));
+ for ( int i=0; i<m_lddstate->getSuccessors()->size(); i++ ) {
+ m_lsucc.push_back ( m_lddstate->getSuccessors()->at ( i ) );
}
- if (lddstate->isDeadLock()) {
- m_lsucc.push_back(pair<LDDState*,int>(&m_deadlock,-1));
+ if ( lddstate->isDeadLock() ) {
+ m_lsucc.push_back ( pair<LDDState*,int> ( &m_deadlock,-1 ) );
}
- if (lddstate->isDiv()) {
- m_lsucc.push_back(pair<LDDState*,int>(&m_div,-1));
+ if ( lddstate->isDiv() ) {
+ m_lsucc.push_back ( pair<LDDState*,int> ( &m_div,-1 ) );
}
}
-bool SogKripkeIteratorTh::first() {
+bool SogKripkeIteratorTh::first()
+{
- // cout<<"entering "<<__func__<<endl;
+ // cout<<"entering "<<__func__<<endl;
m_current_edge=0;
//cout<<"exciting "<<__func__<<endl;
- return m_lsucc.size()!=0;
+ return m_lsucc.size() !=0;
}
-bool SogKripkeIteratorTh::next() {
+bool SogKripkeIteratorTh::next()
+{
//cout<<"entering "<<__func__<<" "<<m_current_edge<<endl;
m_current_edge++;
return m_current_edge<m_lsucc.size();
}
-bool SogKripkeIteratorTh::done() const {
+bool SogKripkeIteratorTh::done() const
+{
//cout<<"entring /excit"<<__func__<<endl;
return m_current_edge==m_lsucc.size();
}
SogKripkeStateTh* SogKripkeIteratorTh::dst() const
- {
+{
/*cout<<"Source "<<m_lddstate->getLDDValue()<<"Destination :"<<m_lsucc.at(m_current_edge).first->getLDDValue()<<" in "<<m_lsucc.size()<<" / "<<m_current_edge<<endl;*/
- return new SogKripkeStateTh(m_lsucc.at(m_current_edge).first);
- }
+ return new SogKripkeStateTh ( m_lsucc.at ( m_current_edge ).first );
+}
-bdd SogKripkeIteratorTh::cond() const {
+bdd SogKripkeIteratorTh::cond() const
+{
//cout<<"entering "<<__func__<<endl;
- if (m_lsucc.at(m_current_edge).second==-1) return bddtrue;
+ if ( m_lsucc.at ( m_current_edge ).second==-1 ) {
+ return bddtrue;
+ }
- string name=m_builder->getTransition(m_lsucc.at(m_current_edge).second);
+ string name=m_builder->getTransition ( m_lsucc.at ( m_current_edge ).second );
//cout<<"Value "<<m_lddstate->getSuccessors()->at(m_current_edge).second<<" Transition name "<<name<<endl;
spot::bdd_dict *p=m_dict_ptr->get();
- spot::formula f=spot::formula::ap(name);
- bdd result=bdd_ithvar((p->var_map.find(f))->second);
+ spot::formula f=spot::formula::ap ( name );
+ bdd result=bdd_ithvar ( ( p->var_map.find ( f ) )->second );
return result & spot::kripke_succ_iterator::cond();
}
@@ -68,10 +74,10 @@ SogKripkeIteratorTh::~SogKripkeIteratorTh()
//dtor
}
-void SogKripkeIteratorTh::recycle(LDDState* aggregate, bdd cond)
+void SogKripkeIteratorTh::recycle ( LDDState* aggregate, bdd cond )
{
- m_lddstate=aggregate;
- spot::kripke_succ_iterator::recycle(cond);
+ m_lddstate=aggregate;
+ spot::kripke_succ_iterator::recycle ( cond );
}
static ModelCheckBaseMT * SogKripkeIteratorTh::m_builder;
diff --git a/src/sylvan_sog.c b/src/sylvan_sog.c
index 80424bb29686816f757e0bb943266d1dc8e056f7..1ed1663c17b1e68e816a2ba8d451ef2f9a3d86e8 100644
--- a/src/sylvan_sog.c
+++ b/src/sylvan_sog.c
@@ -59,15 +59,14 @@ TASK_IMPL_3(MDD, lddmc_firing_lace, MDD, cmark, MDD, minus, MDD ,plus) {
if (cmark == lddmc_false) break;
n_cmark = GETNODE(cmark);
}
- if (count>10) printf("Count %d\n",count);
+
result= lddmc_false;
while (count--) {
lddmc_refs_push(result);
MDD left=lddmc_refs_sync(SYNC(lddmc_firing_lace));
lddmc_refs_push(left);
MDD result2 =
- lddmc_makenode(l_values[count],left, lddmc_false);
- if (l_values[count]>5) printf("%d ",l_values[count]);
+ lddmc_makenode(l_values[count],left, lddmc_false);
lddmc_refs_push(result2);
result = lddmc_union( result, result2);
lddmc_refs_pop(3);