diff --git a/src/.MCHybridSOG.h.kate-swp b/src/.MCHybridSOG.h.kate-swp
new file mode 100644
index 0000000000000000000000000000000000000000..a65057426854c2e2438dac15c8c74a0492744abb
Binary files /dev/null and b/src/.MCHybridSOG.h.kate-swp differ
diff --git a/src/CommonSOG.h b/src/CommonSOG.h
index 44e11d3f90148033e7795f482ec323b37c4ed5ee..0de9bedf203c138c245038a9f5dd59193e86a5bf 100644
--- a/src/CommonSOG.h
+++ b/src/CommonSOG.h
@@ -1,54 +1,54 @@
-#ifndef COMMONSOG_H
-#define COMMONSOG_H
-#include "LDDState.h"
-#include "LDDGraph.h"
-
-#include "TransSylvan.h"
-#include "NewNet.h"
-#include <stack>
-class LDDState;
-typedef pair<LDDState *, MDD> couple;
-typedef pair<couple, Set> Pair;
-typedef stack<Pair> pile;
-
-class LDDGraph;
-
-class CommonSOG
-{
- public:
- CommonSOG();
- virtual ~CommonSOG();
- LDDGraph *getGraph() const;
- static void printhandler(ostream &o, int var);
- vector<TransSylvan>* getTBRelation();
- Set * getNonObservable();
- unsigned int getPlacesCount();
- Set & getPlaceProposition() {return m_place_proposition;}
- string getTransition(int pos);
- string getPlace(int pos);
- protected:
- NewNet m_net;
- int m_nbPlaces = 0;
- LDDGraph *m_graph;
- vector<TransSylvan> m_tb_relation;
- MDD m_initialMarking;
- map<string, int> m_transitionName;
- map<int,string> m_placeName;
+#ifndef COMMONSOG_H
+#define COMMONSOG_H
+#include "LDDState.h"
+#include "LDDGraph.h"
+
+#include "TransSylvan.h"
+#include "NewNet.h"
+#include <stack>
+class LDDState;
+typedef pair<LDDState *, MDD> couple;
+typedef pair<couple, Set> Pair;
+typedef stack<Pair> pile;
+
+class LDDGraph;
+
+class CommonSOG
+{
+ public:
+ CommonSOG();
+ virtual ~CommonSOG();
+ LDDGraph *getGraph() const;
+ static void printhandler(ostream &o, int var);
+ vector<TransSylvan>* getTBRelation();
+ Set * getNonObservable();
+ unsigned int getPlacesCount();
+ set<uint16_t> & getPlaceProposition() {return m_place_proposition;}
+ string getTransition(int pos);
+ string getPlace(int pos);
+ protected:
+ NewNet m_net;
+ int m_nbPlaces = 0;
+ LDDGraph *m_graph;
+ vector<TransSylvan> m_tb_relation;
+ MDD m_initialMarking;
+ map<string, uint16_t> m_transitionName;
+ map<uint16_t,string> m_placeName;
Set m_observable;
- Set m_nonObservable;
- Set InterfaceTrans;
- Set m_place_proposition;
-
- vector<class Transition> transitions;
-
- MDD Accessible_epsilon(MDD From);
- Set firable_obs(MDD State);
- MDD get_successor(MDD From, int t);
- MDD ImageForward(MDD From);
- MDD Canonize(MDD s, unsigned int level);
- bool Set_Div(MDD &M) const;
- bool Set_Bloc(MDD &M) const;
- private:
-};
-
-#endif // COMMONSOG_H
+ Set m_nonObservable;
+ Set InterfaceTrans;
+ set<uint16_t> m_place_proposition;
+
+ vector<class Transition> transitions;
+
+ MDD Accessible_epsilon(MDD From);
+ Set firable_obs(MDD State);
+ MDD get_successor(MDD From, int t);
+ MDD ImageForward(MDD From);
+ MDD Canonize(MDD s, unsigned int level);
+ bool Set_Div(MDD &M) const;
+ bool Set_Bloc(MDD &M) const;
+ private:
+};
+
+#endif // COMMONSOG_H
diff --git a/src/HybridKripke.cpp b/src/HybridKripke.cpp
index ee4946682b092bac07f00e920d42b994dccfa087..d9e4bc98bcd5aad23afbcbb3272525e45186d07a 100644
--- a/src/HybridKripke.cpp
+++ b/src/HybridKripke.cpp
@@ -16,7 +16,7 @@ using namespace spot;
HybridKripke::HybridKripke(const bdd_dict_ptr &dict_ptr): spot::kripke(dict_ptr)
{
- cout<<__func__<<endl;
+ //cout<<__func__<<endl;
HybridKripkeIterator::m_dict_ptr=&dict_ptr;
/*HybridKripkeIterator::m_deadlock.setLDDValue(1);
HybridKripkeIterator::m_deadlock.setVisited();
@@ -62,57 +62,49 @@ state* HybridKripke::get_init_state() const {
// Allows to print state label representing its id
std::string HybridKripke::format_state(const spot::state* s) const
{
- cout<<__func__<<endl;
+ //cout<<__func__<<endl;
auto ss = static_cast<const HybridKripkeState*>(s);
std::ostringstream out;
- out << "( " << ss->hash() << ")";
-
+ out << "( " << ss->hash() << ")";
return out.str();
}
HybridKripkeIterator* HybridKripke::succ_iter(const spot::state* s) const {
- cout<<__func__<<endl;
+ //cout<<__func__<<endl;
auto ss = static_cast<const HybridKripkeState*>(s);
- HybridKripkeState *aggregate=ss;
+ char id[16];
+ memcpy(id,ss->getId(),16);
bdd cond = state_condition(ss);
- if (iter_cache_)
+ uint16_t pcontainer=ss->getContainerProcess();
+ /* if (iter_cache_)
{
auto it = static_cast<HybridKripkeIterator*>(iter_cache_);
iter_cache_ = nullptr; // empty the cache
- it->recycle(ss, cond);
+ it->recycle(id,pcontainer,cond);
return it;
- }
- return new HybridKripkeIterator(*aggregate,cond);
-
-
-
-
-/* auto ss = static_cast<const SogKripkeStateTh*>(s);
- //////////////////////////////////////////////
+ }*/
+
+ return new HybridKripkeIterator(id,pcontainer,cond);
- return new SogKripkeIteratorTh(ss->getLDDState(),state_condition(ss));//,b);//s state_condition(ss));*/
}
bdd HybridKripke::state_condition(const spot::state* s) const
{
auto ss = static_cast<const HybridKripkeState*>(s);
- set<uint16_t> marked_place=ss->getMarkedPlaces();
-
-
- bdd result=bddtrue;
-
- for (auto it=marked_place.begin();it!=marked_place.end();it++) {
+ set<uint16_t>* marked_place=ss->getMarkedPlaces();
+ bdd result=bddtrue;
+ for (auto it=marked_place->begin();it!=marked_place->end();it++) {
string name=m_net->getPlaceName(*it);
spot::formula f=spot::formula::ap(name);
result&=bdd_ithvar((dict_->var_map.find(f))->second);
}
- set<uint16_t> unmarked_place=ss->getUnmarkedPlaces();
- //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);*/
- //}
+ set<uint16_t>* unmarked_place=ss->getUnmarkedPlaces();
+ for (auto it=unmarked_place->begin();it!=unmarked_place->end();it++) {
+ string name=m_net->getPlaceName(*it);
+ spot::formula f=spot::formula::ap(name);
+ result&=!bdd_ithvar((dict_->var_map.find(f))->second);
+ }
return result;
}
diff --git a/src/HybridKripkeIterator.cpp b/src/HybridKripkeIterator.cpp
index 0c7f4bf226a7e33b9c5e22dc1b579565c695348d..93424f9fdaa0d1096af5f77ca72b04f05bd5cf37 100644
--- a/src/HybridKripkeIterator.cpp
+++ b/src/HybridKripkeIterator.cpp
@@ -6,50 +6,43 @@
#define TAG_ACK_SUCC 11
#define TAG_NOTCOMPLETED 20
-HybridKripkeIterator::HybridKripkeIterator(HybridKripkeState &kstate, bdd cnd):m_current_state(&kstate), kripke_succ_iterator(cnd)
+HybridKripkeIterator::HybridKripkeIterator(char *id,uint16_t pcontainer, bdd cnd): m_pcontainer(pcontainer),kripke_succ_iterator(cnd)
{
- cout<<__func__<<endl;
+
+ memcpy(m_id,id,16);
// Ask list of successors
- MPI_Send(m_current_state->getId(),16,MPI_BYTE,m_current_state->getContainerProcess(), TAG_ASK_SUCC, MPI_COMM_WORLD);
- cout<<"Container process to ask :"<<m_current_state->getContainerProcess()<<endl;
- // Receive list of successors
-
+ MPI_Send(m_id,16,MPI_BYTE,m_pcontainer, TAG_ASK_SUCC, MPI_COMM_WORLD);
+
+ // Receive list of successors
MPI_Status status;
MPI_Probe(MPI_ANY_SOURCE,MPI_ANY_TAG,MPI_COMM_WORLD,&status);
uint32_t nbytes;
MPI_Get_count(&status, MPI_BYTE, &nbytes);
char inmsg[nbytes+1];
- cout<<"Received bytes : "<<nbytes<<endl;
+ //cout<<"Received bytes : "<<nbytes<<endl;
MPI_Recv(inmsg, nbytes, MPI_BYTE,status.MPI_SOURCE,TAG_ACK_SUCC,MPI_COMM_WORLD, &status);
uint32_t nb_succ;
memcpy(&nb_succ,inmsg,4);
- cout<<"Number of successors : "<<nb_succ<<endl;
+ //cout<<"Number of successors "<<nb_succ<<endl;
uint32_t indice=4;
+ succ_t *succ_elt;
+ //printf("List of successors of %.16s\n",m_id);
for (uint32_t i=0;i<nb_succ;i++) {
- succ_t succ_elt;
-
- memcpy(succ_elt.id,inmsg+indice,16);
+ succ_elt=new succ_t;
+ memcpy(succ_elt->id,inmsg+indice,16);
indice+=16;
- memcpy(&(succ_elt.pcontainer),inmsg+indice,2);
- indice+=2;
- memcpy(&(succ_elt.transition),inmsg+indice,2);
+ memcpy(&(succ_elt->pcontainer),inmsg+indice,2);
indice+=2;
-
- m_succ.push_back(succ_elt);
- }
-
- /*if (lddstate->isDeadLock()) {
- m_lsucc.push_back(pair<LDDState*,int>(&m_deadlock,-1));
- }
- if (lddstate->isDiv()) {
- m_lsucc.push_back(pair<LDDState*,int>(&m_div,-1));
- }*/
-
+ memcpy(&(succ_elt->transition),inmsg+indice,2);
+ indice+=2;
+ m_succ.push_back(*succ_elt);
+ delete succ_elt;
+ }
}
bool HybridKripkeIterator::first() {
- cout<<"entering "<<__func__<<endl;
+ //cout<<"entering "<<__func__<<endl;
m_current_edge=0;
return m_succ.size()!=0;
@@ -64,19 +57,20 @@ bool HybridKripkeIterator::next() {
}
bool HybridKripkeIterator::done() const {
- cout<<"entring /excit"<<__func__<<endl;
+ //cout<<"entring /excit"<<__func__<<endl;
return m_current_edge==m_succ.size();
}
HybridKripkeState* HybridKripkeIterator::dst() const
{
- succ_t succ_elt= m_succ.at(m_current_edge);
+
+ succ_t succ_elt= m_succ.at(m_current_edge);
return new HybridKripkeState(succ_elt.id,succ_elt.pcontainer);
}
bdd HybridKripkeIterator::cond() const {
- cout<<"entering "<<__func__<<endl;
+ //cout<<"entering "<<__func__<<endl;
succ_t succ_elt=m_succ.at(m_current_edge);
if (succ_elt.transition==-1) return bddtrue;
@@ -99,10 +93,12 @@ HybridKripkeIterator::~HybridKripkeIterator()
}
-void HybridKripkeIterator::recycle(HybridKripkeState* aggregate, bdd cond)
+void HybridKripkeIterator::recycle(char *id,uint16_t pcontainer, bdd cond)
{
- cout<<__func__<<endl;
- m_current_state=aggregate;
+ //cout<<__func__<<endl;
+ memcpy(m_id,id,16);
+ m_pcontainer=pcontainer;
+
spot::kripke_succ_iterator::recycle(cond);
}
diff --git a/src/HybridKripkeIterator.h b/src/HybridKripkeIterator.h
index 720b4ea122f43b27d5c60ca7797c24a6d7eafd9e..a62012e2572ba6767ea6aed646e3b18770dfebdf 100644
--- a/src/HybridKripkeIterator.h
+++ b/src/HybridKripkeIterator.h
@@ -16,8 +16,9 @@ public:
static LDDState m_div;
static NewNet * m_net;
static spot::bdd_dict_ptr* m_dict_ptr;
- // sog_succ_iterator(const RdPBDD& pn, const SogKripkeState& s, const bdd& c);
- HybridKripkeIterator(HybridKripkeState &kstate, bdd cnd);
+
+
+ HybridKripkeIterator(char *id,uint16_t pcontainer, bdd cnd);
virtual ~HybridKripkeIterator();
bool first() override;
bool next() override;
@@ -27,16 +28,14 @@ public:
// HybridKripkeState* current_state() const;
- void recycle(HybridKripkeState *aggregate, bdd cond);
-
-
+ void recycle(char *id,uint16_t pcontainer, bdd cond);
std::string format_transition() const;
private:
- HybridKripkeState *m_current_state;
-
+ char m_id[16];
+ uint16_t m_pcontainer;
unsigned int m_current_edge=0;
vector<succ_t> m_succ;
};
diff --git a/src/HybridKripkeState.cpp b/src/HybridKripkeState.cpp
index 9c2e02ffd800cb2dd52e1b4b5e5be30d20e97393..80744b5d4574debd040f2ace427435e1ed0acaef 100644
--- a/src/HybridKripkeState.cpp
+++ b/src/HybridKripkeState.cpp
@@ -6,7 +6,7 @@
HybridKripkeState::~HybridKripkeState()
{
//dtor
- cout<<__func__<<endl;
+ //cout<<__func__<<endl;
}
//static ModelCheckBaseMT * HybridKripkeState::m_builder;
diff --git a/src/HybridKripkeState.h b/src/HybridKripkeState.h
index 0ed7af28cfcb9f65aa7d5cddd9b66e0bb4bb6a48..902d5dd9dd3c1b6b349f98f33d3ad0e025f4483c 100644
--- a/src/HybridKripkeState.h
+++ b/src/HybridKripkeState.h
@@ -10,46 +10,69 @@ class HybridKripkeState : public spot::state
{
public:
//static ModelCheckBaseMT * m_builder;
- HybridKripkeState(unsigned char * id,uint16_t pcontainer):m_container(pcontainer) {
- cout<<__func__<<"pcontainer :"<<pcontainer<<endl;
- memcpy(m_id,id,16);
+ 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);
- MPI_Send(m_id,16,MPI_BYTE,pcontainer, TAG_ASK_STATE, MPI_COMM_WORLD);
-
-
- char message[9];
MPI_Status status; //int nbytes;
MPI_Probe(MPI_ANY_SOURCE, TAG_ACK_STATE, MPI_COMM_WORLD, &status);
- cout<<"ACK state received..."<<endl;
- MPI_Recv(message, 8, MPI_BYTE,MPI_ANY_SOURCE,TAG_ACK_STATE,MPI_COMM_WORLD, &status);
- memcpy(&m_hashid,message,8);
+ uint32_t nbytes;
+ MPI_Get_count(&status, MPI_BYTE, &nbytes);
+ // cout<<"ACK state received..."<<nbytes<<endl;
+ char message[nbytes];
+ MPI_Recv(message, nbytes, MPI_BYTE,MPI_ANY_SOURCE,TAG_ACK_STATE,MPI_COMM_WORLD, &status);
+ memcpy(&m_hashid,message,8);
+ //cout<<"Pos :"<<m_hashid<<endl;
+ //cout<<"Process :"<<m_container<<endl;
m_hashid=m_hashid | (size_t(m_container)<<56);
+ // Determine Place propositions
+ uint16_t n_mp;
+ memcpy(&n_mp,message+8,2);
+
+ //cout<<" Marked places :"<<n_mp<<endl;
+ uint16_t indice=10;
+ for(int i=0;i<n_mp;i++) {
+ uint16_t val;
+ memcpy(&val,message+indice,2);
+ m_marked_places.insert(val);
+ indice+=2;
+ }
+ uint16_t n_up;
+ memcpy(&n_up,message+indice,2);
+ //cout<<" Unmarked places :"<<n_mp<<endl;
+ indice+=2;
+ for(int i=0;i<n_up;i++) {
+ uint16_t val;
+ memcpy(&val,message+indice,2);
+ m_unmarked_places.insert(val);
+ indice+=2;
+ }
+
}
// Constructor for cloning
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
- {
- cout<<__func__<<m_hashid<<endl;
+ {
return m_hashid;
}
int compare(const spot::state* other) const override
{
- cout<<__func__<<endl;
+
auto o = static_cast<const HybridKripkeState*>(other);
size_t oh = o->hash();
size_t h = hash();
@@ -60,15 +83,14 @@ public:
return h > oh;
}
unsigned char * getId() {
- cout<<__func__<<endl;
+ // cout<<__func__<<endl;
return m_id;
}
- uint16_t getContainerProcess() {
- cout<<__func__<<endl;
+ uint16_t getContainerProcess() {
return m_container;
}
- set<uint16_t> & getMarkedPlaces() { return m_marked_places;}
- set<uint16_t> & getUnmarkedPlaces() { return m_unmarked_places;}
+ set<uint16_t> * getMarkedPlaces() { return &m_marked_places;}
+ set<uint16_t> * getUnmarkedPlaces() { return &m_unmarked_places;}
protected:
private:
diff --git a/src/LDDGraph.cpp b/src/LDDGraph.cpp
index cf0829b14303e1e64cb49b48d07770c59a2bccac..b8e89d2bae4a0594f5f90743344ab3011a2b328f 100644
--- a/src/LDDGraph.cpp
+++ b/src/LDDGraph.cpp
@@ -197,9 +197,9 @@ LDDState *LDDGraph::getLDDStateById(unsigned int id) {
return m_GONodes.at(id);
}
-string LDDGraph::getTransition(int pos) {
+string LDDGraph::getTransition(uint16_t pos) {
- map<string,int>::iterator it=m_transition->begin();
+ map<string,uint16_t>::iterator it=m_transition->begin();
while(it != m_transition->end())
{
if(it->second == pos)
@@ -209,14 +209,14 @@ string LDDGraph::getTransition(int pos) {
return it->first;
}
-string LDDGraph::getPlace(int pos) {
+string LDDGraph::getPlace(uint16_t pos) {
return m_places->find(pos)->second;
}
-void LDDGraph::setTransition(map<string,int>& list_transitions) {
+void LDDGraph::setTransition(map<string,uint16_t>& list_transitions) {
m_transition=&list_transitions;
}
-void LDDGraph::setPlace(map<int,string>& list_places) {
+void LDDGraph::setPlace(map<uint16_t,string>& list_places) {
m_places=&list_places;
}
diff --git a/src/LDDGraph.h b/src/LDDGraph.h
index 891eaf6fc23d4f67efe4928a93610167f1c73083..d29547f9265fc5b6233df4521bf2e8516e58e661 100755
--- a/src/LDDGraph.h
+++ b/src/LDDGraph.h
@@ -14,16 +14,16 @@ class CommonSOG;
class LDDGraph
{
private:
- map<string,int>* m_transition;
- map<int,string>* m_places;
+ map<string,uint16_t>* m_transition;
+ map<uint16_t,string>* m_places;
void printGraph(LDDState *, size_t &);
CommonSOG *m_constructor;
public:
CommonSOG* getConstructor() {return m_constructor;}
- string getTransition(int pos);
- string getPlace(int pos);
- void setPlace(map<int,string>& list_places);
- void setTransition(map<string,int>& list_transitions);
+ string getTransition(uint16_t pos);
+ string getPlace(uint16_t pos);
+ void setPlace(map<uint16_t,string>& list_places);
+ void setTransition(map<string,uint16_t>& list_transitions);
MetaLDDNodes m_GONodes;
LDDState *getLDDStateById(unsigned int id);
void Reset();
diff --git a/src/LDDState.cpp b/src/LDDState.cpp
index 04cc36e0a53c73d2a28b1384bea6a9efc1703613..d1b03429cf9737c15590a12e3568492681fea80b 100644
--- a/src/LDDState.cpp
+++ b/src/LDDState.cpp
@@ -33,10 +33,10 @@ vector<pair<LDDState*, int>>* LDDState::getSuccessors() {
return &Successors;
}
-vector<int> LDDState::getMarkedPlaces(set<int>& lplacesAP) {
- vector<int> result;
+vector<uint16_t> LDDState::getMarkedPlaces(set<uint16_t>& lplacesAP) {
+ vector<uint16_t> result;
MDD mdd=m_lddstate;
- int depth=0;
+ uint16_t depth=0;
while (mdd>lddmc_true)
{
//printf("mddd : %d \n",mdd);
@@ -54,11 +54,11 @@ vector<int> LDDState::getMarkedPlaces(set<int>& lplacesAP) {
return result;
}
-vector<int> LDDState::getUnmarkedPlaces(set<int>& lplacesAP) {
- vector<int> result;
+vector<uint16_t> LDDState::getUnmarkedPlaces(set<uint16_t>& lplacesAP) {
+ vector<uint16_t> result;
MDD mdd=m_lddstate;
- int depth=0;
+ uint16_t depth=0;
while (mdd>lddmc_true)
{
//printf("mddd : %d \n",mdd);
diff --git a/src/LDDState.h b/src/LDDState.h
index e59e7195b46c5ffd15e3ca407376e4ef1d3276fc..7864d207562dc245a5b91002a885a7c26e734ece 100755
--- a/src/LDDState.h
+++ b/src/LDDState.h
@@ -13,7 +13,7 @@ class LDDState {
public:
LDDState() {
- m_boucle = m_blocage = m_visited = false;
+ m_boucle = m_blocage = m_visited = false;m_completed=false;
m_virtual = false;
}
virtual ~LDDState();
@@ -41,8 +41,8 @@ class LDDState {
bool isVisited() {return m_visited;}
void setCompletedSucc() {m_completed=true;}
bool isCompletedSucc() {return m_completed;}
- vector<int> getMarkedPlaces(set<int>& lplacesAP);
- vector<int> getUnmarkedPlaces(set<int>& lplacesAP);
+ vector<uint16_t> getMarkedPlaces(set<uint16_t>& lplacesAP);
+ vector<uint16_t> getUnmarkedPlaces(set<uint16_t>& lplacesAP);
void setProcess(uint16_t v) {m_process=v;}
uint16_t getProcess() {return m_process;}
protected:
diff --git a/src/MCHybridSOG.cpp b/src/MCHybridSOG.cpp
index 9ca13560fece90bb9653c9338b5c9f81f7366774..7f9b91f512542aae8d53e06bc623192ebe28c848 100644
--- a/src/MCHybridSOG.cpp
+++ b/src/MCHybridSOG.cpp
@@ -149,7 +149,7 @@ void *MCHybridSOG::doCompute()
convert_wholemdd_stringcpp(Complete_meta_state,*chaine);
get_md5(*chaine,Identif);
//lddmc_getsha(Complete_meta_state, Identif);
- int destination=(int)(Identif[0]%n_tasks);
+ uint16_t destination=(uint16_t)(Identif[0]%n_tasks);
c->setProcess(destination);
if(destination==0)
{
@@ -167,7 +167,7 @@ void *MCHybridSOG::doCompute()
MDD initialstate=Complete_meta_state;
//cout<<"Initial marking is sent"<<endl;
m_graph->insertSHA(c);
- strcpySHA(c->m_SHA2,Identif);
+ memcpy(c->m_SHA2,Identif,16);
// MDD initialstate=Complete_meta_state;
//pthread_spin_lock(&m_spin_md5);
@@ -176,9 +176,9 @@ void *MCHybridSOG::doCompute()
//pthread_spin_unlock(&m_spin_md5);
//#ifndef
// if (strcmp(red,'C')==0)
- {
+
initialstate=Canonize(Complete_meta_state,0);
- }
+
//#endif // REDUCE
convert_wholemdd_stringcpp(initialstate,*chaine);
@@ -210,28 +210,25 @@ void *MCHybridSOG::doCompute()
m_waitingBuild=false;
m_aggWaiting=m_graph->getLDDStateById(pos);
m_waitingSucc=true;
- cout<<"Get build..."<<endl;
+ // cout<<"Get build..."<<endl;
}
}
if (m_waitingSucc) {
if (m_aggWaiting->isCompletedSucc()) {
- cout<<"Get succ..."<<endl;
+ //cout<<"Get succ..."<<endl;
m_waitingSucc=false;
sendSuccToMC();
}
}
if (m_waitingAgregate) {
- bool res;
+ bool res=false;
size_t pos=m_graph->findSHAPos(m_id_md5,res);
//cout<<"Not found..."<<endl;
if (res) {
m_waitingAgregate=false;
- char mess[9];
- memcpy(mess,&pos,8);
- MPI_Send(mess,8,MPI_BYTE,n_tasks, TAG_ACK_STATE, MPI_COMM_WORLD);
-
+ sendPropToMC(pos);
}
}
}
@@ -335,7 +332,7 @@ void *MCHybridSOG::doCompute()
if(!pos)
{
m_graph->insert(reached_class);
-
+ memcpy(reached_class->m_SHA2,Identif,16);
pthread_mutex_unlock(&m_graph_mutex);
m_graph->addArc();
@@ -385,7 +382,7 @@ void *MCHybridSOG::doCompute()
//MDD Reduced=ldd_reachedclass;
string* message_to_send2=new string();
convert_wholemdd_stringcpp(reached,*message_to_send2);
- get_md5(*message_to_send2,Identif);
+ // get_md5(*message_to_send2,Identif);
@@ -507,45 +504,41 @@ void MCHybridSOG::read_message()
{
//cout<<"message tag :"<<m_status.MPI_TAG<<" by task "<<task_id<<endl;
if (m_status.MPI_TAG==TAG_ASK_STATE) {
- cout<<"TAG ASKSTATE received by task "<<task_id<<" from "<<m_status.MPI_SOURCE<<endl;
+ //cout<<"TAG ASKSTATE received by task "<<task_id<<" from "<<m_status.MPI_SOURCE<<endl;
char mess[17];
MPI_Recv(mess,16,MPI_BYTE,m_status.MPI_SOURCE,m_status.MPI_TAG,MPI_COMM_WORLD,&m_status);
bool res;m_waitingAgregate=false;
size_t pos=m_graph->findSHAPos(mess,res);
if (!res) {
- cout<<"Not found"<<endl;
+ //cout<<"Not found"<<endl;
m_waitingAgregate=true;
memcpy(m_id_md5,mess,16);
}
- else {
- cout<<"pos found :"<<pos<<endl;
- memcpy(mess,&pos,8);
- MPI_Send(mess,8,MPI_BYTE,m_status.MPI_SOURCE, TAG_ACK_STATE, MPI_COMM_WORLD);
- }
+ else sendPropToMC(pos);
+
}
- else if (m_status.MPI_TAG==TAG_ASK_SUCC) {
+ else if (m_status.MPI_TAG==TAG_ASK_SUCC) {
- char mess[17];
-
+ char mess[17];
MPI_Recv(mess,16,MPI_BYTE,m_status.MPI_SOURCE,m_status.MPI_TAG,MPI_COMM_WORLD,&m_status);
m_waitingBuild=false;m_waitingSucc=false;
bool res;
- cout<<"Before "<<res<<endl;
+ //cout<<"Before "<<res<<endl;
size_t pos=m_graph->findSHAPos(mess,res);
- cout<<"After "<<res<<endl;
+ //cout<<"After "<<res<<endl;
if (res) {
LDDState *aggregate=m_graph->getLDDStateById(pos);
m_aggWaiting=aggregate;
if (aggregate->isCompletedSucc()) sendSuccToMC();
else {
m_waitingSucc=true;
- cout<<"Waiting for succ..."<<endl;
+ //cout<<"Waiting for succ..."<<endl;
}
}
else {
m_waitingBuild=true;
- cout<<"Waiting for build..."<<endl;
+ //cout<<"Waiting for build..."<<endl;
memcpy(m_id_md5,mess,16);
}
@@ -554,29 +547,22 @@ void MCHybridSOG::read_message()
switch (m_status.MPI_TAG)
{
case TAG_STATE:
- cout<<"=============================TAG STATE received by task "<<task_id<<endl;
+ //cout<<"=============================TAG STATE received by task "<<task_id<<endl;
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;
case TAG_INITIAL:
- cout<<"TAG INITIAL received by task "<<task_id<<endl;
-
+ // cout<<"TAG INITIAL 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);
- LDDState *i_agregate=m_graph->getInitialState();
-
-
- char message[23];
+ LDDState *i_agregate=m_graph->getInitialState();
+ char message[22];
memcpy(message,i_agregate->getSHAValue(),16);
- uint16_t id_p=i_agregate->getProcess();
- uint32_t jouk=65535;
- memcpy(message+16,&id_p,2);
- memcpy(message+18,&jouk,4);
-
+ uint16_t id_p=i_agregate->getProcess();
+ memcpy(message+16,&id_p,2);
MPI_Send(message,22,MPI_BYTE,m_status.MPI_SOURCE, TAG_ACK_INITIAL, MPI_COMM_WORLD);
break;
@@ -584,11 +570,7 @@ void MCHybridSOG::read_message()
default: cout<<"unknown received "<<m_status.MPI_TAG<<" by task "<<task_id<<endl;
//AbortTerm();
- break;
- /* int v;
- MPI_Recv(&v, 1, MPI_INT, status.MPI_SOURCE, status.MPI_TAG, MPI_COMM_WORLD, &status);
- if (task_id!=0)
- MPI_Send( &v, 1, MPI_INT, 0, TAG_ABORT, MPI_COMM_WORLD);*/
+ break;
}
MPI_Iprobe(MPI_ANY_SOURCE,MPI_ANY_TAG,MPI_COMM_WORLD,&flag,&m_status);
@@ -615,9 +597,6 @@ void MCHybridSOG::read_state_message()
pthread_mutex_unlock(&m_spin_msg[min_charge]);
}
-
-
-
void MCHybridSOG::send_state_message()
{
while (!m_msg[0].empty())
@@ -694,8 +673,6 @@ void MCHybridSOG::computeDSOG(LDDGraph &g)
doCompute();
-
-
for (int i = 0; i < m_nb_thread-1; i++)
{
pthread_join(m_list_thread[i], NULL);
@@ -713,16 +690,8 @@ void MCHybridSOG::computeDSOG(LDDGraph &g)
MPI_Reduce(&nbarcs, &sum_nbArcs, 1, MPI_INT, MPI_SUM, 0, m_comm_world);
MPI_Reduce(&m_size_mess, &total_size_mess, 1, MPI_INT, MPI_SUM, 0, m_comm_world);
-
-
-
if(task_id==0)
{
- //
-
- // cout<<"Nb Iteration internes : "<<m_itint<<endl;*/
- //auto t2 = std::chrono::high_resolution_clock::now();
- //tps=(double)clock() / (double)CLOCKS_PER_SEC-t1;
clock_gettime(CLOCK_REALTIME, &finish);
tps = (finish.tv_sec - start.tv_sec);
@@ -757,15 +726,6 @@ int MCHybridSOG::minCharge()
}
-void MCHybridSOG::strcpySHA(unsigned char *dest,const unsigned char *source)
-{
- for (int i=0; i<LENGTH_ID; i++)
- {
- dest[i]=source[i];
- //if (source[i]=='\0') exit(0);
- }
- dest[LENGTH_ID]='\0';
-}
@@ -774,10 +734,6 @@ MCHybridSOG::~MCHybridSOG()
//dtor
}
-
-
-
-
/******************************************convert char ---> MDD ********************************************/
MDD MCHybridSOG::decodage_message(const char *chaine)
@@ -801,27 +757,6 @@ MDD MCHybridSOG::decodage_message(const char *chaine)
return M;
}
-
-/*void HybridSOG::DisplayMessage(const char *chaine)
-{
- unsigned int longueur=((unsigned char)chaine[1]-1);
- longueur=(longueur<<7) | ((unsigned char)chaine[0]>>1);
- int index=2;
- printf("Chaine longueur %d pour %d places",longueur,m_nbPlaces);
- for (int nb=0; nb<longueur; nb++)
- {
- for (int i=0; i<m_nbPlaces; i++)
- {
-
- printf("%d",((unsigned char)chaine[index]-1));
- index++;
- }
- printf(" ");
- }
-
-} */
-
-
void * MCHybridSOG::threadHandler(void *context)
{
@@ -877,7 +812,7 @@ void MCHybridSOG::get_md5(const string& chaine,unsigned char *md_chaine)
pthread_spin_lock(&m_spin_md5);
MD5(chaine.c_str(), chaine.size(),md_chaine);
pthread_spin_unlock(&m_spin_md5);
- md_chaine[16]='\0';
+ //md_chaine[16]='\0';
}
void MCHybridSOG::sendSuccToMC() {
@@ -887,7 +822,7 @@ void MCHybridSOG::sendSuccToMC() {
char mess_tosend[message_size];
memcpy(mess_tosend,&nb_succ,4);
uint32_t i_message=4;
-
+ //cout<<"***************************Number of succesors to send :"<<nb_succ<<endl;
for (uint32_t i=0;i<nb_succ;i++) {
pair<LDDState*,int> elt;
@@ -895,7 +830,7 @@ void MCHybridSOG::sendSuccToMC() {
memcpy(mess_tosend+i_message,elt.first->getSHAValue(),16);
i_message+=16;
uint16_t pcontainer=elt.first->getProcess();
- cout<<" pcontainer "<<pcontainer<<endl;
+ //cout<<" pcontainer "<<pcontainer<<endl;
memcpy(mess_tosend+i_message,&pcontainer,2);
i_message+=2;
memcpy(mess_tosend+i_message,&(elt.second),2);
@@ -905,3 +840,71 @@ void MCHybridSOG::sendSuccToMC() {
MPI_Send(mess_tosend,message_size,MPI_BYTE,n_tasks, TAG_ACK_SUCC,MPI_COMM_WORLD);
}
+
+set<uint16_t> MCHybridSOG::getMarkedPlaces(LDDState *agg) {
+ set<uint16_t> result;
+ MDD mdd=agg->getLDDValue();
+ uint16_t depth=0;
+ while (mdd>lddmc_true)
+ {
+ //printf("mddd : %d \n",mdd);
+ mddnode_t node=GETNODE(mdd);
+ if (m_place_proposition.find(depth)!=m_place_proposition.end())
+ if (mddnode_getvalue(node)==1) {
+ result.insert(depth);
+ }
+
+ mdd=mddnode_getdown(node);
+ depth++;
+
+ }
+ return result;
+}
+
+set<uint16_t> MCHybridSOG::getUnmarkedPlaces(LDDState *agg) {
+ set<uint16_t> result;
+ MDD mdd=agg->getLDDValue();
+
+ uint16_t depth=0;
+ while (mdd>lddmc_true)
+ {
+ //printf("mddd : %d \n",mdd);
+ mddnode_t node=GETNODE(mdd);
+ if (m_place_proposition.find(depth)!=m_place_proposition.end())
+ if (mddnode_getvalue(node)==0) {
+ result.insert(depth);
+
+ }
+
+ mdd=mddnode_getdown(node);
+ depth++;
+
+ }
+ return result;
+}
+// Send propositions to Model checker
+void MCHybridSOG::sendPropToMC(size_t pos) {
+ LDDState *agg=m_graph->getLDDStateById(pos);
+ set<uint16_t> marked_places=getMarkedPlaces(agg);
+ 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];
+ 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++) {
+
+ memcpy(mess_to_send+indice,&(*it),2);
+ indice+=2;
+ }
+ memcpy(mess_to_send+indice,&s_up,2);
+ indice+=2;
+ for (auto it=unmarked_places.begin();it!=unmarked_places.end();it++) {
+ memcpy(mess_to_send+indice,&(*it),2);
+ indice+=2;
+ }
+ MPI_Send(mess_to_send,indice,MPI_BYTE,n_tasks, TAG_ACK_STATE, MPI_COMM_WORLD);
+}
diff --git a/src/MCHybridSOG.h b/src/MCHybridSOG.h
index 9c250deae146d7543a4fc2fd5b2d95c916695ee8..ae70af3e2739e1c8cc3eab2162447802c1a0fb10 100644
--- a/src/MCHybridSOG.h
+++ b/src/MCHybridSOG.h
@@ -30,6 +30,7 @@
#include <time.h>
#include <chrono>
#include "CommonSOG.h"
+#include <atomic>
// namespace mpi = boost::mpi;
//#define MASTER 0
@@ -59,11 +60,13 @@ protected:
private:
MPI_Comm m_comm_world;
void sendSuccToMC();
- bool m_waitingAgregate=false;
- bool m_waitingBuild=false;
+ void sendPropToMC(size_t pos);
+ atomic_bool m_waitingAgregate;// (false);
+ atomic_bool m_waitingBuild;
+ atomic_bool m_waitingSucc;
char m_id_md5[16];
LDDState * m_aggWaiting=nullptr;
- bool m_waitingSucc=false;
+
/// \ hash function
void get_md5(const string &chaine, unsigned char *md_chaine);
@@ -72,7 +75,7 @@ private:
inline int minCharge();
/// Copie string of caracter
- void strcpySHA(unsigned char *dest, const unsigned char *source);
+
MDD M0;
@@ -133,7 +136,8 @@ private:
int m_total_nb_send = 0, m_total_nb_recv = 0;
MPI_Status m_status;
-
+ set<uint16_t> getUnmarkedPlaces(LDDState *agg);
+ set<uint16_t> getMarkedPlaces(LDDState *agg);
};
diff --git a/src/NewNet.cpp b/src/NewNet.cpp
index 66bf51c694fe6485d2400d022cc95af717bd4290..5b2e4b6c51ff7f3cbc3244ffcffdd2f063edf6c3 100644
--- a/src/NewNet.cpp
+++ b/src/NewNet.cpp
@@ -183,7 +183,7 @@ void NewNet::setListObservable(const set<string> & list_t)
{
cout<<"Error: "<<*i<<" is not a transition!"<<endl;
// Check if the proposition corresponds to a place
- map<string, int>::iterator pi = placeName.find(*i);
+ map<string, uint16_t>::iterator pi = placeName.find(*i);
if (pi!=placeName.end())
cout<<"Place was found!"<<endl;
m_formula_place.insert(pi->second);
@@ -207,7 +207,7 @@ void NewNet::setListObservable(const set<string> & list_t)
else
{
Formula_Trans.insert(pos);
- map<string,int>::iterator ti=transitionName.find(*i);
+ map<string,uint16_t>::iterator ti=transitionName.find(*i);
Observable.insert(pos);
}
}
@@ -365,7 +365,7 @@ ostream &operator<<(ostream &os, const Set &s)
/*----------------------------------------------------------------------*/
bool NewNet::addPlace(const string &place, int marking, int capacity)
{
- map<string, int>::const_iterator pi = placeName.find(place);
+ map<string, uint16_t>::const_iterator pi = placeName.find(place);
if (pi == placeName.end())
{
placeName[place] = places.size();
@@ -379,7 +379,7 @@ bool NewNet::addPlace(const string &place, int marking, int capacity)
bool NewNet::addQueue(const string &place, int capacity)
{
- map<string, int>::const_iterator pi = placeName.find(place);
+ map<string, uint16_t>::const_iterator pi = placeName.find(place);
if (pi == placeName.end())
{
placeName[place] = places.size();
@@ -393,7 +393,7 @@ bool NewNet::addQueue(const string &place, int capacity)
bool NewNet::addLossQueue(const string &place, int capacity)
{
- map<string, int>::const_iterator pi = placeName.find(place);
+ map<string, uint16_t>::const_iterator pi = placeName.find(place);
if (pi == placeName.end())
{
placeName[place] = places.size();
@@ -407,7 +407,7 @@ bool NewNet::addLossQueue(const string &place, int capacity)
bool NewNet::addTrans(const string &trans)
{
- map<string, int>::const_iterator ti = transitionName.find(trans);
+ map<string,uint16_t>::const_iterator ti = transitionName.find(trans);
if (ti == transitionName.end())
{
transitionName[trans] = transitions.size();
@@ -422,12 +422,12 @@ bool NewNet::addTrans(const string &trans)
bool NewNet::addPre(const string &place, const string &trans, int valuation)
{
int p, t;
- map<string, int>::const_iterator pi = placeName.find(place);
+ map<string, uint16_t>::const_iterator pi = placeName.find(place);
if (pi == placeName.end() || places[pi->second].isQueue())
return false;
else
p = pi->second;
- map<string, int>::const_iterator ti = transitionName.find(trans);
+ map<string, uint16_t>::const_iterator ti = transitionName.find(trans);
if (ti == transitionName.end())
return false;
else
@@ -440,12 +440,12 @@ bool NewNet::addPre(const string &place, const string &trans, int valuation)
bool NewNet::addPost(const string &place, const string &trans, int valuation)
{
int p, t;
- map<string, int>::const_iterator pi = placeName.find(place);
+ map<string, uint16_t>::const_iterator pi = placeName.find(place);
if (pi == placeName.end() || places[pi->second].isQueue())
return false;
else
p = pi->second;
- map<string, int>::const_iterator ti = transitionName.find(trans);
+ map<string, uint16_t>::const_iterator ti = transitionName.find(trans);
if (ti == transitionName.end())
return false;
else
@@ -458,12 +458,12 @@ bool NewNet::addPost(const string &place, const string &trans, int valuation)
bool NewNet::addPreQueue(const string &place, const string &trans, int valuation)
{
int p, t;
- map<string, int>::const_iterator pi = placeName.find(place);
+ map<string, uint16_t>::const_iterator pi = placeName.find(place);
if (pi == placeName.end() || !places[pi->second].isQueue())
return false;
else
p = pi->second;
- map<string, int>::const_iterator ti = transitionName.find(trans);
+ map<string, uint16_t>::const_iterator ti = transitionName.find(trans);
if (ti == transitionName.end())
return false;
else
@@ -477,12 +477,12 @@ bool NewNet::addPostQueue(const string &place, const string &trans,
int valuation)
{
int p, t;
- map<string, int>::const_iterator pi = placeName.find(place);
+ map<string, uint16_t>::const_iterator pi = placeName.find(place);
if (pi == placeName.end() || !places[pi->second].isQueue())
return false;
else
p = pi->second;
- map<string, int>::const_iterator ti = transitionName.find(trans);
+ map<string, uint16_t>::const_iterator ti = transitionName.find(trans);
if (ti == transitionName.end())
return false;
else
@@ -496,12 +496,12 @@ bool NewNet::addInhibitor(const string &place, const string &trans,
int valuation)
{
int p, t;
- map<string, int>::const_iterator pi = placeName.find(place);
+ map<string, uint16_t>::const_iterator pi = placeName.find(place);
if (pi == placeName.end())
return false;
else
p = pi->second;
- map<string, int>::const_iterator ti = transitionName.find(trans);
+ map<string, uint16_t>::const_iterator ti = transitionName.find(trans);
if (ti == transitionName.end())
return false;
else
@@ -515,17 +515,17 @@ bool NewNet::addPreAuto(const string &place, const string &trans,
const string &valuation)
{
int p, t, v;
- map<string, int>::const_iterator pi = placeName.find(place);
+ map<string, uint16_t>::const_iterator pi = placeName.find(place);
if (pi == placeName.end() || places[pi->second].isQueue())
return false;
else
p = pi->second;
- map<string, int>::const_iterator ti = transitionName.find(trans);
+ map<string, uint16_t>::const_iterator ti = transitionName.find(trans);
if (ti == transitionName.end())
return false;
else
t = ti->second;
- map<string, int>::const_iterator pv = placeName.find(valuation);
+ map<string, uint16_t>::const_iterator pv = placeName.find(valuation);
if (pv == placeName.end() || places[pv->second].isQueue())
return false;
else
@@ -539,17 +539,17 @@ bool NewNet::addPostAuto(const string &place, const string &trans,
const string &valuation)
{
int p, t, v;
- map<string, int>::const_iterator pi = placeName.find(place);
+ map<string, uint16_t>::const_iterator pi = placeName.find(place);
if (pi == placeName.end() || places[pi->second].isQueue())
return false;
else
p = pi->second;
- map<string, int>::const_iterator ti = transitionName.find(trans);
+ map<string, uint16_t>::const_iterator ti = transitionName.find(trans);
if (ti == transitionName.end())
return false;
else
t = ti->second;
- map<string, int>::const_iterator pv = placeName.find(valuation);
+ map<string, uint16_t>::const_iterator pv = placeName.find(valuation);
if (pv == placeName.end() || places[pi->second].isQueue())
return false;
else
@@ -562,12 +562,12 @@ bool NewNet::addPostAuto(const string &place, const string &trans,
bool NewNet::addReset(const string &place, const string &trans)
{
int p, t;
- map<string, int>::const_iterator pi = placeName.find(place);
+ auto pi = placeName.find(place);
if (pi == placeName.end())
return false;
else
p = pi->second;
- map<string, int>::const_iterator ti = transitionName.find(trans);
+ auto ti = transitionName.find(trans);
if (ti == transitionName.end())
return false;
else
diff --git a/src/NewNet.h b/src/NewNet.h
index 9709a016016507dec081c17a3d9ee6ac867e63fc..8341cf38abf3fbd2be968cfc56401652bcb2b265 100644
--- a/src/NewNet.h
+++ b/src/NewNet.h
@@ -69,13 +69,13 @@ class NewNet : public RdPMonteur {
/* Attributs */
vector<class Place> places;
vector<class Transition> transitions;
- map<string, int> placeName;
- map<string, int> transitionName;
+ map<string, uint16_t> placeName;
+ map<string, uint16_t> transitionName;
Set Observable;
Set NonObservable;
Set InterfaceTrans;
Set Formula_Trans;
- Set m_formula_place;
+ set<uint16_t> m_formula_place;
/* Constructors */
NewNet(){};
@@ -108,10 +108,10 @@ class NewNet : public RdPMonteur {
set<string>& getListPlaceAP() {return m_lplaceAP;}
string& getPlaceName(size_t pos) { return m_placePosName.find(pos)->second;}
string& getTransitionName(size_t pos) { return m_transitionPosName.find(pos)->second;}
- map<int,string> m_placePosName;
+ map<uint16_t,string> m_placePosName;
private:
- map<int,string> m_transitionPosName;
+ map<uint16_t,string> m_transitionPosName;
set<string> m_ltransitionAP;
diff --git a/src/SogKripke.cpp b/src/SogKripke.cpp
index d2dffaa205d2f30cef05ca44a214f5a847a44e01..d8229149513944a4e85c1a209d11fc3778be760c 100644
--- a/src/SogKripke.cpp
+++ b/src/SogKripke.cpp
@@ -52,7 +52,7 @@ bdd SogKripke::state_condition(const spot::state* s) const
{
auto ss = static_cast<const SogKripkeState*>(s);
- vector<int> marked_place=ss->getLDDState()->getMarkedPlaces(m_sog->getConstructor()->getPlaceProposition());
+ vector<uint16_t> marked_place=ss->getLDDState()->getMarkedPlaces(m_sog->getConstructor()->getPlaceProposition());
bdd result=bddtrue;
@@ -62,7 +62,7 @@ bdd SogKripke::state_condition(const spot::state* s) const
spot::formula f=spot::formula::ap(name);
result&=bdd_ithvar((dict_->var_map.find(f))->second);
}
- vector<int> unmarked_place=ss->getLDDState()->getUnmarkedPlaces(m_sog->getConstructor()->getPlaceProposition());
+ vector<uint16_t> unmarked_place=ss->getLDDState()->getUnmarkedPlaces(m_sog->getConstructor()->getPlaceProposition());
for (auto it=unmarked_place.begin();it!=unmarked_place.end();it++) {
string name=m_sog->getPlace(*it);
spot::formula f=spot::formula::ap(name);
diff --git a/src/SogKripkeTh.cpp b/src/SogKripkeTh.cpp
index d2884fa39a07bac631c69d972b3f35f5c523d1a7..b11c54288f3ac4e6cf7e9cfc4384431ed79ef1fa 100644
--- a/src/SogKripkeTh.cpp
+++ b/src/SogKripkeTh.cpp
@@ -78,7 +78,7 @@ 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());
+ vector<uint16_t> marked_place=ss->getLDDState()->getMarkedPlaces(m_builder->getPlaceProposition());
bdd result=bddtrue;
@@ -88,7 +88,7 @@ bdd SogKripkeTh::state_condition(const spot::state* s) const
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());
+ vector<uint16_t> 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);
diff --git a/src/main.cpp b/src/main.cpp
index d358602a16673541c7422350e903f85377b52b99..5477c36adbba09f59a7b275fb926a460f253be45 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -4,8 +4,6 @@
#include <iostream>
#include <string>
#include <fstream>
-//#include "bdd.h"
-//#include "fdd.h"
#include <mpi.h>
#include "DistributedSOG.h"
@@ -121,7 +119,7 @@ int main(int argc, char** argv)
cout<<"Fetching formula..."<<endl;
set<string> list_propositions=buildPropositions(formula);
- NewNet R(argv[3],list_propositions);
+ NewNet Rnewnet(argv[3],list_propositions);
MPI_Init (&argc, &argv );
MPI_Comm_size(MPI_COMM_WORLD,&n_tasks);
@@ -152,13 +150,13 @@ int main(int argc, char** argv)
}
cout<<"Loading net information..."<<endl;
ModelCheckBaseMT* mcl;
- if (!strcmp(argv[1],"otfL")) mcl=new ModelCheckLace(R,bound,nb_th);
+ if (!strcmp(argv[1],"otfL")) mcl=new ModelCheckLace(Rnewnet,bound,nb_th);
else
- mcl=new ModelCheckerTh(R,bound,nb_th);
+ mcl=new ModelCheckerTh(Rnewnet,bound,nb_th);
mcl->loadNet();
auto k =
- std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP());
+ std::make_shared<SogKripkeTh>(d,mcl,Rnewnet.getListTransitionAP(),Rnewnet.getListPlaceAP());
/* spot::twa_graph_ptr k =
spot::make_twa_graph(std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()),
spot::twa::prop_set::all(), true);*/
@@ -199,7 +197,7 @@ int main(int argc, char** argv)
{
cout<<"number of task = 1 \n " <<endl;
bool uselace=(!strcmp(argv[1],"lc")) || (!strcmp(argv[1],"l"));
- threadSOG DR(R, bound,nb_th,uselace);
+ threadSOG DR(Rnewnet, bound,nb_th,uselace);
LDDGraph g(&DR);
if (nb_th==1)
@@ -264,7 +262,7 @@ int main(int argc, char** argv)
//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(),R.getListTransitionAP(),R.getListPlaceAP()),spot::twa::prop_set::all(), true);
+ 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 ?";
@@ -303,7 +301,7 @@ int main(int argc, char** argv)
{
if (task_id==0) cout<<"**************Hybrid version**************** \n" <<endl;
if (strcmp(argv[1],"otf")) {
- HybridSOG DR(R, bound);
+ HybridSOG DR(Rnewnet, bound);
LDDGraph g(&DR);
if (task_id==0) cout<<"Building the Distributed SOG by "<<n_tasks<<" processes..."<<endl;
DR.computeDSOG(g);
@@ -320,7 +318,7 @@ int main(int argc, char** argv)
cout<<" Task id "<<task_id<<"/"<<n_tasks<<endl;
if (task_id!=n_tasks) {
cout<<"N task :"<<n_tasks<<endl;
- MCHybridSOG DR(R,gprocess, bound,false);
+ MCHybridSOG DR(Rnewnet,gprocess, bound,false);
LDDGraph g(&DR);
DR.computeDSOG(g);
}
@@ -328,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,R.getListTransitionAP(),R.getListPlaceAP(),R),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;
//while(1);
/* auto k =
@@ -350,7 +348,7 @@ int main(int argc, char** argv)
//cout<<" sequential version using Sylvan : 1 with BuDDy : 2 \n" <<endl;
cout<<"*************Distibuted version******************* \n" <<endl;
{
- DistributedSOG DR(R, bound);
+ DistributedSOG DR(Rnewnet, bound);
LDDGraph g(nullptr);
DR.computeDSOG(g);
}
diff --git a/src/threadSOG.cpp b/src/threadSOG.cpp
index 328b88f14b5136ae45f7391ade3eb892edc2cdf7..231b1b0fe1aa987f94c168a1a1d97137d2a2ef8b 100644
--- a/src/threadSOG.cpp
+++ b/src/threadSOG.cpp
@@ -66,7 +66,7 @@ threadSOG::threadSOG(const NewNet &R, int BOUND, int nbThread,bool uselace,bool
m_placeName=R.m_placePosName;
cout<<"Toutes les Transitions:"<<endl;
- map<string,int>::iterator it2=m_transitionName.begin();
+ map<string,uint16_t>::iterator it2=m_transitionName.begin();
for (;it2!=m_transitionName.end();it2++) {
cout<<(*it2).first<<" : "<<(*it2).second<<endl;}