From 8206ffd3986b7642af13e5c8c46a417a939832d0 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Mon, 27 May 2019 12:38:14 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/ModelCheckLace.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20?=
=?UTF-8?q?=20=20=20=20=20src/SogKripkeStateOTF.cpp=20=09modifi=C3=A9?=
=?UTF-8?q?=C2=A0:=20=20=20=20=20=20=20=20=20src/SogKripkeStateOTF.h?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/ModelCheckLace.cpp | 12 +++++++-----
src/SogKripkeStateOTF.cpp | 5 +----
src/SogKripkeStateOTF.h | 2 +-
3 files changed, 9 insertions(+), 10 deletions(-)
diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp
index 2df164f..b8eae2a 100644
--- a/src/ModelCheckLace.cpp
+++ b/src/ModelCheckLace.cpp
@@ -126,7 +126,7 @@ string temp;
return temp;
}
-TASK_3 (MDD, Accessible_epsilon_lace, MDD, From, Set*, nonObservable, vector<TransSylvan>*, tb_relation)
+TASK_3 (MDD, Aggregate_epsilon_lace, MDD, From, Set*, nonObservable, vector<TransSylvan>*, tb_relation)
{
MDD M1;
MDD M2=From;
@@ -150,7 +150,7 @@ TASK_3 (MDD, Accessible_epsilon_lace, MDD, From, Set*, nonObservable, vector<Tra
return M2;
}
-TASK_3 (Set, firable_obs_lace,MDD, State, Set*, observable, vector<TransSylvan>*, tb_relation)
+TASK_3 (Set, fire_obs_lace,MDD, State, Set*, observable, vector<TransSylvan>*, tb_relation)
{
Set res;
for(Set::const_iterator i=observable->begin(); !(i==observable->end()); i++)
@@ -166,15 +166,17 @@ TASK_3 (Set, firable_obs_lace,MDD, State, Set*, observable, vector<TransSylvan>*
return res;
}
-#define firable_obs_lace(state,obser,tb) CALL(firable_obs_lace, state, obser,tb)
+#define fire_obs_lace(state,obser,tb) CALL(fire_obs_lace, state, obser,tb)
LDDState * ModelCheckLace::buildInitialMetaState() {
LDDState *c=new LDDState;
LACE_ME;
- MDD initial_meta_state(CALL(Accessible_epsilon_lace,m_initalMarking,&m_nonObservable,&m_tb_relation));
- Set fire=firable_obs_lace(initial_meta_state,&m_observable,&m_tb_relation);
+ MDD initial_meta_state(CALL(Aggregate_epsilon_lace,m_initalMarking,&m_nonObservable,&m_tb_relation));
+ Set fire=fire_obs_lace(initial_meta_state,&m_observable,&m_tb_relation);
// c->m_lddstate=CALL(lddmc_canonize,initial_meta_state,0,*this);
+ m_graph->setInitialState(c);
+ m_graph->insert(c);
return c;
}
diff --git a/src/SogKripkeStateOTF.cpp b/src/SogKripkeStateOTF.cpp
index c86bc26..99b5a51 100644
--- a/src/SogKripkeStateOTF.cpp
+++ b/src/SogKripkeStateOTF.cpp
@@ -7,10 +7,7 @@ SogKripkeStateOTF::~SogKripkeStateOTF()
{
//dtor
}
-SogKripkeStateOTF::SogKripkeStateOTF(const MDD& m)
- : spot::state(), ma(m)
-{
-} //
+
SogKripkeStateOTF* SogKripkeStateOTF::clone() const
diff --git a/src/SogKripkeStateOTF.h b/src/SogKripkeStateOTF.h
index 674ce25..0a50e6e 100644
--- a/src/SogKripkeStateOTF.h
+++ b/src/SogKripkeStateOTF.h
@@ -7,7 +7,7 @@
class SogKripkeStateOTF : public spot::state
{
public:
- SogKripkeStateOTF(const MDD &m);
+ SogKripkeStateOTF(LDDState *st):m_state(st) {};
virtual ~SogKripkeStateOTF();
SogKripkeStateOTF* clone() const override;
--
GitLab