diff --git a/src/CommonSOG.h b/src/CommonSOG.h index a6c165719f7c47a3d2414e15e507f604ff76f5b7..94dedf57682fc5963ef824aae33eb86b608487f6 100644 --- a/src/CommonSOG.h +++ b/src/CommonSOG.h @@ -1,13 +1,16 @@ #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; diff --git a/src/LDDGraph.h b/src/LDDGraph.h index 9bb00fa8856afa14625b0832a78dd83be4227ee7..9c027cece4d3916bc6f2efa970029fd2ed5a7795 100755 --- a/src/LDDGraph.h +++ b/src/LDDGraph.h @@ -1,21 +1,25 @@ #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(); diff --git a/src/LDDState.cpp b/src/LDDState.cpp index feced7a72c97669549344c84b391014930b7f11e..08f95b4f339dd588f3035532e2d92fd9d7447145 100644 --- a/src/LDDState.cpp +++ b/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() { } + diff --git a/src/LDDState.h b/src/LDDState.h index 064b1d6641b69369e5a629df30235cb43931c48e..072580291bb3b0088fca9f7811e5103274585939 100755 --- a/src/LDDState.h +++ b/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: diff --git a/src/SogKripke.cpp b/src/SogKripke.cpp index 439b3e738b155c0cec8be420fbd73ebcaa2e759d..4d5c0713e07d9f10975e2de20cc61e87a27cf60c 100644 --- a/src/SogKripke.cpp +++ b/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); } diff --git a/src/main.cpp b/src/main.cpp index 9fdac55de51ea1b160478caa9031b54131337c87..7378758bbba56dce7472c6b21c7f33158b354e78 100644 --- a/src/main.cpp +++ b/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); }