Commit 984c715c authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 93f1009b
2012-01-05 Alexandre Duret-Lutz <adl@lrde.epita.fr>
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 <adl@lrde.epita.fr>
* configure.ac, NEWS: Bump version to 0.8.1a.
......
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:
......
## Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Dveloppement
## de l'Epita (LRDE).
## Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
## Dveloppement de l'Epita (LRDE).
## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
## Paris 6 (LIP6), dpartement Systmes Rpartis Coopratifs (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 \
......
// 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 <iostream>
#include <cassert>
#include <cstdlib>
#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;
}
#! /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
......@@ -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
......
// 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. <code>a | b | c</code>
/// has length 4, because <code>|</code> is represented once
/// internally).
/// the formula. spot::ltl::multop instances with n arguments
/// count only n-1; for instance <code>a | b | c</code>
/// has length 5, even if there is only as single <code>|</code> node
/// internally.
int length(const formula* f);
}
}
......
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