From 3f473401a77985335dd7b3703e619ef3c1e74665 Mon Sep 17 00:00:00 2001 From: abid <chiheb.abid@gmail.com> Date: Mon, 10 Jun 2019 23:15:43 +0100 Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?= =?UTF-8?q?=20src/NewNet.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20?= =?UTF-8?q?=20=20src/SogKripkeIteratorTh.cpp=20=09modifi=C3=A9=C2=A0:=20?= =?UTF-8?q?=20=20=20=20=20=20=20=20src/SogKripkeIteratorTh.h=20=09modifi?= =?UTF-8?q?=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/SogKripkeTh.cpp=20?= =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/SogKripkeT?= =?UTF-8?q?h.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20src/main?= =?UTF-8?q?.cpp?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .kdev4/mc-sog.kdev4 | 19 +++++++++++++++++++ mc-sog.kdev4 | 4 ++++ src/NewNet.h | 4 ++-- src/SogKripkeIteratorTh.cpp | 2 +- src/SogKripkeIteratorTh.h | 4 ++-- src/SogKripkeTh.cpp | 4 ++-- src/SogKripkeTh.h | 4 ++-- src/main.cpp | 2 +- 8 files changed, 33 insertions(+), 10 deletions(-) create mode 100644 .kdev4/mc-sog.kdev4 create mode 100644 mc-sog.kdev4 diff --git a/.kdev4/mc-sog.kdev4 b/.kdev4/mc-sog.kdev4 new file mode 100644 index 0000000..2ed6747 --- /dev/null +++ b/.kdev4/mc-sog.kdev4 @@ -0,0 +1,19 @@ +[Buildset] +BuildItems=@Variant(\x00\x00\x00\t\x00\x00\x00\x00\x01\x00\x00\x00\x0b\x00\x00\x00\x00\x01\x00\x00\x00\x0c\x00m\x00c\x00-\x00s\x00o\x00g) + +[CMake] +Build Directory Count=1 +Current Build Directory Index-Host System=0 + +[CMake][CMake Build Directory 0] +Build Directory Path=/home/chiheb/ProjectCPP/mc-sog/build +Build Type=Debug +CMake Binary=/usr/bin/cmake +CMake Executable=/usr/bin/cmake +Environment Profile= +Extra Arguments= +Install Directory= +Runtime=Host System + +[Project] +VersionControlSupport=kdevgit diff --git a/mc-sog.kdev4 b/mc-sog.kdev4 new file mode 100644 index 0000000..686e1e7 --- /dev/null +++ b/mc-sog.kdev4 @@ -0,0 +1,4 @@ +[Project] +CreatedFrom=CMakeLists.txt +Manager=KDevCMakeManager +Name=mc-sog diff --git a/src/NewNet.h b/src/NewNet.h index a4f2536..10107a0 100644 --- a/src/NewNet.h +++ b/src/NewNet.h @@ -10,8 +10,8 @@ #include <set> #include <string> #include <vector> -#include "RdPMonteur.hpp" -typedef set<int> Set; +#include "RdPMonteur.hpp" +typedef set<int> Set; class Node { public: Node(){}; diff --git a/src/SogKripkeIteratorTh.cpp b/src/SogKripkeIteratorTh.cpp index f28f324..3bde48f 100644 --- a/src/SogKripkeIteratorTh.cpp +++ b/src/SogKripkeIteratorTh.cpp @@ -71,6 +71,6 @@ SogKripkeIteratorTh::~SogKripkeIteratorTh() //dtor } -static ModelCheckerTh * SogKripkeIteratorTh::m_builder; +static ModelCheckBaseMT * SogKripkeIteratorTh::m_builder; static spot::bdd_dict_ptr* SogKripkeIteratorTh::m_dict_ptr; static LDDState SogKripkeIteratorTh::m_deadlock; diff --git a/src/SogKripkeIteratorTh.h b/src/SogKripkeIteratorTh.h index 1a8adc8..774cbd5 100644 --- a/src/SogKripkeIteratorTh.h +++ b/src/SogKripkeIteratorTh.h @@ -1,14 +1,14 @@ #ifndef SOGKRIPKEITERATORTH_H_INCLUDED #define SOGKRIPKEITERATORTH_H_INCLUDED #include "SogKripkeStateTh.h" -#include "ModelCheckerTh.h" +#include "ModelCheckBaseMT.h" #include <spot/kripke/kripke.hh> // Iterator for a SOG graph class SogKripkeIteratorTh : public spot::kripke_succ_iterator { public: static LDDState m_deadlock; - static ModelCheckerTh * m_builder; + static ModelCheckBaseMT * m_builder; static spot::bdd_dict_ptr* m_dict_ptr; // sog_succ_iterator(const RdPBDD& pn, const SogKripkeState& s, const bdd& c); SogKripkeIteratorTh(const LDDState* lddstate, bdd cnd); diff --git a/src/SogKripkeTh.cpp b/src/SogKripkeTh.cpp index f0dbf22..4f2e563 100644 --- a/src/SogKripkeTh.cpp +++ b/src/SogKripkeTh.cpp @@ -10,7 +10,7 @@ #include "SogKripkeTh.h" #include <map> using namespace spot; -SogKripkeTh::SogKripkeTh(const bdd_dict_ptr &dict_ptr,ModelCheckerTh *builder): spot::kripke(dict_ptr),m_builder(builder) +SogKripkeTh::SogKripkeTh(const bdd_dict_ptr &dict_ptr,ModelCheckBaseMT *builder): spot::kripke(dict_ptr),m_builder(builder) { SogKripkeIteratorTh::m_builder=builder; SogKripkeStateTh::m_builder=builder; @@ -18,7 +18,7 @@ SogKripkeTh::SogKripkeTh(const bdd_dict_ptr &dict_ptr,ModelCheckerTh *builder): } -SogKripkeTh::SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckerTh *builder,set<string> &l_transap,set<string> &l_placeap):SogKripkeTh(dict_ptr,builder) { +SogKripkeTh::SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder,set<string> &l_transap,set<string> &l_placeap):SogKripkeTh(dict_ptr,builder) { for (auto it=l_transap.begin();it!=l_transap.end();it++) { register_ap(*it); diff --git a/src/SogKripkeTh.h b/src/SogKripkeTh.h index 4f4a114..81d27eb 100644 --- a/src/SogKripkeTh.h +++ b/src/SogKripkeTh.h @@ -10,8 +10,8 @@ class SogKripkeTh: public spot::kripke { public: - SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckerTh *builder); - SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckerTh *builder,set<string> &l_transap,set<string> &l_placeap); + SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder); + SogKripkeTh(const spot::bdd_dict_ptr& dict_ptr,ModelCheckBaseMT *builder,set<string> &l_transap,set<string> &l_placeap); virtual ~SogKripkeTh(); spot::state* get_init_state() const; SogKripkeIteratorTh* succ_iter(const spot::state* s) const override; diff --git a/src/main.cpp b/src/main.cpp index 89895cf..9857564 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -151,7 +151,7 @@ int main(int argc, char** argv) ModelCheckLace* mcl=new ModelCheckLace(R,bound,nb_th); mcl->loadNet(); auto k = - std::make_shared<SogKripkeOTF>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()); + std::make_shared<SogKripkeTh>(d,mcl,R.getListTransitionAP(),R.getListPlaceAP()); cout<<"Want to save the graph in a dot file ?"; cin>>c; if (c=='y') -- GitLab