Skip to content
Snippets Groups Projects
Commit 2b355016 authored by Ghofrane Amaimi's avatar Ghofrane Amaimi
Browse files

CndfsV2::fireable works

parent a53df721
No related branches found
No related tags found
1 merge request!6Feature/ufscc emptiness check
Pipeline #5054 passed with stage
in 1 minute and 40 seconds
Hide whitespace changes
Inline Side-by-side
src/algorithm/CNDFS.cpp
+ 6
− 6
View file @ 2b355016
......@@ -128,14 +128,14 @@ myState_t *CNDFS::isStateBuilt(LDDState *sogState, spot::twa_graph_state *spotSt
//compute new successors of a product state
void CNDFS::computeSuccessors(myState_t *state, vector<spot::formula> ap_sog) {
if (state->succState == SuccState::built) return;
if (state->succState == SuccState::done) return;
std::unique_lock lk(mMutexStatus);
if (state->succState == SuccState::beingbuilt) {
mDataCondWait.wait(lk, [state] { return state->succState == SuccState::built; });
if (state->succState == SuccState::doing) {
mDataCondWait.wait(lk, [state] { return state->succState == SuccState::done; });
mMutexStatus.unlock();
return;
}
state->succState = SuccState::beingbuilt;
state->succState = SuccState::doing;
lk.unlock();
auto sog_current_state = state->left;
const spot::twa_graph_state *ba_current_state = state->right;
......@@ -189,11 +189,11 @@ void CNDFS::computeSuccessors(myState_t *state, vector<spot::formula> ap_sog) {
} while (ii->next());
mAa->release_iter(ii);
}
state->succState = SuccState::built;
state->succState = SuccState::done;
mDataCondWait.notify_all();
}
std::random_device rd;
//Perform the dfsBlue
void CNDFS::dfsBlue(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread, vector<spot::formula> ap_sog) {
state->cyan[idThread] = true;
......
src/algorithm/CNDFS.h
+ 3
− 1
View file @ 2b355016
......@@ -14,12 +14,13 @@
#include <condition_variable>
#include "misc/SafeDequeue.h"
#include <spot/tl/contain.hh>
#include <random>
using namespace std;
typedef pair<struct myState_t *, int> coupleSuccessor;
static constexpr uint8_t MAX_THREADS = 64;
enum class SuccState {notyet,beingbuilt,built};
enum class SuccState {notyet,doing,done};
struct myState_t {
LDDState *left;
const spot::twa_graph_state *right;
......@@ -47,6 +48,7 @@ private:
SafeDequeue<struct myState_t *> mSharedPoolTemp;
static spot::bdd_dict_ptr *m_dict_ptr;
spot::language_containment_checker c;
std::random_device rd;
void getInitialState();
......
src/algorithm/CndfsV2.cpp
+ 50
− 24
View file @ 2b355016
......@@ -22,9 +22,13 @@
#include <spot/twaalgos/contains.hh>
#include <spot/tl/contain.hh>
#include <random>
#include <mutex>
using namespace std;
std::mutex mtx;
CndfsV2::CndfsV2(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh) : mMcl(mcl), mAa(af),
mNbTh(nbTh) {
......@@ -60,8 +64,7 @@ void CndfsV2::threadRun() {
uint16_t idThread = mIdThread++;
vector<myState_t *> Rp;
vector<spot::formula> ap_sog;
vector <spot::formula> communTr;
dfsBlue(mInitStatePtr, Rp, idThread, ap_sog, communTr);
dfsBlue(mInitStatePtr, Rp, idThread, ap_sog);
}
/*
......@@ -129,7 +132,16 @@ myState_t *CndfsV2::isStateBuilt(LDDState *sogState, const spot::twa_graph_state
//compute new successors of a product state
vector<spot::formula> CndfsV2::fireable(myState_t *state, vector<spot::formula> ap_sog, vector <spot::formula> communTr) {
void CndfsV2::fireable(myState_t *state, vector<spot::formula> ap_sog, uint8_t idThread) {
if (state->succState == SuccState::done) return;
std::unique_lock lk(mMutexStatus);
if (state->succState == SuccState::doing) {
mDataCondWait.wait(lk, [state] { return state->succState == SuccState::done; });
mMutexStatus.unlock();
return;
}
state->succState = SuccState::doing;
lk.unlock();
auto sog_current_state = state->left;
const spot::twa_graph_state *ba_current_state = state->right;
while (!sog_current_state->isCompletedSucc());
......@@ -158,6 +170,7 @@ vector<spot::formula> CndfsV2::fireable(myState_t *state, vector<spot::formula>
if (p->var_map.find(ap_edge) != p->var_map.end()) {
ap_sog.push_back(ap_edge);
}
spot::formula pa_sog_result = spot::formula::And(ap_sog);
// cout << "formula sog: " << pa_sog_result << endl;
//iterate over the successors of a BA state
......@@ -165,44 +178,57 @@ vector<spot::formula> CndfsV2::fireable(myState_t *state, vector<spot::formula>
if (ii->first())
do {
auto pa_ba_result = spot::bdd_to_formula(ii->cond(), p); // from bdd to formula
if (c.contained(pa_sog_result, pa_ba_result) || c.contained(pa_ba_result, pa_sog_result)) {
communTr.push_back(pa_sog_result);
if (c.contained(pa_sog_result, pa_ba_result) || c.contained(pa_ba_result, pa_sog_result))
{
std::unique_lock lk(mMutex);
if (std::find(commonTr.begin(), commonTr.end(), pa_sog_result) == commonTr.end()) {
cout << "I'm here " << unsigned (idThread) << endl;
commonTr.push_back(pa_sog_result);
}
}
} while (ii->next());
mAa->release_iter(ii);
}
return communTr;
state->succState = SuccState::done;
mDataCondWait.notify_all();
}
int i = 0 ;
//Perform the dfsBlue
void CndfsV2::dfsBlue(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread, vector<spot::formula> ap_sog, vector <spot::formula> communTr) {
void CndfsV2::dfsBlue(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread, vector<spot::formula> ap_sog) {
state->cyan[idThread] = true;
communTr = fireable(state, ap_sog, communTr);
fireable(state, ap_sog, idThread);
// std::mt19937 g(rd());
// std::shuffle(communTr.begin(), communTr.end(), g);
mMutexStatus.lock();
spot::formula sel_elem = communTr[communTr.size()-1];
cout << "hello from thread " << unsigned(idThread) << " transition " << sel_elem << endl;
communTr.pop_back();
mMutexStatus.unlock();
// myState_t* st = buildState(state,tr);
// myState_t* s = isStateBuilt(st->left,st->right);
// if(s)
// {
// std::shuffle(commonTr.begin(), commonTr.end(), g);
//
{
std::unique_lock lk(mMutex);
if (commonTr.size()>0)
{
spot::formula sel_elem = commonTr[commonTr.size()-1];
cout << "hello from thread " << unsigned(idThread) << " transition " << sel_elem << " size " << commonTr.size() << endl;
commonTr.pop_back();
}
}
// myState_t* st = buildState(state,sel_elem);
// myState_t* s = isStateBuilt(st->left,st->right);
// if(s)
// {
// free(st);
// state->new_successors.push_back(make_pair(s,0));
// }else
// {
// }else
// {
// mlBuiltStates.push_back(st);
// state->new_successors.push_back(make_pair(st,0));
// }
// }
// commonTr.pop_back();
// for (const auto &succ: state->new_successors) {
// if (!succ.first->blue && !succ.first->cyan[idThread]) {
// dfsBlue(succ.first, Rp, idThread, ap_sog, communTr);
// dfsBlue(succ.first, Rp, idThread, ap_sog, commonTr);
// }
// }
// state->blue = true;
......
src/algorithm/CndfsV2.h
+ 5
− 3
View file @ 2b355016
......@@ -42,6 +42,7 @@ private:
static spot::bdd_dict_ptr *m_dict_ptr;
spot::language_containment_checker c;
std::random_device rd;
vector <spot::formula> commonTr;
void getInitialState();
......@@ -52,16 +53,17 @@ private:
void threadRun();
// void computeSuccessors(myState_t *state, vector<spot::formula> ap_sog);
vector<spot::formula> fireable(myState_t *state, vector<spot::formula> ap_sog, vector <spot::formula> transition);
void fireable(myState_t *state, vector<spot::formula> ap_sog, uint8_t idThread);
myState_t *buildState(myState_t *state, spot::formula tr);
myState_t* isStateBuilt(LDDState *sogState,const spot::twa_graph_state *spotState);
public:
public:
CndfsV2(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh);
virtual ~CndfsV2();
void dfsBlue(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread,vector<spot::formula> ap_sog, vector <spot::formula> transition);
void dfsBlue(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread,vector<spot::formula> ap_sog);
void dfsRed(myState_t *state, vector<myState_t *> &Rp, uint8_t idThread);
......
src/misc/SafeDequeue.cpp
+ 4
− 4
View file @ 2b355016
......@@ -72,10 +72,10 @@ template <typename T>
T& SafeDequeue<T>::front()
{
std::unique_lock<std::mutex> lk(mut);
while (data_queue.empty())
{
data_cond.wait(lk);
}
// while (data_queue.empty())
// {
// data_cond.wait(lk);
// }
return data_queue.front();
}
......
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