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

formula: b* is siSERE

Browse source 
Since b[+] and [*0] are siSERE, b* is siSERE as well.
Suggested by Victor Khomenko.

* spot/tl/formula.cc: Implement that for Star and also
in the concatenation rule.
* tests/core/kind.test, tests/core/ltlfilt.test: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2019-04-26 22:14:19 +02:00
parent d66eb84643
commit 9e7e6d50fb
3 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

7
spot/tl/formula.cc
View file

@ -1549,7 +1549,8 @@ namespace spot
// concatenation, it means all arguments should be of the
// form b*, except one that is siSERE (i.e., a sub-formula
// that verify is_syntactic_stutter_invariant() and
// !is_boolean());
// !is_boolean()). Since b* is siSERE, that means we
// want at least s-1 operands of the form b*.
if (op_ == op::Concat)
{
unsigned sb = 0; // stared Boolean formulas seen
@ -1567,7 +1568,7 @@ namespace spot
break;
}
}
is_.syntactic_si = sb == s - 1;
is_.syntactic_si = sb >= s - 1;
}
break;
}
@ -1594,7 +1595,7 @@ namespace spot
if (max_ == unbounded())
{
is_.finite = false;
is_.syntactic_si = min_ == 1 && children[0]->is_boolean();
is_.syntactic_si = min_ <= 1 && children[0]->is_boolean();
}
else
{