diff --git a/NEWS b/NEWS index 957b9b254..14b21c99e 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,18 @@ New in spot 2.12.0.dev (not yet released) - Nothing yet. + Command-line tools: + + - autfilt learned --restrict-dead-end-edges, to restricts labels of + edges leading to dead-ends. See the description of + restrict_dead_end_edges_here() below. + + Library: + + - restrict_dead_end_edges_here() can reduce non-determinism (but + not remove it) by restricting the label L of some edge (S)-L->(D) + going to a state D that does not have other successor than + itself. The conditions are detailled in the documentation of + this function. New in spot 2.12 (2024-05-16) diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 420bf2867..1c063af65 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -51,6 +51,7 @@ #include #include #include +#include #include #include #include @@ -148,6 +149,7 @@ enum { OPT_REM_UNREACH, OPT_REM_UNUSED_AP, OPT_REM_FIN, + OPT_RESTRICT_DEAD_ENDS, OPT_SAT_MINIMIZE, OPT_SCCS, OPT_SEED, @@ -373,6 +375,9 @@ static const argp_option options[] = { "remove-dead-states", OPT_REM_DEAD, nullptr, 0, "remove states that are unreachable, or that cannot belong to an " "infinite path", 0 }, + { "restrict-dead-end-edges", OPT_RESTRICT_DEAD_ENDS, nullptr, 0, + "restrict labels of dead-end edges, based on useful transitions of the " + "state they reach", 0 }, { "simplify-acceptance", OPT_SIMPL_ACC, nullptr, 0, "simplify the acceptance condition by merging identical acceptance sets " "and by simplifying some terms containing complementary sets", 0 }, @@ -715,6 +720,7 @@ static bool opt_dca = false; static bool opt_streett_like = false; static bool opt_enlarge_acceptance_set = false; static bool opt_reduce_acceptance_set = false; +static bool opt_restrict_dead_ends = false; static spot::twa_graph_ptr ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false) @@ -1199,6 +1205,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_REM_UNUSED_AP: opt_rem_unused_ap = true; break; + case OPT_RESTRICT_DEAD_ENDS: + opt_restrict_dead_ends = true; + break; case OPT_SAT_MINIMIZE: opt_sat_minimize = arg ? arg : ""; break; @@ -1442,6 +1451,9 @@ namespace else if (opt_clean_acc) cleanup_acceptance_here(aut); + if (opt_restrict_dead_ends) + restrict_dead_end_edges_here(aut); + if (opt_sep_sets) separate_sets_here(aut); if (opt_complement_acc) diff --git a/python/spot/impl.i b/python/spot/impl.i index 778983aac..6fa3e9f07 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -115,6 +115,7 @@ #include #include #include +#include #include #include #include @@ -717,6 +718,7 @@ def state_is_accepting(self, src) -> "bool": %include %include %include +%include %include %include %include diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 74b345dc8..507da630e 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -1845,6 +1845,86 @@ namespace spot return force_inf_rec(&back(), rem); } + namespace + { + static acc_cond::acc_code keep_one_inf_per_branch_rec + (const acc_cond::acc_word* pos, bool inf_seen) + { + auto start = pos - pos->sub.size; + switch (pos->sub.op) + { + case acc_cond::acc_op::And: + { + auto cur = --pos; + auto res = acc_cond::acc_code::t(); + // Make a first pass to find Inf(...) + if (!inf_seen) + do + { + if (cur->sub.op == acc_cond::acc_op::Inf) + { + res = acc_cond::acc_code::inf(cur[-1].mark.lowest()); + inf_seen = true; + break; + } + cur -= cur->sub.size + 1; + } + while (cur > start); + // Now process the rest. + do + { + if (pos->sub.op != acc_cond::acc_op::Inf) + { + auto tmp = + keep_one_inf_per_branch_rec(pos, inf_seen) & + std::move(res); + std::swap(tmp, res); + } + pos -= pos->sub.size + 1; + } + while (pos > start); + return res; + } + case acc_cond::acc_op::Or: + { + --pos; + auto res = acc_cond::acc_code::f(); + do + { + auto tmp = + keep_one_inf_per_branch_rec(pos, inf_seen) | std::move(res); + std::swap(tmp, res); + pos -= pos->sub.size + 1; + } + while (pos > start); + return res; + } + case acc_cond::acc_op::Fin: + return acc_cond::acc_code::fin(pos[-1].mark); + case acc_cond::acc_op::Inf: + if (inf_seen) + return acc_cond::acc_code::t(); + else + return acc_cond::acc_code::inf(pos[-1].mark.lowest()); + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::InfNeg: + SPOT_UNREACHABLE(); + return {}; + } + SPOT_UNREACHABLE(); + return {}; + } + + } + + acc_cond::acc_code + acc_cond::acc_code::keep_one_inf_per_branch() const + { + if (is_t() || is_f()) + return *this; + return keep_one_inf_per_branch_rec(&back(), false); + } + acc_cond::mark_t acc_cond::acc_code::used_sets() const { diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 1749e45cd..6e03d3b20 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -1391,6 +1391,13 @@ namespace spot /// \brief For all `x` in \a m, replaces `Fin(x)` by `false`. acc_code force_inf(mark_t m) const; + /// \brief Rewrite an acceptance condition by keeping at most + /// one Inf(x) on each dijunctive branch. + /// + /// For instance `(Fin(0)&Inf(1)&(Inf(2)|Fin(3))) | Inf(4)&Inf(5)` + /// will become `(Fin(0)&Inf(1) | Inf(4)` + acc_code keep_one_inf_per_branch() const; + /// \brief Return the set of sets appearing in the condition. acc_cond::mark_t used_sets() const; @@ -1992,6 +1999,16 @@ namespace spot return code_.inf_satisfiable(inf); } + /// \brief Rewrite an acceptance condition by keeping at most + /// one Inf(x) on each disjunctive branch. + /// + /// For instance `(Fin(0)&Inf(1)&(Inf(2)|Fin(3))) | Inf(4)&Inf(5)` + /// will become `(Fin(0)&Inf(1) | Inf(4)` + acc_cond keep_one_inf_per_branch() const + { + return {num_sets(), code_.keep_one_inf_per_branch()}; + } + /// \brief Check potential acceptance of an SCC. /// /// Assuming that an SCC intersects all sets in \a diff --git a/spot/twaalgos/Makefile.am b/spot/twaalgos/Makefile.am index 80884cdbb..ede79f81a 100644 --- a/spot/twaalgos/Makefile.am +++ b/spot/twaalgos/Makefile.am @@ -39,6 +39,7 @@ twaalgos_HEADERS = \ copy.hh \ cycles.hh \ dbranch.hh \ + deadends.hh \ degen.hh \ determinize.hh \ dot.hh \ @@ -114,6 +115,7 @@ libtwaalgos_la_SOURCES = \ contains.cc \ cycles.cc \ dbranch.cc \ + deadends.cc \ degen.cc \ determinize.cc \ dot.cc \ diff --git a/spot/twaalgos/deadends.cc b/spot/twaalgos/deadends.cc new file mode 100644 index 000000000..cb8b7f886 --- /dev/null +++ b/spot/twaalgos/deadends.cc @@ -0,0 +1,181 @@ +// -*- coding: utf-8 -*- +// Copyright (C) by the Spot authors, see the AUTHORS file for details. +// +// 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 . + +#include "config.h" + +#include +#include + +namespace spot +{ + namespace + { + // Gather a disjunction of labels that appears on the edges of a + // dead-end state that have to be seen in order to make an + // accepting cycle. + static bdd + gather_useful_labels(const const_twa_graph_ptr& aut, + acc_cond::mark_t used_in_cond, + unsigned state) + { + // First, simplify the acceptance condition c based on the set + // of colors occurring around the state. + auto c = aut->get_acceptance(); + acc_cond::mark_t used_on_no_edge = used_in_cond; + acc_cond::mark_t used_on_all_edges = used_in_cond; + for (auto& e: aut->edges()) + { + used_on_no_edge -= e.acc; + used_on_all_edges &= e.acc; + } + + // if x appears on all edges, then + // Fin(x) = false and Inf(x) = true + if (used_on_all_edges) + c = c.remove(used_on_all_edges, false); + // if x appears on no edge at all, then + // Fin(x) = true and Inf(x) = false + if (used_on_no_edge) + c = c.remove(used_on_no_edge, true); + + if (c.is_f()) + return bddfalse; + if (c.is_t()) + return bddtrue; + + auto d = c.keep_one_inf_per_branch(); + + // Now look for edges that are useful to the simplified + // acceptance condition. + // We consider an edge as useful if its colors satisfy at + // least one Fin(x) or Inf(x) in the acceptance. + bdd useful = bddfalse; + for (auto& e: aut->out(state)) + if (d.accepting(e.acc)) + useful |= e.cond; + return useful; + } + } + + twa_graph_ptr + restrict_dead_end_edges_here(twa_graph_ptr& aut) + { + // We don't have anything to do if the automaton is deterministic. + if (aut->prop_universal()) + return aut; + if (!aut->is_existential()) + throw std::runtime_error + ("restrict_dead_end_edges_here() does not support alternation"); + unsigned ns = aut->num_states(); + // Find the states that are dead ends, i.e., that + // have only themselves as successors. + std::vector dead_end_states(ns, true); + // Also record the disjunction of all self-loops around each + // state. + std::vector self_loops(ns, bddfalse); + for (auto& e: aut->edges()) + if (e.src == e.dst) + self_loops[e.src] |= e.cond; + else + dead_end_states[e.src] = false; + + // If the automaton is weak, we can consider every label of + // the dead-end state as useful. + bool is_weak = aut->prop_weak().is_true(); + + // This will hold the labels of the useful self-loops of the the + // dead-end states. But we don't want to initialize it until we + // need it. + std::vector dead_end_useful(is_weak ? 0U : ns, bddfalse); + std::vector dead_end_useful_computed(is_weak ? 0U : ns, false); + acc_cond::mark_t used_in_cond = aut->get_acceptance().used_sets(); + + std::vector label_unions(ns, bddfalse); + bool created_false_labels = false; + bool nondeterministic_for_sure = false; + for (unsigned s = 0; s < ns; ++s) + { + // compute a union of labels per dead-end destination + for (auto& e: aut->out(s)) + if (e.src != e.dst && dead_end_states[e.dst]) + label_unions[e.dst] |= e.cond; + + // Iterate over all edges (SRC,COND,DST), find those such that + // (1) DST is a dead-end, + // (2) Lab(DST,DST))⇒Lab(SRC,SRC) + // (3) UsefulLab(DST)⇒Lab(SRC,DST)⇒Lab(SRC,SRC) + // + // where Lab(X,Y) is the union of all labels between X and Y + // And UsefulLab(DST) are the labeled of the "useful" self + // loops of DST (see gather_useful_labels). + for (auto& e: aut->out(s)) + if (e.src != e.dst && dead_end_states[e.dst]) + { + if (bdd u = label_unions[e.dst], sl = self_loops[e.src]; + bdd_implies(u, sl) && bdd_implies(self_loops[e.dst], sl)) + { + // Find the edges of DST that are necessary to an + // accepting loop, and gather their labels. + bdd d; + if (is_weak) + { + d = self_loops[e.dst]; + } + else + { + if (!dead_end_useful_computed[e.dst]) + { + dead_end_useful[e.dst] = + gather_useful_labels(aut, used_in_cond, e.dst); + dead_end_useful_computed[e.dst] = true; + } + d = dead_end_useful[e.dst]; + } + if (bdd_implies(d, u)) + { + // Restrict the dead-end transition's label. + bdd cond = e.cond; + cond &= d; + if (cond != e.cond) + { + e.cond = cond; + if (cond == bddfalse) + created_false_labels = true; + else + nondeterministic_for_sure = true; + } + } + } + } + // reset unions before next iteration + for (auto& e: aut->out(s)) + label_unions[e.dst] = bddfalse; + } + // Note that restricting those label will never make the automaton + // deterministic. In fact, it could make the automaton + // non-deterministic. Additionally, completeness will not be + // changed. This is because the restricted Lab(SRC,DST) still + // implies Lab(SRC,SRC). + if (nondeterministic_for_sure) + aut->prop_universal(false); + if (created_false_labels) + aut->merge_edges(); + return aut; + } + +} diff --git a/spot/twaalgos/deadends.hh b/spot/twaalgos/deadends.hh new file mode 100644 index 000000000..58b2d017f --- /dev/null +++ b/spot/twaalgos/deadends.hh @@ -0,0 +1,51 @@ +// -*- coding: utf-8 -*- +// Copyright (C) by the Spot authors, see the AUTHORS file for details. +// +// 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 . + +#pragma once + +#include + +namespace spot +{ + /// \brief restrict labels from "dead-end edges" + /// + /// A dead-end edge is an edge between two states S₁ and S₂ such + /// that S₂ has only itself as successor. I.e., once a run goes + /// through this "dead-end" edge, it gets stuck in S₂. + /// + /// Let Lab(S,D) denote the disjunction of all labels between S and + /// D. Let UsefulLab(D,D) be the disjunction of labels of any + /// subset of self-loops of D that will intersect all accepting + /// cycles around D (one way to compute this subset is to simplify + /// the acceptance condition with keep_one_inf_per_branch(), and + /// then keep each edge that satisfy it). + /// + /// Now, if the following implications are satisfied + /// + /// ⎧ UsefulLab(D,D) ⇒ Lab(S,D) ⇒ Lab(S,S),
+ /// ⎨
+ /// ⎩ Lab(D,D) ⇒ Lab(S,S).
+ /// + /// then any edge between S and D, labeled by ℓ⊆Lab(S,D) + /// can be replaced by ℓ∩UsefulLab(D,D). + /// + /// This algorithm has no effect on deterministic automata (where + /// it is not possible that Lab(S,D) ⇒ Lab(S,S)). + SPOT_API twa_graph_ptr + restrict_dead_end_edges_here(twa_graph_ptr& aut); +} diff --git a/tests/Makefile.am b/tests/Makefile.am index 0c3c995c5..cfe6a033a 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -270,6 +270,7 @@ TESTS_twa = \ core/dupexp.test \ core/exclusive-tgba.test \ core/remprop.test \ + core/deadends.test \ core/degendet.test \ core/degenid.test \ core/degenlskip.test \ @@ -413,6 +414,7 @@ TESTS_python = \ python/dbranch.py \ python/declenv.py \ python/decompose_scc.py \ + python/deadends.py \ python/det.py \ python/dualize.py \ python/ecfalse.py \ diff --git a/tests/core/deadends.test b/tests/core/deadends.test new file mode 100755 index 000000000..4ecb3d552 --- /dev/null +++ b/tests/core/deadends.test @@ -0,0 +1,70 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) by the Spot authors, see the AUTHORS file for details. +# +# 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 + +# The following formula was incorrectly reduced during +# the development of --restrict-dead-edges. +out=`ltl2tgba 'X((GF!p2 R p3) & G(p3 U p2))' | + autfilt --restrict-dead --stats='%T %t'` +test "$out" = '11 11' # should be twice the same value + +# The following formulas are all reduced +cat >input.ltl <. + +# Test that the spot.gen package works, in particular, we want +# to make sure that the objects created from spot.gen methods +# are usable with methods from the spot package. + + +import spot +from unittest import TestCase +tc = TestCase() + +b = spot.translate('FGb') +a = spot.translate('GFa & GFc') +p = spot.product_susp(b, a) +q = spot.scc_filter(spot.simulation(p), True) +s = p.to_str() +spot.restrict_dead_end_edges_here(p) +s += p.to_str() +# Applying it twice should not change anything +spot.restrict_dead_end_edges_here(p) +s += p.to_str() + +tc.assertEqual(s, """HOA: v1 +States: 2 +Start: 0 +AP: 3 "a" "b" "c" +acc-name: generalized-Buchi 2 +Acceptance: 2 Inf(0)&Inf(1) +properties: trans-labels explicit-labels trans-acc stutter-invariant +--BODY-- +State: 0 +[t] 0 +[!0&1&!2] 1 +[0&1&!2] 1 {0} +[!0&1&2] 1 {1} +[0&1&2] 1 {0 1} +State: 1 +[!0&1&!2] 1 +[0&1&!2] 1 {0} +[!0&1&2] 1 {1} +[0&1&2] 1 {0 1} +--END--HOA: v1 +States: 2 +Start: 0 +AP: 3 "a" "b" "c" +acc-name: generalized-Buchi 2 +Acceptance: 2 Inf(0)&Inf(1) +properties: trans-labels explicit-labels trans-acc stutter-invariant +--BODY-- +State: 0 +[t] 0 +[0&1&!2] 1 {0} +[0&1&2] 1 {0 1} +State: 1 +[!0&1&!2] 1 +[0&1&!2] 1 {0} +[!0&1&2] 1 {1} +[0&1&2] 1 {0 1} +--END--HOA: v1 +States: 2 +Start: 0 +AP: 3 "a" "b" "c" +acc-name: generalized-Buchi 2 +Acceptance: 2 Inf(0)&Inf(1) +properties: trans-labels explicit-labels trans-acc stutter-invariant +--BODY-- +State: 0 +[t] 0 +[0&1&!2] 1 {0} +[0&1&2] 1 {0 1} +State: 1 +[!0&1&!2] 1 +[0&1&!2] 1 {0} +[!0&1&2] 1 {1} +[0&1&2] 1 {0 1} +--END--""") + +spot.restrict_dead_end_edges_here(q) +s = q.to_str() +tc.assertEqual(s, """HOA: v1 +States: 2 +Start: 0 +AP: 3 "a" "b" "c" +acc-name: generalized-Buchi 2 +Acceptance: 2 Inf(0)&Inf(1) +properties: trans-labels explicit-labels trans-acc stutter-invariant +--BODY-- +State: 0 +[t] 0 +[0&1] 1 +State: 1 +[!0&1&!2] 1 +[0&1&!2] 1 {0} +[!0&1&2] 1 {1} +[0&1&2] 1 {0 1} +--END--""") + +a = spot.translate('GFa & (FGb | FGc) & GFc') +s = a.to_str() +spot.restrict_dead_end_edges_here(a) +s += a.to_str() +tc.assertEqual(s, """HOA: v1 +States: 3 +Start: 0 +AP: 3 "a" "b" "c" +acc-name: generalized-Buchi 2 +Acceptance: 2 Inf(0)&Inf(1) +properties: trans-labels explicit-labels trans-acc stutter-invariant +--BODY-- +State: 0 +[t] 0 +[0&1 | 1&2] 1 +[2] 2 +State: 1 +[!0&1&!2] 1 +[0&1&!2] 1 {0} +[!0&1&2] 1 {1} +[0&1&2] 1 {0 1} +State: 2 +[!0&2] 2 {1} +[0&2] 2 {0 1} +--END--HOA: v1 +States: 3 +Start: 0 +AP: 3 "a" "b" "c" +acc-name: generalized-Buchi 2 +Acceptance: 2 Inf(0)&Inf(1) +properties: trans-labels explicit-labels trans-acc stutter-invariant +--BODY-- +State: 0 +[t] 0 +[0&1] 1 +[0&2] 2 +State: 1 +[!0&1&!2] 1 +[0&1&!2] 1 {0} +[!0&1&2] 1 {1} +[0&1&2] 1 {0 1} +State: 2 +[!0&2] 2 {1} +[0&2] 2 {0 1} +--END--""")