modifié : src/CommonSOG.cpp

	modifié :         src/HybridKripke.cpp
	modifié :         src/MCHybridSOG.cpp
	modifié :         src/MDGraph.cpp
	modifié :         src/ModelCheckLace.cpp
	modifié :         src/ModelCheckerTh.cpp
	modifié :         src/ModelCheckerTh.h
	modifié :         src/SogKripke.h
	modifié :         src/SogKripkeIteratorTh.cpp
	modifié :         src/sylvan_sog.c
	modifié :         third-party/sylvan (contenu modifié)

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;

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;
   }
 

src/MDGraph.cpp

-
-/********              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();
+    }
 }
 

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];

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);

src/ModelCheckerTh.h

 #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];

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

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;

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);