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

Add support for the {SERE}! PSL operator.

Browse source 
* src/ltlparse/ltlscan.ll: Recognize }!.  Also remove
five duplicate rules.
* src/ltlparse/ltlparse.yy: Build {r}<>->1 when parsing {r}!.
* src/ltlvisit/tostring.cc: Print {r}! instead of {r}<>->1.
* src/ltltest/tostring.test, src/ltltest/equals.test:
Add more tests.
This commit is contained in:
Alexandre Duret-Lutz 2011-02-17 18:47:21 +01:00
parent c48b9bcfb5
commit fdd73d5123
5 changed files with 27 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ltlparse/ltlscan.ll
View file

@ -76,6 +76,7 @@ flex_set_buffer(const char* buf, int start_tok)
"(" BEGIN(0); return token::PAR_OPEN;
")" BEGIN(not_prop); return token::PAR_CLOSE;
"{" BEGIN(0); return token::BRACE_OPEN;
"}"[ \t\n]*"!" BEGIN(not_prop); return token::BRACE_BANG_CLOSE;
"}" BEGIN(not_prop); return token::BRACE_CLOSE;
/* Must go before the other operators, because the F of FALSE
@ -135,11 +136,6 @@ flex_set_buffer(const char* buf, int start_tok)
"^"|"xor" BEGIN(0); return token::OP_XOR;
"=>"|"->"|"-->" BEGIN(0); return token::OP_IMPLIES;
"<=>"|"<->"|"<-->" BEGIN(0); return token::OP_EQUIV;
"*"|"[*]" BEGIN(0); return token::OP_STAR;
";" BEGIN(0); return token::OP_CONCAT;
":" BEGIN(0); return token::OP_FUSION;
"[]->" BEGIN(0); return token::OP_UCONCAT;
"<>->" BEGIN(0); return token::OP_ECONCAT;
/* <>, [], and () are used in Spin. */
"F"|"<>" BEGIN(0); return token::OP_F;