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

tl: first_match does not preserve syntactic_si

Browse source 
* spot/tl/formula.cc: Fix it.
* tests/core/kind.test: Add test case.
This commit is contained in:
Alexandre Duret-Lutz 2019-05-06 21:52:05 +02:00
parent ef8de879dc
commit b7cd475632
2 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
spot/tl/formula.cc
View file

@ -1632,10 +1632,10 @@ namespace spot
break; break;
case op::first_match: case op::first_match:
props = children[0]->props; props = children[0]->props;
// If first_match(r) == r && !(r;[*]), then it should follow
// that if r is stutter-inv, then first_match(r) is
// stutter-inv, so we do not reset the syntactic_si bit.
assert(is_.sere_formula); assert(is_.sere_formula);
// {(a[+];b*);c*}<>->d is stutter invariant
// {first_match(a[+];b*);c*}<>->d is NOT.
is_.syntactic_si = false;
is_.boolean = false; is_.boolean = false;
is_.ltl_formula = false; is_.ltl_formula = false;
is_.psl_formula = false; is_.psl_formula = false;

2
tests/core/kind.test
View file

@ -136,6 +136,8 @@ Fa M b,&!xLPgopra
(!p W Gp) | ({(!p[*];(p[+]:(p[*];!p[+])))[:*4][:+]}<>-> (!p W Gp)),&!xPpla (!p W Gp) | ({(!p[*];(p[+]:(p[*];!p[+])))[:*4][:+]}<>-> (!p W Gp)),&!xPpla
{b[+][:*0..3]},&!fPsopra {b[+][:*0..3]},&!fPsopra
{a->c[*]},xfPsopra {a->c[*]},xfPsopra
{(a[+];b*);c*}<>->d,&!xfPgopra
{first_match(a[+];b*);c*}<>->d,&!fPgopra
EOF EOF
run 0 ../kind input run 0 ../kind input