diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp
index a66b767af1026d21dd65922d6ad4c4721b45c986..db840642b525c32a4627e680b60f078551c4c1c9 100644
--- a/src/ModelCheckLace.cpp
+++ b/src/ModelCheckLace.cpp
@@ -117,12 +117,12 @@ ModelCheckLace::ModelCheckLace(const NewNet &R, int BOUND,int nbThread)
string ModelCheckLace::getTransition(int pos)
{
- m_graph->getTransition(pos);
+ return m_graph->getTransition(pos);
}
string ModelCheckLace::getPlace(int pos)
{
- m_graph->getPlace(pos);
+ return m_graph->getPlace(pos);
}
TASK_3 (MDD, Aggregate_epsilon_lace, MDD, From, Set*, nonObservable, vector<TransSylvan>*, tb_relation)
@@ -169,6 +169,7 @@ TASK_3 (Set, fire_obs_lace,MDD, State, Set*, observable, vector<TransSylvan>*, t
LDDState * ModelCheckLace::buildInitialMetaState()
{
+
LDDState *c=new LDDState;
LDDState *reached_class;
LACE_ME;
@@ -204,6 +205,7 @@ LDDState * ModelCheckLace::buildInitialMetaState()
c->Successors.insert(c->Successors.begin(),LDDEdge(reached_class,t));
reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(c,t));
}
+
return c;
}
diff --git a/src/SogKripkeIterator.cpp b/src/SogKripkeIterator.cpp
index c60d0eae8afbb37110737ca69ec03629016b203e..f7de0915f81eb897c7b40e16ea8c039dbf1779d3 100644
--- a/src/SogKripkeIterator.cpp
+++ b/src/SogKripkeIterator.cpp
@@ -44,6 +44,7 @@ SogKripkeState* SogKripkeIterator::dst() const
bdd SogKripkeIterator::cond() const {
if (m_lsucc.at(m_current_edge).second==-1) return bddtrue;
+
string name=m_graph->getTransition(m_lsucc.at(m_current_edge).second);
//cout<<"Value "<<m_lddstate->getSuccessors()->at(m_current_edge).second<<" Transition name "<<name<<endl;
diff --git a/src/SogKripkeIteratorOTF.cpp b/src/SogKripkeIteratorOTF.cpp
index c2f48285c146f1c55a78e9adafb2acb44f4056fb..12a1081cf50b19e9f1e9a663628bc8ac203930d4 100644
--- a/src/SogKripkeIteratorOTF.cpp
+++ b/src/SogKripkeIteratorOTF.cpp
@@ -6,7 +6,7 @@
SogKripkeIteratorOTF::SogKripkeIteratorOTF(const LDDState* lddstate, bdd cnd):m_lddstate(lddstate), kripke_succ_iterator(cnd)
{
- //vector<pair<LDDState*, int>>
+
m_lddstate->setDiv(true);
for (int i=0;i<m_lddstate->getSuccessors()->size();i++) {
m_lsucc.push_back(m_lddstate->getSuccessors()->at(i));
@@ -17,43 +17,52 @@ SogKripkeIteratorOTF::SogKripkeIteratorOTF(const LDDState* lddstate, bdd cnd):m_
if (lddstate->isDiv()) {
m_lsucc.push_back(pair<LDDState*,int>(m_lddstate,-1));
}
+
}
bool SogKripkeIteratorOTF::first() {
// m_sog->getLDDStateById(m_id)->Successors().
//return m_sog->get_successor()
-
+ cout<<"entering "<<__func__<<endl;
m_current_edge=0;
+ cout<<"exciting "<<__func__<<endl;
return m_lsucc.size()!=0;
+
}
bool SogKripkeIteratorOTF::next() {
-
+ cout<<"entering "<<__func__<<endl;
m_current_edge++;
return m_current_edge<m_lsucc.size();
+
}
bool SogKripkeIteratorOTF::done() const {
-
+cout<<"entring /excit"<<__func__<<endl;
return m_current_edge==m_lsucc.size();
+
}
SogKripkeStateOTF* SogKripkeIteratorOTF::dst() const
{
+ cout<<"enter/excit "<<__func__<<endl;
return new SogKripkeStateOTF(m_lsucc.at(m_current_edge).first);
}
bdd SogKripkeIteratorOTF::cond() const {
+ cout<<"entering "<<__func__<<endl;
if (m_lsucc.at(m_current_edge).second==-1) return bddtrue;
+ cout<<"step 0"<<endl;
string name=m_builder->getTransition(m_lsucc.at(m_current_edge).second);
//cout<<"Value "<<m_lddstate->getSuccessors()->at(m_current_edge).second<<" Transition name "<<name<<endl;
-
+ cout<<"step 1 "<<name<<endl;
spot::bdd_dict *p=m_dict_ptr->get();
+ cout<<"step 2"<<endl;
spot::formula f=spot::formula::ap(name);
bdd result=bdd_ithvar((p->var_map.find(f))->second);
//cout<<"Iterator "<<__func__<<" "<<m_current_edge<<"\n";*/
- //return result;
- return result;
+ cout<<"exciting "<<__func__<<endl;
+ return result & spot::kripke_succ_iterator::cond();
}
/*spot::acc_cond::mark_t SogKripkeIterator::acc() const {
diff --git a/src/SogKripkeOTF.cpp b/src/SogKripkeOTF.cpp
index 61b6348892270de405b3c5ef74c832e94811d9b3..7f3129edffd55d5a3ad1fee55a6d757761ef3cd7 100644
--- a/src/SogKripkeOTF.cpp
+++ b/src/SogKripkeOTF.cpp
@@ -18,30 +18,34 @@ SogKripkeOTF::SogKripkeOTF(const bdd_dict_ptr &dict_ptr,ModelCheckLace *builder)
}
SogKripkeOTF::SogKripkeOTF(const spot::bdd_dict_ptr& dict_ptr,ModelCheckLace *builder,set<string> &l_transap,set<string> &l_placeap):SogKripkeOTF(dict_ptr,builder) {
+
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);
+
}
state* SogKripkeOTF::get_init_state() const {
- //cout<<"Initial state given...\n";
+ cout<<__func__<<endl;
return new SogKripkeStateOTF(m_builder->buildInitialMetaState());//new SpotSogState();
}
// Allows to print state label representing its id
std::string SogKripkeOTF::format_state(const spot::state* s) const
{
+ cout<<__func__<<endl;
auto ss = static_cast<const SogKripkeStateOTF*>(s);
std::ostringstream out;
out << "( " << ss->getLDDState()->getLDDValue() << ")";
- cout << "( " << ss->getLDDState()->getLDDValue() << ")";
+ cout << " ( " << ss->getLDDState()->getLDDValue() << ")";
return out.str();
}
SogKripkeIteratorOTF* SogKripkeOTF::succ_iter(const spot::state* s) const {
+ cout<<__func__<<endl;
auto ss = static_cast<const SogKripkeStateOTF*>(s);
//////////////////////////////////////////////
@@ -69,6 +73,7 @@ bdd SogKripkeOTF::state_condition(const spot::state* s) const
spot::formula f=spot::formula::ap(name);
result&=!bdd_ithvar((dict_->var_map.find(f))->second);
}
+
return result;
}
diff --git a/src/SpotSogIterator.cpp b/src/SpotSogIterator.cpp
index 8d3ba3f18a99cbb23e9da527a92cb60893122882..62b14d346834652a355a888de088864cfbe32862 100644
--- a/src/SpotSogIterator.cpp
+++ b/src/SpotSogIterator.cpp
@@ -7,6 +7,7 @@
SpotSogIterator::SpotSogIterator(const LDDState* lddstate):m_lddstate(lddstate)
{
//vector<pair<LDDState*, int>>
+
m_lddstate->setDiv(true);
for (int i=0;i<m_lddstate->getSuccessors()->size();i++) {
m_lsucc.push_back(m_lddstate->getSuccessors()->at(i));
diff --git a/src/main.cpp b/src/main.cpp
index 434f3e0e6237d9227816ae8dbdabc65d7a4cb1a2..3d07fc7d87967027d48600c61e7eb8e811a5925a 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -147,10 +147,13 @@ int main(int argc, char** argv)
}
// Initialize SOG builder
ModelCheckLace* mcl=new ModelCheckLace(R,bound,nb_th);
+ cout<<"Created"<<endl;
spot::twa_graph_ptr k =
spot::make_twa_graph(std::make_shared<SogKripkeOTF>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()),
spot::twa::prop_set::all(), true);
// Performing on the fly Modelchecking
+ cout<<"Performing on the fly Modelchecking"<<endl;
+ exit(0);
}
else if (n_tasks==1)
{