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

Accept "{E}|->ltl" and "{E}(ltl)" as synonym for "{E}[]->ltl".

Browse source 
* src/ltlparse/ltlparse.yy (parenthesedsubformula): Extract these
rules from...
(subformula): ... here, and use it to recognize "{SERE}(formula)".
* src/ltlparse/ltlscan.ll: Recognize "|->" as "[]->".
* src/ltltest/equals.test: Test these two new syntaxes.
This commit is contained in:
Alexandre Duret-Lutz 2010-03-09 16:26:27 +01:00
parent 8b8633de8c
commit 1ecc6984d3
3 changed files with 18 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/ltlparse/ltlparse.yy
View file

@ -118,7 +118,8 @@ using namespace spot::ltl;
%nonassoc OP_POST_NEG OP_POST_POS
%type <ltl> subformula booleanatom rationalexp bracedrationalexp
%type <ltl> subformula booleanatom rationalexp
%type <ltl> bracedrationalexp parenthesedsubformula
%destructor { delete $$; } <str>
%destructor { $$->destroy(); } <ltl>
@ -232,10 +233,9 @@ booleanatom: ATOMIC_PROP
{ $$ = constant::false_instance(); }
rationalexp: booleanatom
| bracedrationalexp
| CONST_EMPTYWORD
{ $$ = constant::empty_word_instance(); }
| bracedrationalexp
{ $$ = $1; }
| PAR_OPEN rationalexp PAR_CLOSE
{ $$ = $2; }
| PAR_OPEN error PAR_CLOSE
@ -292,8 +292,7 @@ bracedrationalexp: BRACE_OPEN rationalexp BRACE_CLOSE
$$ = constant::false_instance();
}
subformula: booleanatom
| PAR_OPEN subformula PAR_CLOSE
parenthesedsubformula: PAR_OPEN subformula PAR_CLOSE
{ $$ = $2; }
| PAR_OPEN error PAR_CLOSE
{ error_list.push_back(parse_error(@$,
@ -311,6 +310,10 @@ subformula: booleanatom
"treating this parenthetical block as false"));
$$ = constant::false_instance();
}
subformula: booleanatom
| parenthesedsubformula
| subformula OP_AND subformula
{ $$ = multop::instance(multop::And, $1, $3); }
| subformula OP_AND error
@ -367,6 +370,8 @@ subformula: booleanatom
{ $$ = unop::instance(unop::Closure, $1); }
| bracedrationalexp OP_UCONCAT subformula
{ $$ = binop::instance(binop::UConcat, $1, $3); }
| bracedrationalexp parenthesedsubformula
{ $$ = binop::instance(binop::UConcat, $1, $2); }
| bracedrationalexp OP_UCONCAT error
{ missing_right_binop($$, $1, @2, "universal concat operator"); }
| bracedrationalexp OP_ECONCAT subformula

6
src/ltlparse/ltlscan.ll
View file

@ -85,7 +85,13 @@ flex_set_buffer(const char* buf, int start_tok)
/* ~ comes from Goal, ! from everybody else */
"!"|"~" BEGIN(0); return token::OP_NOT;
/* PSL operators */
"[*0]" BEGIN(0); return token::CONST_EMPTYWORD;
"[]->"|"|->" BEGIN(0); return token::OP_UCONCAT;
"<>->" BEGIN(0); return token::OP_ECONCAT;
"*"|"[*]" BEGIN(0); return token::OP_STAR;
";" BEGIN(0); return token::OP_CONCAT;
":" BEGIN(0); return token::OP_FUSION;
/* & and | come from Spin. && and || from LTL2BA.
/\, \/, and xor are from LBTT.

2
src/ltltest/equals.test
View file

@ -120,3 +120,5 @@ run 0 ../equals '{x;x}<>->FF(0)' '0'
run 0 ../equals '{x;x}<>->GX(1)' '{x;x}<>->1'
run 0 ../equals '{x;x}[]->GX(1)' '1'
run 0 ../equals '{x;x}[]->FF(0)' '{x;x}[]->0'
run 0 ../equals '{x;x}[]->y' '{x;x}|->y'
run 0 ../equals '{x;x}[]->y' '{x;x}(y)'