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

main and CNDFS CLASS connexion

parent 53155cc8
No related branches found
No related tags found
1 merge request!6Feature/ufscc emptiness check
Pipeline #4934 failed
......@@ -27,7 +27,7 @@ include_directories(${MPI_INCLUDE_PATH})
# include spot and bddx library
add_library(spot SHARED IMPORTED)
add_library(bddx SHARED IMPORTED)
add_library(bddx SHARED IMPORTED algorithm/CNDFS.cpp algorithm/CNDFS.h)
if(NOT SPOT_LIBRARY)
set_target_properties(spot PROPERTIES IMPORTED_LOCATION "${SPOT_DIR}/lib/libspot.so")
......
//
// Created by ghofrane on 5/4/22.
//
#include "CNDFS.h"
#include <iostream>
using namespace std;
CNDFS::~CNDFS()=default;
void CNDFS::DfsBlue() {
cout << "hello from cndfs class" << endl;
}
\ No newline at end of file
//
// Created by ghofrane on 5/4/22.
//
#ifndef PMC_SOG_CNDFS_H
#define PMC_SOG_CNDFS_H
class CNDFS {
public:
virtual ~CNDFS();
void DfsBlue();
};
#endif //PMC_SOG_CNDFS_H
......@@ -35,6 +35,8 @@
#include "PMCSOGConfig.h"
#include "Hybrid/MCHybridReqPOR/MCHybridSOGReqPOR.h"
#include "Hybrid/MCHybridPOR/MCHybridSOGPOR.h"
#include "algorithm/CNDFS.h"
using namespace std;
......@@ -516,13 +518,12 @@ int main(int argc, char **argv)
if (algorithm == "UFSCC" || algorithm == "CNDFS")
{
cout << "HELLO" << endl;
exit(0);
//runOnTheFlyParallelMC(algorithm);
// auto k = std::make_shared<SogKripkeTh>(d, mcl, Rnewnet.getListTransitionAP(), Rnewnet.getListPlaceAP());
// runOnTheFlyMC("Cou99", k, af);
// cout << mcl->getGraph()->getInitialAggregate()->getSuccessors() <<endl;
// cout << mcl->getGraph()->getInitialAggregate()->isVisited() <<endl;
cout << "HELLO" << endl;
CNDFS n;
n.DfsBlue();
return(0);
//exit(0);
}
else // run on the fly sequential model-checking
{
......@@ -546,8 +547,7 @@ int main(int argc, char **argv)
// TODO: There is no way to run Model-checking when the SOG is built sequentially?
if (nb_th == 1)
{
cout << "\n****************** Sequential version ******************* \n"
<< endl;
cout << "\n****************** Sequential version ******************* \n"<< endl;
// build sequential SOG
DR.computeSeqSOG(g);
......
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