From 492a2b54b6088f70f23b0b96661bc14a7dfdd4fd Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Sat, 4 May 2019 00:41:28 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/LDDState.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20?=
=?UTF-8?q?=20=20=20src/LDDState.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20?=
=?UTF-8?q?=20=20=20=20src/SogKripke.cpp?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/LDDState.cpp | 21 +++++++++++++++++++++
src/LDDState.h | 1 +
src/SogKripke.cpp | 12 ++++++++----
3 files changed, 30 insertions(+), 4 deletions(-)
diff --git a/src/LDDState.cpp b/src/LDDState.cpp
index 08f95b4..3f2ed91 100644
--- a/src/LDDState.cpp
+++ b/src/LDDState.cpp
@@ -55,5 +55,26 @@ vector<int> LDDState::getMarkedPlaces(set<int>& lplacesAP) {
return result;
}
+vector<int> LDDState::getUnmarkedPlaces(set<int>& lplacesAP) {
+ vector<int> result;
+ MDD mdd=m_lddstate;
+
+ int depth=0;
+ while (mdd>lddmc_true)
+ {
+ //printf("mddd : %d \n",mdd);
+ mddnode_t node=GETNODE(mdd);
+ if (lplacesAP.find(depth)!=lplacesAP.end())
+ if (mddnode_getvalue(node)==0) {
+ result.push_back(depth);
+ cout<<"depth "<<depth<<endl;
+ }
+
+ mdd=mddnode_getdown(node);
+ depth++;
+
+ }
+ return result;
+}
diff --git a/src/LDDState.h b/src/LDDState.h
index 0725802..7f444c6 100755
--- a/src/LDDState.h
+++ b/src/LDDState.h
@@ -38,6 +38,7 @@ class LDDState {
void setDeadLock(bool de) {m_blocage=de;}
bool isDeadLock() {return m_blocage;}
vector<int> getMarkedPlaces(set<int>& lplacesAP);
+ vector<int> getUnmarkedPlaces(set<int>& lplacesAP);
protected:
private:
diff --git a/src/SogKripke.cpp b/src/SogKripke.cpp
index db484e9..d2dffaa 100644
--- a/src/SogKripke.cpp
+++ b/src/SogKripke.cpp
@@ -56,14 +56,18 @@ bdd SogKripke::state_condition(const spot::state* s) const
bdd result=bddtrue;
+ // Marked places
for (auto it=marked_place.begin();it!=marked_place.end();it++) {
string name=m_sog->getPlace(*it);
- //cout<<"Place name marked : "<<" "<<name<<endl;
spot::formula f=spot::formula::ap(name);
- result=bdd_ithvar((dict_->var_map.find(f))->second);
- cout<<"verified ldd : "<<ss->getLDDState()->getLDDValue()<<"Place name marked : "<<name<<endl;
+ result&=bdd_ithvar((dict_->var_map.find(f))->second);
+ }
+ vector<int> unmarked_place=ss->getLDDState()->getUnmarkedPlaces(m_sog->getConstructor()->getPlaceProposition());
+ for (auto it=unmarked_place.begin();it!=unmarked_place.end();it++) {
+ string name=m_sog->getPlace(*it);
+ spot::formula f=spot::formula::ap(name);
+ result&=!bdd_ithvar((dict_->var_map.find(f))->second);
}
-
return result;
}
--
GitLab