modifié : src/CommonSOG.h

	modifié :         src/LDDGraph.h
	modifié :         src/LDDState.cpp
	modifié :         src/LDDState.h
	modifié :         src/SogKripke.cpp
	modifié :         src/main.cpp

src/CommonSOG.h

 #ifndef COMMONSOG_H
 #define COMMONSOG_H
+#include "LDDState.h"
 #include "LDDGraph.h"
+
 #include "TransSylvan.h"
 #include "NewNet.h"
 #include <stack>
-
+class LDDState;
 typedef pair<LDDState *, MDD> couple;
 typedef pair<couple, Set> Pair;
 typedef stack<Pair> pile;
+class LDDGraph;
 class CommonSOG
 {
     public:
@@ -18,6 +21,7 @@ class CommonSOG
         vector<TransSylvan>* getTBRelation();
         Set * getNonObservable();
         unsigned int getPlacesCount();
+        Set & getPlaceProposition() {return m_place_proposition;}
     protected:
         NewNet m_net;
         int m_nbPlaces = 0;

src/LDDGraph.h

 #ifndef LDDGRAPH_H
 #define LDDGRAPH_H
 #include "LDDState.h"
+#include "CommonSOG.h"
+
 //#include "LDDStateExtend.h"
 using namespace std;
 #include <iostream>
 #include <map>
+
 typedef set<int> Set;
 typedef vector<LDDState*> MetaLDDNodes;
-
+class CommonSOG;
 class LDDGraph
 {
     private:
         map<string,int>* m_transition;
         map<int,string>* m_places;
 		void printGraph(LDDState *, size_t &);
-
+        CommonSOG *m_constructor;
 	public:
+        CommonSOG* getConstructor() {return m_constructor;}
         string getTransition(int pos);
         string getPlace(int pos);
         void setPlace(map<int,string>& list_places);
@@ -39,7 +43,7 @@ class LDDGraph
 		void printpredecessors(LDDState *);
 		void addArc(){m_nbArcs++;}
 		void insert(LDDState*);
-		LDDGraph() {m_nbStates=m_nbArcs=m_nbMarking=0;}
+		LDDGraph(CommonSOG *constuctor) {m_nbStates=m_nbArcs=m_nbMarking=0;m_constructor=constuctor;}
 		void setInitialState(LDDState*);  //Define the initial state of this graph
 		LDDState* getInitialState() const;
 		void printCompleteInformation();

src/LDDState.cpp

@@ -2,7 +2,8 @@
 
 #include <sylvan_int.h>
 #include "LDDState.h"
-
+#include "LDDGraph.h"
+#include <iostream>
 #define GETNODE(mdd) ((mddnode_t)llmsset_index_to_ptr(nodes, mdd))
 LDDState::~LDDState()
 {
@@ -32,7 +33,7 @@ vector<pair<LDDState*, int>>* LDDState::getSuccessors() {
     return &Successors;
 }
 
-vector<int> LDDState::getMarkedPlaces() {
+vector<int> LDDState::getMarkedPlaces(set<int>& lplacesAP) {
     vector<int> result;
     MDD mdd=m_lddstate;
 
@@ -41,8 +42,10 @@ vector<int> LDDState::getMarkedPlaces() {
     {
         //printf("mddd : %d \n",mdd);
         mddnode_t node=GETNODE(mdd);
+        if (lplacesAP.find(depth)!=lplacesAP.end())
         if (mddnode_getvalue(node)==1) {
             result.push_back(depth);
+            cout<<"depth "<<depth<<endl;
         }
 
         mdd=mddnode_getdown(node);
@@ -53,3 +56,4 @@ vector<int> LDDState::getMarkedPlaces() {
 }
 
 
+

src/LDDState.h

@@ -4,12 +4,14 @@
 #include <set>
 #include <vector>
 #include <string>
+
 using namespace std;
 using namespace sylvan;
 typedef set<int> Set;
 
 class LDDState {
  public:
+
   LDDState() {
     m_boucle = m_blocage = m_visited = false;
     m_virtual = false;
@@ -35,7 +37,7 @@ class LDDState {
   bool isDiv() {return m_boucle;}
   void setDeadLock(bool de) {m_blocage=de;}
   bool isDeadLock() {return m_blocage;}
-  vector<int> getMarkedPlaces();
+  vector<int> getMarkedPlaces(set<int>& lplacesAP);
 
  protected:
  private:

src/SogKripke.cpp

@@ -51,13 +51,13 @@ bdd SogKripke::state_condition(const spot::state* s) const
   {
    cout<<"yessss "<<endl;
     auto ss = static_cast<const SogKripkeState*>(s);
-    vector<int> marked_place=ss->getLDDState()->getMarkedPlaces();
+    vector<int> marked_place=ss->getLDDState()->getMarkedPlaces(m_sog->getConstructor()->getPlaceProposition());
 
     cout<<"function name :"<<__func__<<endl;
     bdd result=bddtrue;
     for (auto it=marked_place.begin();it!=marked_place.end();it++) {
     string name=m_sog->getPlace(*it);
-    cout<<"Place name marked : "<<*it<<endl;
+    cout<<"Place name marked : "<<*it<<"  "<<name<<endl;
     spot::formula f=spot::formula::ap(name);
     result&=bdd_ithvar((dict_->var_map.find(f))->second);
     }

src/main.cpp

@@ -129,7 +129,7 @@ int main(int argc, char** argv)
         cout<<"number of task = 1 \n " <<endl;
         bool uselace=(!strcmp(argv[1],"lc")) || (!strcmp(argv[1],"l"));
         threadSOG DR(R, bound,nb_th,uselace);
-        LDDGraph g;
+        LDDGraph g(&DR);
 
         if (nb_th==1)
         {
@@ -218,7 +218,7 @@ int main(int argc, char** argv)
             cout<<"**************Hybrid version**************** \n" <<endl;
             HybridSOG DR(R, bound);
 
-            LDDGraph g;
+            LDDGraph g(&DR);
             DR.computeDSOG(g);
         }
         else
@@ -228,7 +228,7 @@ int main(int argc, char** argv)
 
             {
                 DistributedSOG DR(R, bound);
-                LDDGraph g;
+                LDDGraph g(nullptr);
                 DR.computeDSOG(g);
             }