modifié : src/ModelCheckLace.cpp

	modifié :         src/ModelCheckLace.h
	modifié :         src/sylvan_sog.c

src/ModelCheckLace.cpp

@@ -33,7 +33,7 @@ void ModelCheckLace::preConfigure() {
     print_h(max);
     printf(" max.\n");
     LACE_ME;
-    sylvan_set_limits(max, 28, 1);
+    sylvan_set_limits(max, 16, 2);
     sylvan_init_package();
     sylvan_init_ldd();
     
@@ -134,8 +134,8 @@ TASK_3 (MDD, Aggregate_epsilon_lace, MDD, From, Set*, nonObservable, vector<Tran
     MDD M1;
     MDD M2=From;
     int it=0;
-    lddmc_refs_pushptr(&M1);
-    lddmc_refs_pushptr(&M2);
+    /*lddmc_refs_pushptr(&M1);
+    lddmc_refs_pushptr(&M2);*/
     cout<<"worker "<<lace_get_worker()->worker<<endl;
     
     do
@@ -145,17 +145,20 @@ TASK_3 (MDD, Aggregate_epsilon_lace, MDD, From, Set*, nonObservable, vector<Tran
         {
             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++)
         {
+            lddmc_refs_push(M1);
+            lddmc_refs_push(M2);
             MDD succ=lddmc_refs_sync(SYNC(lddmc_firing_lace));
-            //cout<<"j :"<<j<<endl;
+            lddmc_refs_push(succ);
             M2=lddmc_union(succ,M2);
+            lddmc_refs_pop(3);
         }
 
     }
-    while(M1!=M2);
-    lddmc_refs_popptr(2);
+    while (M1!=M2);
+   /* lddmc_refs_popptr(2);*/
     return M2;
 }
 
@@ -214,7 +217,7 @@ TASK_3 (bool, SetDivL, MDD, M, Set*, nonObservable, vector<TransSylvan>*, tb_rel
 
 LDDState * ModelCheckLace::getInitialMetaState()
 {
-    cout<<__func__<<endl;
+    if (!m_built_initial) {
     LDDState *initalAggregate=new LDDState();
     LDDState *reached_class;
     LACE_ME;
@@ -260,6 +263,8 @@ LDDState * ModelCheckLace::getInitialMetaState()
         initalAggregate->Successors.insert(initalAggregate->Successors.begin(),LDDEdge(reached_class,t));
         reached_class->Predecessors.insert(reached_class->Predecessors.begin(),LDDEdge(initalAggregate,t));
     }
+    m_built_initial=true;
+    }
 
     return m_graph->getInitialState();
 }

src/ModelCheckLace.h

@@ -8,6 +8,7 @@ public:
         void buildSucc(LDDState *agregate) override;
 private:
         void preConfigure();
+        bool m_built_initial=false;
 
 };
 #endif

src/sylvan_sog.c

@@ -19,6 +19,7 @@ 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;
@@ -36,6 +37,65 @@ TASK_IMPL_3(MDD, lddmc_firing_lace, MDD, cmark, MDD, minus, MDD ,plus) {
     mddnode_t n_plus = GETNODE(plus);
     mddnode_t n_minus = GETNODE(minus);    
     
+    
+    //lddmc_refs_pushptr(&result);
+    uint32_t count=0;
+    uint32_t l_values[128];
+    for (;;)
+    {
+        uint32_t value;
+        value = mddnode_getvalue(n_cmark);
+        uint32_t value_minus = mddnode_getvalue(n_minus);
+        uint32_t value_plus = mddnode_getvalue(n_plus);
+        if (value>=value_minus)
+        {     
+            
+            lddmc_refs_spawn(SPAWN(lddmc_firing_lace, mddnode_getdown(n_cmark), mddnode_getdown(n_minus), mddnode_getdown(n_plus)));
+            l_values[count]=value-value_minus+value_plus;
+            count++;            
+                            
+        }
+        cmark = mddnode_getright(n_cmark);
+        if (cmark == lddmc_false) break;
+        n_cmark = GETNODE(cmark);
+    }
+    if (count>10) printf("Count %d\n",count);
+    result= lddmc_false;
+    while (count--) {
+        lddmc_refs_push(result);
+        MDD left=lddmc_refs_sync(SYNC(lddmc_firing_lace));
+        lddmc_refs_push(left);
+        MDD result2 =
+                lddmc_makenode(l_values[count],left, lddmc_false);            
+        lddmc_refs_push(result2);    
+        result = lddmc_union( result, result2);  
+        lddmc_refs_pop(3);
+    }
+    //lddmc_refs_popptr(1);
+    if (cache_put3(CACHE_FIRING_LACE, cmark, minus, plus,result)) sylvan_stats_count(CACHE_FIRING_LACE);
+    return result;
+}
+
+
+
+
+/*TASK_IMPL_3(MDD, lddmc_firing_lace, MDD, cmark, MDD, minus, MDD ,plus) {
+  
+    if (cmark == lddmc_true) return lddmc_true;
+    if (minus == lddmc_false) return lddmc_false;
+    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);    
+    
     result= lddmc_false;
     //lddmc_refs_pushptr(&result);
     for (;;)
@@ -63,3 +123,4 @@ TASK_IMPL_3(MDD, lddmc_firing_lace, MDD, cmark, MDD, minus, MDD ,plus) {
     if (cache_put3(CACHE_FIRING_LACE, cmark, minus, plus,result)) sylvan_stats_count(CACHE_FIRING_LACE);
     return result;
 }
+*/