diff --git a/src/ModelCheckLace.cpp b/src/ModelCheckLace.cpp
index 9c8cbabd9f80668d2d97ac6ba93e56181409d02f..daaca60f573a731b76fa1655b288e3aa1c3b51b1 100644
--- a/src/ModelCheckLace.cpp
+++ b/src/ModelCheckLace.cpp
@@ -9,22 +9,39 @@ using namespace sylvan;
ModelCheckLace::ModelCheckLace(const NewNet &R, int BOUND,int nbThread):ModelCheckBaseMT(R,BOUND,nbThread)
{
}
-void ModelCheckLace::preConfigure() {
- cout<<__func__<<endl;
+void
+print_h(double size)
+{
+ const char* units[] = {"B", "KB", "MB", "GB", "TB", "PB", "EB", "ZB", "YB"};
+ int i = 0;
+ for (;size>1024;size/=1024) i++;
+ printf("%.*f %s", i, size, units[i]);
+}
+size_t
+getMaxMemory()
+{
+ long pages = sysconf(_SC_PHYS_PAGES);
+ long page_size = sysconf(_SC_PAGE_SIZE);
+ return pages * page_size;
+}
+void ModelCheckLace::preConfigure() {
lace_init(m_nb_thread, 10000000);
lace_startup(0, NULL, NULL);
- sylvan_set_limits(2LL<<30, 16, 3);
+ size_t max = 16LL<<30;
+ if (max > getMaxMemory()) max = getMaxMemory()/10*9;
+ printf("Memory : ");
+ print_h(max);
+ printf(" max.\n");
+ LACE_ME;
+ sylvan_set_limits(max, 28, 1);
sylvan_init_package();
sylvan_init_ldd();
- LACE_ME;
+ //init_gc_seq();
+ sylvan_gc_enable();
+ printf("%zu of %zu buckets filled!\n", llmsset_count_marked(nodes), llmsset_get_size(nodes));
int i;
vector<Place>::const_iterator it_places;
-
-
- init_gc_seq();
-
-
//_______________
transitions=m_net.transitions;
m_observable=m_net.Observable;
@@ -59,7 +76,8 @@ void ModelCheckLace::preConfigure() {
}
m_initialMarking=lddmc_cube(liste_marques,m_net.places.size());
-
+ delete []liste_marques;
+ lddmc_refs_push(m_initialMarking);
@@ -99,9 +117,9 @@ void ModelCheckLace::preConfigure() {
}
MDD _minus=lddmc_cube(prec,m_nbPlaces);
- ldd_refs_push(_minus);
+ lddmc_refs_push(_minus);
MDD _plus=lddmc_cube(postc,m_nbPlaces);
- ldd_refs_push(_plus);
+ lddmc_refs_push(_plus);
m_tb_relation.push_back(TransSylvan(_minus,_plus));
}
delete [] prec;
@@ -116,22 +134,28 @@ TASK_3 (MDD, Aggregate_epsilon_lace, MDD, From, Set*, nonObservable, vector<Tran
MDD M1;
MDD M2=From;
int it=0;
- //cout<<"worker "<<lace_get_worker()->worker<<endl;
+ lddmc_refs_pushptr(&M1);
+ lddmc_refs_pushptr(&M2);
+ cout<<"worker "<<lace_get_worker()->worker<<endl;
+
do
{
M1=M2;
for(Set::const_iterator i=nonObservable->begin(); !(i==nonObservable->end()); i++)
{
- SPAWN(lddmc_firing_lace,M2,(*tb_relation)[(*i)].getMinus(),(*tb_relation)[(*i)].getPlus());
+ lddmc_refs_spawn(SPAWN(lddmc_firing_lace,M2,(*tb_relation)[(*i)].getMinus(),(*tb_relation)[(*i)].getPlus()));
}
+ // j=0;
for(Set::const_iterator i=nonObservable->begin(); !(i==nonObservable->end()); i++)
{
- MDD succ=SYNC(lddmc_firing_lace);
+ MDD succ=lddmc_refs_sync(SYNC(lddmc_firing_lace));
+ //cout<<"j :"<<j<<endl;
M2=lddmc_union(succ,M2);
}
}
while(M1!=M2);
+ lddmc_refs_popptr(2);
return M2;
}
@@ -190,11 +214,13 @@ TASK_3 (bool, SetDivL, MDD, M, Set*, nonObservable, vector<TransSylvan>*, tb_rel
LDDState * ModelCheckLace::getInitialMetaState()
{
-
+ cout<<__func__<<endl;
LDDState *initalAggregate=new LDDState();
LDDState *reached_class;
LACE_ME;
MDD initial_meta_state(CALL(Aggregate_epsilon_lace,m_initialMarking,&m_nonObservable,&m_tb_relation));
+ cout<<"Yep..."<<endl;
+ lddmc_refs_push(initial_meta_state);
Set fire=fire_obs_lace(initial_meta_state,&m_observable,&m_tb_relation);
// c->m_lddstate=CALL(lddmc_canonize,initial_meta_state,0,*this);
@@ -208,8 +234,10 @@ LDDState * ModelCheckLace::getInitialMetaState()
// Compute successors
unsigned int onb_it=0;
Set::iterator iter=fire.begin();
+ int j=0;
while(iter!=fire.end())
{
+
int t = *iter;
SPAWN(Aggregate_epsilon_lace,get_successor(initial_meta_state,t),&m_nonObservable,&m_tb_relation);
onb_it++;
@@ -225,6 +253,7 @@ LDDState * ModelCheckLace::getInitialMetaState()
Complete_meta_state=SYNC(Aggregate_epsilon_lace);
reached_class=new LDDState();
reached_class->m_lddstate=Complete_meta_state;
+ lddmc_refs_push(Complete_meta_state);
reached_class->setDiv(SetDivL(Complete_meta_state,&m_nonObservable,&m_tb_relation));
m_graph->addArc();
m_graph->insert(reached_class);
@@ -237,12 +266,15 @@ LDDState * ModelCheckLace::getInitialMetaState()
void ModelCheckLace::buildSucc(LDDState *agregate)
{
-
+ cout<<__func__<<endl;
if (!agregate->isVisited()) {
// It's first time to visit agregate, then we have to build its successors
- agregate->setVisited();
+ agregate->setVisited();
LDDState *reached_class=nullptr;
LACE_ME;
+ displayMDDTableInfo();
+ sylvan_gc();
+ displayMDDTableInfo();
MDD meta_state=agregate->getLDDValue();//(CALL(Aggregate_epsilon_lace,agregate->getLDDValue(),&m_nonObservable,&m_tb_relation));
Set fire=fire_obs_lace(meta_state,&m_observable,&m_tb_relation);
@@ -268,6 +300,7 @@ void ModelCheckLace::buildSucc(LDDState *agregate)
if(!pos)
{
+ lddmc_refs_push(Complete_meta_state);
reached_class->setDiv(SetDivL(Complete_meta_state,&m_nonObservable,&m_tb_relation));
reached_class->setDeadLock(Set_Bloc(Complete_meta_state));
m_graph->addArc();
diff --git a/src/ModelCheckerTh.cpp b/src/ModelCheckerTh.cpp
index 698815dbe32bc89d3a350305ff3b2094848bcbeb..9a4af0322b55ab5c52e230d402d9986918ad6d8d 100644
--- a/src/ModelCheckerTh.cpp
+++ b/src/ModelCheckerTh.cpp
@@ -201,6 +201,7 @@ void * ModelCheckerTh::Compute_successors()
// #ifdef DEBUG_GC
// displayMDDTableInfo();
// #endif // DEBUG_GC
+
sylvan_gc_seq();
// #ifdef DEBUG_GC
// displayMDDTableInfo();
diff --git a/src/sylvan_sog.c b/src/sylvan_sog.c
index 77edc0602a8e4069f022fc1a676128d409f5c64a..828511871f6e3bda22e3f26c1d695201ce6aa88d 100644
--- a/src/sylvan_sog.c
+++ b/src/sylvan_sog.c
@@ -15,73 +15,29 @@
// Ensure our mddnode is 16 bytes
typedef char __lddmc_check_mddnode_t_is_16_bytes[(sizeof(struct mddnode)==16) ? 1 : -1];
-/*static inline uint32_t __attribute__((unused))
-mddnode_getvalue(mddnode_t n)
-{
- return *(uint32_t*)((uint8_t*)n+6);
-}*/
-
-/*static inline uint8_t __attribute__((unused))
-mddnode_getmark(mddnode_t n)
-{
- return n->a & 1;
-}*/
-
-/*static inline uint8_t __attribute__((unused))
-mddnode_getcopy(mddnode_t n)
-{
- return n->b & 0x10000 ? 1 : 0;
-}*/
-
-/*static inline uint64_t __attribute__((unused))
-mddnode_getright(mddnode_t n)
-{
- return (n->a & 0x0000ffffffffffff) >> 1;
-}
-
-static inline uint64_t __attribute__((unused))
-mddnode_getdown(mddnode_t n)
-{
- return n->b >> 17;
-}*/
+static const uint64_t CACHE_FIRING_LACE = (57LL<<40);
#define GETNODE(mdd) ((mddnode_t)llmsset_index_to_ptr(nodes, mdd))
TASK_IMPL_3(MDD, lddmc_firing_lace, MDD, cmark, MDD, minus, MDD ,plus) {
-
- if (cmark == lddmc_true) return lddmc_true;
+
+ if (cmark == lddmc_true) return lddmc_true;
if (minus == lddmc_false) return lddmc_false;
- if (plus == lddmc_false) return lddmc_false; // we assume that if meta is finished, then the rest is not in rel
-
-
- /* Access cache */
- MDD result;
- MDD _cmark=cmark, _minus=minus, _plus=plus;
- /*if (cache_get3(CACHE_LDD_FIRING, cmark, minus, plus, &result)) {
- sylvan_stats_count(LDD_FIRING_CACHED);
+ if (plus == lddmc_false) return lddmc_false;
+
+ MDD result;
+ if (cache_get3(CACHE_FIRING_LACE, cmark, minus, plus, &result)) {
+ printf("cached\n");
+ sylvan_stats_count(CACHE_FIRING_LACE);
return result;
- }*/
-
- mddnode_t n_cmark = GETNODE(_cmark);
- mddnode_t n_plus = GETNODE(_plus);
- mddnode_t n_minus = GETNODE(_minus);
- // meta: -1 (end; rest not in rel), 0 (not in rel), 1 (read), 2 (write), 3 (only-read), 4 (only-write)
-
- /* Recursive operations */
-
- // write, only-write
-// if (m_val == 4) {
-// // only-write, so we need to include 'for all variables'
-// // the reason is that we did not have a read phase, so we need to 'insert' a read phase here
-//
-// }
-
- // if we're here and we are only-write, then we read the current value
-
- // spawn for every value to write (rel)
-
- result = lddmc_false;
+ }
+ mddnode_t n_cmark = GETNODE(cmark);
+ mddnode_t n_plus = GETNODE(plus);
+ mddnode_t n_minus = GETNODE(minus);
+
+ result= lddmc_false;
+ //lddmc_refs_pushptr(&result);
for (;;)
{
uint32_t value;
@@ -90,15 +46,20 @@ TASK_IMPL_3(MDD, lddmc_firing_lace, MDD, cmark, MDD, minus, MDD ,plus) {
uint32_t value_plus = mddnode_getvalue(n_plus);
if (value>=value_minus)
{
+ lddmc_refs_push(result);
+ MDD left=CALL(lddmc_firing_lace, mddnode_getdown(n_cmark), mddnode_getdown(n_minus), mddnode_getdown(n_plus));
+ lddmc_refs_push(left);
MDD result2 =
- lddmc_makenode(value-value_minus+value_plus,CALL(lddmc_firing_lace, mddnode_getdown(n_cmark), mddnode_getdown(n_minus), mddnode_getdown(n_plus)), lddmc_false);
-
-
- if (result2!=lddmc_false) result = lddmc_union( result, result2);
+ lddmc_makenode(value-value_minus+value_plus,left, lddmc_false);
+ lddmc_refs_push(result2);
+ result = lddmc_union( result, result2);
+ lddmc_refs_pop(3);
}
cmark = mddnode_getright(n_cmark);
if (cmark == lddmc_false) break;
n_cmark = GETNODE(cmark);
}
+ //lddmc_refs_popptr(1);
+ if (cache_put3(CACHE_FIRING_LACE, cmark, minus, plus,result)) sylvan_stats_count(CACHE_FIRING_LACE);
return result;
}