From 728a6456a7c2aeb291f6897fddd94d61b08138b8 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Sat, 21 Mar 2020 15:34:08 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/LDDGraph.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20?=
=?UTF-8?q?=20=20src/LDDState.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20?=
=?UTF-8?q?=20=20=20=20src/LDDState.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20?=
=?UTF-8?q?=20=20=20=20=20src/MCHybridSOG.cpp=20=09modifi=C3=A9=C2=A0:=20?=
=?UTF-8?q?=20=20=20=20=20=20=20=20src/ModelCheckLace.cpp=20=09modifi?=
=?UTF-8?q?=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/ModelCheckerTh.cpp?=
=?UTF-8?q?=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/main.cp?=
=?UTF-8?q?p?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/LDDGraph.h | 2 +-
src/LDDState.cpp | 9 -
src/LDDState.h | 8 +-
src/MCHybridSOG.cpp | 15 +-
src/ModelCheckLace.cpp | 4 +-
src/ModelCheckerTh.cpp | 584 +++++++++++++++++--------------------
src/main.cpp | 633 ++++++++++++++++++++---------------------
7 files changed, 586 insertions(+), 669 deletions(-)
diff --git a/src/LDDGraph.h b/src/LDDGraph.h
index d29547f..f2a562e 100755
--- a/src/LDDGraph.h
+++ b/src/LDDGraph.h
@@ -42,7 +42,7 @@ class LDDGraph
int NbBddNode(LDDState*,size_t&);
void InitVisit(LDDState * S,size_t nb);
void printpredecessors(LDDState *);
- void addArc(){m_nbArcs++;}
+ inline void addArc() {m_nbArcs++;}
void insert(LDDState*);
LDDGraph(CommonSOG *constuctor) {m_nbStates=m_nbArcs=m_nbMarking=0;m_constructor=constuctor;}
void setInitialState(LDDState*); //Define the initial state of this graph
diff --git a/src/LDDState.cpp b/src/LDDState.cpp
index d1b0342..8d51f37 100644
--- a/src/LDDState.cpp
+++ b/src/LDDState.cpp
@@ -21,13 +21,7 @@ unsigned char* LDDState::getSHAValue() {
}
-bool LDDState::isVirtual() {
- return m_virtual;
-}
-void LDDState::setVirtual() {
- m_virtual=true;
-}
vector<pair<LDDState*, int>>* LDDState::getSuccessors() {
return &Successors;
@@ -66,12 +60,9 @@ vector<uint16_t> LDDState::getUnmarkedPlaces(set<uint16_t>& lplacesAP) {
if (lplacesAP.find(depth)!=lplacesAP.end())
if (mddnode_getvalue(node)==0) {
result.push_back(depth);
-
}
-
mdd=mddnode_getdown(node);
depth++;
-
}
return result;
}
diff --git a/src/LDDState.h b/src/LDDState.h
index 7864d20..6734ac9 100755
--- a/src/LDDState.h
+++ b/src/LDDState.h
@@ -31,14 +31,14 @@ class LDDState {
bool m_blocage=false;
- bool isVirtual();
- void setVirtual();
+ bool isVirtual() {return m_virtual;}
+ void setVirtual(){m_virtual=true;}
void setDiv(bool di) {m_boucle=di;}
bool isDiv() {return m_boucle;}
void setDeadLock(bool de) {m_blocage=de;}
bool isDeadLock() {return m_blocage;}
- void setVisited() {m_visited=true;}
- bool isVisited() {return m_visited;}
+ inline void setVisited() {m_visited=true;}
+ inline bool isVisited() {return m_visited;}
void setCompletedSucc() {m_completed=true;}
bool isCompletedSucc() {return m_completed;}
vector<uint16_t> getMarkedPlaces(set<uint16_t>& lplacesAP);
diff --git a/src/MCHybridSOG.cpp b/src/MCHybridSOG.cpp
index e793f5d..35e8816 100644
--- a/src/MCHybridSOG.cpp
+++ b/src/MCHybridSOG.cpp
@@ -1,13 +1,13 @@
#include "MCHybridSOG.h"
//#define DEBUG_GC
-#define REDUCE
-using namespace std;
-#include <stdio.h>
+
+
+#include <cstdio>
#include "sylvan_seq.h"
#include <sylvan_int.h>
-using namespace sylvan;
+
#include <openssl/md5.h>
#define GETNODE(mdd) ((mddnode_t)llmsset_index_to_ptr(nodes, mdd))
@@ -24,7 +24,8 @@ using namespace sylvan;
#define TAG_ACK_STATE 10
#define TAG_ACK_SUCC 11
#define TAG_NOTCOMPLETED 20
-
+using namespace sylvan;
+using namespace std;
MCHybridSOG::MCHybridSOG(const NewNet &R,MPI_Comm &comm_world,bool init)
{
@@ -118,7 +119,7 @@ MCHybridSOG::MCHybridSOG(const NewNet &R,MPI_Comm &comm_world,bool init)
//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
-//////////////////////////////////////////////////// Version distribuée en utilisant les LDD - MPI/////////////////////////////////////////////////////////
+//////////////////////////////////////////////////// Version distribu�e en utilisant les LDD - MPI/////////////////////////////////////////////////////////
//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -422,7 +423,7 @@ void *MCHybridSOG::doCompute()
}
- /******************************* Construction des aggregats à partir de pile de messages ************************************/
+ /******************************* Construction des aggregats � partir de pile de messages ************************************/
if (!m_msg[id_thread].empty())
{
diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp
index e9d174b..cb4c3f8 100644
--- a/src/ModelCheckLace.cpp
+++ b/src/ModelCheckLace.cpp
@@ -42,7 +42,7 @@ void ModelCheckLace::preConfigure() {
printf("%zu of %zu buckets filled!\n", llmsset_count_marked(nodes), llmsset_get_size(nodes));
int i;
vector<Place>::const_iterator it_places;
- //_______________
+
transitions=m_net.transitions;
m_observable=m_net.Observable;
m_place_proposition=m_net.m_formula_place;
@@ -139,8 +139,6 @@ TASK_3 (MDD, Aggregate_epsilon_lace, MDD, From, Set*, nonObservable, vector<Tran
M2=lddmc_union(succ,M2);
lddmc_refs_pop(3);
}
-
-
}
while (M1!=M2);
/* lddmc_refs_popptr(2);*/
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index ab91b12..0666d72 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -7,345 +7,285 @@
using namespace sylvan;
-ModelCheckerTh::ModelCheckerTh(const NewNet &R,int nbThread):ModelCheckBaseMT(R,nbThread) {
+ModelCheckerTh::ModelCheckerTh(const NewNet &R, int nbThread) :
+ ModelCheckBaseMT(R, nbThread) {
}
-void ModelCheckerTh::preConfigure()
-{
-
- lace_init(1, 0);
- lace_startup(0, NULL, NULL);
-
- sylvan_set_limits(2LL<<30, 16, 3);
- sylvan_init_package();
- sylvan_init_ldd();
-
- int i;
- vector<Place>::const_iterator it_places;
-
-
- init_gc_seq();
-
-
- //_______________
- 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;
-
- /* 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;
- }*/
-
-
- 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());
-
- uint32_t *prec = new uint32_t[m_nbPlaces];
- uint32_t *postc= new uint32_t [m_nbPlaces];
- // Transition relation
- for(vector<Transition>::const_iterator 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);
- ldd_refs_push(_minus);
- MDD _plus=lddmc_cube(postc,m_nbPlaces);
- ldd_refs_push(_plus);
- m_tb_relation.push_back(TransSylvan(_minus,_plus));
- }
- delete [] prec;
- delete [] postc;
- ComputeTh_Succ();
-
-}
-
-
-
+void ModelCheckerTh::preConfigure() {
+
+ lace_init(1, 0);
+ lace_startup(0, NULL, NULL);
+
+ sylvan_set_limits(2LL << 30, 16, 3);
+ sylvan_init_package();
+ sylvan_init_ldd();
+
+ int i;
+ vector<Place>::const_iterator it_places;
+
+ init_gc_seq();
+
+ //_______________
+ 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());
+
+ uint32_t *prec = new uint32_t[m_nbPlaces];
+ uint32_t *postc = new uint32_t[m_nbPlaces];
+ // Transition relation
+ for (vector<Transition>::const_iterator 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);
+ ldd_refs_push(_minus);
+ MDD _plus = lddmc_cube(postc, m_nbPlaces);
+ ldd_refs_push(_plus);
+ m_tb_relation.push_back(TransSylvan(_minus, _plus));
+ }
+ delete[] prec;
+ delete[] postc;
+ ComputeTh_Succ();
+}
-LDDState * ModelCheckerTh::getInitialMetaState()
-{
- while (!m_finish_initial);
- LDDState *initial_metastate=m_graph->getInitialState();
- if (!initial_metastate->isVisited()) {
- initial_metastate->setVisited();
- while (!initial_metastate->isCompletedSucc());
- }
- return initial_metastate;
+LDDState* ModelCheckerTh::getInitialMetaState() {
+ while (!m_finish_initial)
+ ;
+ LDDState *initial_metastate = m_graph->getInitialState();
+ if (!initial_metastate->isVisited()) {
+ initial_metastate->setVisited();
+ while (!initial_metastate->isCompletedSucc())
+ ;
+ }
+ return initial_metastate;
}
-void ModelCheckerTh::buildSucc(LDDState *agregate)
-{
- if (!agregate->isVisited())
- {
- agregate->setVisited();
- while (!agregate->isCompletedSucc());
- }
+void ModelCheckerTh::buildSucc(LDDState *agregate) {
+ if (!agregate->isVisited()) {
+ agregate->setVisited();
+ while (!agregate->isCompletedSucc())
+ ;
+ }
}
-void * ModelCheckerTh::Compute_successors()
-{
- int id_thread;
-
- pthread_mutex_lock(&m_mutex);
- id_thread=m_id_thread++;
- pthread_mutex_unlock(&m_mutex);
- Set fire;
- int min_charge=0;
- if (id_thread==0)
- {
- LDDState *c=new LDDState;
-
- MDD Complete_meta_state(Accessible_epsilon(m_initialMarking));
- ldd_refs_push(Complete_meta_state);
- MDD canonised_initial=Complete_meta_state;//Canonize(Complete_meta_state,0);
- ldd_refs_push(canonised_initial);
- fire=firable_obs(Complete_meta_state);
-
-
- c->m_lddstate=canonised_initial;
- c->setDeadLock(Set_Bloc(Complete_meta_state));
- c->setDiv(Set_Div(Complete_meta_state));
- m_st[0].push(Pair(couple(c,Complete_meta_state),fire));
- m_graph->setInitialState(c);
- m_graph->insert(c);
- m_charge[0]=1;
- m_finish_initial=true;
-
- }
-
- LDDState* reached_class;
- do
- {
- while (!m_st[id_thread].empty())
- {
- m_terminaison[id_thread]=false;
- pthread_spin_lock(&m_spin_stack[id_thread]);
- Pair e=m_st[id_thread].top();
- //pthread_spin_lock(&m_accessible);
- m_st[id_thread].pop();
-
- pthread_spin_unlock(&m_spin_stack[id_thread]);
-
-
- m_charge[id_thread]--;
- while(!e.second.empty())
- {
- int t = *e.second.begin();
- e.second.erase(t);
- reached_class=new LDDState();
- if (id_thread)
- {
- pthread_mutex_lock(&m_supervise_gc_mutex);
- m_gc++;
- if (m_gc==1) {
- pthread_mutex_lock(&m_gc_mutex);
- }
- pthread_mutex_unlock(&m_supervise_gc_mutex);
- }
-
-
- MDD Complete_meta_state=Accessible_epsilon(get_successor(e.first.second,t));
-
- ldd_refs_push(Complete_meta_state);
-
- MDD reduced_meta=Complete_meta_state;//Canonize(Complete_meta_state,0);
- ldd_refs_push(reduced_meta);
-
- if (id_thread==0)
- {
- pthread_mutex_lock(&m_gc_mutex);
- // #ifdef DEBUG_GC
- // displayMDDTableInfo();
- // #endif // DEBUG_GC
-
- sylvan_gc_seq();
- // #ifdef DEBUG_GC
- // displayMDDTableInfo();
- // #endif // DEBUG_GC
- pthread_mutex_unlock(&m_gc_mutex);
- }
- reached_class->m_lddstate=reduced_meta;
- //reached_class->m_lddstate=reduced_meta;
- //nbnode=bdd_pathcount(reached_class->m_lddstate);
-
- //pthread_spin_lock(&m_accessible);
- pthread_mutex_lock(&m_graph_mutex);
-
- LDDState* pos=m_graph->find(reached_class);
-
- if(!pos)
- {
- // cout<<"not found"<<endl;
- //reached_class->blocage=Set_Bloc(Complete_meta_state);
- //reached_class->boucle=Set_Div(Complete_meta_state);
-
- m_graph->addArc();
- m_graph->insert(reached_class);
- reached_class->setDiv(Set_Div(Complete_meta_state));
- reached_class->setDeadLock(Set_Bloc(Complete_meta_state));
- pthread_mutex_unlock(&m_graph_mutex);
-
- 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));
- //pthread_mutex_lock(&m_mutex);
- fire=firable_obs(Complete_meta_state);
- //if (max_succ<fire.size()) max_succ=fire.size();
- //pthread_mutex_unlock(&m_mutex);
- min_charge= minCharge();
- //m_min_charge=(m_min_charge+1) % m_nb_thread;
- pthread_spin_lock(&m_spin_stack[min_charge]);
- m_st[min_charge].push(Pair(couple(reached_class,Complete_meta_state),fire));
- pthread_spin_unlock(&m_spin_stack[min_charge]);
- m_charge[min_charge]++;
- }
- else
- {
- m_graph->addArc();
- pthread_mutex_unlock(&m_graph_mutex);
-
- e.first.first->Successors.insert(e.first.first->Successors.begin(),LDDEdge(pos,t));
- pos->Predecessors.insert(pos->Predecessors.begin(),LDDEdge(e.first.first,t));
- delete reached_class;
-
- }
- if (id_thread)
- {
- pthread_mutex_lock(&m_supervise_gc_mutex);
- m_gc--;
- if (m_gc==0) pthread_mutex_unlock(&m_gc_mutex);
- pthread_mutex_unlock(&m_supervise_gc_mutex);
- }
- }
- e.first.first->setCompletedSucc();
- }
- m_terminaison[id_thread]=true;
- }
- while (isNotTerminated() && !m_finish);
- //cout<<"Thread id :"<<id_thread<<endl;
- pthread_barrier_wait(&m_barrier_builder);
-
+void* ModelCheckerTh::Compute_successors() {
+ int id_thread;
+ pthread_mutex_lock(&m_mutex);
+ id_thread = m_id_thread++;
+ pthread_mutex_unlock(&m_mutex);
+ Set fire;
+ int min_charge = 0;
+ if (id_thread == 0) {
+ LDDState *c = new LDDState;
+
+ MDD Complete_meta_state(Accessible_epsilon(m_initialMarking));
+ ldd_refs_push(Complete_meta_state);
+ MDD canonised_initial = Complete_meta_state; //Canonize(Complete_meta_state,0);
+ ldd_refs_push(canonised_initial);
+ fire = firable_obs(Complete_meta_state);
+ c->m_lddstate = canonised_initial;
+ c->setDeadLock(Set_Bloc(Complete_meta_state));
+ c->setDiv(Set_Div(Complete_meta_state));
+ m_st[0].push(Pair(couple(c, Complete_meta_state), fire));
+ m_graph->setInitialState(c);
+ m_graph->insert(c);
+ m_charge[0] = 1;
+ m_finish_initial = true;
+ }
+
+ LDDState *reached_class;
+ do {
+ while (!m_st[id_thread].empty() && !m_finish) {
+ m_terminaison[id_thread] = false;
+ pthread_spin_lock(&m_spin_stack[id_thread]);
+ Pair e = m_st[id_thread].top();
+ //pthread_spin_lock(&m_accessible);
+ m_st[id_thread].pop();
+ pthread_spin_unlock(&m_spin_stack[id_thread]);
+ m_charge[id_thread]--;
+ while (!e.second.empty() && !m_finish) {
+ int t = *e.second.begin();
+ e.second.erase(t);
+
+ if (id_thread) {
+ pthread_mutex_lock(&m_supervise_gc_mutex);
+ m_gc++;
+ if (m_gc == 1) {
+ pthread_mutex_lock(&m_gc_mutex);
+ }
+ pthread_mutex_unlock(&m_supervise_gc_mutex);
+ }
+
+ MDD Complete_meta_state = Accessible_epsilon(get_successor(e.first.second, t));
+
+ ldd_refs_push(Complete_meta_state);
+ MDD reduced_meta = Complete_meta_state; //Canonize(Complete_meta_state,0);
+ ldd_refs_push(reduced_meta);
+
+ if (id_thread == 0) {
+ pthread_mutex_lock(&m_gc_mutex);
+ // #ifdef DEBUG_GC
+ // displayMDDTableInfo();
+ // #endif // DEBUG_GC
+
+ sylvan_gc_seq();
+ // #ifdef DEBUG_GC
+ // displayMDDTableInfo();
+ // #endif // DEBUG_GC
+ pthread_mutex_unlock(&m_gc_mutex);
+ }
+ reached_class = new LDDState();
+ reached_class->m_lddstate = reduced_meta;
+ //reached_class->m_lddstate=reduced_meta;
+ //nbnode=bdd_pathcount(reached_class->m_lddstate);
+
+ //pthread_spin_lock(&m_accessible);
+ pthread_mutex_lock(&m_graph_mutex);
+
+ LDDState *pos = m_graph->find(reached_class);
+
+ if (!pos) {
+ // cout<<"not found"<<endl;
+ //reached_class->blocage=Set_Bloc(Complete_meta_state);
+ //reached_class->boucle=Set_Div(Complete_meta_state);
+
+ m_graph->addArc();
+ m_graph->insert(reached_class);
+ reached_class->setDiv(Set_Div(Complete_meta_state));
+ reached_class->setDeadLock(Set_Bloc(Complete_meta_state));
+ pthread_mutex_unlock(&m_graph_mutex);
+
+ 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));
+ //pthread_mutex_lock(&m_mutex);
+ fire = firable_obs(Complete_meta_state);
+ //if (max_succ<fire.size()) max_succ=fire.size();
+ //pthread_mutex_unlock(&m_mutex);
+ min_charge = minCharge();
+ //m_min_charge=(m_min_charge+1) % m_nb_thread;
+ pthread_spin_lock(&m_spin_stack[min_charge]);
+ m_st[min_charge].push(Pair(couple(reached_class, Complete_meta_state), fire));
+ pthread_spin_unlock(&m_spin_stack[min_charge]);
+ m_charge[min_charge]++;
+ } else {
+ m_graph->addArc();
+ pthread_mutex_unlock(&m_graph_mutex);
+ e.first.first->Successors.insert(e.first.first->Successors.begin(), LDDEdge(pos, t));
+ pos->Predecessors.insert(pos->Predecessors.begin(), LDDEdge(e.first.first, t));
+ delete reached_class;
+
+ }
+ if (id_thread) {
+ pthread_mutex_lock(&m_supervise_gc_mutex);
+ m_gc--;
+ if (m_gc == 0)
+ pthread_mutex_unlock(&m_gc_mutex);
+ pthread_mutex_unlock(&m_supervise_gc_mutex);
+ }
+ }
+ e.first.first->setCompletedSucc();
+ }
+ m_terminaison[id_thread] = true;
+ } while (isNotTerminated() && !m_finish);
+ //cout<<"Thread id :"<<id_thread<<endl;
+ pthread_barrier_wait(&m_barrier_builder);
+
}
-void * ModelCheckerTh::threadHandler(void *context)
-{
- return ((ModelCheckerTh*)context)->Compute_successors();
+void* ModelCheckerTh::threadHandler(void *context) {
+ return ((ModelCheckerTh*) context)->Compute_successors();
}
-void ModelCheckerTh::ComputeTh_Succ()
-{
-
-
- int rc;
-// m_graph=&g;
-// m_graph->setTransition(m_transitionName);
-// m_graph->setPlace(m_placeName);
- m_id_thread=0;
-
- pthread_mutex_init(&m_mutex, NULL);
- 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);
-
- for (int i=0; i<m_nb_thread; i++)
- {
- pthread_spin_init(&m_spin_stack[i], NULL);
- m_charge[i]=0;
- m_terminaison[i]=false;
- }
-
-
-
-
- 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;
- }
- }
+void ModelCheckerTh::ComputeTh_Succ() {
+
+ m_id_thread = 0;
+
+ pthread_mutex_init(&m_mutex, NULL);
+ 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);
+
+ for (int i = 0; i < m_nb_thread; i++) {
+ pthread_spin_init(&m_spin_stack[i], NULL);
+ m_charge[i] = 0;
+ m_terminaison[i] = false;
+ }
+
+ for (int i = 0; i < m_nb_thread; i++) {
+ int rc;
+ if ((rc = pthread_create(&m_list_thread[i], NULL, threadHandler, this))) {
+ cout << "error: pthread_create, rc: " << rc << endl;
+ }
+ }
}
ModelCheckerTh::~ModelCheckerTh() {
- 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);
- }
-
+ 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);
+ }
+
}
-int ModelCheckerTh::minCharge()
-{
- int pos=0;
- int min_charge=m_charge[0];
- for (int i=1; i<m_nb_thread; i++)
- {
- if (m_charge[i]<min_charge)
- {
- min_charge=m_charge[i];
- pos=i;
- }
- }
- return pos;
+int ModelCheckerTh::minCharge() {
+ int pos = 0;
+ int min_charge = m_charge[0];
+ for (int i = 1; i < m_nb_thread; i++) {
+ if (m_charge[i] < min_charge) {
+ min_charge = m_charge[i];
+ pos = i;
+ }
+ }
+ return pos;
}
-bool ModelCheckerTh::isNotTerminated()
-{
- bool res=true;
- int i=0;
- while (i<m_nb_thread && res)
- {
- res=m_terminaison[i];
- i++;
- }
- return !res;
+bool ModelCheckerTh::isNotTerminated() {
+ bool res = true;
+ int i = 0;
+ while (i < m_nb_thread && res) {
+ res = m_terminaison[i];
+ i++;
+ }
+ return !res;
}
diff --git a/src/main.cpp b/src/main.cpp
index 577dbce..d9d482e 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -21,6 +21,9 @@
#include <spot/twaalgos/translate.hh>
#include <spot/twaalgos/emptiness.hh>
#include <spot/tl/apcollect.hh>
+#include <spot/ta/taproduct.hh>
+#include <spot/twa/twaproduct.hh>
+#include <spot/twaalgos/gtec/gtec.hh>
#include "NewNet.h"
#include "SogTwa.h"
#include "SogKripke.h"
@@ -28,9 +31,6 @@
#include "SogKripkeTh.h"
#include "HybridKripke.h"
-
-
-
// #include "RdPBDD.h"
using namespace std;
@@ -39,327 +39,314 @@ using namespace std;
unsigned int nb_th;
int n_tasks, task_id;
spot::formula not_f;
-set<string> buildPropositions(const string &fileName)
-{
- string input;
- set<string> transitionSet;
- ifstream file(fileName);
- if (file.is_open())
- {
- getline (file,input);
- cout<<"Loaded formula : "<<input<<endl;
- file.close();
-
- }
- else
- {
- cout<<"Can not open formula file"<<endl;
- exit(0);
- }
-
- spot::parsed_formula pf = spot::parse_infix_psl(input);
- if (pf.format_errors(std::cerr))
- return transitionSet;
- spot::formula fo = pf.f;
- if (!fo.is_ltl_formula())
- {
- std::cerr << "Only LTL formulas are supported.\n";
- return transitionSet;
- }
- spot::atomic_prop_set *p_list=spot::atomic_prop_collect(fo,0);
- for (spot::atomic_prop_set::const_iterator i=p_list->begin(); i!=p_list->end(); i++)
- {
- transitionSet.insert((*i).ap_name());
- }
- print_spin_ltl(std::cout, fo)<<'\n';
- cout<<"Building formula negation\n";
- not_f = spot::formula::Not(pf.f);
- return transitionSet;
+set<string> buildPropositions(const string &fileName) {
+ string input;
+ set<string> transitionSet;
+ ifstream file(fileName);
+ if (file.is_open()) {
+ getline(file, input);
+ cout << "Loaded formula : " << input << endl;
+ file.close();
+
+ } else {
+ cout << "Can not open formula file" << endl;
+ exit(0);
+ }
+
+ spot::parsed_formula pf = spot::parse_infix_psl(input);
+ if (pf.format_errors(std::cerr))
+ return transitionSet;
+ spot::formula fo = pf.f;
+ if (!fo.is_ltl_formula()) {
+ std::cerr << "Only LTL formulas are supported.\n";
+ return transitionSet;
+ }
+ spot::atomic_prop_set *p_list = spot::atomic_prop_collect(fo, 0);
+ for (spot::atomic_prop_set::const_iterator i = p_list->begin(); i != p_list->end(); i++) {
+ transitionSet.insert((*i).ap_name());
+ }
+ print_spin_ltl(std::cout, fo) << '\n';
+ cout << "Building formula negation\n";
+ not_f = spot::formula::Not(pf.f);
+ return transitionSet;
}
-
+void displayCheckResult(bool res) {
+ if (res)
+ cout << "Property is verified..." << endl;
+ else
+ cout << "Property is violated..." << endl;
+}
+void displayTime(auto startTime, auto finalTime) {
+ cout << "Verification duration : " << std::chrono::duration_cast < std::chrono::milliseconds
+ > (finalTime - startTime).count() << " milliseconds\n";
+}
/***********************************************/
-int main(int argc, char** argv)
-{
- int choix;
- if(argc<3)
- return 0;
- char formula[100]="";
- char Int[100]="";
- strcpy(formula, argv[4]);
- if (argc > 6)
- strcpy(Int, argv[5]);
-
- //if(argc>5)
- nb_th = atoi(argv[2])==0 ? 1 : atoi(argv[2]);
-
- cout<<"Fichier net : "<<argv[3]<<endl;
- cout<<"Fichier formule : "<<formula<<endl;
- cout<<"Fichier Interface : "<<Int<<endl;
-
- cout<<"thread : "<<argv[2]<<endl;
- //strcpy(red,argv[5]);
- //cout<<"Reduce : "<<red<<endl;
-
- if(nb_th==0)
- {
- cout<<"number of thread <= 0 " <<endl;
- exit (0);
- }
-
- cout<<"______________________________________\n";
- cout<<"Fetching formula..."<<endl;
- set<string> list_propositions=buildPropositions(formula);
-
- NewNet Rnewnet(argv[3],list_propositions);
-
- MPI_Init (&argc, &argv );
- MPI_Comm_size(MPI_COMM_WORLD,&n_tasks);
- MPI_Comm_rank(MPI_COMM_WORLD,&task_id);
-
- if (n_tasks==1)
- {
- if (n_tasks==1 && (!strcmp(argv[1],"otfL") || !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 cout<<"Multi-threaded algorithm based on Lace framework!"<<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();
- }
- cout<<"Loading net information..."<<endl;
- ModelCheckBaseMT* mcl;
- if (!strcmp(argv[1],"otfL")) mcl=new ModelCheckLace(Rnewnet,nb_th);
- else
- mcl=new ModelCheckerTh(Rnewnet,nb_th);
- mcl->loadNet();
- double tps;
-
- auto t1 = std::chrono::high_resolution_clock::now();
-
- auto k =
- std::make_shared<SogKripkeTh>(d,mcl,Rnewnet.getListTransitionAP(),Rnewnet.getListPlaceAP());
-
- 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;
- auto t2 = std::chrono::high_resolution_clock::now();
- std::cout << "temps de verification "
- << std::chrono::duration_cast<std::chrono::milliseconds>(t2-t1).count()
- << " milliseconds\n";
-
- cout<<"=================================="<<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";
- auto t2 = std::chrono::high_resolution_clock::now();
- std::cout << "temps de verification "
- << std::chrono::duration_cast<std::chrono::milliseconds>(t2-t1).count()
- << " milliseconds\n";
- }
-
- delete mcl;
- }
-
-
- else
- {
- cout<<"number of task = 1 \n " <<endl;
- bool uselace=(!strcmp(argv[1],"lc")) || (!strcmp(argv[1],"l"));
- threadSOG DR(Rnewnet,nb_th,uselace);
- LDDGraph g(&DR);
-
- if (nb_th==1)
- {
- cout<<"******************Sequential version******************* \n" <<endl;
- DR.computeSeqSOG(g);
- g.printCompleteInformation();
- }
- else
- {
- cout<<"*******************Multithread version****************** \n" <<endl;
- if (!strcmp(argv[1],"p"))
- {
- cout<<"Construction with pthread library."<<endl;
- cout<<"Count of threads to be created: "<<nb_th<<endl;
- DR.computeDSOG(g,false);
- g.printCompleteInformation();
- }
- else if (!strcmp(argv[1],"pc"))
- {
- cout<<"Canonized construction with pthread library."<<endl;
- 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;
- cin>>c;
- if (c='y')
- {
- 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 ?";
- 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();
- }
- //auto k = std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP(),R.getListPlaceAP());
-
- spot::twa_graph_ptr k =
- spot::make_twa_graph(std::make_shared<SogKripke>(d,DR.getGraph(),Rnewnet.getListTransitionAP(),Rnewnet.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, k,"ka");
- file.close();
- }
- if (auto run = k->intersecting_run(af))
- {
- run->highlight(5);
- fstream file;
- file.open("violated.dot",fstream::out);
- cout<<"Property is violated"<<endl;
- cout<<"Check the dot file to get a violation run"<<endl;
- spot::print_dot(file, k, ".kA");
- file.close();
- }
- else
- std::cout << "formula is verified\n";
- }
-
- }
- }
-
- }
- if (n_tasks>1)
- {
- if(nb_th>1)
- {
- if (task_id==0) cout<<"**************Hybrid version**************** \n" <<endl;
- if (strcmp(argv[1],"otf"))
- {
- HybridSOG DR(Rnewnet);
- LDDGraph g(&DR);
- if (task_id==0) cout<<"Building the Distributed SOG by "<<n_tasks<<" processes..."<<endl;
- DR.computeDSOG(g);
- }
- else
- {
- n_tasks--;
- if (task_id==n_tasks)
- {
- cout<<"Model checking on the fly..."<<endl;
- cout<<" One process will perform Model checking"<<endl;
- cout<<n_tasks<<" process will build the Distributed SOG"<<endl;
- }
- MPI_Comm gprocess;
- MPI_Comm_split(MPI_COMM_WORLD,task_id==n_tasks?0:1,task_id,&gprocess);
- //cout<<" Task id "<<task_id<<"/"<<n_tasks<<endl;
- if (task_id!=n_tasks)
- {
- cout<<"N task :"<<n_tasks<<endl;
- MCHybridSOG DR(Rnewnet,gprocess,false);
- LDDGraph g(&DR);
- DR.computeDSOG(g);
- }
- else
- {
- cout<<"On the fly Model checker by process "<<task_id<<endl;
-
- auto d = spot::make_bdd_dict();
- spot::twa_graph_ptr af = spot::translator(d).run(not_f);
-
- double tps;
- auto t1 = std::chrono::high_resolution_clock::now();
- auto k =
- std::make_shared<HybridKripke>(d,Rnewnet.getListTransitionAP(),Rnewnet.getListPlaceAP(),Rnewnet);
- if (auto run = k->intersecting_run(af))
- {
- std::cout << "formula is violated by the following run:\n"<<*run<<endl;
- auto t2 = std::chrono::high_resolution_clock::now();
- std::cout << "temps de verification "
- << std::chrono::duration_cast<std::chrono::milliseconds>(t2-t1).count()
- << " milliseconds\n";
- cout<<"=================================="<<endl;
- }
- else
- {
- std::cout << "formula is verified\n";
- auto t2 = std::chrono::high_resolution_clock::now();
- std::cout << "temps de verification "
- << std::chrono::duration_cast<std::chrono::milliseconds>(t2-t1).count()
- << " milliseconds\n";
-
- }
- }
- }
- }
- else
- {
- cout<<"*************Distibuted version******************* \n" <<endl;
- {
- DistributedSOG DR(Rnewnet);
- LDDGraph g(nullptr);
- DR.computeDSOG(g);
- }
- }
- }
- MPI_Finalize();
- return (EXIT_SUCCESS);
+int main(int argc, char **argv) {
+ int choix;
+ if (argc < 3)
+ return 0;
+ char formula[100] = "";
+ char algorithm[100] = "";
+ strcpy(formula, argv[4]);
+ if (argc > 5) {
+ strcpy(algorithm, argv[5]);
+ }
+
+ nb_th = atoi(argv[2]) == 0 ? 1 : atoi(argv[2]);
+
+ cout << "Net file : " << argv[3] << endl;
+ cout << "Formula file : " << formula << endl;
+ cout << "Checking algorithm : " << algorithm << endl;
+
+ cout << "thread : " << argv[2] << endl;
+
+ if (nb_th == 0) {
+ cout << "number of thread <= 0 " << endl;
+ exit(0);
+ }
+
+ cout << "______________________________________\n";
+ cout << "Fetching formula..." << endl;
+ set<string> list_propositions = buildPropositions(formula);
+
+ NewNet Rnewnet(argv[3], list_propositions);
+
+ MPI_Init(&argc, &argv);
+ MPI_Comm_size(MPI_COMM_WORLD, &n_tasks);
+ MPI_Comm_rank(MPI_COMM_WORLD, &task_id);
+
+ if (n_tasks == 1) {
+ if (n_tasks == 1 && (!strcmp(argv[1], "otfL") || !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
+ cout << "Multi-threaded algorithm based on Lace framework!" << 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();
+ }
+ cout << "Loading net information..." << endl;*/
+ ModelCheckBaseMT *mcl;
+ if (!strcmp(argv[1], "otfL"))
+ mcl = new ModelCheckLace(Rnewnet, nb_th);
+ else
+ mcl = new ModelCheckerTh(Rnewnet, nb_th);
+ mcl->loadNet();
+ auto k = std::make_shared<SogKripkeTh>(d, mcl, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP());
+ cout << "Performing on the fly Modelchecking" << endl;
+ if (!strcmp(algorithm, "couv")) {
+ cout << "Couvreur99 algorithm..." << endl;
+ std::shared_ptr < spot::twa_product > product = make_shared<spot::twa_product>(af, k);
+ spot::couvreur99_check check = spot::couvreur99_check(product);
+ auto startTime = std::chrono::high_resolution_clock::now();
+ bool res = (check.check() == 0);
+ auto finalTime = std::chrono::high_resolution_clock::now();
+ displayTime(startTime, finalTime);
+ displayCheckResult(res);
+
+ } else {
+ auto startTime = std::chrono::high_resolution_clock::now();
+ bool res = (k->intersecting_run(af) == 0);
+ auto finalTime = std::chrono::high_resolution_clock::now();
+ displayTime(startTime, finalTime);
+ displayCheckResult(res);
+ /*
+ if (!resauto run = k->intersecting_run(af)) {
+ 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);
+ 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";
+ auto finalTime = std::chrono::high_resolution_clock::now();
+ displayTime(startTime, finalTime);
+
+ }*/
+ }
+ delete mcl;
+ }
+
+ else {
+ cout << "number of task = 1 \n " << endl;
+ bool uselace = (!strcmp(argv[1], "lc")) || (!strcmp(argv[1], "l"));
+ threadSOG DR(Rnewnet, nb_th, uselace);
+ LDDGraph g(&DR);
+
+ if (nb_th == 1) {
+ cout << "******************Sequential version******************* \n" << endl;
+ DR.computeSeqSOG(g);
+ g.printCompleteInformation();
+ } else {
+ cout << "*******************Multithread version****************** \n" << endl;
+ if (!strcmp(argv[1], "p")) {
+ cout << "Construction with pthread library." << endl;
+ cout << "Count of threads to be created: " << nb_th << endl;
+ DR.computeDSOG(g, false);
+ g.printCompleteInformation();
+ } else if (!strcmp(argv[1], "pc")) {
+ cout << "Canonized construction with pthread library." << endl;
+ 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;
+ cin >> c;
+ if (c == 'y') {
+ 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 ?";
+ 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();
+ }
+ //auto k = std::make_shared<SogKripke>(d,DR.getGraph(),R.getListTransitionAP(),R.getListPlaceAP());
+
+ spot::twa_graph_ptr k = spot::make_twa_graph(
+ std::make_shared<SogKripke>(d, DR.getGraph(), Rnewnet.getListTransitionAP(), Rnewnet.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, k, "ka");
+ file.close();
+ }
+ if (auto run = k->intersecting_run(af)) {
+ run->highlight(5);
+ fstream file;
+ file.open("violated.dot", fstream::out);
+ cout << "Property is violated" << endl;
+ cout << "Check the dot file to get a violation run" << endl;
+ spot::print_dot(file, k, ".kA");
+ file.close();
+ } else
+ std::cout << "formula is verified\n";
+ }
+
+ }
+ }
+
+ }
+ if (n_tasks > 1) {
+ if (nb_th > 1) {
+ if (task_id == 0)
+ cout << "**************Hybrid version**************** \n" << endl;
+ if (strcmp(argv[1], "otf")) {
+ HybridSOG DR(Rnewnet);
+ LDDGraph g(&DR);
+ if (task_id == 0)
+ cout << "Building the Distributed SOG by " << n_tasks << " processes..." << endl;
+ DR.computeDSOG(g);
+ } else {
+ n_tasks--;
+ if (task_id == n_tasks) {
+ cout << "Model checking on the fly..." << endl;
+ cout << " One process will perform Model checking" << endl;
+ cout << n_tasks << " process will build the Distributed SOG" << endl;
+ }
+ MPI_Comm gprocess;
+ MPI_Comm_split(MPI_COMM_WORLD, task_id == n_tasks ? 0 : 1, task_id, &gprocess);
+ //cout<<" Task id "<<task_id<<"/"<<n_tasks<<endl;
+ if (task_id != n_tasks) {
+ cout << "N task :" << n_tasks << endl;
+ MCHybridSOG DR(Rnewnet, gprocess, false);
+ LDDGraph g(&DR);
+ DR.computeDSOG(g);
+ } else {
+ cout << "************************************" << endl;
+ cout << "On the fly Model checker by process " << task_id << endl;
+ auto d = spot::make_bdd_dict();
+ spot::twa_graph_ptr af = spot::translator(d).run(not_f);
+ auto k = std::make_shared<HybridKripke>(d, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP(), Rnewnet);
+ if (!strcmp(algorithm,"couv")) {
+ std::shared_ptr < spot::twa_product > product = make_shared<spot::twa_product>(af, k);
+ spot::couvreur99_check check = spot::couvreur99_check(product);
+ auto startTime = std::chrono::high_resolution_clock::now();
+ bool res = (check.check() == 0);
+ auto finalTime = std::chrono::high_resolution_clock::now();
+ displayTime(startTime, finalTime);
+ displayCheckResult(res);
+ } else {
+ auto startTime = std::chrono::high_resolution_clock::now();
+ bool res= (k->intersecting_run(af)==0);
+ auto finalTime = std::chrono::high_resolution_clock::now();
+ displayTime(startTime, finalTime);
+ displayCheckResult(res);
+ }
+
+ /*if (auto run = k->intersecting_run(af))
+ {
+ std::cout << "formula is violated by the following run:\n"<<*run<<endl;
+ auto t2 = std::chrono::high_resolution_clock::now();
+ std::cout << "temps de verification "
+ << std::chrono::duration_cast<std::chrono::milliseconds>(t2-t1).count()
+ << " milliseconds\n";
+ cout<<"=================================="<<endl;
+ }
+ else
+ {
+ std::cout << "formula is verified\n";
+ auto t2 = std::chrono::high_resolution_clock::now();
+ std::cout << "temps de verification "
+ << std::chrono::duration_cast<std::chrono::milliseconds>(t2-t1).count()
+ << " milliseconds\n";
+
+ }*/
+ }
+ }
+ } else {
+ cout << "*************Distibuted version******************* \n" << endl;
+ {
+ DistributedSOG DR(Rnewnet);
+ LDDGraph g(nullptr);
+ DR.computeDSOG(g);
+ }
+ }
+ }
+ MPI_Finalize();
+ return (EXIT_SUCCESS);
}
--
GitLab