diff --git a/NEWS b/NEWS index 7a3c6b03f..fdb1a187b 100644 --- a/NEWS +++ b/NEWS @@ -218,6 +218,11 @@ New in spot 1.99a (not yet released) - The unused implementation of state-based alternating Büchi automata has been removed. + - Input and output in the old, Spot-specific, text format for + TGBA, has been fully removed. We now use HOA everywhere. (In + case you have a file in this format, install Spot 1.2.6 and use + "src/tgbatest/ltl2tgba -H -X file" to convert the file to HOA.) + New in spot 1.2.6a (not yet released) Nothing yet. diff --git a/doc/org/dstar2tgba.org b/doc/org/dstar2tgba.org index 1a59c5d64..57ed9887b 100644 --- a/doc/org/dstar2tgba.org +++ b/doc/org/dstar2tgba.org @@ -318,8 +318,9 @@ dstar2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' --lbtt[=t] LBTT's format (add =t to force transition-based acceptance even on Büchi automata) --name=FORMAT set the name of the output automaton - -s, --spin Spin neverclaim (implies --ba) - --spot SPOT's format + -s, --spin[=6|c] Spin neverclaim (implies --ba). Add letters to + select (6) Spin's 6.2.4 style, (c) comments on + states --stats=FORMAT output statistics about the automaton #+end_example diff --git a/doc/org/ioltl.org b/doc/org/ioltl.org index f13fd3fd1..b9eacda6d 100644 --- a/doc/org/ioltl.org +++ b/doc/org/ioltl.org @@ -150,8 +150,10 @@ ltlfilt --help | sed -n '/Output options:/,/^$/p' | sed '1d;$d' #+END_SRC #+RESULTS: #+begin_example + -n, --max-count=NUM output at most NUM formulas + -q, --quiet suppress all normal output -8, --utf8 output using UTF-8 characters - --csv quote the formula for use in a CSV file + --csv-escape quote the formula for use in a CSV file --format=FORMAT specify how each line should be output (default: "%f") -l, --lbt output in LBT's syntax diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index 702cb1d69..afff7fddb 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -275,8 +275,9 @@ ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' acceptance even on Büchi automata) --name=FORMAT set the name of the output automaton -q, --quiet suppress all normal output - -s, --spin Spin neverclaim (implies --ba) - --spot SPOT's format + -s, --spin[=6|c] Spin neverclaim (implies --ba). Add letters to + select (6) Spin's 6.2.4 style, (c) comments on + states --stats=FORMAT output statistics about the automaton #+end_example diff --git a/doc/org/oaut.org b/doc/org/oaut.org index fa1186050..a8c4b84dd 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -31,8 +31,9 @@ ltl2tgba --help | sed -n '/Output format:/,/^$/p' | sed '1d;$d' acceptance even on Büchi automata) --name=FORMAT set the name of the output automaton -q, --quiet suppress all normal output - -s, --spin Spin neverclaim (implies --ba) - --spot SPOT's format + -s, --spin[=6|c] Spin neverclaim (implies --ba). Add letters to + select (6) Spin's 6.2.4 style, (c) comments on + states --stats=FORMAT output statistics about the automaton #+end_example @@ -44,14 +45,11 @@ can concatenate multiple automata (and even mix these three formats in the same stream), and the tools will be able to read and process them in sequence. -The other possible outputs are [[http://www.graphviz.org/][GraphViz]] output (=--dot=), Spot's -historical by deprecated format (=--spot=), various statistics -(=--stats=), or nothing at all (=--quiet=). Of course it may seem -strange to ask a tool to not output anything, but it can make sense if +The other possible outputs are [[http://www.graphviz.org/][GraphViz]] output (=--dot=), various +statistics (=--stats=), or nothing at all (=--quiet=). It may seem +strange to ask a tool to not output anything, but it makes sense when only the exit status matters (for instance using [[file:autfilt.org][=autfilt=]] to check -whether an input automaton has some property) or if we are only doing -some timing. - +whether an input automaton has some property) or for timing purposes. * HOAF output diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc index 0031a6518..73b82f38e 100644 --- a/src/bin/common_aoutput.cc +++ b/src/bin/common_aoutput.cc @@ -31,7 +31,6 @@ #include "tgbaalgos/lbtt.hh" #include "tgbaalgos/hoa.hh" #include "tgbaalgos/neverclaim.hh" -#include "tgbaalgos/save.hh" automaton_format_t automaton_format = Dot; static const char* opt_dot = nullptr; @@ -42,9 +41,8 @@ static const char* stats = ""; #define OPT_DOT 1 #define OPT_LBTT 2 -#define OPT_SPOT 3 -#define OPT_STATS 4 -#define OPT_NAME 5 +#define OPT_STATS 3 +#define OPT_NAME 4 static const argp_option options[] = { @@ -68,7 +66,6 @@ static const argp_option options[] = { "spin", 's', "6|c", OPTION_ARG_OPTIONAL, "Spin neverclaim (implies --ba)." " Add letters to select (6) Spin's 6.2.4 style, (c) comments on states", 0 }, - { "spot", OPT_SPOT, 0, 0, "SPOT's format", 0 }, { "utf8", '8', 0, 0, "enable UTF-8 characters in output " "(ignored with --lbtt or --spin)", 0 }, { "stats", OPT_STATS, "FORMAT", 0, @@ -188,9 +185,6 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state*) case OPT_NAME: opt_name = arg; break; - case OPT_SPOT: - automaton_format = Spot; - break; case OPT_STATS: if (!*arg) error(2, 0, "empty format string for --stats"); @@ -248,9 +242,6 @@ automaton_printer::print(const spot::tgba_digraph_ptr& aut, case Hoa: spot::hoa_reachable(std::cout, aut, hoa_opt) << '\n'; break; - case Spot: - spot::tgba_save_reachable(std::cout, aut); - break; case Spin: spot::never_claim_reachable(std::cout, aut, opt_never); break; diff --git a/src/bin/common_aoutput.hh b/src/bin/common_aoutput.hh index 082780dc5..b3f357ba1 100644 --- a/src/bin/common_aoutput.hh +++ b/src/bin/common_aoutput.hh @@ -40,7 +40,6 @@ enum automaton_format_t { Lbtt, Lbtt_t, Spin, - Spot, Stats, Hoa, Quiet, diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index be38c0e3b..5a4d5fb3b 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -34,7 +34,6 @@ #include "tgbaalgos/lbtt.hh" #include "tgbaalgos/hoa.hh" #include "tgbaalgos/neverclaim.hh" -#include "tgbaalgos/save.hh" #include "tgbaalgos/stats.hh" #include "tgba/bddprint.hh" #include "misc/optionmap.hh" @@ -52,9 +51,8 @@ will be output."; #define OPT_TGBA 1 #define OPT_DOT 2 #define OPT_LBTT 3 -#define OPT_SPOT 4 -#define OPT_STATS 5 -#define OPT_NAME 6 +#define OPT_STATS 4 +#define OPT_NAME 5 static const argp_option options[] = { @@ -88,7 +86,6 @@ static const argp_option options[] = { "spin", 's', "6|c", OPTION_ARG_OPTIONAL, "Spin neverclaim (implies --ba)." " Add letters to select (6) Spin's 6.2.4 style, (c) comments on states", 0 }, - { "spot", OPT_SPOT, 0, 0, "SPOT's format", 0 }, { "utf8", '8', 0, 0, "enable UTF-8 characters in output " "(ignored with --lbtt or --spin)", 0 }, { "stats", OPT_STATS, "FORMAT", 0, @@ -134,7 +131,7 @@ static const struct argp_child children[] = { 0, 0, 0, 0 } }; -enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa }; +enum output_format { Dot, Lbtt, Lbtt_t, Spin, Stats, Hoa }; static output_format format = Dot; static const char* opt_dot = nullptr; static const char* stats = ""; @@ -199,9 +196,6 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_NAME: opt_name = arg; break; - case OPT_SPOT: - format = Spot; - break; case OPT_STATS: if (!*arg) error(2, 0, "empty format string for --stats"); @@ -364,9 +358,6 @@ namespace case Hoa: spot::hoa_reachable(std::cout, aut, hoa_opt) << '\n'; break; - case Spot: - spot::tgba_save_reachable(std::cout, aut); - break; case Spin: spot::never_claim_reachable(std::cout, aut, opt_never); break; diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc index 80886b865..5f63a8cdd 100644 --- a/src/ltlvisit/contain.cc +++ b/src/ltlvisit/contain.cc @@ -28,8 +28,6 @@ #include "ltlast/multop.hh" #include "ltlast/constant.hh" #include "tgbaalgos/product.hh" -#include "tgbaalgos/gtec/gtec.hh" -#include "tgbaalgos/save.hh" namespace spot { diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index e80793e76..38c3bdd3f 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -64,7 +64,6 @@ tgbaalgos_HEADERS = \ relabel.hh \ replayrun.hh \ safety.hh \ - save.hh \ sccfilter.hh \ scc.hh \ sccinfo.hh \ @@ -116,7 +115,6 @@ libtgbaalgos_la_SOURCES = \ replayrun.cc \ relabel.cc \ safety.cc \ - save.cc \ scc.cc \ sccinfo.cc \ sccfilter.cc \ diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc deleted file mode 100644 index 9ce00b9c7..000000000 --- a/src/tgbaalgos/save.cc +++ /dev/null @@ -1,86 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2014 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. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include -#include "save.hh" -#include "tgba/bddprint.hh" -#include "ltlvisit/tostring.hh" -#include "ltlast/atomic_prop.hh" -#include "reachiter.hh" -#include "misc/escape.hh" - -namespace spot -{ - namespace - { - class save_bfs: public tgba_reachable_iterator_breadth_first - { - public: - save_bfs(const const_tgba_ptr& a, std::ostream& os) - : tgba_reachable_iterator_breadth_first(a), os_(os) - { - } - - void - start() - { - os_ << "acc = "; - aut_->acc().format_quoted(os_, aut_->acc().all_sets()) - << ";\n"; - } - - void - process_state(const state* s, int, tgba_succ_iterator* si) - { - const bdd_dict_ptr d = aut_->get_dict(); - std::string cur = escape_str(aut_->format_state(s)); - if (si->first()) - do - { - state* dest = si->current_state(); - os_ << '"' << cur << "\", \""; - escape_str(os_, aut_->format_state(dest)); - os_ << "\", \""; - escape_str(os_, bdd_format_formula(d, si->current_condition())); - os_ << "\","; - if (si->current_acceptance_conditions()) - aut_->acc().format_quoted(os_ << ' ', - si->current_acceptance_conditions()); - os_ << ";\n"; - dest->destroy(); - } - while (si->next()); - } - - private: - std::ostream& os_; - }; - } - - std::ostream& - tgba_save_reachable(std::ostream& os, const_tgba_ptr g) - { - save_bfs b(g, os); - b.run(); - return os; - } -} diff --git a/src/tgbaalgos/save.hh b/src/tgbaalgos/save.hh deleted file mode 100644 index 420564934..000000000 --- a/src/tgbaalgos/save.hh +++ /dev/null @@ -1,37 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Developpement -// 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 et Marie Curie. -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#ifndef SPOT_TGBAALGOS_SAVE_HH -# define SPOT_TGBAALGOS_SAVE_HH - -#include "tgba/tgba.hh" -#include - -namespace spot -{ - /// \ingroup tgba_io - /// \brief Save reachable states in text format. - SPOT_API std::ostream& - tgba_save_reachable(std::ostream& os, const_tgba_ptr g); -} - -#endif // SPOT_TGBAALGOS_SAVE_HH diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 7766e605f..328710a93 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -37,7 +37,7 @@ #include "ltlvisit/length.hh" #include "ltlvisit/simplify.hh" #include "tgbaalgos/randomgraph.hh" -#include "tgbaalgos/save.hh" +#include "tgbaalgos/hoa.hh" #include "tgbaalgos/stats.hh" #include "ltlenv/defaultenv.hh" #include "tgbaalgos/dotty.hh" @@ -924,7 +924,7 @@ main(int argc, char** argv) if (!opt_ec) { if (!opt_0 && !opt_dot) - tgba_save_reachable(std::cout, a); + hoa_reachable(std::cout, a, nullptr); } else { diff --git a/src/tgbatest/randtgba.test b/src/tgbatest/randtgba.test index 58a5490a4..debece47b 100755 --- a/src/tgbatest/randtgba.test +++ b/src/tgbatest/randtgba.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2010, 2014 Laboratoire de Recherche et Development de +# Copyright (C) 2010, 2014, 2015 Laboratoire de Recherche et Development de # l'EPITA. # # This file is part of Spot, a model checking library. @@ -23,12 +23,11 @@ set -e for n in 10 20 30 40 50 60 70 80 90 100 200 500 1000; do - # Make sure graph generated by randtgba have successors for each + # Make sure graph generated by randaut have successors for each # of their $n nodes. - r=`../randtgba -n $n a b c | sed -n 's/^"\([0-9]*\)".*/\1/p' | - sort -u | wc -l` - if test "$r" -eq "$n"; then :; else - echo "test failed for n=$n" - exit 1 - fi + ../../bin/randaut -S$n 3 -Hl | + sed 's/.*--BODY--//;s/State:/\n&/g;s/--END--//' > out + grep -q 'State: [0-9][0-9]* .*$' out + grep -q 'State: [0-9]* *$' out && exit 1 done +true diff --git a/wrap/python/spot.i b/wrap/python/spot.i index a39c6805a..d61c5d3f0 100644 --- a/wrap/python/spot.i +++ b/wrap/python/spot.i @@ -122,7 +122,6 @@ namespace std { #include "tgbaalgos/magic.hh" #include "tgbaalgos/minimize.hh" #include "tgbaalgos/neverclaim.hh" -#include "tgbaalgos/save.hh" #include "tgbaalgos/safety.hh" #include "tgbaalgos/sccfilter.hh" #include "tgbaalgos/stats.hh" @@ -253,7 +252,6 @@ namespace spot { %include "tgbaalgos/magic.hh" %include "tgbaalgos/minimize.hh" %include "tgbaalgos/neverclaim.hh" -%include "tgbaalgos/save.hh" %include "tgbaalgos/safety.hh" %include "tgbaalgos/sccfilter.hh" %include "tgbaalgos/stats.hh"