From 88f8af22c3ffaa5c4ed30f0106714125ea6e400d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 25 Mar 2024 17:12:05 +0100 Subject: [PATCH] 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 | 15 ++++++++----- bin/autfilt.cc | 10 +++++++++ doc/org/tut25.org | 49 +++++++++++++++++++++++++++++++++++++++++++ tests/core/split.test | 4 ++++ 4 files changed, 73 insertions(+), 5 deletions(-) diff --git a/NEWS b/NEWS index e7b9b10b2..c782d4233 100644 --- a/NEWS +++ b/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 diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 39a8f46b8..08b17df99 100644 --- a/bin/autfilt.cc +++ b/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::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); diff --git a/doc/org/tut25.org b/doc/org/tut25.org index c3009e690..87ffd544d 100644 --- a/doc/org/tut25.org +++ b/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 diff --git a/tests/core/split.test b/tests/core/split.test index 720133e2e..e109ff4b1 100755 --- a/tests/core/split.test +++ b/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`