From 75328f1a2126d568850b2ad8320c0acb8db1956a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 30 Mar 2015 11:37:32 +0200 Subject: [PATCH] autfilt: add a --simplify-exclusive-ap option * src/bin/autfilt.cc: Add option. * src/ltlvisit/exclusive.cc, src/ltlvisit/exclusive.hh: implement it. * src/tgbatest/exclusive.test: Test it. * src/misc/minato.cc, src/misc/minato.hh: Add an interface to simplify a Boolean function with don't care. --- src/bin/autfilt.cc | 12 ++++++++- src/ltlvisit/exclusive.cc | 32 +++++++++++++++++++----- src/ltlvisit/exclusive.hh | 3 ++- src/misc/minato.cc | 25 ++++++++++++++----- src/misc/minato.hh | 11 ++++++-- src/tgbatest/exclusive.test | 50 +++++++++++++++++++++++++++++++++++-- 6 files changed, 115 insertions(+), 18 deletions(-) diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 837af8132..33d35d632 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -88,6 +88,7 @@ enum { OPT_REM_FIN, OPT_SBACC, OPT_SEED, + OPT_SIMPLIFY_EXCLUSIVE_AP, OPT_STATES, OPT_STRIPACC, OPT_TGBA, @@ -147,6 +148,10 @@ static const argp_option options[] = "ensure two of them may not be true at the same time. Use this option " "multiple times to declare independent groups of exclusive " "propositions.", 0 }, + { "simplify-exclusive-ap", OPT_SIMPLIFY_EXCLUSIVE_AP, 0, 0, + "if --exclusive-ap is used, assume those AP groups are actually exclusive" + " in the system to simplify the expression of transition labels (implies " + "--merge-transitions)", 0 }, { "remove-ap", OPT_REM_AP, "AP[=0|=1][,AP...]", 0, "remove atomic propositions either by existential quantification, or " "by assigning them 0 or 1", 0 }, @@ -239,6 +244,7 @@ static std::vector opt_keep_states = {}; static unsigned int opt_keep_states_initial = 0; static spot::exclusive_ap excl_ap; static spot::remove_ap rem_ap; +static bool opt_simplify_exclusive_ap = false; static int parse_opt(int key, char* arg, struct argp_state*) @@ -403,6 +409,10 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_SEED: opt_seed = to_int(arg); break; + case OPT_SIMPLIFY_EXCLUSIVE_AP: + opt_simplify_exclusive_ap = true; + opt_merge = true; + break; case OPT_STATES: opt_states = parse_range(arg, 0, std::numeric_limits::max()); break; @@ -514,7 +524,7 @@ namespace aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets()); if (!excl_ap.empty()) - aut = excl_ap.constrain(aut); + aut = excl_ap.constrain(aut, opt_simplify_exclusive_ap); if (!rem_ap.empty()) aut = rem_ap.strip(aut); diff --git a/src/ltlvisit/exclusive.cc b/src/ltlvisit/exclusive.cc index 2b9a7e09e..9ca574fc4 100644 --- a/src/ltlvisit/exclusive.cc +++ b/src/ltlvisit/exclusive.cc @@ -24,6 +24,7 @@ #include "ltlast/constant.hh" #include "tgbaalgos/mask.hh" #include "misc/casts.hh" +#include "misc/minato.hh" #include "apcollect.hh" namespace spot @@ -160,7 +161,8 @@ namespace spot return ltl::multop::instance(ltl::multop::And, f->clone(), c); } - tgba_digraph_ptr exclusive_ap::constrain(const_tgba_digraph_ptr aut) const + tgba_digraph_ptr exclusive_ap::constrain(const_tgba_digraph_ptr aut, + bool simplify_guards) const { // Compute the support of the automaton. bdd support = bddtrue; @@ -196,11 +198,29 @@ namespace spot res->copy_ap_of(aut); res->prop_copy(aut, { true, true, true, true }); res->copy_acceptance_of(aut); - transform_accessible(aut, res, [&](unsigned, bdd& cond, - acc_cond::mark_t&, unsigned) - { - cond &= restrict; - }); + if (simplify_guards) + { + transform_accessible(aut, res, [&](unsigned, bdd& cond, + acc_cond::mark_t&, unsigned) + { + minato_isop isop(cond & restrict, + cond | !restrict, + true); + bdd res = bddfalse; + bdd cube = bddfalse; + while ((cube = isop.next()) != bddfalse) + res |= cube; + cond = res; + }); + } + else + { + transform_accessible(aut, res, [&](unsigned, bdd& cond, + acc_cond::mark_t&, unsigned) + { + cond &= restrict; + }); + } return res; } } diff --git a/src/ltlvisit/exclusive.hh b/src/ltlvisit/exclusive.hh index 26ecd81f0..33e1c72c1 100644 --- a/src/ltlvisit/exclusive.hh +++ b/src/ltlvisit/exclusive.hh @@ -42,6 +42,7 @@ namespace spot } const ltl::formula* constrain(const ltl::formula* f) const; - tgba_digraph_ptr constrain(const_tgba_digraph_ptr aut) const; + tgba_digraph_ptr constrain(const_tgba_digraph_ptr aut, + bool simplify_guards = false) const; }; } diff --git a/src/misc/minato.cc b/src/misc/minato.cc index edff46a7e..0d41cce3b 100644 --- a/src/misc/minato.cc +++ b/src/misc/minato.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2009, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -28,8 +28,12 @@ namespace spot { minato_isop::minato_isop(bdd input) - : ret_(bddfalse) + : minato_isop(input, bdd_support(input)) + { + } + minato_isop::minato_isop(bdd input, bdd vars) + : ret_(bddfalse) { // If INPUT has the form a&b&c&(binary function) we want to // compute the ISOP of the only binary and prepend a&b&c latter. @@ -39,14 +43,23 @@ namespace spot // original algorithm, because in many cases we are trying to // build ISOPs out of formulae that are already cubes. cube_.push(bdd_satprefix(input)); - todo_.emplace(input, input, bdd_support(input)); + todo_.emplace(input, input, vars); } - minato_isop::minato_isop(bdd input, bdd vars) + minato_isop::minato_isop(bdd input_min, bdd input_max, bool) : ret_(bddfalse) { - cube_.push(bdd_satprefix(input)); - todo_.emplace(input, input, vars); + if (input_min == input_max) + { + cube_.push(bdd_satprefix(input_min)); + input_max = input_min; + } + else + { + cube_.push(bddtrue); + } + bdd common = input_min & input_max; + todo_.emplace(input_min, input_max, bdd_support(common)); } bdd diff --git a/src/misc/minato.hh b/src/misc/minato.hh index 9d80fcba5..67e6b85fd 100644 --- a/src/misc/minato.hh +++ b/src/misc/minato.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2013, 2014 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2009, 2013, 2014, 2015 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -58,6 +58,13 @@ namespace spot /// \arg input The BDD function to translate in ISOP. /// \arg vars The set of BDD variables to factorize in \a input. minato_isop(bdd input, bdd vars); + /// \brief Conctructor. + /// + /// This version allow some flexibility in computing the ISOP. + /// the result must be within \a input_min and \a input_max. + /// \arg input_min The minimum BDD function to translate in ISOP. + /// \arg input_max The maximum BDD function to translate in ISOP. + minato_isop(bdd input_min, bdd input_max, bool); /// \brief Compute the next sum term of the ISOP form. /// Return \c bddfalse when all terms have been output. bdd next(); diff --git a/src/tgbatest/exclusive.test b/src/tgbatest/exclusive.test index faf9b80a2..8d6c87110 100755 --- a/src/tgbatest/exclusive.test +++ b/src/tgbatest/exclusive.test @@ -35,7 +35,7 @@ State: 0 [0] 1 State: 1 [1] 2 -[2] 2 +[2&!1] 2 State: 2 {0} [1] 2 [0&1] 1 @@ -64,11 +64,34 @@ State: 2 {0} --END-- EOF +cat >expected-simpl <out cat out diff out expected +run 0 ../../bin/autfilt -H --exclusive-ap=a,b,c --exclusive-ap=d,e \ + --simplify-exclusive-ap automaton >out2 +cat out2 +diff out2 expected-simpl + cat >automaton <expected-simpl <out cat out diff out expected + +run 0 ../../bin/autfilt -H --exclusive-ap=a,b,c --exclusive-ap=d,e \ + --simplify-exclusive-ap automaton >out2 +cat out2 +diff out2 expected-simpl