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

Implement UFSCC parallel emptiness-check

parent b1de0fed
No related branches found
No related tags found
1 merge request!7Feature/ufscc emptiness check
Pipeline #5256 failed with stage
in 7 seconds
Subproject commit d4e88608eeac51cb9f3f759e6b98c28f0cb03699
Subproject commit 23e1d1a201121cd014c427d9750d7d4769f1f5f4
......@@ -103,7 +103,7 @@ add_executable(pmc-sog main.cpp
algorithm/UFSCC.h
algorithm/UFSCC.cpp
algorithm/ParallelMCBase.h
algorithm/ParallelMCBase.cpp algorithm/Renault.cpp algorithm/Renault.h)
algorithm/ParallelMCBase.cpp algorithm/Renault.cpp algorithm/Renault.h misc/SafeMap.cpp misc/SafeMap.h)
target_include_directories(pmc-sog PUBLIC "${PROJECT_BINARY_DIR}/src")
......
......@@ -18,6 +18,7 @@ void UFSCC::threadHandler(void *context) {
void UFSCC::threadRun() {
uint16_t idThread = mIdThread++;
vector<myStateU_t *> Rp;
cout<<"Bonjour\n";
ufscc(mInitStatePtr, Rp, idThread);
}
......@@ -28,9 +29,10 @@ void UFSCC::ufscc(myStateU_t *state, vector<myStateU_t *> &Rp, uint8_t idThread)
mCycleDetected=true;
return;
}
assert(state!= nullptr);
Rp.emplace_back(state);
computeSuccessors(state);
auto & setS=mS[state];
auto setS=mS.mMap.at(state);//mS[state];
auto iterVP=setS.begin();
while (iterVP!=setS.end()) {
auto &vp=*iterVP;
......@@ -42,37 +44,41 @@ void UFSCC::ufscc(myStateU_t *state, vector<myStateU_t *> &Rp, uint8_t idThread)
}
if (static_cast<myStateU_t *>(elt.first)->mDead || static_cast<myStateU_t *>(elt.first)->mProcessed) continue;
bool isNew {false};
for (const auto &wp: mS) {
if (std::find(Rp.begin(),Rp.end(),static_cast<myStateU_t *>(elt.first)) == Rp.end())
if (std::find(wp.second.begin(),wp.second.end(),static_cast<myStateU_t *>(elt.first)) != wp.second.end()) {
ufscc(static_cast<myStateU_t *>(elt.first), Rp, idThread);
isNew = true;
break;
}
/*bool isNew {false};
{
for (const auto wp: mS.mMap) {
if (std::find(Rp.begin(), Rp.end(), static_cast<myStateU_t *>(elt.first)) == Rp.end())
if (std::find(wp.second.begin(), wp.second.end(), static_cast<myStateU_t *>(elt.first)) != wp.second.end()) {
ufscc(static_cast<myStateU_t *>(elt.first), Rp, idThread);
isNew = true;
break;
}
}
}*/
bool isNew {mS.findState(static_cast<myStateU_t *>(elt.first),Rp)};
if (isNew) {
ufscc(static_cast<myStateU_t *>(elt.first), Rp, idThread);
}
if (!isNew) {
while (mS[static_cast<myStateU_t *>(elt.first)] != mS[state]) {
auto& r=Rp.back();Rp.pop_back();
auto& s=Rp.back();
mS[r].merge(mS[s]);
mS[s]=mS[r];
else {
while (Rp.size()>1 && !mS.equal(static_cast<myStateU_t *>(elt.first), state)) {
auto r=Rp.back();Rp.pop_back();
auto s=Rp.back();
mS.merge(r,s);//mS.mMap[r].merge(mS.mMap[s]);
}
for (const auto & w: mS[state]) {
for (const auto & w: mS.mMap[state]) {
if (w->isAcceptance) {
mCycleDetected=true;
return;
}
}
}
}
vp->mProcessed=true;
}
++iterVP;
} //End while
for (const auto & elt : mS[state])
for (const auto & elt : mS.mMap[state])
elt->mDead=true;
if (Rp.back()==state) Rp.pop_back();
}
......
......@@ -5,6 +5,7 @@
#ifndef PMC_SOG_UFSCC_H
#define PMC_SOG_UFSCC_H
#include "ParallelMCBase.h"
#include "misc/SafeMap.h"
struct myStateU_t : public myStateBase_t {
......@@ -19,7 +20,8 @@ public:
UFSCC(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh);
virtual ~UFSCC();
private:
std::map<myStateU_t *,std::set<myStateU_t *>> mS;
mutex mMutexMS;
SafeMap<myStateU_t *,std::set<myStateU_t *>> mS;
myStateU_t *mInitStatePtr;
vector<myStateU_t *> mlBuiltStates;
static void threadHandler(void *context);
......
......@@ -41,7 +41,7 @@ SafeDequeue<T>::~SafeDequeue()
template<typename T>
void SafeDequeue<T>::push ( T new_value )
{
std::lock_guard<std::mutex> lk ( mut );
std::lock_guard lk ( mut );
data_queue.push ( new_value );
data_cond.notify_one();
......@@ -64,7 +64,7 @@ bool SafeDequeue<T>::try_pop ( T& value )
template<typename T>
bool SafeDequeue<T>::empty() const
{
std::lock_guard<std::mutex> lk ( mut );
std::lock_guard lk ( mut );
return data_queue.empty();
}
......
//
// Created by chiheb on 28/12/22.
//
#include "SafeMap.h"
#include "algorithm/UFSCC.h"
template<typename T,typename V>
typename std::map<T,V>::iterator SafeMap<T,V>::find(const T & x) {
std::shared_lock lk(mMutex);
return mMap.find(x);
}
template<typename T,typename V>
void SafeMap<T,V>::emplace(T& t,V& v) {
std::lock_guard lk(mMutex);
mMap.emplace(t,v);
}
template<typename T,typename V>
void SafeMap<T,V>::merge(T dest,T src) {
std::lock_guard lk(mMutex);
mMap[dest].merge(mMap[src]);
mMap[src]=mMap[dest];
}
template<typename T,typename V>
bool SafeMap<T,V>::equal(const T& r, T& s) const {
std::shared_lock lk(mMutex);
return mMap[s] == mMap[r];
}
template<typename T,typename V>
bool SafeMap<T,V>::findState(const T& state,const std::vector<T>& Rp) {
bool isNew {false};
std::shared_lock lk(mMutex);
for (const auto & wp: mMap) {
if (std::find(Rp.begin(), Rp.end(), state) == Rp.end())
if (std::find(wp.second.begin(), wp.second.end(), state) != wp.second.end()) {
isNew = true;
break;
}
}
return isNew;
}
template class SafeMap<myStateU_t *,std::set<myStateU_t *>>;
\ No newline at end of file
//
// Created by chiheb on 28/12/22.
//
#ifndef PMC_SOG_SAFEMAP_H
#define PMC_SOG_SAFEMAP_H
#include <mutex>
#include <shared_mutex>
#include <map>
#include <vector>
//#include "algorithm/UFSCC.h"
template<typename T,typename V>
class SafeMap {
private:
mutable std::shared_mutex mMutex;
public:
std::map<T,V> mMap;
typename std::map<T,V>::iterator find(const T & );
void emplace(T&,V&);
void merge(T,T);
bool equal(const T&, T&) const;
bool findState(const T&,const std::vector<T>& );
};
#endif //PMC_SOG_SAFEMAP_H
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment