614810c0db
* doc/tl/tl.tex: Document the rules. * src/ltlvisit/simplify.cc (simplify_visitor): Implement them. * src/ltltest/reduccmp.test: Test them.
238 lines
7.7 KiB
Bash
Executable file
238 lines
7.7 KiB
Bash
Executable file
#! /bin/sh
|
|
# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Developpement
|
|
# de l'Epita (LRDE).
|
|
# Copyright (C) 2004, 2006 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 LTL reductions
|
|
|
|
. ./defs || exit 1
|
|
|
|
for x in ../reduccmp ../reductaustr; do
|
|
|
|
# No reduction
|
|
run 0 $x 'a U b' 'a U b'
|
|
run 0 $x 'a R b' 'a R b'
|
|
run 0 $x 'a & b' 'a & b'
|
|
run 0 $x 'a | b' 'a | b'
|
|
run 0 $x 'a & (a U b)' 'a & (a U b)'
|
|
run 0 $x 'a | (a U b)' 'a | (a U b)'
|
|
|
|
# Syntactic reduction
|
|
run 0 $x 'a & (!b R !a)' 'false'
|
|
run 0 $x '(!b R !a) & a' 'false'
|
|
run 0 $x 'a & (!b R !a) & c' 'false'
|
|
run 0 $x 'c & (!b R !a) & a' 'false'
|
|
|
|
run 0 $x 'a & (!b M !a)' 'false'
|
|
run 0 $x '(!b M !a) & a' 'false'
|
|
run 0 $x 'a & (!b M !a) & c' 'false'
|
|
run 0 $x 'c & (!b M !a) & a' 'false'
|
|
|
|
run 0 $x 'a & (b U a)' 'a'
|
|
run 0 $x '(b U a) & a' 'a'
|
|
run 0 $x 'a | (b U a)' '(b U a)'
|
|
run 0 $x '(b U a) | a' '(b U a)'
|
|
run 0 $x 'a U (b U a)' '(b U a)'
|
|
|
|
run 0 $x 'a & (b W a)' 'a'
|
|
run 0 $x '(b W a) & a' 'a'
|
|
run 0 $x 'a | (b W a)' '(b W a)'
|
|
run 0 $x '(b W a) | a' '(b W a)'
|
|
run 0 $x 'a W (b W a)' '(b W a)'
|
|
|
|
run 0 $x 'a & (b U a) & a' 'a'
|
|
run 0 $x 'a & (b U a) & a' 'a'
|
|
run 0 $x 'a | (b U a) | a' '(b U a)'
|
|
run 0 $x 'a | (b U a) | a' '(b U a)'
|
|
run 0 $x 'a U (b U a)' '(b U a)'
|
|
|
|
run 0 $x 'a <-> !a' '0'
|
|
run 0 $x 'a <-> a' '1'
|
|
run 0 $x 'a ^ a' '0'
|
|
run 0 $x 'a ^ !a' '1'
|
|
|
|
run 0 $x 'GFa | FGa' 'GFa'
|
|
run 0 $x 'XXGa | GFa' 'GFa'
|
|
run 0 $x 'GFa & FGa' 'FGa'
|
|
run 0 $x 'XXGa & GFa' 'XXGa'
|
|
|
|
# Basic reductions
|
|
run 0 $x 'X(true)' 'true'
|
|
run 0 $x 'X(false)' 'false'
|
|
run 0 $x 'F(true)' 'true'
|
|
run 0 $x 'F(false)' 'false'
|
|
|
|
run 0 $x 'XGF(f)' 'GF(f)'
|
|
|
|
case $x in
|
|
*tau*);;
|
|
*)
|
|
run 0 $x 'G(true)' 'true'
|
|
run 0 $x 'G(false)' 'false'
|
|
|
|
run 0 $x 'a M 1' 'Fa'
|
|
run 0 $x 'a W 0' 'Ga'
|
|
run 0 $x '1 U a' 'Fa'
|
|
run 0 $x '0 R a' 'Ga'
|
|
|
|
run 0 $x 'G(a R b)' 'G(b)'
|
|
|
|
run 0 $x 'FX(a)' 'XF(a)'
|
|
run 0 $x 'GX(a)' 'XG(a)'
|
|
|
|
run 0 $x 'X(a) U X(b)' 'X(a U b)'
|
|
run 0 $x 'X(a) R X(b)' 'X(a R b)'
|
|
run 0 $x 'Xa & Xb' 'X(a & b)'
|
|
run 0 $x 'Xa | Xb' 'X(a | b)'
|
|
|
|
run 0 $x '(a U b) & (c U b)' '(a & c) U b'
|
|
run 0 $x '(a R b) & (a R c)' 'a R (b & c)'
|
|
run 0 $x '(a U b) | (a U c)' 'a U (b | c)'
|
|
run 0 $x '(a R b) | (c R b)' '(a | c) R b'
|
|
|
|
run 0 $x 'Xa & FGb' 'X(a & FGb)'
|
|
run 0 $x 'Xa | FGb' 'X(a | FGb)'
|
|
run 0 $x 'Xa & GFb' 'X(a & GFb)'
|
|
run 0 $x 'Xa | GFb' 'X(a | GFb)'
|
|
# The following is not reduced to F(a) & GFb. because
|
|
# (1) is does not help the translate the formula into a
|
|
# smaller automaton, and ...
|
|
run 0 $x 'F(a & GFb)' 'F(a & GFb)'
|
|
# (2) ... it would hinder this useful reduction (that helps to
|
|
# produce a smaller automaton)
|
|
run 0 $x 'F(f1 & GF(f2)) | F(a & GF(b))' 'F((f1&GFf2)|(a&GFb))'
|
|
# FIXME: Don't we want the opposite rewriting?
|
|
# rewriting Fa & GFb as F(a & GFb) seems better, but
|
|
# it not clear how that scales to Fa & Fb & GFc...
|
|
run 0 $x 'Fa & GFb' 'Fa & GFb'
|
|
run 0 $x 'G(a | GFb)' 'Ga | GFb'
|
|
# The following is not reduced to F(a & c) & GF(b) for the same
|
|
# reason as above.
|
|
run 0 $x 'F(a & GFb & c)' 'F(a & GFb & c)'
|
|
run 0 $x 'G(a | GFb | c)' 'G(a | c) | GFb'
|
|
|
|
run 0 $x 'GFa <=> GFb' 'G(Fa&Fb)|FG(!a&!b)'
|
|
|
|
run 0 $x 'Gb W a' 'Gb|a'
|
|
run 0 $x 'Fb M Fa' 'Fa & Fb'
|
|
|
|
run 0 $x 'a U (b | G(a) | c)' 'a W (b | c)'
|
|
run 0 $x 'a U (G(a))' 'Ga'
|
|
run 0 $x '(a U b) | (a W c)' 'a W (b | c)'
|
|
run 0 $x '(a U b) | Ga' 'a W b'
|
|
|
|
run 0 $x 'a R (b & F(a) & c)' 'a M (b & c)'
|
|
run 0 $x 'a R (F(a))' 'Fa'
|
|
run 0 $x '(a R b) & (a M c)' 'a M (b & c)'
|
|
run 0 $x '(a R b) & Fa' 'a M b'
|
|
|
|
run 0 $x '(a U b) & (c W b)' '(a & c) U b'
|
|
run 0 $x '(a W b) & (c W b)' '(a & c) W b'
|
|
run 0 $x '(a R b) | (c M b)' '(a | c) R b'
|
|
run 0 $x '(a M b) | (c M b)' '(a | c) M b'
|
|
|
|
run 0 $x '(a R b) | Gb' 'a R b'
|
|
run 0 $x '(a M b) | Gb' 'a R b'
|
|
run 0 $x '(a U b) & Fb' 'a U b'
|
|
run 0 $x '(a W b) & Fb' 'a U b'
|
|
run 0 $x '(a M b) | Gb | (c M b)' '(a | c) R b'
|
|
|
|
run 0 $x 'GFGa' 'FGa'
|
|
run 0 $x 'b R Ga' 'Ga'
|
|
run 0 $x 'b R FGa' 'FGa'
|
|
|
|
run 0 $x 'G(!a M a) M 1' '0'
|
|
run 0 $x 'G(!a M a) U 1' '1'
|
|
run 0 $x 'a R (!a M a)' '0'
|
|
run 0 $x 'a W (!a M a)' 'Ga'
|
|
|
|
# Syntactic implication
|
|
run 0 $x '(a & b) R (a R c)' '(a & b)R c'
|
|
run 0 $x 'a R ((a & b) R c)' '(a & b)R c'
|
|
run 0 $x 'a R ((a & b) M c)' '(a & b)M c'
|
|
run 0 $x 'a M ((a & b) M c)' '(a & b)M c'
|
|
run 0 $x '(a & b) M (a R c)' '(a & b)M c'
|
|
run 0 $x '(a & b) M (a M c)' '(a & b)M c'
|
|
|
|
# Eventuality and universality class reductions
|
|
run 0 $x 'Fa M b' 'Fa & b'
|
|
run 0 $x 'GFa M b' 'GFa & b'
|
|
|
|
run 0 $x 'Fa|Xb|GFc' 'Fa | X(b|GFc)'
|
|
run 0 $x 'Fa|GFc' 'F(a|GFc)'
|
|
run 0 $x 'FGa|GFc' 'F(Ga|GFc)'
|
|
run 0 $x 'Ga&Xb&FGc' 'Ga & X(b&FGc)'
|
|
run 0 $x 'Ga&Xb&GFc' 'Ga & X(b&GFc)'
|
|
run 0 $x 'Ga&GFc' 'G(a&Fc)'
|
|
run 0 $x 'G(a|b|GFc|GFd|FGe|FGf)' 'G(a|b)|GF(c|d)|F(Ge|Gf)'
|
|
run 0 $x 'G(a|b)|GFc|GFd|FGe|FGf' 'G(a|b)|GF(c|d)|F(Ge|Gf)'
|
|
run 0 $x 'X(a|b)|GFc|GFd|FGe|FGf' 'X(a|b|GF(c|d)|F(Ge|Gf))'
|
|
run 0 $x 'Xa&Xb&GFc&GFd&Ge' 'X(a&b&G(Fc&Fd))&Ge'
|
|
|
|
# F comes in front when possible...
|
|
run 0 $x 'GFc|GFd|FGe|FGf' 'F(GF(c|d)|Ge|Gf)'
|
|
run 0 $x 'G(GFc|GFd|FGe|FGf)' 'F(GF(c|d)|Ge|Gf)'
|
|
|
|
# Because reduccmp will translate the formula,
|
|
# this also check for an old bug in ltl2tgba_fm.
|
|
run 0 $x '{(c&!c)[->0..1]}!' '0'
|
|
|
|
# Tricky case that used to break the translator,
|
|
# because it was translating closer on-the-fly
|
|
# without pruning the rational automaton.
|
|
run 0 $x '{(c&!c)[=2]}' '0'
|
|
|
|
run 0 $x '{a && b && c*} <>-> d' 'a&b&c&d'
|
|
run 0 $x '{a && b && c[*1..3]} <>-> d' 'a&b&c&d'
|
|
run 0 $x '{a && b && c[->0..2]} <>-> d' 'a&b&c&d'
|
|
run 0 $x '{a && b && c[+]} <>-> d' 'a&b&c&d'
|
|
run 0 $x '{a && b && c[=1]} <>-> d' 'a&b&c&d'
|
|
run 0 $x '{a && b && d[=2]} <>-> d' '0'
|
|
run 0 $x '{a && b && d[*2..]} <>-> d' '0'
|
|
run 0 $x '{a && b && d[->2..4]} <>-> d' '0'
|
|
run 0 $x '{a && { c* : b* : (g|h)*}} <>-> d' 'a & c & b & (g | h) & d'
|
|
run 0 $x '{a && {b;c}} <>-> d' '0'
|
|
run 0 $x '{a && {b;c:e}} <>-> d' '0'
|
|
run 0 $x '{a && {b*;c*}} <>-> d' '{a && {b*|c*}} <>-> d' # until better
|
|
run 0 $x '{a && {b*;c*:e}} <>-> d' '{a && {b*|c*} && e} <>-> d' # idem
|
|
run 0 $x '{a && {b*;c}} <>-> d' 'a & c & d'
|
|
run 0 $x '{a && {b*;c:e}} <>-> d' 'a & c & d & e'
|
|
run 0 $x '{a && {b;c*}} <>-> d' 'a & b & d'
|
|
run 0 $x '{a && {b;c*:e}} <>-> d' 'a & b & d & e'
|
|
;;
|
|
esac
|
|
|
|
run 0 $x 'a R (b W G(c))' 'a R (b W G(c))' #not reduced
|
|
|
|
run 0 $x 'a M ((a&b) R c)' 'a M ((a&b) R c)' #not reduced.
|
|
run 0 $x '(a&b) W (a U c)' '(a&b) W (a U c)' #not reduced.
|
|
|
|
# Eventuality and universality class reductions
|
|
run 0 $x 'FFa' 'Fa'
|
|
run 0 $x 'FGFa' 'GFa'
|
|
run 0 $x 'b U Fa' 'Fa'
|
|
run 0 $x 'b U GFa' 'GFa'
|
|
run 0 $x 'Ga' 'Ga'
|
|
|
|
run 0 $x 'a U XXXFb' 'XXXFb'
|
|
done
|