diff --git a/ChangeLog b/ChangeLog index 304186574..2ce235a6d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2011-02-03 Alexandre Duret-Lutz + + Recognize Goal's syntax for Boolean operators. + + * src/ltlparse/ltlscan.ll: Recognize ~, -->, and <--> operators + from Goal, to ease the use of formulas provided by the Goal team. + * src/ltltest/equals.test: Use these once, just to be on the + safe side. + 2011-02-03 Alexandre Duret-Lutz Minor fixes to ltl2tgba.html. diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll index 3f6efc5b7..215a054bb 100644 --- a/src/ltlparse/ltlscan.ll +++ b/src/ltlparse/ltlscan.ll @@ -1,4 +1,4 @@ -/* Copyright (C) 2010, Laboratoire de Recherche et Développement de +/* Copyright (C) 2010, 2011, 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 @@ -72,17 +72,17 @@ flex_set_buffer(const char* buf) "0"|[fF][aA][lL][sS][eE] BEGIN(0); return token::CONST_FALSE; - -"!" BEGIN(0); return token::OP_NOT; + /* ~ comes from Goal, ! from everybody else */ +"!"|"~" BEGIN(0); return token::OP_NOT; /* & and | come from Spin. && and || from LTL2BA. /\, \/, and xor are from LBTT. - */ + --> and <--> come from Goal. */ "||"|"|"|"+"|"\\/" BEGIN(0); return token::OP_OR; "&&"|"&"|"."|"/\\" 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; +"=>"|"->"|"-->" BEGIN(0); return token::OP_IMPLIES; +"<=>"|"<->"|"<-->" BEGIN(0); return token::OP_EQUIV; /* <>, [], and () are used in Spin. */ "F"|"<>" BEGIN(0); return token::OP_F; diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test index b849d140b..8647b4b86 100755 --- a/src/ltltest/equals.test +++ b/src/ltltest/equals.test @@ -1,5 +1,5 @@ #! /bin/sh -# Copyright (C) 2009 Laboratoire de Recherche et Développement +# Copyright (C) 2009, 2011 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 @@ -29,9 +29,11 @@ # A few things which are equal run 0 ../equals 'a' 'a' +run 0 ../equals '~a' '!a' run 0 ../equals '1' '1' run 0 ../equals '0' '0' -run 0 ../equals 'a => b' 'a => b' +run 0 ../equals 'a => b' 'a --> b' +run 0 ../equals 'a <-> b' 'a <--> b' run 0 ../equals 'G a ' ' G a' run 0 ../equals 'a U b' 'a U b' run 0 ../equals 'a & b' 'a & b'