From 16a8c0314371a7bf4ff95230199781d47763c342 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 26 Jan 2015 19:28:11 +0100 Subject: [PATCH] ltldo: new binary * src/bin/common_trans.cc, src/bin/common_trans.hh: New files, extracted from... * src/bin/ltlcross.cc: ... here, so that ltldo can use them. * src/bin/ltldo.cc: New file. * src/bin/Makefile.am: Adjust. * src/bin/common_aoutput.cc, src/bin/common_aoutput.hh: Make it possible to add new statistics. * doc/org/ltldo.org: New file. * doc/Makefile.am, doc/org/tools.org: Adjust. * src/bin/man/ltldo.x: New file. * src/bin/man/Makefile.am: Adjust. * src/bin/man/ltlcross.x, src/bin/man/ltlfilt.x: Mention ltldo(1). * src/tgbatest/ltldo.test, src/tgbatest/ltldo2.test: New files. * src/tgbatest/Makefile.am: Add them. * NEWS: Mention ltldo. --- NEWS | 4 + doc/Makefile.am | 1 + doc/org/.gitignore | 1 + doc/org/ltldo.org | 275 ++++++++++++++++++++++++++ doc/org/tools.org | 2 + src/bin/.gitignore | 1 + src/bin/Makefile.am | 19 +- src/bin/common_aoutput.cc | 7 + src/bin/common_aoutput.hh | 4 + src/bin/common_trans.cc | 381 ++++++++++++++++++++++++++++++++++++ src/bin/common_trans.hh | 123 ++++++++++++ src/bin/ltlcross.cc | 393 ++------------------------------------ src/bin/ltldo.cc | 362 +++++++++++++++++++++++++++++++++++ src/bin/man/Makefile.am | 8 +- src/bin/man/ltlcross.x | 5 +- src/bin/man/ltldo.x | 8 + src/bin/man/ltlfilt.x | 5 +- src/tgbatest/Makefile.am | 2 + src/tgbatest/ltldo.test | 54 ++++++ src/tgbatest/ltldo2.test | 31 +++ 20 files changed, 1294 insertions(+), 392 deletions(-) create mode 100644 doc/org/ltldo.org create mode 100644 src/bin/common_trans.cc create mode 100644 src/bin/common_trans.hh create mode 100644 src/bin/ltldo.cc create mode 100644 src/bin/man/ltldo.x create mode 100755 src/tgbatest/ltldo.test create mode 100755 src/tgbatest/ltldo2.test diff --git a/NEWS b/NEWS index 5d5eac861..3bf0da147 100644 --- a/NEWS +++ b/NEWS @@ -20,6 +20,10 @@ New in spot 1.99a (not yet released) - autfilt is a new tool that converts/filters/transforms a stream of automata. + - ltldo is a new tool that run LTL/PSL formulas through other + tools, but uses Spot's command-line interfaces for specifying + input and output. + - "ltlfilt --stutter-invariant" will now work with PSL formula. The implementation is actually much more efficient than the previous implementation that was only for LTL. diff --git a/doc/Makefile.am b/doc/Makefile.am index 60048e3d5..a143b785c 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -69,6 +69,7 @@ ORG_FILES = \ org/ltl2tgba.org \ org/ltl2tgta.org \ org/ltlcross.org \ + org/ltldo.org \ org/ltlfilt.org \ org/ltlgrind.org \ org/oaut.org \ diff --git a/doc/org/.gitignore b/doc/org/.gitignore index c324884bb..58789332e 100644 --- a/doc/org/.gitignore +++ b/doc/org/.gitignore @@ -11,3 +11,4 @@ gfagfb bogus bogus-grind example.hoa +sample.ltl diff --git a/doc/org/ltldo.org b/doc/org/ltldo.org new file mode 100644 index 000000000..3531b846e --- /dev/null +++ b/doc/org/ltldo.org @@ -0,0 +1,275 @@ +# -*- coding: utf-8 -*- +#+TITLE: =ltldo= +#+SETUPFILE: setup.org +#+HTML_LINK_UP: tools.html + +This tool is a wrapper for tools that read LTL/PSL formulas and +(optionally) output automata. + +It reads formulas specified using the [[file:ioltl.org][common options for specifying +input]] and passes each formula to a tool (or a list of tools) specified +using options similar to those of [[file:ltlcross.org][=ltlcross=]]. In case that tool +returns an automaton, the resulting automaton is read back by =ltldo= +and is finally output as specified using the [[file:oaut.org][common options for +outputing automata]]. + +In effect, =ltldo= wraps the I/O interface of the Spot tools on top of +any other tool. + +* Example: computing statistics for =ltl3ba= + +As a motivating example, consider a scenario where we want to run +[[http://sourceforge.net/projects/ltl3ba/][=ltl3ba=]] on a set of 10 formulas stored in a file. For each formula +we would like to compute compute the number of states and edges in the +Büchi automaton produced by =ltl3ba=. + +Here is the input file: + +#+BEGIN_SRC sh :results verbatim :exports code +cat >sample.ltl < Xc) xor Fb +FXb R (a R (1 U b)) +Ga +G(!(c | (a & (a W Gb))) M Xa) +GF((b R !a) U (Xc M 1)) +G(Xb | Gc) +XG!F(a xor Gb) +EOF +#+END_SRC +#+RESULTS: + +We will first implement this scenario without =ltldo=. + +A first problem that the input is not in the correct syntax: although +=ltl3ba= understands =G= and =F=, it does not support =xor= or =M=, +and requires the Boolean operators =||= and =&&=. This syntax +issue can be fixed by processing the input with [[file:ltlfilt.org][=ltlfilt -s=]]. + +A second problem is that =ltl3ba= (at least version 1.1.1) can only +process one formula at a time. So we'll need to call =ltl3ba= in a +loop. + +Finally, one way to compute the size of the resulting Büchi automaton +is to pipe the output of =ltl3ba= through [[file:autfilt.org][=autfilt=]]. + +Here is how the shell command could look like: + +#+BEGIN_SRC sh :results verbatim :exports both +ltlfilt -F sample.ltl -s | +while read f; do + ltl3ba -f "$f" | autfilt --stats="$f,%s,%t" +done +#+END_SRC +#+RESULTS: +#+begin_example +true,1,1 +true U a,2,4 +!(!((a U []b) U b) U []<>a),2,4 +(((!b && !Xc) || (b && Xc)) && !<>b) || (<>b && !((!b && !Xc) || (b && Xc))),7,21 +<>Xb V (a V (true U b)),6,28 +[]a,1,1 +[](Xa U (Xa && !(c || (a && ([]b V (a || []b)))))),1,0 +[]<>((b V !a) U (true U Xc)),2,4 +[](Xb || []c),3,11 +X[]!<>((a && ![]b) || (!a && []b)),4,10 +#+end_example + + +Using =ltldo= the above command can be reduced to this: + +#+BEGIN_SRC sh :results verbatim :exports both +ltldo -F sample.ltl 'ltl3ba -f %s>%N' --stats='%f,%s,%t' +#+END_SRC +#+RESULTS: +#+begin_example +1,1,1 +1 U a,2,4 +!(!((a U Gb) U b) U GFa),2,4 +(b <-> Xc) xor Fb,7,21 +FXb R (a R (1 U b)),6,28 +Ga,1,1 +G(!(c | (a & (a W Gb))) M Xa),1,0 +GF((b R !a) U (Xc M 1)),2,4 +G(Xb | Gc),3,11 +XG!F(a xor Gb),4,10 +#+end_example + +Note that the formulas look different in both cases, because in the +=while= loop the formula printed has already been processed with +=ltlfilt=, while =ltldo= emits the input string untouched. + +* Example: running =spin= and producing HOA + +Here is another example, where we use Spin to produce two automata in +the [[http://adl.github.io/hoaf/][HOA format]]. Spin has no support for HOA, but =ltldo= simply +converts the never claim produced by =spin= into this format. + +#+BEGIN_SRC sh :results verbatim :exports both +ltldo -f a -f GFa 'spin -f %s>%N' -H +#+END_SRC + +#+RESULTS: +#+begin_example +HOA: v1 +States: 2 +Start: 0 +AP: 1 "a" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 {0} +[0] 1 +State: 1 {0} +[t] 1 +--END-- +HOA: v1 +States: 2 +Start: 0 +AP: 1 "a" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc complete +--BODY-- +State: 0 +[0] 1 +[t] 0 +State: 1 {0} +[t] 0 +--END-- +#+end_example + +* Syntax for specifying tools to call + +The syntax for specifying how a tool should be called is the same as +in [[file:ltlcross.org][=ltlcross=]]. Namely, the following sequences are available. + +#+BEGIN_SRC sh :results verbatim :exports results +ltldo --help | sed -n '/character sequences:/,/^$/p' | sed '1d;$d' +#+END_SRC + +#+RESULTS: +: %f,%s,%l,%w the formula as a (quoted) string in Spot, Spin, +: LBT, or Wring's syntax +: %F,%S,%L,%W the formula as a file in Spot, Spin, LBT, or +: Wring's syntax +: %N,%T,%D,%H the automaton is output as a Never claim, or in +: LBTT's, in LTL2DSTAR's, or in the HOA format + +Contrarily to =ltlcross=, it this not mandatory to specify an output filename +using one of the sequence for that later lines. For instance we could +simply run a formula though =echo= to compare different output syntaxes: + +#+BEGIN_SRC sh :results verbatim :exports both +ltldo -f 'p0 U p1' -f 'GFp0' 'echo %f, %s, %l, %w' +#+END_SRC +#+RESULTS: +: (p0) U (p1), (p0) U (p1), U p0 p1, (p0=1) U (p1=1) +: (G(F(p0))), ([](<>(p0))), G F p0, (G(F(p0=1))) + +In this case (i.e., when the command does not specify any output +filename), =ltldo= will not output anything. + + +As will =ltlcross=, multiple commands can be given, and they will be +executed on each formula in the same order. + +A typical use-case is to compare statistics of different tools: + +#+BEGIN_SRC sh :results verbatim :exports both +ltldo -F sample.ltl 'spin -f %s>%N' 'ltl3ba -f %s>%N' --stats=%T,%f,%s,%e +#+END_SRC + +#+RESULTS: +#+begin_example +spin -f %s>%N,1,2,2 +ltl3ba -f %s>%N,1,1,1 +spin -f %s>%N,1 U a,2,3 +ltl3ba -f %s>%N,1 U a,2,3 +spin -f %s>%N,!(!((a U Gb) U b) U GFa),23,86 +ltl3ba -f %s>%N,!(!((a U Gb) U b) U GFa),2,3 +spin -f %s>%N,(b <-> Xc) xor Fb,12,23 +ltl3ba -f %s>%N,(b <-> Xc) xor Fb,7,11 +spin -f %s>%N,FXb R (a R (1 U b)),28,176 +ltl3ba -f %s>%N,FXb R (a R (1 U b)),6,20 +spin -f %s>%N,Ga,1,1 +ltl3ba -f %s>%N,Ga,1,1 +spin -f %s>%N,G(!(c | (a & (a W Gb))) M Xa),15,51 +ltl3ba -f %s>%N,G(!(c | (a & (a W Gb))) M Xa),1,0 +spin -f %s>%N,GF((b R !a) U (Xc M 1)),12,60 +ltl3ba -f %s>%N,GF((b R !a) U (Xc M 1)),2,4 +spin -f %s>%N,G(Xb | Gc),4,8 +ltl3ba -f %s>%N,G(Xb | Gc),3,5 +spin -f %s>%N,XG!F(a xor Gb),8,21 +ltl3ba -f %s>%N,XG!F(a xor Gb),4,7 +#+end_example + +Here we used =%T= to output the name of the tool used to translate the +formula =%f= as an automaton with =%s= states and =%e= edges. +If you feel that =%T= has too much clutter, you can give each tool +a shorter name by prefixing its command with ={name}=. + +In the following example, we moved the formula used on its own line +using the trick that the command =echo %f= will not be subject to +=--stats= (since it does not declare any output automaton). + +#+BEGIN_SRC sh :results verbatim :exports both +ltldo -F sample.ltl --stats=%T,%s,%e \ + 'echo "#" %f' '{spin}spin -f %s>%N' '{ltl3ba}ltl3ba -f %s>%N' +#+END_SRC + +#+RESULTS: +#+begin_example +# (1) +spin,2,2 +ltl3ba,1,1 +# (1) U (a) +spin,2,3 +ltl3ba,2,3 +# (!((!(((a) U (G(b))) U (b))) U (G(F(a))))) +spin,23,86 +ltl3ba,2,3 +# ((b) <-> (X(c))) xor (F(b)) +spin,12,23 +ltl3ba,7,11 +# (F(X(b))) R ((a) R ((1) U (b))) +spin,28,176 +ltl3ba,6,20 +# (G(a)) +spin,1,1 +ltl3ba,1,1 +# (G((!((c) | ((a) & ((a) W (G(b)))))) M (X(a)))) +spin,15,51 +ltl3ba,1,0 +# (G(F(((b) R (!(a))) U ((X(c)) M (1))))) +spin,12,60 +ltl3ba,2,4 +# (G((X(b)) | (G(c)))) +spin,4,8 +ltl3ba,3,5 +# (X(G(!(F((a) xor (G(b))))))) +spin,8,21 +ltl3ba,4,7 +#+end_example + +Much more readable! + +* Controlling and measuring time + +The run time of each command can be restricted with the =-T NUM= +option. The argument is the maximum number of seconds that each +command is allowed to run. + +When a timeout occurs a warning is printed on stderr, and no automaton +(or statistic) is output by =ltdo= for this specific pair of +command/formula. The processing then continue with other formulas and +tools. Timeouts are not considered as errors, so they have no effect +on the exit status of =ltldo=. + +For each command (that does not terminate with a timeout) the runtime +can be printed using the =%r= escape sequence. This makes =ltldo= an +alternative to [[file:ltlcross.org][=ltlcross=]] for running benchmarks without any +verification. diff --git a/doc/org/tools.org b/doc/org/tools.org index 0f6d3e5c8..fa36dc43c 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -48,6 +48,8 @@ corresponding commands are hidden. Büchi automata. - [[file:randaut.org][=randaut=]] Generate random automata. - [[file:autfilt.org][=autfilt=]] Filter and convert automata. +- [[file:ltldo.org][=ltldo=]] Run LTL/PSL formulas through other tools using common [[file:ioltl.org][input]] + and [[file:oaut.org][output]] interfaces. * Advanced use-cases diff --git a/src/bin/.gitignore b/src/bin/.gitignore index 6cf200db9..fbc1b11fd 100644 --- a/src/bin/.gitignore +++ b/src/bin/.gitignore @@ -4,6 +4,7 @@ genltl ltl2tgba ltl2tgta ltlcross +ltldo ltlfilt ltlgrind randaut diff --git a/src/bin/Makefile.am b/src/bin/Makefile.am index 07c1230c5..ce21f16f4 100644 --- a/src/bin/Makefile.am +++ b/src/bin/Makefile.am @@ -44,10 +44,22 @@ libcommon_a_SOURCES = \ common_r.hh \ common_setup.cc \ common_setup.hh \ - common_sys.hh + common_sys.hh \ + common_trans.cc \ + common_trans.hh -bin_PROGRAMS = autfilt ltlfilt genltl randaut randltl ltl2tgba \ - ltl2tgta ltlcross dstar2tgba ltlgrind +bin_PROGRAMS = \ + autfilt \ + dstar2tgba \ + genltl \ + ltl2tgba \ + ltl2tgta \ + ltlcross \ + ltldo \ + ltlfilt \ + ltlgrind \ + randaut \ + randltl # Dummy program used just to generate man/spot-x.7 in a way that is # consistent with the other man pages (e.g., with a version number that @@ -63,6 +75,7 @@ ltl2tgba_SOURCES = ltl2tgba.cc ltl2tgta_SOURCES = ltl2tgta.cc ltlcross_SOURCES = ltlcross.cc ltlgrind_SOURCES = ltlgrind.cc +ltldo_SOURCES = ltldo.cc dstar2tgba_SOURCES = dstar2tgba.cc spot_x_SOURCES = spot-x.cc ltlcross_LDADD = $(LDADD) $(LIB_GETHRXTIME) diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc index 9038f2a14..0031a6518 100644 --- a/src/bin/common_aoutput.cc +++ b/src/bin/common_aoutput.cc @@ -23,6 +23,7 @@ #include "common_aoutput.hh" #include "common_post.hh" #include "common_cout.hh" +#include "common_post.hh" #include "tgba/bddprint.hh" @@ -259,3 +260,9 @@ automaton_printer::print(const spot::tgba_digraph_ptr& aut, } flush_cout(); } + +void automaton_printer::add_stat(char c, const spot::printable* p) +{ + namer.declare(c, p); + statistics.declare(c, p); +} diff --git a/src/bin/common_aoutput.hh b/src/bin/common_aoutput.hh index 595002f28..082780dc5 100644 --- a/src/bin/common_aoutput.hh +++ b/src/bin/common_aoutput.hh @@ -97,6 +97,8 @@ public: declare('w', &aut_word_); } + using spot::formater::declare; + /// \brief print the configured statistics. /// /// The \a f argument is not needed if the Formula does not need @@ -218,6 +220,8 @@ public: // Time and input automaton for statistics double time = 0.0, const spot::const_hoa_aut_ptr& haut = nullptr); + + void add_stat(char c, const spot::printable* p); }; diff --git a/src/bin/common_trans.cc b/src/bin/common_trans.cc new file mode 100644 index 000000000..2f4bba3ac --- /dev/null +++ b/src/bin/common_trans.cc @@ -0,0 +1,381 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// 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 "common_trans.hh" +#include +#include +#include +#include +#include +#include + +#include "error.h" + +#include "ltlvisit/tostring.hh" +#include "ltlvisit/lbt.hh" +#include "common_conv.hh" + +translator_spec::translator_spec(const char* spec) + : spec(spec), cmd(spec), name(spec) +{ + if (*cmd != '{') + return; + + // Match the closing '}' + const char* pos = cmd; + unsigned count = 1; + while (*++pos) + { + if (*pos == '{') + ++count; + else if (*pos == '}') + if (!--count) + { + name = strndup(cmd + 1, pos - cmd - 1); + cmd = pos + 1; + while (*cmd == ' ' || *cmd == '\t') + ++cmd; + break; + } + } +} + +translator_spec::translator_spec(const translator_spec& other) + : spec(other.spec), cmd(other.cmd), name(other.name) +{ + if (name != spec) + name = strdup(name); +} + +translator_spec::~translator_spec() +{ + if (name != spec) + free(const_cast(name)); +} + +std::vector translators; + +void +quoted_string::print(std::ostream& os, const char* pos) const +{ + os << '\''; + this->spot::printable_value::print(os, pos); + os << '\''; +} + +printable_result_filename::printable_result_filename() +{ + val_ = 0; +} + +printable_result_filename::~printable_result_filename() +{ + delete val_; +} + +void printable_result_filename::reset(unsigned n) +{ + translator_num = n; + format = None; +} + +void printable_result_filename::cleanup() +{ + delete val_; + val_ = 0; +} + +void +printable_result_filename::print(std::ostream& os, const char* pos) const +{ + output_format old_format = format; + if (*pos == 'N') + format = Hoa; // The HOA parse also reads neverclaims + else if (*pos == 'T') + format = Lbtt; + else if (*pos == 'D') + format = Dstar; + else if (*pos == 'H') + format = Hoa; + else + SPOT_UNREACHABLE(); + + if (val_) + { + // It's OK to use a specifier multiple time, but it's not OK + // to mix the formats. + if (format != old_format) + error(2, 0, + "you may not mix %%D, %%H, %%N, and %%T specifiers: %s", + translators[translator_num].spec); + } + else + { + char prefix[30]; + snprintf(prefix, sizeof prefix, "lcr-o%u-", translator_num); + const_cast(this)->val_ + = spot::create_tmpfile(prefix); + } + os << '\'' << val_ << '\''; +} + + +translator_runner::translator_runner(spot::bdd_dict_ptr dict, + bool no_output_allowed) + : dict(dict) +{ + declare('f', &string_ltl_spot); + declare('s', &string_ltl_spin); + declare('l', &string_ltl_lbt); + declare('w', &string_ltl_wring); + declare('F', &filename_ltl_spot); + declare('S', &filename_ltl_spin); + declare('L', &filename_ltl_lbt); + declare('W', &filename_ltl_wring); + declare('D', &output); + declare('H', &output); + declare('N', &output); + declare('T', &output); + + size_t s = translators.size(); + assert(s); + for (size_t n = 0; n < s; ++n) + { + // Check that each translator uses at least one input and + // one output. + std::vector has(256); + const translator_spec& t = translators[n]; + scan(t.cmd, has); + if (!(has['f'] || has['s'] || has['l'] || has['w'] + || has['F'] || has['S'] || has['L'] || has['W'])) + error(2, 0, "no input %%-sequence in '%s'.\n Use " + "one of %%f,%%s,%%l,%%w,%%F,%%S,%%L,%%W to indicate how " + "to pass the formula.", t.spec); + if (!no_output_allowed + && !(has['D'] || has['N'] || has['T'] || has['H'])) + error(2, 0, "no output %%-sequence in '%s'.\n Use one of " + "%%D,%%H,%%N,%%T to indicate where the automaton is saved.", + t.spec); + // Remember the %-sequences used by all translators. + prime(t.cmd); + } +} + +void +translator_runner::string_to_tmp(std::string& str, unsigned n, + std::string& tmpname) +{ + char prefix[30]; + snprintf(prefix, sizeof prefix, "lcr-i%u-", n); + spot::open_temporary_file* tmpfile = spot::create_open_tmpfile(prefix); + tmpname = tmpfile->name(); + int fd = tmpfile->fd(); + ssize_t s = str.size(); + if (write(fd, str.c_str(), s) != s + || write(fd, "\n", 1) != 1) + error(2, errno, "failed to write into %s", tmpname.c_str()); + tmpfile->close(); +} + +const std::string& +translator_runner::formula() const +{ + // Pick the most readable format we have... + if (!string_ltl_spot.val().empty()) + return string_ltl_spot; + if (!string_ltl_spin.val().empty()) + return string_ltl_spin; + if (!string_ltl_wring.val().empty()) + return string_ltl_wring; + if (!string_ltl_lbt.val().empty()) + return string_ltl_lbt; + SPOT_UNREACHABLE(); + return string_ltl_spot; +} + +void +translator_runner::round_formula(const spot::ltl::formula* f, unsigned serial) +{ + if (has('f') || has('F')) + string_ltl_spot = spot::ltl::to_string(f, true); + if (has('s') || has('S')) + string_ltl_spin = spot::ltl::to_spin_string(f, true); + if (has('l') || has('L')) + string_ltl_lbt = spot::ltl::to_lbt_string(f); + if (has('w') || has('W')) + string_ltl_wring = spot::ltl::to_wring_string(f); + if (has('F')) + string_to_tmp(string_ltl_spot, serial, filename_ltl_spot); + if (has('S')) + string_to_tmp(string_ltl_spin, serial, filename_ltl_spin); + if (has('L')) + string_to_tmp(string_ltl_lbt, serial, filename_ltl_lbt); + if (has('W')) + string_to_tmp(string_ltl_wring, serial, filename_ltl_wring); +} + + + +volatile bool timed_out = false; +unsigned timeout_count = 0; + +static unsigned timeout = 0; + +#if ENABLE_TIMEOUT +static volatile int alarm_on = 0; +static int child_pid = -1; + +static void +sig_handler(int sig) +{ + if (child_pid == 0) + error(2, 0, "child received signal %d before starting", sig); + + if (sig == SIGALRM && alarm_on) + { + timed_out = true; + if (--alarm_on) + { + // Send SIGTERM to children. + kill(-child_pid, SIGTERM); + // Try again later if it didn't work. (alarm() will be reset + // if it did work and the call to wait() returns) + alarm(2); + } + else + { + // After a few gentle tries, really kill that child. + kill(-child_pid, SIGKILL); + } + } + else + { + // forward signal + kill(-child_pid, sig); + // cleanup files + spot::cleanup_tmpfiles(); + // and die verbosely + error(2, 0, "received signal %d", sig); + } +} + +void +setup_sig_handler() +{ + struct sigaction sa; + sa.sa_handler = sig_handler; + sigemptyset(&sa.sa_mask); + sa.sa_flags = SA_RESTART; // So that wait() doesn't get aborted by SIGALRM. + sigaction(SIGALRM, &sa, 0); + // Catch termination signals, so we can kill the subprocess. + sigaction(SIGHUP, &sa, 0); + sigaction(SIGINT, &sa, 0); + sigaction(SIGQUIT, &sa, 0); + sigaction(SIGTERM, &sa, 0); +} + +int +exec_with_timeout(const char* cmd) +{ + int status; + + timed_out = false; + + child_pid = fork(); + if (child_pid == -1) + error(2, errno, "failed to fork()"); + + if (child_pid == 0) + { + setpgid(0, 0); + execlp("sh", "sh", "-c", cmd, (char*)0); + error(2, errno, "failed to run 'sh'"); + // never reached + return -1; + } + else + { + alarm(timeout); + // Upon SIGALRM, the child will receive up to 3 + // signals: SIGTERM, SIGTERM, SIGKILL. + alarm_on = 3; + int w = waitpid(child_pid, &status, 0); + alarm_on = 0; + + if (w == -1) + error(2, errno, "error during wait()"); + + alarm(0); + } + return status; +} + +static const argp_option options[] = +{ + /**************************************************/ + { 0, 0, 0, 0, "Specifying translators to call:", 2 }, + { "translator", 't', "COMMANDFMT", 0, + "register one translator to call", 0 }, + { "timeout", 'T', "NUMBER", 0, "kill translators after NUMBER seconds", 0 }, + /**************************************************/ + { 0, 0, 0, 0, + "COMMANDFMT should specify input and output arguments using the " + "following character sequences:", 3 }, + { "%f,%s,%l,%w", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "the formula as a (quoted) string in Spot, Spin, LBT, or Wring's syntax", + 0 }, + { "%F,%S,%L,%W", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "the formula as a file in Spot, Spin, LBT, or Wring's syntax", 0 }, + { "%N,%T,%D,%H", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "the automaton is output as a Never claim, or in LBTT's, in LTL2DSTAR's," + " or in the HOA format", 0 }, + { 0, 0, 0, 0, + "If either %l, %L, or %T are used, any input formula that does " + "not use LBT-style atomic propositions (i.e. p0, p1, ...) will be " + "relabeled automatically.\n" + "Furthermore, if COMMANDFMT has the form \"{NAME}CMD\", then only CMD " + "will be passed to the shell, and NAME will be used to name the tool " + "in the output.", 4 }, + { 0, 0, 0, 0, 0, 0 } +}; + +static int parse_opt_trans(int key, char* arg, struct argp_state*) +{ + switch (key) + { + case 't': + translators.push_back(arg); + break; + case 'T': + timeout = to_pos_int(arg); +#if !ENABLE_TIMEOUT + std::cerr << "warning: setting a timeout is not supported " + << "on your platform" << std::endl; +#endif + break; + default: + return ARGP_ERR_UNKNOWN; + } + return 0; +} + +const struct argp trans_argp { options, parse_opt_trans, 0, 0, 0, 0, 0 }; + + +#endif // ENABLE_TIMEOUT diff --git a/src/bin/common_trans.hh b/src/bin/common_trans.hh new file mode 100644 index 000000000..f847e4031 --- /dev/null +++ b/src/bin/common_trans.hh @@ -0,0 +1,123 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// 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_BIN_COMMON_TRANS_HH +#define SPOT_BIN_COMMON_TRANS_HH + +#include "common_sys.hh" +#include +#include + +#include "misc/formater.hh" +#include "misc/tmpfile.hh" +#include "tgba/tgbagraph.hh" + + +extern const struct argp trans_argp; + +struct translator_spec +{ + // The translator command, as specified on the command-line. + // If this has the form of + // {name}cmd + // then it is split in two components. + // Otherwise, spec=cmd=name. + const char* spec; + // actual shell command (or spec) + const char* cmd; + // name of the translator (or spec) + const char* name; + + translator_spec(const char* spec); + translator_spec(const translator_spec& other); + ~translator_spec(); +}; + +extern std::vector translators; + +struct quoted_string final: public spot::printable_value +{ + using spot::printable_value::operator=; + void print(std::ostream& os, const char* pos) const override; +}; + +struct printable_result_filename final: + public spot::printable_value +{ + unsigned translator_num; + enum output_format { None, Lbtt, Dstar, Hoa }; + mutable output_format format; + + printable_result_filename(); + ~printable_result_filename(); + void reset(unsigned n); + void cleanup(); + + void print(std::ostream& os, const char* pos) const override; +}; + + +class translator_runner: protected spot::formater +{ +protected: + spot::bdd_dict_ptr dict; + // Round-specific variables + quoted_string string_ltl_spot; + quoted_string string_ltl_spin; + quoted_string string_ltl_lbt; + quoted_string string_ltl_wring; + quoted_string filename_ltl_spot; + quoted_string filename_ltl_spin; + quoted_string filename_ltl_lbt; + quoted_string filename_ltl_wring; + // Run-specific variables + printable_result_filename output; +public: + using spot::formater::has; + + translator_runner(spot::bdd_dict_ptr dict, + // whether we accept the absence of output + // specifier + bool no_output_allowed = false); + void string_to_tmp(std::string& str, unsigned n, std::string& tmpname); + const std::string& formula() const; + void round_formula(const spot::ltl::formula* f, unsigned serial); +}; + + +// Disable handling of timeout on systems that miss kill() or alarm(). +// For instance MinGW. +#if HAVE_KILL && HAVE_ALARM +# define ENABLE_TIMEOUT 1 +#else +# define ENABLE_TIMEOUT 0 +#endif + +extern volatile bool timed_out; +extern unsigned timeout_count; +#if ENABLE_TIMEOUT +void setup_sig_handler(); +int exec_with_timeout(const char* cmd); +#else // !ENABLE_TIMEOUT +#define exec_with_timeout(cmd) system(cmd) +#define setup_sig_handler() while (0); +#endif // !ENABLE_TIMEOUT + + +#endif // SPOT_BIN_COMMON_TRANS_HH diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index ab3831cc3..d04e9f962 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -27,24 +27,23 @@ #include #include #include -#include #include -#include #include "error.h" #include "argmatch.h" #include "common_setup.hh" #include "common_cout.hh" #include "common_conv.hh" +#include "common_trans.hh" #include "common_finput.hh" #include "dstarparse/public.hh" #include "hoaparse/public.hh" #include "ltlast/unop.hh" #include "ltlvisit/tostring.hh" #include "ltlvisit/apcollect.hh" -#include "ltlvisit/lbt.hh" #include "ltlvisit/mutation.hh" #include "ltlvisit/relabel.hh" +#include "ltlvisit/lbt.hh" #include "tgbaalgos/lbtt.hh" #include "tgbaalgos/product.hh" #include "tgbaalgos/gtec/gtec.hh" @@ -63,14 +62,6 @@ #include "misc/tmpfile.hh" #include "misc/timer.hh" -// Disable handling of timeout on systems that miss kill() or alarm(). -// For instance MinGW. -#if HAVE_KILL && HAVE_ALARM -# define ENABLE_TIMEOUT 1 -#else -# define ENABLE_TIMEOUT 0 -#endif - const char argp_program_doc[] ="\ Call several LTL/PSL translators and cross-compare their output to detect \ bugs, or to gather statistics. The list of formulas to use should be \ @@ -102,31 +93,7 @@ Exit status:\n\ static const argp_option options[] = { /**************************************************/ - { 0, 0, 0, 0, "Specifying translators to call:", 2 }, - { "translator", 't', "COMMANDFMT", 0, - "register one translator to call", 0 }, - { "timeout", 'T', "NUMBER", 0, "kill translators after NUMBER seconds", 0 }, - /**************************************************/ - { 0, 0, 0, 0, - "COMMANDFMT should specify input and output arguments using the " - "following character sequences:", 3 }, - { "%f,%s,%l,%w", 0, 0, OPTION_DOC | OPTION_NO_USAGE, - "the formula as a (quoted) string in Spot, Spin, LBT, or Wring's syntax", - 0 }, - { "%F,%S,%L,%W", 0, 0, OPTION_DOC | OPTION_NO_USAGE, - "the formula as a file in Spot, Spin, LBT, or Wring's syntax", 0 }, - { "%N,%T,%D,%H", 0, 0, OPTION_DOC | OPTION_NO_USAGE, - "the automaton is output as a Never claim, or in LBTT's, in LTL2DSTAR's," - "or in the HOA format", 0 }, - { 0, 0, 0, 0, - "If either %l, %L, or %T are used, any input formula that does " - "not use LBT-style atomic propositions (i.e. p0, p1, ...) will be " - "relabeled automatically.\n" - "Furthermore, if COMMANDFMT has the form \"{NAME}CMD\", then only CMD " - "will be passed to the shell, and NAME will be used to name the tool " - "in the CSV or JSON outputs.", 0 }, - /**************************************************/ - { 0, 0, 0, 0, "ltlcross behavior:", 4 }, + { 0, 0, 0, 0, "ltlcross behavior:", 5 }, { "allow-dups", OPT_DUPS, 0, 0, "translate duplicate formulas in input", 0 }, { "no-checks", OPT_NOCHECKS, 0, 0, @@ -138,7 +105,7 @@ static const argp_option options[] = "stop on first execution error or failure to pass" " sanity checks (timeouts are OK)", 0 }, /**************************************************/ - { 0, 0, 0, 0, "State-space generation:", 5 }, + { 0, 0, 0, 0, "State-space generation:", 6 }, { "states", OPT_STATES, "INT", 0, "number of the states in the state-spaces (200 by default)", 0 }, { "density", OPT_DENSITY, "FLOAT", 0, @@ -150,7 +117,7 @@ static const argp_option options[] = "number of products to perform (1 by default), statistics will be " "averaged unless the number is prefixed with '+'", 0 }, /**************************************************/ - { 0, 0, 0, 0, "Statistics output:", 6 }, + { 0, 0, 0, 0, "Statistics output:", 7 }, { "json", OPT_JSON, "FILENAME", OPTION_ARG_OPTIONAL, "output statistics as JSON in FILENAME or on standard output", 0 }, { "csv", OPT_CSV, "FILENAME", OPTION_ARG_OPTIONAL, @@ -176,6 +143,7 @@ static const argp_option options[] = const struct argp_child children[] = { { &finput_argp, 0, 0, 1 }, + { &trans_argp, 0, 0, 0 }, { &misc_argp, 0, 0, -1 }, { 0, 0, 0, 0 } }; @@ -204,7 +172,6 @@ const char* reset_color = "\033[m"; unsigned states = 200; float density = 0.1; -unsigned timeout = 0; const char* json_output = 0; const char* csv_output = 0; bool want_stats = false; @@ -222,59 +189,6 @@ std::ofstream* bogus_output = 0; std::ofstream* grind_output = 0; bool verbose = false; -struct translator_spec -{ - // The translator command, as specified on the command-line. - // If this has the form of - // {name}cmd - // then it is split in two components. - // Otherwise, spec=cmd=name. - const char* spec; - // actual shell command (or spec) - const char* cmd; - // name of the translator (or spec) - const char* name; - - translator_spec(const char* spec) - : spec(spec), cmd(spec), name(spec) - { - if (*cmd != '{') - return; - - // Match the closing '}' - const char* pos = cmd; - unsigned count = 1; - while (*++pos) - { - if (*pos == '{') - ++count; - else if (*pos == '}') - if (!--count) - { - name = strndup(cmd + 1, pos - cmd - 1); - cmd = pos + 1; - while (*cmd == ' ' || *cmd == '\t') - ++cmd; - break; - } - } - } - - translator_spec(const translator_spec& other) - : spec(other.spec), cmd(other.cmd), name(other.name) - { - if (name != spec) - name = strdup(name); - } - - ~translator_spec() - { - if (name != spec) - free(const_cast(name)); - } -}; - -std::vector translators; bool global_error_flag = false; @@ -473,17 +387,9 @@ parse_opt(int key, char* arg, struct argp_state*) // This switch is alphabetically-ordered. switch (key) { - case 't': case ARGP_KEY_ARG: translators.push_back(arg); break; - case 'T': - timeout = to_pos_int(arg); -#if !ENABLE_TIMEOUT - std::cerr << "warning: setting a timeout is not supported " - << "on your platform" << std::endl; -#endif - break; case OPT_BOGUS: { bogus_output = new std::ofstream(arg); @@ -555,292 +461,15 @@ parse_opt(int key, char* arg, struct argp_state*) return 0; } -static volatile bool timed_out = false; -unsigned timeout_count = 0; - -#if ENABLE_TIMEOUT -static volatile int alarm_on = 0; -static int child_pid = -1; - -static void -sig_handler(int sig) -{ - if (child_pid == 0) - error(2, 0, "child received signal %d before starting", sig); - - if (sig == SIGALRM && alarm_on) - { - timed_out = true; - if (--alarm_on) - { - // Send SIGTERM to children. - kill(-child_pid, SIGTERM); - // Try again later if it didn't work. (alarm() will be reset - // if it did work and the call to wait() returns) - alarm(2); - } - else - { - // After a few gentle tries, really kill that child. - kill(-child_pid, SIGKILL); - } - } - else - { - // forward signal - kill(-child_pid, sig); - // cleanup files - spot::cleanup_tmpfiles(); - // and die verbosely - error(2, 0, "received signal %d", sig); - } -} - -static void -setup_sig_handler() -{ - struct sigaction sa; - sa.sa_handler = sig_handler; - sigemptyset(&sa.sa_mask); - sa.sa_flags = SA_RESTART; // So that wait() doesn't get aborted by SIGALRM. - sigaction(SIGALRM, &sa, 0); - // Catch termination signals, so we can kill the subprocess. - sigaction(SIGHUP, &sa, 0); - sigaction(SIGINT, &sa, 0); - sigaction(SIGQUIT, &sa, 0); - sigaction(SIGTERM, &sa, 0); -} - -static int -exec_with_timeout(const char* cmd) -{ - int status; - - timed_out = false; - - child_pid = fork(); - if (child_pid == -1) - error(2, errno, "failed to fork()"); - - if (child_pid == 0) - { - setpgid(0, 0); - execlp("sh", "sh", "-c", cmd, (char*)0); - error(2, errno, "failed to run 'sh'"); - // never reached - return -1; - } - else - { - alarm(timeout); - // Upon SIGALRM, the child will receive up to 3 - // signals: SIGTERM, SIGTERM, SIGKILL. - alarm_on = 3; - int w = waitpid(child_pid, &status, 0); - alarm_on = 0; - - if (w == -1) - error(2, errno, "error during wait()"); - - alarm(0); - } - return status; -} -#else // !ENABLE_TIMEOUT -#define exec_with_timeout(cmd) system(cmd) -#define setup_sig_handler() while (0); -#endif // !ENABLE_TIMEOUT - namespace { - struct quoted_string: public spot::printable_value + class xtranslator_runner: public translator_runner { - using spot::printable_value::operator=; - - void - print(std::ostream& os, const char* pos) const - { - os << '\''; - this->spot::printable_value::print(os, pos); - os << '\''; - } - }; - - struct printable_result_filename: - public spot::printable_value - { - unsigned translator_num; - enum output_format { None, Lbtt, Dstar, Hoa }; - mutable output_format format; - - printable_result_filename() - { - val_ = 0; - } - - ~printable_result_filename() - { - delete val_; - } - - void reset(unsigned n) - { - translator_num = n; - format = None; - } - - void cleanup() - { - delete val_; - val_ = 0; - } - - void - print(std::ostream& os, const char* pos) const - { - output_format old_format = format; - if (*pos == 'N') - format = Hoa; // The HOA parse also reads neverclaims - else if (*pos == 'T') - format = Lbtt; - else if (*pos == 'D') - format = Dstar; - else if (*pos == 'H') - format = Hoa; - else - SPOT_UNREACHABLE(); - - if (val_) - { - // It's OK to use a specified multiple time, but it's not OK - // to mix the formats. - if (format != old_format) - error(2, 0, - "you may not mix %%D, %%H, %%N, and %%T specifiers: %s", - translators[translator_num].spec); - } - else - { - char prefix[30]; - snprintf(prefix, sizeof prefix, "lcr-o%u-", translator_num); - const_cast(this)->val_ - = spot::create_tmpfile(prefix); - } - os << '\'' << val_ << '\''; - } - }; - - class translator_runner: protected spot::formater - { - private: - spot::bdd_dict_ptr dict; - // Round-specific variables - quoted_string string_ltl_spot; - quoted_string string_ltl_spin; - quoted_string string_ltl_lbt; - quoted_string string_ltl_wring; - quoted_string filename_ltl_spot; - quoted_string filename_ltl_spin; - quoted_string filename_ltl_lbt; - quoted_string filename_ltl_wring; - // Run-specific variables - printable_result_filename output; public: - using spot::formater::has; - - translator_runner(spot::bdd_dict_ptr dict) - : dict(dict) + xtranslator_runner(spot::bdd_dict_ptr dict) + : translator_runner(dict) { - declare('f', &string_ltl_spot); - declare('s', &string_ltl_spin); - declare('l', &string_ltl_lbt); - declare('w', &string_ltl_wring); - declare('F', &filename_ltl_spot); - declare('S', &filename_ltl_spin); - declare('L', &filename_ltl_lbt); - declare('W', &filename_ltl_wring); - declare('D', &output); - declare('H', &output); - declare('N', &output); - declare('T', &output); - - size_t s = translators.size(); - assert(s); - for (size_t n = 0; n < s; ++n) - { - // Check that each translator uses at least one input and - // one output. - std::vector has(256); - const translator_spec& t = translators[n]; - scan(t.cmd, has); - if (!(has['f'] || has['s'] || has['l'] || has['w'] - || has['F'] || has['S'] || has['L'] || has['W'])) - error(2, 0, "no input %%-sequence in '%s'.\n Use " - "one of %%f,%%s,%%l,%%w,%%F,%%S,%%L,%%W to indicate how " - "to pass the formula.", t.spec); - bool has_d = has['D']; - if (!(has_d || has['N'] || has['T'] || has['H'])) - error(2, 0, "no output %%-sequence in '%s'.\n Use one of " - "%%D,%%H,%%N,%%T to indicate where the automaton is saved.", - t.spec); - has_sr |= has_d; - - // Remember the %-sequences used by all translators. - prime(t.cmd); - } - - } - - void - string_to_tmp(std::string& str, unsigned n, std::string& tmpname) - { - char prefix[30]; - snprintf(prefix, sizeof prefix, "lcr-i%u-", n); - spot::open_temporary_file* tmpfile = spot::create_open_tmpfile(prefix); - tmpname = tmpfile->name(); - int fd = tmpfile->fd(); - ssize_t s = str.size(); - if (write(fd, str.c_str(), s) != s - || write(fd, "\n", 1) != 1) - error(2, errno, "failed to write into %s", tmpname.c_str()); - tmpfile->close(); - } - - const std::string& - formula() const - { - // Pick the most readable format we have... - if (!string_ltl_spot.val().empty()) - return string_ltl_spot; - if (!string_ltl_spin.val().empty()) - return string_ltl_spin; - if (!string_ltl_wring.val().empty()) - return string_ltl_wring; - if (!string_ltl_lbt.val().empty()) - return string_ltl_lbt; - SPOT_UNREACHABLE(); - return string_ltl_spot; - } - - void - round_formula(const spot::ltl::formula* f, unsigned serial) - { - if (has('f') || has('F')) - string_ltl_spot = spot::ltl::to_string(f, true); - if (has('s') || has('S')) - string_ltl_spin = spot::ltl::to_spin_string(f, true); - if (has('l') || has('L')) - string_ltl_lbt = spot::ltl::to_lbt_string(f); - if (has('w') || has('W')) - string_ltl_wring = spot::ltl::to_wring_string(f); - if (has('F')) - string_to_tmp(string_ltl_spot, serial, filename_ltl_spot); - if (has('S')) - string_to_tmp(string_ltl_spin, serial, filename_ltl_spin); - if (has('L')) - string_to_tmp(string_ltl_lbt, serial, filename_ltl_lbt); - if (has('W')) - string_to_tmp(string_ltl_wring, serial, filename_ltl_wring); + has_sr = has('D'); } spot::const_tgba_digraph_ptr @@ -1230,7 +859,7 @@ namespace class processor: public job_processor { spot::bdd_dict_ptr dict = spot::make_bdd_dict(); - translator_runner runner; + xtranslator_runner runner; fset_t unique_set; public: processor(): diff --git a/src/bin/ltldo.cc b/src/bin/ltldo.cc new file mode 100644 index 000000000..0399b1f88 --- /dev/null +++ b/src/bin/ltldo.cc @@ -0,0 +1,362 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// 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 "common_sys.hh" + +#include +#include +#include +#include + +#include "error.h" + +#include "common_setup.hh" +#include "common_cout.hh" +#include "common_conv.hh" +#include "common_finput.hh" +#include "common_aoutput.hh" +#include "common_post.hh" +#include "common_trans.hh" + +#include "ltlvisit/tostring.hh" +#include "misc/timer.hh" +#include "tgbaalgos/lbtt.hh" +#include "hoaparse/public.hh" +#include "dstarparse/public.hh" + +const char argp_program_doc[] ="\ +Run LTL/PSL formulas through another program, performing conversion\n\ +of input and output as required."; + +static const argp_option options[] = + { + { 0, 0, 0, 0, "Miscellaneous options:", -1 }, + { 0, 0, 0, 0, 0, 0 } + }; + + +static const argp_option more_o_format[] = + { + { "%R", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "serial number of the formula translated", 0 }, + { "%T", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "tool used for translation", 0 }, + { "%f", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "formula translated", 0 }, + { 0, 0, 0, 0, 0, 0 } + }; + +// This is not very elegant, but we need to add the above %-escape +// sequences to those of aoutput_o_fromat_argp for the --help output. +// So far I've failed to instruct argp to merge those two lists into a +// single block. +static const struct argp* +build_percent_list() +{ + const argp_option* iter = aoutput_o_format_argp.options; + unsigned count = 0; + while (iter->name || iter->doc) + { + ++count; + ++iter; + } + + unsigned s = count * sizeof(argp_option); + argp_option* d = + static_cast(malloc(sizeof(more_o_format) + s)); + memcpy(d, aoutput_o_format_argp.options, s); + memcpy(d + count, more_o_format, sizeof(more_o_format)); + + static const struct argp more_o_format_argp = + { d, 0, 0, 0, 0, 0, 0 }; + return &more_o_format_argp; +} + +const struct argp_child children[] = + { + { &finput_argp, 0, 0, 1 }, + { &trans_argp, 0, 0, 3 }, + { &aoutput_argp, 0, 0, 4 }, + { build_percent_list(), 0, 0, 5 }, + { &misc_argp, 0, 0, -1 }, + { 0, 0, 0, 0 } + }; + +static int +parse_opt(int key, char* arg, struct argp_state*) +{ + switch (key) + { + case ARGP_KEY_ARG: + translators.push_back(arg); + break; + default: + return ARGP_ERR_UNKNOWN; + } + return 0; +} + +namespace +{ + class xtranslator_runner: public translator_runner + { + public: + xtranslator_runner(spot::bdd_dict_ptr dict) + : translator_runner(dict, true) + { + } + + spot::tgba_digraph_ptr + translate(unsigned int translator_num, bool& problem, double& duration) + { + output.reset(translator_num); + + std::ostringstream command; + format(command, translators[translator_num].cmd); + + //assert(output.format != printable_result_filename::None); + + std::string cmd = command.str(); + //std::cerr << "Running [" << l << translator_num << "]: " + // << cmd << std::endl; + spot::stopwatch sw; + sw.start(); + int es = exec_with_timeout(cmd.c_str()); + duration = sw.stop(); + + spot::tgba_digraph_ptr res = nullptr; + if (timed_out) + { + problem = false; // A timeout is considered benign + std::cerr << "warning: timeout during execution of command \"" + << cmd << "\"\n"; + ++timeout_count; + } + else if (WIFSIGNALED(es)) + { + problem = true; + es = WTERMSIG(es); + std::cerr << "error: execution of command \"" << cmd + << "\" terminated by signal " << es << ".\n"; + } + else if (WIFEXITED(es) && WEXITSTATUS(es) != 0) + { + problem = true; + es = WEXITSTATUS(es); + std::cerr << "error: execution of command \"" << cmd + << "\" returned exit code " << es << ".\n"; + } + else + { + problem = false; + switch (output.format) + { + case printable_result_filename::Lbtt: + { + std::string error; + std::ifstream f(output.val()->name()); + if (!f) + { + problem = true; + std::cerr << "error: could not open " << output.val() + << " after running \"" << cmd << "\".\n"; + } + else + { + res = spot::lbtt_parse(f, error, dict); + if (!res) + { + problem = true; + std::cerr << "error: failed to parse output of \"" + << cmd << "\" in LBTT format:\n" + << "error: " << error << '\n'; + } + } + break; + } + case printable_result_filename::Dstar: + { + spot::dstar_parse_error_list pel; + std::string filename = output.val()->name(); + auto aut = spot::dstar_parse(filename, pel, dict); + if (!pel.empty()) + { + problem = true; + std::cerr << "error: failed to parse the output of \"" + << cmd << "\" as a DSTAR automaton.\n"; + spot::format_dstar_parse_errors(std::cerr, filename, pel); + res = nullptr; + } + else + { + res = dstar_to_tgba(aut); + } + break; + } + case printable_result_filename::Hoa: // Will also read neverclaims + { + spot::hoa_parse_error_list pel; + std::string filename = output.val()->name(); + auto aut = spot::hoa_parse(filename, pel, dict); + if (!pel.empty()) + { + problem = true; + std::cerr << "error: failed to parse the automaton " + "produced by \"" << cmd << "\".\n"; + spot::format_hoa_parse_errors(std::cerr, filename, pel); + res = nullptr; + } + else if (aut->aborted) + { + problem = true; + std::cerr << "error: command \"" << cmd + << "\" aborted its output.\n"; + res = nullptr; + } + else + { + res = aut->aut; + } + } + break; + case printable_result_filename::None: + problem = false; + res = nullptr; + break; + } + } + + output.cleanup(); + return res; + } + }; + + + class processor: public job_processor + { + spot::bdd_dict_ptr dict = spot::make_bdd_dict(); + xtranslator_runner runner; + automaton_printer printer; + spot::postprocessor& post; + spot::printable_value cmdname; + spot::printable_value roundval; + spot::printable_value inputf; + + public: + processor(spot::postprocessor& post) + : runner(dict), post(post) + { + printer.add_stat('T', &cmdname); + printer.add_stat('R', &roundval); + printer.add_stat('f', &inputf); + } + + ~processor() + { + } + + int + process_string(const std::string& input, + const char* filename, + int linenum) + { + spot::ltl::parse_error_list pel; + const spot::ltl::formula* f = parse_formula(input, pel); + + if (!f || !pel.empty()) + { + if (filename) + error_at_line(0, 0, filename, linenum, "parse error:"); + spot::ltl::format_parse_errors(std::cerr, input, pel); + if (f) + f->destroy(); + return 1; + } + + inputf = input; + process_formula(f, filename, linenum); + f->destroy(); + return 0; + } + + + int + process_formula(const spot::ltl::formula* f, + const char* filename = 0, int linenum = 0) + { + static unsigned round = 0; + runner.round_formula(f, round); + + unsigned ts = translators.size(); + for (unsigned t = 0; t < ts; ++t) + { + bool problem; + double translation_time; + auto aut = runner.translate(t, problem, translation_time); + if (problem) + error_at_line(2, 0, filename, linenum, "aborting here"); + if (aut) + { + aut = post.run(aut, f); + cmdname = translators[t].name; + roundval = round; + printer.print(aut, f, filename, linenum, translation_time, + nullptr); + }; + } + ++round; + return 0; + } + }; +} + +int +main(int argc, char** argv) +{ + setup(argv); + + const argp ap = { options, parse_opt, "[COMMANDFMT...]", + argp_program_doc, children, 0, 0 }; + + // Disable post-processing as much as possible by default. + level = spot::postprocessor::Low; + pref = spot::postprocessor::Any; + if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0)) + exit(err); + + if (jobs.empty()) + jobs.emplace_back("-", 1); + + if (translators.empty()) + error(2, 0, "No translator to run? Run '%s --help' for usage.", + program_name); + + setup_sig_handler(); + + spot::postprocessor post; + post.set_pref(pref | comp); + post.set_type(type); + post.set_level(level); + + processor p(post); + if (p.run()) + return 2; + + return 0; +} diff --git a/src/bin/man/Makefile.am b/src/bin/man/Makefile.am index 9f32a687d..3e4f39bc3 100644 --- a/src/bin/man/Makefile.am +++ b/src/bin/man/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et Développement -## de l'Epita (LRDE). +## Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et +## Développement de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. ## @@ -29,6 +29,7 @@ dist_man1_MANS = \ ltl2tgba.1 \ ltl2tgta.1 \ ltlcross.1 \ + ltldo.1 \ ltlfilt.1 \ ltlgrind.1 \ randaut.1 \ @@ -54,6 +55,9 @@ ltl2tgta.1: $(common_dep) $(srcdir)/ltl2tgta.x $(srcdir)/../ltl2tgta.cc ltlcross.1: $(common_dep) $(srcdir)/ltlcross.x $(srcdir)/../ltlcross.cc $(convman) ../ltlcross$(EXEEXT) $(srcdir)/ltlcross.x $@ +ltldo.1: $(common_dep) $(srcdir)/ltlcross.x $(srcdir)/../ltldo.cc + $(convman) ../ltldo$(EXEEXT) $(srcdir)/ltldo.x $@ + ltlfilt.1: $(common_dep) $(srcdir)/ltlfilt.x $(srcdir)/../ltlfilt.cc $(convman) ../ltlfilt$(EXEEXT) $(srcdir)/ltlfilt.x $@ diff --git a/src/bin/man/ltlcross.x b/src/bin/man/ltlcross.x index 232d875b6..7508d4cd8 100644 --- a/src/bin/man/ltlcross.x +++ b/src/bin/man/ltlcross.x @@ -192,7 +192,8 @@ over the \fIN\fR products performed. .BR randltl (1), .BR genltl (1), .BR ltlfilt (1), -.BR ltl2tgba (1) +.BR ltl2tgba (1), +.BR ltldo (1) [BIBLIOGRAPHY] If you would like to give a reference to this tool in an article, @@ -230,5 +231,3 @@ checking the emptiness of Comp(P1)*P2. Our implementation will detect and reports problems (like inconsistencies between two translations) but unlike LBTT it does not offer an interactive mode to investigate such problems. - - diff --git a/src/bin/man/ltldo.x b/src/bin/man/ltldo.x new file mode 100644 index 000000000..f4a8e48ff --- /dev/null +++ b/src/bin/man/ltldo.x @@ -0,0 +1,8 @@ +[NAME] +ltldo \- run LTL/PSL formulas through other tools +[SEE ALSO] +.BR randltl (1), +.BR genltl (1), +.BR ltlfilt (1), +.BR ltl2tgba (1), +.BR ltldo (1) diff --git a/src/bin/man/ltlfilt.x b/src/bin/man/ltlfilt.x index 51a5313ec..7ef700249 100644 --- a/src/bin/man/ltlfilt.x +++ b/src/bin/man/ltlfilt.x @@ -10,7 +10,7 @@ we suggest you cite the following paper: Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0. Proceedings of ATVA'13. LNCS 8172. .PP -The following papers describes algorithms used by ltlfilt: +The following papers describe algorithms used by ltlfilt: .TP \(bu Kousha Etessami: A note on a question of Peled and Wilke regarding @@ -44,4 +44,5 @@ Automata. Proceedings of CONCUR'00. LNCS 1877. Describe the syntactic LTL classes matched by \fB\-\-eventual\fR, and \fB\-\-universal\fR. [SEE ALSO] -.BR randltl (1) +.BR randltl (1), +.BR ltldo (1) diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index a3cb6c901..359f92508 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -83,6 +83,8 @@ TESTS = \ hoaparse.test \ dstar.test \ readsave.test \ + ltldo.test \ + ltldo2.test \ maskacc.test \ simdet.test \ sim2.test \ diff --git a/src/tgbatest/ltldo.test b/src/tgbatest/ltldo.test new file mode 100755 index 000000000..b65640d6e --- /dev/null +++ b/src/tgbatest/ltldo.test @@ -0,0 +1,54 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2015 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). +# +# 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 . + +. ./defs +set -e + +ltldo=../../bin/ltldo +ltl2tgba=../../bin/ltl2tgba +genltl=../../bin/genltl + +run 0 $ltldo -f a -f 'a&b' -t 'echo %f,%s' >output +cat >expected <output 2>stderr +test -z "`cat output`" +test 4 = `grep -c warning: stderr` + +$genltl --and-gf=1..3 | +run 0 $ltldo "{tgba}$ltl2tgba %f -H >%H" "{ba}$ltl2tgba >%N %f -s" \ + --stats="%T,%R,%f,%s,%t,%e" >output +cat output +cat >expected <. + +. ./defs +set -e + +ltldo=../../bin/ltldo +genltl=../../bin/genltl + +test -n "$LTL2BA" || exit 77 + +$genltl --or-g=1..2 | + run 0 $ltldo '{ltl2ba}ltl2ba -f %s>%H' >output +test 2 = `grep -c digraph output`