From c5d991e55c243998622cb2f10d4185c26fa4bdb1 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 30 Aug 2024 11:38:26 +0200 Subject: [PATCH] autfilt: add a --track-formula option Fixes #591. * spot/twaalgos/matchstates.cc, spot/twaalgos/matchstates.hh (match_states_decorate): New function. * bin/autfilt.cc: Add a --track-formula option. * tests/core/trackf.test: New file. * tests/Makefile.am: Test it. * NEWS: Mention it. --- NEWS | 3 + bin/autfilt.cc | 18 ++++- spot/twaalgos/matchstates.cc | 18 ++++- spot/twaalgos/matchstates.hh | 13 +++- tests/Makefile.am | 1 + tests/core/trackf.test | 123 +++++++++++++++++++++++++++++++++++ 6 files changed, 171 insertions(+), 5 deletions(-) create mode 100755 tests/core/trackf.test diff --git a/NEWS b/NEWS index 2833b5cd8..a288b097c 100644 --- a/NEWS +++ b/NEWS @@ -26,6 +26,9 @@ New in spot 2.12.0.dev (not yet released) edges leading to dead-ends. See the description of restrict_dead_end_edges_here() below. + - autfilt learned --track-formula=F to label states with formulas + derived from F. (This is more precise on deterministic automata.) + - ltlfilt learned --pi1, --sigma1, --delta1, --pi2, --sigma2, and --delta2 to filter according to classes Π₁,Σ₁,Δ₁,Π₂,Σ₂, and Δ₂. diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 1c063af65..0252a0562 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -44,6 +44,7 @@ #include #include #include +#include #include #include #include @@ -63,6 +64,7 @@ #include #include #include +#include #include #include #include @@ -165,6 +167,7 @@ enum { OPT_SUM_AND, OPT_TERMINAL_SCCS, OPT_TO_FINITE, + OPT_TRACK_FORMULA, OPT_TRIV_SCCS, OPT_USED_AP_N, OPT_UNUSED_AP_N, @@ -413,6 +416,7 @@ static const argp_option options[] = "Convert an automaton with \"alive\" and \"!alive\" propositions " "into a Büchi automaton interpretable as a finite automaton. " "States with a outgoing \"!alive\" edge are marked as accepting.", 0 }, + /**************************************************/ { nullptr, 0, nullptr, 0, "Decorations (for -d and -H1.1 output):", 9 }, { "highlight-accepting-run", OPT_HIGHLIGHT_ACCEPTING_RUN, "NUM", OPTION_ARG_OPTIONAL, "highlight one accepting run using color NUM", 0}, @@ -426,9 +430,12 @@ static const argp_option options[] = OPTION_ARG_OPTIONAL, "highlight nondeterministic states and edges with color NUM", 0}, { "highlight-word", OPT_HIGHLIGHT_WORD, "[NUM,]WORD", 0, - "highlight one run matching WORD using color NUM", 0}, + "highlight one run matching WORD using color NUM", 0 }, { "highlight-languages", OPT_HIGHLIGHT_LANGUAGES, nullptr, 0 , - "highlight states that recognize identical languages", 0}, + "highlight states that recognize identical languages", 0 }, + { "track-formula", OPT_TRACK_FORMULA, "FORMULA", 0, + "attempt to label the states of the automaton assuming the automaton " + "recognize FORMULA (use deterministic automata for precision)", 0 }, /**************************************************/ { nullptr, 0, nullptr, 0, "If any option among --small, --deterministic, or --any is given, " @@ -716,6 +723,7 @@ static int opt_highlight_nondet_states = -1; static int opt_highlight_nondet_edges = -1; static int opt_highlight_accepting_run = -1; static bool opt_highlight_languages = false; +static spot::formula opt_track_formula = nullptr; static bool opt_dca = false; static bool opt_streett_like = false; static bool opt_enlarge_acceptance_set = false; @@ -1271,6 +1279,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_TO_FINITE: opt_to_finite = arg ? arg : "alive"; break; + case OPT_TRACK_FORMULA: + opt_track_formula = spot::parse_formula(arg); + break; case OPT_TRIV_SCCS: opt_triv_sccs = parse_range(arg, 0, std::numeric_limits::max()); opt_art_sccs_set = true; @@ -1708,6 +1719,9 @@ namespace else if (opt_separate_edges) aut = spot::separate_edges(aut); + if (opt_track_formula) + match_states_decorate(aut, opt_track_formula); + if (opt_to_finite) aut = spot::to_finite(aut, opt_to_finite); diff --git a/spot/twaalgos/matchstates.cc b/spot/twaalgos/matchstates.cc index 0d9595501..b87401706 100644 --- a/spot/twaalgos/matchstates.cc +++ b/spot/twaalgos/matchstates.cc @@ -22,6 +22,8 @@ #include #include #include +#include +#include namespace spot { @@ -73,6 +75,8 @@ namespace spot for (unsigned i = 0; i < sz2; ++i) state_formulas.push_back(parse_formula((*state_names)[i])); + tl_simplifier tls(tl_simplifier_options(2)); + std::vector res; res.reserve(sz1); @@ -82,8 +86,20 @@ namespace spot disjuncts.clear(); for (unsigned j: v[i]) disjuncts.push_back(state_formulas[j]); - res.push_back(formula::Or(disjuncts)); + res.push_back(tls.simplify(formula::Or(disjuncts))); } return res; } + + void + match_states_decorate(twa_graph_ptr& aut, formula f) + { + std::vector v = spot::match_states(aut, f); + auto* n = new std::vector; + n->reserve(v.size()); + for (spot::formula f: v) + n->push_back(str_psl(f)); + aut->set_named_prop("state-names", n); + } + } diff --git a/spot/twaalgos/matchstates.hh b/spot/twaalgos/matchstates.hh index 3c9bb6236..8061993a4 100644 --- a/spot/twaalgos/matchstates.hh +++ b/spot/twaalgos/matchstates.hh @@ -39,8 +39,9 @@ namespace spot match_states(const const_twa_graph_ptr& aut1, const const_twa_graph_ptr& aut2); - /// \ingroup twa_algorithms \brief match the states of \a aut with - /// formulas "reachable" from \a f. + /// \ingroup twa_algorithms + /// \brief match the states of \a aut with formulas "reachable" from + /// \a f. /// /// The returned vector V assigns each state `x` of \a aut to a /// formula `V[x]`. @@ -55,4 +56,12 @@ namespace spot /// accept more than the words accepted from `a` in \a aut. SPOT_API std::vector match_states(const const_twa_graph_ptr& aut, formula f); + + + /// \ingroup twa_algorithms + /// + /// \brief label the state of \a aut with the result of + /// `match_states(aut,f)`. + SPOT_API void + match_states_decorate(twa_graph_ptr& aut, formula f); } diff --git a/tests/Makefile.am b/tests/Makefile.am index 16b283077..898bcccd8 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -316,6 +316,7 @@ TESTS_twa = \ core/sbacc.test \ core/stutter-tgba.test \ core/strength.test \ + core/trackf.test \ core/emptchk.test \ core/emptchke.test \ core/dfs.test \ diff --git a/tests/core/trackf.test b/tests/core/trackf.test new file mode 100755 index 000000000..a5958b59a --- /dev/null +++ b/tests/core/trackf.test @@ -0,0 +1,123 @@ +#!/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 + +ltl2tgba -D 'Ga | Gb | Gc' | + autfilt --track-formula='Ga | Gb | Gc' > out +cat >exp < out +cat >exp < out +cat >exp <