From 7bea6949a2239c6bd43fb215af66d26e83e77195 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Thu, 8 Aug 2019 01:17:25 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20src/HybridKripke.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20?=
=?UTF-8?q?=20=20=20=20src/HybridKripkeIterator.cpp=20=09modifi=C3=A9?=
=?UTF-8?q?=C2=A0:=20=20=20=20=20=20=20=20=20src/HybridKripkeIterator.h=20?=
=?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/HybridKrip?=
=?UTF-8?q?keState.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20sr?=
=?UTF-8?q?c/HybridSOG.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20?=
=?UTF-8?q?=20=20src/MCHybridSOG.cpp=20=09modifi=C3=A9=C2=A0:=20=20=20=20?=
=?UTF-8?q?=20=20=20=20=20src/main.cpp?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/HybridKripke.cpp | 18 +++++-----
src/HybridKripkeIterator.cpp | 53 +++++++----------------------
src/HybridKripkeIterator.h | 16 +++------
src/HybridKripkeState.h | 64 ++++++++++++++++++++++++++++--------
src/HybridSOG.cpp | 2 +-
src/MCHybridSOG.cpp | 6 ++--
src/main.cpp | 21 ++++++++----
7 files changed, 92 insertions(+), 88 deletions(-)
diff --git a/src/HybridKripke.cpp b/src/HybridKripke.cpp
index d9e4bc9..50cd35e 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 93424f9..5297b26 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 a62012e..c56a8e8 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 902d5dd..935d75d 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 ae14cc8..4da8513 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 7f9b91f..a0569d6 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 5477c36..5d36106 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";
}
}
--
GitLab