098e121a36
* src/tgbaalgos/ltl2tgba_fm.cc (ratexp_to_dfa::translate): Do not translate a subformula if we have already proved it useless in a previous rational expression. * src/tgbatest/ltl2tgba.test: Add an example, although that test does not ensure the subformula is ignored early in the translation. I.e., it would still work without the patch.
192 lines
6.3 KiB
Bash
Executable file
192 lines
6.3 KiB
Bash
Executable file
#!/bin/sh
|
|
# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
|
|
# de l'Epita (LRDE).
|
|
# Copyright (C) 2003, 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.
|
|
|
|
|
|
. ./defs
|
|
|
|
set -e
|
|
|
|
check_psl ()
|
|
{
|
|
# We don't check the output, but just running these might be enough to
|
|
# trigger assertions.
|
|
run 0 ../ltl2tgba -f -FC "$1"
|
|
# Make cross products with FM
|
|
run 0 ../ltl2tgba -f -R3 -b "$1" > out.tgba
|
|
run 0 ../ltl2tgba -f -R3 -Pout.tgba -E "!($1)"
|
|
run 0 ../ltl2tgba -f -x -R3 -b "$1" > out.tgba
|
|
run 0 ../ltl2tgba -f -x -R3 -Pout.tgba -E "!($1)"
|
|
}
|
|
|
|
check_ltl ()
|
|
{
|
|
check_psl "$@"
|
|
# Make cross products with LaCIM
|
|
run 0 ../ltl2tgba -l -R3b -b "$1" > out.tgba
|
|
run 0 ../ltl2tgba -l -R3b -Pout.tgba -E "!($1)"
|
|
}
|
|
|
|
check_ltl a
|
|
check_ltl 'a U b'
|
|
check_ltl 'X a'
|
|
check_ltl 'a & b & c'
|
|
check_ltl 'a | b | (c U (d & (g U (h ^ i))))'
|
|
check_ltl 'Xa & (b U !a) & (b U !a)'
|
|
check_ltl 'Fa & Xb & GFc & Gd'
|
|
check_ltl 'Fa & Xa & GFc & Gc'
|
|
check_ltl 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
|
|
check_ltl 'a R (b R c)'
|
|
check_ltl '(a U b) U (c U d)'
|
|
|
|
check_ltl '((Xp2)U(X(1)))&(p1 R(p2 R p0))'
|
|
|
|
check_psl '{a*;c}<>->GFb'
|
|
check_psl '{((a*;b;c)*)&((b*;a;c)*)}<>->x'
|
|
check_psl '{(g;y;r)*}<>->x'
|
|
check_psl 'G({(g;y;r)*}<>->x)'
|
|
check_psl 'G({(a;b)*}<>->x)&G({(c;d)*}<>->y)'
|
|
check_psl 'G({{a;b}*}[]->x)&G({{c;d}*}[]->y)' # try sub-braces
|
|
check_psl '{([*0] + a):c*:([*0] + b)}<>->d'
|
|
check_psl '{a;e;f:(g*);h}<>->d'
|
|
check_psl '{(a:b)* & (c*:d)}<>->e'
|
|
check_psl '{(a:b)*}'
|
|
check_psl 'G{(a:b)*}'
|
|
check_psl '{a;b}'
|
|
check_psl '{(a;b)*}'
|
|
check_psl 'G{(a;b)*}'
|
|
check_psl '{a*}[]->{b*}'
|
|
check_psl '{a*}[]=>{b*}'
|
|
check_psl '{a*&b}'
|
|
check_psl '{a*&b*}'
|
|
check_psl '{((!c;b*) & d);e}'
|
|
check_psl '{(a* & (c;b*) & d);e}'
|
|
check_psl '{[*2];a[*2..4]}|->b'
|
|
check_psl '{a[*2..5] && b[*..3]}|->c'
|
|
check_psl '{{[+];a;[+]} && {[+];b;[+]}}<>->c'
|
|
check_psl '{(a[->3]) & {[+];b}}<>->c'
|
|
# This formula (built by a random formula generator), exhibited an
|
|
# infinite recursion in the translation:
|
|
check_psl '{(a|[*0])[*];1}'
|
|
# Example from "Beyond Hardware Verification" by Glazberg, Moulin, Orni,
|
|
# Ruah, Zarpas (2007).
|
|
check_psl '{[*];req;ack}|=>{start;busy[*];done}'
|
|
# Examples from "Property-by-Example Guide: a Handbook of PSL Examples"
|
|
# by Ben David and Orni (2005)/
|
|
check_psl '{end[=3]}(false)' # 2.27.A
|
|
check_psl '{[*]; {read[=3]} && {write[=2]}} |=>
|
|
{(!read && !write)[*]; ready}' # 3.5.A
|
|
check_psl '{[*]; start && comp_data_en; !comp_data_en && good_comp;
|
|
{status_valid[->]} && {stop[=0]; true}} |-> {!data_out}' # 2.33
|
|
|
|
# Some tricky cases that require the rational automaton to be pruned
|
|
# before it is used in the translation.
|
|
check_psl '{{b[*];c} | {{a && !a}}[=2]}'
|
|
check_psl '{((a&!b);((!a&!b)*))&&(!b*;(!a&b))}'
|
|
# When translating this formula, we expect the translator to ignore
|
|
# `a;(f&!f)[=2];c' on one side because it as already seen it on the
|
|
# other side.
|
|
check_psl '{c;a;(f&!f)[=2];c}|{b;a;(!f&f)[=2];c}'
|
|
|
|
# Make sure 'a U (b U c)' has 3 states and 6 transitions,
|
|
# before and after degeneralization.
|
|
for opt in '' -D -DS; do
|
|
../ltl2tgba -ks -f -R3 $opt 'a U (b U c)' > stdout
|
|
grep 'transitions: 6$' stdout
|
|
grep 'states: 3$' stdout
|
|
done
|
|
|
|
# Make sure '!(Ga U b)' has 3 states and 6 transitions,
|
|
# before and after degeneralization.
|
|
for opt in '' -D -DS; do
|
|
../ltl2tgba -kt -f -R3 $opt '!(Ga U b)' > stdout
|
|
grep 'sub trans.: 11$' stdout
|
|
grep 'transitions: 6$' stdout
|
|
grep 'states: 3$' stdout
|
|
done
|
|
|
|
# Make sure 'Ga U b' has 4 states and 6 transitions,
|
|
# before and after degeneralization.
|
|
for opt in '' -D -DS; do
|
|
../ltl2tgba -kt -f -R3 $opt 'Ga U b' > stdout
|
|
grep 'sub trans.: 12$' stdout
|
|
grep 'transitions: 6$' stdout
|
|
grep 'states: 4$' stdout
|
|
done
|
|
|
|
# Make sure '(G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))'
|
|
# has 6 states and 15 transitions, before and after degeneralization.
|
|
f='(G (p -> F q)) && ((X (p) U q) || ! X (p U (p && q)))'
|
|
for opt in '' -D -DS; do
|
|
../ltl2tgba -ks -f -R3 $opt "$f" > stdout
|
|
grep 'transitions: 15$' stdout
|
|
grep 'states: 6$' stdout
|
|
done
|
|
# Note: this is worse with -R3f.
|
|
../ltl2tgba -ks -f -R3f -DS "$f" > stdout
|
|
grep 'transitions: 17$' stdout
|
|
grep 'states: 7$' stdout
|
|
|
|
# Make sure 'GFa & GFb & GFc & GFd & GFe & GFf'
|
|
# has 7 states and 34 transitions after degeneralization.
|
|
f='GFa & GFb & GFc & GFd & GFe & GFg'
|
|
../ltl2tgba -ks -DS -x -f "$f" > stdout
|
|
grep 'transitions: 34$' stdout
|
|
grep 'states: 7$' stdout
|
|
|
|
# Make sure 'Ga & XXXX!a' is minimized to one state.
|
|
f='Ga & XXXX!a'
|
|
../ltl2tgba -ks -f "$f" > stdout
|
|
grep 'transitions: 4$' stdout
|
|
grep 'states: 5$' stdout
|
|
../ltl2tgba -ks -Rm -f "$f" > stdout
|
|
grep 'transitions: 0$' stdout
|
|
grep 'states: 1$' stdout
|
|
|
|
# Make sure a monitor for F(a & F(b)) accepts everything.
|
|
run 0 ../ltl2tgba -M -f "F(a & F(b))" | grep ' ->' > stdout
|
|
cat >expected <<EOF
|
|
0 -> 1
|
|
1 -> 1 [label="1\n"]
|
|
EOF
|
|
cmp stdout expected
|
|
|
|
# This formula caused a segfault with Spot 0.7.
|
|
run 0 ../ltl2tgba -Rm -ks -f "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout
|
|
grep 'transitions: 5$' stdout
|
|
grep 'states: 3$' stdout
|
|
|
|
# Adding -R3 used to make it work...
|
|
run 0 ../ltl2tgba -R3 -Rm -ks -f "Gq|Gr|(G(q|FGp)&G(r|FG!p))" >stdout
|
|
grep 'transitions: 5$' stdout
|
|
grep 'states: 3$' stdout
|
|
|
|
# Make sure FGa|GFb has the same number of states/transitions when
|
|
# output as a never claim or are a degeneralized BA in Spot's textual
|
|
# format. The option -R1q -R1t used to cause two degeneralizations to
|
|
# occur.
|
|
run 0 ../ltl2tgba -R1q -R1t -N 'FGa|FGb' > out.never
|
|
run 0 ../ltl2tgba -XN -kt out.never > count.never
|
|
run 0 ../ltl2tgba -R1q -R1t -DS -b 'FGa|FGb' > out.spot
|
|
run 0 ../ltl2tgba -X -kt out.spot > count.spot
|
|
cmp count.never count.spot
|