From 022e0647167f5d4d8e25f9d0c041b33b923126e0 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Fri, 3 May 2019 01:11:03 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/CommonSOG.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20?=
=?UTF-8?q?=20=20=20src/LDDGraph.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20?=
=?UTF-8?q?=20=20=20=20src/LDDState.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20?=
=?UTF-8?q?=20=20=20=20=20=20src/LDDState.h=20=09modifi=C3=A9=C2=A0:=20=20?=
=?UTF-8?q?=20=20=20=20=20=20=20src/SogKripke.cpp=20=09modifi=C3=A9=C2=A0:?=
=?UTF-8?q?=20=20=20=20=20=20=20=20=20src/main.cpp?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/CommonSOG.h | 6 +++++-
src/LDDGraph.h | 10 +++++++---
src/LDDState.cpp | 8 ++++++--
src/LDDState.h | 4 +++-
src/SogKripke.cpp | 4 ++--
src/main.cpp | 6 +++---
6 files changed, 26 insertions(+), 12 deletions(-)
diff --git a/src/CommonSOG.h b/src/CommonSOG.h
index a6c1657..94dedf5 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 9bb00fa..9c027ce 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 feced7a..08f95b4 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 064b1d6..0725802 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 439b3e7..4d5c071 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 9fdac55..7378758 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);
}
--
GitLab