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

ltlparse: Preliminary support for utf8 operators.

Browse source 
* src/ltlparse/ltlscan.ll: Recognize several utf8 operators
such as □, ◇, ◯, ↔, ⤇, etc.
This commit is contained in:
Alexandre Duret-Lutz 2012-03-14 18:56:33 +01:00
parent ce437cd499
commit 80a9c3e219
1 changed files with 30 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

49
src/ltlparse/ltlscan.ll
View file

@ -1,7 +1,7 @@
/* Copyright (C) 2010, 2011, Laboratoire de Recherche et Développement de /* Copyright (C) 2010, 2011, 2012, Laboratoire de Recherche et
** l'Epita (LRDE). ** Développement 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
** et Marie Curie. ** et Marie Curie.
** **
** This file is part of Spot, a model checking library. ** This file is part of Spot, a model checking library.
@ -21,7 +21,7 @@
** Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA ** Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
** 02111-1307, USA. ** 02111-1307, USA.
*/ */
%option noyywrap %option noyywrap warn 8bit batch
%option prefix="ltlyy" %option prefix="ltlyy"
%option outfile="lex.yy.c" %option outfile="lex.yy.c"
@ -61,6 +61,17 @@ flex_set_buffer(const char* buf, int start_tok)
%s not_prop %s not_prop
%x sqbracket %x sqbracket
BOX "[]"|"□"|"⬜"|"◻"
DIAMOND "<>"|"◇"|"⋄"|"♢"
ARROWL "->"|"-->"|"→"|"⟶"
DARROWL "=>"|"⇒"|"⟹"
ARROWLR "<->"|"<-->"|"↔"
DARROWLR "<=>"|"⇔"
CIRCLE "()"|"○"|"◯"
NOT "!"|"~"|"¬"
BOXARROW {BOX}{ARROWL}|"|"{ARROWL}|"↦"
BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇"
%% %%
%{ %{
@ -86,20 +97,20 @@ flex_set_buffer(const char* buf, int start_tok)
/* ~ comes from Goal, ! from everybody else */ /* ~ comes from Goal, ! from everybody else */
"!"|"~" BEGIN(0); return token::OP_NOT; {NOT} BEGIN(0); return token::OP_NOT;
/* PSL operators */ /* PSL operators */
"[]->"|"|->" BEGIN(0); return token::OP_UCONCAT; {BOXARROW} BEGIN(0); return token::OP_UCONCAT;
"<>->" BEGIN(0); return token::OP_ECONCAT; {DIAMOND}{ARROWL} BEGIN(0); return token::OP_ECONCAT;
"[]=>"|"|=>" BEGIN(0); return token::OP_UCONCAT_NONO; {BOXDARROW} BEGIN(0); return token::OP_UCONCAT_NONO;
"<>=>" BEGIN(0); return token::OP_ECONCAT_NONO; {DIAMOND}{DARROWL} BEGIN(0); return token::OP_ECONCAT_NONO;
";" BEGIN(0); return token::OP_CONCAT; ";" BEGIN(0); return token::OP_CONCAT;
":" BEGIN(0); return token::OP_FUSION; ":" BEGIN(0); return token::OP_FUSION;
"*"|"[*]" BEGIN(0); return token::OP_STAR; "*"|"[*]" BEGIN(0); return token::OP_STAR;
"[+]" BEGIN(0); return token::OP_PLUS; "[+]" BEGIN(0); return token::OP_PLUS;
"[*" BEGIN(sqbracket); return token::OP_STAR_OPEN; "[*" BEGIN(sqbracket); return token::OP_STAR_OPEN;
"[=" BEGIN(sqbracket); return token::OP_EQUAL_OPEN; "[=" BEGIN(sqbracket); return token::OP_EQUAL_OPEN;
"[->" BEGIN(sqbracket); return token::OP_GOTO_OPEN; "["{ARROWL} BEGIN(sqbracket); return token::OP_GOTO_OPEN;
<sqbracket>"]" BEGIN(0); return token::OP_SQBKT_CLOSE; <sqbracket>"]" BEGIN(0); return token::OP_SQBKT_CLOSE;
<sqbracket>[0-9]+ { <sqbracket>[0-9]+ {
unsigned num = 0; unsigned num = 0;
@ -112,7 +123,7 @@ flex_set_buffer(const char* buf, int start_tok)
{ {
error_list.push_back( error_list.push_back(
spot::ltl::parse_error(*yylloc, spot::ltl::parse_error(*yylloc,
"value too large ignored")); "value too large ignored"));
// Skip this number and read next token // Skip this number and read next token
yylloc->step(); yylloc->step();
} }
@ -131,19 +142,19 @@ flex_set_buffer(const char* buf, int start_tok)
/* & and | come from Spin. && and || from LTL2BA. /* & and | come from Spin. && and || from LTL2BA.
/\, \/, and xor are from LBTT. /\, \/, and xor are from LBTT.
--> and <--> come from Goal. */ --> and <--> come from Goal. */
"||"|"|"|"+"|"\\/" BEGIN(0); return token::OP_OR; "||"|"|"|"+"|"\\/"|"∨"|"∪" BEGIN(0); return token::OP_OR;
"&&"|"/\\" BEGIN(0); return token::OP_AND; "&&"|"/\\"|"∧"|"∩" BEGIN(0); return token::OP_AND;
"&" BEGIN(0); return token::OP_SHORT_AND; "&" BEGIN(0); return token::OP_SHORT_AND;
"^"|"xor" BEGIN(0); return token::OP_XOR; "^"|"xor"|"⊕" BEGIN(0); return token::OP_XOR;
"=>"|"->"|"-->" BEGIN(0); return token::OP_IMPLIES; {ARROWL}|{DARROWL} BEGIN(0); return token::OP_IMPLIES;
"<=>"|"<->"|"<-->" BEGIN(0); return token::OP_EQUIV; {ARROWLR}|{DARROWLR} BEGIN(0); return token::OP_EQUIV;
/* <>, [], and () are used in Spin. */ /* <>, [], and () are used in Spin. */
"F"|"<>" BEGIN(0); return token::OP_F; "F"|{DIAMOND} BEGIN(0); return token::OP_F;
"G"|"[]" BEGIN(0); return token::OP_G; "G"|{BOX} BEGIN(0); return token::OP_G;
"U" BEGIN(0); return token::OP_U; "U" BEGIN(0); return token::OP_U;
"R"|"V" BEGIN(0); return token::OP_R; "R"|"V" BEGIN(0); return token::OP_R;
"X"|"()" BEGIN(0); return token::OP_X; "X"|{CIRCLE} BEGIN(0); return token::OP_X;
"W" BEGIN(0); return token::OP_W; "W" BEGIN(0); return token::OP_W;
"M" BEGIN(0); return token::OP_M; "M" BEGIN(0); return token::OP_M;