From 20563d8a004b0534361d2d5294ce9387dd4b4918 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 2 Apr 2019 23:08:09 +0200 Subject: [PATCH] org: explain how to build automata with state-based acceptance * doc/org/tut22.org: Here. Suggested by Yannick Molinghen. * THANKS: Add him. --- THANKS | 4 +- doc/org/tut22.org | 239 ++++++++++++++++++++++++++++++++++++++++++++-- 2 files changed, 235 insertions(+), 8 deletions(-) diff --git a/THANKS b/THANKS index 24d3acf44..84ad867bd 100644 --- a/THANKS +++ b/THANKS @@ -1,5 +1,4 @@ -We are grateful to these people for their comments, help, or -suggestions. +We are grateful to these people for their comments, help, or suggestions. Akim Demaille Andreas Tollkötter @@ -49,4 +48,5 @@ Tomáš Babiak Valentin Iovene Vitus Lam Yann Thierry-Mieg +Yannick Molinghen Yuri Victorovich diff --git a/doc/org/tut22.org b/doc/org/tut22.org index 50024f908..aefe7e5e1 100644 --- a/doc/org/tut22.org +++ b/doc/org/tut22.org @@ -6,7 +6,15 @@ This example demonstrates how to create an automaton and then print it. -* C++ +* Transition-based Generalized Büchi automaton + :PROPERTIES: + :CUSTOM_ID: tgba + :END: + +For historical reasons, TGBAs are the more commonly used type of +automata in Spot. + +** C++ :PROPERTIES: :CUSTOM_ID: cpp :END: @@ -74,7 +82,7 @@ State: 2 --END-- #+END_SRC -* Python +** Python #+BEGIN_SRC python :results output :exports both :wrap SRC hoa import spot @@ -88,8 +96,8 @@ State: 2 aut = spot.make_twa_graph(bdict) # Since a BDD is associated to every atomic proposition, the register_ap() - # function returns a BDD variable number that can be converted into a BDD using - # bdd_ithvar() from the BuDDy library. + # function returns a BDD variable number that can be converted into a BDD + # using bdd_ithvar() from the BuDDy library. p1 = buddy.bdd_ithvar(aut.register_ap("p1")) p2 = buddy.bdd_ithvar(aut.register_ap("p2")) @@ -102,8 +110,8 @@ State: 2 # specify it explicitely. aut.set_init_state(0) - # new_edge() takes 3 mandatory parameters: source state, destination state, and - # label. A last optional parameter can be used to specify membership to + # new_edge() takes 3 mandatory parameters: source state, destination state, + # and label. A last optional parameter can be used to specify membership to # acceptance sets. In the Python version, the list of acceptance sets the # transition belongs to should be specified as a list. aut.new_edge(0, 1, p1) @@ -134,3 +142,222 @@ State: 2 [0 | 1] 1 {0 1} --END-- #+END_SRC + +* Büchi automaton, with state-based acceptance + :PROPERTIES: + :CUSTOM_ID: sba + :END: + +Spot does not really support state-based acceptance condition; this is +faked as follows: + +- instead of marking states as accepting, we mark *all* outgoing edges + of accepting states, +- additionally, we set =prop_state_acc(true)= to indicate that the + automaton should output as if it were state-based. + +Some algorithm recognize the =prop_state_acc()= properties and trigger +some special handling of the automaton, maybe to preserve its "fake +state-based nature". + +The =print_hoa()= function will check that automata marked with +=prop_state_acc()= are actually using the same acceptance sets on all +outgoing transitions of each state, and raise an exception otherwise. + +In the following example, we are going to use Büchi acceptance, but +=prop_state_acc()= can be used with any acceptance. Again, this property +should be read as "this automaton with transition-based acceptance +is actually encoding a state-based acceptance, so treat it as follows +whenever possible". + +** C++ + +#+BEGIN_SRC C++ :results verbatim :exports both :wrap SRC hoa + #include + #include + #include + + int main(void) + { + // The bdd_dict is used to maintain the correspondence between the + // atomic propositions and the BDD variables that label the edges of + // the automaton. + spot::bdd_dict_ptr dict = spot::make_bdd_dict(); + // This creates an empty automaton that we have yet to fill. + spot::twa_graph_ptr aut = make_twa_graph(dict); + + // Since a BDD is associated to every atomic proposition, the + // register_ap() function returns a BDD variable number + // that can be converted into a BDD using bdd_ithvar(). + bdd p1 = bdd_ithvar(aut->register_ap("p1")); + bdd p2 = bdd_ithvar(aut->register_ap("p2")); + + // Set the acceptance condition of the automaton to Inf(0) + aut->set_buchi(); + aut->prop_state_acc(true); + + // States are numbered from 0. + aut->new_states(3); + // The default initial state is 0, but it is always better to + // specify it explicitely. + aut->set_init_state(0U); + + // new_edge() takes 3 mandatory parameters: source state, + // destination state, and label. A last optional parameter can be + // used to specify membership to acceptance sets. + aut->new_edge(0, 1, p1); + // All edges leaving the same state must belong to the same + // acceptance sets. + aut->new_edge(1, 1, p1 & p2, {0}); + aut->new_edge(1, 2, p2, {0}); + aut->new_edge(2, 1, p1 | p2); + // Print the resulting automaton. + print_hoa(std::cout, aut); + return 0; + } +#+END_SRC + +#+RESULTS: +#+begin_SRC hoa +HOA: v1 +States: 3 +Start: 0 +AP: 2 "p1" "p2" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc +--BODY-- +State: 0 +[0] 1 +State: 1 {0} +[0&1] 1 +[1] 2 +State: 2 +[0 | 1] 1 +--END-- +#+end_SRC + +** Python + +#+BEGIN_SRC python :results output :exports both :wrap SRC hoa + import spot + import buddy + + # The bdd_dict is used to maintain the correspondence between the + # atomic propositions and the BDD variables that label the edges of + # the automaton. + bdict = spot.make_bdd_dict(); + # This creates an empty automaton that we have yet to fill. + aut = spot.make_twa_graph(bdict) + + # Since a BDD is associated to every atomic proposition, the register_ap() + # function returns a BDD variable number that can be converted into a BDD + # using bdd_ithvar() from the BuDDy library. + p1 = buddy.bdd_ithvar(aut.register_ap("p1")) + p2 = buddy.bdd_ithvar(aut.register_ap("p2")) + + # Set the acceptance condition of the automaton to Inf(0) + aut.set_buchi() + + # States are numbered from 0. + aut.new_states(3) + # The default initial state is 0, but it is always better to + # specify it explicitely. + aut.set_init_state(0) + + # new_edge() takes 3 mandatory parameters: source state, destination state, + # and label. A last optional parameter can be used to specify membership to + # acceptance sets. In the Python version, the list of acceptance sets the + # transition belongs to should be specified as a list. + aut.new_edge(0, 1, p1) + # All edges leaving the same state must belong to the same acceptance sets. + aut.new_edge(1, 1, p1 & p2, [0]) + aut.new_edge(1, 2, p2, [0]); + aut.new_edge(2, 1, p1 | p2); + + # Print the resulting automaton. + print(aut.to_str('hoa')) +#+END_SRC + +* Automaton with arbitrary acceptance condition + :PROPERTIES: + :CUSTOM_ID: setacc + :END: + +Generalized Büchi, and Büchi are common enough to warrant a dedicated +method for setting the acceptance condition in the =twa_graph= class. +Arbitrary acceptance condition can be set with =set_acceptance=. + +** C++ + +#+BEGIN_SRC C++ :results verbatim :exports both :wrap SRC hoa + #include + #include + #include + + int main(void) + { + spot::bdd_dict_ptr dict = spot::make_bdd_dict(); + spot::twa_graph_ptr aut = make_twa_graph(dict); + bdd p1 = bdd_ithvar(aut->register_ap("p1")); + bdd p2 = bdd_ithvar(aut->register_ap("p2")); + + // The acceptance condition can be parsed from a string, + // or built from parts using spot::acc_cond. + aut->set_acceptance(3, "(Inf(0) & Fin(1)) | Fin(2)"); + + aut->new_states(3); + aut->set_init_state(0U); + aut->new_edge(0, 1, p1); + aut->new_edge(1, 1, p1 & p2, {0}); + aut->new_edge(1, 2, p2, {1}); + aut->new_edge(2, 1, p1 | p2, {0, 2}); + + print_hoa(std::cout, aut); + return 0; + } +#+END_SRC + +#+RESULTS: +#+begin_SRC hoa +HOA: v1 +States: 3 +Start: 0 +AP: 2 "p1" "p2" +Acceptance: 3 (Inf(0) & Fin(1)) | Fin(2) +properties: trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[0] 1 +State: 1 +[0&1] 1 {0} +[1] 2 {1} +State: 2 +[0 | 1] 1 {0 2} +--END-- +#+end_SRC + +** Python + +#+BEGIN_SRC python :results output :exports both :wrap SRC hoa + import spot + import buddy + + bdict = spot.make_bdd_dict(); + aut = spot.make_twa_graph(bdict) + p1 = buddy.bdd_ithvar(aut.register_ap("p1")) + p2 = buddy.bdd_ithvar(aut.register_ap("p2")) + + # The acceptance condition can be parsed from a string, + # or built from parts using spot.acc_cond. + aut.set_acceptance(3, "(Inf(0) & Fin(1)) | Fin(2)"); + + aut.new_states(3) + aut.set_init_state(0) + aut.new_edge(0, 1, p1) + aut.new_edge(1, 1, p1 & p2, [0]) + aut.new_edge(1, 2, p2, [1]); + aut.new_edge(2, 1, p1 | p2, [0, 2]); + + print(aut.to_str('hoa')) +#+END_SRC