From 720a9fa092ec396946b32040ff59d5490c3269c7 Mon Sep 17 00:00:00 2001
From: ouni <ouni@lipn.univ-paris13.fr>
Date: Sun, 28 Apr 2019 17:54:06 +0200
Subject: [PATCH] src

---
 src/CommonSOG.cpp      | 8 ++++++++
 src/CommonSOG.h        | 7 +++++--
 src/DistributedSOG.cpp | 2 +-
 src/DistributedSOG.h   | 4 ++--
 src/HybridSOG.cpp      | 2 +-
 src/HybridSOG.h        | 4 ++--
 src/LDDState.cpp       | 8 ++++++++
 src/LDDState.h         | 3 +++
 src/threadSOG.cpp      | 2 +-
 src/threadSOG.h        | 4 ++--
 10 files changed, 33 insertions(+), 11 deletions(-)

diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp
index 410d9d5..023a9ae 100644
--- a/src/CommonSOG.cpp
+++ b/src/CommonSOG.cpp
@@ -213,3 +213,11 @@ return ((M&cur)!=lddmc_false);
 	//BLOCAGE
 }
 
+/**************** isMarked **************/
+bool CommonSOG::is_marked(int p, const MDD& m) const {
+  if(0 <= p && p < m_place_proposition.size());
+  return
+  else
+  return false;
+}
+
diff --git a/src/CommonSOG.h b/src/CommonSOG.h
index 8ff04f2..b97e0f0 100644
--- a/src/CommonSOG.h
+++ b/src/CommonSOG.h
@@ -2,7 +2,7 @@
 #define COMMONSOG_H
 #include "LDDGraph.h"
 #include "TransSylvan.h"
-#include "NewNet.h"
+#include "Net.hpp"
 #include <stack>
 
 typedef pair<LDDState *, MDD> couple;
@@ -19,7 +19,7 @@ class CommonSOG
         Set * getNonObservable();
         unsigned int getPlacesCount();
     protected:
-        NewNet m_net;
+        net m_net;
         int m_nbPlaces = 0;
         LDDGraph *m_graph;
         vector<TransSylvan> m_tb_relation;
@@ -39,6 +39,9 @@ class CommonSOG
         MDD Canonize(MDD s, unsigned int level);
         bool Set_Div(MDD &M) const;
         bool Set_Bloc(MDD &M) const;
+        bool is_marked(int p, const MDD & m) const;
+
+
     private:
 };
 
diff --git a/src/DistributedSOG.cpp b/src/DistributedSOG.cpp
index 3c5a77c..fa06503 100644
--- a/src/DistributedSOG.cpp
+++ b/src/DistributedSOG.cpp
@@ -25,7 +25,7 @@ using namespace sylvan;
 /**************************************************/
 
 
-DistributedSOG::DistributedSOG(const NewNet &R, int BOUND,bool init)
+DistributedSOG::DistributedSOG(const net &R, int BOUND,bool init)
 {
 
 
diff --git a/src/DistributedSOG.h b/src/DistributedSOG.h
index d608110..f10880f 100644
--- a/src/DistributedSOG.h
+++ b/src/DistributedSOG.h
@@ -3,7 +3,7 @@
 // #include "RdPBDD.h"
 #include <stack>
 #include <vector>
-#include "NewNet.h"
+#include "Net.hpp"
 // #include "MDD.h"
 //#include "MDGraph.h"
 //#include "bvec.h"
@@ -46,7 +46,7 @@ extern int n_tasks, task_id;
 // typedef vector<Trans> vec_trans;
 class DistributedSOG : public CommonSOG{
  public:
-  DistributedSOG(const NewNet &, int BOUND = 32, bool init = false);
+  DistributedSOG(const net &, int BOUND = 32, bool init = false);
   void buildFromNet(int index);
   void computeDSOG(LDDGraph &g);
   void BuildInitialState(LDDState *m_state, MDD mdd);
diff --git a/src/HybridSOG.cpp b/src/HybridSOG.cpp
index 8ca3114..b9126a3 100644
--- a/src/HybridSOG.cpp
+++ b/src/HybridSOG.cpp
@@ -50,7 +50,7 @@ using namespace sylvan;
 } */
 
 
-HybridSOG::HybridSOG(const NewNet &R, int BOUND,bool init)
+HybridSOG::HybridSOG(const net &R, int BOUND,bool init)
 {
 
 
diff --git a/src/HybridSOG.h b/src/HybridSOG.h
index f480981..6511d11 100644
--- a/src/HybridSOG.h
+++ b/src/HybridSOG.h
@@ -3,7 +3,7 @@
 
 #include <stack>
 #include <vector>
-#include "NewNet.h"
+#include "Net.hpp"
 // #include "MDD.h"
 //#include "MDGraph.h"
 //#include "bvec.h"
@@ -47,7 +47,7 @@ typedef stack<MSG> pile_msg;
 class HybridSOG : public CommonSOG
 {
 public:
-    HybridSOG(const NewNet &, int BOUND = 32, bool init = false);
+    HybridSOG(const net &, int BOUND = 32, bool init = false);
     void buildFromNet(int index);
     /// principal functions to construct the SOG
     void computeDSOG(LDDGraph &g);
diff --git a/src/LDDState.cpp b/src/LDDState.cpp
index a6f372b..afd70ba 100644
--- a/src/LDDState.cpp
+++ b/src/LDDState.cpp
@@ -28,3 +28,11 @@ void LDDState::setVirtual() {
 vector<pair<LDDState*, int>>* LDDState::getSuccessors() {
     return &Successors;
 }
+
+void LDDState::setMarked() {
+    isMarked()=true;
+}
+
+bool LDDState::isMarked() {
+    return m_marked;
+}
diff --git a/src/LDDState.h b/src/LDDState.h
index 4337d85..4447b7f 100755
--- a/src/LDDState.h
+++ b/src/LDDState.h
@@ -12,6 +12,7 @@ class LDDState {
   LDDState() {
     m_boucle = m_blocage = m_visited = false;
     m_virtual = false;
+    m_marked = false;
   }
   virtual ~LDDState();
   Set firable;
@@ -33,6 +34,8 @@ class LDDState {
   bool isDiv() {return m_boucle;}
   void setDeadLock(bool de) {m_blocage=de;}
   bool isDeadLock() {return m_blocage;}
+  bool isMarked();
+  void setMarked();
  protected:
  private:
   bool m_virtual = false;
diff --git a/src/threadSOG.cpp b/src/threadSOG.cpp
index 917a54c..665f8c7 100644
--- a/src/threadSOG.cpp
+++ b/src/threadSOG.cpp
@@ -26,7 +26,7 @@ void write_to_dot(const char *ch,MDD m)
 
 /*************************************************/
 
-threadSOG::threadSOG(const NewNet &R, int BOUND, int nbThread,bool uselace,bool init)
+threadSOG::threadSOG(const net &R, int BOUND, int nbThread,bool uselace,bool init)
 {
     m_nb_thread=nbThread;
     if (uselace)  {
diff --git a/src/threadSOG.h b/src/threadSOG.h
index f088074..fc495b2 100644
--- a/src/threadSOG.h
+++ b/src/threadSOG.h
@@ -3,7 +3,7 @@
 // #include "RdPBDD.h"
 #include <stack>
 #include <vector>
-#include "NewNet.h"
+#include "Net.hpp"
 // #include "MDD.h"
 //#include "MDGraph.h"
 //#include "bvec.h"
@@ -23,7 +23,7 @@ extern unsigned int nb_th;
 
 class threadSOG : public CommonSOG{
  public:
-  threadSOG(const NewNet &, int BOUND = 32, int nbThread=2,bool uselace=false,bool init = false);
+  threadSOG(const net &, int BOUND = 32, int nbThread=2,bool uselace=false,bool init = false);
   void buildFromNet(int index);
   void computeDSOG(LDDGraph &g,bool canonised);
   void computeSeqSOG(LDDGraph &g);
-- 
GitLab