From c2d380651279903d74e32fdaa4261b02530c37ea Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Mon, 27 May 2019 23:50:58 +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?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/ModelCheckLace.cpp | 41 +++++++++++++++++++++++++++++++++++++++++
1 file changed, 41 insertions(+)
diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp
index 2cf50d1..69d802d 100644
--- a/src/ModelCheckLace.cpp
+++ b/src/ModelCheckLace.cpp
@@ -214,6 +214,47 @@ void ModelCheckLace::buildSucc(LDDState *agregate)
{
if (!agregate->isVisited()) {
// It's first time to visit agregate, then we have to build its successors
+ LDDState *reached_class=nullptr;
+ LACE_ME;
+ MDD meta_state(CALL(Aggregate_epsilon_lace,agregate->getLDDValue(),&m_nonObservable,&m_tb_relation));
+
+ Set fire=fire_obs_lace(meta_state,&m_observable,&m_tb_relation);
+ unsigned int onb_it=0;
+ Set::const_iterator iter=fire.begin();
+ while(iter!=fire.end())
+ {
+ int t = *iter;
+ SPAWN(Aggregate_epsilon_lace,get_successor(meta_state,t),&m_nonObservable,&m_tb_relation);
+ onb_it++;iter++;
+ }
+
+ for (unsigned int i=0; i<onb_it; i++)
+ {
+ Set::iterator it = fire.end();
+ it--;
+ int t=*it;
+ fire.erase(it);
+ MDD Complete_meta_state=SYNC(Aggregate_epsilon_lace);
+ reached_class=new LDDState;
+ reached_class->m_lddstate=Complete_meta_state;
+ LDDState* pos=m_graph->find(reached_class);
+
+ if(!pos)
+ {
+ m_graph->addArc();
+ m_graph->insert(reached_class);
+ agregate->Successors.insert(agregate->Successors.begin(),LDDEdge(reached_class,t));
+ reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(agregate,t));
+
+ }
+ else
+ {
+ m_graph->addArc();
+ agregate->Successors.insert(agregate->Successors.begin(),LDDEdge(pos,t));
+ pos->Predecessors.insert(pos->Predecessors.begin(),LDDEdge(agregate,t));
+ delete reached_class;
+ }
+ }
}
--
GitLab