Print F"proc.st" as Fproc.st.
* src/ltlvisit/tostring.cc: Allow '.' in bare words while printing atomic propositions. * src/ltltest/bare.test: New file. * src/ltltest/Makefile.am: Add it.
This commit is contained in:
parent
af639e58c7
commit
64484e7816
3 changed files with 36 additions and 2 deletions
|
|
@ -76,6 +76,7 @@ EXTRA_DIST = $(TESTS)
|
||||||
|
|
||||||
# Ordered by strength of the test. Test basic features first.
|
# Ordered by strength of the test. Test basic features first.
|
||||||
TESTS = \
|
TESTS = \
|
||||||
|
bare.test \
|
||||||
parse.test \
|
parse.test \
|
||||||
parseerr.test \
|
parseerr.test \
|
||||||
utf8.test \
|
utf8.test \
|
||||||
|
|
|
||||||
33
src/ltltest/bare.test
Executable file
33
src/ltltest/bare.test
Executable file
|
|
@ -0,0 +1,33 @@
|
||||||
|
#!/bin/sh
|
||||||
|
# -*- coding: utf-8 -*-
|
||||||
|
# Copyright (C) 2012 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
|
||||||
|
set -e
|
||||||
|
|
||||||
|
test "`../../bin/ltlfilt -p -f 'GFP_0.b_c'`" = "(G(F(P_0.b_c)))"
|
||||||
|
test "`../../bin/ltlfilt -f 'GFP_0.b_c'`" = "GFP_0.b_c"
|
||||||
|
foo=`../../bin/ltlfilt -p -f 'GF"P_0.b_c"'`
|
||||||
|
test "$foo" = "(G(F(P_0.b_c)))"
|
||||||
|
|
||||||
|
foo=`../../bin/ltlfilt -p -f '"a.b" U c.d.e'`
|
||||||
|
test "$foo" = "(a.b) U (c.d.e)"
|
||||||
|
|
||||||
|
foo=`../../bin/ltlfilt -f '"a.b" U c.d.e'`
|
||||||
|
test "$foo" = "a.b U c.d.e"
|
||||||
|
|
@ -198,13 +198,13 @@ namespace spot
|
||||||
|| *str == 'F'
|
|| *str == 'F'
|
||||||
|| *str == 'G'
|
|| *str == 'G'
|
||||||
|| *str == 'X'
|
|| *str == 'X'
|
||||||
|| !(isalpha(*str) || *str == '_')
|
|| !(isalpha(*str) || *str == '_' || *str == '.')
|
||||||
|| !strcasecmp(str, "true")
|
|| !strcasecmp(str, "true")
|
||||||
|| !strcasecmp(str, "false"))
|
|| !strcasecmp(str, "false"))
|
||||||
return false;
|
return false;
|
||||||
// The remaining of the word must be alphanumeric.
|
// The remaining of the word must be alphanumeric.
|
||||||
while (*++str)
|
while (*++str)
|
||||||
if (!(isalnum(*str) || *str == '_'))
|
if (!(isalnum(*str) || *str == '_' || *str == '.'))
|
||||||
return false;
|
return false;
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue