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

Rewrite Exp[=0..] as [*].

Browse source 
* src/ltlast/bunop.cc: Implement this rewriting.
* src/ltlast/bunop.hh: Document it.
* src/ltltest/equals.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2010-10-14 19:14:42 +02:00
parent 8d4a413a37
commit 2c31e541b5
3 changed files with 12 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/ltlast/bunop.cc
View file

@ -167,13 +167,22 @@ namespace spot
{
case Equal:
{
// - Exp[=0..] = [*]
if (min == 0 && max == unbounded)
{
op = Star;
child->destroy();
child = constant::true_instance();
break;
}
// - 0[=0..max] = [*]
// - 0[=min..max] = 0 if min > 0
if (child == constant::false_instance())
{
if (min == 0)
{
max = -1U;
max = unbounded;
op = Star;
child = constant::true_instance();
break;

1
src/ltlast/bunop.hh
View file

@ -55,6 +55,7 @@ namespace spot
/// - 0[=min..max] = 0 if min > 0
/// - 1[=0] = [*0]
/// - 1[=min..max] = 1[*min..max] if max > 0
/// - Exp[=0..] = [*]
/// - Exp[=0] = (!Exp)[*]
///
/// These rewriting rules imply that it is not possible to build