Commit 7de25a32 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

ltlcross: support short names

* NEWS: Mention it.
* doc/org/ltlcross.org: Document it.
* src/bin/ltlcross.cc: Implement it.
* src/tgbatest/Makefile.am, src/tgbatest/defs.in,
src/tgbatest/ltlcross4.test: Test it.
parent 1c5536ea
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.
......
......@@ -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
......
......@@ -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<char*> 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<char*>(name));
}
};
std::vector<translator_spec> 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]);
......
......@@ -114,6 +114,7 @@ TESTS = \
wdba.test \
wdba2.test \
babiak.test \
ltlcross4.test \
ltl2dstar.test \
ltl2dstar2.test \
randtgba.test \
......
# -*- 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()
{
......
#!/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 <http://www.gnu.org/licenses/>.
. ./defs
set -e
test -z "$PYTHON" && exit 77
ltl2tgba=../../bin/ltl2tgba
cat >formulas.txt <<EOF
GFa & GFb
GFa -> 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 <<EOF
import sys
try:
import pandas
except ImportError:
sys.exit(77)
x = pandas.read_csv("output.csv")
print(x.filter(('formula', 'tool',
'states', 'transitions')).groupby('tool').describe())
EOF
# will exit 77 if panda is not installed
$PYTHON test.py >out.1
# remove trailing whitespace from pandas' output
sed 's/[ \t]*$//g' <out.1 > py.out
cat >expected <<EOF
states transitions
tool
ltl2tgba any count 4.000000 4.000000
mean 2.250000 10.000000
std 0.957427 5.163978
min 1.000000 4.000000
25% 1.750000 7.000000
50% 2.500000 10.000000
75% 3.000000 13.000000
max 3.000000 16.000000
ltl2tgba det count 4.000000 4.000000
mean 2.250000 9.250000
std 0.957427 4.573474
min 1.000000 4.000000
25% 1.750000 6.250000
50% 2.500000 9.500000
75% 3.000000 12.500000
max 3.000000 14.000000
ltl2tgba sma count 4.000000 4.000000
mean 2.250000 9.250000
std 0.957427 4.573474
min 1.000000 4.000000
25% 1.750000 6.250000
50% 2.500000 9.500000
75% 3.000000 12.500000
max 3.000000 14.000000
EOF
diff py.out expected
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment