diff --git a/ChangeLog b/ChangeLog index 0238f1003..492926d8d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2010-01-30 Alexandre Duret-Lutz + + 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 Make Couvreur/FM the default translation. diff --git a/NEWS b/NEWS index 4c222bc93..b84a17598 100644 --- a/NEWS +++ b/NEWS @@ -39,6 +39,9 @@ New in spot 0.5 (2010-01-31): function. This is ltl2tgba's -R3b option. * The SCC-based simplification (ltl2tgba's -R3 option) has been 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: - gspn-ssp/ some benchmarks published at ACSD'07, - ltlcounter/ translation of a class of LTL formulae used by diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll index ed6d0a4c1..faef3ae76 100644 --- a/src/ltlparse/ltlscan.ll +++ b/src/ltlparse/ltlscan.ll @@ -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 ** et Marie Curie. ** @@ -77,7 +79,7 @@ flex_set_buffer(const char* buf) /\, \/, and xor are from LBTT. */ "||"|"|"|"+"|"\\/" 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; "=>"|"->" BEGIN(0); return token::OP_IMPLIES; "<=>"|"<->" BEGIN(0); return token::OP_EQUIV; diff --git a/src/tgbatest/kv.test b/src/tgbatest/kv.test index 57f3874b6..45dab503a 100755 --- a/src/tgbatest/kv.test +++ b/src/tgbatest/kv.test @@ -1,5 +1,5 @@ #!/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. # @@ -35,7 +35,7 @@ check () check 'a R (b R c)' 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. check '"G1"U"GG" && "FF"' diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index 675064886..fa2341bfb 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -1,5 +1,5 @@ #!/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). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # 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 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))' diff --git a/src/tgbatest/reductgba.test b/src/tgbatest/reductgba.test index 5f787d653..ecde3d817 100755 --- a/src/tgbatest/reductgba.test +++ b/src/tgbatest/reductgba.test @@ -1,5 +1,5 @@ #!/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). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # 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 'a R (b R c)' 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 1 a @@ -62,7 +62,7 @@ check 1 'Fa & Xa & GFc & Gc' check 1 'Fc & X(a | Xb) & GF(a | Xb) & Gc' check 1 'a R (b R c)' 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 U b' @@ -75,7 +75,7 @@ check 2 'Fa & Xa & GFc & Gc' check 2 'Fc & X(a | Xb) & GF(a | Xb) & Gc' check 2 'a R (b R c)' 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 U b' @@ -89,4 +89,4 @@ check 3 'Fa & Xa & GFc & Gc' check 3 'Fc & X(a | Xb) & GF(a | Xb) & Gc' check 3 'a R (b R c)' 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))' diff --git a/wrap/python/cgi-bin/ltl2tgba.in b/wrap/python/cgi-bin/ltl2tgba.in index 1f073ca04..4575e8893 100755 --- a/wrap/python/cgi-bin/ltl2tgba.in +++ b/wrap/python/cgi-bin/ltl2tgba.in @@ -1,8 +1,8 @@ #!@PYTHON@ # -*- 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). -# 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), # Université Pierre et Marie Curie. # @@ -294,8 +294,7 @@ an identifier: aUb is an atomic proposition, unlike not:! and:& && - . * - /\ + . /\ xor:^ xor true:1 true