From 7f2db1d3a4d3b5da5ac7bfdc080bd489a6039d9b Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Thu, 2 May 2019 23:40:26 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/HybridSOG.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20?=
=?UTF-8?q?=20=20=20src/LDDState.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20?=
=?UTF-8?q?=20=20=20=20=20src/NewNet.h=20=09modifi=C3=A9=C2=A0:=20=20=20?=
=?UTF-8?q?=20=20=20=20=20=20src/SogKripke.cpp=20=09modifi=C3=A9=C2=A0:=20?=
=?UTF-8?q?=20=20=20=20=20=20=20=20src/threadSOG.cpp?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/HybridSOG.cpp | 1 +
src/LDDState.cpp | 3 ++-
src/NewNet.h | 3 ++-
src/SogKripke.cpp | 13 ++++++-------
src/threadSOG.cpp | 6 ++++--
5 files changed, 15 insertions(+), 11 deletions(-)
diff --git a/src/HybridSOG.cpp b/src/HybridSOG.cpp
index 8ca3114..ae14cc8 100644
--- a/src/HybridSOG.cpp
+++ b/src/HybridSOG.cpp
@@ -78,6 +78,7 @@ HybridSOG::HybridSOG(const NewNet &R, int BOUND,bool init)
m_nonObservable=R.NonObservable;
m_place_proposition=R.m_formula_place;
m_transitionName=R.transitionName;
+ m_placeName=R.m_placePosName;
InterfaceTrans=R.InterfaceTrans;
m_nbPlaces=R.places.size();
diff --git a/src/LDDState.cpp b/src/LDDState.cpp
index f81f1a3..feced7a 100644
--- a/src/LDDState.cpp
+++ b/src/LDDState.cpp
@@ -39,7 +39,8 @@ vector<int> LDDState::getMarkedPlaces() {
int depth=0;
while (mdd>lddmc_true)
{
- mddnode_t node=GETNODE(m_lddstate);
+ //printf("mddd : %d \n",mdd);
+ mddnode_t node=GETNODE(mdd);
if (mddnode_getvalue(node)==1) {
result.push_back(depth);
}
diff --git a/src/NewNet.h b/src/NewNet.h
index a1f269f..a4f2536 100644
--- a/src/NewNet.h
+++ b/src/NewNet.h
@@ -106,9 +106,10 @@ class NewNet : public RdPMonteur {
int nbTransition() const { return transitions.size(); };
set<string>& getListTransitionAP() {return m_ltransitionAP;}
set<string>& getListPlaceAP() {return m_lplaceAP;}
+ map<int,string> m_placePosName;
private:
map<int,string> m_transitionPosName;
- map<int,string> m_placePosName;
+
set<string> m_ltransitionAP;
set<string> m_lplaceAP;
diff --git a/src/SogKripke.cpp b/src/SogKripke.cpp
index 6182a15..439b3e7 100644
--- a/src/SogKripke.cpp
+++ b/src/SogKripke.cpp
@@ -43,22 +43,21 @@ SogKripkeIterator* SogKripke::succ_iter(const spot::state* s) const {
auto ss = static_cast<const SogKripkeState*>(s);
//////////////////////////////////////////////
- // Must be changed
- // State condition ????
- ///////////////////////
- bdd b=bddtrue;
- return new SogKripkeIterator(ss->getLDDState(),b);//,b);//s state_condition(ss));
+
+ return new SogKripkeIterator(ss->getLDDState(),state_condition(ss));//,b);//s state_condition(ss));
}
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();
- spot::formula f=spot::formula::ap("jhkh");
- //dict_->var_map.find(f);
+
+ 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;
spot::formula f=spot::formula::ap(name);
result&=bdd_ithvar((dict_->var_map.find(f))->second);
}
diff --git a/src/threadSOG.cpp b/src/threadSOG.cpp
index 047dd30..a281b20 100644
--- a/src/threadSOG.cpp
+++ b/src/threadSOG.cpp
@@ -63,6 +63,7 @@ threadSOG::threadSOG(const NewNet &R, int BOUND, int nbThread,bool uselace,bool
m_nonObservable=R.NonObservable;
m_transitionName=R.transitionName;
+ m_placeName=R.m_placePosName;
cout<<"Toutes les Transitions:"<<endl;
map<string,int>::iterator it2=m_transitionName.begin();
@@ -624,7 +625,7 @@ void threadSOG::computeDSOG(LDDGraph &g,bool canonised)
int rc;
m_graph=&g;
m_graph->setTransition(m_transitionName);
-
+ m_graph->setPlace(m_placeName);
m_id_thread=0;
pthread_mutex_init(&m_mutex, NULL);
@@ -777,6 +778,7 @@ void threadSOG::computeSOGLace(LDDGraph &g)
Set fire;
m_graph=&g;
m_graph->setTransition(m_transitionName);
+ m_graph->setPlace(m_placeName);
m_nbmetastate=0;
m_MaxIntBdd=0;
@@ -965,7 +967,7 @@ void threadSOG::computeSOGLaceCanonized(LDDGraph &g)
Set fire;
m_graph=&g;
m_graph->setTransition(m_transitionName);
-
+ m_graph->setPlace(m_placeName);
m_nbmetastate=0;
m_MaxIntBdd=0;
--
GitLab