From 337aeefcc32f6cda773aa10a1fc405c7f2cff28d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 25 Jul 2013 18:27:51 +0200 Subject: [PATCH] ltlcross: add support for ltl2dstar's output. * 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. --- NEWS | 11 ++++++ src/bin/ltlcross.cc | 47 +++++++++++++++++++----- src/bin/man/ltlcross.x | 17 +++++++++ src/tgbatest/Makefile.am | 1 + src/tgbatest/ltl2dstar.test | 72 +++++++++++++++++++++++++++++++++++++ 5 files changed, 140 insertions(+), 8 deletions(-) create mode 100755 src/tgbatest/ltl2dstar.test diff --git a/NEWS b/NEWS index cf7f5440e..58ba086e6 100644 --- a/NEWS +++ b/NEWS @@ -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. diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 827f81d87..c0b50d40e 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -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 { 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"); } diff --git a/src/bin/man/ltlcross.x b/src/bin/man/ltlcross.x index 0f4c5603d..3727521b6 100644 --- a/src/bin/man/ltlcross.x +++ b/src/bin/man/ltlcross.x @@ -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. + diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 1f87f14e1..bdab80b05 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -108,6 +108,7 @@ TESTS = \ wdba.test \ wdba2.test \ babiak.test \ + ltl2dstar.test \ randtgba.test \ emptchk.test \ emptchke.test \ diff --git a/src/tgbatest/ltl2dstar.test b/src/tgbatest/ltl2dstar.test new file mode 100755 index 000000000..decdca4cb --- /dev/null +++ b/src/tgbatest/ltl2dstar.test @@ -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 . + +# 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 < 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"