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

Trivially reduce 'a[*1]' to 'a'.

Browse source 
* src/ltlast/bunop.cc (bunop::instance): Here.
* src/ltlast/bunop.hh, doc/tl/tl.tex: Document it.
* src/ltltest/equals.test: Test it.
This commit is contained in:
Alexandre Duret-Lutz 2012-04-17 16:00:22 +02:00
parent abaf102746
commit a4353d3985
4 changed files with 13 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

5
doc/tl/tl.tex
View file

@ -651,7 +651,7 @@ it for output. $b$ must be a Boolean formula.
b\EQUAL{\mvar{i}..\mvar{j}} &\equiv \mathtt{\{\{}\NOT b\mathtt{\}}\STAR{0..}\CONCAT b\mathtt{\}}\STAR{\mvar{i}..\mvar{j}}\CONCAT \mathtt{\{}\NOT b\mathtt{\}}\STAR{0..} \\ b\EQUAL{\mvar{i}..\mvar{j}} &\equiv \mathtt{\{\{}\NOT b\mathtt{\}}\STAR{0..}\CONCAT b\mathtt{\}}\STAR{\mvar{i}..\mvar{j}}\CONCAT \mathtt{\{}\NOT b\mathtt{\}}\STAR{0..} \\
b\GOTO{\mvar{i}..} &\equiv \mathtt{\{\{}\NOT b\mathtt{\}}\STAR{0..}\CONCAT b\mathtt{\}}\STAR{\mvar{i}..} & b\GOTO{\mvar{i}..} &\equiv \mathtt{\{\{}\NOT b\mathtt{\}}\STAR{0..}\CONCAT b\mathtt{\}}\STAR{\mvar{i}..} &
b\EQUAL{\mvar{i}..} &\equiv \mathtt{\{\{}\NOT b\mathtt{\}}\STAR{0..}\CONCAT b\mathtt{\}}\STAR{\mvar{i}..}\CONCAT \mathtt{\{}\NOT b\mathtt{\}}\STAR{0..}\text{~if~}i>0 \\ b\EQUAL{\mvar{i}..} &\equiv \mathtt{\{\{}\NOT b\mathtt{\}}\STAR{0..}\CONCAT b\mathtt{\}}\STAR{\mvar{i}..}\CONCAT \mathtt{\{}\NOT b\mathtt{\}}\STAR{0..}\text{~if~}i>0 \\
&& b\EQUAL{0..} &\equiv \mathtt{\{\{}\1\STAR{0..}\mathtt{\}} && b\EQUAL{0..} &\equiv \1\STAR{0..}
\end{align*} \end{align*}
\begin{align*} \begin{align*}
f\STARALT &\equiv f\STAR{0..}\\ f\STARALT &\equiv f\STAR{0..}\\
@ -687,7 +687,8 @@ $b_1$, $b_2$ are assumed to be Boolean formul\ae.
\0\STAR{\mvar{i}..\mvar{j}} &\equiv \0 \text{~if~}i>0 \\ \0\STAR{\mvar{i}..\mvar{j}} &\equiv \0 \text{~if~}i>0 \\
\eword\STAR{\var{i}..\mvar{j}} &\equiv \eword& \eword\STAR{\var{i}..\mvar{j}} &\equiv \eword&
f\STAR{\mvar{i}..\mvar{j}}\STAR{\mvar{k}..\mvar{l}} &\equiv f\STAR{\mvar{ik}..\mvar{jl}}\text{~if~}i(k+1)\le jk+1 \\ f\STAR{\mvar{i}..\mvar{j}}\STAR{\mvar{k}..\mvar{l}} &\equiv f\STAR{\mvar{ik}..\mvar{jl}}\text{~if~}i(k+1)\le jk+1 \\
f\STAR{0}&\equiv \eword f\STAR{0}&\equiv \eword \\
f\STAR{1}&\equiv f\\
\end{align*} \end{align*}
\noindent \noindent

4
src/ltlast/bunop.cc
View file

@ -211,6 +211,10 @@ namespace spot
return constant::empty_word_instance(); return constant::empty_word_instance();
} }
// - Exp[*1] = Exp
if (min == 1 && max == 1)
return child;
// - Exp[*i..j][*min..max] = Exp[*i(min)..j(max)] // - Exp[*i..j][*min..max] = Exp[*i(min)..j(max)]
// if i*(min+1)<=j(min)+1. // if i*(min+1)<=j(min)+1.
if (child->kind() == BUnOp) if (child->kind() == BUnOp)

1
src/ltlast/bunop.hh
View file

@ -51,6 +51,7 @@ namespace spot
/// - [*0][*min..max] = [*0] /// - [*0][*min..max] = [*0]
/// - Exp[*0] = [*0] /// - Exp[*0] = [*0]
/// - Exp[*i..j][*k..l] = Exp[*ik..jl] if i*(k+1)<=jk+1. /// - Exp[*i..j][*k..l] = Exp[*ik..jl] if i*(k+1)<=jk+1.
/// - Exp[*1] = Exp
/// ///
/// These rewriting rules imply that it is not possible to build /// These rewriting rules imply that it is not possible to build
/// an LTL formula object that is SYNTACTICALLY equal to one of /// an LTL formula object that is SYNTACTICALLY equal to one of

8
src/ltltest/equals.test
View file

@ -1,8 +1,9 @@
#! /bin/sh #! /bin/sh
# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement # -*- coding: utf-8 -*-
# de l'Epita (LRDE). # Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre # département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie. # et Marie Curie.
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -160,6 +161,7 @@ run 0 ../equals '{a[*..3][*to2]}' '{a[*:6]}'
run 0 ../equals '{a[*..3][*2..$]}' '{a[*]}' run 0 ../equals '{a[*..3][*2..$]}' '{a[*]}'
run 0 ../equals '{a[*..3][*2:]}' '{a[*:inf]}' run 0 ../equals '{a[*..3][*2:]}' '{a[*:inf]}'
run 0 ../equals '{a[*1..]}' '{a[+]}' run 0 ../equals '{a[*1..]}' '{a[+]}'
run 0 ../equals '{a[*1]}' '{a}'
run 0 ../equals '{a[+][*1..3]}' '{a[+]}' run 0 ../equals '{a[+][*1..3]}' '{a[+]}'
run 0 ../equals '{a[*1..3][+]}' '{a[+]}' run 0 ../equals '{a[*1..3][+]}' '{a[+]}'
run 0 ../equals '{[*2][+]}' '{[*2][+]}' run 0 ../equals '{[*2][+]}' '{[*2][+]}'