alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltlcross: add support for ltl2dstar's output.

Browse source 
* src/bin/ltlcross.cc: Add support for %D.
* src/bin/man/ltlcross.x: Add example.
* NEWS: Mention it.
* src/tgbatest/ltl2dstar.test: New file.
* src/tgbatest/Makefile.am: Add it.
This commit is contained in:
Alexandre Duret-Lutz 2013-07-25 18:27:51 +02:00
parent 2da0053c53
commit 337aeefcc3
5 changed files with 140 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

11
NEWS
View file

@ -10,6 +10,17 @@ New in spot 1.1.4a (not relased)
two automata when the product between a positive automaton and
a negative automaton is non-empty.
* ltlcross can now read the Rabin and Streett automata output by
ltl2dstar. This type of output should be specified using '%D':
ltlcross 'ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-s %L %D'
However because Spot only supports Büchi acceptance, these Rabin
and Streett automata are immediately converted to TGBA before
further processing by ltlcross. This is still interesting to
search for bugs in translators to Rabin or Streett automata, but
the statistics might not be very relevant.
* Environment variables SPOT_TMPDIR and SPOT_TMPKEEP control where
temporary files are created and if they should be erased. Read
the man page of ltlcross for detail.

47
src/bin/ltlcross.cc
View file

@ -38,6 +38,7 @@
#include "common_cout.hh"
#include "common_finput.hh"
#include "neverparse/public.hh"
#include "dstarparse/public.hh"
#include "ltlast/unop.hh"
#include "ltlvisit/tostring.hh"
#include "ltlvisit/apcollect.hh"
@ -107,8 +108,9 @@ static const argp_option options[] =
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", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"the output automaton as a Never claim, or in LBTT's format", 0 },
{ "%N,%T,%D", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
"the output automaton as a Never claim, in LBTT's or in LTL2DSTAR's "
"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 "
@ -532,7 +534,7 @@ namespace
public spot::printable_value<spot::temporary_file*>
{
unsigned translator_num;
enum output_format { None, Spin, Lbtt };
enum output_format { None, Spin, Lbtt, Dstar };
mutable output_format format;
printable_result_filename()
@ -562,10 +564,15 @@ namespace
{
if (*pos == 'N')
format = Spin;
else
else if (*pos == 'T')
format = Lbtt;
else if (*pos == 'D')
format = Dstar;
else
assert(!"BUG");
if (val_)
error(2, 0, "you may have only one %%N or %%T specifier: %s",
error(2, 0, "you may have only one %%D, %%N, or %%T specifier: %s",
translators[translator_num]);
char prefix[30];
snprintf(prefix, sizeof prefix, "lcr-o%u-", translator_num);
@ -604,6 +611,7 @@ namespace
declare('S', &filename_ltl_spin);
declare('L', &filename_ltl_lbt);
declare('W', &filename_ltl_wring);
declare('D', &output);
declare('N', &output);
declare('T', &output);
@ -621,9 +629,9 @@ namespace
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]);
if (!(has['N'] || has['T']))
error(2, 0, "no output %%-sequence in '%s'.\n Use "
"one of %%N,%%T to indicate where the automaton is saved.",
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]);
// Remember the %-sequences used by all translators.
@ -763,6 +771,29 @@ namespace
}
break;
}
case printable_result_filename::Dstar:
{
spot::dstar_parse_error_list pel;
std::string filename = output.val()->name();
spot::dstar_aut* aut;
aut = spot::dstar_parse(filename, pel, &dict);
if (!pel.empty())
{
std::ostream& err = global_error();
err << "error: failed to parse the produced DSTAR"
" output.\n";
spot::format_dstar_parse_errors(err, filename, pel);
end_error();
delete aut;
res = 0;
}
if (aut->type == spot::Rabin)
res = spot::nra_to_nba(aut);
else
res = spot::nsa_to_tgba(aut);
delete aut;
break;
}
case printable_result_filename::None:
assert(!"unreachable code");
}

17
src/bin/man/ltlcross.x
View file

@ -30,6 +30,22 @@ in LBT's format, and \f(CW%T\fR to read the output in LBTT's format
.fi
.LP
Rabin or Streett automata output by ltl2dstar can be read from a
file specified with \f(CW%D\fR. For instance:
.nf
% ltlcross \-F input.ltl \e
'ltl2dstar \-\-ltl2nba=spin:path/ltl2tgba@\-s %L %D' \e
'ltl2dstar \-\-automata=streett \-\-ltl2nba=spin:path/ltl2tgba@\-s %L %D' \e
.fi
.LP
However because Spot only supports Büchi acceptance, these Rabin and
Streett automata are immediately converted to TGBA before further
processing by ltlcross. This is still interesting to search for bugs
in translators to Rabin or Streett automata, but the statistics might
not be very relevant.
If you use ltlcross in an automated testsuite just to check for
potential problems, avoid the \fB\-\-csv\fR and \fB\-\-json\fR
options: ltlcross is faster when it does not have to compute these
@ -75,3 +91,4 @@ th02
H. Tauriainen and K. Heljanko: Testing LTL formula translation into
Büchi automata. Int. J. on Software Tools for Technology Transfer.
Volume 4, number 1, October 2002.

1
src/tgbatest/Makefile.am
View file

@ -108,6 +108,7 @@ TESTS = \
wdba.test \
wdba2.test \
babiak.test \
ltl2dstar.test \
randtgba.test \
emptchk.test \
emptchke.test \

72
src/tgbatest/ltl2dstar.test Executable file
View file

@ -0,0 +1,72 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 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/>.
# Do some quick translations to make sure the neverclaims produced by
# spot actually look correct! We do that by parsing them via ltlcross.
# ltl2neverclaim-lbtt.test does the same with LBTT if it is installed.
. ./defs
set -e
# Skip this test if ltl2dstar is not installed.
(ltl2dstar --version) || exit 77
ltlfilt=../../bin/ltlfilt
ltl2tgba=../../bin/ltl2tgba
ltlcross=../../bin/ltlcross
randltl=../../bin/randltl
ltlfilt=../../bin/ltlfilt
$ltlfilt -f 'a U b' -l |
ltl2dstar --ltl2nba=spin:$ltl2tgba@-s - - |
../ltl2tgba -XDB - |
tee out
cat >expected <<EOF
digraph G {
0 [label="", style=invis, height=0]
0 -> 1
1 [label="1"]
1 -> 1 [label="a & !b\n"]
1 -> 2 [label="a & !b\n"]
1 -> 3 [label="b\n"]
1 -> 4 [label="b\n"]
2 [label="2"]
2 -> 2 [label="a & !b\n"]
2 -> 4 [label="b\n"]
3 [label="5"]
3 -> 3 [label="1\n"]
3 -> 4 [label="1\n"]
4 [label="6", peripheries=2]
4 -> 4 [label="1\n{Acc[1]}"]
}
EOF
diff expected out
$randltl -n 15 a b | $ltlfilt --nnf --remove-wm |
$ltlcross -F - -f 'GFa & GFb & GFc' -f '(GFa -> GFb) & (GFc -> GFd)' \
--timeout=10 \
"$ltl2tgba -s %f >%N" \
"ltl2dstar --automata=rabin --output=nba --ltl2nba=spin:$ltl2tgba@-s %L %T" \
"ltl2dstar --automata=rabin --ltl2nba=spin:$ltl2tgba@-s %L %D" \
"ltl2dstar --automata=streett --output=nba --ltl2nba=spin:$ltl2tgba@-s %L %T" \
"ltl2dstar --automata=streett --ltl2nba=spin:$ltl2tgba@-s %L %D"