ltlparse: Add compatibility with ltl2dsar's input.
* src/ltlparse/ltlscan.ll: Accept as a proposition any alphanumeric string that is not an operator. * NEWS: Mention it. * src/ltltest/lbt.test: New file. Also tests previous patch. * src/ltltest/Makefile.am: Add it.
This commit is contained in:
Alexandre Duret-Lutz
parent
3a5eec42de
commit
edd687a301
4 changed files with 130 additions and 6 deletions
4
NEWS
4
NEWS
|
|
@ -27,6 +27,10 @@ New in spot 1.0a (not released):
|
|||
transition counts, just as the ltlcross tool.
|
||||
- ltlcross will display the number of timeouts at the end
|
||||
of its execution.
|
||||
- The parser for LBT's prefix-style LTL formulas will now
|
||||
read atomic propositions that are not of the form p1, p2...
|
||||
This makes it possible to process formulas written in
|
||||
ltl2dstar's syntax.
|
||||
* Pruning:
|
||||
- lbtt has been removed from the distribution. A copy of the last
|
||||
version we distributed is still available at
|
||||
|
|
|
|||
|
|
@ -1,4 +1,5 @@
|
|||
/* Copyright (C) 2010, 2011, 2012, Laboratoire de Recherche et
|
||||
/* -*- coding: utf-8 -*-
|
||||
** Copyright (C) 2010, 2011, 2012, 2013, 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
|
||||
|
|
@ -87,7 +88,10 @@ BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇"
|
|||
yylval->str = new std::string();
|
||||
}
|
||||
<in_par>{
|
||||
"(" ++parent_level; yylval->str->append(yytext, yyleng);
|
||||
"(" {
|
||||
++parent_level;
|
||||
yylval->str->append(yytext, yyleng);
|
||||
}
|
||||
")" {
|
||||
if (--parent_level)
|
||||
{
|
||||
|
|
@ -126,7 +130,10 @@ BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇"
|
|||
yylval->str = new std::string();
|
||||
}
|
||||
<in_bra>{
|
||||
"{" ++parent_level; yylval->str->append(yytext, yyleng);
|
||||
"{" {
|
||||
++parent_level;
|
||||
yylval->str->append(yytext, yyleng);
|
||||
}
|
||||
"}"[ \t\n]*"!" {
|
||||
if (--parent_level)
|
||||
{
|
||||
|
|
@ -281,11 +288,16 @@ BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇"
|
|||
return token::ATOMIC_PROP;
|
||||
}
|
||||
|
||||
/* in LBT's format, atomic proposition look like p0 or p3141592 */
|
||||
<lbt>p[0-9]+ {
|
||||
/* these are operators */
|
||||
<lbt>[eitfXFGUVRWM] return *yytext;
|
||||
/* in LBT's format, atomic proposition look like p0 or p3141592, but
|
||||
for compatibility with ltl2dstar we also accept any alphanumeric
|
||||
string that is not an operator. */
|
||||
<lbt>[a-zA-Z._][a-zA-Z0-9._]* {
|
||||
yylval->str = new std::string(yytext, yyleng);
|
||||
return token::ATOMIC_PROP;
|
||||
}
|
||||
|
||||
/* Atomic propositions can also be enclosed in double quotes. */
|
||||
<lbt>\"[^\"]*\" {
|
||||
yylval->str = new std::string(yytext + 1,
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
## Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
|
||||
## Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche et
|
||||
## Développement de l'Epita (LRDE).
|
||||
## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
|
||||
## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
|
|
@ -90,6 +90,7 @@ TESTS = \
|
|||
unabbrevwm.test \
|
||||
consterm.test \
|
||||
kind.test \
|
||||
lbt.test \
|
||||
lenient.test \
|
||||
syntimpl.test \
|
||||
reduc.test \
|
||||
|
|
|
|||
107
src/ltltest/lbt.test
Executable file
107
src/ltltest/lbt.test
Executable file
|
|
@ -0,0 +1,107 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2013 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
. ./defs
|
||||
|
||||
ltlfilt=../../bin/ltlfilt
|
||||
randltl=../../bin/randltl
|
||||
genltl=../../bin/genltl
|
||||
|
||||
# Some example formulas taken from Ruediger Ehlers's dbaminimizer
|
||||
# http://react.cs.uni-saarland.de/tools/dbaminimizer
|
||||
# which are expected to be processed by ltl2dstar.
|
||||
cat >formulas <<'EOF'
|
||||
& G F a G F b
|
||||
X X a
|
||||
G F e a X X b
|
||||
G F e a X X X b
|
||||
G i a X X X b
|
||||
G F i a X X X b
|
||||
& G i a F b G i b F c
|
||||
G i a F b
|
||||
& G i a F b G c
|
||||
& & G ! c G i a F b G i b F c
|
||||
& G i a F b G i c F d
|
||||
& i G a F b i G ! a F ! b
|
||||
& G i a F b G i ! a F ! b
|
||||
U p & q X U r s
|
||||
U p & q X & r F & s X F & u X F & v X F w
|
||||
F & p X & q X F r
|
||||
F & q X U p r
|
||||
G i p U q r
|
||||
F & p X F & q X F & r X F s
|
||||
& & & & G F p G F q G F r G F s G F u
|
||||
| | U p U q r U q U r p U r U p q
|
||||
| | G F a G F b G F c
|
||||
G F a
|
||||
U a U b U c d
|
||||
G U a U b U ! a ! b
|
||||
EOF
|
||||
|
||||
# More examples taken from scheck's test suite.
|
||||
# http://tcs.legacy.ics.tkk.fi/users/tlatvala/scheck/
|
||||
cat >>formulas <<EOF
|
||||
| F X p1 F X p2
|
||||
| | X p7 F p6 & | | t p3 p7 U | f p3 p3
|
||||
F p99
|
||||
X p3
|
||||
X ! p3
|
||||
X t
|
||||
X X X p3
|
||||
F X X X t
|
||||
! G p5
|
||||
| X p0 F p5
|
||||
| F p2 F p9
|
||||
! | G p0 & G p1 F p3
|
||||
& U & X p0 X p4 F p1 X X U X F p5 U p0 X X p3
|
||||
| p3 p5
|
||||
& p1 p6
|
||||
| p1 | p2 p1
|
||||
| & p1 p3 p3
|
||||
p6
|
||||
U p1 ! p2
|
||||
| p5 U p2 p2
|
||||
& p5 U p2 p2
|
||||
U F p5 ! p1
|
||||
U p0 & | p0 p5 p1
|
||||
EOF
|
||||
|
||||
# More examples randomly generated
|
||||
$randltl -l -n 100 a p1 "X" "U" "U12" >> formulas
|
||||
|
||||
# Some examples from scalables formulas
|
||||
$genltl --rv-counter=1..10 --go-theta=1..10 -l >> formulas
|
||||
|
||||
count=`wc -l < formulas`
|
||||
|
||||
test $count -eq 168
|
||||
|
||||
run 0 $ltlfilt --lbt-input formulas > formulas.2
|
||||
run 0 $ltlfilt -l formulas.2 > formulas.3
|
||||
run 0 $ltlfilt -l --lbt-input formulas > formulas.4
|
||||
test `wc -l < formulas.2` -eq 168
|
||||
test `wc -l < formulas.3` -eq 168
|
||||
test `wc -l < formulas.4` -eq 168
|
||||
|
||||
|
||||
# Make sure ltl2dstar-style litterals always get quoted.
|
||||
test "`$ltlfilt -l --lbt-input -f 'G F a'`" = 'G F "a"'
|
||||
# Original lbt-style litterals are unquoted.
|
||||
test "`$ltlfilt -l --lbt-input -f 'G F p42'`" = 'G F p42'
|
||||
Loading…
Add table
Add a link
Reference in a new issue