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

Get rid of bunop::Equal and bunop::Goto.

Browse source 
* src/ltlast/bunop.hh, src/ltlast/bunop.cc, src/ltlvisit/randomltl.cc,
src/ltlvisit/simplify.cc, src/ltlvisit/tostring.cc,
src/tgbaalgos/ltl2tgba_fm.cc: Remove all traces of these two
operators since they are not handled like sugar.
* doc/tl/tl.tex: Adjust documentation to reflect the fact that these
two operators are sugar.
This commit is contained in:
Alexandre Duret-Lutz 2012-04-15 00:13:42 +02:00
parent 210723e30c
commit abaf102746
7 changed files with 38 additions and 272 deletions
Download patch file Download diff file Expand all files Collapse all files

65
doc/tl/tl.tex
View file

@ -580,22 +580,6 @@ denote arbitrary SERE and $b$ denotes a Boolean formula.
& $f\STAR{\mvar{i}:}$ & $f\STAR{\mvar{i}:}$
& $f\STAR{\mvar{i} to}$ & $f\STAR{\mvar{i} to}$
& $f\STAR{\mvar{i},}$\\ & $f\STAR{\mvar{i},}$\\
bounded occurrence & $b\EQUAL{\mvar{i}..\mvar{j}}$
& $b\EQUAL{\mvar{i}:\mvar{j}}$
& $b\EQUAL{\mvar{i} to \mvar{j}}$
& $b\EQUAL{\mvar{i},\mvar{j}}$\\
unbounded occurrence & $b\EQUAL{\mvar{i}..}$
& $b\EQUAL{\mvar{i}:}$
& $b\EQUAL{\mvar{i} to}$
& $b\EQUAL{\mvar{i},}$\\
bounded goto & $b\GOTO{\mvar{i}..\mvar{j}}$
& $b\GOTO{\mvar{i}:\mvar{j}}$
& $b\GOTO{\mvar{i} to \mvar{j}}$
& $b\GOTO{\mvar{i},\mvar{j}}$\\
unbounded goto & $b\GOTO{\mvar{i}..}$
& $b\GOTO{\mvar{i}:}$
& $b\GOTO{\mvar{i} to}$
& $b\GOTO{\mvar{i},}$\\
\end{tabular} \end{tabular}
\end{center} \end{center}
@ -642,15 +626,7 @@ $b$ is a Boolean formula.
\text{or} & \mvar{i}>0 \land (\exists k\in\N,\, \text{or} & \mvar{i}>0 \land (\exists k\in\N,\,
(\sigma^{0..k-1}\VDash f) \land (\sigma^{k..} (\sigma^{0..k-1}\VDash f) \land (\sigma^{k..}
\VDash f\STAR{\mvar{i-1}..}))\\ \VDash f\STAR{\mvar{i-1}..}))\\
\end{cases}\\ \end{cases}
\sigma\VDash b\EQUAL{\mvar{i}..\mvar{j}} & \iff
\sigma\VDash\mathtt{\{\{}\NOT b\,\mathtt\}\STAR{0..}\CONCAT\ b\,\mathtt\}\STAR{\mvar{i}..\mvar{j}}\CONCAT\mathtt\{\NOT b\,\mathtt\}\STAR{0..}\\
\sigma\VDash b\EQUAL{\mvar{i}..} & \iff
\sigma\VDash\mathtt{\{\{}\NOT b\,\mathtt\}\STAR{0..}\CONCAT\ b\,\mathtt\}\STAR{\mvar{i}..}\CONCAT\mathtt\{\NOT b\,\mathtt\}\STAR{0..}\\
\sigma\VDash b\GOTO{\mvar{i}..\mvar{j}} & \iff
\sigma\VDash\mathtt{\{\{}\NOT b\,\mathtt\}\STAR{0..}\CONCAT\ b\,\mathtt\}\STAR{\mvar{i}..\mvar{j}}\\
\sigma\VDash b\GOTO{\mvar{i}..} & \iff
\sigma\VDash\mathtt{\{\{}\NOT b\,\mathtt\}\STAR{0..}\CONCAT\ b\,\mathtt\}\STAR{\mvar{i}..}\\
\end{align*}} \end{align*}}
Notes: Notes:
@ -667,9 +643,16 @@ operands are Boolean formul\ae.
The syntax on the left is equivalent to the syntax on the right. The syntax on the left is equivalent to the syntax on the right.
These rewritings are performed from left to right when parsing a These rewritings are performed from left to right when parsing a
formula, and some are performed from right to left when writing it for formula, and \emph{some} are performed from right to left when writing
output. it for output. $b$ must be a Boolean formula.
\begin{align*}
b\GOTO{\mvar{i}..\mvar{j}} &\equiv \mathtt{\{\{}\NOT b\mathtt{\}}\STAR{0..}\CONCAT b\mathtt{\}}\STAR{\mvar{i}..\mvar{j}} &
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\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{\}}
\end{align*}
\begin{align*} \begin{align*}
f\STARALT &\equiv f\STAR{0..}\\ f\STARALT &\equiv f\STAR{0..}\\
f\STAR{} &\equiv f\STAR{0..} & f\STAR{} &\equiv f\STAR{0..} &
@ -701,22 +684,10 @@ $b_1$, $b_2$ are assumed to be Boolean formul\ae.
\begin{align*} \begin{align*}
\0\STAR{0..\mvar{j}} &\equiv \eword & \0\STAR{0..\mvar{j}} &\equiv \eword &
\0\EQUAL{0..\mvar{j}} &\equiv \1\STAR{} & \0\STAR{\mvar{i}..\mvar{j}} &\equiv \0 \text{~if~}i>0 \\
\0\GOTO{0..\mvar{j}} &\equiv \eword \\
\0\STAR{\mvar{i}..\mvar{j}} &\equiv \0 \text{~if~}i>0 &
\0\EQUAL{\mvar{i}..\mvar{j}} &\equiv \0 \text{~if~}i>0&
\0\GOTO{\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&
\1\EQUAL{0} &\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 \\
\1\GOTO{0} &\equiv\eword\\ f\STAR{0}&\equiv \eword
f\STAR{0}&\equiv \eword &
\1\EQUAL{\mvar{i}..\mvar{j}}&\equiv \1\STAR{\mvar{i}..\mvar{j}}&
\1\GOTO{\mvar{i}..\mvar{j}}&\equiv \1\STAR{\mvar{i}..\mvar{j}}\\
f\STAR{\mvar{i}..\mvar{j}}\STAR{\mvar{k}..\mvar{l}} &\equiv f\STAR{\mvar{ik}..\mvar{jl}}&
b\EQUAL{0..}&\equiv 1\STAR{} &
b\GOTO{0}&\equiv \eword \\
&\drsh\text{~if~}i(k+1)\le jk+1 &
b\EQUAL{0}&\equiv (\NOT b)\STAR{} \\
\end{align*} \end{align*}
\noindent \noindent
@ -1396,16 +1367,6 @@ SERE.
b \ANDALT r &\text{if~} i\le 1\le j\\ b \ANDALT r &\text{if~} i\le 1\le j\\
\0 &\text{else}\\ \0 &\text{else}\\
\end{cases}\\ \end{cases}\\
b \ANDALT r\EQUAL{\mvar{i}..\mvar{j}} &\equiv
\begin{cases}
b \ANDALT r &\text{if~} i\le 1\le j\\
\0 &\text{else}\\
\end{cases}\\
b \ANDALT r\GOTO{\mvar{i}..\mvar{j}} &\equiv
\begin{cases}
b \ANDALT r &\text{if~} i\le 1\le j\\
\0 &\text{else}\\
\end{cases}\\
b \ANDALT \sere{r_1 \FUSION \ldots \FUSION r_n} &\equiv b \ANDALT r_1 \ANDALT \ldots \ANDALT r_n \\ b \ANDALT \sere{r_1 \FUSION \ldots \FUSION r_n} &\equiv b \ANDALT r_1 \ANDALT \ldots \ANDALT r_n \\
b \ANDALT \sere{r_1 \CONCAT \ldots \CONCAT r_n} &\equiv b \ANDALT \sere{r_1 \CONCAT \ldots \CONCAT r_n} &\equiv
\begin{cases} \begin{cases}

120
src/ltlast/bunop.cc
View file

@ -57,13 +57,6 @@ namespace spot
if (min_ == 0) if (min_ == 0)
is.accepting_eword = true; is.accepting_eword = true;
break; break;
case Equal:
case Goto:
is.finite = false;
is.accepting_eword = (min_ == 0);
// Equal and Goto can only apply to Boolean formulae.
assert(child->is_boolean());
break;
} }
} }
@ -140,12 +133,8 @@ namespace spot
{ {
switch (op_) switch (op_)
{ {
case Equal:
return "Equal";
case Star: case Star:
return "Star"; return "Star";
case Goto:
return "Goto";
} }
// Unreachable code. // Unreachable code.
assert(0); assert(0);
@ -157,9 +146,6 @@ namespace spot
{ {
std::ostringstream out; std::ostringstream out;
unsigned default_min = 0;
unsigned default_max = unbounded;
switch (op_) switch (op_)
{ {
case Star: case Star:
@ -171,39 +157,14 @@ namespace spot
} }
out << "[*"; out << "[*";
break; break;
case Equal:
out << "[=";
break;
case Goto:
out << "[->";
default_min = 1;
default_max = 1;
break;
} }
// Beware that the default parameters of the Goto operator are if (min_ != 0 || max_ != unbounded)
// not the same as Star or Equal:
//
// [->] = [->1..1]
// [->..] = [->1..unbounded]
// [*] = [*0..unbounded]
// [*..] = [*0..unbounded]
// [=] = [=0..unbounded]
// [=..] = [=0..unbounded]
//
// Strictly speaking [=] is not specified by PSL, and anyway we
// automatically rewrite Exp[=0..unbounded] as
// Exp[*0..unbounded], so we should never have to print [=]
// here.
//
// Also
// [*..] = [*0..unbounded]
if (min_ != default_min || max_ != default_max)
{ {
// Always print the min_, even when it is equal to // Always print the min_, even when it is equal to
// default_min, this way we avoid ambiguities (like // default_min, this way we avoid ambiguities (like
// when reading [*..3] near [*->..2]) // when reading a[*..3];b[->..2] which actually
// means a[*0..3];b[->1..2].
out << min_; out << min_;
if (min_ != max_) if (min_ != max_)
{ {
@ -227,81 +188,6 @@ namespace spot
switch (op) switch (op)
{ {
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 = unbounded;
op = Star;
child = constant::true_instance();
break;
}
else
return child;
}
// - 1[=0] = [*0]
// - 1[=min..max] = 1[*min..max]
if (child == constant::true_instance())
{
if (max == 0)
return constant::empty_word_instance();
else
{
op = Star;
break;
}
}
// - Exp[=0] = (!Exp)[*]
if (max == 0)
return bunop::instance(bunop::Star,
unop::instance(unop::Not, child));
break;
}
case Goto:
{
// - 0[->min..max] = 0 if min>0
// - 0[->0..max] = [*0]
if (child == constant::false_instance())
{
if (min == 0)
return constant::empty_word_instance();
else
return child;
}
// - 1[->0] = [*0]
// - 1[->min..max] = 1[*min..max]
if (child == constant::true_instance())
{
if (max == 0)
return constant::empty_word_instance();
else
{
op = Star;
break;
}
}
// - Exp[->0] = [*0]
if (max == 0)
{
child->destroy();
return constant::empty_word_instance();
}
break;
}
case Star: case Star:
{ {
// - [*0][*min..max] = [*0] // - [*0][*min..max] = [*0]

13
src/ltlast/bunop.hh
View file

@ -37,7 +37,7 @@ namespace spot
class bunop : public ref_formula class bunop : public ref_formula
{ {
public: public:
enum type { Star, Equal, Goto }; enum type { Star };
static const unsigned unbounded = -1U; static const unsigned unbounded = -1U;
@ -51,17 +51,6 @@ 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.
/// - 0[=0..max] = 1[*]
/// - 0[=min..max] = 0 if min > 0
/// - 1[=0] = [*0]
/// - 1[=min..max] = 1[*min..max]
/// - Exp[=0..] = [*]
/// - Exp[=0] = (!Exp)[*]
/// - 0[->0..max] = [*0]
/// - 0[->min..max] = 0 if min>0
/// - 1[->0] = [*0]
/// - 1[->min..max] = 1[*min..max]
/// - Exp[->0] = [*0]
/// ///
/// 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

20
src/ltlvisit/randomltl.cc
View file

@ -1,5 +1,5 @@
// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et // Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche
// Développement de l'Epita (LRDE). // et Développement de l'Epita (LRDE).
// Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
// Pierre et Marie Curie. // Pierre et Marie Curie.
@ -8,7 +8,7 @@
// //
// Spot is free software; you can redistribute it and/or modify it // Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by // under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or // the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version. // (at your option) any later version.
// //
// Spot is distributed in the hope that it will be useful, but WITHOUT // Spot is distributed in the hope that it will be useful, but WITHOUT
@ -276,7 +276,7 @@ namespace spot
// SEREs // SEREs
random_sere::random_sere(const atomic_prop_set* ap) random_sere::random_sere(const atomic_prop_set* ap)
: random_formula(11, ap), rb(ap) : random_formula(9, ap), rb(ap)
{ {
proba_[0].setup("eword", 1, eword_builder); proba_[0].setup("eword", 1, eword_builder);
proba_2_ = proba_ + 1; proba_2_ = proba_ + 1;
@ -284,13 +284,11 @@ namespace spot
proba_[1].setup("boolform", 1, boolform_builder); proba_[1].setup("boolform", 1, boolform_builder);
proba_[2].setup("star", 2, bunop_unbounded_builder<bunop::Star>); proba_[2].setup("star", 2, bunop_unbounded_builder<bunop::Star>);
proba_[3].setup("star_b", 2, bunop_bounded_builder<bunop::Star>); proba_[3].setup("star_b", 2, bunop_bounded_builder<bunop::Star>);
proba_[4].setup("equal_b", 2, bunop_bool_bounded_builder<bunop::Equal>); proba_[4].setup("and", 3, multop_builder<multop::And>);
proba_[5].setup("goto_b", 2, bunop_bool_bounded_builder<bunop::Goto>); proba_[5].setup("andNLM", 3, multop_builder<multop::AndNLM>);
proba_[6].setup("and", 3, multop_builder<multop::And>); proba_[6].setup("or", 3, multop_builder<multop::Or>);
proba_[7].setup("andNLM", 3, multop_builder<multop::AndNLM>); proba_[7].setup("concat", 3, multop_builder<multop::Concat>);
proba_[8].setup("or", 3, multop_builder<multop::Or>); proba_[8].setup("fusion", 3, multop_builder<multop::Fusion>);
proba_[9].setup("concat", 3, multop_builder<multop::Concat>);
proba_[10].setup("fusion", 3, multop_builder<multop::Fusion>);
update_sums(); update_sums();
} }

9
src/ltlvisit/simplify.cc
View file

@ -5,7 +5,7 @@
// //
// Spot is free software; you can redistribute it and/or modify it // Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by // under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or // the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version. // (at your option) any later version.
// //
// Spot is distributed in the hope that it will be useful, but WITHOUT // Spot is distributed in the hope that it will be useful, but WITHOUT
@ -2266,8 +2266,9 @@ namespace spot
bunop* r = down_cast<bunop*>(*i); bunop* r = down_cast<bunop*>(*i);
// b && r[*i..j] = b & r if i<=1<=j // b && r[*i..j] = b & r if i<=1<=j
// = 0 otherwise // = 0 otherwise
// likewise for b && r[=i..j] switch (r->op())
// and b && r[->i..j] {
case bunop::Star:
if (r->min() > 1 || r->max() < 1) if (r->min() > 1 || r->max() < 1)
goto returnfalse; goto returnfalse;
ares->push_back(r->child()->clone()); ares->push_back(r->child()->clone());
@ -2275,6 +2276,8 @@ namespace spot
*i = 0; *i = 0;
break; break;
} }
break;
}
case formula::MultOp: case formula::MultOp:
{ {
multop* r = down_cast<multop*>(*i); multop* r = down_cast<multop*>(*i);

6
src/ltlvisit/tostring.cc
View file

@ -385,12 +385,6 @@ namespace spot
} }
} }
break; break;
case bunop::Goto:
sugar = Goto;
break;
case bunop::Equal:
sugar = Equal;
break;
} }
emit_bunop_child(c); emit_bunop_child(c);

65
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -548,71 +548,6 @@ namespace spot
res_ |= now_to_concat(); res_ |= now_to_concat();
} }
return; return;
case bunop::Equal:
{
// b[=min..max] == (!b;b[=min..max]) | (b;b[=min-1..max-1])
// b[=0..max] == [*0] | (!b;b[=0..max]) | (b;b[=0..max-1])
// Note: b[=0] == (!b)[*] is a trivial identity, so it will
// never occur here.
formula* f1 = // !b;b[=min..max] or !b;b[->min..max]
multop::instance(multop::Concat,
unop::instance(unop::Not,
bo->child()->clone()),
bo->clone());
formula* f2 = // b;b[=min-1..max-1] or b;b[->min-1..max-1]
multop::instance(multop::Concat,
bo->child()->clone(),
bunop::instance(op,
bo->child()->clone(),
min2, max2));
f = multop::instance(multop::Or, f1, f2);
res_ = recurse_and_concat(f);
f->destroy();
if (min == 0)
res_ |= now_to_concat();
return;
}
case bunop::Goto:
{
// It is important to understand why we do not define Goto
// similarly to equal, i.e.:
//
// b[->min..max] == (!b;b[->min..max]) | (b;b[->min-1..max-1])
// b[->0..max] == [*0] | (!b;b[->0..max]) | (b;b[->0..max-1])
// Note: b[->0] == [*0] is a trivial identity, so it will
// never occur here.
//
// The above would be wrong when min=0.
// For instance consider {(c&!c)[->0..1]}<>->1
// This formula is equivalent to {[*0]}<>->1 which is false.
// However with above above rewritings, we get
// {[*0] | !(c&!c);(c&!c)[->0..1] | (c&!c);(c&!c)[->0] }<>->1
// which is equivalent to { 1;[*0] }<>-> 1 which is true. Oops!
//
// We therefore use the following rules instead:
// b[->min..max] == (!b)[*];b;b[->min-1..max-1]
// b[->0..max] == [*0] | (!b)[*];b;b[->min-1..max-1]
formula* f1 = // (!b)[*]
bunop::instance(bunop::Star,
unop::instance(unop::Not,
bo->child()->clone()),
0, bunop::unbounded);
formula* f2 = // b;b[->min-1..max-1]
multop::instance(multop::Concat,
bo->child()->clone(),
bunop::instance(op,
bo->child()->clone(),
min2, max2));
f = multop::instance(multop::Concat, f1, f2);
res_ = recurse_and_concat(f);
f->destroy();
if (min == 0)
res_ |= now_to_concat();
return;
}
} }
/* Unreachable code. */ /* Unreachable code. */
assert(0); assert(0);