diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 59aa408cd..3807244c4 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -43,6 +43,7 @@ #include "misc/timer.hh" #include "misc/random.hh" #include "hoaparse/public.hh" +#include "ltlvisit/exclusive.hh" #include "tgbaalgos/randomize.hh" #include "tgbaalgos/are_isomorphic.hh" #include "tgbaalgos/canonicalize.hh" @@ -71,6 +72,7 @@ enum { OPT_DESTUT, OPT_DNF_ACC, OPT_EDGES, + OPT_EXCLUSIVE_AP, OPT_INSTUT, OPT_INTERSECT, OPT_IS_COMPLETE, @@ -138,6 +140,11 @@ static const argp_option options[] = { "complement-acceptance", OPT_COMPLEMENT_ACC, 0, 0, "complement the acceptance condition (without touching the automaton)", 0 }, + { "exclusive-ap", OPT_EXCLUSIVE_AP, "AP,AP,...", 0, + "if any of those APs occur in the automaton, restrict all edges to " + "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 }, /**************************************************/ { 0, 0, 0, 0, "Filtering options:", 6 }, { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0, @@ -225,6 +232,7 @@ static bool opt_complement_acc = false; static spot::acc_cond::mark_t opt_mask_acc = 0U; static std::vector opt_keep_states = {}; static unsigned int opt_keep_states_initial = 0; +static spot::exclusive_ap excl_ap; static int parse_opt(int key, char* arg, struct argp_state*) @@ -287,6 +295,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_EDGES: opt_edges = parse_range(arg, 0, std::numeric_limits::max()); break; + case OPT_EXCLUSIVE_AP: + excl_ap.add_group(arg); + break; case OPT_INSTUT: if (!arg || (arg[0] == '1' && arg[1] == 0)) opt_instut = 1; @@ -490,6 +501,9 @@ namespace if (opt_mask_acc) aut = mask_acc_sets(aut, opt_mask_acc & aut->acc().all_sets()); + if (!excl_ap.empty()) + aut = excl_ap.constrain(aut); + if (opt_destut) aut = spot::closure(std::move(aut)); if (opt_instut == 1) diff --git a/src/ltlvisit/exclusive.cc b/src/ltlvisit/exclusive.cc index 857480863..2b9a7e09e 100644 --- a/src/ltlvisit/exclusive.cc +++ b/src/ltlvisit/exclusive.cc @@ -22,6 +22,7 @@ #include "ltlast/multop.hh" #include "ltlast/unop.hh" #include "ltlast/constant.hh" +#include "tgbaalgos/mask.hh" #include "misc/casts.hh" #include "apcollect.hh" @@ -158,4 +159,48 @@ namespace spot ltl::multop::instance(ltl::multop::And, v)); return ltl::multop::instance(ltl::multop::And, f->clone(), c); } + + tgba_digraph_ptr exclusive_ap::constrain(const_tgba_digraph_ptr aut) const + { + // Compute the support of the automaton. + bdd support = bddtrue; + { + std::set bdd_seen; + for (auto& t: aut->transitions()) + if (bdd_seen.insert(t.cond.id()).second) + support &= bdd_support(t.cond); + } + + bdd restrict = bddtrue; + auto d = aut->get_dict(); + + std::vector group; + for (auto& g: groups) + { + group.clear(); + + for (auto ap: g) + { + int v = d->has_registered_proposition(ap, aut); + if (v >= 0) + group.push_back(bdd_nithvar(v)); + } + + unsigned s = group.size(); + for (unsigned j = 0; j < s; ++j) + for (unsigned k = j + 1; k < s; ++k) + restrict &= group[j] | group[k]; + } + + tgba_digraph_ptr res = make_tgba_digraph(aut->get_dict()); + 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; + }); + return res; + } } diff --git a/src/ltlvisit/exclusive.hh b/src/ltlvisit/exclusive.hh index cd9d20ff6..26ecd81f0 100644 --- a/src/ltlvisit/exclusive.hh +++ b/src/ltlvisit/exclusive.hh @@ -22,6 +22,7 @@ #include #include "ltlast/atomic_prop.hh" #include "ltlast/formula.hh" +#include "tgba/tgbagraph.hh" namespace spot { @@ -41,5 +42,6 @@ namespace spot } const ltl::formula* constrain(const ltl::formula* f) const; + tgba_digraph_ptr constrain(const_tgba_digraph_ptr aut) const; }; } diff --git a/src/tgba/bdddict.cc b/src/tgba/bdddict.cc index 61c1abc23..321d8f42f 100644 --- a/src/tgba/bdddict.cc +++ b/src/tgba/bdddict.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2012, 2013, 2014 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2012, 2013, 2014, 2015 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -118,6 +118,20 @@ namespace spot return num; } + int + bdd_dict::has_registered_proposition(const ltl::formula* f, + const void* me) + { + auto ssi = var_map.find(f); + if (ssi == var_map.end()) + return -1; + int num = ssi->second; + auto& r = bdd_map[num].refs; + if (r.find(me) == r.end()) + return -1; + return num; + } + void bdd_dict::register_propositions(bdd f, const void* for_me) { diff --git a/src/tgba/bdddict.hh b/src/tgba/bdddict.hh index f9e7faf28..eea37dfd9 100644 --- a/src/tgba/bdddict.hh +++ b/src/tgba/bdddict.hh @@ -1,9 +1,9 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre -// et Marie Curie. +// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). +// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris +// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -126,7 +126,23 @@ namespace spot } /// @} - /// \brief Register an atomic proposition. + /// \brief whether a proposition has already been registered + /// + /// If \a f has been registered for \a me, this returns + /// a non-negative value that is the BDD variable number. + /// Otherwise this returns -1. + /// @{ + int has_registered_proposition(const ltl::formula* f, + const void* me); + template + int has_registered_proposition(const ltl::formula* f, + std::shared_ptr for_me) + { + return has_registered_proposition(f, for_me.get()); + } + /// @} + + /// \brief Register an acceptance variable. /// /// Return (and maybe allocate) a BDD variable designating an /// acceptance set associated to formula \a f. The \a for_me diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 37ebe2f86..41b734ad6 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -91,6 +91,7 @@ TESTS = \ explpro4.test \ tripprod.test \ dupexp.test \ + exclusive.test \ degendet.test \ degenid.test \ degenlskip.test \ diff --git a/src/tgbatest/exclusive.test b/src/tgbatest/exclusive.test new file mode 100755 index 000000000..faf9b80a2 --- /dev/null +++ b/src/tgbatest/exclusive.test @@ -0,0 +1,116 @@ +#! /bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2015 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + + +. ./defs || exit 1 + +set -e + +cat >automaton <expected <out +cat out +diff out expected + +cat >automaton <expected <out +cat out +diff out expected