diff --git a/README.md b/README.md
index 79810f39ebba8d2de4bfc1d921548fa5077aa2ec..c775693237a97dd7b42cb41756ba1107dfa3b894 100644
--- a/README.md
+++ b/README.md
@@ -41,7 +41,9 @@ This repository hosts the experiments and results for the Hybrid (MPI/pthreads)
SOG building from an LTL formula (philo3.net example)
```
-mpirun -n 2 hybrid-sog arg1 arg 2 arg3 arg4
+Multi-threading execution
+
+mpirun -n 1 hybrid-sog arg1 arg 2 arg3 arg4
arg1: specifies method of creating threads or/and specifies if modelchecking should be performed on the fly. It can be set with one of the following values:
* p : using pthread library
* pc : using pthread library and applying canonization on nodes
@@ -53,5 +55,14 @@ arg2: specifies the number of threads/workers to be created
arg3: specifies the net to build its SOG
arg4: specifies the LTL formula file
+Distributed execution
+mpirun -n arg0 hybrid-sog arg1 arg 2 arg3 arg4
+arg0 : specifies the number of processes must be >1
+arg1: specifies whether modelchecking should be performed on the fly. It can be set with one of the following values:
+ * otf : Construction performing Model checking on the fly
+ * otherwise : construction without Model checking
+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/HybridKripke.cpp b/src/HybridKripke.cpp
index 50cd35e772004513c236f071558d826f069ac4a1..55bb4ed8cb7501460b61a95718b816ffa043a932 100644
--- a/src/HybridKripke.cpp
+++ b/src/HybridKripke.cpp
@@ -41,9 +41,7 @@ HybridKripke::HybridKripke(const spot::bdd_dict_ptr& dict_ptr,set<string> &l_tra
}
-state* HybridKripke::get_init_state() const {
-
-
+state* HybridKripke::get_init_state() const {
int v;
MPI_Send( &v, 1, MPI_INT, 0, TAG_INITIAL, MPI_COMM_WORLD);
char message[23];
@@ -51,12 +49,11 @@ state* HybridKripke::get_init_state() const {
MPI_Probe(MPI_ANY_SOURCE, TAG_ACK_INITIAL, MPI_COMM_WORLD, &status);
MPI_Get_count(&status, MPI_BYTE, &v);
MPI_Recv(message, 22, MPI_BYTE,MPI_ANY_SOURCE,TAG_ACK_INITIAL,MPI_COMM_WORLD, &status);
- char id[16];
- memcpy(id,message,16);
-
- uint16_t p_container;
- memcpy(&p_container,message+16,2);
- return new HybridKripkeState(id,p_container);
+ succ_t* elt=new succ_t;
+ memcpy(elt->id,message,16);
+ memcpy(&elt->pcontainer,message+16,2);
+ elt->_virtual=false;
+ return new HybridKripkeState(*elt);
}
// Allows to print state label representing its id
@@ -74,13 +71,13 @@ HybridKripkeIterator* HybridKripke::succ_iter(const spot::state* s) const {
auto ss = static_cast<const HybridKripkeState*>(s);
bdd cond = state_condition(ss);
HybridKripkeState* st=ss;
- if (iter_cache_)
+ /* if (iter_cache_)
{
auto it = static_cast<HybridKripkeIterator*>(iter_cache_);
iter_cache_ = nullptr; // empty the cache
it->recycle(*st,cond);
return it;
- }
+ }*/
return new HybridKripkeIterator(*st,cond);
diff --git a/src/HybridKripkeIterator.cpp b/src/HybridKripkeIterator.cpp
index 5297b26a16e881864625a309c8fc4f29d98267d1..f82ceae43593cd5e890aab2151497a92be545e6c 100644
--- a/src/HybridKripkeIterator.cpp
+++ b/src/HybridKripkeIterator.cpp
@@ -32,25 +32,19 @@ bool HybridKripkeIterator::done() const {
}
HybridKripkeState* HybridKripkeIterator::dst() const
- {
-
- succ_t succ_elt= m_current_state->getListSucc()->at(m_current_edge);
- return new HybridKripkeState(succ_elt.id,succ_elt.pcontainer);
-
- }
+{
+ succ_t succ_elt= m_current_state->getListSucc()->at(m_current_edge);
+ return new HybridKripkeState(succ_elt);
+}
bdd HybridKripkeIterator::cond() const {
//cout<<"entering "<<__func__<<endl;
- succ_t succ_elt=m_current_state->getListSucc()->at(m_current_edge);
-
- if (succ_elt.transition==-1) return bddtrue;
-
+ succ_t succ_elt=m_current_state->getListSucc()->at(m_current_edge);
+ if (succ_elt.transition==-1) return bddtrue;
string name=m_net->getTransitionName(succ_elt.transition);
-
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);
-
return result & spot::kripke_succ_iterator::cond();
}
@@ -64,18 +58,11 @@ HybridKripkeIterator::~HybridKripkeIterator()
}
void HybridKripkeIterator::recycle(HybridKripkeState &st, bdd cond)
-{
- //cout<<__func__<<endl;
- m_current_state=&st;
-
+{
+ m_current_state=&st;
spot::kripke_succ_iterator::recycle(cond);
}
-/*HybridKripkeState* HybridKripkeIterator::current_state() const {
- cout<<__func__<<endl;
- return m_current_state;
-}*/
static NewNet * HybridKripkeIterator::m_net;
static spot::bdd_dict_ptr* HybridKripkeIterator::m_dict_ptr;
-static LDDState HybridKripkeIterator::m_deadlock;
-static LDDState HybridKripkeIterator::m_div;
+
diff --git a/src/HybridKripkeState.h b/src/HybridKripkeState.h
index 935d75d654e741669b1f1ae3f428949163456fe4..b25258801650c03d11e478d26328626261e19d7e 100644
--- a/src/HybridKripkeState.h
+++ b/src/HybridKripkeState.h
@@ -10,23 +10,42 @@
#define TAG_ACK_SUCC 11
#define TAG_NOTCOMPLETED 20
typedef struct {
- char id[17];
+ char id[16];
int16_t transition;
uint16_t pcontainer;
+ bool _virtual;
} succ_t;
class HybridKripkeState : public spot::state
{
public:
//static ModelCheckBaseMT * m_builder;
- HybridKripkeState(unsigned char * id,uint16_t pcontainer):m_container(pcontainer) {
- memcpy(m_id,id,16);
- MPI_Send(m_id,16,MPI_BYTE,pcontainer, TAG_ASK_STATE, MPI_COMM_WORLD);
+ HybridKripkeState(succ_t &e):m_container(e.pcontainer) {
+
+ if (e._virtual) { //div or deadlock
+ if (e.id[0]=='v') { // div
+ cout<<"div created..."<<endl;
+ m_hashid=0xFFFFFFFFFFFFFFFE;
+ m_id[0]='v';
+ succ_t elt;
+ elt.id[0]='v';
+ elt.transition=-1;
+ elt._virtual=true;
+ m_succ.push_back(elt);
+ }
+ else {
+ m_id[0]='d';
+ m_hashid=0xFFFFFFFFFFFFFFFF; // deadlock
+ }
+ }
+ else {
+ memcpy(m_id,e.id,16);
+ MPI_Send(m_id,16,MPI_BYTE,e.pcontainer, TAG_ASK_STATE, MPI_COMM_WORLD);
MPI_Status status; //int nbytes;
MPI_Probe(MPI_ANY_SOURCE, TAG_ACK_STATE, MPI_COMM_WORLD, &status);
uint32_t nbytes;
MPI_Get_count(&status, MPI_BYTE, &nbytes);
- // cout<<"ACK state received..."<<nbytes<<endl;
+ // Receive hash id =idprocess | position
char message[nbytes];
MPI_Recv(message, nbytes, MPI_BYTE,MPI_ANY_SOURCE,TAG_ACK_STATE,MPI_COMM_WORLD, &status);
memcpy(&m_hashid,message,8);
@@ -55,7 +74,12 @@ public:
memcpy(&val,message+indice,2);
m_unmarked_places.emplace_front(val);
indice+=2;
- }
+ }
+ // Get div & deadlock
+ uint8_t divblock;
+ memcpy(&divblock,message+indice,1);
+ m_div=divblock & 1;
+ m_deadlock=(divblock>>1) & 1;
// Get successors
MPI_Send(m_id,16,MPI_BYTE,m_container, TAG_ASK_SUCC, MPI_COMM_WORLD);
@@ -81,9 +105,28 @@ public:
indice+=2;
memcpy(&(succ_elt->transition),inmsg+indice,2);
indice+=2;
+ succ_elt->_virtual=false;
m_succ.push_back(*succ_elt);
delete succ_elt;
}
+
+ if (m_div) {
+ succ_t el;
+ el.id[0]='v';
+ el.transition=-1;
+ el._virtual=true;
+ cout<<"yep..."<<endl;
+ m_succ.push_back(el);
+ }
+ if (m_deadlock) {
+ succ_t el;
+ el.id[0]='d';
+ el.pcontainer=0;
+ el._virtual=true;
+ el.transition=-1;
+ m_succ.push_back(el);
+ }
+ }
}
@@ -91,14 +134,14 @@ public:
HybridKripkeState(unsigned char *id,uint16_t pcontainer,size_t hsh,bool ddiv, bool deadlock):m_container(pcontainer),m_div(ddiv),m_deadlock(deadlock),m_hashid(hsh) {
memcpy(m_id,id,16);
- // cout<<__func__<<endl;
+ cout<<__func__<<endl;
}
virtual ~HybridKripkeState();
HybridKripkeState* clone() const override
{
- //cout<<__func__<<endl;
+ cout<<__func__<<endl;
return new HybridKripkeState(m_id,m_container,m_hashid,m_div,m_deadlock);
}
size_t hash() const override
diff --git a/src/MCHybridSOG.cpp b/src/MCHybridSOG.cpp
index a0569d68770c45369427441ff6f8883f5e9c5e0e..1ed2bc9514f27cedf05c27c498cfda25fb125db2 100644
--- a/src/MCHybridSOG.cpp
+++ b/src/MCHybridSOG.cpp
@@ -331,11 +331,12 @@ void *MCHybridSOG::doCompute()
LDDState* pos=m_graph->find(reached_class);
if(!pos)
{
+ reached_class->setDiv(Set_Div(ldd_reachedclass));
+ reached_class->setDeadLock(Set_Bloc(ldd_reachedclass));
m_graph->insert(reached_class);
memcpy(reached_class->m_SHA2,Identif,16);
pthread_mutex_unlock(&m_graph_mutex);
m_graph->addArc();
-
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));
@@ -445,8 +446,11 @@ void *MCHybridSOG::doCompute()
pthread_mutex_lock(&m_graph_mutex);
if (!m_graph->find(Agregate))
{
- m_graph->insert(Agregate);
+ ldd_refs_push(MState);
+ Agregate->setDiv(Set_Div(MState));
+ Agregate->setDeadLock(Set_Bloc(MState));
Agregate->setProcess(task_id);
+ m_graph->insert(Agregate);
string* chaine=new string();
convert_wholemdd_stringcpp(MState,*chaine);
get_md5(*chaine,Identif);
@@ -457,8 +461,7 @@ void *MCHybridSOG::doCompute()
min_charge=minCharge();
pthread_mutex_lock(&m_spin_stack[min_charge]);
m_st[min_charge].push(Pair(couple(Agregate,MState),fire));
- pthread_mutex_unlock(&m_spin_stack[min_charge]);
- ldd_refs_push(MState);
+ pthread_mutex_unlock(&m_spin_stack[min_charge]);
m_charge[min_charge]++;
}
@@ -551,7 +554,7 @@ void MCHybridSOG::read_message()
read_state_message();
break;
case TAG_FINISH:
- cout<<"TAG FINISH received by task "<<task_id<<endl;
+ //cout<<"TAG FINISH received by task "<<task_id<<endl;
MPI_Recv(&v, 1, MPI_INT, m_status.MPI_SOURCE, m_status.MPI_TAG, MPI_COMM_WORLD, &m_status);
m_Terminated=true;
break;
@@ -889,14 +892,13 @@ void MCHybridSOG::sendPropToMC(size_t pos) {
set<uint16_t> unmarked_places=getUnmarkedPlaces(agg);
uint16_t s_mp=marked_places.size();
uint16_t s_up=unmarked_places.size();
- char mess_to_send[8+s_mp*2+s_up*2+4];
+ char mess_to_send[8+s_mp*2+s_up*2+5];
memcpy(mess_to_send,&pos,8);
//cout<<"************* Pos to send :"<<pos<<endl;
size_t indice=8;
memcpy(mess_to_send+indice,&s_mp,2);
indice+=2;
- for (auto it=marked_places.begin();it!=marked_places.end();it++) {
-
+ for (auto it=marked_places.begin();it!=marked_places.end();it++) {
memcpy(mess_to_send+indice,&(*it),2);
indice+=2;
}
@@ -906,5 +908,9 @@ void MCHybridSOG::sendPropToMC(size_t pos) {
memcpy(mess_to_send+indice,&(*it),2);
indice+=2;
}
+ uint8_t divblock=agg->isDiv();
+ divblock=divblock | (agg->isDeadLock()<<1);
+ memcpy(mess_to_send+indice,&divblock,1);
+ indice++;
MPI_Send(mess_to_send,indice,MPI_BYTE,n_tasks, TAG_ACK_STATE, MPI_COMM_WORLD);
}
diff --git a/src/main.cpp b/src/main.cpp
index 5d36106fafdeb6019ba12081c0493c4dd65694a1..a1536e66e8fbf0624e42a52cd06c6fb1dd37063a 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -326,7 +326,7 @@ int main(int argc, char** argv)
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);
- /* spot::twa_graph_ptr k =spot::make_twa_graph(std::make_shared<HybridKripke>(d,Rnewnet.getListTransitionAP(),Rnewnet.getListPlaceAP(),Rnewnet),spot::twa::prop_set::all(), true);
+ spot::twa_graph_ptr k =spot::make_twa_graph(std::make_shared<HybridKripke>(d,Rnewnet.getListTransitionAP(),Rnewnet.getListPlaceAP(),Rnewnet),spot::twa::prop_set::all(), true);
cout<<"finished...."<<endl;
@@ -335,8 +335,8 @@ int main(int argc, char** argv)
st+=".dot";
file.open(st.c_str(),fstream::out);
spot::print_dot(file, k,"ka");
- file.close();*/
- auto k =
+ file.close();
+ /* auto k =
std::make_shared<HybridKripke>(d,Rnewnet.getListTransitionAP(),Rnewnet.getListPlaceAP(),Rnewnet);
if (auto run = k->intersecting_run(af))
{
@@ -344,7 +344,7 @@ int main(int argc, char** argv)
cout<<"=================================="<<endl;
}
else
- std::cout << "formula is verified\n";
+ std::cout << "formula is verified\n";*/
}
}