From 14bee1ae7f6c96cd0233df0ae7894dd39c8efaf5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 4 Aug 2016 22:24:30 +0200 Subject: [PATCH] implement conversion to GRA and GSA Fixes #174. * spot/twaalgos/totgba.hh, spot/twaalgos/totgba.cc (to_generalized_streett, to_generalized_rabin): New functions. * spot/twa/acc.hh: Declare more methods as static. * bin/autfilt.cc: Implement --generalized-rabin and --generalized-streett options. * NEWS: Mention these. * tests/core/gragsa.test: New file. * tests/Makefile.am: Add it. --- NEWS | 7 ++ bin/autfilt.cc | 63 ++++++++++++- spot/twa/acc.hh | 16 ++-- spot/twaalgos/totgba.cc | 201 +++++++++++++++++++++++++++++++++++++++- spot/twaalgos/totgba.hh | 30 +++++- tests/Makefile.am | 1 + tests/core/gragsa.test | 31 +++++++ 7 files changed, 338 insertions(+), 11 deletions(-) create mode 100755 tests/core/gragsa.test diff --git a/NEWS b/NEWS index 72e459f4e..fe5b95a08 100644 --- a/NEWS +++ b/NEWS @@ -82,6 +82,9 @@ New in spot 2.0.3a (not yet released) --highlight-word=[NUM,]WORD option. However currently this only work on automata with Fin-less acceptance. + * autfilt learned two options --generalized-rabin and + --generalized-streett to convert the acceptance conditions. + * genltl learned three new families: --dac-patterns=1..45, --eh-patterns=1..12, and --sb-patterns=1..27. Unlike other options these do not output scalable patterns, but simply a list of formulas @@ -127,6 +130,10 @@ New in spot 2.0.3a (not yet released) and pushing acceptance marks common to all incoming edges) to reduce the number of additional states needed. + * to_generalized_rabin() and to_generalized_streett() are two new + functions that convert the acceptance condition as requested + without changing the transition structure. + * language_containment_checker now has default values for all parameters of its constructor. diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 691c265ed..6435d68ef 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -27,6 +27,7 @@ #include #include "error.h" +#include "argmatch.h" #include "common_setup.hh" #include "common_finput.hh" @@ -62,6 +63,7 @@ #include #include #include +#include static const char argp_program_doc[] ="\ Convert, transform, and filter omega-automata.\v\ @@ -88,7 +90,8 @@ enum { OPT_EDGES, OPT_EQUIVALENT_TO, OPT_EXCLUSIVE_AP, - OPT_GENERIC, + OPT_GENERALIZED_RABIN, + OPT_GENERALIZED_STREETT, OPT_HIGHLIGHT_NONDET, OPT_HIGHLIGHT_NONDET_EDGES, OPT_HIGHLIGHT_NONDET_STATES, @@ -252,6 +255,20 @@ static const argp_option options[] = "put the acceptance condition in Conjunctive Normal Form", 0 }, { "remove-fin", OPT_REM_FIN, nullptr, 0, "rewrite the automaton without using Fin acceptance", 0 }, + { "generalized-rabin", OPT_GENERALIZED_RABIN, + "unique-inf|share-inf", OPTION_ARG_OPTIONAL, + "rewrite the acceptance condition as generalized Rabin; the default " + "\"unique-inf\" option uses the generalized Rabin definition from the " + "HOA format; the \"share-inf\" option allows clauses to share Inf sets, " + "therefore reducing the number of sets", 0 }, + { "gra", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, + { "generalized-streett", OPT_GENERALIZED_STREETT, + "unique-fin|share-fin", OPTION_ARG_OPTIONAL, + "rewrite the acceptance condition as generalized Streett;" + " the \"share-fin\" option allows clauses to share Fin sets," + " therefore reducing the number of sets; the default" + " \"unique-fin\" does not", 0 }, + { "gsa", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, { "cleanup-acceptance", OPT_CLEAN_ACC, nullptr, 0, "remove unused acceptance sets from the automaton", 0 }, { "complement", OPT_COMPLEMENT, nullptr, 0, @@ -329,6 +346,7 @@ static const struct argp_child children[] = { nullptr, 0, nullptr, 0 } }; + typedef spot::twa_graph::graph_t::edge_storage_t tr_t; typedef std::set> unique_aut_t; static long int match_count = 0; @@ -337,6 +355,30 @@ static bool randomize_st = false; static bool randomize_tr = false; static int opt_seed = 0; +enum gra_type { GRA_NO = 0, GRA_SHARE_INF = 1, GRA_UNIQUE_INF = 2 }; +static gra_type opt_gra = GRA_NO; +static char const *const gra_args[] = +{ + "default", "share-inf", "hoa", "unique-inf", nullptr +}; +static gra_type const gra_types[] = +{ + GRA_UNIQUE_INF, GRA_SHARE_INF, GRA_UNIQUE_INF, GRA_UNIQUE_INF +}; +ARGMATCH_VERIFY(gra_args, gra_types); + +enum gsa_type { GSA_NO = 0, GSA_SHARE_FIN = 1, GSA_UNIQUE_FIN = 2 }; +static gsa_type opt_gsa = GSA_NO; +static char const *const gsa_args[] = +{ + "default", "share-fin", "unique-fin", nullptr +}; +static gsa_type const gsa_types[] = +{ + GSA_UNIQUE_FIN, GSA_SHARE_FIN, GSA_UNIQUE_FIN +}; +ARGMATCH_VERIFY(gsa_args, gsa_types); + // We want all these variables to be destroyed when we exit main, to // make sure it happens before all other global variables (like the // atomic propositions maps) are destroyed. Otherwise we risk @@ -517,6 +559,20 @@ parse_opt(int key, char* arg, struct argp_state*) opt->equivalent_neg = spot::dtwa_complement(ensure_deterministic(opt->equivalent_pos)); break; + case OPT_GENERALIZED_RABIN: + if (arg) + opt_gra = XARGMATCH("--generalized-rabin", arg, gra_args, gra_types); + else + opt_gra = GRA_UNIQUE_INF; + opt_gsa = GSA_NO; + break; + case OPT_GENERALIZED_STREETT: + if (arg) + opt_gsa = XARGMATCH("--generalized-streett", arg, gsa_args, gsa_types); + else + opt_gsa = GSA_UNIQUE_FIN; + opt_gra = GRA_NO; + break; case OPT_HIGHLIGHT_NONDET: { int v = arg ? to_pos_int(arg) : 1; @@ -1013,6 +1069,11 @@ namespace aut = post.run(aut, nullptr); + if (opt_gra) + aut = spot::to_generalized_rabin(aut, opt_gra == GRA_SHARE_INF); + if (opt_gsa) + aut = spot::to_generalized_streett(aut, opt_gsa == GSA_SHARE_FIN); + if (opt_simplify_exclusive_ap && !opt->excl_ap.empty()) aut = opt->excl_ap.constrain(aut, true); else if (opt_rem_unused_ap) // constrain(aut, true) already does that diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 842a8d7c7..256132ece 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -1056,42 +1056,42 @@ namespace spot bool check_fin_acceptance() const; public: - acc_code inf(mark_t mark) const + static acc_code inf(mark_t mark) { return acc_code::inf(mark); } - acc_code inf(std::initializer_list vals) const + static acc_code inf(std::initializer_list vals) { return inf(mark_t(vals.begin(), vals.end())); } - acc_code inf_neg(mark_t mark) const + static acc_code inf_neg(mark_t mark) { return acc_code::inf_neg(mark); } - acc_code inf_neg(std::initializer_list vals) const + static acc_code inf_neg(std::initializer_list vals) { return inf_neg(mark_t(vals.begin(), vals.end())); } - acc_code fin(mark_t mark) const + static acc_code fin(mark_t mark) { return acc_code::fin(mark); } - acc_code fin(std::initializer_list vals) const + static acc_code fin(std::initializer_list vals) { return fin(mark_t(vals.begin(), vals.end())); } - acc_code fin_neg(mark_t mark) const + static acc_code fin_neg(mark_t mark) { return acc_code::fin_neg(mark); } - acc_code fin_neg(std::initializer_list vals) const + static acc_code fin_neg(std::initializer_list vals) { return fin_neg(mark_t(vals.begin(), vals.end())); } diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index 73eff8da4..c4c2bc5d0 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -329,7 +329,7 @@ namespace spot // Handle false specifically. We want the output // an automaton with Acceptance: t, that has a single // state without successor. - if (cnf.size() == 2 && cnf.back().op == acc_cond::acc_op::Fin) + if (cnf.is_f()) { assert(cnf.front().mark == 0U); res = make_twa_graph(aut->get_dict()); @@ -357,4 +357,203 @@ namespace spot } return res; } + + namespace + { + // If the DNF is + // Fin(1)&Inf(2)&Inf(4) | Fin(2)&Fin(3)&Inf(1) | + // Inf(1)&Inf(3) | Inf(1)&Inf(2) | Fin(4) + // this returns the following vector of pairs: + // [({1}, {2,4}) + // ({2,3}, {1}), + // ({}, {1,3}), + // ({}, {2}), + // ({4}, t)] + static std::vector> + split_dnf_acc(const acc_cond::acc_code& acc) + { + std::vector> res; + if (acc.empty()) + { + res.emplace_back(0U, 0U); + return res; + } + auto pos = &acc.back(); + if (pos->op == acc_cond::acc_op::Or) + --pos; + auto start = &acc.front(); + while (pos > start) + { + if (pos->op == acc_cond::acc_op::Fin) + { + // We have only a Fin term, without Inf. In this case + // only, the Fin() may encode a disjunction of sets. + for (auto s: pos[-1].mark.sets()) + res.emplace_back(acc_cond::mark_t({s}), 0U); + pos -= pos->size + 1; + } + else + { + // We have a conjunction of Fin and Inf sets. + auto end = pos - pos->size - 1; + acc_cond::mark_t fin = 0U; + acc_cond::mark_t inf = 0U; + while (pos > end) + { + switch (pos->op) + { + case acc_cond::acc_op::And: + --pos; + break; + case acc_cond::acc_op::Fin: + fin |= pos[-1].mark; + assert(pos[-1].mark.count() == 1); + pos -= 2; + break; + case acc_cond::acc_op::Inf: + inf |= pos[-1].mark; + pos -= 2; + break; + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::InfNeg: + case acc_cond::acc_op::Or: + SPOT_UNREACHABLE(); + break; + } + } + assert(pos == end); + res.emplace_back(fin, inf); + } + } + return res; + } + + + static twa_graph_ptr + to_generalized_rabin_aux(const const_twa_graph_ptr& aut, + bool share_inf, bool complement) + { + auto res = cleanup_acceptance(aut); + auto oldacc = res->get_acceptance(); + if (complement) + res->set_acceptance(res->acc().num_sets(), oldacc.complement()); + + { + std::vector pairs; + if (res->acc().is_generalized_rabin(pairs)) + { + if (complement) + res->set_acceptance(res->acc().num_sets(), oldacc); + return res; + } + } + auto dnf = res->get_acceptance().to_dnf(); + if (dnf.is_f()) + { + if (complement) + res->set_acceptance(0, acc_cond::acc_code::t()); + return res; + } + + auto v = split_dnf_acc(dnf); + + // Decide how we will rename each input set. + // + // inf_rename is only used if hoa_style=false, to + // reuse previously used Inf sets. + + unsigned ns = res->num_sets(); + std::vector rename(ns); + std::vector inf_rename(ns); + + unsigned next_set = 0; + // The output acceptance conditions. + acc_cond::acc_code code = + complement ? acc_cond::acc_code::t() : acc_cond::acc_code::f(); + for (auto& i: v) + { + unsigned fin_set = 0U; + + if (!complement) + { + for (auto s: i.first.sets()) + rename[s].set(next_set); + fin_set = next_set++; + } + + acc_cond::mark_t infsets = 0U; + + if (share_inf) + for (auto s: i.second.sets()) + { + unsigned n = inf_rename[s]; + if (n == 0) + n = inf_rename[s] = next_set++; + rename[s].set(n); + infsets.set(n); + } + else // HOA style + { + for (auto s: i.second.sets()) + { + unsigned n = next_set++; + rename[s].set(n); + infsets.set(n); + } + } + + // The definition of Streett wants the Fin first in clauses, + // so we do the same for generalized Streett since HOA does + // not specify anything. See + // https://github.com/adl/hoaf/issues/62 + if (complement) + { + for (auto s: i.first.sets()) + rename[s].set(next_set); + fin_set = next_set++; + + auto pair = acc_cond::inf({fin_set}); + pair |= acc_cond::acc_code::fin(infsets); + pair &= std::move(code); + code = std::move(pair); + } + else + { + auto pair = acc_cond::acc_code::inf(infsets); + pair &= acc_cond::fin({fin_set}); + pair |= std::move(code); + code = std::move(pair); + } + } + + // Fix the automaton + res->set_acceptance(next_set, code); + for (auto& e: res->edges()) + { + acc_cond::mark_t m = 0U; + for (auto s: e.acc.sets()) + m |= rename[s]; + e.acc = m; + } + return res; + } + + + } + + + + twa_graph_ptr + to_generalized_rabin(const const_twa_graph_ptr& aut, + bool share_inf) + { + return to_generalized_rabin_aux(aut, share_inf, false); + } + + twa_graph_ptr + to_generalized_streett(const const_twa_graph_ptr& aut, + bool share_fin) + { + return to_generalized_rabin_aux(aut, share_fin, true); + } } diff --git a/spot/twaalgos/totgba.hh b/spot/twaalgos/totgba.hh index 0bbbbd65b..07d5ebfd1 100644 --- a/spot/twaalgos/totgba.hh +++ b/spot/twaalgos/totgba.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015 Laboratoire de Recherche et Développement +// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -38,4 +38,32 @@ namespace spot /// less than the number of pairs used by IN. SPOT_API twa_graph_ptr streett_to_generalized_buchi_maybe(const const_twa_graph_ptr& in); + + /// \brief Take an automaton with any acceptance condition and return + /// an equivalent Generalized Rabin automaton. + /// + /// This works by putting the acceptance condition in disjunctive + /// normal form, and then merging all the + /// Fin(x1)&Fin(x2)&...&Fin(xn) that may occur in clauses into a + /// single Fin(X). + /// + /// The acceptance-set numbers used by Inf may appear in + /// multiple clauses if \a share_inf is set. + SPOT_API twa_graph_ptr + to_generalized_rabin(const const_twa_graph_ptr& aut, + bool share_inf = false); + + /// \brief Take an automaton with any acceptance condition and return + /// an equivalent Generalized Streett automaton. + /// + /// This works by putting the acceptance condition in cunjunctive + /// normal form, and then merging all the + /// Inf(x1)|Inf(x2)|...|Inf(xn) that may occur in clauses into a + /// single Inf(X). + /// + /// The acceptance-set numbers used by Fin may appear in + /// multiple clauses if \a share_fin is set. + SPOT_API twa_graph_ptr + to_generalized_streett(const const_twa_graph_ptr& aut, + bool share_fin = false); } diff --git a/tests/Makefile.am b/tests/Makefile.am index 8dc5d20ba..b90f719c6 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -207,6 +207,7 @@ TESTS_twa = \ core/complete.test \ core/complement.test \ core/remfin.test \ + core/gragsa.test \ core/dstar.test \ core/readsave.test \ core/ltldo.test \ diff --git a/tests/core/gragsa.test b/tests/core/gragsa.test new file mode 100755 index 000000000..d6316eb1c --- /dev/null +++ b/tests/core/gragsa.test @@ -0,0 +1,31 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2016 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 +set -e + +randltl -n 100 p1 p2 p3 --tree-size 5..15 --seed=200 | +ltlcross --timeout=60 \ +"ltl2tgba %f > %T" \ +"ltl2tgba -G -D %f > %T" \ +"ltl2tgba -G -D %f | autfilt --gsa=unique-fin > %T" \ +"ltl2tgba -G -D %f | autfilt --gra=unique-inf > %T" \ +"ltl2tgba -G -D %f | autfilt --gsa=share-fin > %T" \ +"ltl2tgba -G -D %f | autfilt --gra=share-inf > %T"