From 3020bee90e337ec0a2a9aaa2c6d74029af13d287 Mon Sep 17 00:00:00 2001
From: Ghofrane Amaimi <ghofraneeamaimi@gmail.com>
Date: Wed, 4 May 2022 18:28:33 +0200
Subject: [PATCH] get initial states of SOG and BA
---
src/CMakeLists.txt | 3 ++-
src/algorithm/CNDFS.cpp | 8 ++++++--
src/algorithm/CNDFS.h | 6 +++---
src/main.cpp | 14 +++++++++-----
src/threadSOG.cpp | 2 --
5 files changed, 20 insertions(+), 13 deletions(-)
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index ec66b0a..3a31882 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -49,7 +49,8 @@ add_executable(pmc-sog main.cpp
LDDState.cpp
LDDState.h
TransSylvan.cpp
-
+ algorithm/CNDFS.h
+ algorithm/CNDFS.cpp
SpotSogState.cpp
SpotSogState.h
SpotSogIterator.cpp
diff --git a/src/algorithm/CNDFS.cpp b/src/algorithm/CNDFS.cpp
index 7fbbe51..6c2c0a7 100644
--- a/src/algorithm/CNDFS.cpp
+++ b/src/algorithm/CNDFS.cpp
@@ -2,11 +2,15 @@
// Created by ghofrane on 5/4/22.
//
#include "CNDFS.h"
+#include "ModelCheckBaseMT.h"
#include <iostream>
+#include <spot/tl/apcollect.hh>
+#include <spot/twa/twagraph.hh>
using namespace std;
CNDFS::~CNDFS()=default;
-void CNDFS::DfsBlue() {
- cout << "hello from cndfs class" << endl;
+void CNDFS::DfsBlue( ModelCheckBaseMT &mcl, shared_ptr<spot::twa_graph> af) {
+ cout << "First state SOG from CNDFS " << mcl.getInitialMetaState() << endl;
+ cout << "First state BA from CNDFS " << af->acc() <<endl;
}
\ No newline at end of file
diff --git a/src/algorithm/CNDFS.h b/src/algorithm/CNDFS.h
index f7a0484..81011a6 100644
--- a/src/algorithm/CNDFS.h
+++ b/src/algorithm/CNDFS.h
@@ -4,12 +4,12 @@
#ifndef PMC_SOG_CNDFS_H
#define PMC_SOG_CNDFS_H
-
+#include "ModelCheckBaseMT.h"
+#include <spot/tl/apcollect.hh>
class CNDFS {
public:
-
virtual ~CNDFS();
- void DfsBlue();
+ void DfsBlue(ModelCheckBaseMT &mcl, shared_ptr<spot::twa_graph> af);
};
diff --git a/src/main.cpp b/src/main.cpp
index b4b7947..01fb415 100644
--- a/src/main.cpp
+++ b/src/main.cpp
@@ -36,7 +36,7 @@
#include "Hybrid/MCHybridReqPOR/MCHybridSOGReqPOR.h"
#include "Hybrid/MCHybridPOR/MCHybridSOGPOR.h"
#include "algorithm/CNDFS.h"
-
+#include <typeinfo>
using namespace std;
@@ -509,6 +509,7 @@ 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);
+ shared_ptr<spot::twa_graph> aa = formula2Automaton(negate_formula.f, d, dot_formula);
// create the SOG
mcl->loadNet();
@@ -517,10 +518,13 @@ int main(int argc, char **argv)
// TODO: Implement here Ghofrane's algorithms
if (algorithm == "UFSCC" || algorithm == "CNDFS")
{
+ cout<<"pointeur sur le sog "<< typeid(mcl).name() <<endl;
+ //cout << "pointeur sur le BA "<< typeid(af).name() <<endl;
+ cout << "pointeur sur le BA "<< typeid(aa).name() <<endl;
- cout << "HELLO" << endl;
- CNDFS n;
- n.DfsBlue();
+ CNDFS n;
+ //n.DfsBlue();
+ n.DfsBlue(*mcl, aa);
return(0);
//exit(0);
@@ -528,7 +532,7 @@ int main(int argc, char **argv)
else // run on the fly sequential model-checking
{
auto k = std::make_shared<SogKripkeTh>(d, mcl, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP());
- runOnTheFlyMC(algorithm, k, af);
+ //runOnTheFlyMC(algorithm, k, af);
}
// stop model checker process
diff --git a/src/threadSOG.cpp b/src/threadSOG.cpp
index 303bb70..dab8331 100644
--- a/src/threadSOG.cpp
+++ b/src/threadSOG.cpp
@@ -6,8 +6,6 @@
#include "threadSOG.h"
-
-
/*
void write_to_dot(const char *ch,MDD m)
{
--
GitLab