From 0786e068aed6770918cd83f743691828e23fbc17 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 14 May 2015 20:04:50 +0200 Subject: [PATCH] postproc: add a SBAcc option Producing state-based acceptance is now part of the postprocessing routines. That means we can more easily simplify automata with state-based acceptance (using autfilt -S --small --high, for instance) and as as side-effect, ltl2tgba can produce GBA. However the result of ltl2tgba -S is often larger than that of ltl2tgba -B. * src/twaalgos/postproc.cc, src/twaalgos/postproc.hh: Implement the SBAcc option. * src/bin/common_post.cc, src/bin/common_post.hh: Implement -S. * src/bin/autfilt.cc, src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc, src/bin/ltldo.cc: Adjust. * src/tests/sim3.test: Augment test case. * NEWS, doc/org/ltl2tgba.org, doc/org/autfilt.org: Document it -S. --- NEWS | 6 +++++ doc/org/autfilt.org | 34 +++++++++++++++++-------- doc/org/ltl2tgba.org | 55 ++++++++++++++++++++++++++++++++++++++++ src/bin/autfilt.cc | 14 +--------- src/bin/common_post.cc | 10 ++++++++ src/bin/common_post.hh | 3 ++- src/bin/dstar2tgba.cc | 2 +- src/bin/ltl2tgba.cc | 2 +- src/bin/ltl2tgta.cc | 2 +- src/bin/ltldo.cc | 2 +- src/tests/sim3.test | 37 +++++++++++++++++++++++++++ src/twaalgos/postproc.cc | 50 +++++++++++++++++++++++++++--------- src/twaalgos/postproc.hh | 6 +++-- 13 files changed, 181 insertions(+), 42 deletions(-) diff --git a/NEWS b/NEWS index 1de5e6cee..9396e1f92 100644 --- a/NEWS +++ b/NEWS @@ -80,6 +80,12 @@ New in spot 1.99b (not yet released) accepting run (but there might be several ways to reject a word). This works for LTL and PSL formulas. + - ltl2tgba has a new option, -S to produce generalized-Büchi + automata with state-based acceptance. Those are obtained by + converting some transition-based GBA into a state-based GBA, so + they are usually not as small as one would wish. The same + option -S is also supported by autfilt. + - ltlcross will work with translator producing automata with any acceptance condition, provided the output is in the HOA format. So it can effectively be used to validate tools producing Rabin diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index 2ff3e5452..964c50c00 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -143,7 +143,6 @@ refer to the output automaton. Of course this distinction makes sense only if =autfilt= was instructed to perform an operation on the input automaton. - * Filtering automata =autfilt= supports multiple ways to filter automata based on different @@ -192,10 +191,10 @@ autfilt --help | sed -n '/Output automaton type:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: : -B, --ba Büchi Automaton +: --generic Any acceptance is allowed (default) : -M, --monitor Monitor (accepts all finite prefixes of the given : property) : --tgba Transition-based Generalized Büchi Automaton -: (default) These options specifies desired properties: @@ -203,11 +202,14 @@ These options specifies desired properties: autfilt --help | sed -n '/Translation intent:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: -: -a, --any no preference (default) +: -a, --any no preference, do not bother making it small or +: deterministic (default) : -C, --complete output a complete automaton (combine with other : intents) : -D, --deterministic prefer deterministic automata : --small prefer small automata +: -S, --state-based-acceptance, --sbacc +: define the acceptance using states Finally, the following switches control the amount of effort applied to reach the desired properties: @@ -252,7 +254,8 @@ autfilt --help | sed -n '/Transformations:/,/^$/p' | sed '1d;$d' exclusive propositions. --instut[=1|2] allow more stuttering (two possible algorithms) --keep-states=NUM[,NUM...] only keep specified states. The first state - will be the new initial state + will be the new initial state. Implies + --remove-unreachable-states. --mask-acc=NUM[,NUM...] remove all transitions in specified acceptance sets --merge-transitions merge transitions with same destination and @@ -263,10 +266,20 @@ autfilt --help | sed -n '/Transformations:/,/^$/p' | sed '1d;$d' --remove-ap=AP[=0|=1][,AP...] remove atomic propositions either by existential quantification, or by assigning them 0 or 1 - --remove-fin rewrite the automaton without using Fin - acceptance - --state-based-acceptance, --sbacc - define the acceptance using states + --remove-dead-states remove states that are unreachable, or that cannot + belong to an infinite path + --remove-fin rewrite the automaton without using Fin acceptance + + --remove-unreachable-states + remove states that are unreachable from the + initial state + --separate-sets if both Inf(x) and Fin(x) appear in the acceptance + condition, replace Fin(x) by a new Fin(y) and + adjust the automaton + --simplify-exclusive-ap if --exclusive-ap is used, assume those AP + groups are actually exclusive in the system to + simplify the expression of transition labels + (implies --merge-transitions) --strip-acceptance remove the acceptance condition and all acceptance sets #+end_example @@ -345,11 +358,11 @@ $txt #+RESULTS: [[file:autfilt-ex1.png]] -Using =--sbacc= will "push" the acceptance membership of the transitions to the states: +Using =-S= will "push" the acceptance membership of the transitions to the states: #+NAME: autfilt-ex2 #+BEGIN_SRC sh :results verbatim :export code -autfilt --sbacc aut-ex1.hoa --dot=.a +autfilt -S aut-ex1.hoa --dot=.a #+END_SRC #+RESULTS: autfilt-ex2 @@ -358,6 +371,7 @@ digraph G { rankdir=LR label=<(Fin(❶) & Fin(❸) & Inf(⓿)) | (Inf(❷)&Inf(❸)) | Inf(❶)> labelloc="t" + node [shape="circle"] fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index 02591195d..87788b61c 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -214,6 +214,61 @@ $txt #+RESULTS: [[file:dotex2ba-t.png]] +Using option =-S= instead of option =-B= you can obtain generalized +Büchi automata with state-based acceptance. Here is the same formula +as above, for comparison. + +#+NAME: dotex2gba +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba -S 'GFa & GFb' +#+END_SRC + +#+RESULTS: dotex2gba +#+begin_example +digraph G { + rankdir=LR + node [shape="circle"] + fontname="Lato" + node [fontname="Lato"] + edge [fontname="Lato"] + node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7] + I [label="", style=invis, width=0] + I -> 0 + 0 [label=<0
⓿❶>] + 0 -> 0 [label=] + 0 -> 1 [label=] + 0 -> 2 [label=] + 0 -> 3 [label=] + 1 [label=<1>] + 1 -> 0 [label=] + 1 -> 1 [label=] + 1 -> 2 [label=] + 1 -> 3 [label=] + 2 [label=<2
❶>] + 2 -> 0 [label=] + 2 -> 1 [label=] + 2 -> 2 [label=] + 2 -> 3 [label=] + 3 [label=<3
⓿>] + 3 -> 0 [label=] + 3 -> 1 [label=] + 3 -> 2 [label=] + 3 -> 3 [label=] +} +#+end_example + +#+BEGIN_SRC dot :file dotex2gba.png :cmdline -Tpng :var txt=dotex2gba :exports results +$txt +#+END_SRC +#+RESULTS: +[[file:dotex2gba.png]] + +Note that =ltl2tgba= is not very good at generating state-based +generalized Büchi automata (GBA): all it does is generating a +transition-based one internally, and then pushing acceptance sets onto +states. On this example, the resulting GBA produced by =-S= is larger +than the BA produced by =-B=. + As already discussed on the page about [[file:oaut.org][common output options]], various options controls the output format of =ltl2tgba=: diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 3da677203..71601d39c 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -50,7 +50,6 @@ #include "twaalgos/are_isomorphic.hh" #include "twaalgos/canonicalize.hh" #include "twaalgos/mask.hh" -#include "twaalgos/sbacc.hh" #include "twaalgos/sepsets.hh" #include "twaalgos/stripacc.hh" #include "twaalgos/remfin.hh" @@ -92,7 +91,6 @@ enum { OPT_REM_DEAD, OPT_REM_UNREACH, OPT_REM_FIN, - OPT_SBACC, OPT_SEED, OPT_SEP_SETS, OPT_SIMPLIFY_EXCLUSIVE_AP, @@ -133,9 +131,6 @@ static const argp_option options[] = { "destut", OPT_DESTUT, 0, 0, "allow less stuttering", 0 }, { "mask-acc", OPT_MASK_ACC, "NUM[,NUM...]", 0, "remove all transitions in specified acceptance sets", 0 }, - { "state-based-acceptance", OPT_SBACC, 0, 0, - "define the acceptance using states", 0 }, - { "sbacc", 0, 0, OPTION_ALIAS, 0, 0 }, { "strip-acceptance", OPT_STRIPACC, 0, 0, "remove the acceptance condition and all acceptance sets", 0 }, { "keep-states", OPT_KEEP_STATES, "NUM[,NUM...]", 0, @@ -251,7 +246,6 @@ static int opt_max_count = -1; static bool opt_destut = false; static char opt_instut = 0; static bool opt_is_empty = false; -static bool opt_sbacc = false; static bool opt_stripacc = false; static bool opt_dnf_acc = false; static bool opt_cnf_acc = false; @@ -437,9 +431,6 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_REM_UNREACH: opt_rem_unreach = true; break; - case OPT_SBACC: - opt_sbacc = true; - break; case OPT_SEED: opt_seed = to_int(arg); break; @@ -583,9 +574,6 @@ namespace if (opt->product) aut = spot::product(std::move(aut), opt->product); - if (opt_sbacc) - aut = spot::sbacc(aut); - aut = post.run(aut, nullptr); if (randomize_st || randomize_tr) @@ -686,7 +674,7 @@ main(int argc, char** argv) spot::srand(opt_seed); spot::postprocessor post(&extra_options); - post.set_pref(pref | comp); + post.set_pref(pref | comp | sbacc); post.set_type(type); post.set_level(level); diff --git a/src/bin/common_post.cc b/src/bin/common_post.cc index 88145fdd3..60872c01e 100644 --- a/src/bin/common_post.cc +++ b/src/bin/common_post.cc @@ -24,6 +24,7 @@ spot::postprocessor::output_type type = spot::postprocessor::TGBA; spot::postprocessor::output_pref pref = spot::postprocessor::Small; spot::postprocessor::output_pref comp = spot::postprocessor::Any; +spot::postprocessor::output_pref sbacc = spot::postprocessor::Any; spot::postprocessor::optimization_level level = spot::postprocessor::High; enum { @@ -43,6 +44,9 @@ static const argp_option options[] = "or deterministic", 0 }, { "complete", 'C', 0, 0, "output a complete automaton (combine " "with other intents)", 0 }, + { "state-based-acceptance", 'S', 0, 0, + "define the acceptance using states", 0 }, + { "sbacc", 0, 0, OPTION_ALIAS, 0, 0 }, /**************************************************/ { 0, 0, 0, 0, "Optimization level:", 21 }, { "low", OPT_LOW, 0, 0, "minimal optimizations (fast)", 0 }, @@ -62,6 +66,9 @@ static const argp_option options_disabled[] = "or deterministic (default)", 0 }, { "complete", 'C', 0, 0, "output a complete automaton (combine " "with other intents)", 0 }, + { "state-based-acceptance", 'S', 0, 0, + "define the acceptance using states", 0 }, + { "sbacc", 0, 0, OPTION_ALIAS, 0, 0 }, /**************************************************/ { 0, 0, 0, 0, "Optimization level:", 21 }, { "low", OPT_LOW, 0, 0, "minimal optimizations (fast, default)", 0 }, @@ -86,6 +93,9 @@ parse_opt_post(int key, char*, struct argp_state*) case 'D': pref = spot::postprocessor::Deterministic; break; + case 'S': + sbacc = spot::postprocessor::SBAcc; + break; case OPT_HIGH: level = spot::postprocessor::High; simplification_level = 3; diff --git a/src/bin/common_post.hh b/src/bin/common_post.hh index 8fecf7a18..2d0d73c1f 100644 --- a/src/bin/common_post.hh +++ b/src/bin/common_post.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -29,4 +29,5 @@ extern const struct argp post_argp_disabled; // postprocessing disabled extern spot::postprocessor::output_type type; extern spot::postprocessor::output_pref pref; extern spot::postprocessor::output_pref comp; +extern spot::postprocessor::output_pref sbacc; extern spot::postprocessor::optimization_level level; diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index e1ed9f657..d49281c9f 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -428,7 +428,7 @@ main(int argc, char** argv) jobs.emplace_back("-", true); spot::postprocessor post(&extra_options); - post.set_pref(pref | comp); + post.set_pref(pref | comp | sbacc); post.set_type(type); post.set_level(level); diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index 6c7d41a97..d7b14b303 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -204,7 +204,7 @@ main(int argc, char** argv) program_name); spot::translator trans(&extra_options); - trans.set_pref(pref | comp); + trans.set_pref(pref | comp | sbacc); trans.set_type(type); trans.set_level(level); if (unambiguous) diff --git a/src/bin/ltl2tgta.cc b/src/bin/ltl2tgta.cc index fb36cc325..b1b78b301 100644 --- a/src/bin/ltl2tgta.cc +++ b/src/bin/ltl2tgta.cc @@ -232,7 +232,7 @@ main(int argc, char** argv) program_name); spot::translator trans(&extra_options); - trans.set_pref(pref | comp); + trans.set_pref(pref | comp | sbacc); trans.set_type(type); trans.set_level(level); diff --git a/src/bin/ltldo.cc b/src/bin/ltldo.cc index 3b23687f6..f164174bb 100644 --- a/src/bin/ltldo.cc +++ b/src/bin/ltldo.cc @@ -358,7 +358,7 @@ main(int argc, char** argv) setup_sig_handler(); spot::postprocessor post; - post.set_pref(pref | comp); + post.set_pref(pref | comp | sbacc); post.set_type(type); post.set_level(level); diff --git a/src/tests/sim3.test b/src/tests/sim3.test index fd6bf3397..4e3d5a99c 100755 --- a/src/tests/sim3.test +++ b/src/tests/sim3.test @@ -47,3 +47,40 @@ State: 6 {0 3} EOF test "`../../bin/autfilt --small input --stats=%S,%s`" = 7,5 + +../../bin/autfilt -S --high --small input -H > out +cat >expected <acc().num_sets(); @@ -173,7 +177,7 @@ namespace spot a = scc_filter_states(a); else if (scc_filter_ > 0) { - if (type_ == BA && a->is_sba()) + if (state_based_ && a->has_state_based_acc()) a = scc_filter_states(a); else a = scc_filter(a, scc_filter_ > 1); @@ -208,8 +212,10 @@ namespace spot { if (type_ == BA) a = do_degen(a); - if (COMP_ == Complete) + if (COMP_) a = tgba_complete(a); + if (SBACC_) + a = sbacc(a); return a; } @@ -243,9 +249,11 @@ namespace spot // at hard levels if we want a small output. if (!dba || (level_ == High && PREF_ == Small)) { - if (type_ == BA && a->is_sba() && !tba_determinisation_) + if (((SBACC_ && a->has_state_based_acc()) + || (type_ == BA && a->is_sba())) + && !tba_determinisation_) { - sim = do_ba_simul(a, ba_simul_); + sim = do_sba_simul(a, ba_simul_); } else { @@ -254,6 +262,8 @@ namespace spot // No need to do that if tba_determinisation_ will be used. if (type_ == BA && !tba_determinisation_) sim = do_degen(sim); + else if (SBACC_ && !tba_determinisation_) + sim = sbacc(sim); } } @@ -266,10 +276,18 @@ namespace spot // We postponed degeneralization above i case we would need // to perform TBA-determinisation, but now it is clear // that we won't perform it. So do degeneralize. - if (tba_determinisation_ && type_ == BA) + if (tba_determinisation_) { - dba = do_degen(dba); - assert(is_deterministic(dba)); + if (type_ == BA) + { + dba = do_degen(dba); + assert(is_deterministic(dba)); + } + else if (SBACC_) + { + dba = sbacc(dba); + assert(is_deterministic(dba)); + } } } @@ -412,12 +430,18 @@ namespace spot { if (dba && !dba_is_minimal) // WDBA is already clean. { - dba = scc_filter(dba, true); + if (state_based_ && dba->has_state_based_acc()) + dba = scc_filter_states(dba); + else + dba = scc_filter(dba, true); assert(!sim); } else if (sim) { - sim = scc_filter(sim, true); + if (state_based_ && sim->has_state_based_acc()) + sim = scc_filter_states(sim); + else + sim = scc_filter(sim, true); assert(!dba); } } @@ -426,6 +450,8 @@ namespace spot if (COMP_) sim = tgba_complete(sim); + if (SBACC_) + sim = sbacc(sim); return sim; } diff --git a/src/twaalgos/postproc.hh b/src/twaalgos/postproc.hh index 80d70ccbf..93f23d528 100644 --- a/src/twaalgos/postproc.hh +++ b/src/twaalgos/postproc.hh @@ -78,7 +78,9 @@ namespace spot Deterministic = 2, // 3 reserved for unambiguous // Combine Complete as 'Small | Complete' or 'Deterministic | Complete' - Complete = 4 + Complete = 4, + // Likewise. State-based acceptance. + SBAcc = 8, }; typedef int output_pref; @@ -104,7 +106,7 @@ namespace spot protected: twa_graph_ptr do_simul(const twa_graph_ptr& input, int opt); - twa_graph_ptr do_ba_simul(const twa_graph_ptr& input, int opt); + twa_graph_ptr do_sba_simul(const twa_graph_ptr& input, int opt); twa_graph_ptr do_degen(const twa_graph_ptr& input); output_type type_;