Commit 77d704ea authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Add trivial identity {b}=b and !{b}=!b for any Boolean formula b.

* src/ltlast/unop.cc: Perform the simplification.
* src/ltlast/unop.hh, doc/tl/tl.tex: Document it.
* src/ltltest/equals.test: Adjust test cases.
parent 98f67973
......@@ -794,17 +794,17 @@ while $f$ is a PSL formula.
\begin{align*}
\sigma\vDash \ratgroup{r}\Esuffix f &\iff \exists k\ge 0, (\sigma^{0..k}\VDash r)\land(\sigma^{k..}\vDash f)\\
\sigma\vDash \ratgroup{r}\Asuffix f &\iff \forall k\ge 0, (\sigma^{0..k}\VDash r)\limplies (\sigma^{k..}\vDash f)\\
\sigma\vDash \ratgroup{r} & \iff (\exists k\ge 0, \sigma^{0..k}\VDash r)\lor(\forall k\ge 0,\,\exists \pi\in(\B^\AP)^\star,\, (\sigma^{0..k}\prec \pi)\land(\pi\VDash r))\\
\sigma\vDash \nratgroup{r} & \iff (\forall k\ge 0, \sigma^{0..k}\nVDash r)\land(\exists k\ge 0,\,\exists \forall\in(\B^\AP)^\star,\, (\sigma^{0..k}\prec \pi)\limplies(\pi\nVDash r))\\
\sigma\vDash \ratgroup{r} & \iff (\exists k\ge 0, \sigma^{0..k}\VDash r)\lor(\forall k\ge 0,\,\exists\pi\in(\B^\AP)^\star,\, (\sigma^{0..k}\prec \pi)\land(\pi\VDash r))\\
\sigma\vDash \nratgroup{r} & \iff (\forall k\ge 0, \sigma^{0..k}\nVDash r)\land(\exists k\ge 0,\,\forall\pi\in(\B^\AP)^\star,\, (\sigma^{0..k}\prec \pi)\limplies(\pi\nVDash r))\\
\end{align*}
The $\prec$ symbol should be read as ``\emph{is a prefix of}''. So
the semantic for `$\sigma\vDash \ratgroup{r}$' is that either there is
a finite prefix of $\sigma$ that is a model of $r$, or any prefix of
$\sigma$ can be extended into a finite sequence $\pi$ that is a model
of $r$. An infinite sequence $\texttt{a;a;a;a;a;}\ldots$ is therefore a
model of the formula \samp{$\ratgroup{a\PLUS{};\NOT a}$} even though
it never sees \samp{$\NOT a$}.
a (non-empty) finite prefix of $\sigma$ that is a model of $r$, or any
prefix of $\sigma$ can be extended into a finite sequence $\pi$ that
is a model of $r$. An infinite sequence $\texttt{a;a;a;a;a;}\ldots$
is therefore a model of the formula \samp{$\ratgroup{a\PLUS{};\NOT
a}$} even though it never sees \samp{$\NOT a$}.
\subsection{Syntactic Sugar}
......@@ -842,10 +842,12 @@ formula $b$, the following rewritings are systematically performed
& \ratgroup{\eword}\Esuffix f&\equiv \0
& \ratgroup{\eword} & \equiv \0
& \nratgroup{\eword} & \equiv \1 \\
\ratgroup{b}\Asuffix f&\equiv b\IMPLIES f
& \ratgroup{b}\Esuffix f&\equiv b\AND f
& \ratgroup{b} &\equiv b
& \nratgroup{b} &\equiv \NOT b\\
\ratgroup{r}\Asuffix \1&\equiv \1
& \ratgroup{r}\Esuffix \0&\equiv \0 \\
\ratgroup{b}\Asuffix f&\equiv b\IMPLIES f
& \ratgroup{b}\Esuffix f&\equiv b\AND f \\
\end{align*}
\chapter{Grammar}
......
......@@ -295,19 +295,25 @@ namespace spot
break;
case Closure:
if (child == constant::true_instance()
|| child == constant::empty_word_instance())
return constant::true_instance();
if (child == constant::false_instance())
// {0} = 0, {1} = 1, {b} = b
if (child->is_boolean())
return child;
// {[*0]} = 1
if (child == constant::empty_word_instance())
return constant::true_instance();
break;
case NegClosure:
// {1} = 0, {[*0]} = 0
if (child == constant::true_instance()
|| child == constant::empty_word_instance())
return constant::false_instance();
// {0} = 1
if (child == constant::false_instance())
return constant::true_instance();
// {b} = !b
if (child->is_boolean())
return unop::instance(Not, child);
break;
}
......
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
......@@ -73,9 +73,11 @@ namespace spot
/// - Closure([*0]) = 1
/// - Closure(1) = 1
/// - Closure(0) = 0
/// - Closure(b) = b
/// - NegClosure([*0]) = 0
/// - NegClosure(1) = 0
/// - NegClosure(0) = 1
/// - NegClosure(b) = !b
///
/// This rewriting implies that it is not possible to build an
/// LTL formula object that is SYNTACTICALLY equal to one of
......
......@@ -179,9 +179,9 @@ run 0 ../equals '{b[=0to$]}' '{*}'
run 0 ../equals '{0[->10..100];b}' '0'
run 0 ../equals '{0[->1..];b}' '0'
run 0 ../equals '{0[->0,100];b}' '{b}'
run 0 ../equals '{0[->0..$];b}' '{b}'
run 0 ../equals '{1[->0];b}' '{b}'
run 0 ../equals '{0[->0,100];b}' 'b'
run 0 ../equals '{0[->0..$];b}' 'b'
run 0 ../equals '!{1[->0];b}' '!b'
run 0 ../equals '{1[->10,20];b}' '{[*10..20];b}'
run 0 ../equals '{1[->..];b}' '{[*1..];b}'
run 0 ../equals '{{a&!c}[->0];b}' '{b}'
run 0 ../equals '{{a&!c}[->0];b}' 'b'
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment