modifié : src/CommonSOG.cpp

	modifié :         src/CommonSOG.h
	modifié :         src/LDDGraph.cpp
	modifié :         src/ModelCheckBaseMT.cpp
	modifié :         src/ModelCheckerTh.cpp
	modifié :         src/SogKripkeTh.cpp

CMakeLists.txt

@@ -6,7 +6,7 @@ project(pmc-sog C CXX)
 
 # compiler flags
 if(CMAKE_COMPILER_IS_GNUCC)
-  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fpermissive")
+  set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fpermissive -g3")
 endif()
 
 # add pn parser

src/CommonSOG.cpp

@@ -226,4 +226,4 @@ string CommonSOG::getPlace(int pos)
 {
     return m_graph->getPlace(pos);
 }
-
+static LDDGraph *CommonSOG::m_graph;

src/CommonSOG.h

@@ -29,7 +29,7 @@ class CommonSOG
     protected:
         NewNet* m_net;
         int m_nbPlaces = 0;
-        LDDGraph *m_graph;
+        static LDDGraph *m_graph;
         vector<TransSylvan> m_tb_relation;
         MDD m_initialMarking;
         map<string, uint16_t> m_transitionName;

src/LDDGraph.cpp

@@ -12,6 +12,7 @@ LDDGraph::~LDDGraph()
 void LDDGraph::setInitialState(LDDState *c)
 {
 	m_currentstate=m_initialstate=c;
+	//
 
 }
 

src/ModelCheckBaseMT.cpp

@@ -14,8 +14,8 @@ ModelCheckBaseMT::ModelCheckBaseMT(const NewNet &R,int nbThread)
 }
 void ModelCheckBaseMT::loadNet()
 {
-    preConfigure();    
-    m_graph=new LDDGraph(this);
+	m_graph=new LDDGraph(this);
+	preConfigure();
     m_graph->setTransition(m_transitionName);
     m_graph->setPlace(m_placeName);
 }

src/ModelCheckerTh.cpp

@@ -86,8 +86,7 @@ void ModelCheckerTh::preConfigure() {
 }
 
 LDDState* ModelCheckerTh::getInitialMetaState() {
-	while (!m_finish_initial)
-		;
+	while (!m_finish_initial)	;
 	LDDState *initial_metastate = m_graph->getInitialState();
 	if (!initial_metastate->isVisited()) {
 		initial_metastate->setVisited();
@@ -112,18 +111,20 @@ void* ModelCheckerTh::Compute_successors() {
 	pthread_mutex_unlock(&m_mutex);
 	Set fire;
 	int min_charge = 0;
+
 	if (id_thread == 0) {
 		LDDState *c = new LDDState;
 
 		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);
+		/*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->setDeadLock(false);//Set_Bloc(Complete_meta_state));
+		c->setDiv(false);//Set_Div(Complete_meta_state));
 		m_st[0].push(Pair(couple(c, Complete_meta_state), fire));
+
 		m_graph->setInitialState(c);
 		m_graph->insert(c);
 		m_charge[0] = 1;
@@ -154,10 +155,9 @@ void* ModelCheckerTh::Compute_successors() {
 				}
 
 				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);
-				ldd_refs_push(reduced_meta);
+				/*ldd_refs_push(reduced_meta);*/
 
 				if (id_thread == 0) {
 					pthread_mutex_lock(&m_gc_mutex);
@@ -188,8 +188,8 @@ 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(false);//Set_Div(Complete_meta_state));
+					reached_class->setDeadLock(false);//Set_Bloc(Complete_meta_state));
 					pthread_mutex_unlock(&m_graph_mutex);
 
 					e.first.first->Successors.insert(e.first.first->Successors.begin(), LDDEdge(reached_class, t));

src/SogKripkeTh.cpp

@@ -78,7 +78,7 @@ bdd SogKripkeTh::state_condition(const spot::state* s) const
   {
 
     auto ss = static_cast<const SogKripkeStateTh*>(s);
-    vector<uint16_t> marked_place=ss->getLDDState()->getMarkedPlaces(m_builder->getPlaceProposition());
+	vector<uint16_t> marked_place = ss->getLDDState()->getMarkedPlaces(m_builder->getPlaceProposition());
 
 
     bdd result=bddtrue;