diff --git a/src/LDDGraph.h b/src/LDDGraph.h index 3c1b356dae33d2e4891827dca50c3db89dec2d51..bf174ef4a2a2d8782d543e039560b3ae41387533 100755 --- a/src/LDDGraph.h +++ b/src/LDDGraph.h @@ -12,10 +12,12 @@ class LDDGraph { private: map<string,int>* m_transition; + map<int,string>* m_places; void printGraph(LDDState *, size_t &); public: string getTransition(int pos); + string getPlace(int pos); void setTransition(map<string,int>& list_transitions); MetaLDDNodes m_GONodes; LDDState *getLDDStateById(unsigned int id); diff --git a/src/LDDState.cpp b/src/LDDState.cpp index 6d4809142480528e80de9bfc3a36a865d3bb1329..f81f1a3848ee6a860e167e19352109c9d735da43 100644 --- a/src/LDDState.cpp +++ b/src/LDDState.cpp @@ -1,6 +1,9 @@ -#include "LDDState.h" +#include <sylvan.h> +#include <sylvan_int.h> +#include "LDDState.h" +#define GETNODE(mdd) ((mddnode_t)llmsset_index_to_ptr(nodes, mdd)) LDDState::~LDDState() { //dtor @@ -29,8 +32,23 @@ vector<pair<LDDState*, int>>* LDDState::getSuccessors() { return &Successors; } -void LDDState::setMarked() { - m_marked=true; +vector<int> LDDState::getMarkedPlaces() { + vector<int> result; + MDD mdd=m_lddstate; + + int depth=0; + while (mdd>lddmc_true) + { + mddnode_t node=GETNODE(m_lddstate); + if (mddnode_getvalue(node)==1) { + result.push_back(depth); + } + + mdd=mddnode_getdown(node); + depth++; + + } + return result; } diff --git a/src/LDDState.h b/src/LDDState.h index ba11fbae03a2c133cca4cd908eb9b6c0d34b6956..064b1d6641b69369e5a629df30235cb43931c48e 100755 --- a/src/LDDState.h +++ b/src/LDDState.h @@ -3,6 +3,7 @@ #include <sylvan.h> #include <set> #include <vector> +#include <string> using namespace std; using namespace sylvan; typedef set<int> Set; @@ -27,17 +28,19 @@ 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;} - void setMarked(); + vector<int> getMarkedPlaces(); + protected: private: bool m_virtual = false; + }; typedef pair<LDDState*, int> LDDEdge; diff --git a/src/main.cpp b/src/main.cpp index 4922e4ac340fb910e85055a20c3e665f7411310c..bcba3af558ced24720697c63058845cc458141b8 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -122,8 +122,6 @@ int main(int argc, char** argv) MPI_Comm_size(MPI_COMM_WORLD,&n_tasks); MPI_Comm_rank(MPI_COMM_WORLD,&task_id); - - // if (n_tasks==1) {