From 8568c3b423a2c0f8ca9e2da6b76ef8a479265dbc Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 6 Feb 2016 14:15:16 +0100 Subject: [PATCH] postproc: integrate tgba_determinize() * spot/twa/acc.hh: Add a smaller version of is_parity(). * spot/twaalgos/postproc.cc: Call tgba_determinize() if asked for Generic acceptance and Deterministic output. * bin/common_post.cc: Add 'G' as a shorthand for --generic. * doc/org/ltl2tgba.org: Illustrate =ltl2tgba -G -D=. --- bin/common_post.cc | 25 ++++++++------ doc/org/ltl2tgba.org | 71 ++++++++++++++++++++++++++++++++++++--- spot/twa/acc.hh | 10 ++++-- spot/twaalgos/postproc.cc | 53 +++++++++++++++++------------ 4 files changed, 120 insertions(+), 39 deletions(-) diff --git a/bin/common_post.cc b/bin/common_post.cc index 6c14f5373..bb751835d 100644 --- a/bin/common_post.cc +++ b/bin/common_post.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -32,8 +32,7 @@ bool level_set = false; bool pref_set = false; enum { - OPT_GENERIC = 1, - OPT_HIGH, + OPT_HIGH = 1, OPT_LOW, OPT_MEDIUM, OPT_SMALL, @@ -44,6 +43,8 @@ static const argp_option options[] = { /**************************************************/ { nullptr, 0, nullptr, 0, "Output automaton type:", 2 }, + { "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, @@ -57,7 +58,9 @@ static const argp_option options[] = /**************************************************/ { nullptr, 0, nullptr, 0, "Simplification goal:", 20 }, { "small", OPT_SMALL, nullptr, 0, "prefer small automata (default)", 0 }, - { "deterministic", 'D', nullptr, 0, "prefer deterministic automata", 0 }, + { "deterministic", 'D', nullptr, 0, "prefer deterministic automata " + "(combine with --generic to be sure to obtain a deterministic " + "automaton)", 0 }, { "any", 'a', nullptr, 0, "no preference, do not bother making it small " "or deterministic", 0 }, /**************************************************/ @@ -73,7 +76,7 @@ static const argp_option options_disabled[] = { /**************************************************/ { nullptr, 0, nullptr, 0, "Output automaton type:", 2 }, - { "generic", OPT_GENERIC, nullptr, 0, + { "generic", 'G', nullptr, 0, "any acceptance is allowed (default)", 0 }, { "tgba", OPT_TGBA, nullptr, 0, "Transition-based Generalized Büchi Automaton", 0 }, @@ -88,7 +91,9 @@ static const argp_option options_disabled[] = /**************************************************/ { nullptr, 0, nullptr, 0, "Simplification goal:", 20 }, { "small", OPT_SMALL, nullptr, 0, "prefer small automata", 0 }, - { "deterministic", 'D', nullptr, 0, "prefer deterministic automata", 0 }, + { "deterministic", 'D', nullptr, 0, "prefer deterministic automata " + "(combine with --generic to be sure to obtain a deterministic " + "automaton)", 0 }, { "any", 'a', nullptr, 0, "no preference, do not bother making it small " "or deterministic", 0 }, /**************************************************/ @@ -120,15 +125,15 @@ parse_opt_post(int key, char*, struct argp_state*) pref = spot::postprocessor::Deterministic; pref_set = true; break; + case 'G': + type = spot::postprocessor::Generic; + break; case 'M': type = spot::postprocessor::Monitor; break; case 'S': sbacc = spot::postprocessor::SBAcc; break; - case OPT_GENERIC: - type = spot::postprocessor::Generic; - break; case OPT_HIGH: level = spot::postprocessor::High; simplification_level = 3; diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index d689ade18..6c1abc328 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -3,11 +3,22 @@ #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html -This tool translates LTL or PSL formulas into two kinds of Büchi -automata, or to monitors. The default is to output Transition-based -Generalized Büchi Automata (hereinafter abbreviated TGBA), but more -traditional Büchi automata (BA) may be requested using the =-B= -option. +This tool translates LTL or PSL formulas into different types of +automata. + +The inner algorithm produces Transition-based Generalized Büchi +Automata, hence the name of the tools, but =ltl2tgba= has grown and +now offers several options to adjust the type of automaton output. +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 +- =--monitor= (or =-M=) outputs Monitors +- =--generic --deterministic= (or =-GD=) will do whatever it takes to + produce a deterministic automaton, and may output generalized Büchi, + or parity acceptance. * TGBA and BA @@ -448,6 +459,13 @@ Note that options =--deterministic= and =--small= express /preferences/. They certainly do /not/ guarantee that the output will be deterministic, or will be the smallest automaton possible. +In particular, for properties more complex than obligations, it is +possible that no deterministic TGBA exist, and even if it exists, +=ltl2tgba= might not find it: so a non-deterministic automaton can be +returned in this case. If you absolutely want a deterministic +automaton, [[#generic][read on about the =--generic= option below]]. + + An example formula where the difference between =-D= and =--small= is flagrant is =Ga|Gb|Gc=: @@ -697,6 +715,49 @@ to experiment with the different settings on a small version of the pattern, and select the lowest setting that satisfies your expectations. +* Deterministic automata with =--generic= + :PROPERTIES: + :CUSTOM_ID: generic + :END: + + The =--generic= (or =-G=) option allows =ltl2tgba= to use more + complex acceptance. Combined with =--deterministic= (or =-D=) this + allows the use of a determinization algorithm that produce automata + with parity acceptance. + + For instance =FGa= is the typical formula for which not + deterministic TGBA exists. + +#+NAME: ltl2tgba-fga +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgba "FGa" -D -d.a +#+END_SRC + +#+BEGIN_SRC dot :file ltl2tgba-fga.png :cmdline -Tpng :var txt=ltl2tgba-fga :exports results + $txt +#+END_SRC + +#+RESULTS: +[[file:ltl2tgba-fga.png]] + + But with =--generic=, =ltl2tgba= will output the following Rabin automaton: + +#+NAME: ltl2tgba-fga-D +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgba "FGa" -G -D -d.a +#+END_SRC + +#+BEGIN_SRC dot :file ltl2tgba-fga-D.png :cmdline -Tpng :var txt=ltl2tgba-fga-D :exports results + $txt +#+END_SRC + +#+RESULTS: +[[file:ltl2tgba-fga-D.png]] + +Note that determinization algorithm implemented actually outputs +parity acceptance, but =Fin(0)&Inf(1)= can be interpreted either as +=Rabin 1= or =parity min odd 2=. + * Translating multiple formulas for statistics If multiple formulas are given to =ltl2tgba=, the corresponding diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 22202cc91..38add6566 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de -// l'Epita. +// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et +// Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -1040,6 +1040,12 @@ namespace spot // check whether the condition is logically equivalent to some // parity acceptance condition. bool is_parity(bool& max, bool& odd, bool equiv = false) const; + bool is_parity() const + { + bool max; + bool min; + return is_parity(max, min); + } // Return (true, m) if there exist some acceptance mark m that // does not satisfy the acceptance condition. Return (false, 0U) diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index aead169be..9c6ddd421 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -33,6 +33,7 @@ #include #include #include +#include namespace spot { @@ -175,27 +176,25 @@ namespace spot if (type_ == BA || SBACC_) state_based_ = true; - bool tgb_used = false; if (type_ != Generic && !a->acc().is_generalized_buchi()) { a = to_generalized_buchi(a); - tgb_used = true; + if (PREF_ == Any && level_ == Low) + a = do_scc_filter(a, true); } - if (PREF_ == Any && level_ == Low) - if (type_ == Generic - || type_ == TGBA - || (type_ == BA && a->is_sba()) - || (type_ == Monitor && a->num_sets() == 0)) - { - if (tgb_used) - a = do_scc_filter(a, true); - if (COMP_) - a = complete(a); - if (SBACC_) - a = sbacc(a); - return a; - } + if (PREF_ == Any && level_ == Low + && (type_ == Generic + || type_ == TGBA + || (type_ == BA && a->is_sba()) + || (type_ == Monitor && a->num_sets() == 0))) + { + if (COMP_) + a = complete(a); + if (SBACC_) + a = sbacc(a); + return a; + } int original_acc = a->num_sets(); @@ -365,14 +364,26 @@ namespace spot } } + if (PREF_ == Deterministic && type_ == Generic && !dba) + { + dba = tgba_determinize(to_generalized_buchi(sim)); + if (level_ != Low) + dba = simulation(dba); + sim = nullptr; + } + // Now dba contains either the result of WDBA-minimization (in // that case dba_is_wdba=true), or some deterministic automaton // that is either the result of the simulation or of the - // TBA-determinization (dba_is_wdba=false in both cases). If the - // dba is a WDBA, we do not have to run SAT-minimization. A - // negative value in sat_minimize_ can for its use for debugging. + // TBA-determinization (dba_is_wdba=false in both cases), or a + // parity automaton coming from tgba_determinize(). If the dba is + // a WDBA, we do not have to run SAT-minimization. A negative + // value in sat_minimize_ can force its use for debugging. if (sat_minimize_ && dba && (!dba_is_wdba || sat_minimize_ < 0)) { + if (type_ == Generic) + throw std::runtime_error + ("postproc() no yet updated to mix sat-minimize and Generic"); unsigned target_acc; if (type_ == BA) target_acc = 1; @@ -393,10 +404,8 @@ namespace spot // because the input TBA might be smaller. if (state_based_) in = degeneralize(dba); - else if (dba->num_sets() != 1) - in = degeneralize_tba(dba); else - in = dba; + in = degeneralize_tba(dba); } else {