From 437128b55be66203ce9e35ce4a8246ac551cd8ed Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 19 May 2010 18:56:57 +0200 Subject: [PATCH] Add functions to compute the kind of a formula (LTL, PSL, Boolean...) * src/ltlvisit/kind.hh, src/ltlvisit/kind.cc: New files. * src/ltlvisit/Makefile.am: Add them. * src/ltltest/kind.test, src/ltltest/kind.cc: New files. * src/ltltest/Makefile.am: Add them. --- src/ltltest/.gitignore | 2 + src/ltltest/Makefile.am | 3 + src/ltltest/kind.cc | 57 ++++++++++ src/ltltest/kind.test | 72 ++++++++++++ src/ltlvisit/Makefile.am | 2 + src/ltlvisit/kind.cc | 229 +++++++++++++++++++++++++++++++++++++++ src/ltlvisit/kind.hh | 69 ++++++++++++ 7 files changed, 434 insertions(+) create mode 100644 src/ltltest/kind.cc create mode 100755 src/ltltest/kind.test create mode 100644 src/ltlvisit/kind.cc create mode 100644 src/ltlvisit/kind.hh diff --git a/src/ltltest/.gitignore b/src/ltltest/.gitignore index 2b95bf96c..afffa4ef8 100644 --- a/src/ltltest/.gitignore +++ b/src/ltltest/.gitignore @@ -22,3 +22,5 @@ randltl reductau reductaustr genltl +kind +consterm diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am index a3693158a..e297f20ae 100644 --- a/src/ltltest/Makefile.am +++ b/src/ltltest/Makefile.am @@ -30,6 +30,7 @@ check_SCRIPTS = defs check_PROGRAMS = \ consterm \ equals \ + kind \ length \ ltl2dot \ ltl2text \ @@ -51,6 +52,7 @@ noinst_PROGRAMS = \ consterm_SOURCES = consterm.cc equals_SOURCES = equals.cc genltl_SOURCES = genltl.cc +kind_SOURCES = kind.cc length_SOURCES = length.cc ltl2dot_SOURCES = readltl.cc ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY @@ -89,6 +91,7 @@ TESTS = \ nenoform.test \ tunenoform.test \ consterm.test \ + kind.test \ syntimpl.test \ reduc.test \ reduccmp.test diff --git a/src/ltltest/kind.cc b/src/ltltest/kind.cc new file mode 100644 index 000000000..04b8c5ca2 --- /dev/null +++ b/src/ltltest/kind.cc @@ -0,0 +1,57 @@ +// Copyright (C) 2010 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/kind.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; + + unsigned k = spot::ltl::kind_of(f1); + spot::ltl::print_kind(std::cout, k, true) << " = "; + spot::ltl::print_kind(std::cout, k, false) << 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/kind.test b/src/ltltest/kind.test new file mode 100755 index 000000000..4befe04b9 --- /dev/null +++ b/src/ltltest/kind.test @@ -0,0 +1,72 @@ +#! /bin/sh +# Copyright (C) 2010 Laboratoire de Recherche et Developement to +# 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. + + +# Check for the constant_term visitor + +. ./defs || exit 1 + +set -e + +check() +{ + run 0 ../kind "$1" >out + read word rest b' 'BxfLEP' +check '!a' 'B&!xfLEP' +check '!(a|b)' 'B&xfLEP' +check 'a U b' '&!xfLP' +check 'a U Fb' '&!xLP' +check 'Ga U b' '&!xLP' +check 'a W b' '&!xfLP' +check 'a M b' '&!xfLP' +check 'a R b' '&!xfLP' +check '{a}|->!Xb' '&fP' +check '{a}|->X!b' '&!fP' +check '{a}|->!Gb' '&xP' +check '{a}|->F!b' '&!xP' + +run 0 ../consterm '1' +run 0 ../consterm '0' +run 1 ../consterm '[*0]' +run 1 ../consterm 'a*' +run 1 ../consterm '0*' +run 1 ../consterm 'a[*0]' +run 1 ../consterm 'a[*0..]' +run 1 ../consterm 'a[*0..3]' +run 0 ../consterm 'a[*1..3]' +run 0 ../consterm 'a[*3]' +run 1 ../consterm 'a[*..4][*3]' +run 0 ../consterm 'a[*1..4][*3]' +run 1 ../consterm 'a[*1..4][*0..3]' +run 0 ../consterm '((a ; b) + c)' +run 1 ../consterm '((a ; b) + [*0])' +run 0 ../consterm '((a ; b) + [*0]) & e' +run 1 ../consterm '((a ; b) + [*0]) & [*0]' +run 1 ../consterm '((a ; b) + [*0]) & (a* + b)' +run 1 ../consterm '{{a ; b} + {[*0]}} & {a* + b}' # test braces +run 1 ../consterm '(a + [*0]);(b + [*0]);(c + [*0])' +run 0 ../consterm '(a + [*0]);(b + e);(c + [*0])' +run 1 ../consterm '(a + [*0]);(b + e)*;(c + [*0])' diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index 186d1d286..813894805 100644 --- a/src/ltlvisit/Makefile.am +++ b/src/ltlvisit/Makefile.am @@ -35,6 +35,7 @@ ltlvisit_HEADERS = \ destroy.hh \ dotty.hh \ dump.hh \ + kind.hh \ length.hh \ lunabbrev.hh \ mark.hh \ @@ -57,6 +58,7 @@ libltlvisit_la_SOURCES = \ destroy.cc \ dotty.cc \ dump.cc \ + kind.cc \ length.cc \ lunabbrev.cc \ mark.cc \ diff --git a/src/ltlvisit/kind.cc b/src/ltlvisit/kind.cc new file mode 100644 index 000000000..cd2fe378c --- /dev/null +++ b/src/ltlvisit/kind.cc @@ -0,0 +1,229 @@ +// Copyright (C) 2010 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 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 "kind.hh" +#include "ltlast/allnodes.hh" +#include "ltlast/visitor.hh" +#include + +namespace spot +{ + namespace ltl + { + namespace + { + + class kind_visitor : public visitor + { + unsigned result_; + public: + kind_visitor() + : result_(All_Kind) + { + } + ~kind_visitor() + { + } + + unsigned + result() + { + return result_; + } + + void + visit(atomic_prop*) + { + } + + void + visit(constant* c) + { + if (c == constant::empty_word_instance()) + result_ &= ~(Boolean_Kind | LTL_Kind | ELTL_Kind); + } + + void + visit(bunop* bo) + { + result_ = recurse(bo->child()); + result_ &= ~(Boolean_Kind | LTL_Kind | ELTL_Kind); + } + + void + visit(unop* uo) + { + result_ = recurse(uo->child()); + + switch (uo->op()) + { + case unop::NegClosure: + case unop::Closure: + result_ &= ~(Boolean_Kind | LTL_Kind | ELTL_Kind); + return; + case unop::Finish: + result_ &= ~(Boolean_Kind | LTL_Kind | PSL_Kind); + return; + case unop::Not: + if (!dynamic_cast(uo->child())) + result_ &= ~NeNoForm_Kind; + return; + case unop::X: + result_ &= ~(Boolean_Kind | No_X_Kind | ELTL_Kind); + return; + case unop::F: + case unop::G: + result_ &= ~(Boolean_Kind | SugarFree_LTL_Kind | ELTL_Kind); + return; + } + /* Unreachable code. */ + assert(0); + } + + void + visit(automatop* ao) + { + unsigned aos = ao->size(); + for (unsigned i = 0; i < aos && !result_; ++i) + result_ &= recurse(ao->nth(i)); + + result_ &= ~(Boolean_Kind | LTL_Kind | PSL_Kind); + } + + void + visit(multop* mo) + { + unsigned mos = mo->size(); + for (unsigned i = 0; i < mos && !result_; ++i) + result_ &= recurse(mo->nth(i)); + + switch (mo->op()) + { + case multop::Or: + case multop::And: + return; + case multop::AndNLM: + // The non-matching-length-And (&) can only appear + // in the rational parts of PSL formula. We + // don't remove the Boolean_Kind flags, because + // applied to atomic propositions a&b has the same + // effect as a&&b. + result_ &= ~(LTL_Kind | ELTL_Kind); + return; + case multop::Concat: + case multop::Fusion: + result_ &= ~(Boolean_Kind | LTL_Kind | ELTL_Kind); + return; + } + } + + void + visit(binop* bo) + { + result_ = recurse(bo->first()) & recurse(bo->second()); + + switch (bo->op()) + { + case binop::EConcatMarked: + case binop::UConcat: + case binop::EConcat: + result_ &= ~(Boolean_Kind | LTL_Kind | ELTL_Kind); + return; + case binop::Xor: + case binop::Implies: + case binop::Equiv: + result_ &= ~(NeNoForm_Kind | SugarFree_Boolean_Kind); + return; + case binop::U: + case binop::W: + case binop::M: + case binop::R: + result_ &= ~(Boolean_Kind | ELTL_Kind); + return; + } + /* Unreachable code. */ + assert(0); + } + + unsigned + recurse(const formula* f) + { + return kind_of(f); + } + }; + } + + unsigned + kind_of(const formula* f) + { + kind_visitor v; + const_cast(f)->accept(v); + return v.result(); + } + + + + std::ostream& + print_kind(std::ostream& o, unsigned k, bool abbreviated) + { + struct data { char abbrev; const char* name; }; + static const data kind_name[] = + { + {'B', "Boolean formula"}, // 1 + {'&', "no sugar Boolean operator"}, // 2 + {'!', "in negative normal form"}, // 4 + {'x', "no X LTL operator"}, // 8 + {'f', "no sugar LTL operator"}, // 16 + {'L', "LTL formula"}, // 32 + {'E', "ELTL formula"}, // 64 + {'P', "PSL formula"}, // 128 + }; + const char* comma = ""; + unsigned size = (sizeof kind_name)/(sizeof *kind_name); + for (unsigned i = 0; i < size; ++i) + { + if ((k & 1)) + { + if (abbreviated) + { + o << kind_name[i].abbrev; + } + else + { + o << comma << kind_name[i].name; + comma = ", "; + } + } + k >>= 1; + } + return o; + } + + + std::ostream& + print_kind(std::ostream& o, const formula* f, bool abbreviated) + { + print_kind(o, kind_of(f), abbreviated); + return o; + } + + + } +} diff --git a/src/ltlvisit/kind.hh b/src/ltlvisit/kind.hh new file mode 100644 index 000000000..d984ffa70 --- /dev/null +++ b/src/ltlvisit/kind.hh @@ -0,0 +1,69 @@ +// Copyright (C) 2010 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 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. + +#ifndef SPOT_LTLVISIT_KIND_HH +# define SPOT_LTLVISIT_KIND_HH + +#include "ltlast/predecl.hh" +#include + +namespace spot +{ + namespace ltl + { + /// Different kinds or proporties of formulae. + // If you change this list, you have to adjust + // the kind_name array in print_kind() (kind.cc) + enum kind + { + Boolean_Kind = 1, + SugarFree_Boolean_Kind = 2, + NeNoForm_Kind = 4, + No_X_Kind = 8, + SugarFree_LTL_Kind = 16, + LTL_Kind = 32, + ELTL_Kind = 64, + PSL_Kind = 128, + All_Kind = -1U, + }; + + + /// \brief Compute properties of a formula. + /// \ingroup ltl_visitor + /// + /// Return a sum of ltl::kind values depending on the operators + /// used by a formula. + /// + /// \param f The formula to analyze. + unsigned kind_of(const formula* f); + + /// \brief Print a ltl::kind (computed by kind_of()). + /// \ingroup ltl_visitor + std::ostream& print_kind(std::ostream& o, unsigned k, + bool abbreviated = false); + + /// \brief Print the properties of a formula. + /// \ingroup ltl_visitor + std::ostream& print_kind(std::ostream& o, const formula* f, + bool abbreviated = false); + } +} + +#endif // SPOT_LTLVISIT_KIND_HH