From ad29696fa8d8d248df4f40805bd01a7f7ad9dbba Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Wed, 29 May 2019 11:07:16 +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/SogKripkeIteratorOTF.cpp=20=09modifi=C3=A9?=
=?UTF-8?q?=C2=A0:=20=20=20=20=20=20=20=20=20src/SogKripkeOTF.cpp=20=09mod?=
=?UTF-8?q?ifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/main.cpp?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/ModelCheckLace.cpp | 13 +++++++------
src/SogKripkeIteratorOTF.cpp | 15 +++++++--------
src/SogKripkeOTF.cpp | 2 +-
src/main.cpp | 5 +++--
4 files changed, 18 insertions(+), 17 deletions(-)
diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp
index db84064..db8c87a 100644
--- a/src/ModelCheckLace.cpp
+++ b/src/ModelCheckLace.cpp
@@ -170,15 +170,16 @@ TASK_3 (Set, fire_obs_lace,MDD, State, Set*, observable, vector<TransSylvan>*, t
LDDState * ModelCheckLace::buildInitialMetaState()
{
- LDDState *c=new LDDState;
+ LDDState *initalAggregate=new LDDState;
LDDState *reached_class;
LACE_ME;
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);
+ initalAggregate->m_lddstate=initial_meta_state;
+ m_graph->setInitialState(initalAggregate);
+ m_graph->insert(initalAggregate);
// Compute successors
unsigned int onb_it=0;
Set::const_iterator iter=fire.begin();
@@ -202,11 +203,11 @@ LDDState * ModelCheckLace::buildInitialMetaState()
reached_class->m_lddstate=Complete_meta_state;
m_graph->addArc();
m_graph->insert(reached_class);
- c->Successors.insert(c->Successors.begin(),LDDEdge(reached_class,t));
- reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(c,t));
+ initalAggregate->Successors.insert(initalAggregate->Successors.begin(),LDDEdge(reached_class,t));
+ reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(initalAggregate,t));
}
- return c;
+ return initalAggregate;
}
void ModelCheckLace::buildSucc(LDDState *agregate)
diff --git a/src/SogKripkeIteratorOTF.cpp b/src/SogKripkeIteratorOTF.cpp
index 12a1081..3c2ba89 100644
--- a/src/SogKripkeIteratorOTF.cpp
+++ b/src/SogKripkeIteratorOTF.cpp
@@ -30,38 +30,37 @@ bool SogKripkeIteratorOTF::first() {
}
bool SogKripkeIteratorOTF::next() {
- cout<<"entering "<<__func__<<endl;
+ //cout<<"entering "<<__func__<<endl;
m_current_edge++;
return m_current_edge<m_lsucc.size();
}
bool SogKripkeIteratorOTF::done() const {
-cout<<"entring /excit"<<__func__<<endl;
+ //cout<<"entring /excit"<<__func__<<endl;
return m_current_edge==m_lsucc.size();
}
SogKripkeStateOTF* SogKripkeIteratorOTF::dst() const
{
- cout<<"enter/excit "<<__func__<<endl;
+ //out<<"enter/excit "<<__func__<<endl;
return new SogKripkeStateOTF(m_lsucc.at(m_current_edge).first);
}
bdd SogKripkeIteratorOTF::cond() const {
- cout<<"entering "<<__func__<<endl;
+ //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";*/
- cout<<"exciting "<<__func__<<endl;
+ //cout<<"exciting "<<__func__<<endl;
return result & spot::kripke_succ_iterator::cond();
}
diff --git a/src/SogKripkeOTF.cpp b/src/SogKripkeOTF.cpp
index 7f3129e..3bc8c85 100644
--- a/src/SogKripkeOTF.cpp
+++ b/src/SogKripkeOTF.cpp
@@ -29,7 +29,7 @@ SogKripkeOTF::SogKripkeOTF(const spot::bdd_dict_ptr& dict_ptr,ModelCheckLace *bu
state* SogKripkeOTF::get_init_state() const {
- cout<<__func__<<endl;
+ // cout<<__func__<<endl;
return new SogKripkeStateOTF(m_builder->buildInitialMetaState());//new SpotSogState();
}
diff --git a/src/main.cpp b/src/main.cpp
index e67360c..4d9e172 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -171,13 +171,14 @@ int main(int argc, char** argv)
run->highlight(5); // 5 is a color number.
fstream file;
file.open("violated.dot",fstream::out);
- cout<<"xxxxxviolatedxxxxxxx"<<endl;
+ cout<<"Property is violated!"<<endl;
+ cout<<"Check the dot file."<<endl;
spot::print_dot(file, k, ".kA");
file.close();
}
else
std::cout << "formula is verified\n";
- // exit(0);
+
}
else if (n_tasks==1)
{
--
GitLab