From edd687a3011e1be55a9b6f9be7e4064221831b0f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 19 Jan 2013 15:29:27 +0100 Subject: [PATCH] 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. --- NEWS | 4 ++ src/ltlparse/ltlscan.ll | 22 +++++++-- src/ltltest/Makefile.am | 3 +- src/ltltest/lbt.test | 107 ++++++++++++++++++++++++++++++++++++++++ 4 files changed, 130 insertions(+), 6 deletions(-) create mode 100755 src/ltltest/lbt.test diff --git a/NEWS b/NEWS index e831ead7b..ead5684b7 100644 --- a/NEWS +++ b/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 diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll index db883d42c..912d0dabe 100644 --- a/src/ltlparse/ltlscan.ll +++ b/src/ltlparse/ltlscan.ll @@ -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(); } { - "(" ++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(); } { - "{" ++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 */ -p[0-9]+ { + /* these are operators */ +[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. */ +[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. */ \"[^\"]*\" { yylval->str = new std::string(yytext + 1, diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am index f6e0202e6..196fc6629 100644 --- a/src/ltltest/Makefile.am +++ b/src/ltltest/Makefile.am @@ -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 \ diff --git a/src/ltltest/lbt.test b/src/ltltest/lbt.test new file mode 100755 index 000000000..27029f7cf --- /dev/null +++ b/src/ltltest/lbt.test @@ -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 . + +. ./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 <> 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'