diff --git a/CMakeLists.txt b/CMakeLists.txt index 3ef9451ac2d242247209c3333f98f0fb5e1468b3..d8507aa14d437c493b8a91ab0500eb7fecfcb238 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -12,7 +12,7 @@ set(CMAKE_CXX_EXTENSIONS OFF) # Add compiler flags if(CMAKE_COMPILER_IS_GNUCC) - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -g0 -falign-functions -falign-jumps -falign-loops -falign-labels -freorder-blocks -freorder-blocks-algorithm=stc -freorder-blocks-and-partition -fprefetch-loop-arrays -foptimize-strlen -fcaller-saves -finline-functions -funswitch-loops -fpermissive -std=c++17 -pthread") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fpermissive -std=c++17 -pthread -Og ") endif() diff --git a/src/CommonSOG.cpp b/src/CommonSOG.cpp index ab4d06272728f247044e57508af44fe67941f70e..45c52184139a1fcd9952807007f0389eb934417a 100644 --- a/src/CommonSOG.cpp +++ b/src/CommonSOG.cpp @@ -27,7 +27,7 @@ MDD CommonSOG::Accessible_epsilon(MDD From) { M1 = M2; for (Set::const_iterator i = m_nonObservable.begin(); !(i == m_nonObservable.end()); i++) { //fireTransition - MDD succ = fireTransition(M2, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus()); + MDD succ = SylvanWrapper::lddmc_firing_mono(M2, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus()); M2 = SylvanWrapper::lddmc_union_mono(M2, succ); @@ -42,7 +42,7 @@ Set CommonSOG::firable_obs(MDD State) { Set res; for (Set::const_iterator i = m_observable.begin(); !(i == m_observable.end()); i++) { //cout<<"firable..."<<endl; - MDD succ = fireTransition(State, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus()); + MDD succ = SylvanWrapper::lddmc_firing_mono(State, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus()); if (succ != lddmc_false) { res.insert(*i); } @@ -52,14 +52,14 @@ Set CommonSOG::firable_obs(MDD State) { } MDD CommonSOG::get_successor(MDD From, int t) { - return fireTransition(From, m_tb_relation[(t)].getMinus(), m_tb_relation[(t)].getPlus()); + return SylvanWrapper::lddmc_firing_mono(From, m_tb_relation[(t)].getMinus(), m_tb_relation[(t)].getPlus()); } MDD CommonSOG::ImageForward(MDD From) { MDD Res = lddmc_false; for (Set::const_iterator i = m_nonObservable.begin(); !(i == m_nonObservable.end()); i++) { - MDD succ = fireTransition(From, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus()); + MDD succ = SylvanWrapper::lddmc_firing_mono(From, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus()); Res = SylvanWrapper::lddmc_union_mono(Res, succ); } return Res; @@ -173,7 +173,7 @@ bool CommonSOG::Set_Div(MDD &M) const { do { Reached = lddmc_false; for (i = m_nonObservable.begin(); !(i == m_nonObservable.end()); i++) { - MDD To = fireTransition(From, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus()); + MDD To = SylvanWrapper::lddmc_firing_mono(From, m_tb_relation[(*i)].getMinus(), m_tb_relation[(*i)].getPlus()); Reached = SylvanWrapper::lddmc_union_mono(Reached, To); } @@ -213,9 +213,9 @@ struct elt_t { uint32_t level; }; -MDD CommonSOG::fireTransition(MDD cmark, MDD minus, MDD plus) { +/*MDD CommonSOG::fireTransition(MDD cmark, MDD minus, MDD plus) { return SylvanWrapper::lddmc_firing_mono(cmark,minus,plus); -} +}*/ //string_view CommonSOG::getTransition(int pos) { // cout<<"yes it is : "<<m_transitions.at(pos).name<<endl; diff --git a/src/CommonSOG.h b/src/CommonSOG.h index 5f6f7e166a4e6247d32bba1565d0f2f2fc905c5a..1598c5b00382111ba9032432e4e7e87f6b25f866 100644 --- a/src/CommonSOG.h +++ b/src/CommonSOG.h @@ -60,7 +60,7 @@ class CommonSOG uint8_t m_nb_thread; std::mutex m_graph_mutex,m_gc_mutex; atomic<uint8_t> m_gc; - MDD fireTransition(MDD cmark,MDD minus, MDD plus); + //MDD fireTransition(MDD cmark,MDD minus, MDD plus); private: };