diff --git a/src/LDDState.cpp b/src/LDDState.cpp index afd70ba1dfd33372f411d1c5cae9bd5b9015cf94..6d4809142480528e80de9bfc3a36a865d3bb1329 100644 --- a/src/LDDState.cpp +++ b/src/LDDState.cpp @@ -30,9 +30,7 @@ vector<pair<LDDState*, int>>* LDDState::getSuccessors() { } void LDDState::setMarked() { - isMarked()=true; + m_marked=true; } -bool LDDState::isMarked() { - return m_marked; -} + diff --git a/src/LDDState.h b/src/LDDState.h index 4447b7fe97a03499b6e4b7a24d251c49b5318502..ba11fbae03a2c133cca4cd908eb9b6c0d34b6956 100755 --- a/src/LDDState.h +++ b/src/LDDState.h @@ -12,7 +12,6 @@ class LDDState { LDDState() { m_boucle = m_blocage = m_visited = false; m_virtual = false; - m_marked = false; } virtual ~LDDState(); Set firable; @@ -28,13 +27,13 @@ class LDDState { bool m_boucle; bool m_blocage; bool m_visited; + bool m_marked; bool isVirtual(); void setVirtual(); void setDiv(bool di) {m_boucle=di;} bool isDiv() {return m_boucle;} void setDeadLock(bool de) {m_blocage=de;} bool isDeadLock() {return m_blocage;} - bool isMarked(); void setMarked(); protected: private: diff --git a/src/NewNet.cpp b/src/NewNet.cpp index e9d7625eca23b737b040dae2caa1eb7845ebbd49..7ba29cf236d0c9aebf5e6b9f838f81daecb05435 100644 --- a/src/NewNet.cpp +++ b/src/NewNet.cpp @@ -136,21 +136,26 @@ NewNet::NewNet(const char *f, const set<string> & f_trans) { int pos_trans(TRANSITIONS T, string trans); for (set<string>::const_iterator i=list_t.begin();i!=list_t.end();i++) { int pos = pos_trans(transitions, *i); + Observable.clear(); if (pos==-1) { cout<<"Error: "<<*i<<" is not a transition!"<<endl; // Check if the proposition corresponds to a place map<string, int>::iterator pi = placeName.find(*i); if (pi!=placeName.end()) cout<<"Place was found!"<<endl; m_formula_place.insert(pi->second); + Observable.insert(pi->first->pre); + //Observable.insert(pi->post); } else { Formula_Trans.insert(pos); cout<<"Transition found pos="<<pos<<endl; map<string,int>::iterator ti=transitionName.find(*i); cout<<"pos= "<<ti->second<<endl; + Observable.insert(pos); + } } } - } + /*---------------------------------Set_formula_trans()------------------*/ bool NewNet::Set_Formula_Trans(const char *f) { diff --git a/src/threadSOG.cpp b/src/threadSOG.cpp index 917a54ce5d2229728b79551c008eb11cc57ae5b4..130d7388831d5d4986da0ba266258c45e4d506d5 100644 --- a/src/threadSOG.cpp +++ b/src/threadSOG.cpp @@ -215,11 +215,14 @@ void threadSOG::computeSeqSOG(LDDGraph &g) // cout<<"Avant Accessible epsilon \n"; MDD Complete_meta_state=Accessible_epsilon(get_successor(e.first.second,t)); //MDD reduced_meta=Canonize(Complete_meta_state,0); + ldd_refs_push(Complete_meta_state); //ldd_refs_push(reduced_meta); //sylvan_gc_seq(); reached_class->m_lddstate=Complete_meta_state; + if (is_marcked()) + reached_class->setMarked(); // reached_class->m_lddstate=reduced_meta; LDDState* pos=g.find(reached_class); //nbnode=sylvan_pathcount(reached_class->m_lddstate); @@ -1053,3 +1056,13 @@ cout<<"\n=========================================\n"; std::cout << "TIME OF CONSTRUCTION OF THE SOG " << tps << " seconds\n"; } + +bool LDDState::isMarked() { + + for (set<string>::const_iterator i=m_place_proposition.begin();i!=m_place_proposition.end();i++) + { + if (i->marking>0) + return true; + } + return false; +} diff --git a/src/threadSOG.h b/src/threadSOG.h index f0880740447ef681031bf03b9f575a79bd34e5c2..fcce6dcd29cabc0a48bcfb2991ceae19758740ae 100644 --- a/src/threadSOG.h +++ b/src/threadSOG.h @@ -32,8 +32,6 @@ class threadSOG : public CommonSOG{ static void *threadHandlerCanonized(void *context); void *doCompute(); void *doComputeCanonized(); - - void computeSOGLace(LDDGraph &g); void computeSOGLaceCanonized(LDDGraph &g);