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

adjacency list for successors added

parent 58019f52
No related branches found
No related tags found
1 merge request!6Feature/ufscc emptiness check
Pipeline #5002 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
src/algorithm/CNDFS.cpp
+ 69
− 62
View file @ a4e1affc
......@@ -8,6 +8,7 @@
#include <spot/twa/twagraph.hh>
#include <thread>
#include <vector>
#include <utility>
#include <spot/twa/twa.hh>
#include <bddx.h>
using namespace std;
......@@ -22,18 +23,15 @@ struct end_state{
const spot::state* right;
bool isAcceptance;
};
struct graphEdge {
start_state ss;
end_state es;
int weight;
};
vector<pair<end_state, int> > SOG_successors;
list<spot::formula> transitionNames;
vector<bdd>temp;
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)
{
sog_current_state = mcl->getInitialMetaState();
ba_current_state = mAa->get_init_state();
spawnThreads();
}
......@@ -43,9 +41,8 @@ CNDFS::~CNDFS() {
delete mlThread[i];
}
}
/*
* @Brief Create threads
*/
// Create threads
void CNDFS::spawnThreads() {
for (int i = 0; i < mNbTh; ++i) {
mlThread[i] = new thread(threadHandler, this);
......@@ -59,68 +56,78 @@ void CNDFS::threadHandler(void *context) {
((CNDFS *) context)->computeProduct();
}
/*
* @brief Compute the synchornized product
*/
//Compute the synchronized product
void CNDFS::computeProduct() {
uint16_t idThread = mIdThread++;
while (!mMcl->getInitialMetaState());
LDDState *initialAgg = mMcl->getInitialMetaState();
while (!sog_current_state);
LDDState *initialAgg = sog_current_state;
while (!initialAgg->isCompletedSucc());
//fetch the state's atomic proposition
for (auto vv: mMcl->getInitialMetaState()->getMarkedPlaces(mMcl->getPlaceProposition()))
//fetch the state's atomic proposition
for (auto vv: sog_current_state->getMarkedPlaces(mMcl->getPlaceProposition()))
{
string name = string(mMcl->getPlace(vv));
auto f = spot::formula::ap(name);
transitionNames.push_back(f);
}
// for (int i = 0; i < mMcl->getInitialMetaState()->Successors.size(); i++) {
// cout <<"------"<< " SOG's successor " << i << " ------" << endl;
int transition = mMcl->getInitialMetaState()->Successors.at(0).second; // je récupère le numéro de la première 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_back(f); // push state'S AP to edge'S AP
auto p = mAa->get_dict(); //avoir le dictionnaire bdd,proposition atomique
spot::twa_succ_iterator* ii = mAa->succ_iter(mAa->get_init_state());
if (ii->first())
do
{
temp.push_back(ii->cond());
}
while (ii->next());
mAa->release_iter(ii);
// cout << temp.size() << endl; // 22
// cout << p->bdd_map.size() << endl; //62
for (auto v: p->var_map)
{
cout << v.first << "-----" << v.second << endl;
}
for (auto it = transitionNames.begin(); it != transitionNames.end(); ++it) {
if (p->var_map.find(*it) != p->var_map.end()) { // Chercher la transition
const bdd result=bdd_ithvar((p->var_map.find(*it))->second);
cout << "dbb result " << result << endl;
//chercher les transitions en commun avec les successeurs du premier etat
for (auto i: temp)
for (auto tn: transitionNames)
{
cout << "AP in state " << tn << endl;
}
for (int i = 0; i < sog_current_state->Successors.size(); i++)
{
cout <<"------"<< " SOG's successor " << i << " ------" << endl;
int transition = sog_current_state->Successors.at(i).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_back(f); // push state'S AP to edge'S AP
auto p = mAa->get_dict(); //avoir le dictionnaire bdd,proposition atomique
spot::twa_succ_iterator* ii = mAa->succ_iter(ba_current_state);
if (ii->first())
do
{
// if (result & (const bdd)i == bddtrue)
bdd matched = i&result;
if (matched!=bddfalse)
cout << "matched bdd " << matched << endl;
cout << "is succ acceptance " << mAa->state_is_accepting(ii->dst()) << endl;
temp.push_back(ii->cond());
}
//new starting state
struct start_state ns = {mMcl->getInitialMetaState(), mAa->get_init_state()};
//new terminal state
struct end_state nd = {mMcl->getInitialMetaState()->Successors.at(0).first, ii->dst()}; // Pblm: here I want to detect the right successor of initial state of BA
struct graphEdge ge = {ns,nd,1};
cout << *it << " is a common transaction!" << endl; // p->var_map.find ( f )->second => donne la bdd
} else cout << *it << " isn't a common transaction" << endl;
}
transitionNames.pop_back();
while (ii->next());
mAa->release_iter(ii);
//cout << temp.size() << endl;
//cout << p->bdd_map.size() << endl;
for (auto v: p->var_map)
{
cout << v.first << "-----" << v.second << endl;
}
for (auto it = transitionNames.begin(); it != transitionNames.end(); ++it)
{
if (p->var_map.find(*it) != p->var_map.end())
{ // Chercher la transition
const bdd result=bdd_ithvar((p->var_map.find(*it))->second);
cout << "dbb result " << result << endl;
//chercher les transitions en commun avec les successeurs du premier etat
for (auto tr: temp)
{
bdd matched = tr&result;
if (matched!=bddfalse)
{
cout << "matched bdd " << matched << endl;
//new starting state
struct start_state ns = {sog_current_state, ba_current_state, mAa->state_is_accepting(ba_current_state)};
//new terminal state
struct end_state nd = {sog_current_state->Successors.at(i).first, ii->dst(), mAa->state_is_accepting(ii->dst())};
SOG_successors.push_back(make_pair(nd,transition));
cout << *it << " is a common transaction!" << endl; // p->var_map.find ( f )->second => donne la bdd
}
}
} else cout << *it << " isn't a common transaction" << endl;
}
transitionNames.pop_back();
}
//}
for (auto p: SOG_successors) {
std::cout << "list of successors of current state " << "({ " << p.first.right << ", " << p.first.left << ", " << p.first.isAcceptance << " }" << ", " << p.second << ") ";
}
}
spot::bdd_dict_ptr *CNDFS::m_dict_ptr;
////
......
src/algorithm/CNDFS.h
+ 3
− 2
View file @ a4e1affc
......@@ -9,12 +9,15 @@
#include <spot/tl/apcollect.hh>
#include <cstdint>
#include <thread>
#include <spot/twa/twagraph.hh>
class CNDFS {
private:
static constexpr uint8_t MAX_THREADS=64;
ModelCheckBaseMT * mMcl;
spot::twa_graph_ptr mAa;
LDDState* sog_current_state;
const spot::twa_graph_state* ba_current_state;
uint16_t mNbTh;
atomic<uint8_t> mIdThread;
static void threadHandler(void *context);
......@@ -23,9 +26,7 @@ private:
void spawnThreads();
public:
CNDFS(ModelCheckBaseMT *mcl,const spot::twa_graph_ptr &af,const uint16_t& nbTh);
// CNDFS(shared_ptr<SogKripkeTh> k,const spot::twa_graph_ptr &af,const uint16_t& nbTh);
virtual ~CNDFS();
//static void DfsBlue();
void computeProduct();
static spot::bdd_dict_ptr* m_dict_ptr;
};
......
src/main.cpp
+ 6
− 3
View file @ a4e1affc
......@@ -129,6 +129,7 @@ Formula negateFormula(const string &fileName)
spot::twa_graph_ptr formula2Automaton(const spot::formula &f, spot::bdd_dict_ptr bdd, bool save_dot = false)
{
cout << "\nBuilding automata for not(formula)\n";
spot::twa_graph_ptr af = spot::translator(bdd).run(f);
cout << "Formula automata built." << endl;
......@@ -515,7 +516,6 @@ int main(int argc, char **argv)
// build automata of the negation of the formula
auto d = spot::make_bdd_dict();
spot::twa_graph_ptr af = formula2Automaton(negate_formula.f, d, dot_formula);
// create the SOG
mcl->loadNet();
......@@ -525,8 +525,11 @@ int main(int argc, char **argv)
{
std::cout<<"------------CNDFS-------------"<<std::endl;
// auto k = std::make_shared<SogKripkeTh>(d, mcl, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP());
// CNDFS cndfs(k,af,1);
// threadSOG DR(Rnewnet, nb_th, uselace);
// LDDGraph g(&DR);
//
// DR.computeSeqSOG(g);
// g.printCompleteInformation();
CNDFS cndfs(mcl,af,1);
return(0);
......
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