From d9a2375e6ea3ab454663ff4f1f205439c4df2892 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Thu, 13 Jun 2019 11:37:06 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/ModelCheckBaseMT.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20?=
=?UTF-8?q?=20=20=20=20=20=20src/ModelCheckBaseMT.h=20=09modifi=C3=A9?=
=?UTF-8?q?=C2=A0:=20=20=20=20=20=20=20=20=20src/ModelCheckerTh.cpp=20=09m?=
=?UTF-8?q?odifi=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/ModelCheckBaseMT.cpp | 6 ++++
src/ModelCheckBaseMT.h | 1 +
src/ModelCheckerTh.cpp | 6 ++++
src/main.cpp | 74 ++++++----------------------------------
4 files changed, 24 insertions(+), 63 deletions(-)
diff --git a/src/ModelCheckBaseMT.cpp b/src/ModelCheckBaseMT.cpp
index 1b54f66..166eed4 100644
--- a/src/ModelCheckBaseMT.cpp
+++ b/src/ModelCheckBaseMT.cpp
@@ -20,6 +20,12 @@ void ModelCheckBaseMT::loadNet()
m_graph->setPlace(m_placeName);
}
+ModelCheckBaseMT::~ModelCheckBaseMT()
+{
+ cout<<__func__<<endl;
+}
+
+
diff --git a/src/ModelCheckBaseMT.h b/src/ModelCheckBaseMT.h
index 00d313c..af8a2d5 100644
--- a/src/ModelCheckBaseMT.h
+++ b/src/ModelCheckBaseMT.h
@@ -7,6 +7,7 @@ public:
virtual LDDState * buildInitialMetaState()=0;
virtual void buildSucc(LDDState *agregate)=0;
void loadNet();
+ virtual ~ModelCheckBaseMT();
protected:
int m_nb_thread;
private:
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index b5ca2cb..aedecaf 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -185,6 +185,7 @@ void * ModelCheckerTh::Compute_successors()
pthread_barrier_wait(&m_barrier_builder);
}
while (!m_finish);
+ cout<<"exit thread i"<<id_thread<<endl;
}
@@ -228,10 +229,15 @@ void ModelCheckerTh::ComputeTh_Succ()
}
ModelCheckerTh::~ModelCheckerTh() {
m_finish=true;
+ cout<<"Destructor"<<endl;
pthread_barrier_wait(&m_barrier_threads);
+ cout<<"Before builder..."<<endl;
pthread_barrier_wait(&m_barrier_builder);
+ cout<<"After barrier..."<<endl;
for (int i = 0; i < m_nb_thread; i++)
{
+ cout<<"thread "<<i<<endl;
pthread_join(m_list_thread[i], NULL);
}
+ cout<<"Exit Destructor"<<endl;
}
diff --git a/src/main.cpp b/src/main.cpp
index 9857564..620d144 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -127,12 +127,14 @@ int main(int argc, char** argv)
MPI_Comm_rank(MPI_COMM_WORLD,&task_id);
//
- if (n_tasks==1 && !strcmp(argv[1],"otfL"))
+ if (n_tasks==1 && (!strcmp(argv[1],"otfL") || !strcmp(argv[1],"otfP")))
{
- cout<<"Multi-threaded on the fly Model checking (Lace)..."<<endl;
+ cout<<"Performing on the fly Model checking..."<<endl;
+ if (!strcmp(argv[1],"otfP")) cout<<"Multi-threaded algorithm based on Pthread library!"<<endl;
+ else cout<<"Multi-threaded algorithm based on Lace framework!"<<endl;
cout<<"Building automata for not(formula)\n";
auto d = spot::make_bdd_dict();
- // d->register_ap("jbhkj");
+
spot::twa_graph_ptr af = spot::translator(d).run(not_f);
cout<<"Formula automata built.\n";
cout<<"Want to save the graph in a dot file ?";
@@ -147,8 +149,11 @@ int main(int argc, char** argv)
spot::print_dot(file, af);
file.close();
}
- // Initialize SOG builder
- ModelCheckLace* mcl=new ModelCheckLace(R,bound,nb_th);
+ cout<<"Loading net information..."<<endl;
+ ModelCheckBaseMT* mcl;
+ if (!strcmp(argv[1],"otfL")) mcl=new ModelCheckLace(R,bound,nb_th);
+ else
+ mcl=new ModelCheckerTh(R,bound,nb_th);
mcl->loadNet();
auto k =
std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP());
@@ -170,62 +175,7 @@ int main(int argc, char** argv)
if (auto run = k->intersecting_run(af))
{
std::cout << "formula is violated by the following run:\n"<<*run<<endl;
- /*run->highlight(5); // 5 is a color number.
- fstream file;
- file.open("violated.dot",fstream::out);
- 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";
-
- }
- else if (n_tasks==1 && !strcmp(argv[1],"otfP"))
- {
- cout<<"Multi-threaded on the fly Model checking (Pthread)..."<<endl;
- cout<<"Building automata for not(formula)\n";
- auto d = spot::make_bdd_dict();
-
- spot::twa_graph_ptr af = spot::translator(d).run(not_f);
- cout<<"Formula automata built.\n";
- cout<<"Want to save the graph in a dot file ?";
- char c;
- cin>>c;
- if (c=='y')
- {
- fstream file;
- string st(formula);
- st+=".dot";
- file.open(st.c_str(),fstream::out);
- spot::print_dot(file, af);
- file.close();
- }
- // Initialize SOG builder
- ModelCheckerTh* mcl=new ModelCheckerTh(R,bound,nb_th);
- mcl->loadNet();
- auto k =
- std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()); ;
-
- // Performing on the fly Modelchecking
- 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, k,"ka");
- file.close();
- }
- cout<<"Performing on the fly Modelchecking"<<endl;
-
- if (auto run = k->intersecting_run(af))
- {
- std::cout << "formula is violated by the following run:\n"<<*run<<endl;
+ cout<<"=================================="<<endl;
/*run->highlight(5); // 5 is a color number.
fstream file;
file.open("violated.dot",fstream::out);
@@ -237,9 +187,7 @@ int main(int argc, char** argv)
else
std::cout << "formula is verified\n";
delete mcl;
-
}
-
else if (n_tasks==1)
{
cout<<"number of task = 1 \n " <<endl;
--
GitLab