From e5090c162eaaf10aec40b684e5e6047723fa78ca Mon Sep 17 00:00:00 2001 From: abid <chiheb.abid@gmail.com> Date: Sat, 22 Jan 2022 20:40:35 +0100 Subject: [PATCH] Correct SykvanWrapper::isFirable --- src/CommonSOG.h | 2 -- src/SylvanWrapper.cpp | 9 +++++---- src/main.cpp | 18 +++++++++--------- 3 files changed, 14 insertions(+), 15 deletions(-) diff --git a/src/CommonSOG.h b/src/CommonSOG.h index 05160f8..6240857 100644 --- a/src/CommonSOG.h +++ b/src/CommonSOG.h @@ -43,9 +43,7 @@ public: virtual void computeDSOG(LDDGraph &g) {}; protected: void initializeLDD(); - void loadNetFromFile(); - const NewNet *m_net; int m_nbPlaces = 0; static LDDGraph *m_graph; diff --git a/src/SylvanWrapper.cpp b/src/SylvanWrapper.cpp index 4bfe6fb..cfdbff6 100644 --- a/src/SylvanWrapper.cpp +++ b/src/SylvanWrapper.cpp @@ -815,16 +815,17 @@ bool SylvanWrapper::isFirable(MDD cmark, MDD minus) { MDD _cmark = cmark, _minus = minus; mddnode_t n_cmark = GETNODE(_cmark); mddnode_t n_minus = GETNODE(_minus); + std::cout<<(int)mddnode_getvalue(n_cmark)<<" \n"; while (!result) { uint32_t value; value = mddnode_getvalue(n_cmark); uint32_t value_minus = mddnode_getvalue(n_minus); if (value >= value_minus) { - mddnode_t node_mark=mddnode_getdown(n_cmark); - if (node_mark==lddmc_true) return true; - mddnode_t node_minus=mddnode_getdown(n_minus); - result=isFirable(node_mark, mddnode_getdown(node_minus)); + MDD _mark=mddnode_getdown(n_cmark); + if (_mark==lddmc_true) return true; + MDD _minus=mddnode_getdown(n_minus); + result=isFirable(_mark, _minus); } cmark = mddnode_getright(n_cmark); if (cmark == lddmc_false || result) return result; diff --git a/src/main.cpp b/src/main.cpp index 39da26a..dca1501 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -1,4 +1,4 @@ -#include <time.h> +#include <ctime> #include <chrono> #include <iostream> #include <string> @@ -62,9 +62,9 @@ set<string> buildPropositions(const string &fileName) { std::cerr << "Only LTL formulas are supported.\n"; return transitionSet; } - spot::atomic_prop_set *p_list = spot::atomic_prop_collect(fo, 0); - for (spot::atomic_prop_set::const_iterator i = p_list->begin(); i != p_list->end(); i++) { - transitionSet.insert((*i).ap_name()); + spot::atomic_prop_set *p_list = spot::atomic_prop_collect(fo, nullptr); + for (const auto i : *p_list) { + transitionSet.insert(i.ap_name()); } print_spin_ltl(std::cout, fo) << '\n'; cout << "Building formula negation\n"; @@ -84,7 +84,7 @@ void displayTime(auto startTime,auto finalTime) { } /***********************************************/ int main(int argc, char **argv) { - int choix; + if (argc < 3) return 0; char formula[100] = ""; @@ -159,14 +159,14 @@ int main(int argc, char **argv) { } auto startTime = std::chrono::steady_clock::now(); spot::emptiness_check_ptr echptr = echeck_inst->instantiate(product); - bool res = (echptr->check() == 0); + bool res = (echptr->check() == nullptr); auto finalTime = std::chrono::steady_clock::now(); displayTime(startTime, finalTime); displayCheckResult(res); } else { auto startTime = std::chrono::steady_clock::now(); - bool res = (k->intersecting_run(af) == 0); + bool res = (k->intersecting_run(af) == nullptr); auto finalTime = std::chrono::steady_clock::now(); displayTime(startTime, finalTime); displayCheckResult(res); @@ -304,13 +304,13 @@ int main(int argc, char **argv) { cout<<"Spot emptiness check algorithm : "<<algorithm<<endl; auto startTime = std::chrono::high_resolution_clock::now(); spot::emptiness_check_ptr echptr = echeck_inst->instantiate(product); - bool res = (echptr->check() == 0); + bool res = (echptr->check() == nullptr); auto finalTime = std::chrono::high_resolution_clock::now(); displayTime(startTime, finalTime); displayCheckResult(res); } else { auto startTime = std::chrono::steady_clock::now(); - bool res = (k->intersecting_run(af) == 0); + bool res = (k->intersecting_run(af) == nullptr); auto finalTime = std::chrono::steady_clock::now(); displayTime(startTime, finalTime); displayCheckResult(res); -- GitLab