alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Do not recognize "*" as "and". This leaves room for an

Browse source 
implementation of rational operators in a future version.

* src/ltlparse/ltlscan.ll: Do not recognize "*".
* wrap/python/cgi-bin/ltl2tgba.in: Undocument it.
* NEWS: Mention this.
* src/tgbatest/kv.test, src/tgbatest/ltl2tgba.test,
src/tgbatest/reductgba.test: Replace "*" by "&".
This commit is contained in:
Alexandre Duret-Lutz 2010-01-30 11:41:31 +01:00
parent 55b693e123
commit 85532dc8f8
7 changed files with 30 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

11
ChangeLog
View file

@ -1,3 +1,14 @@
2010-01-30 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Do not recognize "*" as "and". This leaves room for an
implementation of rational operators in a future version.
* src/ltlparse/ltlscan.ll: Do not recognize "*".
* wrap/python/cgi-bin/ltl2tgba.in: Undocument it.
* NEWS: Mention this.
* src/tgbatest/kv.test, src/tgbatest/ltl2tgba.test,
src/tgbatest/reductgba.test: Replace "*" by "&".
2010-01-30 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2010-01-30 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Make Couvreur/FM the default translation. Make Couvreur/FM the default translation.

3
NEWS
View file

@ -39,6 +39,9 @@ New in spot 0.5 (2010-01-31):
function. This is ltl2tgba's -R3b option. function. This is ltl2tgba's -R3b option.
* The SCC-based simplification (ltl2tgba's -R3 option) has been * The SCC-based simplification (ltl2tgba's -R3 option) has been
rewritten and improved. rewritten and improved.
* The "*" symbol, previously parsed as a synonym for "&" is no
longer recognized. This makes room for an upcoming support of
rational operators.
* More benchmarks: * More benchmarks:
- gspn-ssp/ some benchmarks published at ACSD'07, - gspn-ssp/ some benchmarks published at ACSD'07,
- ltlcounter/ translation of a class of LTL formulae used by - ltlcounter/ translation of a class of LTL formulae used by

6
src/ltlparse/ltlscan.ll
View file

@ -1,4 +1,6 @@
/* Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), /* Copyright (C) 2010, 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 ** département Systèmes Répartis Coopératifs (SRC), Université Pierre
** et Marie Curie. ** et Marie Curie.
** **
@ -77,7 +79,7 @@ flex_set_buffer(const char* buf)
/\, \/, and xor are from LBTT. /\, \/, and xor are from LBTT.
*/ */
"||"|"|"|"+"|"\\/" BEGIN(0); return token::OP_OR; "||"|"|"|"+"|"\\/" BEGIN(0); return token::OP_OR;
"&&"|"&"|"."|"*"|"/\\" BEGIN(0); return token::OP_AND; "&&"|"&"|"."|"/\\" BEGIN(0); return token::OP_AND;
"^"|"xor" BEGIN(0); return token::OP_XOR; "^"|"xor" BEGIN(0); return token::OP_XOR;
"=>"|"->" BEGIN(0); return token::OP_IMPLIES; "=>"|"->" BEGIN(0); return token::OP_IMPLIES;
"<=>"|"<->" BEGIN(0); return token::OP_EQUIV; "<=>"|"<->" BEGIN(0); return token::OP_EQUIV;

4
src/tgbatest/kv.test
View file

@ -1,5 +1,5 @@
#!/bin/sh #!/bin/sh
# Copyright (C) 2009 Laboratoire de Recherche et Development de l'EPITA. # Copyright (C) 2009, 2010 Laboratoire de Recherche et Development de l'EPITA.
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
@ -35,7 +35,7 @@ check ()
check 'a R (b R c)' check 'a R (b R c)'
check '(a U b) U (c U d)' check '(a U b) U (c U d)'
check '((Xp2)U(X(1)))*(p1 R(p2 R p0))' check '((Xp2)U(X(1)))&(p1 R(p2 R p0))'
# Make sure escaped variables print OK. # Make sure escaped variables print OK.
check '"G1"U"GG" && "FF"' check '"G1"U"GG" && "FF"'

4
src/tgbatest/ltl2tgba.test
View file

@ -1,5 +1,5 @@
#!/bin/sh #!/bin/sh
# Copyright (C) 2009 Laboratoire de Recherche et Développement # Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
# de l'Epita (LRDE). # de l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -49,4 +49,4 @@ check 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
check 'a R (b R c)' check 'a R (b R c)'
check '(a U b) U (c U d)' check '(a U b) U (c U d)'
check '((Xp2)U(X(1)))*(p1 R(p2 R p0))' check '((Xp2)U(X(1)))&(p1 R(p2 R p0))'

10
src/tgbatest/reductgba.test
View file

@ -1,5 +1,5 @@
#!/bin/sh #!/bin/sh
# Copyright (C) 2009 Laboratoire de Recherche et Développement # Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
# de l'Epita (LRDE). # de l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -48,7 +48,7 @@ check 0 'Fa & Xa & GFc & Gc'
check 0 'Fc & X(a | Xb) & GF(a | Xb) & Gc' check 0 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
check 0 'a R (b R c)' check 0 'a R (b R c)'
check 0 '(a U b) U (c U d)' check 0 '(a U b) U (c U d)'
check 0 '((Xp2)U(X(1)))*(p1 R(p2 R p0))' check 0 '((Xp2)U(X(1)))&(p1 R(p2 R p0))'
check 0 '((p3 | Xp3 | Xp2) & (X!p3 | (!p3 & X!p2))) R F(0)' check 0 '((p3 | Xp3 | Xp2) & (X!p3 | (!p3 & X!p2))) R F(0)'
check 1 a check 1 a
@ -62,7 +62,7 @@ check 1 'Fa & Xa & GFc & Gc'
check 1 'Fc & X(a | Xb) & GF(a | Xb) & Gc' check 1 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
check 1 'a R (b R c)' check 1 'a R (b R c)'
check 1 '(a U b) U (c U d)' check 1 '(a U b) U (c U d)'
check 1 '((Xp2)U(X(1)))*(p1 R(p2 R p0))' check 1 '((Xp2)U(X(1)))&(p1 R(p2 R p0))'
check 2 a check 2 a
check 2 'a U b' check 2 'a U b'
@ -75,7 +75,7 @@ check 2 'Fa & Xa & GFc & Gc'
check 2 'Fc & X(a | Xb) & GF(a | Xb) & Gc' check 2 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
check 2 'a R (b R c)' check 2 'a R (b R c)'
check 2 '(a U b) U (c U d)' check 2 '(a U b) U (c U d)'
check 2 '((Xp2)U(X(1)))*(p1 R(p2 R p0))' check 2 '((Xp2)U(X(1)))&(p1 R(p2 R p0))'
check 3 a check 3 a
check 3 'a U b' check 3 'a U b'
@ -89,4 +89,4 @@ check 3 'Fa & Xa & GFc & Gc'
check 3 'Fc & X(a | Xb) & GF(a | Xb) & Gc' check 3 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
check 3 'a R (b R c)' check 3 'a R (b R c)'
check 3 '(a U b) U (c U d)' check 3 '(a U b) U (c U d)'
check 3 '((Xp2)U(X(1)))*(p1 R(p2 R p0))' check 3 '((Xp2)U(X(1)))&(p1 R(p2 R p0))'

7
wrap/python/cgi-bin/ltl2tgba.in
View file

@ -1,8 +1,8 @@
#!@PYTHON@ #!@PYTHON@
# -*- mode: python; coding: iso-8859-1 -*- # -*- mode: python; coding: iso-8859-1 -*-
# Copyright (C) 2009 Laboratoire de Recherche et Développement # Copyright (C) 2007, 2009, 2010 Laboratoire de Recherche et Développement
# de l'Epita (LRDE). # de l'Epita (LRDE).
# Copyright (C) 2003, 2004, 2006, 2007 Laboratoire d'Informatique de # Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
# Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), # Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
# Université Pierre et Marie Curie. # Université Pierre et Marie Curie.
# #
@ -294,8 +294,7 @@ an identifier: <code>aUb</code> is an atomic proposition, unlike
<tr> <tr>
<td align="right">not:</td><td><code>!</code></td> <td align="right">not:</td><td><code>!</code></td>
<td align="right">and:</td><td><code>&</code> <code>&&</code> <td align="right">and:</td><td><code>&</code> <code>&&</code>
<code>.</code> <code>*</code> <code>.</code> <code>/\</code></td>
<code>/\</code></td>
<td align="right">xor:</td><td><code>^</code> <code>xor</code></td> <td align="right">xor:</td><td><code>^</code> <code>xor</code></td>
<td align="right">true:</td><td><code>1</code> <td align="right">true:</td><td><code>1</code>
<code>true</code></td> <code>true</code></td>