Skip to content
Snippets Groups Projects
Commit c7f454a3 authored by chihebabid's avatar chihebabid
Browse files

Fix code for NDFS algorithm

parent 770b7030
No related branches found
No related tags found
1 merge request!6Feature/ufscc emptiness check
Pipeline #5038 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
src/algorithm/CNDFS.cpp
+ 100
− 117
View file @ c7f454a3
......@@ -11,17 +11,16 @@
#include <utility>
#include <spot/twa/twa.hh>
#include <bddx.h>
#include <cstddef>
#include <deque>
#include <atomic>
#include <condition_variable>
#include "misc/SafeDequeue.h"
#include <algorithm>
#include "misc/stacksafe.h"
using namespace std;
CNDFS::CNDFS(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh) : mMcl(mcl), mAa(af), mNbTh(nbTh)
{
CNDFS::CNDFS(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh) : mMcl(mcl), mAa(af),
mNbTh(nbTh) {
getInitialState();
spawnThreads();
}
......@@ -46,168 +45,151 @@ void CNDFS::spawnThreads() {
void CNDFS::threadHandler(void *context) {
((CNDFS *) context)->threadRun();
}
void CNDFS::threadRun() {
uint16_t idThread = mIdThread++;
vector<myState_t*> Rp;
dfsBlue(mInitStatePtr,Rp,idThread);
vector<myState_t *> Rp;
dfsBlue(mInitStatePtr, Rp, idThread);
}
//get initial state of the product automata
void CNDFS::getInitialState(){
mInitStatePtr = new myState_t; //static_cast<_state *>(malloc(sizeof(_state)));
/*
* Build initial state of the product automata
*/
void CNDFS::getInitialState() {
mInitStatePtr = new myState_t;
mInitStatePtr->left = mMcl->getInitialMetaState();
mInitStatePtr->right = mAa->get_init_state();
//mInitStatePtr->new_successors = nullptr;
mInitStatePtr->isAcceptance = mAa->state_is_accepting(mAa->get_init_state());
mInitStatePtr->isConstructed = true;
mlBuiltStates.push_back(mInitStatePtr);
}
//this function is to build a state with list of successor initially null
myState_t* CNDFS::buildState(LDDState* left, spot::state* right, bool acc, bool constructed, bool cyan){
myState_t * buildStatePtr = new myState_t;
myState_t *CNDFS::buildState(LDDState *left, spot::state *right, bool acc, bool constructed, bool cyan) {
myState_t *buildStatePtr = new myState_t;
buildStatePtr->left = left;
buildStatePtr->right = dynamic_cast<const spot::twa_graph_state *>(right);
buildStatePtr->right = (spot::twa_graph_state *) right;
buildStatePtr->isAcceptance = acc;
buildStatePtr->isConstructed = constructed;
return buildStatePtr;
}
std::ostream & operator<<(std::ostream & Str,myState_t* state) {
Str << "({ Sog state= " << state->left << ", BA state= " << state->right << ", acceptance= " << state->isAcceptance << ", constructed= " << state->isConstructed << ", red= " << state->red << ", blue= " << state->blue << " }" << endl;
int i = 0;
for (const auto & ii : state->new_successors)
{
cout << "succ num " << i << ii.first << " with transition " << ii.second<< endl;
i++;
}
std::ostream &operator<<(std::ostream &Str, myState_t *state) {
Str << "({ Sog state= " << state->left << ", BA state= " << state->right << ", acceptance= " << state->isAcceptance
<< ", constructed= " << state->isConstructed << ", red= " << state->red << ", blue= " << state->blue << " }"
<< endl;
int i = 0;
for (const auto &ii: state->new_successors) {
cout << "succ num " << i << ii.first << " with transition " << ii.second << endl;
i++;
}
return Str;
}
//block all threads while awaitCondition is false
//void CNDFS::WaitForTestCompleted(_state* state) {
// while ( awaitCondition(state) == false) ;
//}
void CNDFS::dfsRed(myState_t *state, vector<myState_t*>& Rp,uint8_t idThread)
{
void CNDFS::dfsRed(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread) {
cout << "dfsRed" << endl;
Rp.push_back(state);
computeSuccessors(state);
for (const auto& succ:state->new_successors) {
if (succ.first->cyan[idThread])
{
cout << "cycle detected" << endl;
exit(0);
}
// unvisited and not red state
if ((find(Rp.begin(), Rp.end(), state) != Rp.end()) && ! succ.first->red )
dfsRed(succ.first, Rp,idThread);
for (const auto &succ: state->new_successors) {
if (succ.first->cyan[idThread]) {
cout << "cycle detected" << endl;
exit(0);
}
// unvisited and not red state
if ((find(Rp.begin(), Rp.end(), state) != Rp.end()) && !succ.first->red)
dfsRed(succ.first, Rp, idThread);
}
}
/*
* Check whether a product state exists or not
*/
myState_t *CNDFS::isStateBuilt(LDDState *sogState, spot::twa_graph_state *spotState) {
auto compare = [sogState, spotState](myState_t *state) {
return (state->left == sogState && state->right == spotState);
};
auto result = find_if(begin(mlBuiltStates), end(mlBuiltStates), compare);
return result == end(mlBuiltStates) ? nullptr : *result;
}
//compute new successors of a product state
void CNDFS::computeSuccessors(myState_t *state)
{
auto sog_current_state = state->left;
const spot::twa_graph_state* ba_current_state = state->right;
void CNDFS::computeSuccessors(myState_t *state) {
if (state->succState == SuccState::built) return;
std::unique_lock lk(mMutexStatus);
if (state->succState == SuccState::beingbuilt) {
mMutexStatus.unlock();
mDataCondWait.wait(lk, [state] { return state->succState == SuccState::built; });
return;
}
state->succState = SuccState::beingbuilt;
lk.unlock();
auto sog_current_state = state->left;
const spot::twa_graph_state *ba_current_state = state->right;
while (!sog_current_state->isCompletedSucc());
auto p = mAa->get_dict(); //avoir le dictionnaire bdd,proposition atomique
//fetch the state's atomic proposition
for (const auto & vv: sog_current_state->getMarkedPlaces(mMcl->getPlaceProposition()))
{
auto name = string(mMcl->getPlace(vv));
auto f = spot::formula::ap(name);
transitionNames.push(f);
/* for (const auto & vv: sog_current_state->getMarkedPlaces(mMcl->getPlaceProposition()))
{
auto name = string(mMcl->getPlace(vv));
auto f = spot::formula::ap(name);
transitionNames.push(f);
}
}*/
//iterate over the successors of a current aggregate
for (const auto &elt : sog_current_state->Successors)
{
for (const auto &elt: sog_current_state->Successors) {
auto transition = elt.second; // je récupère le numéro du transition
auto name = string(mMcl->getTransition(transition)); // récuprer le nom de la transition
auto f = spot::formula::ap(name);// récuperer la proposition atomique qui correspond à la transition
transitionNames.push(f); // push state'S AP to edge'S AP
SafeDequeue<spot::formula> tempTransitionNames = transitionNames;
while (!tempTransitionNames.empty())
{
//iterate over the successors of a BA state
auto ii = mAa->succ_iter(ba_current_state);
if (ii->first())
do {
if (p->var_map.find(tempTransitionNames.front()) !=p->var_map.end())
{
//fetch the transition of BA that have the same AP as the SOG transition
const bdd result = bdd_ithvar((p->var_map.find(tempTransitionNames.front()))->second);
if ((ii->cond() & result) != bddfalse)
{
//make a copy that we can iterate
// SafeDequeue<myCouple> tempSharedPool = sharedPool;
SafeDequeue<myState_t*> tempSharedPool = mSharedPoolTemp;
while (!tempSharedPool.empty())
{
std::lock_guard<std::mutex> guard(mMutex);
// if ((tempSharedPool.front().first == sog_current_state->Successors.at(i).first) &&
// (tempSharedPool.front().second == const_cast<spot::state *>(ii->dst())))
if ((tempSharedPool.front()->left == elt.first) && (tempSharedPool.front()->right == const_cast<spot::state *>(ii->dst())))
{
// nd->cyan = true;
state->new_successors.push_back(make_pair(tempSharedPool.front(), transition));
} else
{
//new terminal state without successors
//state_is_accepting() should only be called on automata with state-based acceptance
myState_t *nd = buildState(elt.first,
const_cast<spot::state *>(ii->dst()),
mAa->state_is_accepting(ii->dst()), true, false);
state->new_successors.push_back(make_pair(nd, transition));
}
//
}
}
//iterate over the successors of a BA state
auto ii = mAa->succ_iter(ba_current_state);
if (ii->first())
do {
if (p->var_map.find(f) != p->var_map.end()) {
//fetch the transition of BA that have the same AP as the SOG transition
const bdd result = bdd_ithvar((p->var_map.find(f))->second);
if ((ii->cond() & result) != bddfalse) {
std::unique_lock lk(mMutex);
auto result = isStateBuilt(elt.first, (spot::twa_graph_state *) ii->dst());
if (result) {
state->new_successors.push_back(make_pair(result, transition));
} else {
myState_t *nd = buildState(elt.first,
const_cast<spot::state *>(ii->dst()),
mAa->state_is_accepting(ii->dst()), true, false);
state->new_successors.push_back(make_pair(nd, transition));
}
}
while (ii->next());
mAa->release_iter(ii);
tempTransitionNames.try_pop(tempTransitionNames.front());
}
transitionNames.try_pop(transitionNames.front());
}
} while (ii->next());
mAa->release_iter(ii);
}
state->succState = SuccState::built;
mDataCondWait.notify_all();
}
//Perform the dfsBlue
void CNDFS::dfsBlue(myState_t *state, vector<myState_t*>& Rp,uint8_t idThread) {
state->cyan[idThread]=true;
for (const auto & succ:state->new_successors)
{
if (!succ.first->blue && !succ.first->cyan[idThread])
{
dfsBlue(succ.first,Rp,idThread);
}
void CNDFS::dfsBlue(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread) {
state->cyan[idThread] = true;
for (const auto &succ: state->new_successors) {
if (!succ.first->blue && !succ.first->cyan[idThread]) {
dfsBlue(succ.first, Rp, idThread);
}
}
state->blue = true;
if (state->isAcceptance)
{
if (state->isAcceptance) {
cout << "Acceptance state detected " << endl;
if (state->left->isDeadLock() || state->left->isDiv())
{
cout << "cycle detected: an aggregate with deal_lock or live_lock" << endl;
if (state->left->isDeadLock() || state->left->isDiv()) {
cout << "cycle detected: an aggregate with deal_lock or live_lock" << endl;
exit(0);
} else
{
} else {
Rp.clear();
dfsRed(state, Rp,idThread); //looking for an accepting cycle
// the thread processed the current state waits for all visited accepting nodes (non seed, non red) to turn red
// the late red coloring forces the other acceptance states to be processed in post-order by the other threads
dfsRed(state, Rp, idThread); //looking for an accepting cycle
// the thread processed the current state waits for all visited accepting nodes (non seed, non red) to turn red
// the late red coloring forces the other acceptance states to be processed in post-order by the other threads
bool cond;
do {
cond = true;
......@@ -218,7 +200,7 @@ void CNDFS::dfsBlue(myState_t *state, vector<myState_t*>& Rp,uint8_t idThread) {
}
} while (!cond);
for (const auto& qu: Rp) // prune other dfsRed
for (const auto &qu: Rp) // prune other dfsRed
{
qu->red = true;
}
......@@ -227,5 +209,6 @@ void CNDFS::dfsBlue(myState_t *state, vector<myState_t*>& Rp,uint8_t idThread) {
}
state->cyan[idThread] = false;
}
spot::bdd_dict_ptr *CNDFS::m_dict_ptr;
src/algorithm/CNDFS.h
+ 41
− 25
View file @ c7f454a3
......@@ -3,6 +3,7 @@
//
#ifndef PMC_SOG_CNDFS_H
#define PMC_SOG_CNDFS_H
#include "../ModelCheckBaseMT.h"
#include <spot/tl/apcollect.hh>
#include <cstdint>
......@@ -13,49 +14,64 @@
#include <condition_variable>
#include "misc/SafeDequeue.h"
using namespace std ;
typedef pair<struct myState_t*, int> coupleSuccessor;
static constexpr uint8_t MAX_THREADS=64;
using namespace std;
typedef pair<struct myState_t *, int> coupleSuccessor;
static constexpr uint8_t MAX_THREADS = 64;
enum class SuccState {notyet,beingbuilt,built};
struct myState_t {
LDDState *left;
const spot::twa_graph_state* right;
vector<pair<struct myState_t*, int>> new_successors;
const spot::twa_graph_state *right;
vector<pair<struct myState_t *, int>> new_successors;
bool isAcceptance {false};
bool isConstructed {false};
array<bool,MAX_THREADS> cyan {false};
atomic<bool> blue {false};
atomic<bool> red {false};
array<bool, MAX_THREADS> cyan {false};
atomic<bool> blue{false};
atomic<bool> red{false};
SuccState succState {SuccState::notyet};
};
class CNDFS {
private:
ModelCheckBaseMT * mMcl;
ModelCheckBaseMT *mMcl;
spot::twa_graph_ptr mAa;
uint16_t mNbTh;
atomic<uint8_t> mIdThread;
std::thread* mlThread[MAX_THREADS];
mutex mMutex;
std::thread *mlThread[MAX_THREADS];
mutex mMutex,mMutexStatus;
std::condition_variable mDataCondWait;
condition_variable cv;
void spawnThreads();
myState_t * mInitStatePtr;
SafeDequeue<struct myState_t*> mSharedPoolTemp;
static spot::bdd_dict_ptr* m_dict_ptr;
myState_t *mInitStatePtr;
vector<myState_t *> mlBuiltStates;
SafeDequeue<struct myState_t *> mSharedPoolTemp;
static spot::bdd_dict_ptr *m_dict_ptr;
void getInitialState();
void spawnThreads();
static void threadHandler(void *context);
void threadRun();
void computeSuccessors(myState_t *state);
myState_t *buildState(LDDState *left, spot::state *right, bool acc, bool constructed, bool cyan);
myState_t* isStateBuilt(LDDState *sogState,spot::twa_graph_state *spotState);
public:
// SafeDequeue<myCouple> sharedPool;
SafeDequeue<spot::formula> transitionNames;
SafeDequeue<coupleSuccessor> new_successor;
CNDFS(ModelCheckBaseMT *mcl,const spot::twa_graph_ptr &af,const uint16_t& nbTh);
CNDFS(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh);
virtual ~CNDFS();
void computeSuccessors(myState_t *state);
void dfsBlue(myState_t *state, vector<myState_t*>& Rp,uint8_t idThread);
void dfsRed(myState_t* state, vector<myState_t*>& Rp,uint8_t idThread);
void WaitForTestCompleted(myState_t* state);
myState_t* buildState(LDDState* left, spot::state* right, bool acc, bool constructed,bool cyan);
void dfsBlue(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread);
void dfsRed(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread);
};
......
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