From 680059bd95fc927052727d129834d2ce85a6a4b8 Mon Sep 17 00:00:00 2001
From: chihebabid <chiheb.abid@fst.utm.tn>
Date: Fri, 20 May 2022 10:19:12 +0100
Subject: [PATCH] Add transition fetching
---
src/MCMultiCore/ModelCheckerCPPThread.h | 1 +
src/algorithm/CNDFS.cpp | 23 ++++++++++++++++++++---
src/algorithm/CNDFS.h | 1 +
src/main.cpp | 5 +++--
4 files changed, 25 insertions(+), 5 deletions(-)
diff --git a/src/MCMultiCore/ModelCheckerCPPThread.h b/src/MCMultiCore/ModelCheckerCPPThread.h
index e6a6a6c..bee99e8 100644
--- a/src/MCMultiCore/ModelCheckerCPPThread.h
+++ b/src/MCMultiCore/ModelCheckerCPPThread.h
@@ -20,6 +20,7 @@ public:
static void threadHandler(void *context);
void Compute_successors();
void ComputeTh_Succ();
+ //LDDState * getInitialMetaState() override;
private:
void preConfigure();
bool hasToProcess() const;
diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp
index 83bf87e..a476ce7 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -34,7 +34,9 @@ vector<new_state_succ> successors_new_node;
CNDFS::CNDFS(ModelCheckBaseMT *mcl, const spot::twa_graph_ptr &af, const uint16_t &nbTh) : mMcl(mcl), mAa(af),
- mNbTh(nbTh) {}
+ mNbTh(nbTh) {
+ spawnThreads();
+}
CNDFS::~CNDFS() {
for (int i = 0; i < mNbTh; ++i) {
@@ -94,6 +96,21 @@ void CNDFS::threadHandler(void *context) {
* @brief Compute the synchornized product
*/
void CNDFS::computeProduct() {
- mIdThread++;
+ uint16_t idThread=mIdThread++;
+ //cout<<"My id : "<<mMcl;
+ while (!mMcl->getInitialMetaState());
+ LDDState * initialAgg=mMcl->getInitialMetaState();
+ while (!initialAgg->isCompletedSucc());
+ int transition=mMcl->getInitialMetaState()->Successors.at(0).second;
+ std::cout<<"La transition : "<<string(mMcl->getTransition ( transition ))<<std::endl;
+ auto f=spot::formula::ap (string("Catch1_3"));//string(mMcl->getTransition ( transition )));
+ auto p=mAa->get_dict();
+ if (p->var_map.find ( f )==p->var_map.end()) {
+ cout<<"Ok!";
+ }
+ //bdd result=bdd_ithvar ( ( p->var_map.find ( f ) )->second );
+
+ //mAa->edge_data(0)
+}
-}
\ No newline at end of file
+spot::bdd_dict_ptr* CNDFS::m_dict_ptr;
\ No newline at end of file
diff --git a/src/algorithm/CNDFS.h b/src/algorithm/CNDFS.h
index 13fd776..185520e 100644
--- a/src/algorithm/CNDFS.h
+++ b/src/algorithm/CNDFS.h
@@ -25,6 +25,7 @@ public:
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 4354610..294a73c 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -500,6 +500,7 @@ int main(int argc, char **argv)
/**************************************************************************
* Multi-core version
**************************************************************************/
+ //n_tasks=1;
if (n_tasks == 1)
{
cout<< "Hello Multi-core version" <<endl;
@@ -507,6 +508,7 @@ int main(int argc, char **argv)
if (!explicit_mc)
{
// get the corresponding multi-core model-checker
+ // exit(0);
ModelCheckBaseMT *mcl = getMultiCoreMC(Rnewnet, nb_th, thread_library, progressive, por);
// build automata of the negation of the formula
@@ -521,8 +523,7 @@ int main(int argc, char **argv)
if (algorithm == "UFSCC" || algorithm == "CNDFS")
{
-// cout<<"pointeur sur sog "<< typeid(mcl).name() <<endl;
-// cout <<"pointeur sur BA "<< typeid(aa).name() <<endl;
+ std::cout<<"I'm here"<<std::endl;
CNDFS cndfs(mcl,af,3);
--
GitLab