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

@@ -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 Δ₂.
 

bin/autfilt.cc

@@ -44,6 +44,7 @@
 #include <spot/misc/timer.hh>
 #include <spot/parseaut/public.hh>
 #include <spot/tl/exclusive.hh>
+#include <spot/tl/parse.hh>
 #include <spot/twaalgos/alternation.hh>
 #include <spot/twaalgos/are_isomorphic.hh>
 #include <spot/twaalgos/canonicalize.hh>
@@ -63,6 +64,7 @@
 #include <spot/twaalgos/isweakscc.hh>
 #include <spot/twaalgos/langmap.hh>
 #include <spot/twaalgos/mask.hh>
+#include <spot/twaalgos/matchstates.hh>
 #include <spot/twaalgos/product.hh>
 #include <spot/twaalgos/randomize.hh>
 #include <spot/twaalgos/remfin.hh>
@@ -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<int>::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);
 

spot/twaalgos/matchstates.cc

@@ -22,6 +22,8 @@
 #include <spot/twaalgos/product.hh>
 #include <spot/twaalgos/ltl2tgba_fm.hh>
 #include <spot/tl/parse.hh>
+#include <spot/tl/print.hh>
+#include <spot/tl/simplify.hh>
 
 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<formula> 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<formula> v = spot::match_states(aut, f);
+    auto* n = new std::vector<std::string>;
+    n->reserve(v.size());
+    for (spot::formula f: v)
+      n->push_back(str_psl(f));
+    aut->set_named_prop("state-names", n);
+  }
+
 }

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
+  /// \ingroup twa_algorithms
-  /// formulas "reachable" from \a f.
+  /// \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<formula>
   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);
 }

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 \

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 <http://www.gnu.org/licenses/>.
+
+. ./defs
+
+set -e
+
+ltl2tgba -D 'Ga | Gb | Gc' |
+  autfilt --track-formula='Ga | Gb | Gc' > out
+cat >exp <<EOF
+HOA: v1
+name: "Ga | Gb | Gc"
+States: 7
+Start: 6
+AP: 3 "a" "b" "c"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc deterministic
+properties: stutter-invariant very-weak
+--BODY--
+State: 0 "Gc"
+[2] 0
+State: 1 "Gb | Gc"
+[!1&2] 0
+[1&2] 1
+[1&!2] 2
+State: 2 "Gb"
+[1] 2
+State: 3 "Ga"
+[0] 3
+State: 4 "Ga | Gc"
+[!0&2] 0
+[0&!2] 3
+[0&2] 4
+State: 5 "Ga | Gb"
+[!0&1] 2
+[0&!1] 3
+[0&1] 5
+State: 6 "Ga | Gb | Gc"
+[!0&!1&2] 0
+[!0&1&2] 1
+[!0&1&!2] 2
+[0&!1&!2] 3
+[0&!1&2] 4
+[0&1&!2] 5
+[0&1&2] 6
+--END--
+EOF
+diff out exp
+
+
+
+ltl2tgba 'Ga | Gb | Gc' | autfilt --track-formula='Ga | Gb | Gc' > out
+cat >exp <<EOF
+HOA: v1
+name: "Ga | Gb | Gc"
+States: 4
+Start: 0
+AP: 3 "a" "b" "c"
+acc-name: all
+Acceptance: 0 t
+properties: trans-labels explicit-labels state-acc stutter-invariant
+properties: very-weak
+--BODY--
+State: 0 "Ga | Gb | Gc"
+[0] 1
+[1] 2
+[2] 3
+State: 1 "Ga | Gb | Gc"
+[0] 1
+State: 2 "Ga | Gb | Gc"
+[1] 2
+State: 3 "Ga | Gb | Gc"
+[2] 3
+--END--
+EOF
+diff out exp
+
+
+ltl2tgba --low -U 'a U b U c' | autfilt --track-formula='a U b U c' > out
+cat >exp <<EOF
+HOA: v1
+name: "a U (b U c)"
+States: 4
+Start: 0
+AP: 3 "a" "b" "c"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc unambiguous
+properties: stutter-invariant
+--BODY--
+State: 0 "a U (b U c)"
+[0&!1&!2] 0
+[2] 1 {0}
+[1&!2] 2
+[0&1&!2] 3
+State: 1 "1"
+[t] 1 {0}
+State: 2 "a U (b U c)"
+[2] 1 {0}
+[1&!2] 2
+State: 3 "a U (b U c)"
+[0&!1&!2] 0
+[0&1&!2] 3
+--END--
+EOF
+diff out exp