diff --git a/README.md b/README.md
index 77db7b8394d540fc658d43c2efd96bfaed75e6a4..79810f39ebba8d2de4bfc1d921548fa5077aa2ec 100644
--- a/README.md
+++ b/README.md
@@ -13,7 +13,6 @@ BuDDy used for sequential version and Sylvan for both sequential and parallel co
It is necessary to install Spot [Spot](https://spot.lrde.epita.fr/install.html).
-# Hybrid-SOG
## Description
This repository hosts the experiments and results for the Hybrid (MPI/pthreads) approach for the SOG construction and provides a short guide on how to install the tools and reproduce the results.
@@ -48,7 +47,8 @@ arg1: specifies method of creating threads or/and specifies if modelchecking sho
* pc : using pthread library and applying canonization on nodes
* l : using lace framework
* lc : using lace framework and applying canonization on nodes
- * otf : perform modelchecking on the fly using laceframework
+ * otfL : perform modelchecking on the fly using laceframework
+ * otfP : perform modelchecking on the fly using pthread
arg2: specifies the number of threads/workers to be created
arg3: specifies the net to build its SOG
arg4: specifies the LTL formula file
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..55925ec7565590f222c4af507489bda1dbb8346c
--- /dev/null
+++ b/src/ModelCheckerTh.cpp
@@ -0,0 +1,303 @@
+#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_graph->setInitialState(c);
+ m_graph->insert(c);
+ m_st[0].push(c);
+ ComputeTh_Succ();
+ return c;
+}
+
+void ModelCheckerTh::buildSucc(LDDState *agregate)
+{
+ if (!agregate->isVisited())
+ {
+ agregate->setVisited();
+ m_min_charge=minCharge();
+ pthread_spin_lock(&m_spin_stack[m_min_charge]);
+ m_st[m_min_charge].push(agregate);
+ pthread_spin_unlock(&m_spin_stack[m_min_charge]);
+
+ }
+}
+
+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=nullptr;
+ // 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]);
+ LDDState* agregate=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--;
+ MDD meta_state=agregate->getLDDValue();
+ Set fire=firable_obs(meta_state);
+
+ //compute successors
+ Set::const_iterator iter=fire.begin();
+ while(iter!=fire.end())
+ {
+ int t = *iter;
+
+ MDD complete_state=Accessible_epsilon(get_successor(meta_state,t));
+ iter++;
+ 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);
+
+ 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();
+ pthread_mutex_unlock(&m_graph_mutex);
+ agregate->Successors.insert(agregate->Successors.begin(),LDDEdge(pos,t));
+ pos->Predecessors.insert(pos->Predecessors.begin(),LDDEdge(agregate,t));
+ delete reached_class;
+ }
+ }
+
+
+ }
+ m_terminaison[id_thread]=true;
+
+
+
+ }
+ while (isNotTerminated());
+
+}
+
+bool ModelCheckerTh::isNotTerminated()
+{
+ bool res=true;
+ int i=0;
+ while (i<m_nb_thread && res)
+ {
+ res=m_terminaison[i];
+ i++;
+ }
+ return !res;
+}
+
+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;
+
+}
+
+void * ModelCheckerTh::threadHandler(void *context)
+{
+ return ((ModelCheckerTh*)context)->Compute_successors();
+}
+
+void ModelCheckerTh::ComputeTh_Succ(){
+
+ cout << "number of threads "<<m_nb_thread<<endl;
+ 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);
+ m_gc=0;
+ 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-1; 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);
+ }
+
+
+}
diff --git a/src/ModelCheckerTh.h b/src/ModelCheckerTh.h
new file mode 100644
index 0000000000000000000000000000000000000000..2d31b0319537583cb9ee2c8752f5132d1191e9d5
--- /dev/null
+++ b/src/ModelCheckerTh.h
@@ -0,0 +1,41 @@
+#ifndef MODELCHECKERTH_H
+#define MODELCHECKERTH_H
+#include "CommonSOG.h"
+typedef stack<LDDState *> pile_t;
+
+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();
+ void ComputeTh_Succ();
+ int minCharge();
+ bool isNotTerminated();
+
+
+private:
+ int m_nb_thread;
+ MDD m_initalMarking;
+ int m_min_charge;
+ pile_t m_st[128];
+ int m_charge[128];
+ bool m_terminaison[128];
+ int m_id_thread;
+
+
+ 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/SogKripkeIteratorTh.cpp b/src/SogKripkeIteratorTh.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..d6ae60ab5236533cd2950b48c15820dae38c6000
--- /dev/null
+++ b/src/SogKripkeIteratorTh.cpp
@@ -0,0 +1,76 @@
+#include <spot/kripke/kripke.hh>
+#include "LDDGraph.h"
+#include "SogKripkeStateTh.h"
+#include "SogKripkeIteratorTh.h"
+
+
+SogKripkeIteratorTh::SogKripkeIteratorTh(const LDDState* lddstate, bdd cnd):m_lddstate(lddstate), kripke_succ_iterator(cnd)
+{
+
+ m_lddstate->setDiv(true);
+ for (int i=0;i<m_lddstate->getSuccessors()->size();i++) {
+ m_lsucc.push_back(m_lddstate->getSuccessors()->at(i));
+ }
+ /* if (lddstate->isDeadLock()) {
+ m_lsucc.push_back(pair(,-1));
+ }*/
+ if (lddstate->isDiv()) {
+ m_lsucc.push_back(pair<LDDState*,int>(m_lddstate,-1));
+ }
+
+}
+bool SogKripkeIteratorTh::first() {
+
+ // cout<<"entering "<<__func__<<endl;
+ m_current_edge=0;
+ //cout<<"exciting "<<__func__<<endl;
+ return m_lsucc.size()!=0;
+
+}
+
+bool SogKripkeIteratorTh::next() {
+ //cout<<"entering "<<__func__<<endl;
+ m_current_edge++;
+ return m_current_edge<m_lsucc.size();
+
+}
+
+bool SogKripkeIteratorTh::done() const {
+ //cout<<"entring /excit"<<__func__<<endl;
+ return m_current_edge==m_lsucc.size();
+
+}
+
+SogKripkeStateTh* SogKripkeIteratorTh::dst() const
+ {
+ //cout<<"enter/excit "<<__func__<<endl;
+ return new SogKripkeStateTh(m_lsucc.at(m_current_edge).first);
+ }
+
+bdd SogKripkeIteratorTh::cond() const {
+ //cout<<"entering "<<__func__<<endl;
+ if (m_lsucc.at(m_current_edge).second==-1) return bddtrue;
+
+ string name=m_builder->getTransition(m_lsucc.at(m_current_edge).second);
+ //cout<<"Value "<<m_lddstate->getSuccessors()->at(m_current_edge).second<<" Transition name "<<name<<endl;
+
+ spot::bdd_dict *p=m_dict_ptr->get();
+ spot::formula f=spot::formula::ap(name);
+ bdd result=bdd_ithvar((p->var_map.find(f))->second);
+
+ //cout<<"Iterator "<<__func__<<" "<<m_current_edge<<"\n";*/
+ //cout<<"exciting "<<__func__<<endl;
+ return result & spot::kripke_succ_iterator::cond();
+}
+
+/*spot::acc_cond::mark_t SogKripkeIterator::acc() const {
+ //cout<<"Iterator acc()\n";
+ return 0U;
+}*/
+SogKripkeIteratorTh::~SogKripkeIteratorTh()
+{
+ //dtor
+}
+
+static ModelCheckerTh * SogKripkeIteratorTh::m_builder;
+static spot::bdd_dict_ptr* SogKripkeIteratorTh::m_dict_ptr;
diff --git a/src/SogKripkeIteratorTh.h b/src/SogKripkeIteratorTh.h
new file mode 100644
index 0000000000000000000000000000000000000000..b3624d6be8d978eb81bb81169c8012e230bbafde
--- /dev/null
+++ b/src/SogKripkeIteratorTh.h
@@ -0,0 +1,39 @@
+#ifndef SOGKRIPKEITERATORTH_H_INCLUDED
+#define SOGKRIPKEITERATORTH_H_INCLUDED
+#include "SogKripkeStateTh.h"
+#include "ModelCheckerTh.h"
+#include <spot/kripke/kripke.hh>
+// Iterator for a SOG graph
+class SogKripkeIteratorTh : public spot::kripke_succ_iterator
+{
+public:
+
+ static ModelCheckerTh * m_builder;
+ static spot::bdd_dict_ptr* m_dict_ptr;
+ // sog_succ_iterator(const RdPBDD& pn, const SogKripkeState& s, const bdd& c);
+ SogKripkeIteratorTh(const LDDState* lddstate, bdd cnd);
+ virtual ~SogKripkeIteratorTh();
+ bool first() override;
+ bool next() override;
+ bool done() const override;
+ SogKripkeStateTh* dst() const override;
+ bdd cond() const override final;
+
+ SogKripkeStateTh* current_state() const;
+
+ bdd current_condition() const;
+
+ int current_transition() const;
+
+ bdd current_acceptance_conditions() const;
+
+ std::string format_transition() const;
+
+private:
+ LDDState * m_lddstate;
+ vector<pair<LDDState*, int>> m_lsucc;
+ unsigned int m_current_edge=0;
+};
+
+
+#endif // SOGKRIPKEITERATOR_H_INCLUDED
diff --git a/src/SogKripkeStateTh.cpp b/src/SogKripkeStateTh.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..76c38845a939bbf61a9c9ba4c2aca9f92add023a
--- /dev/null
+++ b/src/SogKripkeStateTh.cpp
@@ -0,0 +1,11 @@
+#include <spot/kripke/kripke.hh>
+#include "LDDState.h"
+#include "SogKripkeStateTh.h"
+
+
+SogKripkeStateTh::~SogKripkeStateTh()
+{
+ //dtor
+}
+
+static ModelCheckerTh * SogKripkeStateTh::m_builder;
diff --git a/src/SogKripkeStateTh.h b/src/SogKripkeStateTh.h
new file mode 100644
index 0000000000000000000000000000000000000000..48d64ff99e8eab4d4981030c3548ca76976c81ef
--- /dev/null
+++ b/src/SogKripkeStateTh.h
@@ -0,0 +1,46 @@
+#ifndef SOGKRIPKESTATETH_H_INCLUDED
+#define SOGKRIPKESTATETH_H_INCLUDED
+
+
+#include "LDDState.h"
+#include "ModelCheckerTh.h"
+
+class SogKripkeStateTh : public spot::state
+{
+public:
+ static ModelCheckerTh * m_builder;
+ SogKripkeStateTh(LDDState *st):m_state(st) {
+ m_builder->buildSucc(st);
+ };
+ virtual ~SogKripkeStateTh();
+
+ SogKripkeStateTh* clone() const override
+ {
+ return new SogKripkeStateTh(m_state);
+ }
+ size_t hash() const override
+ {
+ return m_state->getLDDValue();
+ }
+
+ int compare(const spot::state* other) const override
+ {
+ auto o = static_cast<const SogKripkeStateTh*>(other);
+ size_t oh = o->hash();
+ size_t h = hash();
+ if (h < oh)
+ return -1;
+ else
+ return h > oh;
+ }
+ LDDState* getLDDState() {
+ return m_state;
+ }
+protected:
+
+private:
+ LDDState *m_state;
+};
+
+
+#endif // SOGKRIPKESTATE_H_INCLUDED
diff --git a/src/SogKripkeTh.cpp b/src/SogKripkeTh.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..0e5f86d8b685cb91688e6bc79166b462147b22f3
--- /dev/null
+++ b/src/SogKripkeTh.cpp
@@ -0,0 +1,86 @@
+#include <spot/twaalgos/dot.hh>
+#include <spot/twaalgos/hoa.hh>
+#include <spot/kripke/kripke.hh>
+#include <spot/twa/bdddict.hh>
+
+
+#include "SogKripkeIteratorTh.h"
+#include "SogKripkeStateTh.h"
+
+#include "SogKripkeTh.h"
+#include <map>
+using namespace spot;
+SogKripkeTh::SogKripkeTh(const bdd_dict_ptr &dict_ptr,ModelCheckerTh *builder): spot::kripke(dict_ptr),m_builder(builder)
+{
+ SogKripkeIteratorTh::m_builder=builder;
+ SogKripkeStateTh::m_builder=builder;
+ SogKripkeIteratorTh::m_dict_ptr=&dict_ptr;
+ //cout<<__func__<<endl;
+}
+
+SogKripkeTh::SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckerTh *builder,set<string> &l_transap,set<string> &l_placeap):SogKripkeTh(dict_ptr,builder) {
+
+ for (auto it=l_transap.begin();it!=l_transap.end();it++) {
+ register_ap(*it);
+ }
+ for (auto it=l_placeap.begin();it!=l_placeap.end();it++)
+ register_ap(*it);
+
+}
+
+
+state* SogKripkeTh::get_init_state() const {
+ // cout<<__func__<<endl;
+ return new SogKripkeStateTh(m_builder->buildInitialMetaState());//new SpotSogState();
+
+}
+// Allows to print state label representing its id
+std::string SogKripkeTh::format_state(const spot::state* s) const
+ {
+ //cout<<__func__<<endl;
+ auto ss = static_cast<const SogKripkeStateTh*>(s);
+ std::ostringstream out;
+ out << "( " << ss->getLDDState()->getLDDValue() << ")";
+ // cout << " ( " << ss->getLDDState()->getLDDValue() << ")";
+ return out.str();
+ }
+
+SogKripkeIteratorTh* SogKripkeTh::succ_iter(const spot::state* s) const {
+ // cout<<__func__<<endl;
+
+ auto ss = static_cast<const SogKripkeStateTh*>(s);
+ //////////////////////////////////////////////
+
+ return new SogKripkeIteratorTh(ss->getLDDState(),state_condition(ss));//,b);//s state_condition(ss));
+}
+
+bdd SogKripkeTh::state_condition(const spot::state* s) const
+ {
+
+ auto ss = static_cast<const SogKripkeStateTh*>(s);
+ vector<int> marked_place=ss->getLDDState()->getMarkedPlaces(m_builder->getPlaceProposition());
+
+
+ bdd result=bddtrue;
+ // Marked places
+ for (auto it=marked_place.begin();it!=marked_place.end();it++) {
+ string name=m_builder->getPlace(*it);
+ spot::formula f=spot::formula::ap(name);
+ result&=bdd_ithvar((dict_->var_map.find(f))->second);
+ }
+ vector<int> unmarked_place=ss->getLDDState()->getUnmarkedPlaces(m_builder->getPlaceProposition());
+ for (auto it=unmarked_place.begin();it!=unmarked_place.end();it++) {
+ string name=m_builder->getPlace(*it);
+ spot::formula f=spot::formula::ap(name);
+ result&=!bdd_ithvar((dict_->var_map.find(f))->second);
+ }
+
+ return result;
+ }
+
+
+SogKripkeTh::~SogKripkeTh()
+{
+ //dtor
+}
+
diff --git a/src/SogKripkeTh.h b/src/SogKripkeTh.h
new file mode 100644
index 0000000000000000000000000000000000000000..4f4a114286a9b024fefcb7f5b697f9344b7e6b06
--- /dev/null
+++ b/src/SogKripkeTh.h
@@ -0,0 +1,34 @@
+#ifndef SOGKRIPKETH_H_INCLUDED
+#define SOGKRIPKETH_H_INCLUDED
+#include "LDDGraph.h"
+#include "SogKripkeIteratorTh.h"
+#include <spot/kripke/kripke.hh>
+#include <LDDGraph.h>
+#include <NewNet.h>
+
+
+class SogKripkeTh: public spot::kripke {
+ public:
+
+ SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckerTh *builder);
+ SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckerTh *builder,set<string> &l_transap,set<string> &l_placeap);
+ virtual ~SogKripkeTh();
+ spot::state* get_init_state() const;
+ SogKripkeIteratorTh* succ_iter(const spot::state* s) const override;
+ std::string format_state(const spot::state* s) const override;
+ bdd state_condition(const spot::state* s) const override;
+
+ /// \brief Get the graph associated to the automaton.
+ /* const LDDGraph& get_graph() const {
+ return *m_sog;
+ }*/
+ ModelCheckerTh *m_builder;
+
+ protected:
+
+ private:
+ std::map<int, int> place_prop;
+ //LDDGraph* m_sog;
+};
+
+#endif // SOGKRIPKE_H_INCLUDED
diff --git a/src/main.cpp b/src/main.cpp
index 977117ee2f0412824972de1236bfff6cff44ca56..cab03898a3bf6020b3ecfd92b659bb76d0be2548 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,9 +127,9 @@ 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<<"Multi-threaded on the fly Model checking (Lace)..."<<endl;
cout<<"Building automata for not(formula)\n";
auto d = spot::make_bdd_dict();
// d->register_ap("jbhkj");
@@ -168,6 +170,50 @@ int main(int argc, char** argv)
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();
+ // 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;