diff --git a/NEWS b/NEWS index e8485acee..3d5c25c7c 100644 --- a/NEWS +++ b/NEWS @@ -17,6 +17,10 @@ New in spot 2.8.5.dev (not yet released) - When running translators ltlcross will now display {names} when supplied. + - autfilt learned the --partial-degeneralize option, to remove + conjunctions of Inf, or disjunction of Fin that appears in + arbitrary conditions. + Library: - Historically, Spot only supports LTL with infinite semantics @@ -58,9 +62,8 @@ New in spot 2.8.5.dev (not yet released) parity_min_even(n) = parity_min(false, n) - partial_degeneralize() is a new function performing partial - degeneralization to get rid of conjunctions of Inf terms in - acceptance conditions. This also works with disjunctions of - Fin terms in deterministic automata. + degeneralization to get rid of conjunctions of Inf terms, or + disjunctions of Fin terms in acceptance conditions. - simplify_acceptance_here() and simplify_acceptance() learned to simplify subformulas like Fin(i)&Fin(j) or Inf(i)|Inf(j), or some diff --git a/bin/autfilt.cc b/bin/autfilt.cc index e0f8279b2..1f25e4fd4 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2020 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -133,6 +133,7 @@ enum { OPT_MASK_ACC, OPT_MERGE, OPT_NONDET_STATES, + OPT_PARTIAL_DEGEN, OPT_PRODUCT_AND, OPT_PRODUCT_OR, OPT_RANDOMIZE, @@ -363,6 +364,10 @@ static const argp_option options[] = { "sum-and", OPT_SUM_AND, "FILENAME", 0, "build the sum with the automaton in FILENAME " "to intersect languages", 0 }, + { "partial-degeneralize", OPT_PARTIAL_DEGEN, "NUM1,NUM2,...", + OPTION_ARG_OPTIONAL, "Degeneralize automata according to sets " + "NUM1,NUM2,... If no sets are given, partial degeneralization " + "is performed for all conjunctions of Inf and disjunctions of Fin.", 0 }, { "separate-sets", OPT_SEP_SETS, nullptr, 0, "if both Inf(x) and Fin(x) appear in the acceptance condition, replace " "Fin(x) by a new Fin(y) and adjust the automaton", 0 }, @@ -619,6 +624,8 @@ static bool opt_complement = false; static bool opt_complement_acc = false; static char* opt_decompose_scc = nullptr; static bool opt_dualize = false; +static bool opt_partial_degen_set = false; +static spot::acc_cond::mark_t opt_partial_degen = {}; static spot::acc_cond::mark_t opt_mask_acc = {}; static std::vector opt_keep_states = {}; static unsigned int opt_keep_states_initial = 0; @@ -1005,6 +1012,23 @@ parse_opt(int key, char* arg, struct argp_state*) opt_nondet_states = parse_range(arg, 0, std::numeric_limits::max()); opt_nondet_states_set = true; break; + case OPT_PARTIAL_DEGEN: + { + opt_partial_degen_set = true; + if (arg) + for (auto res : to_longs(arg)) + { + if (res < 0) + error(2, 0, "acceptance sets should be non-negative:" + " --partial-degeneralize=%ld", res); + if (static_cast(res) >= + spot::acc_cond::mark_t::max_accsets()) + error(2, 0, "this implementation does not support that many" + " acceptance sets: --partial-degeneralize=%ld", res); + opt_partial_degen.set(res); + } + break; + } case OPT_PRODUCT_AND: { auto a = read_automaton(arg, opt->dict); @@ -1478,6 +1502,19 @@ namespace else if (opt_rem_unreach) aut->purge_unreachable_states(); + if (opt_partial_degen_set) + { + if (opt_partial_degen) + { + auto sets = opt_partial_degen & aut->acc().all_sets(); + aut = spot::partial_degeneralize(aut, sets); + } + else + { + aut = spot::partial_degeneralize(aut); + } + } + if (opt->product_and) aut = ::product(std::move(aut), opt->product_and); if (opt->product_or) diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index 744c581c9..cbbe5eabf 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -750,8 +750,7 @@ namespace spot namespace { static acc_cond::mark_t - to_strip(const acc_cond::acc_code& code, acc_cond::mark_t todegen, - bool also_fin) + to_strip(const acc_cond::acc_code& code, acc_cond::mark_t todegen) { if (code.empty()) return todegen; @@ -768,14 +767,6 @@ namespace spot break; case acc_cond::acc_op::Fin: case acc_cond::acc_op::FinNeg: - if (!also_fin) - { - pos -= 2; - tostrip -= code[pos].mark; - break; - } - // Handle Fin and Inf in the same way - SPOT_FALLTHROUGH; case acc_cond::acc_op::Inf: case acc_cond::acc_op::InfNeg: { @@ -796,8 +787,7 @@ namespace spot update_acc_for_partial_degen(acc_cond::acc_code& code, acc_cond::mark_t todegen, acc_cond::mark_t tostrip, - acc_cond::mark_t accmark, - bool also_fin) + acc_cond::mark_t accmark) { if (!todegen || code.empty()) { @@ -817,14 +807,6 @@ namespace spot break; case acc_cond::acc_op::Fin: case acc_cond::acc_op::FinNeg: - if (!also_fin) - { - pos -= 2; - code[pos].mark = code[pos].mark.strip(tostrip); - break; - } - // Handle Fin and Inf in the same way - SPOT_FALLTHROUGH; case acc_cond::acc_op::Inf: case acc_cond::acc_op::InfNeg: { @@ -869,9 +851,6 @@ namespace spot if (code.empty()) return {}; - if (allow_fin) - allow_fin = is_deterministic(aut); - acc_cond::mark_t res = {}; unsigned res_sz = -1U; auto update = [&](const acc_cond::mark_t& m) @@ -926,16 +905,11 @@ namespace spot res->copy_ap_of(a); acc_cond::acc_code acc = a->get_acceptance(); - // We can also degeneralize disjunctions of Fin if the input is - // deterministic. - bool also_fin = a->acc().uses_fin_acceptance() && is_deterministic(a); - - acc_cond::mark_t tostrip = to_strip(acc, todegen, also_fin); + acc_cond::mark_t tostrip = to_strip(acc, todegen); acc_cond::mark_t keep = a->acc().all_sets() - tostrip; acc_cond::mark_t degenmark = {keep.count()}; - if (!update_acc_for_partial_degen(acc, todegen, tostrip, degenmark, - also_fin)) + if (!update_acc_for_partial_degen(acc, todegen, tostrip, degenmark)) report_invalid_partial_degen_arg(todegen, acc); res->set_acceptance(acc); diff --git a/spot/twaalgos/degen.hh b/spot/twaalgos/degen.hh index 27ba43f5a..67ef07a3b 100644 --- a/spot/twaalgos/degen.hh +++ b/spot/twaalgos/degen.hh @@ -107,13 +107,12 @@ namespace spot /// /// Cases where the sets listed in \a todegen also occur outside /// of the Inf-conjunction are also supported. Subformulas that - /// are disjunctions of Fin(.) terms (e.g., Fin(1)|Fin(2)) can - /// also be degeneralized if the input automaton is deterministic. + /// are disjunctions of Fin(.) terms (e.g., Fin(1)|Fin(2)) will + /// be degeneralized as well. /// /// If this functions is called with a value of \a todegen that does - /// not match a conjunction of Inf(.), or in a deterministic - /// automaton a disjunction of Fin(.), an std::runtime_error - /// exception is thrown. + /// not match a conjunction of Inf(.), or a disjunction of Fin(.), + /// an std::runtime_error exception is thrown. /// /// The version of the function that has no \a todegen argument will /// perform all possible partial degeneralizations, and may return @@ -132,10 +131,9 @@ namespace spot /// \brief Is the automaton partially degeneralizable? /// - /// Return a mark `M={m₁, m₂, ..., mₙ}` such that either (1) - /// `Inf(m₁)&Inf(m₂)&...&Inf(mₙ)` appears in the acceptance - /// condition of \a aut, or (2) \a aut is deterministic and - /// `Inf(m₁)|Inf(m₂)|...|Fin(mₙ)` appear in its conditions. + /// Return a mark `M={m₁, m₂, ..., mₙ}` such that either + /// `Inf(m₁)&Inf(m₂)&...&Inf(mₙ)` or `Fin(m₁)|Fin(m₂)|...|Fin(mₙ)` + /// appears in the acceptance condition of \a aut. /// /// If multiple such marks exist the smallest such mark is returned. /// (This is important in case of overlapping options. E.g., in the diff --git a/tests/Makefile.am b/tests/Makefile.am index a577c76ec..30a46d9a0 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -285,6 +285,7 @@ TESTS_twa = \ core/ltl2dstar4.test \ core/ltl2ta.test \ core/ltl2ta2.test \ + core/pdegen.test \ core/randaut.test \ core/randtgba.test \ core/isomorph.test \ diff --git a/tests/core/pdegen.test b/tests/core/pdegen.test new file mode 100755 index 000000000..875e78946 --- /dev/null +++ b/tests/core/pdegen.test @@ -0,0 +1,32 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2020 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 + +randaut -n10 -e.3 -Q7 -A 'generalized-co-Buchi 2..5' 2 | + autcross --verbose --language-preserved \ + 'autfilt --partial-degen' \ + 'autfilt --partial-degen=1,2,3' + +randaut -n10 -e.3 -Q7 -A 'random 2..5' 2 | + autcross --verbose --language-preserved 'autfilt --partial-degen' diff --git a/tests/python/pdegen.py b/tests/python/pdegen.py index abea21053..dedcc5a19 100644 --- a/tests/python/pdegen.py +++ b/tests/python/pdegen.py @@ -144,10 +144,14 @@ State: 3 "2#0" assert spot.is_partially_degeneralizable(de) == [] +df = spot.partial_degeneralize(f, [0, 1]) +df.equivalent_to(f) +assert str(df.acc()) == '(1, Fin(0))' + try: - df = spot.partial_degeneralize(f, [0, 1]) + df = spot.partial_degeneralize(f, [0, 1, 2]) except RuntimeError as e: - assert 'partial_degeneralize(): {0,1} does not' in str(e) + assert 'partial_degeneralize(): {0,1,2} does not' in str(e) else: raise RuntimeError("missing exception")