From 889ce05ca11378239ebdfdda166f929205efc9ff Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Tue, 4 Jun 2019 23:42:33 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/ModelCheckerTh.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20?=
=?UTF-8?q?=20=20=20=20=20src/main.cpp?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/ModelCheckerTh.cpp | 23 +++++++----------------
src/main.cpp | 25 ++++++++++++++++++++++++-
2 files changed, 31 insertions(+), 17 deletions(-)
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index 55925ec..b155c67 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -130,14 +130,11 @@ string ModelCheckerTh::getPlace(int pos)
LDDState * ModelCheckerTh::buildInitialMetaState()
{
- Set fire;
LDDState *c=new LDDState;
- LDDState *reached_class;
- MDD initial_meta_state(Accessible_epsilon(m_initalMarking));
+ cout<<"Initial marking : "<<m_initalMarking<<endl;
+ MDD initial_meta_state=Accessible_epsilon(m_initalMarking);
ldd_refs_push(initial_meta_state);
- fire=firable_obs(initial_meta_state);
-
c->m_lddstate=initial_meta_state;
m_graph->setInitialState(c);
m_graph->insert(c);
@@ -175,7 +172,7 @@ void * ModelCheckerTh::Compute_successors()
while (!m_st[id_thread].empty())
{
-
+ cout<<"Entering thread "<<endl;
nb_it++;
m_terminaison[id_thread]=false;
pthread_spin_lock(&m_spin_stack[id_thread]);
@@ -206,7 +203,6 @@ void * ModelCheckerTh::Compute_successors()
m_graph->addArc();
m_graph->insert(reached_class);
pthread_mutex_unlock(&m_graph_mutex);
-
agregate->Successors.insert(agregate->Successors.begin(),LDDEdge(reached_class,t));
reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(agregate,t));
@@ -220,15 +216,10 @@ void * ModelCheckerTh::Compute_successors()
delete reached_class;
}
}
-
-
}
m_terminaison[id_thread]=true;
-
-
-
}
- while (isNotTerminated());
+ while (1);
}
@@ -267,7 +258,7 @@ void * ModelCheckerTh::threadHandler(void *context)
void ModelCheckerTh::ComputeTh_Succ(){
- cout << "number of threads "<<m_nb_thread<<endl;
+
int rc;
// m_graph=&g;
// m_graph->setTransition(m_transitionName);
@@ -293,11 +284,11 @@ void ModelCheckerTh::ComputeTh_Succ(){
cout<<"error: pthread_create, rc: "<<rc<<endl;
}
}
- Compute_successors();
+ /* Compute_successors();
for (int i = 0; i < m_nb_thread-1; i++)
{
pthread_join(m_list_thread[i], NULL);
- }
+ }*/
}
diff --git a/src/main.cpp b/src/main.cpp
index cab0389..84156d7 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -193,8 +193,31 @@ int main(int argc, char** argv)
// Initialize SOG builder
ModelCheckerTh* mcl=new ModelCheckerTh(R,bound,nb_th);
cout<<"Created"<<endl;
+ /********************************************************************/
+ spot::twa_graph_ptr kk =
+ spot::make_twa_graph(std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()),
+ spot::twa::prop_set::all(), true);
+
+
+ cout<<"SOG translated to SPOT succeeded.."<<endl;
+ cout<<"Want to save the graph in a dot file ?";
+ cin>>c;
+ if (c=='y')
+ {
+ fstream file;
+
+ string st(argv[3]);
+ st+=".dot";
+ file.open(st.c_str(),fstream::out);
+ spot::print_dot(file, kk,"ka");
+ file.close();
+ }
+
+ /********************************************************************/
+
+
auto k =
- std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()); ;
+ std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()); ;
// Performing on the fly Modelchecking
cout<<"Performing on the fly Modelchecking"<<endl;
--
GitLab