ltl: fix detection of some siPSL formulas
* src/ltlast/bunop.cc: Fix detection of f[:*2] as siPSL if f is siPSL * src/tests/kind.test: Test it. * NEWS: Mention it.
This commit is contained in:
parent
9ae2af209b
commit
5d9e7d1f93
3 changed files with 9 additions and 9 deletions
3
NEWS
3
NEWS
|
|
@ -1,6 +1,7 @@
|
|||
New in spot 1.99.1a (not yet released)
|
||||
|
||||
Nothing yet.
|
||||
* Bugs fixed:
|
||||
- p[+][:*2] was not detected as belonging to siPSL
|
||||
|
||||
New in spot 1.99.1 (2015-06-23)
|
||||
|
||||
|
|
|
|||
|
|
@ -69,15 +69,11 @@ namespace spot
|
|||
break;
|
||||
case FStar:
|
||||
is.accepting_eword = false;
|
||||
if (max_ == unbounded)
|
||||
{
|
||||
is.finite = false;
|
||||
is.syntactic_si &= !child->is_boolean();
|
||||
}
|
||||
else
|
||||
{
|
||||
if (max_ == unbounded)
|
||||
is.finite = false;
|
||||
if (min_ == 0)
|
||||
is.syntactic_si = false;
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -130,6 +130,9 @@ Fa M b,&!xLPgopra
|
|||
{a[+];b*;c[+]},&!xfPsopra
|
||||
{a[+] && b || c[+]},&!fPsopra
|
||||
{a[+] && b[+] || c[+]},&!xfPsopra
|
||||
{p[+]:p[+]},&!xfPsoprla
|
||||
(!p W Gp) | ({(!p[*];(p[+]:(p[*];!p[+])))[:*4][:+]}<>-> (!p W Gp)),&!xPpla
|
||||
{b[+][:*0..3]},&!fPsopra
|
||||
EOF
|
||||
|
||||
run 0 ../kind input
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue