From 60b0e4c685206c31a3f237bb5ed19a6145742f79 Mon Sep 17 00:00:00 2001
From: Ghofrane Amaimi <ghofraneeamaimi@gmail.com>
Date: Wed, 1 Jun 2022 18:37:50 +0200
Subject: [PATCH] add an adjacency list to the _state struct
---
src/algorithm/CNDFS.cpp | 33 +++++++++++++++++++++++++--------
src/algorithm/CNDFS.h | 8 +++++---
2 files changed, 30 insertions(+), 11 deletions(-)
diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp
index 1e164a3..480bbde 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -11,6 +11,7 @@
#include <utility>
#include <spot/twa/twa.hh>
#include <bddx.h>
+#include <cstddef>
using namespace std;
@@ -47,15 +48,29 @@ CNDFS::_state* CNDFS::getInitialState(){
_state * initStatePtr = static_cast<_state *>(malloc(sizeof(_state)));
initStatePtr->left = mMcl->getInitialMetaState();
initStatePtr->right = mAa->get_init_state();
+ initStatePtr->new_successors = static_cast<vector<pair<_state *, int>>>(NULL);
initStatePtr->isAcceptance = mAa->state_is_accepting(mAa->get_init_state());
initStatePtr->isConstructed = true;
return initStatePtr;
}
+//this function is to build a state with list of successor initially null
+CNDFS::_state* CNDFS::buildState(LDDState* left, spot::state* right, vector<pair<_state *, int>> succ, bool acc, bool constructed){
+ _state * buildStatePtr = static_cast<_state *>(malloc(sizeof(_state)));
+ buildStatePtr->left = left;
+ buildStatePtr->right = dynamic_cast<const spot::twa_graph_state *>(right);
+ buildStatePtr->new_successors = static_cast<vector<pair<_state *, int>>>(NULL);
+ buildStatePtr->isAcceptance = acc;
+ buildStatePtr->isConstructed = constructed;
+ return buildStatePtr;
+}
+
+
//compute new successors of a product state
-void CNDFS::computeSuccessors(LDDState *sog_current_state, const spot::twa_graph_state *ba_current_state)
+void CNDFS::computeSuccessors(_state *state)
{
-
+ LDDState* sog_current_state = state->left;
+ const spot::twa_graph_state* ba_current_state = state->right;
while (!sog_current_state);
while (!sog_current_state->isCompletedSucc());
//fetch the state's atomic proposition
@@ -101,9 +116,11 @@ void CNDFS::computeSuccessors(LDDState *sog_current_state, const spot::twa_graph
if (matched!=bddfalse)
{
cout << "matched bdd " << matched << endl;
- //new terminal state
- _state nd = {sog_current_state->Successors.at(i).first, dynamic_cast<const spot::twa_graph_state *> (ii->dst()), mAa->state_is_accepting(ii->dst()),true};
- new_successors.push_back(make_pair(nd,transition));
+ //new terminal state without successors
+ _state* nd = buildState(sog_current_state->Successors.at(i).first,
+ const_cast<spot::state *>(ii->dst()), static_cast<vector<pair<_state *, int>>>(NULL), mAa->state_is_accepting(ii->dst()), true);
+ //add the successor found to the vestor of successor of the current state
+ state->new_successors.push_back(make_pair(nd,transition));
cout << *it << " is a common transaction!" << endl; // p->var_map.find ( f )->second => donne la bdd
}
}
@@ -121,9 +138,9 @@ void CNDFS::dfsBlue(_state *state) {
uint16_t idThread = mIdThread++;
cout << state->isConstructed << endl;
- computeSuccessors(state->left,state->right);
- for (auto p: new_successors) {
- std::cout << "list of successors of current state " << "({ " << p.first.right << ", " << p.first.left << ", " << p.first.isAcceptance << ", " << p.first.isConstructed << " }" << ", " << p.second << ") ";
+ computeSuccessors(state);
+ for (auto p:state->new_successors) {
+ std::cout << "list of successors of current state " << "({ " << p.first->right << ", " << p.first->left << ", " << p.first->isAcceptance << ", " << p.first->isConstructed << " }" << ", " << p.second << ") ";
}
// for (auto k = new_successors.begin(); k != new_successors.end(); ++k)
diff --git a/src/algorithm/CNDFS.h b/src/algorithm/CNDFS.h
index a4d654e..0e44440 100644
--- a/src/algorithm/CNDFS.h
+++ b/src/algorithm/CNDFS.h
@@ -27,18 +27,20 @@ public:
typedef struct _state{
LDDState *left;
const spot::twa_graph_state* right;
- bool isAcceptance;
+ vector<pair<_state* , int>> new_successors ;
+ bool isAcceptance = false;
bool isConstructed = false;
} _state;
- vector<pair<_state , int>> new_successors;
+// vector<pair<_state , int>> new_successors;
list<spot::formula> transitionNames;
vector<bdd>temp;
CNDFS(ModelCheckBaseMT *mcl,const spot::twa_graph_ptr &af,const uint16_t& nbTh);
virtual ~CNDFS();
- void computeSuccessors(LDDState* sog_current_state,const spot::twa_graph_state* ba_current_state);
+ void computeSuccessors(_state *state);
void dfsBlue(_state *state);
_state* getInitialState();
+ _state* buildState(LDDState* left, spot::state* right, vector<pair<_state *, int>> succ, bool acc, bool constructed);
static spot::bdd_dict_ptr* m_dict_ptr;
};
--
GitLab