From 3fe4985b5b270c034dccecf8219a7f9b1a9687c1 Mon Sep 17 00:00:00 2001 From: abid <chiheb.abid@gmail.com> Date: Wed, 1 May 2019 23:06:08 +0100 Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?= =?UTF-8?q?=20src/LDDGraph.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20?= =?UTF-8?q?=20=20src/LDDState.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20?= =?UTF-8?q?=20=20=20=20src/LDDState.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20?= =?UTF-8?q?=20=20=20=20=20src/main.cpp?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/LDDGraph.h | 2 ++ src/LDDState.cpp | 24 +++++++++++++++++++++--- src/LDDState.h | 7 +++++-- src/main.cpp | 2 -- 4 files changed, 28 insertions(+), 7 deletions(-) diff --git a/src/LDDGraph.h b/src/LDDGraph.h index 3c1b356..bf174ef 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 6d48091..f81f1a3 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 ba11fba..064b1d6 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 4922e4a..bcba3af 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) { -- GitLab