diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp
index a373ab99083c86dde82b93239095d2895e778071..6b570d2a5446aeb66b4e0378194613e26980bd83 100644
--- a/src/CommonSOG.cpp
+++ b/src/CommonSOG.cpp
@@ -175,15 +175,17 @@ unsigned int CommonSOG::getPlacesCount() {
/**** Detect divergence in an agregate ****/
bool CommonSOG::Set_Div(MDD &M) const
{
+
if (m_nonObservable.empty())
return false;
Set::const_iterator i;
MDD Reached,From;
//cout<<"Ici detect divergence \n";
- Reached=M;
+ Reached=lddmc_false;
+ From=M;
do
{
- From=Reached;
+
for(i=m_nonObservable.begin();!(i==m_nonObservable.end());i++)
{
@@ -191,10 +193,13 @@ bool CommonSOG::Set_Div(MDD &M) const
Reached=lddmc_union_mono(Reached,To);
//Reached=To;
}
+
if(Reached==From) return true;
+ From=Reached;
+ Reached=lddmc_false;
- }while(Reached!=lddmc_false && Reached != From);
- // cout<<"PAS DE SEQUENCE DIVERGENTE \n";
+ } while(Reached!=lddmc_false && Reached != lddmc_true);
+
return false;
}
diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp
index 301fb01cbf7f1734a19ca381ba7c7161cd28598a..41d109531b4c1a82ee5afcd23a2d9d9ad36de7b8 100644
--- a/src/ModelCheckLace.cpp
+++ b/src/ModelCheckLace.cpp
@@ -34,22 +34,19 @@ void ModelCheckLace::preConfigure() {
m_transitionName=m_net.transitionName;
m_placeName=m_net.m_placePosName;
- cout<<"Toutes les Transitions:"<<endl;
+ /* cout<<"Toutes les Transitions:"<<endl;
map<string,int>::iterator it2=m_transitionName.begin();
for (; it2!=m_transitionName.end(); it2++)
{
cout<<(*it2).first<<" : "<<(*it2).second<<endl;
- }
-
-
-
- cout<<"Transitions observables :"<<endl;
+ }*/
+ //cout<<"Transitions observables :"<<endl;
Set::iterator it=m_observable.begin();
- for (; it!=m_observable.end(); it++)
+ /*for (; it!=m_observable.end(); it++)
{
cout<<*it<<" ";
}
- cout<<endl;
+ cout<<endl;*/
InterfaceTrans=m_net.InterfaceTrans;
cout<<"Nombre de places : "<<m_nbPlaces<<endl;
@@ -156,6 +153,41 @@ TASK_3 (Set, fire_obs_lace,MDD, State, Set*, observable, vector<TransSylvan>*, t
#define fire_obs_lace(state,obser,tb) CALL(fire_obs_lace, state, obser,tb)
+/// Compute divergence
+
+TASK_3 (bool, SetDivL, MDD, M, Set*, nonObservable, vector<TransSylvan>*, tb_relation)
+{
+
+ if (nonObservable->empty()) return false;
+ Set::iterator i;
+ MDD Reached,From;
+ //cout<<"Ici detect divergence \n";
+ Reached=lddmc_false;
+ From=M;
+ do
+ {
+
+ for(i=nonObservable->begin();!(i==nonObservable->end());i++)
+ SPAWN(lddmc_firing_lace,From,(*tb_relation)[(*i)].getMinus(),(*tb_relation)[(*i)].getPlus());
+
+
+ for(i=nonObservable->begin();!(i==nonObservable->end());i++)
+ {
+ MDD To=SYNC(lddmc_firing_lace);
+ Reached=lddmc_union(Reached,To);
+ }
+ if(Reached==From) return true;
+ From=Reached;
+ Reached=lddmc_false;
+
+ } while(Reached!=lddmc_false && Reached != lddmc_true);
+
+ return false;
+}
+
+#define SetDivL(M, nonObservable,tb) CALL(SetDivL, M, nonObservable,tb)
+
+
LDDState * ModelCheckLace::getInitialMetaState()
{
@@ -170,6 +202,7 @@ LDDState * ModelCheckLace::getInitialMetaState()
initalAggregate->setVisited();
m_graph->setInitialState(initalAggregate);
m_graph->insert(initalAggregate);
+ initalAggregate->setDiv(SetDivL(initial_meta_state,&m_nonObservable,&m_tb_relation));
// Compute successors
unsigned int onb_it=0;
Set::const_iterator iter=fire.begin();
@@ -191,6 +224,7 @@ LDDState * ModelCheckLace::getInitialMetaState()
MDD Complete_meta_state=SYNC(Aggregate_epsilon_lace);
reached_class=new LDDState;
reached_class->m_lddstate=Complete_meta_state;
+ reached_class->setDiv(SetDivL(Complete_meta_state,&m_nonObservable,&m_tb_relation));
m_graph->addArc();
m_graph->insert(reached_class);
initalAggregate->Successors.insert(initalAggregate->Successors.begin(),LDDEdge(reached_class,t));
@@ -233,6 +267,7 @@ void ModelCheckLace::buildSucc(LDDState *agregate)
if(!pos)
{
+ reached_class->setDiv(SetDivL(Complete_meta_state,&m_nonObservable,&m_tb_relation));
m_graph->addArc();
m_graph->insert(reached_class);
agregate->Successors.insert(agregate->Successors.begin(),LDDEdge(reached_class,t));
@@ -254,3 +289,6 @@ void ModelCheckLace::buildSucc(LDDState *agregate)
}
+
+
+
diff --git a/src/ModelCheckLace.h b/src/ModelCheckLace.h
index f418a7eb6e428d7cf0bb6b8d2efa91ea6486b28a..e77ee3997bc9f74e6d0da62ee3f64a9c9fc9331a 100644
--- a/src/ModelCheckLace.h
+++ b/src/ModelCheckLace.h
@@ -11,3 +11,4 @@ private:
};
#endif
+
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index 56a589519435b7496cad517de9445f07d9f2198e..55a4d37dbd7afff1d49b9f129aa9b8a151709d61 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -98,6 +98,7 @@ void ModelCheckerTh::preConfigure()
}
delete [] prec;
delete [] postc;
+ ComputeTh_Succ();
}
@@ -107,11 +108,14 @@ void ModelCheckerTh::preConfigure()
LDDState * ModelCheckerTh::getInitialMetaState()
{
- ComputeTh_Succ();
+ cout<<"**********************************"<<endl;
+
while (!m_finish_initial);
- LDDState *initial_metastate=m_graph->getInitialState();
- while (!initial_metastate->isCompletedSucc());
- initial_metastate->setVisited();
+ LDDState *initial_metastate=m_graph->getInitialState();
+ if (!initial_metastate->isVisited()) {
+ initial_metastate->setVisited();
+ while (!initial_metastate->isCompletedSucc());
+ }
return initial_metastate;
}
@@ -156,11 +160,8 @@ void * ModelCheckerTh::Compute_successors()
}
LDDState* reached_class;
-
-
do
{
-
while (!m_st[id_thread].empty())
{
m_terminaison[id_thread]=false;
@@ -267,13 +268,9 @@ void * ModelCheckerTh::Compute_successors()
}
- while (isNotTerminated());
-
-
-
-
-
-
+ while (isNotTerminated() && !m_finish);
+ cout<<"Thread id :"<<id_thread<<endl;
+ pthread_barrier_wait(&m_barrier_builder);
}
@@ -298,8 +295,8 @@ void ModelCheckerTh::ComputeTh_Succ()
pthread_mutex_init(&m_gc_mutex,NULL);
pthread_mutex_init(&m_graph_mutex,NULL);
pthread_mutex_init(&m_supervise_gc_mutex,NULL);
- /* pthread_barrier_init(&m_barrier_threads, NULL, m_nb_thread+1);
- pthread_barrier_init(&m_barrier_builder, NULL, m_nb_thread+1);*/
+ /* pthread_barrier_init(&m_barrier_threads, NULL, m_nb_thread+1);*/
+ pthread_barrier_init(&m_barrier_builder, NULL, m_nb_thread+1);
for (int i=0; i<m_nb_thread; i++)
{
@@ -318,21 +315,14 @@ void ModelCheckerTh::ComputeTh_Succ()
cout<<"error: pthread_create, rc: "<<rc<<endl;
}
}
- /* Compute_successors();
- for (int i = 0; i < m_nb_thread-1; i++)
- {
- pthread_join(m_list_thread[i], NULL);
- }*/
-
-
}
+
ModelCheckerTh::~ModelCheckerTh() {
m_finish=true;
- /* pthread_barrier_wait(&m_barrier_threads);
- pthread_barrier_wait(&m_barrier_builder); */
+ cout<<__func__<<endl;
+ pthread_barrier_wait(&m_barrier_builder);
for (int i = 0; i < m_nb_thread; i++)
- {
- cout<<"thread "<<i<<endl;
+ {
pthread_join(m_list_thread[i], NULL);
}
diff --git a/src/ModelCheckerTh.h b/src/ModelCheckerTh.h
index 8f7c37eaa2e1214a635aa79cc4018536dba30c50..f03025cbf4ea3467bd51b3f1bca45946a5dbc066 100644
--- a/src/ModelCheckerTh.h
+++ b/src/ModelCheckerTh.h
@@ -27,7 +27,7 @@ private:
pthread_mutex_t m_gc_mutex;
pthread_mutex_t m_supervise_gc_mutex;
- //pthread_barrier_t m_barrier_builder;
+ pthread_barrier_t m_barrier_builder;
unsigned int m_gc;
bool m_finish=false;
bool m_finish_initial=false;
diff --git a/src/SogKripkeIteratorTh.cpp b/src/SogKripkeIteratorTh.cpp
index b36577afce581c9fc0d5679f6d476575b8bbb2dc..738556672322410a8a964951f7369063da632b2f 100644
--- a/src/SogKripkeIteratorTh.cpp
+++ b/src/SogKripkeIteratorTh.cpp
@@ -16,7 +16,7 @@ SogKripkeIteratorTh::SogKripkeIteratorTh(const LDDState* lddstate, bdd cnd):m_ld
m_lsucc.push_back(pair<LDDState*,int>(&m_deadlock,-1));
}
if (lddstate->isDiv()) {
- m_lsucc.push_back(pair<LDDState*,int>(m_lddstate,-1));
+ m_lsucc.push_back(pair<LDDState*,int>(&m_div,-1));
}
}
diff --git a/src/SogKripkeTh.cpp b/src/SogKripkeTh.cpp
index 5345637baec86cce711a94744f83fa1b433cdd73..abb36931815f3f210b5fae9bf45c8cb59a7de94d 100644
--- a/src/SogKripkeTh.cpp
+++ b/src/SogKripkeTh.cpp
@@ -16,7 +16,11 @@ SogKripkeTh::SogKripkeTh(const bdd_dict_ptr &dict_ptr,ModelCheckBaseMT *builder)
SogKripkeStateTh::m_builder=builder;
SogKripkeIteratorTh::m_dict_ptr=&dict_ptr;
SogKripkeIteratorTh::m_deadlock.setLDDValue(1);
+ SogKripkeIteratorTh::m_deadlock.setVisited();
+ SogKripkeIteratorTh::m_deadlock.setCompletedSucc();
SogKripkeIteratorTh::m_div.setLDDValue(0);
+ SogKripkeIteratorTh::m_div.setVisited();
+ SogKripkeIteratorTh::m_div.setCompletedSucc();
SogKripkeIteratorTh::m_div.Successors.push_back(pair<LDDState*,int>(&SogKripkeIteratorTh::m_div,-1));
}
diff --git a/src/main.cpp b/src/main.cpp
index d872d70135c318b04449a7e2c3aa19f9485d4091..ae3018bb58085067b0d231212ddbd4a9832f15c0 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -157,7 +157,7 @@ int main(int argc, char** argv)
mcl->loadNet();
auto k =
std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP());
- /* cout<<"Want to save the graph in a dot file ?";
+ /* cout<<"Want to save the graph in a dot file ?";
cin>>c;
if (c=='y')
{
@@ -167,7 +167,7 @@ int main(int argc, char** argv)
file.open(st.c_str(),fstream::out);
spot::print_dot(file, k,"ka");
file.close();
- } */ ;
+ } */ ;
// Performing on the fly Modelchecking
cout<<"Performing on the fly Modelchecking"<<endl;