diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp
index c0267d9a73b761a7c8aa9fd530a3034d1d62fac5..4cf3002afddc8121eefd65113af25ca70840601c 100644
--- a/src/CommonSOG.cpp
+++ b/src/CommonSOG.cpp
@@ -274,10 +274,18 @@ void CommonSOG::AddConflict(const MDD &S, const int &transition, Set &le) {
} else {
for (auto i = 0; i < m_transitions.size(); i++) {
if (i != transition) {
- auto &preT1 = m_transitions[i].post;
+ auto &postT1 = m_transitions[i].post;
auto &preT2 = m_transitions[transition].pre;
- if (!haveCommonPre(preT1, preT2)) ample.insert(i);
+ if (!haveCommonPre(postT1, preT2)) ample.insert(i);
}
}
}
}
+
+Set CommonSOG::computeAmple(const MDD &s) {
+ Set ample;
+ for (auto &t : ample) {
+ AddConflict(s,t,ample);
+ }
+ return ample;
+}
diff --git a/src/CommonSOG.h b/src/CommonSOG.h
index 39fee9d0e246f834de07a1afce043144c2df88ad..05160f8d1ba2a4f47254eee14c7dc740c35cd96a 100644
--- a/src/CommonSOG.h
+++ b/src/CommonSOG.h
@@ -1,5 +1,6 @@
#ifndef COMMONSOG_H
#define COMMONSOG_H
+
#include "LDDState.h"
#include "LDDGraph.h"
@@ -11,6 +12,7 @@
// #define GCENABLE 0
class LDDState;
+
typedef pair<LDDState *, MDD> couple;
typedef pair<couple, Set> Pair;
typedef stack<Pair> pile;
@@ -18,54 +20,75 @@ typedef stack<Pair> pile;
class LDDGraph;
-class CommonSOG
-{
- public:
- CommonSOG();
- virtual ~CommonSOG();
- static LDDGraph *getGraph();
- inline set<uint16_t> & getPlaceProposition() {return m_place_proposition;}
- inline string_view getTransition(int pos) {
- {
- return string_view {m_transitions.at(pos).name};
- }
+class CommonSOG {
+public:
+ CommonSOG();
+
+ virtual ~CommonSOG();
+
+ static LDDGraph *getGraph();
+
+ inline set<uint16_t> &getPlaceProposition() { return m_place_proposition; }
+
+ inline string_view getTransition(int pos) {
+ {
+ return string_view{m_transitions.at(pos).name};
}
- static string_view getPlace(int pos);
- void finish() {m_finish=true;}
- virtual void computeDSOG(LDDGraph &g) { };
- protected:
- void initializeLDD();
- void loadNetFromFile();
- const NewNet* m_net;
- int m_nbPlaces = 0;
- static LDDGraph *m_graph;
- vector<TransSylvan> m_tb_relation;
- MDD m_initialMarking;
- map<string, uint16_t> * m_transitionName;
- map<uint16_t,string> * m_placeName;
- Set m_observable;
- Set m_nonObservable;
- Set InterfaceTrans;
- set<uint16_t> m_place_proposition;
- vector<class Transition> m_transitions;
- MDD Accessible_epsilon(MDD From);
- Set firable_obs(MDD State);
- MDD get_successor(const MDD& From,const int& t);
- MDD ImageForward(MDD From);
- MDD Canonize(MDD s, unsigned int level);
- bool Set_Div(MDD &M) const;
- bool Set_Bloc(MDD &M) const;
- uint8_t m_nb_thread;
- std::mutex m_graph_mutex,m_gc_mutex;
- atomic<uint8_t> m_gc;
- volatile bool m_finish=false;
- // Functions for POR
- /*
- * Determine ample set in S for transition
- */
- void AddConflict(const MDD& S,const int &transition,Set& ample);
- private:
+ }
+
+ static string_view getPlace(int pos);
+
+ void finish() { m_finish = true; }
+
+ virtual void computeDSOG(LDDGraph &g) {};
+protected:
+ void initializeLDD();
+
+ void loadNetFromFile();
+
+ const NewNet *m_net;
+ int m_nbPlaces = 0;
+ static LDDGraph *m_graph;
+ vector<TransSylvan> m_tb_relation;
+ MDD m_initialMarking;
+ map<string, uint16_t> *m_transitionName;
+ map<uint16_t, string> *m_placeName;
+ Set m_observable;
+ Set m_nonObservable;
+ Set InterfaceTrans;
+ set<uint16_t> m_place_proposition;
+ vector<class Transition> m_transitions;
+
+ MDD Accessible_epsilon(MDD From);
+
+ Set firable_obs(MDD State);
+
+ MDD get_successor(const MDD &From, const int &t);
+
+ MDD ImageForward(MDD From);
+
+ MDD Canonize(MDD s, unsigned int level);
+
+ bool Set_Div(MDD &M) const;
+
+ bool Set_Bloc(MDD &M) const;
+
+ uint8_t m_nb_thread;
+ std::mutex m_graph_mutex, m_gc_mutex;
+ atomic<uint8_t> m_gc;
+ volatile bool m_finish = false;
+
+
+private:
+ /*
+ * Compute ample set @ample for state @s
+ */
+ Set computeAmple(const MDD &s);
+ /*
+ * Determine ample set in S for transition
+ */
+ void AddConflict(const MDD &S, const int &transition, Set &le);
};
#endif // COMMONSOG_H
diff --git a/src/MCMultiCore/ModelCheckThReq.cpp b/src/MCMultiCore/ModelCheckThReq.cpp
index a1203b945cc99a3c8679d568890576d3357fda38..5de886be3946c87093a48620579a9fd4e8ba9bd4 100644
--- a/src/MCMultiCore/ModelCheckThReq.cpp
+++ b/src/MCMultiCore/ModelCheckThReq.cpp
@@ -159,8 +159,6 @@ void *ModelCheckThReq::Compute_successors() {
}
} while (!m_finish);
-
-
}
diff --git a/src/sylvan_sog.c b/src/sylvan_sog.c
deleted file mode 100644
index 66feb488753d9642486257f0bca792d3f996fafb..0000000000000000000000000000000000000000
--- a/src/sylvan_sog.c
+++ /dev/null
@@ -1,135 +0,0 @@
-
-#include <sylvan.h>
-#include <sylvan_int.h>
-#include <sylvan_sog.h>
-
-/*******************************************MDD node structur*********************************/
-/*typedef struct __attribute__((packed)) mddnode
-{
- uint64_t a, b;
-} * mddnode_t; // 16 bytes*/
-
-// RmRR RRRR RRRR VVVV | VVVV DcDD DDDD DDDD (little endian - in memory)
-// VVVV RRRR RRRR RRRm | DDDD DDDD DDDc VVVV (big endian)
-
-// Ensure our mddnode is 16 bytes
-typedef char __lddmc_check_mddnode_t_is_16_bytes[ ( sizeof ( struct mddnode ) ==16 ) ? 1 : -1];
-
-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 ( 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 );
-
-
- //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 );
- }
-
- 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;
- }
-
-
-MDD ldd_firing_fast ( MDD cmark, MDD minus, MDD plus ) {
- // for an empty set of source states, or an empty transition relation, return the empty set
- if ( cmark == lddmc_true ) return lddmc_true;
- if ( minus == lddmc_false || plus == lddmc_false ) return lddmc_false;
-
- MDD result;
- MDD _cmark=cmark, _minus=minus, _plus=plus;
-
-
- mddnode_t n_cmark = GETNODE ( _cmark );
- mddnode_t n_plus = GETNODE ( _plus );
- mddnode_t n_minus = GETNODE ( _minus );
-
-
- result = lddmc_false;
- uint16_t depth=0;
- uint16_t new_ldd[256];
-
- for ( ; _cmark!=lddmc_false; ) {
- uint32_t value;
- value = mddnode_getvalue ( n_cmark );
- uint32_t value_minus = mddnode_getvalue ( n_minus );
- uint32_t value_plus = mddnode_getvalue ( n_plus );
- uint8_t res=1;
- while ( _cmark!=lddmc_false && _cmark!=lddmc_true && res ) {
- if ( value>=value_minus ) {
- //new_ldd=value-value_minus+value_plus;
- //push ( mddnode_getdown ( n_cmark ), mddnode_getdown ( n_minus ), mddnode_getdown ( n_plus ) );
- MDD result2 =
- ldd_makenode ( value-value_minus+value_plus,lddmc_firing_mono ( mddnode_getdown ( n_cmark ), mddnode_getdown ( n_minus ), mddnode_getdown ( n_plus ) ), lddmc_false );
-
-
- if ( result2!=lddmc_false ) result = lddmc_union_mono ( result, result2 );
- }
- else res=0;
- }
- if (res) {/* Build LDD and Union*/}
- cmark = mddnode_getright ( n_cmark );
- if ( cmark == lddmc_false ) break;
- n_cmark = GETNODE ( cmark );
- }
- //cache_put3(CACHE_LDD_FIRE, cmark, minus, plus, result);
-
- return result;
- }
-
-void displayMDDTableInfo()
-{
- printf("%zu of %zu buckets filled!\n", seq_llmsset_count_marked(nodes), llmsset_get_size(nodes));
-}
-int isGCRequired()
-{
- return (g_created>llmsset_get_size(nodes)/2);
-}
-uint32_t getCountMDD() {
- return g_created;
-}
-
diff --git a/src/sylvan_sog.h b/src/sylvan_sog.h
deleted file mode 100644
index c5e15ae245eb3e35d74f8baf5282d547998eddbc..0000000000000000000000000000000000000000
--- a/src/sylvan_sog.h
+++ /dev/null
@@ -1,25 +0,0 @@
-#ifndef SYLVAN_SOG_H_INCLUDED
-#define SYLVAN_SOG_H_INCLUDED
-
-#ifdef __cplusplus
-extern "C" {
-#endif /* __cplusplus */
-
-
-
-
-TASK_DECL_3(MDD, lddmc_firing_lace, MDD, MDD, MDD)
-#define lddmc_firing_lace(cmark, minus, plus) CALL(lddmc_firing_lace, cmark, minus, plus)
-
-
-void displayMDDTableInfo();
-int isGCRequired();
-uint32_t getCountMDD();
-
-#ifdef __cplusplus
-}
-#endif /* __cplusplus */
-
-
-
-#endif // SYLVAN_SOG_H_INCLUDED