diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index a042d27f9947f696921e586c1d8ade70a4034042..4a476dd2cd49c0eb5e8c05334843f7488fda8c6e 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -66,6 +66,14 @@ add_executable(hybrid-sog main.cpp
SogKripkeIteratorOTF.h
SogKripkeOTF.cpp
SogKripkeOTF.h
+ SogKripkeTh.cpp
+ SogKripkeTh.h
+ SogKripkeStateTh.cpp
+ SogKripkeStateTh.h
+ SogKripkeIteratorTh.cpp
+ SogKripkeIteratorTh.h
+ ModelCheckerTh.cpp
+ ModelCheckerTh.h
)
target_link_libraries(hybrid-sog
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..013532a069ea10d89456fc8fa21a350b3e3213e3
--- /dev/null
+++ b/src/ModelCheckerTh.cpp
@@ -0,0 +1,289 @@
+#include "ModelCheckerTh.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;
+ }
+
+
+
+ cout<<"Transitions observables :"<<endl;
+ Set::iterator it=m_observable.begin();
+ for (; it!=m_observable.end(); it++)
+ {
+ cout<<*it<<" ";
+ }
+ cout<<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()
+{ Set fire;
+
+ LDDState *c=new LDDState;
+ LDDState *reached_class;
+ 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_old_size=lddmc_nodecount(c->m_lddstate);
+ m_graph->setInitialState(c);
+ m_graph->insert(c);
+
+ // Compute successors
+
+ /* 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=Accessible_epsilon(it);
+ reached_class=new LDDState;
+ reached_class->m_lddstate=Complete_meta_state;
+ m_graph->addArc();
+ m_graph->insert(reached_class);
+ c->Successors.insert(c->Successors.begin(),LDDEdge(reached_class,t));
+ reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(c,t));
+ } */
+
+ return c;
+}
+
+void ModelCheckerTh::buildSucc(LDDState *agregate)
+{
+ if (!agregate->isVisited()) {
+ agregate->setVisited();
+ LDDState *reached_class=nullptr;
+
+}
+}
+
+/*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);
+ Set fire;
+ LDDState* reached_class;
+ // size_t max_meta_state_size;
+ // int min_charge;
+ do
+ {
+
+ while (!m_st[id_thread].empty())
+ {
+
+ nb_it++;
+ 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_nbmetastate--;
+
+ 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);
+
+ if (id_thread==0)
+ {
+ pthread_mutex_lock(&m_gc_mutex);
+ sylvan_gc_seq();
+
+ pthread_mutex_unlock(&m_gc_mutex);
+ }
+ reached_class->m_lddstate=Complete_meta_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);
+
+ 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_nbmetastate++;
+ //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);
+ m_min_charge= minCharge();
+ //m_min_charge=(m_min_charge+1) % m_nb_thread;
+ pthread_spin_lock(&m_spin_stack[m_min_charge]);
+ m_st[m_min_charge].push(Pair(couple(reached_class,Complete_meta_state),fire));
+ pthread_spin_unlock(&m_spin_stack[m_min_charge]);
+ m_charge[m_min_charge]++;
+ }
+ else
+ {
+ nb_failed++;
+ 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);
+ }
+ }
+ }
+ m_terminaison[id_thread]=true;
+
+
+
+ }
+ while (isNotTerminated());
+ //cout<<"Thread :"<<id_thread<<" has performed "<<nb_it<<" itérations avec "<<nb_failed<<" échecs"<<endl;
+ //cout<<"Max succ :"<<max_succ<<endl;
+}
+
+
+void * ModelCheckerTh::threadHandler(void *context)
+{
+ return ((ModelCheckerTh*)context)->Compute_successors();
+} */
diff --git a/src/ModelCheckerTh.h b/src/ModelCheckerTh.h
new file mode 100644
index 0000000000000000000000000000000000000000..12bb4a635ee46e5b149bca7590b268a5fbc858af
--- /dev/null
+++ b/src/ModelCheckerTh.h
@@ -0,0 +1,36 @@
+#ifndef MODELCHECKERTH_H
+#define MODELCHECKERTH_H
+#include "CommonSOG.h"
+class ModelCheckerTh : public CommonSOG
+{
+public:
+ ModelCheckerTh(const NewNet &R, int BOUND,int nbThread);
+ LDDState * buildInitialMetaState();
+ string getTransition(int pos);
+ string getPlace(int pos);
+ void buildSucc(LDDState *agregate);
+ // static void *threadHandler(void *context);
+ // void *Compute_successors();
+
+
+
+private:
+ int m_nb_thread;
+ MDD m_initalMarking;
+
+ pile m_st[128];
+ int m_charge[128];
+ bool m_terminaison[128];
+
+
+ pthread_mutex_t m_mutex;
+ pthread_mutex_t m_graph_mutex;
+ pthread_mutex_t m_gc_mutex;
+ pthread_mutex_t m_supervise_gc_mutex;
+ unsigned int m_gc;
+
+ pthread_mutex_t m_mutex_stack[128];
+ pthread_spinlock_t m_spin_stack[128];
+ pthread_t m_list_thread[128];
+};
+#endif
diff --git a/src/main.cpp b/src/main.cpp
index 7dc13f6a179ad529ac7db51526e408f595587324..4c29dd70af7565b735485b63d2845710cab4a404 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -13,6 +13,7 @@
#include "HybridSOG.h"
#include "LDDGraph.h"
#include "ModelCheckLace.h"
+#include "ModelCheckerTh.h"
#include <spot/misc/version.hh>
#include <spot/twaalgos/dot.hh>
@@ -25,6 +26,7 @@
#include "SogTwa.h"
#include "SogKripke.h"
#include "SogKripkeOTF.h"
+#include "SogKripkeTh.h"
@@ -125,7 +127,7 @@ int main(int argc, char** argv)
MPI_Comm_rank(MPI_COMM_WORLD,&task_id);
//
- if (n_tasks==1 && !strcmp(argv[1],"otf"))
+ if (n_tasks==1 && !strcmp(argv[1],"otfL"))
{
cout<<"Multi-threaded on the fly Model checking..."<<endl;
cout<<"Building automata for not(formula)\n";
@@ -168,6 +170,50 @@ int main(int argc, char** argv)
std::cout << "formula is verified\n";
}
+ else if (n_tasks==1 && !strcmp(argv[1],"otfTh"))
+ {
+ cout<<"Multi-threaded on the fly Model checking..."<<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 ?";
+ 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);
+ cout<<"Created"<<endl;
+ auto k =
+ std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()); ;
+ // Performing on the fly Modelchecking
+ 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;
+ /*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)
{
cout<<"number of task = 1 \n " <<endl;