From 70bc6526a169e3decf78d17aff8fa889f3f60c51 Mon Sep 17 00:00:00 2001
From: ouni <ouni@lipn.univ-paris13.fr>
Date: Fri, 12 Apr 2019 14:08:44 +0200
Subject: [PATCH] src
---
libraries/parser | 2 +-
src/CMakeLists.txt | 16 ++++++++++-
src/Class_of_state.h | 2 +-
src/DistributedSOG.cpp | 8 +++---
src/DistributedSOG.h | 2 +-
src/LDDGraph.cpp | 30 +++++++++++++++++++--
src/LDDGraph.h | 8 ++++--
src/LDDState.cpp | 4 +++
src/LDDState.h | 1 +
src/ModelChecker.cpp | 11 ++++++++
src/ModelChecker.h | 16 +++++++++++
src/SogTwa.cpp | 60 +++++++++++++++++++++++++++++++++++++++++
src/SogTwa.h | 21 +++++++++++++++
src/SpotSogIterator.cpp | 52 +++++++++++++++++++++++++++++++++++
src/SpotSogIterator.h | 31 +++++++++++++++++++++
src/SpotSogState.cpp | 9 +++++++
src/SpotSogState.h | 39 +++++++++++++++++++++++++++
src/main.cpp | 18 ++++++++++++-
src/threadSOG.cpp | 12 ++++++---
src/threadSOG.h | 3 ++-
20 files changed, 327 insertions(+), 18 deletions(-)
create mode 100644 src/ModelChecker.cpp
create mode 100644 src/ModelChecker.h
create mode 100644 src/SogTwa.cpp
create mode 100644 src/SogTwa.h
create mode 100644 src/SpotSogIterator.cpp
create mode 100644 src/SpotSogIterator.h
create mode 100644 src/SpotSogState.cpp
create mode 100644 src/SpotSogState.h
diff --git a/libraries/parser b/libraries/parser
index a56f328..7034bd4 160000
--- a/libraries/parser
+++ b/libraries/parser
@@ -1 +1 @@
-Subproject commit a56f328d4bc2dc4b088574278d053aeb749fa9ab
+Subproject commit 7034bd4843a46d746e1ff326a8e9f813fe9f2355
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index dcc56ac..84f9f4e 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -18,7 +18,11 @@ set_target_properties(spot PROPERTIES
INTERFACE_INCLUDE_DIRECTORIES "/usr/include/spot/"
)
-
+add_library(bddx SHARED IMPORTED) # or STATIC instead of SHARED
+set_target_properties(bddx PROPERTIES
+ IMPORTED_LOCATION "/usr/lib/x86_64-linux-gnu/libbddx.so"
+ INTERFACE_INCLUDE_DIRECTORIES "/usr/include/spot/"
+)
@@ -33,12 +37,22 @@ add_executable(hybrid-sog main.cpp
threadSOG.cpp
threadSOG.h
LDDGraph.cpp
+ LDDGraph.h
LDDState.cpp
+ LDDState.h
TransSylvan.cpp
sylvan_sog.c
+ SpotSogState.cpp
+ SpotSogState.h
+ SpotSogIterator.cpp
+ SpotSogIterator.h
+ SogTwa.cpp
+ SogTwa.h
+
)
target_link_libraries(hybrid-sog
+ bddx
spot
sylvan
RdP
diff --git a/src/Class_of_state.h b/src/Class_of_state.h
index 38b11a1..5c45ea7 100644
--- a/src/Class_of_state.h
+++ b/src/Class_of_state.h
@@ -1,7 +1,7 @@
#ifndef CLASS_OF_STATE
#define CLASS_OF_STATE
using namespace std;
-#include "bddx.h"
+#include "bdd.h"
//#include <map.h>
#include<unordered_map>
#include <set>
diff --git a/src/DistributedSOG.cpp b/src/DistributedSOG.cpp
index 73832c1..8c8ba94 100644
--- a/src/DistributedSOG.cpp
+++ b/src/DistributedSOG.cpp
@@ -129,7 +129,7 @@ void *DistributedSOG::doCompute()
Pair S;
// pile m_st;
- unsigned char msg[LENGTH_ID];
+ char msg[LENGTH_ID];
int v_nbmetastate=0;
int term=0;
@@ -150,7 +150,7 @@ void *DistributedSOG::doCompute()
c->m_lddstate=Complete_meta_state;
- // lddmc_getsha(Complete_meta_state, msg);
+ lddmc_getsha(Complete_meta_state, msg);
cout <<"nb task "<<n_tasks<<endl;
int destination=(int)abs((msg[0])%n_tasks);
@@ -207,7 +207,7 @@ void *DistributedSOG::doCompute()
MDD marking=get_successorMDD(e.first.second,t);
MDD lddmarq=Accessible_epsilon(marking);
reached_class->m_lddstate=lddmarq;
-// lddmc_getsha(lddmarq, msg);
+ lddmc_getsha(lddmarq, msg);
int destination=(int)abs((msg[0])%n_tasks);
@@ -639,7 +639,7 @@ char * DistributedSOG::concat_string(const char *s1,int longueur1,const char *s2
}
-void DistributedSOG::strcpySHA(unsigned char *dest,const unsigned char *source)
+void DistributedSOG::strcpySHA(char *dest,const char *source)
{
for (int i=0; i<LENGTH_ID; i++)
{
diff --git a/src/DistributedSOG.h b/src/DistributedSOG.h
index ed84562..41cd1c6 100644
--- a/src/DistributedSOG.h
+++ b/src/DistributedSOG.h
@@ -69,7 +69,7 @@ class DistributedSOG {
int minCharge();
bool isNotTerminated();
int Terminate();
- void strcpySHA(unsigned char *dest, const unsigned char *source);
+ void strcpySHA(char *dest, const char *source);
char *concat_string(const char *s1, int longueur1, const char *s2,
int longueur2, char *dest);
void sha256(LDDState *state, char output[65]);
diff --git a/src/LDDGraph.cpp b/src/LDDGraph.cpp
index 8a7bc24..426e2b7 100644
--- a/src/LDDGraph.cpp
+++ b/src/LDDGraph.cpp
@@ -2,7 +2,7 @@
#include <sylvan.h>
#include <stdio.h>
#include <string.h>
-
+#include <map>
LDDGraph::~LDDGraph()
{
//dtor
@@ -14,6 +14,10 @@ void LDDGraph::setInitialState(LDDState *c)
m_currentstate=m_initialstate=c;
}
+
+LDDState* LDDGraph::getInitialState() const {
+ return m_GONodes.at(0);
+}
/*----------------------find()----------------*/
LDDState * LDDGraph::find(LDDState* c)
{
@@ -104,7 +108,7 @@ void LDDGraph::printCompleteInformation()
char c;
cin>>c;
//InitVisit(initialstate,n);
- m_tab=new MDD[(int)m_nbStates];
+
size_t n=1;
//cout<<"NB BDD NODE : "<<NbBddNode(initialstate,n)<<endl;
NbBddNode(m_initialstate,n);
@@ -202,3 +206,25 @@ void LDDGraph::printpredecessors(LDDState *s)
}*/
cout<<"Not implemented yet!"<<endl;
}
+/*** Giving a position in m_GONodes Returns an LDDState ****/
+LDDState *LDDGraph::getLDDStateById(unsigned int id) {
+ return m_GONodes.at(id);
+}
+
+string LDDGraph::getTransition(int pos) {
+ map<string,int>::iterator it=m_transition->begin();
+ while(it != m_transition->end())
+ {
+ if(it->second == pos)
+ return it->first;
+ it++;
+ }
+ return "";
+}
+
+void LDDGraph::setTransition(map<string,int>& list_transitions) {
+ m_transition=&list_transitions;
+}
+
+//void LDDGraph::setTransition(vector<string> list)
+
diff --git a/src/LDDGraph.h b/src/LDDGraph.h
index 4399850..3c1b356 100755
--- a/src/LDDGraph.h
+++ b/src/LDDGraph.h
@@ -4,18 +4,21 @@
//#include "LDDStateExtend.h"
using namespace std;
#include <iostream>
-
+#include <map>
typedef set<int> Set;
typedef vector<LDDState*> MetaLDDNodes;
class LDDGraph
{
private:
- MDD * m_tab;
+ map<string,int>* m_transition;
void printGraph(LDDState *, size_t &);
public:
+ string getTransition(int pos);
+ void setTransition(map<string,int>& list_transitions);
MetaLDDNodes m_GONodes;
+ LDDState *getLDDStateById(unsigned int id);
void Reset();
LDDState *m_initialstate;
LDDState *m_currentstate;
@@ -35,6 +38,7 @@ class LDDGraph
void insert(LDDState*);
LDDGraph() {m_nbStates=m_nbArcs=m_nbMarking=0;}
void setInitialState(LDDState*); //Define the initial state of this graph
+ LDDState* getInitialState() const;
void printCompleteInformation();
virtual ~LDDGraph();
};
diff --git a/src/LDDState.cpp b/src/LDDState.cpp
index 616246c..a6f372b 100644
--- a/src/LDDState.cpp
+++ b/src/LDDState.cpp
@@ -24,3 +24,7 @@ bool LDDState::isVirtual() {
void LDDState::setVirtual() {
m_virtual=true;
}
+
+vector<pair<LDDState*, int>>* LDDState::getSuccessors() {
+ return &Successors;
+}
diff --git a/src/LDDState.h b/src/LDDState.h
index 17b3420..5829008 100755
--- a/src/LDDState.h
+++ b/src/LDDState.h
@@ -16,6 +16,7 @@ class LDDState {
virtual ~LDDState();
Set firable;
void* Class_Appartenance;
+ vector<pair<LDDState*, int>>* getSuccessors();
vector<pair<LDDState*, int> > Predecessors, Successors;
pair<LDDState*, int> LastEdge;
void setLDDValue(MDD m);
diff --git a/src/ModelChecker.cpp b/src/ModelChecker.cpp
new file mode 100644
index 0000000..9fca2b5
--- /dev/null
+++ b/src/ModelChecker.cpp
@@ -0,0 +1,11 @@
+#include "ModelChecker.h"
+
+ModelChecker::ModelChecker()
+{
+ //ctor
+}
+
+ModelChecker::~ModelChecker()
+{
+ //dtor
+}
diff --git a/src/ModelChecker.h b/src/ModelChecker.h
new file mode 100644
index 0000000..93a6aa4
--- /dev/null
+++ b/src/ModelChecker.h
@@ -0,0 +1,16 @@
+#ifndef MODELCHECKER_H
+#define MODELCHECKER_H
+
+
+class ModelChecker
+{
+ public:
+ ModelChecker();
+ virtual ~ModelChecker();
+
+ protected:
+
+ private:
+};
+
+#endif // MODELCHECKER_H
diff --git a/src/SogTwa.cpp b/src/SogTwa.cpp
new file mode 100644
index 0000000..7927e15
--- /dev/null
+++ b/src/SogTwa.cpp
@@ -0,0 +1,60 @@
+#include <spot/twaalgos/dot.hh>
+#include <spot/twaalgos/hoa.hh>
+#include <spot/twa/twa.hh>
+#include <spot/twa/bdddict.hh>
+
+
+#include "SpotSogIterator.h"
+#include "SpotSogState.h"
+
+#include "SogTwa.h"
+#include <map>
+using namespace spot;
+SogTwa::SogTwa(const bdd_dict_ptr &dict_ptr,LDDGraph *sog): twa(dict_ptr),m_sog(sog)
+{
+ SpotSogIterator::m_graph=sog;
+/*spot::bdd_dict *p=dict_ptr.get();
+cout<<"Taille du dictionnaire :"<<p->var_map.size()<<endl;
+
+map<spot::formula,int>::iterator i=(p->var_map).begin();
+
+while (i!=(p->var_map).end()) {
+ cout<<" test :"<<(*i).first.ap_name()<<endl;
+std::ostringstream stream;
+ stream << (*i).first;
+ std::string str = stream.str();
+ cout<<" formule 1: "<<str<<endl;
+ cout<<" formule 2: "<<str<<endl;
+ i++;
+}*/
+//spot::bdd_format_formula(dict_ptr,"test");
+//map<bdd,spot::ltl::formula>.iterator it=p->vf_map.begin();
+
+}
+state* SogTwa::get_init_state() const {
+ //cout<<"Initial state given...\n";
+ return new SpotSogState(m_sog->getInitialState());//new SpotSogState();
+
+}
+// Allows to print state label representing its id
+std::string SogTwa::format_state(const spot::state* s) const
+ {
+ auto ss = static_cast<const SpotSogState*>(s);
+ std::ostringstream out;
+ out << "( " << ss->getLDDState()->getLDDValue() << ")";
+ return out.str();
+ }
+
+SpotSogIterator* SogTwa::succ_iter(const spot::state* s) const {
+
+ auto ss = static_cast<const SpotSogState*>(s);
+ bdd b=bddfalse;
+ return new SpotSogIterator(ss->getLDDState());//,b);//s state_condition(ss));
+}
+
+
+SogTwa::~SogTwa()
+{
+ //dtor
+}
+
diff --git a/src/SogTwa.h b/src/SogTwa.h
new file mode 100644
index 0000000..05a0033
--- /dev/null
+++ b/src/SogTwa.h
@@ -0,0 +1,21 @@
+#ifndef SOGTWA_H
+#define SOGTWA_H
+#include "LDDGraph.h"
+#include "SpotSogIterator.h"
+
+class SogTwa : public spot::twa
+{
+ public:
+ SogTwa(const spot::bdd_dict_ptr& dict_ptr,LDDGraph *sog);
+ virtual ~SogTwa();
+ spot::state* get_init_state() const;
+ SpotSogIterator* succ_iter(const spot::state* s) const override;
+ std::string format_state(const spot::state* s) const override;
+
+ protected:
+
+ private:
+ LDDGraph* m_sog;
+};
+
+#endif // SOGTWA_H
diff --git a/src/SpotSogIterator.cpp b/src/SpotSogIterator.cpp
new file mode 100644
index 0000000..83e3376
--- /dev/null
+++ b/src/SpotSogIterator.cpp
@@ -0,0 +1,52 @@
+#include <spot/twa/twa.hh>
+#include "LDDGraph.h"
+#include "SpotSogState.h"
+#include "SpotSogIterator.h"
+
+
+SpotSogIterator::SpotSogIterator(const LDDState* lddstate):m_lddstate(lddstate)
+{
+
+}
+bool SpotSogIterator::first() {
+ // m_sog->getLDDStateById(m_id)->Successors().
+ //return m_sog->get_successor()
+
+ m_current_edge=0;
+ return m_lddstate->getSuccessors()->size()!=0;
+}
+
+bool SpotSogIterator::next() {
+
+ m_current_edge++;
+ return m_current_edge<m_lddstate->getSuccessors()->size();
+}
+
+bool SpotSogIterator::done() const {
+
+ return m_current_edge==m_lddstate->getSuccessors()->size();
+}
+
+SpotSogState* SpotSogIterator::dst() const
+ {
+ return new SpotSogState(m_lddstate->getSuccessors()->at(m_current_edge).first);
+ }
+
+bdd SpotSogIterator::cond() const {
+ bdd a=bddtrue;//1;
+ string name=m_graph->getTransition(m_lddstate->getSuccessors()->at(m_current_edge).second);
+ cout<<"Transition name "<<name<<endl;
+ //cout<<"Iterator cond()"<<m_current_edge<<"\n";
+ return a;
+}
+
+spot::acc_cond::mark_t SpotSogIterator::acc() const {
+ //cout<<"Iterator acc()\n";
+ return 1U;
+}
+SpotSogIterator::~SpotSogIterator()
+{
+ //dtor
+}
+
+static LDDGraph * SpotSogIterator::m_graph;
diff --git a/src/SpotSogIterator.h b/src/SpotSogIterator.h
new file mode 100644
index 0000000..fb42500
--- /dev/null
+++ b/src/SpotSogIterator.h
@@ -0,0 +1,31 @@
+#ifndef SPOTSOGITERATOR_H
+#define SPOTSOGITERATOR_H
+#include "SpotSogState.h"
+#include "LDDGraph.h"
+// Iterator for a SOG graph
+class SpotSogIterator : public spot::twa_succ_iterator
+{
+ public:
+ static LDDGraph * m_graph;
+ SpotSogIterator(const LDDState *lddstate);
+ virtual ~SpotSogIterator();
+ bool first() override;
+ bool next() override;
+ bool done() const override;
+ SpotSogState* dst() const override;
+// const state * dst () const override;//
+ // a non derived function
+ // std::string format_transition() const;
+ bdd cond() const override final;
+ spot::acc_cond::mark_t acc() const override final;
+
+ protected:
+
+ private:
+ // Associated SOG graph
+
+ LDDState * m_lddstate;
+ unsigned int m_current_edge=0;
+};
+
+#endif // SPOTSOGITERATOR_H
diff --git a/src/SpotSogState.cpp b/src/SpotSogState.cpp
new file mode 100644
index 0000000..ba5e78e
--- /dev/null
+++ b/src/SpotSogState.cpp
@@ -0,0 +1,9 @@
+#include <spot/twa/twa.hh>
+#include "LDDState.h"
+#include "SpotSogState.h"
+
+
+SpotSogState::~SpotSogState()
+{
+ //dtor
+}
diff --git a/src/SpotSogState.h b/src/SpotSogState.h
new file mode 100644
index 0000000..4f5b3fe
--- /dev/null
+++ b/src/SpotSogState.h
@@ -0,0 +1,39 @@
+#ifndef SPOTSOGSTATE_H
+#define SPOTSOGSTATE_H
+
+#include "LDDState.h"
+class SpotSogState : public spot::state
+{
+public:
+ SpotSogState(LDDState *st):m_state(st) {};
+ virtual ~SpotSogState();
+
+ SpotSogState* clone() const override
+ {
+ return new SpotSogState(m_state);
+ }
+ size_t hash() const override
+ {
+ return m_state->getLDDValue();
+ }
+
+ int compare(const spot::state* other) const override
+ {
+ auto o = static_cast<const SpotSogState*>(other);
+ size_t oh = o->hash();
+ size_t h = hash();
+ if (h < oh)
+ return -1;
+ else
+ return h > oh;
+ }
+ LDDState* getLDDState() {
+ return m_state;
+ }
+protected:
+
+private:
+ LDDState *m_state;
+};
+
+#endif // SPOTSOGSTATE_H
diff --git a/src/main.cpp b/src/main.cpp
index aa4cbab..eef6a27 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -22,6 +22,7 @@
#include <spot/twaalgos/emptiness.hh>
#include <spot/tl/apcollect.hh>
#include "Net.hpp"
+#include "SogTwa.h"
@@ -36,7 +37,7 @@ int Formula_transitions(const char * f, Set_mot& formula_trans, net Rv) ;
unsigned int nb_th;
int n_tasks, task_id;
-
+spot::formula not_f;
set<string> buildObsTransitions(const string &fileName) {
string input;
set<string> transitionSet;
@@ -64,6 +65,8 @@ set<string> buildObsTransitions(const string &fileName) {
transitionSet.insert((*i).ap_name());
}
print_spin_ltl(std::cout, fo)<<'\n';
+ cout<<"Building formula negation\n";
+ not_f = spot::formula::Not(pf.f);
return transitionSet;
}
@@ -154,6 +157,19 @@ int main(int argc, char** argv)
DR.computeSOGLaceCanonized(g);
g.printCompleteInformation();
}
+ cout<<"Building automata for not(formula)\n";
+ auto d = spot::make_bdd_dict();
+ spot::twa_graph_ptr af = spot::translator(d).run(not_f);
+ cout<<"Formula automata built.\n";
+ auto k = std::make_shared<SogTwa>(d,DR.getGraph());
+ spot::print_dot(std::cout, k);
+
+ /*
+ if (auto run = k->intersecting_run(af))
+ std::cout << "formula is violated by the following run:\n" << *run;
+ else
+ std::cout << "formula is verified\n";*/
+
}
}
diff --git a/src/threadSOG.cpp b/src/threadSOG.cpp
index 40da1bf..2785c1f 100644
--- a/src/threadSOG.cpp
+++ b/src/threadSOG.cpp
@@ -84,6 +84,7 @@ threadSOG::threadSOG(const net &R, int BOUND, int nbThread,bool uselace,bool ini
NonObservable=R.NonObservable;
Formula_Trans=R.Formula_Trans;
transitionName=R.transitionName;
+
InterfaceTrans=R.InterfaceTrans;
m_nbPlaces=R.places.size();
cout<<"Nombre de places : "<<m_nbPlaces<<endl;
@@ -255,11 +256,7 @@ void threadSOG::computeSeqSOG(LDDGraph &g)
{
// cout<<"not found"<<endl;
reached_class->m_boucle=Set_Div(Complete_meta_state);
- // cout<<"Divergence "<<Set_Div(Complete_meta_state)<<endl;
- // cout<<"blocage "<<Set_Bloc(Complete_meta_state)<<endl;
- //reached_class->blocage=Set_Bloc(Complete_meta_state);
- //reached_class->boucle=Set_Div(Complete_meta_state);
fire=firable_obs(Complete_meta_state);
st.push(Pair(couple(reached_class,Complete_meta_state),fire));
//TabMeta[nbmetastate]=reached_class->m_lddstate;
@@ -663,6 +660,7 @@ void threadSOG::computeDSOG(LDDGraph &g,bool canonised)
cout << "number of threads "<<m_nb_thread<<endl;
int rc;
m_graph=&g;
+ m_graph->setTransition(transitionName);
m_id_thread=0;
pthread_mutex_init(&m_mutex, NULL);
@@ -1130,6 +1128,7 @@ void threadSOG::computeSOGLace(LDDGraph &g)
clock_gettime(CLOCK_REALTIME, &start);
Set fire;
m_graph=&g;
+ m_graph->setTransition(transitionName);
m_nbmetastate=0;
m_MaxIntBdd=0;
@@ -1322,6 +1321,7 @@ void threadSOG::computeSOGLaceCanonized(LDDGraph &g)
clock_gettime(CLOCK_REALTIME, &start);
Set fire;
m_graph=&g;
+ m_graph->setTransition(transitionName);
m_nbmetastate=0;
@@ -1411,3 +1411,7 @@ cout<<"\n=========================================\n";
}
+LDDGraph *threadSOG::getGraph() const {
+ return m_graph;
+}
+
diff --git a/src/threadSOG.h b/src/threadSOG.h
index 977526a..26008f2 100644
--- a/src/threadSOG.h
+++ b/src/threadSOG.h
@@ -37,7 +37,8 @@ class threadSOG {
void computeSOGLace(LDDGraph &g);
void computeSOGLaceCanonized(LDDGraph &g);
Set * getNonObservable();
- vector<TransSylvan>* getTBRelation();
+ vector<TransSylvan>* getTBRelation();
+ LDDGraph *getGraph() const;
protected:
private:
////////////////////////////////
--
GitLab