From 18f57045570ac7cf253c86642a61763ea985da2b Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Thu, 2 May 2019 23:03:12 +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.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20?=
=?UTF-8?q?=20=20=20=20=20src/LDDGraph.h=20=09modifi=C3=A9=C2=A0:=20=20=20?=
=?UTF-8?q?=20=20=20=20=20=20src/NewNet.cpp=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/SogKripke.h=20=09modifi=C3=A9?=
=?UTF-8?q?=C2=A0:=20=20=20=20=20=20=20=20=20src/main.cpp=20=09modifi?=
=?UTF-8?q?=C3=A9=C2=A0:=20=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/CommonSOG.h | 1 +
src/LDDGraph.cpp | 7 +++++++
src/LDDGraph.h | 1 +
src/NewNet.cpp | 2 +-
src/SogKripke.cpp | 23 ++++++++++++++---------
src/SogKripke.h | 2 +-
src/main.cpp | 2 +-
src/threadSOG.cpp | 1 +
8 files changed, 27 insertions(+), 12 deletions(-)
diff --git a/src/CommonSOG.h b/src/CommonSOG.h
index 8ff04f2..a6c1657 100644
--- a/src/CommonSOG.h
+++ b/src/CommonSOG.h
@@ -25,6 +25,7 @@ class CommonSOG
vector<TransSylvan> m_tb_relation;
LDDState m_M0;
map<string, int> m_transitionName;
+ map<int,string> m_placeName;
Set m_observable;
Set m_nonObservable;
Set InterfaceTrans;
diff --git a/src/LDDGraph.cpp b/src/LDDGraph.cpp
index 13a89d3..ddfe473 100644
--- a/src/LDDGraph.cpp
+++ b/src/LDDGraph.cpp
@@ -197,9 +197,16 @@ string LDDGraph::getTransition(int pos) {
return it->first;
}
+string LDDGraph::getPlace(int pos) {
+ return m_places->find(pos)->second;
+}
+
void LDDGraph::setTransition(map<string,int>& list_transitions) {
m_transition=&list_transitions;
}
+void LDDGraph::setPlace(map<int,string>& list_places) {
+ m_places=&list_places;
+}
//void LDDGraph::setTransition(vector<string> list)
diff --git a/src/LDDGraph.h b/src/LDDGraph.h
index bf174ef..9bb00fa 100755
--- a/src/LDDGraph.h
+++ b/src/LDDGraph.h
@@ -18,6 +18,7 @@ class LDDGraph
public:
string getTransition(int pos);
string getPlace(int pos);
+ void setPlace(map<int,string>& list_places);
void setTransition(map<string,int>& list_transitions);
MetaLDDNodes m_GONodes;
LDDState *getLDDStateById(unsigned int id);
diff --git a/src/NewNet.cpp b/src/NewNet.cpp
index 67939da..66bf51c 100644
--- a/src/NewNet.cpp
+++ b/src/NewNet.cpp
@@ -187,7 +187,7 @@ void NewNet::setListObservable(const set<string> & list_t)
if (pi!=placeName.end())
cout<<"Place was found!"<<endl;
m_formula_place.insert(pi->second);
-
+ m_lplaceAP.insert(*i);
// Adding adjacent transitions of a place as observable transitions
Place p=places.at(pi->second);
for (auto iter=p.post.begin(); iter!=p.post.end(); iter++)
diff --git a/src/SogKripke.cpp b/src/SogKripke.cpp
index 2cc68c6..6182a15 100644
--- a/src/SogKripke.cpp
+++ b/src/SogKripke.cpp
@@ -16,10 +16,12 @@ SogKripke::SogKripke(const bdd_dict_ptr &dict_ptr,LDDGraph *sog): spot::kripke(d
SogKripkeIterator::m_dict_ptr=&dict_ptr;
}
-SogKripke::SogKripke(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog,set<string> &l_transap):SogKripke(dict_ptr,sog) {
+SogKripke::SogKripke(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog,set<string> &l_transap,set<string> &l_placeap):SogKripke(dict_ptr,sog) {
for (auto it=l_transap.begin();it!=l_transap.end();it++) {
register_ap(*it);
}
+ for (auto it=l_placeap.begin();it!=l_placeap.end();it++)
+ register_ap(*it);
}
@@ -50,15 +52,18 @@ SogKripkeIterator* SogKripke::succ_iter(const spot::state* s) const {
bdd SogKripke::state_condition(const spot::state* s) const
{
- /*auto ss = static_cast<const SogKripkeState*>(s);
-
- MDD res = lddmc_true;
- std::map<int, int>::const_iterator it;
- for (it = place_prop.begin(); it != place_prop.end(); ++it)
- if (m_sog->is_marked(it->first, m))
+ 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);
+ bdd result=bddtrue;
+ for (auto it=marked_place.begin();it!=marked_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 res;*/
- return bddtrue;
+ return result;
}
diff --git a/src/SogKripke.h b/src/SogKripke.h
index a2bac01..d4b13c8 100644
--- a/src/SogKripke.h
+++ b/src/SogKripke.h
@@ -9,7 +9,7 @@ class SogKripke: public spot::kripke {
SogKripke(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog);
- SogKripke(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog,set<string> &l_transap);
+ SogKripke(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog,set<string> &l_transap,set<string> &l_placeap);
virtual ~SogKripke();
spot::state* get_init_state() const;
SogKripkeIterator* succ_iter(const spot::state* s) const override;
diff --git a/src/main.cpp b/src/main.cpp
index 5ce1d93..9fdac55 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -189,7 +189,7 @@ int main(int argc, char** argv)
spot::print_dot(file, af);
file.close();
}
- auto k = std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP());
+ auto k = std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP(),R.getListPlaceAP());
cout<<"SOG translated to SPOT succeeded.."<<endl;
cout<<"Want to save the graph in a dot file ?";
cin>>c;
diff --git a/src/threadSOG.cpp b/src/threadSOG.cpp
index 14e820a..047dd30 100644
--- a/src/threadSOG.cpp
+++ b/src/threadSOG.cpp
@@ -624,6 +624,7 @@ void threadSOG::computeDSOG(LDDGraph &g,bool canonised)
int rc;
m_graph=&g;
m_graph->setTransition(m_transitionName);
+
m_id_thread=0;
pthread_mutex_init(&m_mutex, NULL);
--
GitLab