diff --git a/doc/Makefile.am b/doc/Makefile.am index 992870a9f..4998104f0 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -91,6 +91,7 @@ ORG_FILES = \ org/tut20.org \ org/tut21.org \ org/tut22.org \ + org/tut30.org \ org/satmin.org \ org/satmin.tex \ org/setup.org \ diff --git a/doc/org/tut.org b/doc/org/tut.org index 7fb7f123d..2fb7d1517 100644 --- a/doc/org/tut.org +++ b/doc/org/tut.org @@ -17,6 +17,7 @@ three interfaces supported by Spot: shell commands, Python, or C++. - [[file:tut02.org][Relabeling Formulas]] - [[file:tut10.org][Translating an LTL formula into a never claim]] - [[file:tut20.org][Converting a never claim into HOA]] +- [[file:tut30.org][Converting Rabin (or Other) to Büchi, and simplifying it]] * Examples in Python and C++ diff --git a/doc/org/tut30.org b/doc/org/tut30.org new file mode 100644 index 000000000..75cfeb807 --- /dev/null +++ b/doc/org/tut30.org @@ -0,0 +1,288 @@ +# -*- coding: utf-8 -*- +#+TITLE: Converting Rabin (or Other) to Büchi, and simplifying it +#+SETUPFILE: setup.org +#+HTML_LINK_UP: tut.html + +Consider the following Rabin automaton, generated by =ltl2dstar=: + +#+BEGIN_SRC sh :results verbatim :exports code +ltldo ltl2dstar -f 'F(Xp1 xor XXp1)' -H > tut30.hoa +#+END_SRC + +#+RESULTS: + +#+NAME: tut30in +#+BEGIN_SRC sh :results verbatim :exports none +autfilt tut30.hoa --dot=.a +#+END_SRC + +#+RESULTS: tut30in +#+begin_example +digraph G { + rankdir=LR + label=<(Fin(⓿) & Inf(❶)) | (Fin(❷) & Inf(❸)) | (Fin(❹) & Inf(❺))> + labelloc="t" + 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 -> 6 + 0 [label=<0
❷❺>] + 0 -> 2 [label=] + 0 -> 4 [label=] + 1 [label=<1
❷❺>] + 1 -> 4 [label=] + 1 -> 3 [label=] + 2 [label=<2
❸❹>] + 2 -> 0 [label=] + 2 -> 4 [label=] + 3 [label=<3
❸❹>] + 3 -> 4 [label=] + 3 -> 1 [label=] + 4 [label=<4
❶❷❹>] + 4 -> 4 [label=] + 4 -> 4 [label=] + 5 [label=<5
❷❹>] + 5 -> 2 [label=] + 5 -> 3 [label=] + 6 [label=<6
❷❹>] + 6 -> 5 [label=] + 6 -> 5 [label=] +} +#+end_example + +#+BEGIN_SRC dot :file tut30in.png :cmdline -Tpng :var txt=tut30in :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:tut30in.png]] + +Our goal is to generate an equivalent Büchi automaton, preserving +determinism if possible. However nothing of what we will write is +specific to Rabin acceptance: the same code will convert automata with +any acceptance to Büchi acceptance. + +* Shell + +We use =autfilt= with option =-B= to request Büchi acceptance and +state-based output, =-D= to express a preference for deterministic +output, and =-H= for output in the HOA format. Using option +=-D/--deterministic= (or =--small=) actually activates the +"postprocessing" routines of Spot: the acceptance will not only be +changed to Büchi, but simplification routines (useless SCCs removal, +simulation-based reductions, acceptance sets simplifications, +WDBA-minimization, ...) will also be applied. + +#+BEGIN_SRC sh :results verbatim :exports both +autfilt -B -D -H tut30.hoa +#+END_SRC + +#+RESULTS: +#+begin_example +HOA: v1 +States: 5 +Start: 1 +AP: 1 "p1" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic inherently-weak +--BODY-- +State: 0 {0} +[t] 0 +State: 1 +[t] 2 +State: 2 +[!0] 3 +[0] 4 +State: 3 +[0] 0 +[!0] 3 +State: 4 +[!0] 0 +[0] 4 +--END-- +#+end_example + +#+NAME: tut30out +#+BEGIN_SRC sh :results verbatim :exports none +autfilt -B -D tut30.hoa +#+END_SRC + +#+RESULTS: tut30out +#+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 -> 1 + 0 [label="0", peripheries=2] + 0 -> 0 [label=<1>] + 1 [label="1"] + 1 -> 2 [label=<1>] + 2 [label="2"] + 2 -> 3 [label=] + 2 -> 4 [label=] + 3 [label="3"] + 3 -> 0 [label=] + 3 -> 3 [label=] + 4 [label="4"] + 4 -> 0 [label=] + 4 -> 4 [label=] +} +#+end_example + +#+BEGIN_SRC dot :file tut30out.png :cmdline -Tpng :var txt=tut30out :exports results +$txt +#+END_SRC + +#+RESULTS: +[[file:tut30out.png]] + +In the general case transforming an automaton with a complex +acceptance condition into a Büchi automaton can make the output +bigger. However the postprocessing routines may manage to simplify +the result further. + + +* Python + +The Python version uses the =postprocess()= routine: + +#+BEGIN_SRC python :results output :exports both +import spot +aut = spot.automaton('tut30.hoa').postprocess('BA', 'deterministic') +print(aut.to_str('hoa')) +#+END_SRC + +#+RESULTS: +#+begin_example +HOA: v1 +States: 5 +Start: 1 +AP: 1 "p1" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic inherently-weak +--BODY-- +State: 0 {0} +[t] 0 +State: 1 +[t] 2 +State: 2 +[!0] 3 +[0] 4 +State: 3 +[0] 0 +[!0] 3 +State: 4 +[!0] 0 +[0] 4 +--END-- +#+end_example + +The =postprocess()= function has an interface similar to +[[file:tut10.org][the =translate()= function discussed previously]]: + +#+BEGIN_SRC python :results output :exports both +import spot +help(spot.postprocess) +#+END_SRC + +#+RESULTS: +#+begin_example +Help on function postprocess in module spot: + +postprocess(automaton, *args) + Post process an automaton. + + This applies a number of simlification algorithms, depending on + the options supplied. Keep in mind that 'Deterministic' expresses + just a preference that may not be satisfied if the input is + not already 'Deterministic'. + + The optional arguments should be strings among the following: + - at most one in 'Generic', 'TGBA', 'BA', or 'Monitor' + (type of automaton to build) + - at most one in 'Small', 'Deterministic', 'Any' + (preferred characteristics of the produced automaton) + - at most one in 'Low', 'Medium', 'High' + (optimization level) + - any combination of 'Complete' and 'StateBasedAcceptance' + (or 'SBAcc' for short) + + The default corresponds to 'generic', 'small' and 'high'. + +#+end_example + + +* C++ + +The C++ version of this code is a bit more verbose, because the +=postprocess()= function does not exist. You have to instantiate a +=postprocessor= object, configure it, and then call it for each +automaton to process. + +#+BEGIN_SRC C++ :results verbatim :exports both + #include + #include "parseaut/public.hh" + #include "twaalgos/postproc.hh" + #include "twaalgos/hoa.hh" + + int main() + { + std::string input = "tut30.hoa"; + spot::parse_aut_error_list pel; + spot::bdd_dict_ptr dict = spot::make_bdd_dict(); + spot::parsed_aut_ptr pa = parse_aut(input, pel, dict); + if (spot::format_parse_aut_errors(std::cerr, input, pel)) + return 1; + if (pa->aborted) + { + std::cerr << "--ABORT-- read\n"; + return 1; + } + spot::postprocessor post; + post.set_type(spot::postprocessor::BA); + post.set_pref(spot::postprocessor::Deterministic); + post.set_level(spot::postprocessor::High); + auto aut = post.run(pa->aut); + spot::print_hoa(std::cout, aut) << '\n'; + return 0; + } +#+END_SRC + +#+RESULTS: +#+begin_example +HOA: v1 +States: 5 +Start: 1 +AP: 1 "p1" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic inherently-weak +--BODY-- +State: 0 {0} +[t] 0 +State: 1 +[t] 2 +State: 2 +[!0] 3 +[0] 4 +State: 3 +[0] 0 +[!0] 3 +State: 4 +[!0] 0 +[0] 4 +--END-- +#+end_example