Skip to content
Snippets Groups Projects
Commit 18147bfd authored by Chiheb Amer Abid's avatar Chiheb Amer Abid
Browse files

Remove unused files

parent 0fa51bde
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/CommonSOG.cpp
+ 10
− 2
View file @ 18147bfd
......@@ -274,10 +274,18 @@ void CommonSOG::AddConflict(const MDD &S, const int &transition, Set &ample) {
} 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;
}
src/CommonSOG.h
+ 69
− 46
View file @ 18147bfd
#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 &ample);
};
#endif // COMMONSOG_H
src/MCMultiCore/ModelCheckThReq.cpp
+ 0
− 2
View file @ 18147bfd
......@@ -159,8 +159,6 @@ void *ModelCheckThReq::Compute_successors() {
}
} while (!m_finish);
}
......
src/sylvan_sog.c deleted 100644 → 0
+ 0
− 135
View file @ 0fa51bde
#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;
}
src/sylvan_sog.h deleted 100644 → 0
+ 0
− 25
View file @ 0fa51bde
#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
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment