diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp
index 41d109531b4c1a82ee5afcd23a2d9d9ad36de7b8..9c8cbabd9f80668d2d97ac6ba93e56181409d02f 100644
--- a/src/ModelCheckLace.cpp
+++ b/src/ModelCheckLace.cpp
@@ -190,8 +190,8 @@ TASK_3 (bool, SetDivL, MDD, M, Set*, nonObservable, vector<TransSylvan>*, tb_rel
LDDState * ModelCheckLace::getInitialMetaState()
{
-
- LDDState *initalAggregate=new LDDState;
+
+ LDDState *initalAggregate=new LDDState();
LDDState *reached_class;
LACE_ME;
MDD initial_meta_state(CALL(Aggregate_epsilon_lace,m_initialMarking,&m_nonObservable,&m_tb_relation));
@@ -202,27 +202,28 @@ LDDState * ModelCheckLace::getInitialMetaState()
initalAggregate->setVisited();
m_graph->setInitialState(initalAggregate);
m_graph->insert(initalAggregate);
+
initalAggregate->setDiv(SetDivL(initial_meta_state,&m_nonObservable,&m_tb_relation));
+ initalAggregate->setDeadLock(Set_Bloc(initial_meta_state));
// Compute successors
unsigned int onb_it=0;
- Set::const_iterator iter=fire.begin();
+ Set::iterator iter=fire.begin();
while(iter!=fire.end())
{
int t = *iter;
-
SPAWN(Aggregate_epsilon_lace,get_successor(initial_meta_state,t),&m_nonObservable,&m_tb_relation);
onb_it++;
iter++;
}
-
+ MDD Complete_meta_state;
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;
+ 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();
@@ -231,18 +232,18 @@ LDDState * ModelCheckLace::getInitialMetaState()
reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(initalAggregate,t));
}
- return initalAggregate;
+ return m_graph->getInitialState();
}
void ModelCheckLace::buildSucc(LDDState *agregate)
{
-
+
if (!agregate->isVisited()) {
// It's first time to visit agregate, then we have to build its successors
agregate->setVisited();
LDDState *reached_class=nullptr;
LACE_ME;
- MDD meta_state(CALL(Aggregate_epsilon_lace,agregate->getLDDValue(),&m_nonObservable,&m_tb_relation));
+ MDD meta_state=agregate->getLDDValue();//(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;
@@ -261,13 +262,14 @@ void ModelCheckLace::buildSucc(LDDState *agregate)
int t=*it;
fire.erase(it);
MDD Complete_meta_state=SYNC(Aggregate_epsilon_lace);
- reached_class=new LDDState;
+ reached_class=new LDDState();
reached_class->m_lddstate=Complete_meta_state;
LDDState* pos=m_graph->find(reached_class);
if(!pos)
{
reached_class->setDiv(SetDivL(Complete_meta_state,&m_nonObservable,&m_tb_relation));
+ reached_class->setDeadLock(Set_Bloc(Complete_meta_state));
m_graph->addArc();
m_graph->insert(reached_class);
agregate->Successors.insert(agregate->Successors.begin(),LDDEdge(reached_class,t));
diff --git a/src/ModelCheckLace.h b/src/ModelCheckLace.h
index e77ee3997bc9f74e6d0da62ee3f64a9c9fc9331a..00437d340f4d1a7642dbadb5593d03904f8fe595 100644
--- a/src/ModelCheckLace.h
+++ b/src/ModelCheckLace.h
@@ -4,8 +4,8 @@
class ModelCheckLace : public ModelCheckBaseMT {
public:
ModelCheckLace(const NewNet &R, int BOUND,int nbThread);
- LDDState * getInitialMetaState();
- void buildSucc(LDDState *agregate);
+ LDDState * getInitialMetaState() override;
+ void buildSucc(LDDState *agregate) override;
private:
void preConfigure();
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index 55a4d37dbd7afff1d49b9f129aa9b8a151709d61..698815dbe32bc89d3a350305ff3b2094848bcbeb 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -108,8 +108,6 @@ void ModelCheckerTh::preConfigure()
LDDState * ModelCheckerTh::getInitialMetaState()
{
- cout<<"**********************************"<<endl;
-
while (!m_finish_initial);
LDDState *initial_metastate=m_graph->getInitialState();
if (!initial_metastate->isVisited()) {
@@ -264,18 +262,13 @@ void * ModelCheckerTh::Compute_successors()
e.first.first->setCompletedSucc();
}
m_terminaison[id_thread]=true;
-
-
-
}
while (isNotTerminated() && !m_finish);
- cout<<"Thread id :"<<id_thread<<endl;
+ //cout<<"Thread id :"<<id_thread<<endl;
pthread_barrier_wait(&m_barrier_builder);
}
-
-
void * ModelCheckerTh::threadHandler(void *context)
{
return ((ModelCheckerTh*)context)->Compute_successors();
@@ -319,7 +312,7 @@ void ModelCheckerTh::ComputeTh_Succ()
ModelCheckerTh::~ModelCheckerTh() {
m_finish=true;
- cout<<__func__<<endl;
+
pthread_barrier_wait(&m_barrier_builder);
for (int i = 0; i < m_nb_thread; i++)
{
diff --git a/src/SogKripkeIteratorTh.cpp b/src/SogKripkeIteratorTh.cpp
index 738556672322410a8a964951f7369063da632b2f..4862d6095e2c762e1cdcd3309099c0ecd265be5a 100644
--- a/src/SogKripkeIteratorTh.cpp
+++ b/src/SogKripkeIteratorTh.cpp
@@ -6,9 +6,6 @@
SogKripkeIteratorTh::SogKripkeIteratorTh(const LDDState* lddstate, bdd cnd):m_lddstate(lddstate), kripke_succ_iterator(cnd)
{
-
- //m_lddstate->setDiv(true);
- //if (m_lddstate->getLDDValue()) m_lddstate->setDeadLock(true);
for (int i=0;i<m_lddstate->getSuccessors()->size();i++) {
m_lsucc.push_back(m_lddstate->getSuccessors()->at(i));
}
@@ -30,7 +27,7 @@ bool SogKripkeIteratorTh::first() {
}
bool SogKripkeIteratorTh::next() {
- //cout<<"entering "<<__func__<<endl;
+ //cout<<"entering "<<__func__<<" "<<m_current_edge<<endl;
m_current_edge++;
return m_current_edge<m_lsucc.size();
@@ -44,7 +41,7 @@ bool SogKripkeIteratorTh::done() const {
SogKripkeStateTh* SogKripkeIteratorTh::dst() const
{
- //cout<<"enter/excit "<<__func__<<endl;
+ /*cout<<"Source "<<m_lddstate->getLDDValue()<<"Destination :"<<m_lsucc.at(m_current_edge).first->getLDDValue()<<" in "<<m_lsucc.size()<<" / "<<m_current_edge<<endl;*/
return new SogKripkeStateTh(m_lsucc.at(m_current_edge).first);
}
@@ -71,6 +68,12 @@ SogKripkeIteratorTh::~SogKripkeIteratorTh()
//dtor
}
+void SogKripkeIteratorTh::recycle(LDDState* aggregate, bdd cond)
+{
+ m_lddstate=aggregate;
+ spot::kripke_succ_iterator::recycle(cond);
+}
+
static ModelCheckBaseMT * SogKripkeIteratorTh::m_builder;
static spot::bdd_dict_ptr* SogKripkeIteratorTh::m_dict_ptr;
static LDDState SogKripkeIteratorTh::m_deadlock;
diff --git a/src/SogKripkeIteratorTh.h b/src/SogKripkeIteratorTh.h
index 938803db2b3cada535326c715773228d9fb4fb4f..c5307b4c2549d541dc53ca7998de158de6258cfb 100644
--- a/src/SogKripkeIteratorTh.h
+++ b/src/SogKripkeIteratorTh.h
@@ -22,11 +22,11 @@ public:
SogKripkeStateTh* current_state() const;
- bdd current_condition() const;
+ void recycle(LDDState *aggregate, bdd cond);
- int current_transition() const;
+ //int current_transition() const;
- bdd current_acceptance_conditions() const;
+ //bdd current_acceptance_conditions() const;
std::string format_transition() const;
diff --git a/src/SogKripkeStateTh.cpp b/src/SogKripkeStateTh.cpp
index 76c38845a939bbf61a9c9ba4c2aca9f92add023a..70712c959c9f31f743b067701b6265b9d27d7b66 100644
--- a/src/SogKripkeStateTh.cpp
+++ b/src/SogKripkeStateTh.cpp
@@ -8,4 +8,4 @@ SogKripkeStateTh::~SogKripkeStateTh()
//dtor
}
-static ModelCheckerTh * SogKripkeStateTh::m_builder;
+static ModelCheckBaseMT * SogKripkeStateTh::m_builder;
diff --git a/src/SogKripkeStateTh.h b/src/SogKripkeStateTh.h
index 48d64ff99e8eab4d4981030c3548ca76976c81ef..f07ab07d4d426b77c3a061d64e6cd3e344de0742 100644
--- a/src/SogKripkeStateTh.h
+++ b/src/SogKripkeStateTh.h
@@ -3,12 +3,12 @@
#include "LDDState.h"
-#include "ModelCheckerTh.h"
+#include "ModelCheckBaseMT.h"
class SogKripkeStateTh : public spot::state
{
public:
- static ModelCheckerTh * m_builder;
+ static ModelCheckBaseMT * m_builder;
SogKripkeStateTh(LDDState *st):m_state(st) {
m_builder->buildSucc(st);
};
@@ -28,6 +28,7 @@ public:
auto o = static_cast<const SogKripkeStateTh*>(other);
size_t oh = o->hash();
size_t h = hash();
+ //return (h!=oh);
if (h < oh)
return -1;
else
diff --git a/src/SogKripkeTh.cpp b/src/SogKripkeTh.cpp
index abb36931815f3f210b5fae9bf45c8cb59a7de94d..d2884fa39a07bac631c69d972b3f35f5c523d1a7 100644
--- a/src/SogKripkeTh.cpp
+++ b/src/SogKripkeTh.cpp
@@ -36,8 +36,8 @@ SogKripkeTh::SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *bu
state* SogKripkeTh::get_init_state() const {
- // cout<<__func__<<endl;
- return new SogKripkeStateTh(m_builder->getInitialMetaState());//new SpotSogState();
+ LDDState *ss=m_builder->getInitialMetaState();
+ return new SogKripkeStateTh(ss);//new SpotSogState();
}
// Allows to print state label representing its id
@@ -52,12 +52,26 @@ std::string SogKripkeTh::format_state(const spot::state* s) const
}
SogKripkeIteratorTh* SogKripkeTh::succ_iter(const spot::state* s) const {
- // cout<<__func__<<endl;
-
+
auto ss = static_cast<const SogKripkeStateTh*>(s);
+ LDDState *aggregate=ss->getLDDState();
+ bdd cond = state_condition(ss);
+ if (iter_cache_)
+ {
+ auto it = static_cast<SogKripkeIteratorTh*>(iter_cache_);
+ iter_cache_ = nullptr; // empty the cache
+ it->recycle(aggregate, cond);
+ return it;
+ }
+ return new SogKripkeIteratorTh(aggregate,cond);
+
+
+
+
+/* auto ss = static_cast<const SogKripkeStateTh*>(s);
//////////////////////////////////////////////
- return new SogKripkeIteratorTh(ss->getLDDState(),state_condition(ss));//,b);//s state_condition(ss));
+ return new SogKripkeIteratorTh(ss->getLDDState(),state_condition(ss));//,b);//s state_condition(ss));*/
}
bdd SogKripkeTh::state_condition(const spot::state* s) const
diff --git a/src/SogKripkeTh.h b/src/SogKripkeTh.h
index 81d27eb07d33c23094447c14b669176e1c44c8d6..46c06ce67e8461050fecebef7082edb3189854e1 100644
--- a/src/SogKripkeTh.h
+++ b/src/SogKripkeTh.h
@@ -13,16 +13,12 @@ class SogKripkeTh: public spot::kripke {
SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder);
SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder,set<string> &l_transap,set<string> &l_placeap);
virtual ~SogKripkeTh();
- spot::state* get_init_state() const;
+ spot::state* get_init_state() const override;
SogKripkeIteratorTh* succ_iter(const spot::state* s) const override;
std::string format_state(const spot::state* s) const override;
bdd state_condition(const spot::state* s) const override;
- /// \brief Get the graph associated to the automaton.
- /* const LDDGraph& get_graph() const {
- return *m_sog;
- }*/
- ModelCheckerTh *m_builder;
+ ModelCheckBaseMT *m_builder;
protected:
diff --git a/src/main.cpp b/src/main.cpp
index ae3018bb58085067b0d231212ddbd4a9832f15c0..adb7c2fa516bc83bb8f412e9bbe78566428225d6 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -154,10 +154,14 @@ int main(int argc, char** argv)
if (!strcmp(argv[1],"otfL")) mcl=new ModelCheckLace(R,bound,nb_th);
else
mcl=new ModelCheckerTh(R,bound,nb_th);
- mcl->loadNet();
+ mcl->loadNet();
+
auto k =
std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP());
- /* cout<<"Want to save the graph in a dot file ?";
+ /* spot::twa_graph_ptr k =
+ spot::make_twa_graph(std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()),
+ spot::twa::prop_set::all(), true);*/
+ /* cout<<"Want to save the graph in a dot file ?";
cin>>c;
if (c=='y')
{
@@ -167,8 +171,9 @@ 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
+ }
+ mcl->getGraph()->printCompleteInformation();
+ // Performing on the fly Modelchecking*/
cout<<"Performing on the fly Modelchecking"<<endl;
if (auto run = k->intersecting_run(af))
@@ -185,6 +190,8 @@ int main(int argc, char** argv)
}
else
std::cout << "formula is verified\n";
+ //cin>>c;
+ //mcl->getGraph()->printCompleteInformation();
delete mcl;
}
else if (n_tasks==1)