From eed7e2df8feaa34b11c5be94a182bd4300457258 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 9 May 2013 19:13:51 +0200 Subject: [PATCH] lbtt: improve the LBTT output Provide a way to output automata with state-based acceptance. Also print the guards using to_lbt_string() for consistency: as a consequence, atomic proposition that do not match p[0-9]+ are now double-quoted. * src/tgbaalgos/lbtt.hh (lbtt_reachable): Add a sba option. * src/tgbaalgos/lbtt.cc: Implement it, and use to_lbt_string(). * src/ltlvisit/lbt.cc (is_pnum): Reject 'p' without number. * src/bin/ltl2tgba.cc: Activate the sba option of --ba was given. Add an option --lbtt=t to get the old behavior. * src/bin/man/ltl2tgba.x: Document the LBTT format we use with some links and examples. * src/tgbatest/lbttparse.test: More tests. * src/tgbatest/ltlcross2.test: Add a check with --lbtt --ba. * NEWS: Update. --- NEWS | 26 +++++++- src/bin/ltl2tgba.cc | 23 ++++++-- src/bin/man/ltl2tgba.x | 82 ++++++++++++++++++++++++- src/ltlvisit/lbt.cc | 3 +- src/tgbaalgos/lbtt.cc | 115 +++++++++++++++++++++--------------- src/tgbaalgos/lbtt.hh | 10 ++-- src/tgbatest/lbttparse.test | 25 +++++++- src/tgbatest/ltlcross2.test | 1 + 8 files changed, 225 insertions(+), 60 deletions(-) diff --git a/NEWS b/NEWS index b3e69866c..4959d9a22 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,30 @@ New in spot 1.1a (not yet released): - Bug fixes: + * New features: + + - lbtt_reachable(), the function that outputs a TGBA in LBTT's + format, has a new option to indicate that the TGBA being printed + is in fact a Büchi automaton. In this case it outputs an LBTT + automaton with state-based acceptance. + + The output of the guards has also been changed in two ways: + 1. atomic propositions that do not match p[0-9]+ are always + double-quoted. This avoids issues where t or f were used as + atomic propositions in the formula, output as-is in the + automaton, and read back as true or false. Other names that + correspond to LBT operators would cause problem as well. + 2. formulas that label transitions are now output as + irredundant-sums-of-products. + + - 'ltl2tgba --ba --lbtt' will now output automata with state-based + acceptance. You can use 'ltl2tgba --ba --lbtt=t' to force the + output of transition-based acceptance like in the previous + versions. + + Some illustrations of this point and the previous one can be + found in the man page for ltl2tgba(1). + + * Bug fixes: - genltl --gh-r generated the wrong formulas due to a typo. diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index d922ebca2..70cb71bf0 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -67,7 +67,9 @@ static const argp_option options[] = /**************************************************/ { 0, 0, 0, 0, "Output format:", 3 }, { "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 }, - { "lbtt", OPT_LBTT, 0, 0, "LBTT's format", 0 }, + { "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL, + "LBTT's format (add =t to force transition-based acceptance even" + " on Büchi automata)", 0 }, { "spin", 's', 0, 0, "Spin neverclaim (implies --ba)", 0 }, { "spot", OPT_SPOT, 0, 0, "SPOT's format", 0 }, { "utf8", '8', 0, 0, "enable UTF-8 characters in output " @@ -106,7 +108,7 @@ const struct argp_child children[] = { 0, 0, 0, 0 } }; -enum output_format { Dot, Lbtt, Spin, Spot, Stats } format = Dot; +enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats } format = Dot; bool utf8 = false; const char* stats = ""; spot::option_map extra_options; @@ -142,7 +144,17 @@ parse_opt(int key, char* arg, struct argp_state*) format = Dot; break; case OPT_LBTT: - format = Lbtt; + if (arg) + { + if (arg[0] == 't' && arg[1] == 0) + format = Lbtt_t; + else + error(2, 0, "unknown argument for --lbtt: '%s'", arg); + } + else + { + format = Lbtt; + } break; case OPT_SPOT: format = Spot; @@ -220,7 +232,10 @@ namespace || (type == spot::postprocessor::Monitor)); break; case Lbtt: - spot::lbtt_reachable(std::cout, aut); + spot::lbtt_reachable(std::cout, aut, type == spot::postprocessor::BA); + break; + case Lbtt_t: + spot::lbtt_reachable(std::cout, aut, false); break; case Spot: spot::tgba_save_reachable(std::cout, aut); diff --git a/src/bin/man/ltl2tgba.x b/src/bin/man/ltl2tgba.x index 20ddafdbf..554e2e96e 100644 --- a/src/bin/man/ltl2tgba.x +++ b/src/bin/man/ltl2tgba.x @@ -1,6 +1,84 @@ [NAME] ltl2tgba \- translate LTL/PSL formulas into Büchi automata -[DESCRIPTION] -.\" Add any additional description here +[NOTE ON LBTT'S FORMAT] +The format, described at +http://www.tcs.hut.fi/Software/lbtt/doc/html/Format-for-automata.html, +has support for both transition-based and state based generalized acceptance. + +Because Spot uses transition-based generalized Büchi automata +internally, it will normally use the transition-based flavor of that +format, indicated with a 't' flag after the number of acceptance sets. +For instance: + + % bin/ltl2tgba --lbtt 'GFp0 & GFp1 & FGp2' + 2 2t // 2 states, 2 transition-based acceptance sets + 0 1 // state 0: initial + 0 -1 t // trans. to state 0, no acc., label: true + 1 -1 | & p0 p2 & p1 p2 // trans. to state 1, no acc., label: (p0&p2)|(p1&p2) + -1 // end of state 0 + 1 0 // state 1: not initial + 1 0 1 -1 & & p0 p1 p2 // trans. to state 1, acc. 0 and 1, label: p0&p1&p2 + 1 0 -1 & & p1 p2 ! p0 // trans. to state 1, acc. 0, label: !p0&p1&p2 + 1 1 -1 & & p0 p2 ! p1 // trans. to state 1, acc. 1, label: p0&!p1&p2 + 1 -1 & & p2 ! p0 ! p1 // trans. to state 1, no acc., label: !p0&!p1&p2 + -1 // end if state 1 + +Here, the two acceptance sets are represented by the numbers 0 and 1, +and they each contain two transitions (the first transition of state 1 +belongs to both sets). + +When both --ba and --lbtt options are used, the state-based flavor of +the format is used instead. Note that the LBTT format supports +generalized acceptance conditions on states, but Spot only use this +format for Büchi automata, where there is always only one acceptance +set. Unlike in the LBTT documentation, we do not use the +optional 's' flag to indicate the state-based acceptance, this way our +output is also compatible with that of LBT (see +http://www.tcs.hut.fi/Software/maria/tools/lbt/). + + % ltl2tgba --ba --lbtt FGp0 + 2 1 // 2 states, 1 (state-based) accepance set + 0 1 -1 // state 0: initial, non-accepting + 0 t // trans. to state 0, label: true + 1 p0 // trans. to state 1, label: p0 + -1 // end of state 0 + 1 0 0 -1 // state 1: not initial, in acceptance set 0 + 1 p0 // trans. to state 0, label: p0 + -1 // end if state 1 + +You can force ltl2tgba to use the transition-based flavor of the +format even for Büchi automaton using --lbtt=t. + + % ltl2tgba --ba --lbtt=t FGp0 + 2 1t // 2 states, 1 transition-based accepance set. + 0 1 // state 0: initial + 0 -1 t // trans. to state 0, no acc., label: true + 1 -1 p0 // trans. to state 1, no acc., label: p0 + -1 // end of state 0 + 1 0 // state 1: not initial + 1 0 -1 p0 // trans. to state 1, acc. 0, label: p0 + -1 // end if state 1 + +When representing a Büchi automaton using transition-based acceptance, +all transitions leaving accepting states are put into the acceptance set. + +A final note concerns the name of the atomic propositions. The +original LBTT and LBT formats require these atomic propositions to +have names such as 'p0', 'p32', ... We extend the format to accept +atomic proposition with arbitrary names that do not conflict with +LBT's operators (e.g. 'i' is the symbol of the implication operator so +it may not be used as an atomic proposition), or as double-quoted +strings. Spot will always output atomic-proposition that do not match +p[0-9]+ as double-quoted strings. + + % bin/ltl2tgba --lbtt 'GFa & GFb' + 1 2t + 0 1 + 0 0 1 -1 & "a" "b" + 0 0 -1 & "b" ! "a" + 0 1 -1 & "a" ! "b" + 0 -1 & ! "b" ! "a" + -1 + [SEE ALSO] .BR spot-x (7) diff --git a/src/ltlvisit/lbt.cc b/src/ltlvisit/lbt.cc index 826736497..5d657656d 100644 --- a/src/ltlvisit/lbt.cc +++ b/src/ltlvisit/lbt.cc @@ -33,10 +33,11 @@ namespace spot { namespace { + // Does str match p[0-9]+ ? static bool is_pnum(const char* str) { - if (str[0] != 'p') + if (str[0] != 'p' || str[1] == 0) return false; while (*++str) if (*str < '0' || *str > '9') diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index a8360f80b..36f0e40a0 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -25,10 +25,10 @@ #include #include #include -#include "tgba/bddprint.hh" #include "tgba/tgbaexplicit.hh" #include "reachiter.hh" #include "misc/bddlt.hh" +#include "ltlvisit/lbt.hh" #include "ltlparse/public.hh" namespace spot @@ -70,54 +70,64 @@ namespace spot split_map sm; }; - // Convert a BDD formula to the syntax used by LBTT's transition guards. - // Conjunctions are printed by bdd_format_sat, so we just have - // to handle the other cases. - static std::string - bdd_to_lbtt(bdd b, const bdd_dict* d) - { - if (b == bddfalse) - return "f"; - else if (b == bddtrue) - return "t"; - else - { - bdd cube = bdd_satone(b); - b -= cube; - if (b != bddfalse) - { - return "| " + bdd_to_lbtt(b, d) + " " + bdd_to_lbtt(cube, d); - } - else - { - std::string res = ""; - for (int count = bdd_nodecount(cube); count > 1; --count) - res += "& "; - return res + bdd_format_sat(d, cube); - } - } - - } - class lbtt_bfs : public tgba_reachable_iterator_breadth_first { public: - lbtt_bfs(const tgba* a, std::ostream& os) + lbtt_bfs(const tgba* a, std::ostream& os, bool sba_format) : tgba_reachable_iterator_breadth_first(a), os_(os), - acc_count_(a->number_of_acceptance_conditions()), - acs_(a->all_acceptance_conditions()) + all_acc_conds_(a->all_acceptance_conditions()), + acs_(all_acc_conds_), + sba_format_(sba_format), + // If outputting with state-based acceptance, check if the + // automaton can be converted into an sba. This makes the + // state_is_accepting() function more efficient. + sba_(sba_format ? dynamic_cast(a) : 0) { } + bool + state_is_accepting(const state *s) const + { + // If the automaton has a SBA type, it's easier to just query the + // state_is_accepting() method. + if (sba_) + return sba_->state_is_accepting(s); + + // Otherwise, since we are dealing with a degeneralized + // automaton nonetheless, the transitions leaving an accepting + // state are either all accepting, or all non-accepting. So + // we just check the acceptance of the first transition. This + // is not terribly efficient since we have to create the + // iterator. + tgba_succ_iterator* it = aut_->succ_iter(s); + it->first(); + bool accepting = + !it->done() && it->current_acceptance_conditions() == all_acc_conds_; + delete it; + return accepting; + } + + void - process_state(const state*, int n, tgba_succ_iterator*) + process_state(const state* s, int n, tgba_succ_iterator*) { --n; if (n == 0) - body_ << "0 1" << std::endl; + body_ << "0 1"; else - body_ << "-1" << std::endl << n << " 0" << std::endl; + body_ << "-1\n" << n << " 0"; + // Do we have state-based acceptance? + if (sba_format_) + { + // We support only one acceptance condition in the + // state-based format. + if (state_is_accepting(s)) + body_ << " 0 -1"; + else + body_ << " -1"; + } + body_ << "\n"; } void @@ -125,31 +135,44 @@ namespace spot const state*, int out, const tgba_succ_iterator* si) { body_ << out - 1 << " "; - acs_.split(body_, si->current_acceptance_conditions()); - body_ << "-1 " << bdd_to_lbtt(si->current_condition(), - aut_->get_dict()) << std::endl; + if (!sba_format_) + { + acs_.split(body_, si->current_acceptance_conditions()); + body_ << "-1 "; + } + const ltl::formula* f = bdd_to_formula(si->current_condition(), + aut_->get_dict()); + to_lbt_string(f, body_); + f->destroy(); + body_ << "\n"; } void end() { - os_ << seen.size() << " " << acc_count_ << "t" << std::endl - << body_.str() << "-1" << std::endl; + os_ << seen.size() << " "; + if (sba_format_) + os_ << "1"; + else + os_ << aut_->number_of_acceptance_conditions() << "t"; + os_ << "\n" << body_.str() << "-1" << std::endl; } private: std::ostream& os_; std::ostringstream body_; - unsigned acc_count_; + bdd all_acc_conds_; acceptance_cond_splitter acs_; + bool sba_format_; + const sba* sba_; }; } // anonymous std::ostream& - lbtt_reachable(std::ostream& os, const tgba* g) + lbtt_reachable(std::ostream& os, const tgba* g, bool sba) { - lbtt_bfs b(g, os); + lbtt_bfs b(g, os, sba); b.run(); return os; } diff --git a/src/tgbaalgos/lbtt.hh b/src/tgbaalgos/lbtt.hh index a206a3c1b..3c2183648 100644 --- a/src/tgbaalgos/lbtt.hh +++ b/src/tgbaalgos/lbtt.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012 Laboratoire de Recherche et Développement de +// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -29,13 +29,15 @@ namespace spot { - /// \brief Print reachable states in LBTT format. + /// \brief Print reachable states in LBTT's format. /// \ingroup tgba_io /// /// \param g The automata to print. /// \param os Where to print. - std::ostream& lbtt_reachable(std::ostream& os, const tgba* g); - + /// \param sba Assume \a g is an SBA and use LBTT's state-based + /// acceptance format (similar to LBT's format). + std::ostream& lbtt_reachable(std::ostream& os, const tgba* g, + bool sba = false); /// \brief Read an automaton in LBTT's format /// \ingroup tgba_io diff --git a/src/tgbatest/lbttparse.test b/src/tgbatest/lbttparse.test index ff552e94b..c08c70d4c 100755 --- a/src/tgbatest/lbttparse.test +++ b/src/tgbatest/lbttparse.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2012 Laboratoire de Recherche et Développement +# Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -38,8 +38,29 @@ do tr=`cat size | sed -n 's/transitions: //p'` l=`expr $st \* 2 + $tr + 1` test "$s" -eq "$l" -done + # Do the same with bin/ltl2tgba + run 0 ../../bin/ltl2tgba --low --any --lbtt "$f" >out3 + cmp out out3 + head -n 1 out3 | grep t + # Make sure we output the state-based format + # for BA... + run 0 ../../bin/ltl2tgba --ba --lbtt --low --any "$f" >out4 + head -n 1 out4 | grep t && exit 1 + s4=`wc -l < out4` + test "$s" -eq "$s4" + run 0 ../ltl2tgba -t -XL out4 > out5 + s5=`wc -l < out5` + test "$s" -eq "$s5" + # ... unless --lbtt=t is used. + run 0 ../../bin/ltl2tgba --ba --lbtt=t --low --any "$f" >out6 + head -n 1 out6 | grep t + s6=`wc -l < out6` + test "$s" -eq "$s6" + run 0 ../ltl2tgba -t -XL out6 > out7 + s7=`wc -l < out7` + test "$s" -eq "$s7" +done # This is the output of 'lbt' on the formula 'U p0 p1'. cat >Up0p1 <%T" \ "$ltl2tgba --lbtt -x comp-susp,early-susp --lbtt --small %f >%T" \ "$ltl2tgba --lbtt -x comp-susp,!skel-wdba,!skel-simul --lbtt --small %f >%T" \ +"$ltl2tgba --lbtt --ba --high %f > %T" \ --json=output.json --csv=output.csv