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

Support non-overlapping concatenations operators []=> and <>=>.

Browse source 
* src/ltlparse/ltlscan.ll: Recognize "[]=>" (a.k.a "|=>") and "<>=>".
* src/ltlparse/ltlparse.yy: Support them by rewriting them using
"[]->" and "<>->".
* src/tgbatest/ltl2tgba.test: More tests.
This commit is contained in:
Alexandre Duret-Lutz 2010-03-10 15:47:04 +01:00
parent 4aa82ec762
commit 4bde130d38
3 changed files with 32 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/ltlparse/ltlparse.yy
View file

@ -87,6 +87,8 @@ using namespace spot::ltl;
%token OP_X "next operator" OP_NOT "not operator" OP_STAR "star operator"
%token OP_UCONCAT "universal concat operator"
%token OP_ECONCAT "existential concat operator"
%token OP_UCONCAT_NONO "universal non-overlapping concat operator"
%token OP_ECONCAT_NONO "existential non-overlapping concat operator"
%token <str> ATOMIC_PROP "atomic proposition"
%token OP_CONCAT "concat operator" OP_FUSION "fusion operator"
%token CONST_TRUE "constant true" CONST_FALSE "constant false"
@ -96,7 +98,7 @@ using namespace spot::ltl;
/* Priorities. */
/* Low priority regex operator. */
%left OP_UCONCAT OP_ECONCAT
%left OP_UCONCAT OP_ECONCAT OP_UCONCAT_NONO OP_ECONCAT_NONO
%left OP_CONCAT OP_FUSION
@ -386,12 +388,34 @@ subformula: booleanatom
| bracedrationalexp parenthesedsubformula
{ $$ = binop::instance(binop::UConcat, $1, $2); }
| bracedrationalexp OP_UCONCAT error
{ missing_right_binop($$, $1, @2, "universal concat operator"); }
{ missing_right_binop($$, $1, @2,
"universal overlapping concat operator"); }
| bracedrationalexp OP_ECONCAT subformula
{ $$ = binop::instance(binop::EConcat, $1, $3); }
| bracedrationalexp OP_ECONCAT error
{ missing_right_binop($$, $1, @2, "universal concat operator"); }
{ missing_right_binop($$, $1, @2,
"existential overlapping concat operator");
}
| bracedrationalexp OP_UCONCAT_NONO subformula
/* {SERE}[]=>EXP = {SERE;1}[]->EXP */
{ $$ = binop::instance(binop::UConcat,
multop::instance(multop::Concat, $1,
constant::true_instance()), $3);
}
| bracedrationalexp OP_UCONCAT_NONO error
{ missing_right_binop($$, $1, @2,
"universal non-overlapping concat operator");
}
| bracedrationalexp OP_ECONCAT_NONO subformula
/* {SERE}<>=>EXP = {SERE;1}<>->EXP */
{ $$ = binop::instance(binop::EConcat,
multop::instance(multop::Concat, $1,
constant::true_instance()), $3);
}
| bracedrationalexp OP_ECONCAT_NONO error
{ missing_right_binop($$, $1, @2,
"existential non-overlapping concat operator");
}
;
%%

2
src/ltlparse/ltlscan.ll
View file

@ -89,6 +89,8 @@ flex_set_buffer(const char* buf, int start_tok)
"[*0]" BEGIN(0); return token::CONST_EMPTYWORD;
"[]->"|"|->" BEGIN(0); return token::OP_UCONCAT;
"<>->" BEGIN(0); return token::OP_ECONCAT;
"[]=>"|"|=>" BEGIN(0); return token::OP_UCONCAT_NONO;
"<>=>" BEGIN(0); return token::OP_ECONCAT_NONO;
"*"|"[*]" BEGIN(0); return token::OP_STAR;
";" BEGIN(0); return token::OP_CONCAT;
":" BEGIN(0); return token::OP_FUSION;

3
src/tgbatest/ltl2tgba.test
View file

@ -76,13 +76,14 @@ check_psl '{a;b}'
check_psl '{(a;b)*}'
check_psl 'G{(a;b)*}'
check_psl '{a*}[]->{b*}'
check_psl '{a*}[]=>{b*}'
check_psl '{a*&b}'
check_psl '{a*&b*}'
check_psl '{((!c;b*) & d);e}'
check_psl '{(a* & (c;b*) & d);e}'
# Example from "Beyond Hardware Verification" by Glazberg, Moulin, Orni,
# Ruah, Zarpas (2007).
check_psl '{1[*];req;ack;1}[]->{start;busy[*];done}'
check_psl '{1[*];req;ack}|=>{start;busy[*];done}'
# Make sure 'a U (b U c)' has 3 states and 6 transitions,
# before and after degeneralization.