Skip to content
Snippets Groups Projects
Commit 3178c63e authored by Chiheb Amer Abid's avatar Chiheb Amer Abid
Browse files

Deleted useless files

parent 5c35ef87
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/ModelCheckLace.h
+ 1
− 1
View file @ 3178c63e
......@@ -7,7 +7,7 @@ public:
LDDState * buildInitialMetaState();
void buildSucc(LDDState *agregate);
private:
void preConfigure();
void preConfigure();
};
#endif
src/ModelChecker.cpp deleted 100644 → 0
+ 0
− 11
View file @ 5c35ef87
#include "ModelChecker.h"
ModelChecker::ModelChecker()
{
//ctor
}
ModelChecker::~ModelChecker()
{
//dtor
}
src/ModelChecker.h deleted 100644 → 0
+ 0
− 16
View file @ 5c35ef87
#ifndef MODELCHECKER_H
#define MODELCHECKER_H
class ModelChecker
{
public:
ModelChecker();
virtual ~ModelChecker();
protected:
private:
};
#endif // MODELCHECKER_H
src/ModelCheckerBase.cpp deleted 100644 → 0
+ 0
− 248
View file @ 5c35ef87
#include "ModelCheckerBase.h"
#include "sylvan.h"
#include "sylvan_seq.h"
#include <sylvan_sog.h>
#include <sylvan_int.h>
using namespace sylvan;
ModelCheckerTh::ModelCheckerTh(const NewNet &R, int BOUND,int nbThread)
{
m_nb_thread=nbThread;
lace_init(1, 0);
lace_startup(0, NULL, NULL);
sylvan_set_limits(2LL<<30, 16, 3);
sylvan_init_package();
sylvan_init_ldd();
// LACE_ME;
m_net=R;
int i;
vector<Place>::const_iterator it_places;
init_gc_seq();
//_______________
transitions=R.transitions;
m_observable=R.Observable;
m_place_proposition=R.m_formula_place;
m_nonObservable=R.NonObservable;
m_transitionName=R.transitionName;
m_placeName=R.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=R.InterfaceTrans;
m_nbPlaces=R.places.size();
cout<<"Nombre de places : "<<m_nbPlaces<<endl;
cout<<"Derniere place : "<<R.places[m_nbPlaces-1].name<<endl;
uint32_t * liste_marques=new uint32_t[R.places.size()];
for(i=0,it_places=R.places.begin(); it_places!=R.places.end(); i++,it_places++)
{
liste_marques[i] =it_places->marking;
}
m_initalMarking=lddmc_cube(liste_marques,R.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=R.transitions.begin();
t!=R.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;
m_graph=new LDDGraph(this);
m_graph->setTransition(m_transitionName);
m_graph->setPlace(m_placeName);
}
string ModelCheckerTh::getTransition(int pos)
{
return m_graph->getTransition(pos);
}
string ModelCheckerTh::getPlace(int pos)
{
return m_graph->getPlace(pos);
}
LDDState * ModelCheckerTh::buildInitialMetaState()
{
ComputeTh_Succ();
LDDState *c=new LDDState;
MDD initial_meta_state=Accessible_epsilon(m_initalMarking);
ldd_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;
}
void ModelCheckerTh::buildSucc(LDDState *agregate)
{
if (!agregate->isVisited())
{
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);
//Wait for all threads to finish their work
}
}
void * ModelCheckerTh::Compute_successors()
{
int id_thread;
int nb_it=0,nb_failed=0,max_succ=0;
pthread_mutex_lock(&m_mutex);
id_thread=m_id_thread++;
pthread_mutex_unlock(&m_mutex);
LDDState* reached_class=nullptr;
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;
pthread_mutex_lock(&m_graph_mutex);
LDDState* pos=m_graph->find(reached_class);
if(!pos)
{
m_graph->addArc();
m_graph->insert(reached_class);
pthread_mutex_unlock(&m_graph_mutex);
aggregate->Successors.insert(aggregate->Successors.begin(),LDDEdge(reached_class,transition));
reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(aggregate,transition));
}
else
{
m_graph->addArc();
pthread_mutex_unlock(&m_graph_mutex);
aggregate->Successors.insert(aggregate->Successors.begin(),LDDEdge(pos,transition));
pos->Predecessors.insert(pos->Predecessors.begin(),LDDEdge(aggregate,transition));
delete reached_class;
}
}
pthread_barrier_wait(&m_barrier_builder);
}
while (!m_finish);
}
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++)
{
if ((rc = pthread_create(&m_list_thread[i], NULL,threadHandler,this)))
{
cout<<"error: pthread_create, rc: "<<rc<<endl;
}
}
/* Compute_successors();
for (int i = 0; i < m_nb_thread-1; i++)
{
pthread_join(m_list_thread[i], NULL);
}*/
}
ModelCheckerTh::~ModelCheckerTh() {
m_finish=true;
pthread_barrier_wait(&m_barrier_threads);
pthread_barrier_wait(&m_barrier_builder);
for (int i = 0; i < m_nb_thread-1; i++)
{
pthread_join(m_list_thread[i], NULL);
}
}
src/ModelCheckerBase.h deleted 100644 → 0
+ 0
− 24
View file @ 5c35ef87
#ifndef MODELCHECKERBASE_H
#define MODELCHECKERBASE_H
#include "CommonSOG.h"
typedef pair<LDDState *, int> couple_th;
typedef stack<pair<LDDState *,int>> pile_t;
class ModelCheckerBase : public CommonSOG
{
public:
virtual ModelCheckerTh(const NewNet &R, int BOUND,int nbThread);
virtual ~ModelCheckerTh();
LDDState * buildInitialMetaState();
void buildSucc(LDDState *agregate);
void *Compute_successors();
void ComputeTh_Succ();
private:
MDD m_initalMarking;
};
#endif
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment