From 984c715cc67c14a87ee2fe2840d70fa3cbffc14e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 5 Jan 2012 18:34:23 +0100 Subject: [PATCH] Fix computation of length of LTL formulas. * src/ltlvisit/length.cc: Fix computation for ltl::multop operator. "a&b&c" was reported with length 3, ignoring the "&" operators, because of a typo. * src/ltlvisit/length.hh: Fix description to correctly reflect this change intended since 2010-01-22. * src/ltltest/length.test, src/ltltest/length.cc: New files. * src/ltltest/Makefile.am: Add them. --- ChangeLog | 12 +++++++++ NEWS | 4 ++- src/ltltest/Makefile.am | 7 ++++-- src/ltltest/length.cc | 55 +++++++++++++++++++++++++++++++++++++++++ src/ltltest/length.test | 29 ++++++++++++++++++++++ src/ltlvisit/length.cc | 2 +- src/ltlvisit/length.hh | 10 +++++--- 7 files changed, 111 insertions(+), 8 deletions(-) create mode 100644 src/ltltest/length.cc create mode 100755 src/ltltest/length.test diff --git a/ChangeLog b/ChangeLog index a31f5c24c..baeeead25 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,15 @@ +2012-01-05 Alexandre Duret-Lutz + + Fix computation of length of LTL formulas. + + * src/ltlvisit/length.cc: Fix computation for ltl::multop + operator. "a&b&c" was reported with length 3, ignoring the + "&" operators, because of a typo. + * src/ltlvisit/length.hh: Fix description to correctly + reflect this change intended since 2010-01-22. + * src/ltltest/length.test, src/ltltest/length.cc: New files. + * src/ltltest/Makefile.am: Add them. + 2011-12-18 Alexandre Duret-Lutz * configure.ac, NEWS: Bump version to 0.8.1a. diff --git a/NEWS b/NEWS index 61139cc78..a0d52ce4d 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,8 @@ New in spot 0.8.1a: - * Nothing yet. + * Bug fixes: + - spot::ltl::length() forgot to count the '&' and '|' operators + in an LTL formula. New in spot 0.8.1: diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am index 7f2a2f42b..4c23e44bd 100644 --- a/src/ltltest/Makefile.am +++ b/src/ltltest/Makefile.am @@ -1,5 +1,5 @@ -## Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement -## de l'Epita (LRDE). +## Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et +## Développement de l'Epita (LRDE). ## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de ## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), ## Université Pierre et Marie Curie. @@ -29,6 +29,7 @@ check_SCRIPTS = defs # Keep this sorted alphabetically. check_PROGRAMS = \ equals \ + length \ ltl2dot \ ltl2text \ lunabbrev \ @@ -48,6 +49,7 @@ noinst_PROGRAMS = \ equals_SOURCES = equals.cc genltl_SOURCES = genltl.cc +length_SOURCES = length.cc ltl2dot_SOURCES = readltl.cc ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY ltl2text_SOURCES = readltl.cc @@ -77,6 +79,7 @@ EXTRA_DIST = $(TESTS) TESTS = \ parse.test \ parseerr.test \ + length.test \ equals.test \ tostring.test \ lunabbrev.test \ diff --git a/src/ltltest/length.cc b/src/ltltest/length.cc new file mode 100644 index 000000000..3fbfe70f2 --- /dev/null +++ b/src/ltltest/length.cc @@ -0,0 +1,55 @@ +// Copyright (C) 2012 Laboratoire de Recherche et Developement 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 2 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 Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include +#include +#include "ltlparse/public.hh" +#include "ltlvisit/length.hh" +#include "ltlast/allnodes.hh" + +void +syntax(char *prog) +{ + std::cerr << prog << " formula" << std::endl; + exit(2); +} + +int +main(int argc, char **argv) +{ + if (argc != 2) + syntax(argv[0]); + + spot::ltl::parse_error_list p1; + spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1); + + if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1)) + return 2; + + std::cout << spot::ltl::length(f1) << std::endl; + + f1->destroy(); + assert(spot::ltl::atomic_prop::instance_count() == 0); + assert(spot::ltl::unop::instance_count() == 0); + assert(spot::ltl::binop::instance_count() == 0); + assert(spot::ltl::multop::instance_count() == 0); + return 0; +} diff --git a/src/ltltest/length.test b/src/ltltest/length.test new file mode 100755 index 000000000..6faf1b2bc --- /dev/null +++ b/src/ltltest/length.test @@ -0,0 +1,29 @@ +#! /bin/sh +# Copyright (C) 2012 Laboratoire de Recherche et Developpement +# 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 2 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 Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + + +. ./defs || exit 1 + +set -e + +test `run 0 ../length 'a U Xc'` = 4 +test `run 0 ../length 'a&b&c'` = 5 +test `run 0 ../length 'a|b|c'` = 5 diff --git a/src/ltlvisit/length.cc b/src/ltlvisit/length.cc index ba214b37e..7ca96955e 100644 --- a/src/ltlvisit/length.cc +++ b/src/ltlvisit/length.cc @@ -53,7 +53,7 @@ namespace spot mo->nth(i)->accept(*this); // "a & b & c" should count for 5, even though it is // stored as And(a,b,c). - mo += s - 1; + result_ += s - 1; } virtual void diff --git a/src/ltlvisit/length.hh b/src/ltlvisit/length.hh index ddf5ec36c..dabd34ef0 100644 --- a/src/ltlvisit/length.hh +++ b/src/ltlvisit/length.hh @@ -1,3 +1,5 @@ +// Copyright (C) 2012 Laboratoire de Recherche et Developement de +// l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -33,10 +35,10 @@ namespace spot /// /// The length of a formula is the number of atomic properties, /// constants, and operators (logical and temporal) occurring in - /// the formula. spot::ltl::multops count only for 1, even if - /// they have more than two operands (e.g. a | b | c - /// has length 4, because | is represented once - /// internally). + /// the formula. spot::ltl::multop instances with n arguments + /// count only n-1; for instance a | b | c + /// has length 5, even if there is only as single | node + /// internally. int length(const formula* f); } }