From 850507ffe7b17313bf5936097da7b35ca6d07933 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Thu, 12 Nov 2020 16:22:04 +0100
Subject: [PATCH] modified: CMakeLists.txt modified:
src/CMakeLists.txt modified: src/LDDGraph.cpp modified:
src/LDDGraph.h modified: src/MCHybridSOG.cpp new file:
src/ModelCheckThReq.cpp new file: src/ModelCheckThReq.h
modified: src/ModelCheckerTh.cpp modified: src/ModelCheckerTh.h
modified: src/SogKripkeTh.cpp modified: src/SylvanWrapper.h
modified: src/main.cpp
---
CMakeLists.txt | 2 +-
src/CMakeLists.txt | 3 +-
src/LDDGraph.cpp | 2 -
src/LDDGraph.h | 5 +-
src/MCHybridSOG.cpp | 5 +-
src/ModelCheckLace.cpp | 314 ----------------------------------------
src/ModelCheckLace.h | 15 --
src/ModelCheckThReq.cpp | 224 ++++++++++++++++++++++++++++
src/ModelCheckThReq.h | 31 ++++
src/ModelCheckerTh.cpp | 24 +--
src/ModelCheckerTh.h | 4 +-
src/SogKripkeTh.cpp | 10 +-
src/SylvanWrapper.h | 2 +-
src/main.cpp | 30 +---
14 files changed, 291 insertions(+), 380 deletions(-)
delete mode 100644 src/ModelCheckLace.cpp
delete mode 100644 src/ModelCheckLace.h
create mode 100644 src/ModelCheckThReq.cpp
create mode 100644 src/ModelCheckThReq.h
diff --git a/CMakeLists.txt b/CMakeLists.txt
index bbd7e98..4f93205 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -11,7 +11,7 @@ set(CMAKE_CXX_EXTENSIONS OFF)
# Add compiler flags
if(CMAKE_COMPILER_IS_GNUCC)
-
+ #used flags -Og -DNDEBUG
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fpermissive -std=c++17 -pthread -Og -DNDEBUG")
endif()
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 2672d04..90327eb 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -72,7 +72,8 @@ add_executable(mc-sog main.cpp
ModelCheckerTh.cpp ModelCheckerTh.h
threadSOG.cpp threadSOG.h
HybridSOG.cpp HybridSOG.h
- MCHybridSOG.cpp MCHybridSOG.h)
+ MCHybridSOG.cpp MCHybridSOG.h
+ ModelCheckThReq.cpp ModelCheckThReq.h)
target_link_libraries(mc-sog
bddx
diff --git a/src/LDDGraph.cpp b/src/LDDGraph.cpp
index 99e8ad6..4959465 100644
--- a/src/LDDGraph.cpp
+++ b/src/LDDGraph.cpp
@@ -11,8 +11,6 @@ LDDGraph::~LDDGraph() {
void LDDGraph::setInitialState(LDDState *c) {
m_currentstate = m_initialstate = c;
- //
-
}
diff --git a/src/LDDGraph.h b/src/LDDGraph.h
index 1d7413b..aebec6e 100755
--- a/src/LDDGraph.h
+++ b/src/LDDGraph.h
@@ -30,7 +30,7 @@ class LDDGraph
MetaLDDNodes m_GONodes;
LDDState *getLDDStateById(unsigned int id);
void Reset();
- LDDState *m_initialstate;
+ LDDState *m_initialstate=nullptr;
LDDState *m_currentstate;
uint64_t m_nbStates;
uint64_t m_nbMarking;
@@ -54,6 +54,9 @@ class LDDGraph
//LDDState* getInitialState() const;
LDDState *getInitialState() const {
return m_GONodes.at(0);
+ }
+ LDDState *getInitialAggregate() {
+ return m_initialstate;
}
void printCompleteInformation();
virtual ~LDDGraph();
diff --git a/src/MCHybridSOG.cpp b/src/MCHybridSOG.cpp
index 957c9cc..c7f6fd7 100644
--- a/src/MCHybridSOG.cpp
+++ b/src/MCHybridSOG.cpp
@@ -14,12 +14,12 @@
#define TAG_INITIAL 3
#define TAG_ASK_SUCC 4
-#define TAG_AGREGATE 5
+
#define TAG_ACK_INITIAL 8
#define TAG_ASK_STATE 9
#define TAG_ACK_STATE 10
#define TAG_ACK_SUCC 11
-#define TAG_NOTCOMPLETED 20
+
//#define DEBUG_GC 1
using namespace std;
@@ -655,7 +655,6 @@ void MCHybridSOG::get_md5 ( const string& chaine,unsigned char *md_chaine )
pthread_spin_lock ( &m_spin_md5 );
MD5 ( chaine.c_str(), chaine.size(),md_chaine );
pthread_spin_unlock ( &m_spin_md5 );
- //md_chaine[16]='\0';
}
void MCHybridSOG::sendSuccToMC()
diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp
deleted file mode 100644
index 407da87..0000000
--- a/src/ModelCheckLace.cpp
+++ /dev/null
@@ -1,314 +0,0 @@
-#include "ModelCheckLace.h"
-
-#include "sylvan.h"
-#include "sylvan_seq.h"
-#include <sylvan_sog.h>
-#include <sylvan_int.h>
-
-using namespace sylvan;
-ModelCheckLace::ModelCheckLace(const NewNet &R,int nbThread):ModelCheckBaseMT(R,nbThread)
-{
-}
-void
-print_h(double size)
-{
- const char* units[] = {"B", "KB", "MB", "GB", "TB", "PB", "EB", "ZB", "YB"};
- int i = 0;
- for (;size>1024;size/=1024) i++;
- printf("%.*f %s", i, size, units[i]);
-}
-size_t
-getMaxMemoryTh()
-{
- long pages = sysconf(_SC_PHYS_PAGES);
- long page_size = sysconf(_SC_PAGE_SIZE);
- return pages * page_size;
-}
-void ModelCheckLace::preConfigure() {
- lace_init(m_nb_thread, 10000000);
- lace_startup(0, NULL, NULL);
- size_t max = 16LL<<30;
- if (max > getMaxMemoryTh()) max = getMaxMemoryTh()/10*9;
- printf("Memory : ");
- print_h(max);
- printf(" max.\n");
- LACE_ME;
- sylvan_set_limits(max, 16, 1);
- sylvan_init_package();
- sylvan_init_ldd();
-
- //init_gc_seq();
- sylvan_gc_enable();
- printf("%zu of %zu buckets filled!\n", llmsset_count_marked(nodes), llmsset_get_size(nodes));
- int i;
- vector<Place>::const_iterator it_places;
-
- m_transitions=m_net->transitions;
- m_observable=m_net->Observable;
- m_place_proposition=m_net->m_formula_place;
- m_nonObservable=m_net->NonObservable;
-
- m_transitionName=m_net->transitionName;
- m_placeName=m_net->m_placePosName;
-
-
- InterfaceTrans=m_net->InterfaceTrans;
-
- cout<<"Nombre de places : "<<m_nbPlaces<<endl;
- cout<<"Derniere place : "<<m_net->places[m_nbPlaces-1].name<<endl;
-
- uint32_t * liste_marques=new uint32_t[m_net->places.size()];
- for(i=0,it_places=m_net->places.begin(); it_places!=m_net->places.end(); i++,it_places++)
- {
- liste_marques[i] =it_places->marking;
- }
-
- m_initialMarking=lddmc_cube(liste_marques,m_net->places.size());
- lddmc_refs_push(m_initialMarking);
- delete []liste_marques;
-
- uint32_t *prec = new uint32_t[m_nbPlaces];
- uint32_t *postc= new uint32_t [m_nbPlaces];
- // Transition relation
- for(auto t=m_net->transitions.begin();
- t!=m_net->transitions.end(); t++)
- {
- // Initialisation
- for(i=0; i<m_nbPlaces; i++)
- {
- prec[i]=0;
- postc[i]=0;
- }
- // Calculer les places adjacentes a la transition t
- set<int> adjacentPlace;
- for(vector< pair<int,int> >::const_iterator it=t->pre.begin(); it!=t->pre.end(); it++)
- {
- adjacentPlace.insert(it->first);
- prec[it->first] = prec[it->first] + it->second;
- //printf("It first %d \n",it->first);
- //printf("In prec %d \n",prec[it->first]);
- }
- // arcs post
- for(vector< pair<int,int> >::const_iterator it=t->post.begin(); it!=t->post.end(); it++)
- {
- adjacentPlace.insert(it->first);
- postc[it->first] = postc[it->first] + it->second;
-
- }
- for(set<int>::const_iterator it=adjacentPlace.begin(); it!=adjacentPlace.end(); it++)
- {
- MDD Precond=lddmc_true;
- Precond = Precond & ((*it) >= prec[*it]);
- }
-
- MDD _minus=lddmc_cube(prec,m_nbPlaces);
- lddmc_refs_push(_minus);
- MDD _plus=lddmc_cube(postc,m_nbPlaces);
- lddmc_refs_push(_plus);
- m_tb_relation.push_back(TransSylvan(_minus,_plus));
- }
- delete [] prec;
- delete [] postc;
-}
-
-
-
-
-TASK_3 (MDD, Aggregate_epsilon_lace, MDD, From, Set*, nonObservable, vector<TransSylvan>*, tb_relation)
-{
- MDD M1;
- MDD M2=From;
-
- do
- {
- M1=M2;
- for(Set::iterator i=nonObservable->begin(); !(i==nonObservable->end()); i++)
- {
- lddmc_refs_spawn(SPAWN(lddmc_firing_lace,M2,(*tb_relation)[(*i)].getMinus(),(*tb_relation)[(*i)].getPlus()));
- }
-
- for(Set::iterator i=nonObservable->begin(); !(i==nonObservable->end()); i++)
- {
- lddmc_refs_push(M1);
- lddmc_refs_push(M2);
- MDD succ=lddmc_refs_sync(SYNC(lddmc_firing_lace));
- lddmc_refs_push(succ);
- M2=lddmc_union(succ,M2);
- lddmc_refs_pop(3);
- }
- }
- while (M1!=M2);
- /* lddmc_refs_popptr(2);*/
- return M2;
-}
-
-TASK_3 (Set, fire_obs_lace,MDD, State, Set*, observable, vector<TransSylvan>*, tb_relation)
-{
- Set res;
- for(Set::const_iterator i=observable->begin(); !(i==observable->end()); i++)
- {
- MDD succ = lddmc_firing_lace(State,(*tb_relation)[(*i)].getMinus(),(*tb_relation)[(*i)].getPlus());
- if(succ!=lddmc_false)
- {
- res.insert(*i);
-
- }
-
- }
- return res;
-}
-
-#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;
-
- 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()
-{
- if (!m_built_initial) {
- LDDState *initalAggregate=new LDDState();
- LDDState *reached_class;
- LACE_ME;
- MDD initial_meta_state(CALL(Aggregate_epsilon_lace,m_initialMarking,&m_nonObservable,&m_tb_relation));
-
- lddmc_refs_push(initial_meta_state);
- Set fire=fire_obs_lace(initial_meta_state,&m_observable,&m_tb_relation);
-
- // c->m_lddstate=CALL(lddmc_canonize,initial_meta_state,0,*this);
- initalAggregate->m_lddstate=initial_meta_state;
- 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::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);
- Complete_meta_state=SYNC(Aggregate_epsilon_lace);
- reached_class=new LDDState();
- reached_class->m_lddstate=Complete_meta_state;
- lddmc_refs_push(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));
- reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(initalAggregate,t));
- }
- m_built_initial=true;
- }
-
- return m_graph->getInitialState();
-}
-
-void ModelCheckLace::buildSucc(LDDState *agregate)
-{
- //cout<<__func__<<endl;
- 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;
- //displayMDDTableInfo();
- sylvan_gc();
- //displayMDDTableInfo();
- 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;
- Set::const_iterator iter=fire.begin();
- while(iter!=fire.end())
- {
- int t = *iter;
- SPAWN(Aggregate_epsilon_lace,get_successor(meta_state,t),&m_nonObservable,&m_tb_relation);
- onb_it++;iter++;
- }
-
- 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();
- reached_class->m_lddstate=Complete_meta_state;
- LDDState* pos=m_graph->find(reached_class);
-
- if(!pos)
- {
- lddmc_refs_push(Complete_meta_state);
- 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));
- reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(agregate,t));
-
- }
- else
- {
- m_graph->addArc();
- agregate->Successors.insert(agregate->Successors.begin(),LDDEdge(pos,t));
- pos->Predecessors.insert(pos->Predecessors.begin(),LDDEdge(agregate,t));
- delete reached_class;
- }
- }
-
-
- }
-
-}
-
-
-
-
-
diff --git a/src/ModelCheckLace.h b/src/ModelCheckLace.h
deleted file mode 100644
index 447af87..0000000
--- a/src/ModelCheckLace.h
+++ /dev/null
@@ -1,15 +0,0 @@
-#ifndef MODELCHECKLACE_H
-#define MODELCHECKLACE_H
-#include "ModelCheckBaseMT.h"
-class ModelCheckLace : public ModelCheckBaseMT {
-public:
- ModelCheckLace(const NewNet &R,int nbThread);
- LDDState * getInitialMetaState() override;
- void buildSucc(LDDState *agregate) override;
-private:
- void preConfigure();
- bool m_built_initial=false;
-
-};
-#endif
-
diff --git a/src/ModelCheckThReq.cpp b/src/ModelCheckThReq.cpp
new file mode 100644
index 0000000..d65eaf7
--- /dev/null
+++ b/src/ModelCheckThReq.cpp
@@ -0,0 +1,224 @@
+#include "ModelCheckThReq.h"
+#include <unistd.h>
+
+
+ModelCheckThReq::ModelCheckThReq(const NewNet &R, int nbThread) : ModelCheckBaseMT(R, nbThread) {
+}
+
+void
+print_h(double size) {
+ const char *units[] = {"B", "KB", "MB", "GB", "TB", "PB", "EB", "ZB", "YB"};
+ int i = 0;
+ for (; size > 1024; size /= 1024) i++;
+ printf("%.*f %s", i, size, units[i]);
+}
+
+size_t
+getMaxMemoryTh() {
+ long pages = sysconf(_SC_PHYS_PAGES);
+ long page_size = sysconf(_SC_PAGE_SIZE);
+ return pages * page_size;
+}
+
+void ModelCheckThReq::preConfigure() {
+ //cout<<"Enter : "<<__func__ <<endl;
+ SylvanWrapper::sylvan_set_limits(16LL << 30, 10, 0);
+ SylvanWrapper::sylvan_init_package();
+ SylvanWrapper::sylvan_init_ldd();
+ SylvanWrapper::init_gc_seq();
+ SylvanWrapper::displayMDDTableInfo();
+ int i;
+ vector<Place>::const_iterator it_places;
+
+ m_transitions = m_net->transitions;
+ m_observable = m_net->Observable;
+ m_place_proposition = m_net->m_formula_place;
+ m_nonObservable = m_net->NonObservable;
+
+ m_transitionName = &m_net->transitionName;
+ m_placeName = &m_net->m_placePosName;
+
+
+ InterfaceTrans = m_net->InterfaceTrans;
+
+ cout << "Nombre de places : " << m_nbPlaces << endl;
+ cout << "Derniere place : " << m_net->places[m_nbPlaces - 1].name << endl;
+
+ uint32_t *liste_marques = new uint32_t[m_net->places.size()];
+ for (i = 0, it_places = m_net->places.begin(); it_places != m_net->places.end(); i++, it_places++) {
+ liste_marques[i] = it_places->marking;
+ }
+
+ m_initialMarking = SylvanWrapper::lddmc_cube(liste_marques, m_net->places.size());
+ SylvanWrapper::lddmc_refs_push(m_initialMarking);
+ delete[]liste_marques;
+
+ uint32_t *prec = new uint32_t[m_nbPlaces];
+ uint32_t *postc = new uint32_t[m_nbPlaces];
+ // Transition relation
+ for (auto t = m_net->transitions.begin();
+ t != m_net->transitions.end(); t++) {
+ // Initialisation
+ for (i = 0; i < m_nbPlaces; i++) {
+ prec[i] = 0;
+ postc[i] = 0;
+ }
+ // Calculer les places adjacentes a la transition t
+ set<int> adjacentPlace;
+ for (vector<pair<int, int> >::const_iterator it = t->pre.begin(); it != t->pre.end(); it++) {
+ adjacentPlace.insert(it->first);
+ prec[it->first] = prec[it->first] + it->second;
+ //printf("It first %d \n",it->first);
+ //printf("In prec %d \n",prec[it->first]);
+ }
+ // arcs post
+ for (vector<pair<int, int> >::const_iterator it = t->post.begin(); it != t->post.end(); it++) {
+ adjacentPlace.insert(it->first);
+ postc[it->first] = postc[it->first] + it->second;
+
+ }
+ for (set<int>::const_iterator it = adjacentPlace.begin(); it != adjacentPlace.end(); it++) {
+ MDD Precond = lddmc_true;
+ Precond = Precond & ((*it) >= prec[*it]);
+ }
+
+ MDD _minus = SylvanWrapper::lddmc_cube(prec, m_nbPlaces);
+ SylvanWrapper::lddmc_refs_push(_minus);
+ MDD _plus = SylvanWrapper::lddmc_cube(postc, m_nbPlaces);
+ SylvanWrapper::lddmc_refs_push(_plus);
+ m_tb_relation.push_back(TransSylvan(_minus, _plus));
+ }
+ delete[] prec;
+ delete[] postc;
+}
+/**
+ * Creates builder threads
+ */
+void ModelCheckThReq::ComputeTh_Succ()
+{
+ int rc;
+ m_id_thread=0;
+ //cout<<"Enter : "<<__func__ <<endl;
+ pthread_mutex_init(&m_mutex, NULL);
+ pthread_mutex_init(&m_graph_mutex,NULL);
+ 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++)
+ {
+ if ((rc = pthread_create(&m_list_thread[i], NULL,threadHandler,this)))
+ {
+ cout<<"error: pthread_create, rc: "<<rc<<endl;
+ }
+ }
+}
+
+/*
+ * Build initial aggregate
+ */
+LDDState * ModelCheckThReq::getInitialMetaState() {
+ //cout<<"Enter : "<<__func__ <<endl;
+ if (m_graph->getInitialAggregate()!= nullptr) return m_graph->getInitialAggregate();
+ ComputeTh_Succ();
+ LDDState *c = new LDDState;
+ MDD initial_meta_state = Accessible_epsilon(m_initialMarking);
+ SylvanWrapper::lddmc_refs_push(initial_meta_state);
+ c->m_lddstate = initial_meta_state;
+ m_graph->setInitialState(c);
+ m_graph->insert(c);
+ Set fire = firable_obs(initial_meta_state);
+ int j = 0;
+ for (auto it = fire.begin(); it != fire.end(); it++, j++)
+ m_st[j % m_nb_thread].push(couple_th(c, *it));
+ pthread_barrier_wait(&m_barrier_threads);
+ pthread_barrier_wait(&m_barrier_builder);
+ c->setVisited();
+ return c;
+}
+
+/*
+ * Build successors of @aggregate using PThreads
+ */
+void ModelCheckThReq::buildSucc(LDDState *agregate) {
+ if (!agregate->isVisited())
+ {
+ //SylvanWrapper::displayMDDTableInfo();
+ agregate->setVisited();
+ Set fire=firable_obs(agregate->getLDDValue());
+ int j=0;
+ for(auto it=fire.begin(); it!=fire.end(); it++,j++)
+ m_st[j%m_nb_thread].push(couple_th(agregate,*it));
+ pthread_barrier_wait(&m_barrier_threads);
+ pthread_barrier_wait(&m_barrier_builder);
+ }
+}
+
+
+void * ModelCheckThReq::threadHandler(void *context)
+{
+ return ((ModelCheckThReq*)context)->Compute_successors();
+}
+
+
+
+void * ModelCheckThReq::Compute_successors()
+{
+ int id_thread;
+ id_thread=m_id_thread++;
+ LDDState* reached_class=nullptr;
+ // cout<<"Before do : "<<__func__ <<endl;
+ do
+ {
+ pthread_barrier_wait(&m_barrier_threads);
+ while (!m_st[id_thread].empty())
+ {
+ couple_th elt=m_st[id_thread].top();
+ m_st[id_thread].pop();
+ LDDState *aggregate=elt.first;
+ MDD meta_state=aggregate->getLDDValue();
+ int transition=elt.second;
+ MDD complete_state=Accessible_epsilon(get_successor(meta_state,transition));
+ reached_class=new LDDState;
+ reached_class->m_lddstate=complete_state;
+ reached_class->setDiv(Set_Div(complete_state));
+ reached_class->setDeadLock(Set_Bloc(complete_state));
+ pthread_mutex_lock(&m_graph_mutex);
+ LDDState* pos=m_graph->find(reached_class);
+ if(!pos)
+ {
+ m_graph->insert(reached_class);
+ aggregate->Successors.insert(aggregate->Successors.begin(),LDDEdge(reached_class,transition));
+ reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(aggregate,transition));
+ pthread_mutex_unlock(&m_graph_mutex);
+ m_graph->addArc();
+ }
+ else
+ { aggregate->Successors.insert(aggregate->Successors.begin(),LDDEdge(pos,transition));
+ pos->Predecessors.insert(pos->Predecessors.begin(),LDDEdge(aggregate,transition));
+ pthread_mutex_unlock(&m_graph_mutex);
+ m_graph->addArc();
+ delete reached_class;
+ }
+
+ }
+ //cout<<"Before barrier : "<<__func__ <<endl;
+ pthread_barrier_wait(&m_barrier_builder);
+ //m_finish=m_finish;
+ //cout<<"After barrier : "<<__func__ <<endl;
+ }
+ while (!m_finish);
+ //cout<<"Quit : "<<__func__ <<" ; "<<id_thread<<endl;
+}
+
+
+ModelCheckThReq::~ModelCheckThReq() {
+ //cout<<"1 : "<<__func__ <<endl;
+ pthread_barrier_wait(&m_barrier_threads);
+ m_finish=true;
+ pthread_barrier_wait(&m_barrier_builder);
+ /*for (int i = 0; i < m_nb_thread; i++)
+ {
+ pthread_join(m_list_thread[i], NULL);
+ }*/
+ //cout<<"3 : "<<__func__ <<endl;
+}
+
diff --git a/src/ModelCheckThReq.h b/src/ModelCheckThReq.h
new file mode 100644
index 0000000..db4ef2a
--- /dev/null
+++ b/src/ModelCheckThReq.h
@@ -0,0 +1,31 @@
+#ifndef MODELCHECKLACE_H
+#define MODELCHECKLACE_H
+#include "ModelCheckBaseMT.h"
+#include <atomic>
+#include <mutex>
+
+typedef pair<LDDState *, int> couple_th;
+typedef stack<pair<LDDState *,int>> pile_t;
+class ModelCheckThReq : public ModelCheckBaseMT {
+public:
+ ModelCheckThReq(const NewNet &R,int nbThread);
+ ~ModelCheckThReq();
+
+ void buildSucc(LDDState *agregate) override;
+ static void *threadHandler(void *context);
+ void *Compute_successors();
+ void ComputeTh_Succ();
+ LDDState * getInitialMetaState();
+private:
+ void preConfigure();
+ pile_t m_st[128];
+ atomic<uint8_t> m_id_thread;
+ pthread_mutex_t m_mutex;
+ pthread_mutex_t m_graph_mutex;
+ pthread_barrier_t m_barrier_threads,m_barrier_builder;
+ pthread_t m_list_thread[128];
+ volatile atomic<bool> m_finish=false;
+
+};
+#endif
+
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index a5aecf1..2517e05 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -145,17 +145,17 @@ void* ModelCheckerTh::Compute_successors() {
reached_class = new LDDState();
reached_class->m_lddstate = reduced_meta;
//pthread_spin_lock(&m_accessible);
-
+
LDDState *pos = m_graph->find(reached_class);
- if (!pos) {
+ if (!pos) {
+ m_graph_mutex.lock();
+ e.first.first->Successors.insert(e.first.first->Successors.begin(), LDDEdge(reached_class, t));
+ reached_class->Predecessors.insert(reached_class->Predecessors.begin(), LDDEdge(e.first.first, t));
+ m_graph_mutex.unlock();
m_graph->addArc();
m_graph->insert(reached_class);
reached_class->setDeadLock(Set_Bloc(reduced_meta));
reached_class->setDiv(Set_Div(reduced_meta));
- m_graph_mutex.lock();
- e.first.first->Successors.insert(e.first.first->Successors.begin(), LDDEdge(reached_class, t));
- reached_class->Predecessors.insert(reached_class->Predecessors.begin(), LDDEdge(e.first.first, t));
- m_graph_mutex.unlock();
fire = firable_obs(reduced_meta);
min_charge = minCharge();
//m_min_charge=(m_min_charge+1) % m_nb_thread;
@@ -164,11 +164,12 @@ void* ModelCheckerTh::Compute_successors() {
pthread_spin_unlock(&m_spin_stack[min_charge]);
m_charge[min_charge]++;
} else {
- m_graph->addArc();
- m_graph_mutex.lock();
- e.first.first->Successors.insert(e.first.first->Successors.begin(), LDDEdge(pos, t));
- pos->Predecessors.insert(pos->Predecessors.begin(), LDDEdge(e.first.first, t));
+ //m_graph_mutex.lock();
+ m_graph_mutex.lock();
+ e.first.first->Successors.insert(e.first.first->Successors.begin(), LDDEdge(pos, t));
+ pos->Predecessors.insert(pos->Predecessors.begin(), LDDEdge(e.first.first, t));
m_graph_mutex.unlock();
+ m_graph->addArc();
delete reached_class;
}
#ifdef GCENABLE
@@ -201,7 +202,7 @@ void ModelCheckerTh::ComputeTh_Succ() {
pthread_barrier_init(&m_barrier_builder, NULL, m_nb_thread + 1);
for (int i = 0; i < m_nb_thread; i++) {
- pthread_spin_init(&m_spin_stack[i], NULL);
+ pthread_spin_init(&m_spin_stack[i],0);
m_charge[i] = 0;
m_terminaison[i] = false;
}
@@ -219,7 +220,6 @@ ModelCheckerTh::~ModelCheckerTh() {
for (int i = 0; i < m_nb_thread; i++) {
pthread_join(m_list_thread[i], NULL);
}
-
}
uint8_t ModelCheckerTh::minCharge() {
diff --git a/src/ModelCheckerTh.h b/src/ModelCheckerTh.h
index a94b6c7..f325ec0 100644
--- a/src/ModelCheckerTh.h
+++ b/src/ModelCheckerTh.h
@@ -21,10 +21,8 @@ private:
pile m_st[MAXT];
int m_charge[MAXT];
bool m_terminaison[MAXT];
- atomic<uint8_t> m_id_thread;
-
+ atomic<uint8_t> m_id_thread;
pthread_barrier_t m_barrier_builder;
-
volatile bool m_finish=false;
pthread_mutex_t m_mutex_stack[MAXT];
pthread_t m_list_thread[MAXT];
diff --git a/src/SogKripkeTh.cpp b/src/SogKripkeTh.cpp
index 6f727c4..f2836b1 100644
--- a/src/SogKripkeTh.cpp
+++ b/src/SogKripkeTh.cpp
@@ -57,13 +57,13 @@ SogKripkeIteratorTh* SogKripkeTh::succ_iter(const spot::state* s) const {
auto ss = static_cast<const SogKripkeStateTh*>(s);
LDDState *aggregate=ss->getLDDState();
bdd cond = state_condition(ss);
- if (iter_cache_)
+ /*if (iter_cache_)
{
- /*auto it = static_cast<SogKripkeIteratorTh*>(iter_cache_);
- iter_cache_ = nullptr; // empty the cache
+ auto it = static_cast<SogKripkeIteratorTh*>(iter_cache_);
it->recycle(aggregate, cond);
- return it;*/
- }
+ iter_cache_ = nullptr; // empty the cache
+ return it;
+ }*/
return new SogKripkeIteratorTh(aggregate,cond);
diff --git a/src/SylvanWrapper.h b/src/SylvanWrapper.h
index 325cd82..8251052 100644
--- a/src/SylvanWrapper.h
+++ b/src/SylvanWrapper.h
@@ -123,7 +123,7 @@ public:
static void sylvan_init_package(void);
- static mddnode_t GETNODE(MDD mdd) { return ((mddnode_t) llmsset_index_to_ptr(m_nodes, mdd)); }
+ inline static mddnode_t GETNODE(MDD mdd) { return ((mddnode_t) llmsset_index_to_ptr(m_nodes, mdd)); }
static void *llmsset_index_to_ptr(const llmsset2_t dbs, size_t index) {
return dbs->data + index * 16;
diff --git a/src/main.cpp b/src/main.cpp
index c20e178..87dc1b3 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -10,6 +10,7 @@
#include "LDDGraph.h"
#include "ModelCheckerCPPThread.h"
#include "ModelCheckerTh.h"
+#include "ModelCheckThReq.h"
#include "threadSOG.h"
#include "HybridSOG.h"
#include "MCHybridSOG.h"
@@ -119,12 +120,12 @@ int main(int argc, char **argv) {
if (n_tasks == 1) {
- if (n_tasks == 1 && (!strcmp(argv[1], "otfL") || !strcmp(argv[1], "otfC") || !strcmp(argv[1], "otfP"))) {
+ if (n_tasks == 1 && (!strcmp(argv[1], "otfPR") || !strcmp(argv[1], "otfC") || !strcmp(argv[1], "otfP"))) {
cout << "Performing on the fly Model checking..." << endl;
if (!strcmp(argv[1], "otfP"))
cout << "Multi-threaded algorithm based on Pthread library!" << endl;
- else if (!strcmp(argv[1], "otfL"))
- cout << "Multi-threaded algorithm based on Lace framework!" << endl;
+ else if (!strcmp(argv[1], "otfPR"))
+ cout << "Multi-threaded algorithm (progressive) based on PThread!" << endl;
else
cout << "Multi-threaded algorithm based on C++ Thread library!" << endl;
cout << "Building automata for not(formula)\n";
@@ -150,8 +151,10 @@ int main(int argc, char **argv) {
else*/
if (!strcmp(argv[1], "otfP"))
mcl = new ModelCheckerTh(Rnewnet, nb_th);
- else
+ else if (!strcmp(argv[1], "otfC"))
mcl = new ModelCheckerCPPThread(Rnewnet, nb_th);
+ else
+ mcl=new ModelCheckThReq(Rnewnet, nb_th);
mcl->loadNet();
auto k = std::make_shared<SogKripkeTh>(d, mcl, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP());
cout << "Performing on the fly Modelchecking" << endl;
@@ -231,17 +234,7 @@ int main(int argc, char **argv) {
cout << "Count of threads to be created: " << nb_th << endl;
DR.computeDSOG(g, true);
g.printCompleteInformation();
- } /*else if (!strcmp(argv[1], "l")) {
- cout << "Construction with lace framework." << endl;
- cout << "Count of workers to be created: " << nb_th << endl;
- DR.computeSOGLace(g);
- g.printCompleteInformation();
- } else if (!strcmp(argv[1], "lc")) {
- cout << "Canonised construction with lace framework." << endl;
- cout << "Count of workers to be created: " << nb_th << endl;
- DR.computeSOGLaceCanonized(g);
- g.printCompleteInformation();
- }*/
+ }
cout << "Perform Model checking ?";
char c;
@@ -389,13 +382,6 @@ int main(int argc, char **argv) {
}*/
}
}
-
-
-
-
-
-
-
MPI_Finalize();
return (EXIT_SUCCESS);
}
--
GitLab