From c317154df41f33f3cf09ff4d570fd2601b9ed9c6 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 21 Nov 2003 10:58:44 +0000 Subject: [PATCH] * src/misc/minato.cc, src/misc/minato.hh: New files. * src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them. * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Use minato_isop. --- ChangeLog | 6 ++ src/misc/Makefile.am | 2 + src/misc/minato.cc | 109 +++++++++++++++++++++++++++++++++++ src/misc/minato.hh | 65 +++++++++++++++++++++ src/tgbaalgos/ltl2tgba_fm.cc | 13 ++--- 5 files changed, 186 insertions(+), 9 deletions(-) create mode 100644 src/misc/minato.cc create mode 100644 src/misc/minato.hh diff --git a/ChangeLog b/ChangeLog index 873364840..df16bb16a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,9 @@ +2003-11-21 Alexandre Duret-Lutz + + * src/misc/minato.cc, src/misc/minato.hh: New files. + * src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them. + * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Use minato_isop. + 2003-11-14 Alexandre Duret-Lutz * src/ltltest/Makefile.am (AM_CXXFLAGS): New variable. diff --git a/src/misc/Makefile.am b/src/misc/Makefile.am index 8f39b4a9b..1ba35fc24 100644 --- a/src/misc/Makefile.am +++ b/src/misc/Makefile.am @@ -7,9 +7,11 @@ misc_HEADERS = \ bddalloc.hh \ bddlt.hh \ hash.hh \ + minato.hh \ version.hh noinst_LTLIBRARIES = libmisc.la libmisc_la_SOURCES = \ bddalloc.cc \ + minato.cc \ version.cc diff --git a/src/misc/minato.cc b/src/misc/minato.cc new file mode 100644 index 000000000..a532765d2 --- /dev/null +++ b/src/misc/minato.cc @@ -0,0 +1,109 @@ +#include "minato.hh" +#include + +namespace spot +{ + + minato_isop::minato_isop(bdd input) + : ret(bddfalse) + { + todo.push(local_vars(input, input)); + cube.push(bddtrue); + } + + bdd + minato_isop::next() + { + while (todo.size()) + { + local_vars& l = todo.top(); + switch (l.step) + { + case local_vars::FirstStep: + if (l.f_min == bddfalse) + { + ret = bddfalse; + todo.pop(); + continue; + } + if (l.f_max == bddtrue) + { + ret = bddtrue; + todo.pop(); + return cube.top(); + } + l.step = local_vars::SecondStep; + + { + // Pick the topmost variable. + int v_min = bdd_var(l.f_min); + int v_max = bdd_var(l.f_max); + int v = std::min(v_min, v_max); + + // The following two `if's do + // v0 = bdd_nithvar(v); + // v1 = bdd_ithvar(v); + // f0_min = bdd_restrict(f_min, v0); + // f0_max = bdd_restrict(f_max, v0); + // f1_min = bdd_restrict(f_min, v1); + // f1_max = bdd_restrict(f_max, v1); + // but since we now the v is the topmost variable, + // its more efficient to use bdd_low and bdd_high. + if (v == v_min) + { + l.f0_min = bdd_low(l.f_min); + l.f1_min = bdd_high(l.f_min); + } + else + { + l.f1_min = l.f0_min = l.f_min; + } + if (v == v_max) + { + l.f0_max = bdd_low(l.f_max); + l.f1_max = bdd_high(l.f_max); + } + else + { + l.f1_max = l.f0_max = l.f_max; + } + + l.v1 = bdd_ithvar(v); + cube.push(cube.top() & bdd_nithvar(v)); + todo.push(local_vars(l.f0_min - l.f1_max, l.f0_max)); + } + continue; + + case local_vars::SecondStep: + l.step = local_vars::ThirdStep; + l.g0 = ret; + cube.pop(); + cube.push(cube.top() & l.v1); + todo.push(local_vars(l.f1_min - l.f0_max, l.f1_max)); + continue; + + case local_vars::ThirdStep: + l.step = local_vars::FourthStep; + l.g1 = ret; + cube.pop(); + { + bdd f0s_min = l.f0_min - l.g0; + bdd f1s_min = l.f1_min - l.g1; + bdd fs_max = l.f0_max & l.f1_max; + bdd fs_min = fs_max & (f0s_min | f1s_min); + todo.push(local_vars(fs_min, fs_max)); + } + continue; + + case local_vars::FourthStep: + ret |= (l.g0 - l.v1) | (l.g1 & l.v1); + todo.pop(); + continue; + } + // Unreachable code. + assert(0); + } + return bddfalse; + } + +} diff --git a/src/misc/minato.hh b/src/misc/minato.hh new file mode 100644 index 000000000..1f7a1626d --- /dev/null +++ b/src/misc/minato.hh @@ -0,0 +1,65 @@ +#ifndef SPOT_MISC_MINATO_HH +# define SPOT_MISC_MINATO_HH + +# include +# include + +namespace spot +{ + /// \brief Generate an irredundant sum-of-products (ISOP) form of a + /// BDD function. + /// + /// This algorithm implements a derecursived version the Minato-Morreale + /// algorithm presented in the following paper. + /// \verbatim + /// @InProceedings{ minato.92.sasimi, + /// author = {Shin-ichi Minato}, + /// title = {Fast Generation of Irredundant Sum-of-Products Forms + /// from Binary Decision Diagrams}, + /// booktitle = {Proceedings of the third Synthesis and Simulation + /// and Meeting International Interchange workshop + /// (SASIMI'92)}, + /// pages = {64--73}, + /// year = {1992}, + /// address = {Kobe, Japan}, + /// month = {April} + /// } + /// \endverbatim + class minato_isop + { + public: + /// \brief Conctructor. + /// \arg input The BDD function to translate in ISOP. + minato_isop(bdd input); + /// \brief Compute the next sum term of the ISOP form. + /// Return \c bddfalse when all terms have been output. + bdd next(); + + private: + /// Internal variables for minato_isop. + struct local_vars + { + // If you are following the paper, f_min and f_max corresponds + // to the pair of BDD function used to encode the ternary function `f' + // (see Section 3.4). + // Also note that f0, f0', and f0'' all share the same _max function. + // Likewise for f1, f1', and f1''. + bdd f_min, f_max; + // Because we need a non-recursive version of the algorithm, + // we had to split it in four step (each step is separated + // from the other by a call to ISOP in the original algorithm). + enum { FirstStep, SecondStep, ThirdStep, FourthStep } step; + bdd v1; + bdd f0_min, f0_max; + bdd f1_min, f1_max; + bdd g0, g1; + local_vars(bdd f_min, bdd f_max) + : f_min(f_min), f_max(f_max), step(FirstStep) {} + }; + std::stack todo; + std::stack cube; + bdd ret; + }; +} + +#endif // SPOT_MISC_MINATO_HH diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index b5d86b864..5e9a84224 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -1,5 +1,6 @@ #include "misc/hash.hh" #include "misc/bddalloc.hh" +#include "misc/minato.hh" #include "ltlast/visitor.hh" #include "ltlast/allnodes.hh" #include "ltlvisit/lunabbrev.hh" @@ -440,15 +441,10 @@ namespace spot std::string now = to_string(f); - bdd all = res; - bdd outside = !all; - while (all != bddfalse) + minato_isop isop(res); + bdd cube; + while ((cube = isop.next()) != bddfalse) { - - bdd cube = bdd_satone(all); - cube = bdd_simplify(cube, cube | outside); - all -= cube; - ltl::formula* dest = d.conj_bdd_to_formula(bdd_existcomp(cube, d.next_set)); @@ -459,7 +455,6 @@ namespace spot d.conj_bdd_to_atomic_props(a, bdd_existcomp(cube, d.var_set), t); d.conj_bdd_to_acc(a, bdd_existcomp(cube, d.a_set), t); - if (formulae_seen.find(dest) == formulae_seen.end()) { formulae_seen.insert(dest);