autfilt: add option --separate-edges

* bin/autfilt.cc: Implement it.
* tests/core/split.test: Test it.
* doc/org/tut25.org: Demonstrate it.
* NEWS: Mention it.

NEWS

@@ -1,5 +1,11 @@
 New in spot 2.11.6.dev  (not yet released)
 
+  Documentation:
+
+  - https://spot.lre.epita.fr/tut25.html is a new example showing
+    how to print an automaton in the "BA format" (used by Rabbit
+    and other tools).
+
   Command-line tools:
 
   - In places that accept format strings with '%' sequences, like
@@ -19,6 +25,10 @@ New in spot 2.11.6.dev  (not yet released)
     and its negation is already a basis).  This can help reducing the
     size of large HOA files.
 
+  - autfilt learned --separate-edges, to split the labels of
+    the automaton using a basis of disjoint labels.  See
+    https://spot.lre.epita.fr/tut25.html for some motivation.
+
   - ltlfilt has a new option --relabel-overlapping-bool=abc|pnn that
     will replace boolean subformulas by fresh atomic propositions even
     if those subformulas share atomic propositions.
@@ -204,11 +214,6 @@ New in spot 2.11.6.dev  (not yet released)
     This version of Spot now declares its svg outputs as HTML to
     prevent Jypyter from wrapping them is images.
 
-  Documentation:
-
-  - https://spot.lre.epita.fr/tut25.html is a new example showing
-    how to print an automaton in the "BA format" (used by Rabbit).
-
   Bugs fixed:
 
   - tgba_determinize()'s use_simulation option would cause it to

bin/autfilt.cc

@@ -149,6 +149,7 @@ enum {
   OPT_SAT_MINIMIZE,
   OPT_SCCS,
   OPT_SEED,
+  OPT_SEPARATE_EDGES,
   OPT_SEP_SETS,
   OPT_SIMPL_ACC,
   OPT_SIMPLIFY_EXCLUSIVE_AP,
@@ -370,6 +371,9 @@ static const argp_option options[] =
     { "split-edges", OPT_SPLIT_EDGES, nullptr, 0,
       "split edges into transitions labeled by conjunctions of all atomic "
       "propositions, so they can be read as letters", 0 },
+    { "separate-edges", OPT_SEPARATE_EDGES, nullptr, 0,
+      "split edges into transitions labeled by a disjoint set of labels that"
+      " form a basis for the original automaton", 0 },
     { "sum", OPT_SUM_OR, "FILENAME", 0,
       "build the sum with the automaton in FILENAME "
       "to sum languages", 0 },
@@ -692,6 +696,7 @@ static bool opt_rem_unreach = false;
 static bool opt_rem_unused_ap = false;
 static bool opt_sep_sets = false;
 static bool opt_split_edges = false;
+static bool opt_separate_edges = false;
 static const char* opt_sat_minimize = nullptr;
 static const char* opt_to_finite = nullptr;
 static int opt_highlight_nondet_states = -1;
@@ -1204,6 +1209,9 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_SPLIT_EDGES:
       opt_split_edges = true;
       break;
+    case OPT_SEPARATE_EDGES:
+      opt_separate_edges = true;
+      break;
     case OPT_STATES:
       opt_states = parse_range(arg, 0, std::numeric_limits<int>::max());
       break;
@@ -1664,6 +1672,8 @@ namespace
 
       if (opt_split_edges)
         aut = spot::split_edges(aut);
+      else if (opt_separate_edges)
+        aut = spot::separate_edges(aut);
 
       if (opt_to_finite)
         aut = spot::to_finite(aut, opt_to_finite);

doc/org/tut25.org

@@ -283,3 +283,52 @@ produces the same output.
 #+begin_src sh :results silent :exports results
 rm -f tut25.hoa
 #+end_src
+
+* Improving the split
+
+=split_edges()= is not the only way to split the edge labels.  Another
+option, introduced in Spot 2.12, is =separate_edges()=: this looks at
+the labels used in the automaton and intersects them to construct a
+new set of disjoint labels that can be used as a basis for all labels.
+In the worst case, the basis will be equal to $2^{\{a,b,c\}}$ and this
+reduces to =split_edges()=.  However in many cases, as in our running
+example, it will require fewer labels.
+
+#+NAME: tut25ex3
+#+BEGIN_SRC sh :exports code
+ltl2tgba -B "a W G(b->c)" | autfilt --separate-edges -d
+#+END_SRC
+
+#+BEGIN_SRC dot :file tut25ex3.svg :var txt=tut25ex3 :exports results
+$txt
+#+END_SRC
+
+#+RESULTS:
+[[file:tut25ex3.svg]]
+
+Fixing the above Python/C++ code to use =separate_edges()= instead of
+=split_edges()= allows to convert this example using only 3 letters:
+
+#+NAME: toba.py
+#+begin_src python :exports results
+  import spot
+  aut = spot.translate("a W G(b->c)", "BA")
+  aut = spot.separate_edges(aut)
+  acc = aut.acc()
+  print(aut.get_init_state_number())
+  for e in aut.edges():
+     print(f"{e.cond.id()},{e.src}->{e.dst}")
+  for s in range(aut.num_states()):
+      if acc.accepting(aut.state_acc_sets(s)):
+         print(s)
+#+end_src
+
+#+RESULTS: toba.py
+: 1
+: 83,0->0
+: 85,0->0
+: 85,1->0
+: 83,1->1
+: 76,1->1
+: 0
+: 1

tests/core/split.test

@@ -23,6 +23,10 @@ set -e
 
 test 3,7 = `ltl2tgba 'a U b' --stats=%e,%t`
 test 7,7 = `ltl2tgba 'a U b' | autfilt --split --stats=%e,%t`
+test 5,7 = `ltl2tgba 'a U b' | autfilt --separate-edges --stats=%e,%t`
 test 12,12 = `ltl2tgba 'a U b' | autfilt -C --split --stats=%e,%t`
+test 9,12 = `ltl2tgba 'a U b' | autfilt -C --separate-edges --stats=%e,%t`
 test 0,0 = `ltl2tgba 0 | autfilt --split --stats=%e,%t`
+test 0,0 = `ltl2tgba 0 | autfilt --separate-edges --stats=%e,%t`
 test 1,1 = `ltl2tgba 0 | autfilt -C --split --stats=%e,%t`
+test 1,1 = `ltl2tgba 0 | autfilt -C --separate-edges --stats=%e,%t`