diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp
index 8c1a4bf4213127ad73cad8370bd1cadbfba40cee..b4a4d6874dcf3ecb262a86df74fd817e771f722e 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -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;
////
diff --git a/src/algorithm/CNDFS.h b/src/algorithm/CNDFS.h
index d367f6a565c61be7e4245c7b97e8f35c1927d043..588582f5d80bb316fa6d77887b231a4d71da1db7 100644
--- a/src/algorithm/CNDFS.h
+++ b/src/algorithm/CNDFS.h
@@ -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;
};
diff --git a/src/main.cpp b/src/main.cpp
index 80d45355b658f9030b11718a2de179cd6b083fc5..5c6337e1277f33e3a988d9c8bfc5417a8960e111 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -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);