diff --git a/NEWS b/NEWS index 519322801..2b82628c0 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,13 @@ New in spot 1.2a (not released) + * New features: + - commands for translators specified to ltlcross can now + be given "short names" to be used in the CSV or JSON output. + For instance + ltlcross '{small} ltl2tgba -s --small %f >%N' ... + will run the command "ltl2tgba -s --small %f >%N", but only + print "small" in output files. + * Bug fixes: - ltlcross' CSV output now stricly follows RFC 4180. diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 9a524f13f..0ce07774f 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -425,6 +425,50 @@ is used, =N= products are builds instead of one, and the fields =product_states=, =product_transitions=, and =product_scc= contain average values. +** Changing the name of the translators + +By default, the names used in the CSV and JSON output to designate the +translators are the command specified on the command line. + +For instance in the following, =ltl2tgba= is run in two +configurations, and the strings =ltl2tgba -s --small %f >%N= and +=ltl2tgba -s --deter %f >%N= appear verbatim in the output: + +#+BEGIN_SRC sh :results verbatim :exports both +ltlcross -f a -f Ga 'ltl2tgba -s --small %f >%N' 'ltl2tgba -s --deter %f >%N' --csv +#+END_SRC +#+RESULTS: +: "formula","tool","states","edges","transitions","acc","scc","nonacc_scc","terminal_scc","weak_scc","strong_scc","nondet_states","nondet_aut","terminal_aut","weak_aut","strong_aut","time","product_states","product_transitions","product_scc" +: "(a)","ltl2tgba -s --small %f >%N",2,2,3,1,2,1,1,0,0,0,0,1,0,0,0.0309309,201,4092,2 +: "(a)","ltl2tgba -s --deter %f >%N",2,2,3,1,2,1,1,0,0,0,0,1,0,0,0.0280637,201,4092,2 +: "(!(a))","ltl2tgba -s --small %f >%N",2,2,3,1,2,1,1,0,0,0,0,1,0,0,0.026676,201,4098,2 +: "(!(a))","ltl2tgba -s --deter %f >%N",2,2,3,1,2,1,1,0,0,0,0,1,0,0,0.0250905,201,4098,2 +: "(G(a))","ltl2tgba -s --small %f >%N",1,1,1,1,1,0,0,1,0,0,0,0,1,0,0.0244696,200,2023,1 +: "(G(a))","ltl2tgba -s --deter %f >%N",1,1,1,1,1,0,0,1,0,0,0,0,1,0,0.0240073,200,2023,1 +: "(!(G(a)))","ltl2tgba -s --small %f >%N",2,3,4,1,2,1,1,0,0,0,0,1,0,0,0.0229872,400,8166,2 +: "(!(G(a)))","ltl2tgba -s --deter %f >%N",2,3,4,1,2,1,1,0,0,0,0,1,0,0,0.0229391,400,8166,2 + +To present these results graphically, or even when analyzing these +data, it might be convenient to give each configured tool a shorter +name. =ltlcross= supports the specification of such short names by +looking whether the command specification for a translator has the +form "={short name}actual command=". + +For instance: +#+BEGIN_SRC sh :results verbatim :exports both +ltlcross -f a -f Ga '{small} ltl2tgba -s --small %f >%N' '{deter} ltl2tgba -s --deter %f >%N' --csv +#+END_SRC +#+RESULTS: +: "formula","tool","states","edges","transitions","acc","scc","nonacc_scc","terminal_scc","weak_scc","strong_scc","nondet_states","nondet_aut","terminal_aut","weak_aut","strong_aut","time","product_states","product_transitions","product_scc" +: "(a)","small",2,2,3,1,2,1,1,0,0,0,0,1,0,0,0.0272853,201,4092,2 +: "(a)","deter",2,2,3,1,2,1,1,0,0,0,0,1,0,0,0.02555,201,4092,2 +: "(!(a))","small",2,2,3,1,2,1,1,0,0,0,0,1,0,0,0.0242986,201,4098,2 +: "(!(a))","deter",2,2,3,1,2,1,1,0,0,0,0,1,0,0,0.0239094,201,4098,2 +: "(G(a))","small",1,1,1,1,1,0,0,1,0,0,0,0,1,0,0.0232251,200,2023,1 +: "(G(a))","deter",1,1,1,1,1,0,0,1,0,0,0,0,1,0,0.0230073,200,2023,1 +: "(!(G(a)))","small",2,3,4,1,2,1,1,0,0,0,0,1,0,0,0.0226587,400,8166,2 +: "(!(G(a)))","deter",2,3,4,1,2,1,1,0,0,0,0,1,0,0,0.0229191,400,8166,2 + * Detecting problems If a translator exits with a non-zero status code, or fails to output diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 69c263b48..a336c2fc2 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -116,7 +116,10 @@ static const argp_option options[] = { 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.", 0 }, + "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 }, { "allow-dups", OPT_DUPS, 0, 0, @@ -199,7 +202,61 @@ bool stop_on_error = false; int seed = 0; unsigned products = 1; -std::vector translators; + +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; static std::ostream& @@ -587,7 +644,7 @@ namespace // to mix the formats. if (format != old_format) error(2, 0, "you may not mix %%D, %%N, and %%T specifiers: %s", - translators[translator_num]); + translators[translator_num].spec); } else { @@ -641,19 +698,20 @@ namespace // Check that each translator uses at least one input and // one output. has.clear(); - scan(translators[n], has); + 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.", translators[n]); + "to pass the formula.", t.spec); if (!(has['D'] || has['N'] || has['T'])) error(2, 0, "no output %%-sequence in '%s'.\n Use one of " "%%D,%%N,%%T to indicate where the automaton is saved.", - translators[n]); + t.spec); // Remember the %-sequences used by all translators. - prime(translators[n]); + prime(t.cmd); } } @@ -716,7 +774,7 @@ namespace output.reset(translator_num); std::ostringstream command; - format(command, translators[translator_num]); + format(command, translators[translator_num].cmd); assert(output.format != printable_result_filename::None); @@ -1353,7 +1411,7 @@ print_stats_csv(const char* filename) *out << "\""; spot::escape_rfc4180(*out, formulas[r]); *out << "\",\""; - spot::escape_rfc4180(*out, translators[t]); + spot::escape_rfc4180(*out, translators[t].name); *out << "\","; vstats[r][t].to_csv(*out); *out << "\r\n"; @@ -1382,11 +1440,11 @@ print_stats_json(const char* filename) assert(rounds == formulas.size()); *out << "{\n \"tool\": [\n \""; - spot::escape_str(*out, translators[0]); + spot::escape_str(*out, translators[0].name); for (unsigned t = 1; t < ntrans; ++t) { *out << "\",\n \""; - spot::escape_str(*out, translators[t]); + spot::escape_str(*out, translators[t].name); } *out << "\"\n ],\n \"formula\": [\n \""; spot::escape_str(*out, formulas[0]); diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index e8154f01f..1eeb1e9c3 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -114,6 +114,7 @@ TESTS = \ wdba.test \ wdba2.test \ babiak.test \ + ltlcross4.test \ ltl2dstar.test \ ltl2dstar2.test \ randtgba.test \ diff --git a/src/tgbatest/defs.in b/src/tgbatest/defs.in index ee04eb935..da73cf85f 100644 --- a/src/tgbatest/defs.in +++ b/src/tgbatest/defs.in @@ -1,6 +1,6 @@ # -*- mode: shell-script; coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). +# Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. @@ -64,6 +64,7 @@ LBTT_TRANSLATE="@LBTT_TRANSLATE@" VALGRIND='@VALGRIND@' SPIN='@SPIN@' LTL2BA='@LTL2BA@' +PYTHON='@PYTHON@' need_lbtt() { diff --git a/src/tgbatest/ltlcross4.test b/src/tgbatest/ltlcross4.test new file mode 100755 index 000000000..8c092a945 --- /dev/null +++ b/src/tgbatest/ltlcross4.test @@ -0,0 +1,86 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2012, 2013 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 + +test -z "$PYTHON" && exit 77 + +ltl2tgba=../../bin/ltl2tgba + +cat >formulas.txt < GFb +EOF + +../../bin/ltlcross -F formulas.txt \ + "{ltl2tgba any} $ltl2tgba --lbtt --any %f > %T" \ + "{ltl2tgba det} $ltl2tgba --lbtt --deterministic %f > %T" \ + "{ltl2tgba sma} $ltl2tgba --lbtt --small %f > %T" \ + --csv=output.csv + +cat >test.py <out.1 + +# remove trailing whitespace from pandas' output +sed 's/[ \t]*$//g' py.out + +cat >expected <