diff --git a/NEWS b/NEWS index 03283857b..57e3752ad 100644 --- a/NEWS +++ b/NEWS @@ -18,6 +18,19 @@ New in spot 2.9.5.dev (not yet released) Choices are "ITE" for the if-then-else normal form or "ISOP" for relying on irreducible sums of products. + - ltl2tgba, autfilt, dstar2tgba, and randaut learned a --buchi + option, or -b for short. This output Büchi automata without + forcing state-based acceptance. + + The following aliases have also been added for consistency: + --gba is an alias for --tgba, because the "t" of --tgba is + never forced. + --sba is an alias for -B/--ba, because -B really + implies -S and that is not clear from --ba. + As a consequence of the introduction of --sba, the option + --sbacc (an alias for --state-based-acceptance) cannot be + abbreviated as --sba anymore. + Library: - Historically, Spot labels automata by Boolean formulas over @@ -67,10 +80,14 @@ New in spot 2.9.5.dev (not yet released) can be replaced by - postprocessor::set_type(postprocessor::BA) + postprocessor::set_type(postprocessor::GeneralizedBuchi) and + postprocessor::set_type(postprocessor::BA) + + by + postprocessor::set_type(postprocessor::Buchi) postprocessor::set_pref(postprocessor::Small | postprocessor::SBAcc) diff --git a/bin/common_post.cc b/bin/common_post.cc index 6998eeb4f..089473210 100644 --- a/bin/common_post.cc +++ b/bin/common_post.cc @@ -50,9 +50,15 @@ static constexpr const argp_option options[] = { "generic", 'G', nullptr, 0, "any acceptance condition is allowed", 0 }, { "tgba", OPT_TGBA, nullptr, 0, - "Transition-based Generalized Büchi Automaton (default)", 0 }, - { "ba", 'B', nullptr, 0, - "Büchi Automaton (implies -S)", 0 }, + "automaton with Generalized Büchi acceptance (default)", 0 }, + { "gba", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, + { "sba", 'B', nullptr, 0, + "state-based Büchi Automaton (same as -S -b)", 0 }, + // Historical name of the --sba option. + { "ba", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, + { "buchi", 'b', nullptr, 0, + "automaton with Büchi acceptance", 0 }, + { "Buchi", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, { "monitor", 'M', nullptr, 0, "Monitor (accepts all finite prefixes " "of the given property)", 0 }, { "complete", 'C', nullptr, 0, "output a complete automaton", 0 }, @@ -113,9 +119,15 @@ static const argp_option options_disabled[] = { "generic", 'G', nullptr, 0, "any acceptance is allowed (default)", 0 }, { "tgba", OPT_TGBA, nullptr, 0, - "Transition-based Generalized Büchi Automaton", 0 }, - { "ba", 'B', nullptr, 0, - "Büchi Automaton (with state-based acceptance)", 0 }, + "automaton with Generalized Büchi acceptance", 0 }, + { "gba", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, + { "sba", 'B', nullptr, 0, + "state-based Büchi Automaton (same as -S -b)", 0 }, + // Historical name of the --sba option. + { "ba", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, + { "buchi", 'b', nullptr, 0, + "automaton with Büchi acceptance", 0 }, + { "Buchi", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, { "monitor", 'M', nullptr, 0, "Monitor (accepts all finite prefixes " "of the given property)", 0 }, { "complete", 'C', nullptr, 0, "output a complete automaton", 0 }, @@ -164,6 +176,10 @@ parse_opt_post(int key, char* arg, struct argp_state*) pref = spot::postprocessor::Any; pref_set = true; break; + case 'b': + type = spot::postprocessor::Buchi; + colored = spot::postprocessor::Any; + break; case 'B': type = spot::postprocessor::Buchi; colored = spot::postprocessor::Any; diff --git a/bin/randaut.cc b/bin/randaut.cc index 8a14ae740..27512c9ce 100644 --- a/bin/randaut.cc +++ b/bin/randaut.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2016, 2018-2019 Laboratoire de Recherche et +// Copyright (C) 2012-2016, 2018-2020 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -81,8 +81,14 @@ static const argp_option options[] = "probability that an edge belongs to one acceptance set (0.2)", 0 }, { "automata", 'n', "INT", 0, "number of automata to output (1)\n"\ "use a negative value for unbounded generation", 0 }, - { "ba", 'B', nullptr, 0, - "build a Buchi automaton (implies --acceptance=Buchi --state-acc)", 0 }, + { "sba", 'B', nullptr, 0, + "build a state-based Buchi automaton " + "(implies --acceptance=Buchi --state-acc)", 0 }, + // historical name for --sba + { "ba", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, + { "buchi", 'b', nullptr, 0, + "build a Büchi automaton (same as --acceptance=Buchi)", 0 }, + { "Buchi", 0, nullptr, OPTION_ALIAS, nullptr, 0 }, { "colored", OPT_COLORED, nullptr, 0, "build an automaton in which each edge (or state if combined with " "-S) belong to a single acceptance set", 0 }, @@ -161,10 +167,10 @@ static bool gba_wanted = false; static std::unique_ptr opt_uniq = nullptr; static void -ba_options() +ba_options(bool sbacc) { opt_acc_sets = { 1, 1 }; - opt_state_acc = true; + opt_state_acc = sbacc; } // Range should have the form 12..34 or 12:34, maybe with spaces. The @@ -209,8 +215,12 @@ parse_opt(int key, char* arg, struct argp_state* as) generic_wanted = true; } break; + case 'b': + ba_options(false); + ba_wanted = true; + break; case 'B': - ba_options(); + ba_options(true); ba_wanted = true; break; case 'e': @@ -300,20 +310,22 @@ main(int argc, char** argv) error(2, 0, "--spin implies --ba so should not be used with --acceptance"); if (generic_wanted && ba_wanted) - error(2, 0, "--acceptance and --ba may not be used together"); + error(2, 0, "--acceptance and %s may not be used together", + opt_state_acc ? "--ba" : "--buchi"); if (automaton_format == Spin && opt_acc_sets.max > 1) error(2, 0, "--spin is incompatible with --acceptance=%d..%d", opt_acc_sets.min, opt_acc_sets.max); if (ba_wanted && opt_acc_sets.min != 1 && opt_acc_sets.max != 1) - error(2, 0, "--ba is incompatible with --acceptance=%d..%d", + error(2, 0, "%s is incompatible with --acceptance=%d..%d", + opt_state_acc ? "--ba" : "--buchi", opt_acc_sets.min, opt_acc_sets.max); if (ba_wanted && generic_wanted) error(2, 0, "--ba is incompatible with --acceptance=%s", opt_acceptance); if (automaton_format == Spin) - ba_options(); + ba_options(true); if (opt_colored && opt_acc_sets.min == -1 && !generic_wanted) error(2, 0, "--colored requires at least one acceptance set; " diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index c2b911049..f0c7e4231 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -15,8 +15,10 @@ Those options will be covered in more detail below, but here is a quick summary: - =--tgba= (the default) outputs Transition-based Generalized Büchi - Automata -- =--ba= (or =-B=) outputs state-based Büchi automata + Automata, += =--buchi= (or =-b=) outputs transition-based Büchi automata, +- =--sba= (or =-B=) outputs state-based Büchi automata + (=--ba= is a historical alias for this option) - =--monitor= (or =-M=) outputs monitors - =--generic --deterministic= (or =-DG=) will do whatever it takes to produce a deterministic automaton, and may use any acceptance @@ -24,8 +26,19 @@ a quick summary: - =--parity --deterministic= (or =-DP=) will produce a deterministic automaton with parity acceptance. -(The latter two can also be used with =--deterministic=, but that is -less frequent.) +The latter two can also be used without =--deterministic=, but that is +less frequent. + +Except for =-B= which forces state-based acceptance, these options +build transition-based automata by default. Internally, Spot only +supports transition-based automata. However, while transition-based +automata can be smaller then their state-based counterpart, there are +many cases where transition-based acceptance does not bring any benefits. + +In case where it is detected that the transition-based automaton looks +like a state-based automaton, the different automaton printers will +usually present the result as an automaton with state-based acceptance +for simplicity. * TGBA and BA @@ -57,11 +70,11 @@ State: 1 --END-- #+end_SRC -Actually, because =ltl2tgba= is often used with a single formula -passed on the command line, the =-f= option can be omitted and any -command-line parameter that is not the argument of some option will be -assumed to be a formula to translate (this differs from [[file:ltlfilt.org][=ltlfilt=]], -where such parameters are assumed to be filenames). +As =ltl2tgba= is often used with a single formula passed on the +command line, the =-f= option can be omitted and any command-line +parameter that is not the argument of some option will be assumed to +be a formula to translate (this differs from [[file:ltlfilt.org][=ltlfilt=]], where such +parameters are assumed to be filenames). =ltl2tgba= honors the [[file:oaut.org][common options for selecting the output format]]. The default output format, as shown above, is the [[file:hoa.org][HOA]] format, as this @@ -69,7 +82,7 @@ can easily be piped to other tools. To convert the automaton into a picture, or into vectorial format, use =--dot= or =-d= to request [[http://www.graphviz.org/][GraphViz output]] and process the result with -=dot= or =dotty=. Typically, you could get a =pdf= of this TGBA using +=dot= or =dotty=. Typically, one can get a =pdf= of this TGBA using #+BEGIN_SRC sh :exports code ltl2tgba "Fa & GFb" -d | dot -Tpdf > tgba.pdf #+END_SRC @@ -92,10 +105,10 @@ $txt Characters like ⓿, ❶, etc. denotes the acceptance sets a transition belongs to. In this case, there is only one acceptance set, called -=0=, containing a single transition. You may have many transitions in -the same acceptance set, and a transition may also belong to multiple +=0=, containing a single transition. An acceptance set can contains +multiple transitions, and a transition may also belong to multiple acceptance sets. An infinite path through this automaton is accepting -iff it visit each acceptance set infinitely often. Therefore, in the +iff it visits each acceptance set infinitely often. Therefore, in the above example, any accepted path will /necessarily/ leave the initial state after a finite amount of steps, and then it will verify the property =b= infinitely often. It is also possible that an automaton @@ -137,99 +150,66 @@ these acceptance sets ensures that atomic propositions =a= and =b= must be true infinitely often. A Büchi automaton for the previous formula can be obtained with the -=-B= option: +=-B= or =-b= options, depending on whether we insist on have +state-based acceptance (=-B=) or if transition-based acceptance is OK +(=-b=). + +#+NAME: dotex2tba +#+BEGIN_SRC sh :exports code +ltl2tgba -b 'GFa & GFb' -d +#+END_SRC +#+BEGIN_SRC dot :file dotex2tba.svg :var txt=dotex2tba :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:dotex2tba.svg]] #+NAME: dotex2ba #+BEGIN_SRC sh :exports code ltl2tgba -B 'GFa & GFb' -d #+END_SRC -#+RESULTS: dotex2ba -#+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", peripheries=2] - 0 -> 0 [label=] - 0 -> 1 [label=] - 0 -> 2 [label=] - 1 [label="1"] - 1 -> 0 [label=] - 1 -> 1 [label=] - 1 -> 2 [label=] - 2 [label="2"] - 2 -> 0 [label=] - 2 -> 2 [label=] -} -#+end_example - #+BEGIN_SRC dot :file dotex2ba.svg :var txt=dotex2ba :exports results $txt #+END_SRC #+RESULTS: [[file:dotex2ba.svg]] -Although accepting states in the Büchi automaton are (traditionally) -pictured with double-lines, internally this automaton is still handled -as a TGBA with a single acceptance set such that the transitions -leaving the state are either all accepting, or all non-accepting. You -can see this underlying TGBA if you pass the =--dot=t= option (the =t= -requests the use of transition-based acceptance as it is done -internally): +Although accepting states in state-based Büchi automaton are +(traditionally) pictured with double-lines, internally this automaton +is still handled as a TGBA with a single acceptance set such that the +transitions leaving the state are either all accepting, or all +non-accepting. The underlying TGBA can be seen by passing the +=--dot=t= option (the =t= requests the use of transition-based +acceptance, as it is done internally): #+BEGIN_SRC sh :exports code -ltl2tgba --dot=t -B 'GFa & GFb' +ltl2tgba -B 'GFa & GFb' --dot=t #+END_SRC - #+NAME: dotex2ba-t #+BEGIN_SRC sh :exports none -ltl2tgba --dot=.t -B 'GFa & GFb' +ltl2tgba -B 'GFa & GFb' --dot=.t #+END_SRC - -#+RESULTS: dotex2ba-t -#+begin_example -digraph G { - rankdir=LR - 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=⓿>] - 1 [label="1"] - 1 -> 0 [label=] - 1 -> 1 [label=] - 1 -> 2 [label=] - 2 [label="2"] - 2 -> 0 [label=] - 2 -> 2 [label=] -} -#+end_example - #+BEGIN_SRC dot :file dotex2ba-t.svg :var txt=dotex2ba-t :exports results $txt #+END_SRC #+RESULTS: [[file:dotex2ba-t.svg]] -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. + +Option =-B= is in fact a shorthand for =-b -S=, where =-b= requests +Büchi acceptance, and =-S= requests state-based acceptance. + +Calling =ltl2tgba -S= will build an automaton with generalized Büchi +acceptance (the default for =ltltgba=), but force state-based +acceptance on the output. + +Here is the same formula as above, for comparison. #+NAME: dotex2gba #+BEGIN_SRC sh :exports code ltl2tgba -S 'GFa & GFb' -d #+END_SRC - #+BEGIN_SRC dot :file dotex2gba.svg :var txt=dotex2gba :exports results $txt #+END_SRC @@ -254,23 +234,32 @@ ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' --lbtt or --spin) --check[=PROP] test for the additional property PROP and output the result in the HOA format (implies -H). PROP - may be any prefix of 'all' (default), - 'unambiguous', 'stutter-invariant', or - 'strength'. - -d, --dot[=1|a|b|B|c|e|f(FONT)|h|n|N|o|r|R|s|t|v|+INT] + may be some prefix of 'all' (default), + 'unambiguous', 'stutter-invariant', + 'stutter-sensitive-example', 'semi-determinism', + or 'strength'. + -d, --dot[=1|a|A|b|B|c|C(COLOR)|e|E|f(FONT)|h|k|K|n|N|o|r|R|s|t|u|v|y|+INT| 0 - 0 [label=<0
⓿>] - 0 -> 0 [label=] - 0 -> 1 [label=] - 0 -> 2 [label=] - 1 [label=<1>] - 1 -> 0 [label=] - 1 -> 1 [label=] - 1 -> 2 [label=] - 2 [label=<2>] - 2 -> 0 [label=] - 2 -> 2 [label=] -} -#+end_example - #+BEGIN_SRC dot :file dotex2ba8.svg :var txt=dotex2ba8 :exports results $txt #+END_SRC diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 9f872a9f9..cbe0e80b9 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -297,48 +297,67 @@ represented in the first version. * LBTT output -The [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT]] output has two flavors: state-based (which is used to output -Büchi automata or monitors) or transition-based (for TGBA). +The [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT]] output has two flavors: state-based or transition-based. The +transition flavor can be recognized by the present of a =t= after the +second number. (The first number is the number of states, while the +second number is the number of acceptance sets used.) + +Compare the following transition-based and state-based Büchi automata +for =GFp0=: #+BEGIN_SRC sh -ltl2tgba --ba --lbtt 'p0 U p1' +ltl2tgba -b --lbtt 'GFp0' +#+END_SRC +#+RESULTS: +: 1 1t +: 0 1 +: 0 -1 ! p0 +: 0 0 -1 p0 +: -1 + +#+BEGIN_SRC sh +ltl2tgba -B --lbtt 'GFp0' #+END_SRC #+RESULTS: : 2 1 -: 0 1 -1 -: 1 p1 -: 0 & p0 ! p1 +: 0 1 0 -1 +: 0 p0 +: 1 ! p0 : -1 -: 1 0 0 -1 -: 1 t +: 1 0 -1 +: 0 p0 +: 1 ! p0 : -1 -If you want to request transition-based output even for Büchi automata, -use =--lbtt=t=. +Since even state-based automata are stored as transition-based +automata by Spot, it is also possible to force transition-based +LBTT output to be used even if the automaton declares itself as +state-based. This is done by passing =--lbtt=t=. #+BEGIN_SRC sh -ltl2tgba --ba --lbtt=t 'p0 U p1' +ltl2tgba -B --lbtt=t 'GFp0' #+END_SRC #+RESULTS: : 2 1t : 0 1 -: 1 -1 p1 -: 0 -1 & p0 ! p1 +: 0 0 -1 p0 +: 1 0 -1 ! p0 : -1 : 1 0 -: 1 0 -1 t +: 0 -1 p0 +: 1 -1 ! p0 : -1 Note that the [[http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html][LBTT]] output generalizes the format output by [[http://www.tcs.hut.fi/Software/maria/tools/lbt/][LBT]] with support for transition-based acceptance. Both formats however are restricted to atomic propositions of the form =p0=, =p1=, etc... In case other atomic propositions are used, Spot output them in double -quotes. This other extension of the format is also supported by +quotes. This second extension of the format was introduced by [[http://www.ltl2dstar.de/][ltl2dstar]]. #+BEGIN_SRC sh -ltl2tgba --ba --lbtt 'a U b' +ltl2tgba -B --lbtt 'a U b' #+END_SRC #+RESULTS: diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index ffaaa6f8c..de6a9dc27 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -33,332 +33,336 @@ genltl --dac --eh --sb --hkrss --p --and-fg=32 --format=%F,%L,%f >pos ltl2tgba -Fformulas/3 --stats='%<,%f, %s,%t' | ltl2tgba -D -F-/3 --stats='%<,%f,%>, %s,%t' | + ltl2tgba -b -F-/3 --stats='%<,%f,%>, %s,%t' | + ltl2tgba -bD -F-/3 --stats='%<,%f,%>, %s,%t' | ltl2tgba -B -F-/3 --stats='%<,%f,%>, %s,%t' | ltl2tgba -BD -F-/3 --stats='%<,%>, %s,%t' > output +fg42=2,4294967298 +gf42=1,4294967296 cat >expected <%T" \ "ltl2tgba --lbtt -x comp-susp,!skel-wdba,!skel-simul --small %f >%T" \ "ltl2tgba --spin --ba -x degen-lskip=0 %f >%N" \ -"ltl2tgba --lbtt --ba --high %f > %T" \ +"ltl2tgba --lbtt --sba --high %f > %T" \ +"ltl2tgba --buchi %f > %T" \ "ltl2tgba --spin=6 --ba -x degen-order,degen-lcache=2 --medium %f > %N" \ "ltl2tgba --hoa -x degen-lcache=3 -BDC %f > %H" \ "ltl2tgba --lbtt -BC %f > %T" \ -"ltl2tgba --lbtt --unambiguous --low %f > %T" \ +"ltl2tgba --lbtt --unambiguous -x exprop=0 --low %f > %T" \ "ltl2tgba --lbtt --unambiguous --high %f > %T" \ --json=output.json --csv=output.csv diff --git a/tests/core/randaut.test b/tests/core/randaut.test index ea432ec3f..67edd1d4c 100755 --- a/tests/core/randaut.test +++ b/tests/core/randaut.test @@ -52,6 +52,12 @@ grep 'ba.*incompatible' stderr randaut --ba -A0 3 2>stderr && exit 1 grep 'ba.*incompatible' stderr +randaut --buchi -A2 3 2>stderr && exit 1 +grep 'buchi.*incompatible' stderr + +randaut -b 2 | autfilt --acceptance-is=Buchi | grep trans-acc +randaut -B 2 | autfilt --acceptance-is=Buchi | grep state-acc + randaut --states 10..20 2 -n 100 -H > aut.hoa a=`autfilt --states=..14 -c out.hoa +autfilt --sbacc -H expected > out.hoa diff out.hoa expected autfilt --strip-acc -H expected -n1 > out.hoa