* 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.
This commit is contained in:
Alexandre Duret-Lutz
parent
121a55c48f
commit
6e3fd873ba
10 changed files with 149 additions and 116 deletions
14
ChangeLog
14
ChangeLog
|
|
@ -1,4 +1,16 @@
|
||||||
2004-05-30 Alexandre Duret-Lutz <adl@gnu.org>
|
2004-06-01 Alexandre Duret-Lutz <adl@gnu.org>
|
||||||
|
|
||||||
|
* 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 <adl@src.lip6.fr>
|
||||||
|
|
||||||
* src/ltlvisit/forminf.cc (form_eventual_universal_visitor,
|
* src/ltlvisit/forminf.cc (form_eventual_universal_visitor,
|
||||||
inf_form_right_recurse_visitor, inf_form_left_recurse_visitor): Rename
|
inf_form_right_recurse_visitor, inf_form_left_recurse_visitor): Rename
|
||||||
|
|
|
||||||
|
|
@ -30,18 +30,17 @@ check_SCRIPTS = defs
|
||||||
# Keep this sorted alphabetically.
|
# Keep this sorted alphabetically.
|
||||||
check_PROGRAMS = \
|
check_PROGRAMS = \
|
||||||
equals \
|
equals \
|
||||||
inf \
|
|
||||||
ltl2dot \
|
ltl2dot \
|
||||||
ltl2text \
|
ltl2text \
|
||||||
lunabbrev \
|
lunabbrev \
|
||||||
nenoform \
|
nenoform \
|
||||||
reduc \
|
reduc \
|
||||||
|
syntimpl \
|
||||||
tostring \
|
tostring \
|
||||||
tunabbrev \
|
tunabbrev \
|
||||||
tunenoform
|
tunenoform
|
||||||
|
|
||||||
equals_SOURCES = equals.cc
|
equals_SOURCES = equals.cc
|
||||||
inf_SOURCES = inf.cc
|
|
||||||
ltl2dot_SOURCES = readltl.cc
|
ltl2dot_SOURCES = readltl.cc
|
||||||
ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY
|
ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY
|
||||||
ltl2text_SOURCES = readltl.cc
|
ltl2text_SOURCES = readltl.cc
|
||||||
|
|
@ -50,6 +49,7 @@ lunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DLUNABBREV
|
||||||
nenoform_SOURCES = equals.cc
|
nenoform_SOURCES = equals.cc
|
||||||
nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM
|
nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM
|
||||||
reduc_SOURCES = reduc.cc
|
reduc_SOURCES = reduc.cc
|
||||||
|
syntimpl_SOURCES = syntimpl.cc
|
||||||
tostring_SOURCES = tostring.cc
|
tostring_SOURCES = tostring.cc
|
||||||
tunabbrev_SOURCES = equals.cc
|
tunabbrev_SOURCES = equals.cc
|
||||||
tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DTUNABBREV
|
tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DTUNABBREV
|
||||||
|
|
@ -69,7 +69,7 @@ TESTS = \
|
||||||
tunabbrev.test \
|
tunabbrev.test \
|
||||||
nenoform.test \
|
nenoform.test \
|
||||||
tunenoform.test \
|
tunenoform.test \
|
||||||
inf.test \
|
syntimpl.test \
|
||||||
reduc.test
|
reduc.test
|
||||||
|
|
||||||
CLEANFILES = stdout expect parse.dot result.data
|
CLEANFILES = stdout expect parse.dot result.data
|
||||||
|
|
|
||||||
|
|
@ -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'
|
|
||||||
|
|
@ -25,10 +25,9 @@
|
||||||
#include "ltlvisit/lunabbrev.hh"
|
#include "ltlvisit/lunabbrev.hh"
|
||||||
#include "ltlvisit/tunabbrev.hh"
|
#include "ltlvisit/tunabbrev.hh"
|
||||||
#include "ltlvisit/dump.hh"
|
#include "ltlvisit/dump.hh"
|
||||||
#include "ltlvisit/nenoform.hh"
|
|
||||||
#include "ltlvisit/destroy.hh"
|
#include "ltlvisit/destroy.hh"
|
||||||
#include "ltlvisit/tostring.hh"
|
#include "ltlvisit/tostring.hh"
|
||||||
#include "ltlvisit/reducform.hh"
|
#include "ltlvisit/syntimpl.hh"
|
||||||
#include "ltlast/allnodes.hh"
|
#include "ltlast/allnodes.hh"
|
||||||
|
|
||||||
void
|
void
|
||||||
83
src/ltltest/syntimpl.test
Executable file
83
src/ltltest/syntimpl.test
Executable file
|
|
@ -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)'
|
||||||
|
|
@ -34,6 +34,7 @@ ltlvisit_HEADERS = \
|
||||||
nenoform.hh \
|
nenoform.hh \
|
||||||
postfix.hh \
|
postfix.hh \
|
||||||
reducform.hh \
|
reducform.hh \
|
||||||
|
syntimpl.hh \
|
||||||
tostring.hh \
|
tostring.hh \
|
||||||
tunabbrev.hh
|
tunabbrev.hh
|
||||||
|
|
||||||
|
|
@ -44,11 +45,11 @@ libltlvisit_la_SOURCES = \
|
||||||
destroy.cc \
|
destroy.cc \
|
||||||
dotty.cc \
|
dotty.cc \
|
||||||
dump.cc \
|
dump.cc \
|
||||||
forminf.cc \
|
|
||||||
length.cc \
|
length.cc \
|
||||||
lunabbrev.cc \
|
lunabbrev.cc \
|
||||||
nenoform.cc \
|
nenoform.cc \
|
||||||
postfix.cc \
|
postfix.cc \
|
||||||
reducform.cc \
|
reducform.cc \
|
||||||
|
syntimpl.cc \
|
||||||
tostring.cc \
|
tostring.cc \
|
||||||
tunabbrev.cc
|
tunabbrev.cc
|
||||||
|
|
|
||||||
|
|
@ -20,6 +20,7 @@
|
||||||
// 02111-1307, USA.
|
// 02111-1307, USA.
|
||||||
|
|
||||||
#include "reducform.hh"
|
#include "reducform.hh"
|
||||||
|
#include "syntimpl.hh"
|
||||||
#include "ltlast/allnodes.hh"
|
#include "ltlast/allnodes.hh"
|
||||||
#include <cassert>
|
#include <cassert>
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -56,16 +56,6 @@ namespace spot
|
||||||
/// Basic rewritings.
|
/// Basic rewritings.
|
||||||
formula* basic_reduce(const formula* f);
|
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.
|
/// \brief Check whether a formula is eventual.
|
||||||
///
|
///
|
||||||
/// FIXME: Describe what eventual formulae are. Cite paper.
|
/// FIXME: Describe what eventual formulae are. Cite paper.
|
||||||
|
|
|
||||||
|
|
@ -19,7 +19,7 @@
|
||||||
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
||||||
// 02111-1307, USA.
|
// 02111-1307, USA.
|
||||||
|
|
||||||
#include "reducform.hh"
|
#include "syntimpl.hh"
|
||||||
#include "ltlast/allnodes.hh"
|
#include "ltlast/allnodes.hh"
|
||||||
#include <cassert>
|
#include <cassert>
|
||||||
|
|
||||||
45
src/ltlvisit/syntimpl.hh
Normal file
45
src/ltlvisit/syntimpl.hh
Normal file
|
|
@ -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
|
||||||
Loading…
Add table
Add a link
Reference in a new issue