diff --git a/src/HybridKripke.cpp b/src/HybridKripke.cpp
index d9e4bc98bcd5aad23afbcbb3272525e45186d07a..50cd35e772004513c236f071558d826f069ac4a1 100644
--- a/src/HybridKripke.cpp
+++ b/src/HybridKripke.cpp
@@ -71,20 +71,18 @@ std::string HybridKripke::format_state(const spot::state* s) const
HybridKripkeIterator* HybridKripke::succ_iter(const spot::state* s) const {
//cout<<__func__<<endl;
- auto ss = static_cast<const HybridKripkeState*>(s);
- char id[16];
- memcpy(id,ss->getId(),16);
+ auto ss = static_cast<const HybridKripkeState*>(s);
bdd cond = state_condition(ss);
- uint16_t pcontainer=ss->getContainerProcess();
- /* if (iter_cache_)
+ HybridKripkeState* st=ss;
+ if (iter_cache_)
{
auto it = static_cast<HybridKripkeIterator*>(iter_cache_);
iter_cache_ = nullptr; // empty the cache
- it->recycle(id,pcontainer,cond);
+ it->recycle(*st,cond);
return it;
- }*/
+ }
- return new HybridKripkeIterator(id,pcontainer,cond);
+ return new HybridKripkeIterator(*st,cond);
}
@@ -92,14 +90,14 @@ bdd HybridKripke::state_condition(const spot::state* s) const
{
auto ss = static_cast<const HybridKripkeState*>(s);
- set<uint16_t>* marked_place=ss->getMarkedPlaces();
+ list<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();
+ list<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);
diff --git a/src/HybridKripkeIterator.cpp b/src/HybridKripkeIterator.cpp
index 93424f9fdaa0d1096af5f77ca72b04f05bd5cf37..5297b26a16e881864625a309c8fc4f29d98267d1 100644
--- a/src/HybridKripkeIterator.cpp
+++ b/src/HybridKripkeIterator.cpp
@@ -2,76 +2,46 @@
#include "LDDGraph.h"
#include "HybridKripkeState.h"
#include "HybridKripkeIterator.h"
-#define TAG_ASK_SUCC 4
-#define TAG_ACK_SUCC 11
-#define TAG_NOTCOMPLETED 20
-HybridKripkeIterator::HybridKripkeIterator(char *id,uint16_t pcontainer, bdd cnd): m_pcontainer(pcontainer),kripke_succ_iterator(cnd)
+
+HybridKripkeIterator::HybridKripkeIterator(HybridKripkeState &st, bdd cnd): kripke_succ_iterator(cnd)
{
- memcpy(m_id,id,16);
- // Ask 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;
- 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;
- 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_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);
- indice+=2;
- m_succ.push_back(*succ_elt);
- delete succ_elt;
- }
+ m_current_state=&st;
+
}
bool HybridKripkeIterator::first() {
//cout<<"entering "<<__func__<<endl;
m_current_edge=0;
- return m_succ.size()!=0;
+ return m_current_state->getListSucc()->size()!=0;
}
bool HybridKripkeIterator::next() {
m_current_edge++;
- return m_current_edge<m_succ.size();
+ return m_current_edge<m_current_state->getListSucc()->size();
}
bool HybridKripkeIterator::done() const {
//cout<<"entring /excit"<<__func__<<endl;
- return m_current_edge==m_succ.size();
+ return m_current_edge==m_current_state->getListSucc()->size();
}
HybridKripkeState* HybridKripkeIterator::dst() const
{
- succ_t succ_elt= m_succ.at(m_current_edge);
+ succ_t succ_elt= m_current_state->getListSucc()->at(m_current_edge);
return new HybridKripkeState(succ_elt.id,succ_elt.pcontainer);
}
bdd HybridKripkeIterator::cond() const {
//cout<<"entering "<<__func__<<endl;
- succ_t succ_elt=m_succ.at(m_current_edge);
+ succ_t succ_elt=m_current_state->getListSucc()->at(m_current_edge);
if (succ_elt.transition==-1) return bddtrue;
@@ -93,11 +63,10 @@ HybridKripkeIterator::~HybridKripkeIterator()
}
-void HybridKripkeIterator::recycle(char *id,uint16_t pcontainer, bdd cond)
+void HybridKripkeIterator::recycle(HybridKripkeState &st, bdd cond)
{
//cout<<__func__<<endl;
- memcpy(m_id,id,16);
- m_pcontainer=pcontainer;
+ m_current_state=&st;
spot::kripke_succ_iterator::recycle(cond);
}
diff --git a/src/HybridKripkeIterator.h b/src/HybridKripkeIterator.h
index a62012e2572ba6767ea6aed646e3b18770dfebdf..c56a8e84ebf5d8a59b99bdd53c44c58a6801829b 100644
--- a/src/HybridKripkeIterator.h
+++ b/src/HybridKripkeIterator.h
@@ -4,11 +4,7 @@
#include "ModelCheckBaseMT.h"
#include <spot/kripke/kripke.hh>
// Iterator for a SOG graph
-typedef struct {
- char id[17];
- int16_t transition;
- uint16_t pcontainer;
-} succ_t;
+
class HybridKripkeIterator : public spot::kripke_succ_iterator
{
public:
@@ -18,7 +14,7 @@ public:
static spot::bdd_dict_ptr* m_dict_ptr;
- HybridKripkeIterator(char *id,uint16_t pcontainer, bdd cnd);
+ HybridKripkeIterator(HybridKripkeState &st, bdd cnd);
virtual ~HybridKripkeIterator();
bool first() override;
bool next() override;
@@ -28,16 +24,14 @@ public:
// HybridKripkeState* current_state() const;
- void recycle(char *id,uint16_t pcontainer, bdd cond);
+ void recycle(HybridKripkeState &st, bdd cond);
std::string format_transition() const;
private:
-
- char m_id[16];
- uint16_t m_pcontainer;
unsigned int m_current_edge=0;
- vector<succ_t> m_succ;
+ HybridKripkeState *m_current_state;
+
};
diff --git a/src/HybridKripkeState.h b/src/HybridKripkeState.h
index 902d5dd9dd3c1b6b349f98f33d3ad0e025f4483c..935d75d654e741669b1f1ae3f428949163456fe4 100644
--- a/src/HybridKripkeState.h
+++ b/src/HybridKripkeState.h
@@ -6,6 +6,14 @@
#include "ModelCheckBaseMT.h"
#define TAG_ASK_STATE 9
#define TAG_ACK_STATE 10
+#define TAG_ASK_SUCC 4
+#define TAG_ACK_SUCC 11
+#define TAG_NOTCOMPLETED 20
+typedef struct {
+ char id[17];
+ int16_t transition;
+ uint16_t pcontainer;
+} succ_t;
class HybridKripkeState : public spot::state
{
public:
@@ -31,26 +39,54 @@ public:
memcpy(&n_mp,message+8,2);
//cout<<" Marked places :"<<n_mp<<endl;
- uint16_t indice=10;
- for(int i=0;i<n_mp;i++) {
+ uint32_t indice=10;
+ for(uint16_t i=0;i<n_mp;i++) {
uint16_t val;
memcpy(&val,message+indice,2);
- m_marked_places.insert(val);
+ m_marked_places.emplace_front(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++) {
+ for(uint16_t i=0;i<n_up;i++) {
uint16_t val;
memcpy(&val,message+indice,2);
- m_unmarked_places.insert(val);
+ m_unmarked_places.emplace_front(val);
indice+=2;
}
+ // Get successors
+ MPI_Send(m_id,16,MPI_BYTE,m_container, TAG_ASK_SUCC, MPI_COMM_WORLD);
+
+ // Receive list of successors
+
+ MPI_Probe(MPI_ANY_SOURCE,MPI_ANY_TAG,MPI_COMM_WORLD,&status);
+ MPI_Get_count(&status, MPI_BYTE, &nbytes);
+ char inmsg[nbytes+1];
+ //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;
+ 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_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);
+ indice+=2;
+ m_succ.push_back(*succ_elt);
+ delete succ_elt;
+ }
- }
+
+}
// 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);
@@ -82,27 +118,27 @@ public:
else
return h > oh;
}
- unsigned char * getId() {
- // cout<<__func__<<endl;
+ char * getId() {
return m_id;
}
uint16_t getContainerProcess() {
return m_container;
}
- set<uint16_t> * getMarkedPlaces() { return &m_marked_places;}
- set<uint16_t> * getUnmarkedPlaces() { return &m_unmarked_places;}
+ list<uint16_t> * getMarkedPlaces() { return &m_marked_places;}
+ list<uint16_t> * getUnmarkedPlaces() { return &m_unmarked_places;}
+ vector<succ_t>* getListSucc() { return &m_succ;}
protected:
-private:
- //LDDState *m_state;
+private:
char m_id[17];
uint32_t m_pos;
size_t m_hashid;
bool m_div;
bool m_deadlock;
uint16_t m_container;
- set<uint16_t> m_marked_places;
- set<uint16_t> m_unmarked_places;
+ list<uint16_t> m_marked_places;
+ list<uint16_t> m_unmarked_places;
+ vector<succ_t> m_succ;
};
diff --git a/src/HybridSOG.cpp b/src/HybridSOG.cpp
index ae14cc890331e05cadfb29dea2a5f5d4ed8cbba0..4da85135feb6a97fc2329a2de3481f2d5004a5a6 100644
--- a/src/HybridSOG.cpp
+++ b/src/HybridSOG.cpp
@@ -738,7 +738,7 @@ void HybridSOG::computeDSOG(LDDGraph &g)
MPI_Barrier(MPI_COMM_WORLD);
// int nb_th;
m_nb_thread=nb_th;
- cout<<"nb de thread"<<nb_th<<endl;
+ //cout<<"nb de thread"<<nb_th<<endl;
int rc;
m_id_thread=0;
m_nbrecv=0;
diff --git a/src/MCHybridSOG.cpp b/src/MCHybridSOG.cpp
index 7f9b91f512542aae8d53e06bc623192ebe28c848..a0569d68770c45369427441ff6f8883f5e9c5e0e 100644
--- a/src/MCHybridSOG.cpp
+++ b/src/MCHybridSOG.cpp
@@ -623,12 +623,12 @@ void MCHybridSOG::computeDSOG(LDDGraph &g)
double tps;
// double t1=(double)clock() / (double)CLOCKS_PER_SEC;
- cout<<"process with id "<<task_id<<" / "<<n_tasks<<endl;
+ //cout<<"process with id "<<task_id<<" / "<<n_tasks<<endl;
MPI_Barrier(m_comm_world);
- cout<<"After!!!!process with id "<<task_id<<endl;
+ // cout<<"After!!!!process with id "<<task_id<<endl;
// int nb_th;
m_nb_thread=nb_th;
- cout<<"nb de thread"<<nb_th<<endl;
+ //cout<<"nb de thread"<<nb_th<<endl;
int rc;
m_id_thread=0;
m_nbrecv=0;
diff --git a/src/main.cpp b/src/main.cpp
index 5477c36adbba09f59a7b275fb926a460f253be45..5d36106fafdeb6019ba12081c0493c4dd65694a1 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -315,7 +315,7 @@ int main(int argc, char** argv)
}
MPI_Comm gprocess;
MPI_Comm_split(MPI_COMM_WORLD,task_id==n_tasks?0:1,task_id,&gprocess);
- cout<<" Task id "<<task_id<<"/"<<n_tasks<<endl;
+ //cout<<" Task id "<<task_id<<"/"<<n_tasks<<endl;
if (task_id!=n_tasks) {
cout<<"N task :"<<n_tasks<<endl;
MCHybridSOG DR(Rnewnet,gprocess, bound,false);
@@ -326,18 +326,25 @@ 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;
- //while(1);
- /* auto k =
- std::make_shared<HybridKripke>(d,R.getListTransitionAP(),R.getListPlaceAP());*/
+
+
fstream file;
string st(argv[3]);
st+=".dot";
file.open(st.c_str(),fstream::out);
spot::print_dot(file, k,"ka");
- file.close();
-
+ file.close();*/
+ auto k =
+ std::make_shared<HybridKripke>(d,Rnewnet.getListTransitionAP(),Rnewnet.getListPlaceAP(),Rnewnet);
+ if (auto run = k->intersecting_run(af))
+ {
+ std::cout << "formula is violated by the following run:\n"<<*run<<endl;
+ cout<<"=================================="<<endl;
+ }
+ else
+ std::cout << "formula is verified\n";
}
}