From 6e3fd873ba403291c523f0917ce5fed8ac8a2a1f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 1 Jun 2004 20:43:00 +0000 Subject: [PATCH] * src/ltltest/inf.cc, src/ltltest/inf.test: Rename as ... * src/ltltest/syntimpl.cc, src/ltltest/syntimpl.test: ... these. * src/ltltest/Makefile.am: Adjust. * src/ltlvisit/forminf.cc: Rename as... * src/ltlvisit/syntimpl.cc: ... this. * src/ltlvisit/syntimpl.hh: New file with definitions extracted from ... * src/ltlvisit/reducform.hh: ... this one. * src/ltlvisit/Makefile.am, src/ltlvisit/reducform.cc: Adjust. --- ChangeLog | 14 +++- src/ltltest/Makefile.am | 6 +- src/ltltest/inf.test | 98 ------------------------ src/ltltest/{inf.cc => syntimpl.cc} | 3 +- src/ltltest/syntimpl.test | 83 ++++++++++++++++++++ src/ltlvisit/Makefile.am | 3 +- src/ltlvisit/reducform.cc | 1 + src/ltlvisit/reducform.hh | 10 --- src/ltlvisit/{forminf.cc => syntimpl.cc} | 2 +- src/ltlvisit/syntimpl.hh | 45 +++++++++++ 10 files changed, 149 insertions(+), 116 deletions(-) delete mode 100755 src/ltltest/inf.test rename src/ltltest/{inf.cc => syntimpl.cc} (97%) create mode 100755 src/ltltest/syntimpl.test rename src/ltlvisit/{forminf.cc => syntimpl.cc} (99%) create mode 100644 src/ltlvisit/syntimpl.hh diff --git a/ChangeLog b/ChangeLog index 742f775ce..55ba1ce99 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,4 +1,16 @@ -2004-05-30 Alexandre Duret-Lutz +2004-06-01 Alexandre Duret-Lutz + + * src/ltltest/inf.cc, src/ltltest/inf.test: Rename as ... + * src/ltltest/syntimpl.cc, src/ltltest/syntimpl.test: ... these. + * src/ltltest/Makefile.am: Adjust. + * src/ltlvisit/forminf.cc: Rename as... + * src/ltlvisit/syntimpl.cc: ... this. + * src/ltlvisit/syntimpl.hh: New file with definitions extracted + from ... + * src/ltlvisit/reducform.hh: ... this one. + * src/ltlvisit/Makefile.am, src/ltlvisit/reducform.cc: Adjust. + +2004-05-30 Alexandre Duret-Lutz * src/ltlvisit/forminf.cc (form_eventual_universal_visitor, inf_form_right_recurse_visitor, inf_form_left_recurse_visitor): Rename diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am index 908eb0eb1..d40644441 100644 --- a/src/ltltest/Makefile.am +++ b/src/ltltest/Makefile.am @@ -30,18 +30,17 @@ check_SCRIPTS = defs # Keep this sorted alphabetically. check_PROGRAMS = \ equals \ - inf \ ltl2dot \ ltl2text \ lunabbrev \ nenoform \ reduc \ + syntimpl \ tostring \ tunabbrev \ tunenoform equals_SOURCES = equals.cc -inf_SOURCES = inf.cc ltl2dot_SOURCES = readltl.cc ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY ltl2text_SOURCES = readltl.cc @@ -50,6 +49,7 @@ lunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DLUNABBREV nenoform_SOURCES = equals.cc nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM reduc_SOURCES = reduc.cc +syntimpl_SOURCES = syntimpl.cc tostring_SOURCES = tostring.cc tunabbrev_SOURCES = equals.cc tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DTUNABBREV @@ -69,7 +69,7 @@ TESTS = \ tunabbrev.test \ nenoform.test \ tunenoform.test \ - inf.test \ + syntimpl.test \ reduc.test CLEANFILES = stdout expect parse.dot result.data diff --git a/src/ltltest/inf.test b/src/ltltest/inf.test deleted file mode 100755 index 824166835..000000000 --- a/src/ltltest/inf.test +++ /dev/null @@ -1,98 +0,0 @@ -#! /bin/sh -# Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -# département Systèmes Répartis Coopératifs (SRC), Université Pierre -# et Marie Curie. -# -# 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 reduc visitor - -. ./defs || exit 1 - -# -run 1 ./inf 0 'Xa' 'X(b U a)' -run 1 ./inf 0 'XXa' 'XX(b U a)' - -run 1 ./inf 0 '(e R f)' '(g U f)' -run 1 ./inf 0 '( X(a + b))' '( X((a + b)+(c)+(d)))' -run 1 ./inf 0 '( X(a + b)) U (e R f)' '( X((a + b)+(c)+(d))) U (g U f)' - -run 0 ./inf 0 'Xa' 'XX(b U a)' -run 0 ./inf 0 'XXa' 'X(b U a)' - -run 0 ./inf 0 '( X(a + b))' '( X(X(a + b)+(c)+(d)))' -run 0 ./inf 0 '( X(a + b)) U (e R f)' '( X(X(a + b)+(c)+(d))) U (g U f)' - -run 0 ./inf 0 'a' 'b' -run 0 ./inf 0 'a' 'b + c' -run 0 ./inf 0 'a + b' 'a' -run 0 ./inf 0 'a' 'a * c' -run 0 ./inf 0 'a * b' 'c' -run 0 ./inf 0 'a' 'a U b' -run 0 ./inf 0 'a' 'a R b' -run 0 ./inf 0 'a R b' 'a' - -run 1 ./inf 0 '1' '1' -run 1 ./inf 0 '0' '0' - -run 1 ./inf 0 'a' '1' -run 1 ./inf 0 'a' 'a' - -run 1 ./inf 0 'a' 'a * 1' - -run 1 ./inf 0 'a * b' 'b' -run 1 ./inf 0 'a * b' 'a' - -run 1 ./inf 0 'a' 'a + b' -run 1 ./inf 0 'b' 'a + b' - -run 1 ./inf 0 'a + b' '1' - -run 1 ./inf 0 'a' 'b U a' -run 1 ./inf 0 'a' 'b U 1' -run 1 ./inf 0 'a U b' '1' - -run 1 ./inf 0 'a' '1 R a' -run 1 ./inf 0 'a' 'a R 1' -run 1 ./inf 0 'a R b' 'b' -run 1 ./inf 0 'a R b' '1' - -run 1 ./inf 0 'Xa' 'X(b U a)' -run 1 ./inf 0 'X(a R b)' 'Xb' - -run 1 ./inf 0 'a U b' '1 U b' -run 1 ./inf 0 'a R b' '1 R b' - -run 1 ./inf 0 'b * (a U b)' 'a U b' -run 1 ./inf 0 'a U b' 'c + (a U b)' - -exit 0 -# - -#run 1 ./inf 0 '(a U b) U ((a U b) U (a U b))' 'a U b' -#run 1 ./inf 0 '(a U b) && (a U b)' 'a U b' - -'X1' '1' -'a U 0' '0' -'a R 1' '1' -'Xa * Xb' 'X(a * b)' -'F(a * GFb)' 'Fa * GFb' -'G(a + GFb)' 'Ga + GFb' -'X(a * GFb)' 'Xa * GFb' -'X(a + GFb)' 'Xa + GFb' diff --git a/src/ltltest/inf.cc b/src/ltltest/syntimpl.cc similarity index 97% rename from src/ltltest/inf.cc rename to src/ltltest/syntimpl.cc index c2e68ae99..ff5ba4ab8 100644 --- a/src/ltltest/inf.cc +++ b/src/ltltest/syntimpl.cc @@ -25,10 +25,9 @@ #include "ltlvisit/lunabbrev.hh" #include "ltlvisit/tunabbrev.hh" #include "ltlvisit/dump.hh" -#include "ltlvisit/nenoform.hh" #include "ltlvisit/destroy.hh" #include "ltlvisit/tostring.hh" -#include "ltlvisit/reducform.hh" +#include "ltlvisit/syntimpl.hh" #include "ltlast/allnodes.hh" void diff --git a/src/ltltest/syntimpl.test b/src/ltltest/syntimpl.test new file mode 100755 index 000000000..79ccd3dc5 --- /dev/null +++ b/src/ltltest/syntimpl.test @@ -0,0 +1,83 @@ +#! /bin/sh +# Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# et Marie Curie. +# +# 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 syntactic implication. + +. ./defs || exit 1 + +# +run 1 ./syntimpl 0 'Xa' 'X(b U a)' +run 1 ./syntimpl 0 'XXa' 'XX(b U a)' + +run 1 ./syntimpl 0 '(e R f)' '(g U f)' +run 1 ./syntimpl 0 '( X(a + b))' '( X((a + b)+(c)+(d)))' +run 1 ./syntimpl 0 '( X(a + b)) U (e R f)' '( X((a + b)+(c)+(d))) U (g U f)' + +run 0 ./syntimpl 0 'Xa' 'XX(b U a)' +run 0 ./syntimpl 0 'XXa' 'X(b U a)' + +run 0 ./syntimpl 0 '( X(a + b))' '( X(X(a + b)+(c)+(d)))' +run 0 ./syntimpl 0 '( X(a + b)) U (e R f)' '( X(X(a + b)+(c)+(d))) U (g U f)' + +run 0 ./syntimpl 0 'a' 'b' +run 0 ./syntimpl 0 'a' 'b + c' +run 0 ./syntimpl 0 'a + b' 'a' +run 0 ./syntimpl 0 'a' 'a * c' +run 0 ./syntimpl 0 'a * b' 'c' +run 0 ./syntimpl 0 'a' 'a U b' +run 0 ./syntimpl 0 'a' 'a R b' +run 0 ./syntimpl 0 'a R b' 'a' + +run 1 ./syntimpl 0 '1' '1' +run 1 ./syntimpl 0 '0' '0' + +run 1 ./syntimpl 0 'a' '1' +run 1 ./syntimpl 0 'a' 'a' + +run 1 ./syntimpl 0 'a' 'a * 1' + +run 1 ./syntimpl 0 'a * b' 'b' +run 1 ./syntimpl 0 'a * b' 'a' + +run 1 ./syntimpl 0 'a' 'a + b' +run 1 ./syntimpl 0 'b' 'a + b' + +run 1 ./syntimpl 0 'a + b' '1' + +run 1 ./syntimpl 0 'a' 'b U a' +run 1 ./syntimpl 0 'a' 'b U 1' +run 1 ./syntimpl 0 'a U b' '1' + +run 1 ./syntimpl 0 'a' '1 R a' +run 1 ./syntimpl 0 'a' 'a R 1' +run 1 ./syntimpl 0 'a R b' 'b' +run 1 ./syntimpl 0 'a R b' '1' + +run 1 ./syntimpl 0 'Xa' 'X(b U a)' +run 1 ./syntimpl 0 'X(a R b)' 'Xb' + +run 1 ./syntimpl 0 'a U b' '1 U b' +run 1 ./syntimpl 0 'a R b' '1 R b' + +run 1 ./syntimpl 0 'b * (a U b)' 'a U b' +run 1 ./syntimpl 0 'a U b' 'c + (a U b)' diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am index 0a0522c58..c337bbdc0 100644 --- a/src/ltlvisit/Makefile.am +++ b/src/ltlvisit/Makefile.am @@ -34,6 +34,7 @@ ltlvisit_HEADERS = \ nenoform.hh \ postfix.hh \ reducform.hh \ + syntimpl.hh \ tostring.hh \ tunabbrev.hh @@ -44,11 +45,11 @@ libltlvisit_la_SOURCES = \ destroy.cc \ dotty.cc \ dump.cc \ - forminf.cc \ length.cc \ lunabbrev.cc \ nenoform.cc \ postfix.cc \ reducform.cc \ + syntimpl.cc \ tostring.cc \ tunabbrev.cc diff --git a/src/ltlvisit/reducform.cc b/src/ltlvisit/reducform.cc index d48efb655..300eaf685 100644 --- a/src/ltlvisit/reducform.cc +++ b/src/ltlvisit/reducform.cc @@ -20,6 +20,7 @@ // 02111-1307, USA. #include "reducform.hh" +#include "syntimpl.hh" #include "ltlast/allnodes.hh" #include diff --git a/src/ltlvisit/reducform.hh b/src/ltlvisit/reducform.hh index 35715daf6..9995e809b 100644 --- a/src/ltlvisit/reducform.hh +++ b/src/ltlvisit/reducform.hh @@ -56,16 +56,6 @@ namespace spot /// Basic rewritings. formula* basic_reduce(const formula* f); - /// \brief Syntactic implication. - bool syntactic_implication(const formula* f1, const formula* f2); - - /// \brief Syntactic implication. - /// - /// If right==false, true if !f1 < f2, false otherwise. - /// If right==true, true if f1 < !f2, false otherwise. - bool syntactic_implication_neg(const formula* f1, const formula* f2, - bool right); - /// \brief Check whether a formula is eventual. /// /// FIXME: Describe what eventual formulae are. Cite paper. diff --git a/src/ltlvisit/forminf.cc b/src/ltlvisit/syntimpl.cc similarity index 99% rename from src/ltlvisit/forminf.cc rename to src/ltlvisit/syntimpl.cc index 0a1b20025..06c4c5312 100644 --- a/src/ltlvisit/forminf.cc +++ b/src/ltlvisit/syntimpl.cc @@ -19,7 +19,7 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#include "reducform.hh" +#include "syntimpl.hh" #include "ltlast/allnodes.hh" #include diff --git a/src/ltlvisit/syntimpl.hh b/src/ltlvisit/syntimpl.hh new file mode 100644 index 000000000..f5993a547 --- /dev/null +++ b/src/ltlvisit/syntimpl.hh @@ -0,0 +1,45 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// 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_SYNTIMPL_HH +# define SPOT_LTLVISIT_SYNTIMPL_HH + +#include "ltlast/formula.hh" + +namespace spot +{ + namespace ltl + { + // FIXME: Cite paper. + + /// \brief Syntactic implication. + bool syntactic_implication(const formula* f1, const formula* f2); + + /// \brief Syntactic implication. + /// + /// If right==false, true if !f1 < f2, false otherwise. + /// If right==true, true if f1 < !f2, false otherwise. + bool syntactic_implication_neg(const formula* f1, const formula* f2, + bool right); + } +} + +#endif // SPOT_LTLVISIT_SYNTIMPL_HH