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

simplify: reduce {r;1} to {r} or {1}

Browse source 
Fixes #3.

* spot/tl/simplify.cc: Implement this new rule.
* doc/tl/tl.tex, NEWS: Document it.
* tests/core/reduccmp.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2018-03-15 07:59:25 +01:00
parent 2d18ac22fb
commit cfcc18e680
4 changed files with 29 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -18,6 +18,10 @@ New in spot 2.5.1.dev (not yet released)
update an external structure that references states of the twa
that we want to purge.
- the PSL simplification routines learned that {SERE;1} can be
simplified to {1} or {SERE} depending on whether SERE accepts
the empty word or not.
Bugs fixed:
- acc_cond::is_generalized_rabin() and

4
doc/tl/tl.tex
View file

@ -1636,6 +1636,10 @@ Here are the basic rewritings for the weak closure and its negation:
\begin{align*}
\sere{r\STAR{}}&\equiv \sere{r}&
\nsere{r\STAR{}}&\equiv \nsere{r}\\
\sere{r;\1}&\equiv \sere{r} \quad\text{if~}\varepsilon\not\VDash r&
\nsere{r;\1}&\equiv \nsere{r} \quad\text{if~}\varepsilon\not\VDash r\\
\sere{r;\1}&\equiv \1 \quad\text{if~}\varepsilon\VDash r&
\nsere{r;\1}&\equiv \0 \quad\text{if~}\varepsilon\VDash r\\
\sere{r_1;r_2}&\equiv \sere{r_1}\phantom{{}\OR\sere{r_2}}\quad\text{if~}\varepsilon\not\VDash r_1\land\varepsilon\VDash r_2&
\nsere{r_1;r_2}&\equiv \nsere{r_1}\phantom{{}\AND\nsere{r_2}}\quad\text{if~}\varepsilon\not\VDash r_1\land\varepsilon\VDash r_2\\
\sere{r_1;r_2}&\equiv \sere{r_1}\OR\sere{r_2}\quad\text{if~}\varepsilon\VDash r_1\land\varepsilon\VDash r_2&

14
spot/tl/simplify.cc
View file

@ -1268,12 +1268,26 @@ namespace spot
// Some term does not accept the empty word.
unsigned end = c.size() - 1;
// {r;1} = 1 if r accepts [*0], else {r}
// !{r;1} = 0 if r accepts [*0], else !{r}
if (c[end].is_tt())
{
formula rest = c.all_but(end);
if (rest.accepts_eword())
return o == op::Closure ? formula::tt() : formula::ff();
return recurse(formula::unop(o, rest));
}
// {b₁;b₂;e₁;f₁;e₂;f₂;e₂;e₃;e₄}
// = b₁&X(b₂&X({e₁;f₁;e₂;f₂}))
// !{b₁;b₂;e₁;f₁;e₂;f₂;e₂;e₃;e₄}
// = !b₁|X(!b₂|X(!{e₁;f₁;e₂;f₂}))
// if e denotes a term that accepts [*0]
// and b denotes a Boolean formula.
//
// if reduce_size_strictly is set, we simply remove
// the trailing e2;e3;e4.
while (c[end].accepts_eword())
--end;
unsigned start = 0;

8
tests/core/reduccmp.test
View file

@ -1,6 +1,6 @@
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2009-2014, 2016-2017 Laboratoire de Recherche et
# Copyright (C) 2009-2014, 2016-2018 Laboratoire de Recherche et
# Developpement de l'Epita (LRDE).
# Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -388,6 +388,12 @@ G(GFc|GFd|FGe|FGf), F(GF(c|d)|Ge|Gf)
{a|b*|c|d*}[]->e, (e | !(a | c)) & (e W !b) & (e W !d)
{{[*0]|a};b;{[*0]|a};c;e[*]}[]->f,{{[*0]|a};b;{[*0]|a}}[]->X((f&X(f W !e))|!c)
{(a[*]|b)[*0..1];c}, {{b | a[*]};c}
{{a|b*};1}, 1
!{{a|b*};1}, 0
{{a|b[+]};1}, a|b
!{{a|b[+]};1}, !a&!b
{{{a|b[+]}&c[*]};1}, {{a|b[+]}&c[*]}
!{{{a|b[+]}&c[*]};1}, !{{a|b[+]}&c[*]}
{a&b&c*}<>->!Xb, (a & b & X!b) | (a & b & c & X(c U !b))
{[*]}<>->b, Fb