diff --git a/src/MDGraph.cpp b/src/MDGraph.cpp
deleted file mode 100644
index 7236995dbf5f119bf0522e848a40fb57483a77fe..0000000000000000000000000000000000000000
--- a/src/MDGraph.cpp
+++ /dev/null
@@ -1,156 +0,0 @@
-#include "MDGraph.h"
-
-
-bdd * Tab;
-/********* setInitialState *****/
-
-void MDGraph::setInitialState ( Class_Of_State *c )
-{
- currentstate=initialstate=c;
-
-}
-/*----------------------find()----------------*/
-Class_Of_State * MDGraph::find ( Class_Of_State* c )
-{
- for ( MetaGrapheNodes::const_iterator i=GONodes.begin(); ! ( i==GONodes.end() ); i++ )
- //if((c->class_state.id()==(*i)->class_state.id())&&(c->blocage==(*i)->blocage)&&(c->boucle==(*i)->boucle))
- if ( c->class_state.id() == ( *i )->class_state.id() ) {
- return *i;
- }
- return NULL;
-}
-
-
-/*----------------------insert() ------------*/
-void MDGraph::insert ( Class_Of_State *c )
-{
- c->Visited=false;
- this->GONodes.push_back ( c );
- nbStates++;
-}
-
-/*----------------------NbBddNod()------------------------*/
-int MDGraph::NbBddNode ( Class_Of_State * S, size_t& nb )
-{
- if ( S->Visited==false ) {
- //cout<<"insertion du meta etat numero :"<<nb<<"son id est :"<<S->class_state.id()<<endl;
- //cout<<"sa taille est :"<<bdd_nodecount(S->class_state)<<" noeuds \n";
- Tab[nb-1]=S->class_state;
- S->Visited=true;
- int bddnode=bdd_nodecount ( S->class_state );
- int size_succ=0;
- for ( Edges::const_iterator i=S->Successors.begin(); ! ( i==S->Successors.end() ); i++ ) {
- if ( ( *i ).first->Visited==false ) {
- nb++;
- size_succ+=NbBddNode ( ( *i ).first,nb );
- }
- }
- return size_succ+bddnode;
-
- } else {
- return 0;
- }
-}
-
-/*----------------------Visualisation du graphe------------------------*/
-void MDGraph::printCompleteInformation()
-{
-
-
- cout << "\n\nGRAPH SIZE : \n";
- cout<< "\n\tNB MARKING : "<< nbMarking;
- cout<< "\n\tNB NODES : "<< nbStates;
- cout<<"\n\tNB ARCS : " <<nbArcs<<endl;
- cout<<" \n\nCOMPLETE INFORMATION ?(y/n)\n";
- char c;
- cin>>c;
- //InitVisit(initialstate,n);
- Tab=new bdd[ ( int ) nbStates];
- size_t n=1;
- //cout<<"NB BDD NODE : "<<NbBddNode(initialstate,n)<<endl;
- NbBddNode ( initialstate,n );
- cout<<"NB BDD NODE : "<<bdd_anodecount ( Tab, ( int ) nbStates ) <<endl;
- //cout<<"Shared Nodes : "<<bdd_anodecount(Tab,nbStates)<<endl;
- InitVisit ( initialstate,1 );
- //int toto;cin>>toto;
- //bdd Union=UnionMetaState(initialstate,1);
- //cout<<"a titre indicatif taille de l'union : "<<bdd_nodecount(Union)<<endl;
- if ( c=='y'||c=='Y' ) {
- size_t n=1;
- printGraph ( initialstate,n );
- }
-
-
-}
-/*----------------------InitVisit()------------------------*/
-void MDGraph::InitVisit ( Class_Of_State * S,size_t nb )
-{
-
- if ( nb<=nbStates ) {
- S->Visited=false;
- for ( Edges::const_iterator i=S->Successors.begin(); ! ( i==S->Successors.end() ); i++ ) {
-
- if ( ( *i ).first->Visited==true ) {
- nb++;
- InitVisit ( ( *i ).first,nb );
- }
- }
-
- }
-}
-/********* printGraph *****/
-
-void MDGraph::printGraph ( Class_Of_State *s,size_t &nb )
-{
- if ( nb<=nbStates ) {
- cout<<"\nSTATE NUMBER "<<nb<<" : \n";
- s->Visited=true;
- printsuccessors ( s );
- getchar();
- printpredecessors ( s );
- getchar();
- Edges::const_iterator i;
- for ( i=s->Successors.begin(); ! ( i==s->Successors.end() ); i++ ) {
- if ( ( *i ).first->Visited==false ) {
- nb++;
- printGraph ( ( *i ).first, nb );
- }
- }
-
- }
-
-}
-
-
-/*---------void print_successors_class(Class_Of_State *)------------*/
-void MDGraph::printsuccessors ( Class_Of_State *s )
-{
- Edges::const_iterator i;
- cout<<bddtable<<s->class_state<<endl;
- if ( s->boucle ) {
- cout<<"\n\tON BOUCLE DESSUS AVEC EPSILON\n";
- }
- if ( s->blocage ) {
- cout<<"\n\tEXISTENCE D'UN ETAT BLOCANT\n";
- }
- cout<<"\n\tSES SUCCESSEURS SONT ( "<<s->Successors.size() <<" ) :\n\n";
- getchar();
- for ( i =s->Successors.begin(); ! ( i==s->Successors.end() ); i++ ) {
- cout<<" \t- t"<< ( *i ).second<<" ->";
- cout<<bddtable<< ( *i ).first->class_state<<endl;
- getchar();
- }
-}
-/*---------void printpredescessors(Class_Of_State *)------------*/
-void MDGraph::printpredecessors ( Class_Of_State *s )
-{
- Edges::const_iterator i;
- cout<<"\n\tSES PREDESCESSEURS SONT ( "<<s->Predecessors.size() <<" ) :\n\n";
- getchar();
- for ( i =s->Predecessors.begin(); ! ( i==s->Predecessors.end() ); i++ ) {
- cout<<" \t- t"<< ( *i ).second<<" ->";
- cout<<bddtable<< ( *i ).first->class_state<<endl;
- getchar();
- }
-}
-
diff --git a/src/MDGraph.h b/src/MDGraph.h
deleted file mode 100644
index ad8d7c069f94d45a236006b05cc84377287f5abb..0000000000000000000000000000000000000000
--- a/src/MDGraph.h
+++ /dev/null
@@ -1,43 +0,0 @@
-
-
-/****************** Graph.hpp **************************/
-
-#ifndef _MDGRAPH_
-
-#define _MDGRAPH_
-using namespace std;
-#include <iostream>
-/*#include <time>*/
-#include <vector>
-#include "Class_of_state.h"
-#include <list>
-typedef set<int> Set;
-typedef vector<Class_Of_State*> MetaGrapheNodes;
-class MDGraph
-{
- private:
- void printGraph(Class_Of_State *, size_t &);
- MetaGrapheNodes GONodes;
- public:
- void Reset();
- Class_Of_State *initialstate;
- Class_Of_State *currentstate;
- double nbStates;
- double nbMarking;
- double nbArcs;
- Class_Of_State* find(Class_Of_State*);
- Edges& get_successor(Class_Of_State*);
- void printsuccessors(Class_Of_State *);
- int NbBddNode(Class_Of_State*,size_t&);
- void InitVisit(Class_Of_State * S,size_t nb);
- void printpredecessors(Class_Of_State *);
- void addArc(){nbArcs++;}
- void insert(Class_Of_State*);
- MDGraph(){nbStates=nbArcs=nbMarking=0;}
- void setInitialState(Class_Of_State*); //Define the initial state of this graph
- void printCompleteInformation();
-
-
-
-};
-#endif
diff --git a/src/SylvanWrapper.cpp b/src/SylvanWrapper.cpp
index 0e70078a7e9ce0fa865d765e1629818e778a08c9..4bfe6fb68065f57b8f78e205868a7900b51aef3f 100644
--- a/src/SylvanWrapper.cpp
+++ b/src/SylvanWrapper.cpp
@@ -806,8 +806,35 @@ MDD SylvanWrapper::ldd_minus(MDD a, MDD b) {
SylvanCacheWrapper::cache_put(CACHE_LDD_MINUS, a, b, result);
return result;
}
+/*
+ * Check whether transition removing @minus tokens is firable in marking @cmark
+ */
+bool SylvanWrapper::isFirable(MDD cmark, MDD minus) {
+ if (cmark == lddmc_true) return true;
+ bool result {false};
+ MDD _cmark = cmark, _minus = minus;
+ mddnode_t n_cmark = GETNODE(_cmark);
+ mddnode_t n_minus = GETNODE(_minus);
+ while (!result) {
+ uint32_t value;
+ value = mddnode_getvalue(n_cmark);
+ uint32_t value_minus = mddnode_getvalue(n_minus);
+
+ if (value >= value_minus) {
+ mddnode_t node_mark=mddnode_getdown(n_cmark);
+ if (node_mark==lddmc_true) return true;
+ mddnode_t node_minus=mddnode_getdown(n_minus);
+ result=isFirable(node_mark, mddnode_getdown(node_minus));
+ }
+ cmark = mddnode_getright(n_cmark);
+ if (cmark == lddmc_false || result) return result;
+ n_cmark = GETNODE(cmark);
+ }
+
+ return result;
+}
MDD SylvanWrapper::lddmc_firing_mono(MDD cmark, const MDD minus,const 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;
diff --git a/src/SylvanWrapper.h b/src/SylvanWrapper.h
index 58030b764c5223763089741028ff6b6272f10d15..0848011068c00149352ded4d68e57cfe1f4de444 100644
--- a/src/SylvanWrapper.h
+++ b/src/SylvanWrapper.h
@@ -242,6 +242,7 @@ public:
static int isGCRequired();
static void convert_wholemdd_stringcpp(MDD cmark,std::string &res);
static void sylvan_gc_seq();
+ static bool isFirable(MDD cmark, MDD minus);
private:
static int is_custom_bucket(const llmsset2_t dbs, uint64_t index);
static int llmsset_rehash_bucket(const llmsset2_t dbs, uint64_t d_idx);
diff --git a/src/main.cpp b/src/main.cpp
index 91c403152a3f7647a7d7c31a62f495260c27a415..39da26a7b1e73fdd80981ea6292ef289e3b56791 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -78,9 +78,9 @@ void displayCheckResult(bool res) {
else
cout << "Property is violated..." << endl;
}
+
void displayTime(auto startTime,auto finalTime) {
cout << "Verification duration : " << std::chrono::duration_cast < std::chrono::milliseconds> (finalTime - startTime).count() << " milliseconds\n";
-
}
/***********************************************/
int main(int argc, char **argv) {