diff --git a/CMakeLists.txt b/CMakeLists.txt
index 990d917d17ed365c14997ae7a4ef3f69d930e1f5..5ed08f3a1756867c18241faf6399e8a58f036105 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -5,7 +5,7 @@ cmake_minimum_required(VERSION 3.8 FATAL_ERROR)
project(pmc-sog C CXX)
-set(CMAKE_CXX_STANDARD 14)
+#set(CMAKE_CXX_STANDARD 14)
set(CMAKE_CXX_STANDARD_REQUIRED ON)
set(CMAKE_CXX_EXTENSIONS OFF)
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 89b6a20ae8dde0c64d72997e49de7cddf344ee63..759b2b3fdb27fb58ba3005404da1455546b3b3cb 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -77,7 +77,9 @@ add_executable(mc-sog main.cpp
HybridKripkeIterator.h
HybridKripkeState.cpp
HybridKripkeState.h
- )
+ SylvanWrapper.cpp
+ SylvanWrapper.h
+ )
target_link_libraries(mc-sog
bddx
diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp
index 0bdc5abef6cb5e698d16b626247471ea3cce8b68..ea44c8242996cedcacf5b69d070b235821e9cfd2 100644
--- a/src/CommonSOG.cpp
+++ b/src/CommonSOG.cpp
@@ -1,135 +1,136 @@
#include "CommonSOG.h"
+#include "sylvan.h"
#include "sylvan_seq.h"
+#include <sylvan_sog.h>
+#include <sylvan_int.h>
+#include <stack>
+#define GETNODE(mdd) ((mddnode_t)llmsset_index_to_ptr(nodes, mdd))
const vector<class Place> *_places = NULL;
-CommonSOG::CommonSOG()
-{
+
+CommonSOG::CommonSOG() {
//ctor
}
-CommonSOG::~CommonSOG()
-{
+CommonSOG::~CommonSOG() {
//dtor
}
-LDDGraph *CommonSOG::getGraph() const
-{
+LDDGraph *CommonSOG::getGraph() const {
return m_graph;
}
-MDD CommonSOG::Accessible_epsilon ( MDD From )
-{
+MDD CommonSOG::Accessible_epsilon(MDD From) {
MDD M1;
- MDD M2=From;
+ MDD M2 = From;
do {
- M1=M2;
- for ( Set::const_iterator i=m_nonObservable.begin(); ! ( i==m_nonObservable.end() ); i++ ) {
- MDD succ= lddmc_firing_mono ( M2,m_tb_relation[ ( *i )].getMinus(),m_tb_relation[ ( *i )].getPlus() );
- M2=lddmc_union_mono ( M2,succ );
- //M2=succ|M2;
+ M1 = M2;
+ for (Set::const_iterator i = m_nonObservable.begin(); !(i == m_nonObservable.end()); i++) {
+ //fireTransition
+
+ MDD succ = fireTransition(M2, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus());
+
+ M2 = lddmc_union_mono(M2, succ);
+
}
- } while ( M1!=M2 );
+ } while (M1 != M2);
return M2;
}
+
// Return the set of firable observable transitions from an agregate
-Set CommonSOG::firable_obs ( MDD State )
-{
+Set CommonSOG::firable_obs(MDD State) {
Set res;
- for ( Set::const_iterator i=m_observable.begin(); ! ( i==m_observable.end() ); i++ ) {
+ for (Set::const_iterator i = m_observable.begin(); !(i == m_observable.end()); i++) {
//cout<<"firable..."<<endl;
- MDD succ = lddmc_firing_mono ( State,m_tb_relation[ ( *i )].getMinus(),m_tb_relation[ ( *i )].getPlus() );
- if ( succ!=lddmc_false ) {
- res.insert ( *i );
+ MDD succ = fireTransition(State, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus());
+ if (succ != lddmc_false) {
+ res.insert(*i);
}
}
return res;
}
-MDD CommonSOG::get_successor ( MDD From,int t )
-{
- return lddmc_firing_mono ( From,m_tb_relation[ ( t )].getMinus(),m_tb_relation[ ( t )].getPlus() );
+MDD CommonSOG::get_successor(MDD From, int t) {
+ return fireTransition(From, m_tb_relation[(t)].getMinus(), m_tb_relation[(t)].getPlus());
}
-MDD CommonSOG::ImageForward ( MDD From )
-{
- MDD Res=lddmc_false;
- for ( Set::const_iterator i=m_nonObservable.begin(); ! ( i==m_nonObservable.end() ); i++ ) {
- MDD succ= lddmc_firing_mono ( From,m_tb_relation[ ( *i )].getMinus(),m_tb_relation[ ( *i )].getPlus() );
- Res=lddmc_union_mono ( Res,succ );
+MDD CommonSOG::ImageForward(MDD From) {
+ MDD Res = lddmc_false;
+ for (Set::const_iterator i = m_nonObservable.begin(); !(i == m_nonObservable.end()); i++) {
+ MDD succ = fireTransition(From, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus());
+ Res = lddmc_union_mono(Res, succ);
}
return Res;
}
/*----------------------------------------------CanonizeR()------------------------------------*/
-MDD CommonSOG::Canonize ( MDD s,unsigned int level )
-{
- if ( level>m_nbPlaces || s==lddmc_false ) {
+MDD CommonSOG::Canonize(MDD s, unsigned int level) {
+ if (level > m_nbPlaces || s == lddmc_false) {
return lddmc_false;
}
- if ( isSingleMDD ( s ) ) {
+ if (isSingleMDD(s)) {
return s;
}
- MDD s0=lddmc_false,s1=lddmc_false;
+ MDD s0 = lddmc_false, s1 = lddmc_false;
- bool res=false;
+ bool res = false;
do {
- if ( get_mddnbr ( s,level ) >1 ) {
- s0=ldd_divide_rec ( s,level );
- s1=ldd_minus ( s,s0 );
- res=true;
+ if (get_mddnbr(s, level) > 1) {
+ s0 = ldd_divide_rec(s, level);
+ s1 = ldd_minus(s, s0);
+ res = true;
} else {
level++;
}
- } while ( level<m_nbPlaces && !res );
+ } while (level < m_nbPlaces && !res);
- if ( s0==lddmc_false && s1==lddmc_false ) {
+ if (s0 == lddmc_false && s1 == lddmc_false) {
return lddmc_false;
}
// if (level==nbPlaces) return lddmc_false;
- MDD Front,Reach;
- if ( s0!=lddmc_false && s1!=lddmc_false ) {
- Front=s1;
- Reach=s1;
+ MDD Front, Reach;
+ if (s0 != lddmc_false && s1 != lddmc_false) {
+ Front = s1;
+ Reach = s1;
do {
// cout<<"premiere boucle interne \n";
- Front=ldd_minus ( ImageForward ( Front ),Reach );
- Reach = lddmc_union_mono ( Reach,Front );
- s0 = ldd_minus ( s0,Front );
- } while ( ( Front!=lddmc_false ) && ( s0!=lddmc_false ) );
+ Front = ldd_minus(ImageForward(Front), Reach);
+ Reach = lddmc_union_mono(Reach, Front);
+ s0 = ldd_minus(s0, Front);
+ } while ((Front != lddmc_false) && (s0 != lddmc_false));
}
- if ( ( s0!=lddmc_false ) && ( s1!=lddmc_false ) ) {
- Front=s0;
+ if ((s0 != lddmc_false) && (s1 != lddmc_false)) {
+ Front = s0;
Reach = s0;
do {
// cout<<"deuxieme boucle interne \n";
- Front=ldd_minus ( ImageForward ( Front ),Reach );
- Reach = lddmc_union_mono ( Reach,Front );
- s1 = ldd_minus ( s1,Front );
- } while ( Front!=lddmc_false && s1!=lddmc_false );
+ Front = ldd_minus(ImageForward(Front), Reach);
+ Reach = lddmc_union_mono(Reach, Front);
+ s1 = ldd_minus(s1, Front);
+ } while (Front != lddmc_false && s1 != lddmc_false);
}
+ MDD Repr = lddmc_false;
- MDD Repr=lddmc_false;
-
- if ( isSingleMDD ( s0 ) ) {
- Repr=s0;
+ if (isSingleMDD(s0)) {
+ Repr = s0;
} else {
- Repr=Canonize ( s0,level );
+ Repr = Canonize(s0, level);
}
- if ( isSingleMDD ( s1 ) ) {
- Repr=lddmc_union_mono ( Repr,s1 );
+ if (isSingleMDD(s1)) {
+ Repr = lddmc_union_mono(Repr, s1);
} else {
- Repr=lddmc_union_mono ( Repr,Canonize ( s1,level ) );
+ Repr = lddmc_union_mono(Repr, Canonize(s1, level));
}
@@ -138,85 +139,159 @@ MDD CommonSOG::Canonize ( MDD s,unsigned int level )
}
-void CommonSOG::printhandler ( ostream &o, int var )
-{
- o << ( *_places ) [var/2].name;
- if ( var%2 ) {
+void CommonSOG::printhandler(ostream &o, int var) {
+ o << (*_places)[var / 2].name;
+ if (var % 2) {
o << "_p";
}
}
-vector<TransSylvan>* CommonSOG::getTBRelation()
-{
+vector<TransSylvan> *CommonSOG::getTBRelation() {
return &m_tb_relation;
}
-Set * CommonSOG::getNonObservable()
-{
+Set *CommonSOG::getNonObservable() {
return &m_nonObservable;
}
/*********Returns the count of places******************************************/
-unsigned int CommonSOG::getPlacesCount()
-{
+unsigned int CommonSOG::getPlacesCount() {
return m_nbPlaces;
}
/**** Detect divergence in an agregate ****/
-bool CommonSOG::Set_Div ( MDD &M ) const
-{
+bool CommonSOG::Set_Div(MDD &M) const {
- if ( m_nonObservable.empty() ) {
+ if (m_nonObservable.empty()) {
return false;
}
Set::const_iterator i;
- MDD Reached,From;
+ MDD Reached, From;
//cout<<"Ici detect divergence \n";
- Reached=lddmc_false;
- From=M;
+ Reached = lddmc_false;
+ From = M;
do {
- for ( i=m_nonObservable.begin(); ! ( i==m_nonObservable.end() ); i++ ) {
+ for (i = m_nonObservable.begin(); !(i == m_nonObservable.end()); i++) {
- MDD To= lddmc_firing_mono ( From,m_tb_relation[ ( *i )].getMinus(),m_tb_relation[ ( *i )].getPlus() );
- Reached=lddmc_union_mono ( Reached,To );
+ MDD To = fireTransition(From, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus());
+ Reached = lddmc_union_mono(Reached, To);
//Reached=To;
}
- if ( Reached==From ) {
+ if (Reached == From) {
return true;
}
- From=Reached;
- Reached=lddmc_false;
+ From = Reached;
+ Reached = lddmc_false;
- } while ( Reached!=lddmc_false && Reached != lddmc_true );
+ } while (Reached != lddmc_false && Reached != lddmc_true);
return false;
}
/**** Detetc deadlocks ****/
-bool CommonSOG::Set_Bloc ( MDD &M ) const
-{
+bool CommonSOG::Set_Bloc(MDD &M) const {
- MDD cur=lddmc_true;
- for ( vector<TransSylvan>::const_iterator i = m_tb_relation.begin(); i!=m_tb_relation.end(); i++ ) {
+ MDD cur = lddmc_true;
+ for (vector<TransSylvan>::const_iterator i = m_tb_relation.begin(); i != m_tb_relation.end(); i++) {
- cur=cur& ( TransSylvan ( *i ).getMinus() );
+ cur = cur & (TransSylvan(*i).getMinus());
}
- return ( ( M&cur ) !=lddmc_false );
+ return ((M & cur) != lddmc_false);
//BLOCAGE
}
-string CommonSOG::getTransition ( int pos )
-{
- return m_graph->getTransition ( pos );
+string CommonSOG::getTransition(int pos) {
+ return m_graph->getTransition(pos);
}
-string CommonSOG::getPlace ( int pos )
-{
- return m_graph->getPlace ( pos );
+string CommonSOG::getPlace(int pos) {
+ return m_graph->getPlace(pos);
}
-static LDDGraph *CommonSOG::m_graph;
+
+LDDGraph *CommonSOG::m_graph;
+struct elt_t {
+ MDD cmark;
+ MDD minus;
+ MDD plus;
+ uint32_t level;
+};
+
+MDD CommonSOG::fireTransition(MDD cmark, MDD minus, MDD plus) {
+ return lddmc_firing_mono(cmark,minus,plus);
+ // for an empty set of source states, or an empty transition relation, return the empty set
+
+ MDD result;
+ mddnode_t n_cmark, n_plus, n_minus;
+ uint32_t value, value_minus, value_plus;
+ std::stack<elt_t> lstack;
+ elt_t elt;
+ elt.cmark = cmark;
+ elt.plus = plus;
+ elt.minus = minus;
+ elt.level = 0;
+ lstack.push(elt);
+ result = lddmc_false;
+ uint32_t *currentMarking = new uint32_t[m_nbPlaces];
+ elt_t relt;
+ bool goDown = false;
+ //MDD temp;
+ while (!lstack.empty() || goDown) {
+ if (!goDown) {
+ elt = lstack.top();
+ lstack.pop();
+ n_cmark = GETNODE(elt.cmark);
+ n_minus = GETNODE(elt.minus);
+ n_plus = GETNODE(elt.plus);
+ value = mddnode_getvalue(n_cmark);
+ value_minus = mddnode_getvalue(n_minus);
+ value_plus = mddnode_getvalue(n_plus);
+ } else goDown = false;
+
+ //cout << "Level : " << elt.level << endl;
+ //cout << "Current : " << value << " Minus : " << value_minus << " Plus : " << value_plus << endl;
+ if (value >= value_minus) {
+ *(currentMarking + elt.level) = value - value_minus + value_plus;
+ if (elt.level == m_nbPlaces - 1) {
+ MDD b = ldd_cube(currentMarking, m_nbPlaces);
+ result = lddmc_union_mono(result, b);
+ } else { // Goto next level and push right
+ if (mddnode_getright(n_cmark) != lddmc_false) { // Look for another node in the same level
+ relt = elt;
+ relt.cmark = mddnode_getright(n_cmark);
+ lstack.push(relt);
+ }
+ //} while (temp>lddmc_true);
+ if (elt.level < m_nbPlaces - 1) { // Go down
+ elt.level++;
+ elt.cmark = mddnode_getdown(n_cmark);
+ n_cmark = GETNODE(elt.cmark);
+ elt.minus = mddnode_getdown(n_minus);
+ n_minus = GETNODE(elt.minus);
+ elt.plus = mddnode_getdown(n_plus);
+ n_plus = GETNODE(elt.plus);
+ goDown = true;
+ value = mddnode_getvalue(n_cmark);
+ value_minus = mddnode_getvalue(n_minus);
+ value_plus = mddnode_getvalue(n_plus);
+ }
+ }
+ } else {
+ // Look for another node in the same level
+ elt.cmark = mddnode_getright(n_cmark);
+ while (elt.cmark>lddmc_true && !goDown) {
+ n_cmark = GETNODE(elt.cmark);
+ value = mddnode_getvalue(n_cmark);
+ if (value >= value_minus) goDown = true; else elt.cmark = mddnode_getright(n_cmark);
+ }
+
+ }
+ }
+ delete[]currentMarking;
+
+ return result;
+}
\ No newline at end of file
diff --git a/src/CommonSOG.h b/src/CommonSOG.h
index 1b59950b5c9c0b7399abaabc4da7279f140369f3..e5136a0c038b0413f48cb58213c00bec26b3f46e 100644
--- a/src/CommonSOG.h
+++ b/src/CommonSOG.h
@@ -8,6 +8,7 @@
#include <stack>
#include <mutex>
#include <atomic>
+
// #define GCENABLE 0
class LDDState;
typedef pair<LDDState *, MDD> couple;
@@ -16,6 +17,7 @@ typedef stack<Pair> pile;
class LDDGraph;
+
class CommonSOG
{
public:
@@ -52,7 +54,9 @@ class CommonSOG
uint8_t m_nb_thread;
std::mutex m_graph_mutex,m_gc_mutex;
atomic<uint8_t> m_gc;
+ MDD fireTransition(MDD cmark,MDD minus, MDD plus);
private:
+
};
#endif // COMMONSOG_H
diff --git a/src/HybridKripke.cpp b/src/HybridKripke.cpp
index e7eb9e37e9d443d6c1c7017e13157bdc6054037e..ad06063e81ae32c176c928064f6d714e73ceeb00 100644
--- a/src/HybridKripke.cpp
+++ b/src/HybridKripke.cpp
@@ -53,6 +53,7 @@ state* HybridKripke::get_init_state() const {
memcpy(elt->id,message,16);
memcpy(&elt->pcontainer,message+16,2);
elt->_virtual=false;
+
return new HybridKripkeState(*elt);
}
@@ -71,14 +72,16 @@ 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;
- }*/
-
+ }
+ SylvanWrapper::m_agg++;
+ SylvanWrapper::m_Size+=ss->getSize();
+ cout<<"Expolored states : "<<SylvanWrapper::m_Size<<" , Explored agg : "<<SylvanWrapper::m_agg<<" , Avg per agg : " <<SylvanWrapper::m_Size/SylvanWrapper::m_agg<<endl;
return new HybridKripkeIterator(*st,cond);
}
@@ -100,7 +103,8 @@ bdd HybridKripke::state_condition(const spot::state* s) const
spot::formula f=spot::formula::ap(name);
result&=!bdd_ithvar((dict_->var_map.find(f))->second);
}
- return result;
+
+ return result;
}
diff --git a/src/HybridKripkeIterator.cpp b/src/HybridKripkeIterator.cpp
index f82ceae43593cd5e890aab2151497a92be545e6c..7202533a5693ea7e09dc3d892d80b4f2cac50bb3 100644
--- a/src/HybridKripkeIterator.cpp
+++ b/src/HybridKripkeIterator.cpp
@@ -63,6 +63,6 @@ void HybridKripkeIterator::recycle(HybridKripkeState &st, bdd cond)
spot::kripke_succ_iterator::recycle(cond);
}
-static NewNet * HybridKripkeIterator::m_net;
-static spot::bdd_dict_ptr* HybridKripkeIterator::m_dict_ptr;
+NewNet * HybridKripkeIterator::m_net;
+spot::bdd_dict_ptr* HybridKripkeIterator::m_dict_ptr;
diff --git a/src/HybridKripkeState.h b/src/HybridKripkeState.h
index cd5afa9496e16b47b5f2b76879cfff5eb4376b8f..7d1b4b3f7caee717a848e245c10f3a790e3478ee 100644
--- a/src/HybridKripkeState.h
+++ b/src/HybridKripkeState.h
@@ -4,6 +4,7 @@
#include <mpi.h>
#include "LDDState.h"
#include "ModelCheckBaseMT.h"
+#include "SylvanWrapper.h"
constexpr auto TAG_ASK_STATE = 9;
constexpr auto TAG_ACK_STATE = 10;
#define TAG_ASK_SUCC 4
@@ -80,6 +81,9 @@ public:
memcpy(&divblock,message+indice,1);
m_div=divblock & 1;
m_deadlock=(divblock>>1) & 1;
+ indice++; // Added for stats
+ memcpy(&m_size,message+indice,8); // Added for stats
+
// Get successors
MPI_Send(m_id,16,MPI_BYTE,m_container, TAG_ASK_SUCC, MPI_COMM_WORLD);
@@ -169,15 +173,17 @@ public:
}
list<uint16_t> * getMarkedPlaces() { return &m_marked_places;}
list<uint16_t> * getUnmarkedPlaces() { return &m_unmarked_places;}
- vector<succ_t>* getListSucc() { return &m_succ;}
+ vector<succ_t>* getListSucc() { return &m_succ;}
+ uint64_t getSize() {return m_size;} // Added for stats
protected:
private:
char m_id[17];
- uint32_t m_pos;
+ uint32_t m_pos; // Added for stats
size_t m_hashid;
bool m_div;
bool m_deadlock;
+ uint64_t m_size;
uint16_t m_container;
list<uint16_t> m_marked_places;
list<uint16_t> m_unmarked_places;
diff --git a/src/MCHybridSOG.cpp b/src/MCHybridSOG.cpp
index 574dbc99e84cd476ed150cce7445a2b2d8a760df..7986e0506a5aee8e2e213d158331ecee53ea4ecc 100644
--- a/src/MCHybridSOG.cpp
+++ b/src/MCHybridSOG.cpp
@@ -6,7 +6,7 @@
#include "sylvan_sog.h"
#include "sylvan_seq.h"
#include <sylvan_int.h>
-
+#include "SylvanWrapper.h"
#include <openssl/md5.h>
#define GETNODE(mdd) ((mddnode_t)llmsset_index_to_ptr(nodes, mdd))
@@ -135,21 +135,17 @@ void *MCHybridSOG::doCompute()
/****************************************** initial state ********************************************/
if ( task_id==0 && id_thread==0 ) {
string* chaine=new string();
-
-
LDDState *c=new LDDState;
MDD Complete_meta_state=Accessible_epsilon ( m_initialMarking );
c->m_lddstate=Complete_meta_state;
ldd_refs_push ( Complete_meta_state );
// MDD reduced_initialstate=Canonize(Complete_meta_state,0);
-
convert_wholemdd_stringcpp ( Complete_meta_state,*chaine );
get_md5 ( *chaine,Identif );
//lddmc_getsha(Complete_meta_state, Identif);
uint16_t destination= ( uint16_t ) ( Identif[0]%n_tasks );
c->setProcess ( destination );
if ( destination==0 ) {
-
m_nbmetastate++;
Set fire=firable_obs ( Complete_meta_state );
m_st[1].push ( Pair ( couple ( c,Complete_meta_state ),fire ) );
@@ -163,11 +159,8 @@ void *MCHybridSOG::doCompute()
m_graph->insertSHA ( c );
memcpy ( c->m_SHA2,Identif,16 );
initialstate=Canonize ( Complete_meta_state,0 );
-
//#endif // REDUCE
convert_wholemdd_stringcpp ( initialstate,*chaine );
-
-
pthread_mutex_lock ( &m_spin_msg[0] );
m_msg[0].push ( MSG ( chaine,destination ) );
pthread_mutex_unlock ( &m_spin_msg[0] );
@@ -236,8 +229,6 @@ void *MCHybridSOG::doCompute()
int t = * ( e.second.begin() );
e.second.erase ( t );
reached_class=new LDDState();
-
-
MDD ldd_reachedclass=Accessible_epsilon ( get_successor ( e.first.second,t ) );
ldd_refs_push ( ldd_reachedclass );
@@ -425,15 +416,15 @@ 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;
- char mess[17];
+ char mess[25];
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;
+
m_waitingAgregate=true;
- memcpy ( m_id_md5,mess,16 );
+ memcpy ( m_id_md5,mess,16 ); // Added for stats
} else {
sendPropToMC ( pos );
}
@@ -480,6 +471,7 @@ void MCHybridSOG::read_message()
// 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[22];
memcpy ( message,i_agregate->getSHAValue(),16 );
uint16_t id_p=i_agregate->getProcess();
@@ -776,11 +768,12 @@ set<uint16_t> MCHybridSOG::getUnmarkedPlaces ( LDDState *agg )
void MCHybridSOG::sendPropToMC ( size_t pos )
{
LDDState *agg=m_graph->getLDDStateById ( pos );
+ uint64_t size=SylvanWrapper::getMarksCount(agg->m_lddstate); // Added for stats
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+5];
+ char mess_to_send[8+s_mp*2+s_up*2+5+8]; // 8 Added for stats
memcpy ( mess_to_send,&pos,8 );
//cout<<"************* Pos to send :"<<pos<<endl;
size_t indice=8;
@@ -800,5 +793,7 @@ void MCHybridSOG::sendPropToMC ( size_t pos )
divblock=divblock | ( agg->isDeadLock() <<1 );
memcpy ( mess_to_send+indice,&divblock,1 );
indice++;
+ memcpy(mess_to_send+indice,&size,8); // Added for stats
+ indice+=8;
MPI_Send ( mess_to_send,indice,MPI_BYTE,n_tasks, TAG_ACK_STATE, MPI_COMM_WORLD );
}
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index de81add4746e64f0d75ef894d5107b31dae8a7b3..10ce48cc82ace9b3f71c478295c62b4074d5c8ed 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -23,7 +23,7 @@ void ModelCheckerTh::preConfigure() {
lace_startup(0, NULL, NULL);
size_t max = 16LL<<30;
if (max > getMaxMemory()) max = getMaxMemory()/10*9;
- sylvan_set_limits(16LL<<30, 8, 0);
+ sylvan_set_limits(16LL<<29, 8, 0);
sylvan_init_package();
sylvan_init_ldd();
@@ -253,3 +253,4 @@ bool ModelCheckerTh::isNotTerminated() {
}
return !res;
}
+
diff --git a/src/ModelCheckerTh.h b/src/ModelCheckerTh.h
index a94b6c74b01c45a2b71d10f9ce6360683dd95748..23fb2923d9634409bf1bef6f8fcb852dcdafdcaa 100644
--- a/src/ModelCheckerTh.h
+++ b/src/ModelCheckerTh.h
@@ -14,6 +14,7 @@ public:
static void *threadHandler(void *context);
void *Compute_successors();
void ComputeTh_Succ();
+
private:
void preConfigure();
bool isNotTerminated();
diff --git a/src/ModelCheckerThV2.cpp b/src/ModelCheckerThV2.cpp
index 12b4efa71498cc5d06f65a46afea0b31f6d972ad..3a09e768e3074b80120e721ef50513e378f38900 100644
--- a/src/ModelCheckerThV2.cpp
+++ b/src/ModelCheckerThV2.cpp
@@ -4,7 +4,10 @@
#include <sylvan_sog.h>
#include <sylvan_int.h>
#include <functional>
-
+#include <iostream>
+#include <fstream>
+#include "SylvanWrapper.h"
+#define GETNODE(mdd) ((mddnode_t)llmsset_index_to_ptr(nodes, mdd))
using namespace sylvan;
using namespace std;
@@ -28,7 +31,7 @@ void ModelCheckerThV2::preConfigure()
if ( max > getMaxMemoryV3() ) {
max = getMaxMemoryV3() /10*9;
}
- sylvan_set_limits ( 16LL<<30, 16, 0 );
+ sylvan_set_limits ( 16LL<<29, 8, 0 );
sylvan_init_package();
sylvan_init_ldd();
@@ -111,6 +114,8 @@ void ModelCheckerThV2::Compute_successors()
if ( id_thread == 0 ) {
LDDState *c = new LDDState;
MDD Complete_meta_state=Accessible_epsilon ( m_initialMarking );
+ /*SylvanWrapper::getMarksCount(Complete_meta_state);
+ exit(0);*/
ldd_refs_push ( Complete_meta_state );
fire = firable_obs ( Complete_meta_state );
c->m_lddstate = Complete_meta_state;
@@ -122,7 +127,6 @@ void ModelCheckerThV2::Compute_successors()
m_condStack.notify_one();
m_finish_initial = true;
}
-
LDDState *reached_class;
//pthread_barrier_wait ( &m_barrier_builder );
Pair e;
@@ -132,32 +136,26 @@ void ModelCheckerThV2::Compute_successors()
lk.unlock();
if ( m_common_stack.try_pop ( e ) && !m_finish ) {
-
while ( !e.second.empty() && !m_finish ) {
int t = *e.second.begin();
e.second.erase ( t );
MDD reduced_meta = Accessible_epsilon ( get_successor ( e.first.second, t ) );
-
ldd_refs_push ( reduced_meta );
reached_class = new LDDState();
reached_class->m_lddstate = reduced_meta;
LDDState *pos = m_graph->find ( reached_class );
- if ( !pos ) {
-
+ if ( !pos ) {
m_graph->addArc();
- m_graph->insert ( reached_class );
-
+ m_graph->insert ( reached_class );
fire = firable_obs ( reduced_meta );
reached_class->setDeadLock ( Set_Bloc ( reduced_meta ) );
reached_class->setDiv ( Set_Div ( reduced_meta ) );
-
m_common_stack.push ( Pair ( couple ( reached_class, reduced_meta ), fire ) );
m_condStack.notify_one();
- m_graph_mutex.lock();
+ m_graph_mutex.lock();
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 ) );
m_graph_mutex.unlock();
-
} else {
delete reached_class;
m_graph->addArc();
@@ -170,8 +168,6 @@ void ModelCheckerThV2::Compute_successors()
}
e.first.first->setCompletedSucc();m_condBuild.notify_one();
} //end advance
-
-
} while ( !m_finish );
@@ -217,5 +213,3 @@ ModelCheckerThV2::~ModelCheckerThV2()
bool ModelCheckerThV2::hasToProcess() const {
return m_finish || !m_common_stack.empty();
}
-
-
diff --git a/src/ModelCheckerThV2.h b/src/ModelCheckerThV2.h
index ea0267c05a3f7853b311caa290fed1ab4fa515f1..610c13ebc9cd30a04fa90bc959743049221d238c 100644
--- a/src/ModelCheckerThV2.h
+++ b/src/ModelCheckerThV2.h
@@ -20,7 +20,8 @@ public:
void ComputeTh_Succ();
private:
void preConfigure();
- bool hasToProcess() const;
+ bool hasToProcess() const;
+
SafeDequeue<Pair> m_common_stack;
atomic<uint8_t> m_id_thread;
std::mutex m_mutex;
diff --git a/src/SogKripkeIteratorTh.cpp b/src/SogKripkeIteratorTh.cpp
index 638840e4a2d5254af15fd4d5e492db8f65c5a129..44356a32e7a64f8b0319f33a6720e2263f5a59e5 100644
--- a/src/SogKripkeIteratorTh.cpp
+++ b/src/SogKripkeIteratorTh.cpp
@@ -44,7 +44,7 @@ bool SogKripkeIteratorTh::done() const
SogKripkeStateTh* SogKripkeIteratorTh::dst() const
{
- /*cout<<"Source "<<m_lddstate->getLDDValue()<<"Destination :"<<m_lsucc.at(m_current_edge).first->getLDDValue()<<" in "<<m_lsucc.size()<<" / "<<m_current_edge<<endl;*/
+ //cout<<"Source "<<m_lddstate->getLDDValue()<<"Destination :"<<m_lsucc.at(m_current_edge).first->getLDDValue()<<" in "<<m_lsucc.size()<<" / "<<m_current_edge<<endl;
return new SogKripkeStateTh ( m_lsucc.at ( m_current_edge ).first );
}
@@ -54,14 +54,10 @@ bdd SogKripkeIteratorTh::cond() const
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 );
-
return result & spot::kripke_succ_iterator::cond();
}
@@ -80,7 +76,7 @@ void SogKripkeIteratorTh::recycle ( LDDState* aggregate, bdd cond )
spot::kripke_succ_iterator::recycle ( cond );
}
-static ModelCheckBaseMT * SogKripkeIteratorTh::m_builder;
-static spot::bdd_dict_ptr* SogKripkeIteratorTh::m_dict_ptr;
-static LDDState SogKripkeIteratorTh::m_deadlock;
-static LDDState SogKripkeIteratorTh::m_div;
+ModelCheckBaseMT * SogKripkeIteratorTh::m_builder;
+spot::bdd_dict_ptr* SogKripkeIteratorTh::m_dict_ptr;
+LDDState SogKripkeIteratorTh::m_deadlock;
+LDDState SogKripkeIteratorTh::m_div;
diff --git a/src/SogKripkeTh.cpp b/src/SogKripkeTh.cpp
index d410ea5a49c9b769f4d3d378066e6fefac464b17..ee2f5bae67cf28feb7b60a9e78ba40f9ccb70c6c 100644
--- a/src/SogKripkeTh.cpp
+++ b/src/SogKripkeTh.cpp
@@ -9,6 +9,7 @@
#include "SogKripkeTh.h"
#include <map>
+#include "SylvanWrapper.h"
using namespace spot;
SogKripkeTh::SogKripkeTh(const bdd_dict_ptr &dict_ptr,ModelCheckBaseMT *builder): spot::kripke(dict_ptr),m_builder(builder)
{
@@ -56,13 +57,14 @@ SogKripkeIteratorTh* SogKripkeTh::succ_iter(const spot::state* s) const {
auto ss = static_cast<const SogKripkeStateTh*>(s);
LDDState *aggregate=ss->getLDDState();
bdd cond = state_condition(ss);
- /*if (iter_cache_)
+ if (iter_cache_)
{
auto it = static_cast<SogKripkeIteratorTh*>(iter_cache_);
iter_cache_ = nullptr; // empty the cache
it->recycle(aggregate, cond);
return it;
- }*/
+ }
+
return new SogKripkeIteratorTh(aggregate,cond);
@@ -80,21 +82,22 @@ bdd SogKripkeTh::state_condition(const spot::state* s) const
auto ss = static_cast<const SogKripkeStateTh*>(s);
vector<uint16_t> marked_place = ss->getLDDState()->getMarkedPlaces(m_builder->getPlaceProposition());
-
+ SylvanWrapper::m_Size+=SylvanWrapper::getMarksCount(ss->getLDDState()->getLDDValue());
+ SylvanWrapper::m_agg++;
+ cout<<"Expolored states : "<<SylvanWrapper::m_Size<<" , Explored agg : "<<SylvanWrapper::m_agg<<" , Avg per agg : " <<SylvanWrapper::m_Size/SylvanWrapper::m_agg<<endl;
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);
+ string name=m_builder->getPlace(*it);
+ spot::formula f=spot::formula::ap(name);
+ result&=bdd_ithvar((dict_->var_map.find(f))->second);
}
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);
- result&=!bdd_ithvar((dict_->var_map.find(f))->second);
+ string name=m_builder->getPlace(*it);
+ spot::formula f=spot::formula::ap(name);
+ result&=!bdd_ithvar((dict_->var_map.find(f))->second);
}
-
return result;
}
diff --git a/src/SylvanWrapper.cpp b/src/SylvanWrapper.cpp
new file mode 100644
index 0000000000000000000000000000000000000000..2fb461ffc21c4b7db17aa10506143f3bf5c28037
--- /dev/null
+++ b/src/SylvanWrapper.cpp
@@ -0,0 +1,53 @@
+//
+// Created by chiheb on 10/06/2020.
+//
+
+
+#include "sylvan.h"
+#include "LDDState.h"
+#include <sylvan_int.h>
+#include "sylvan_seq.h"
+//#include <sylvan_sog.h>
+
+
+#include <functional>
+#include <iostream>
+#include <fstream>
+
+#include "SylvanWrapper.h"
+#define GETNODE(mdd) ((mddnode_t)llmsset_index_to_ptr(nodes, mdd))
+using namespace sylvan;
+using namespace std;
+
+
+uint64_t SylvanWrapper::m_Size=0;
+uint64_t SylvanWrapper::m_agg=0;
+/**************************************
+ * Computes number of markings in an MDD
+ * @param cmark : an MDD
+ */
+
+uint64_t SylvanWrapper::getMarksCount ( MDD cmark )
+{
+ //typedef pair<string,MDD> Pair_stack;
+ vector<MDD> local_stack;
+ uint64_t compteur=0;
+ MDD explore_mdd=cmark;
+ local_stack.push_back ( cmark );
+ do {
+ explore_mdd=local_stack.back();
+ local_stack.pop_back();
+ compteur++;
+ while ( explore_mdd!= lddmc_false && explore_mdd!=lddmc_true ) {
+ mddnode_t n_val = GETNODE ( explore_mdd );
+ if ( mddnode_getright ( n_val ) !=lddmc_false ) {
+ local_stack.push_back ( mddnode_getright ( n_val ) );
+ }
+ unsigned int val = mddnode_getvalue ( n_val );
+ explore_mdd=mddnode_getdown ( n_val );
+ }
+
+ } while ( local_stack.size() !=0 );
+
+ return compteur;
+}
diff --git a/src/SylvanWrapper.h b/src/SylvanWrapper.h
new file mode 100644
index 0000000000000000000000000000000000000000..8988d9b302dad91adec34fb34d4be91f06a69731
--- /dev/null
+++ b/src/SylvanWrapper.h
@@ -0,0 +1,18 @@
+//
+// Created by chiheb on 10/06/2020.
+//
+
+#ifndef PMC_SOG_SYLVANWRAPPER_H
+#define PMC_SOG_SYLVANWRAPPER_H
+
+
+ class SylvanWrapper {
+ public:
+ static uint64_t getMarksCount ( MDD cmark );
+ static uint64_t m_Size;
+ static uint64_t m_agg;
+
+};
+
+
+#endif //PMC_SOG_SYLVANWRAPPER_H
diff --git a/src/main.cpp b/src/main.cpp
index 1fa50200ff56f644609384e3cf3414e3be1087ee..bc7219a0ea12cc1a3d087f47d684a45213b2bcc3 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -31,6 +31,7 @@
#include "SogKripkeTh.h"
#include "HybridKripke.h"
+#include "SylvanWrapper.h"
// #include "RdPBDD.h"
@@ -175,6 +176,8 @@ int main(int argc, char **argv) {
displayCheckResult(res);
/****************************/
+
+
/*auto startTime = std::chrono::steady_clock::now();
bool res = (check.check() == 0);
auto finalTime = std::chrono::steady_clock::now();
@@ -205,6 +208,7 @@ int main(int argc, char **argv) {
}*/
}
+
delete mcl;
}
diff --git a/third-party/sylvan b/third-party/sylvan
index a88d88020693b35b272800fe0ded4293a22720e2..035a0aca68ec77dbfe8b48ed8c58c3ebf8a469bb 160000
--- a/third-party/sylvan
+++ b/third-party/sylvan
@@ -1 +1 @@
-Subproject commit a88d88020693b35b272800fe0ded4293a22720e2
+Subproject commit 035a0aca68ec77dbfe8b48ed8c58c3ebf8a469bb