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

psl: add support for the [:*i..j] operator

Browse source 
This operator is to ':' what [*i..j] is to ';'.

Part of issue #51.

* doc/tl/tl.tex: Document syntax, semantic, and trivial
simplifications.
* doc/tl/spotltl.sty: Add macros for new operators.
* src/ltlast/bunop.cc, src/ltlast/bunop.hh: Implement it.
* src/ltlast/multop.cc: Add some trivial simplifications.
* src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Parse it.
* src/ltltest/equals.test, src/ltltest/latex.test,
src/tgbatest/ltl2tgba.test: Add more tests.
* src/ltlvisit/randomltl.cc: Output this operator in
random PSL formulas.
* src/ltltest/rand.test: Adjust.
* src/tgbaalgos/ltl2tgba_fm.cc: Add translation rules.
* src/ltlvisit/tostring.cc: Add pretty printing code.
* src/ltlvisit/simplify.cc, src/ltlvisit/snf.cc: Adjust
switches.
* NEWS: Mention the new operator.
This commit is contained in:
Alexandre Duret-Lutz 2015-01-15 18:50:32 +01:00
parent eebbcac281
commit a79db4eefe
17 changed files with 442 additions and 162 deletions
Download patch file Download diff file Expand all files Collapse all files

9
NEWS
View file

@ -67,7 +67,14 @@ New in spot 1.99a (not yet released)
either by Divine (as patched by the LTSmin people) or by
Spins (the LTSmin compiler for Promela).
- LTL formulas can include /* comments */.
- LTL/PSL formulas can include /* comments */.
- PSL SEREs support a new operator [:*i..j], the iterated fusion.
[:*i..j] is to the fusion operator ':' what [*i..j] is to the
concatenation operator ';'. For instance (a*;b)[:*3] is the
same as (a*;b):(a*;b):(a*;b). The operator [:+], is syntactic
sugar for [:*1..], and corresponds to the operator ⊕ introduced
by Dax et al. (ATVA'09).
- GraphViz output now uses an horizontal layout by default.
The --dot option of the various command-line tools takes an

8
doc/tl/spotltl.sty
View file

@ -8,11 +8,11 @@
\newcommand{\ffalse}{\bot}
\newcommand{\eword}{\varepsilon} % empty word, denoted by [*0] in PSL
% These three are not declared as operator
% These three are not declared as operators
\newcommand{\F}{\mathsf{F}} % eventually
\newcommand{\G}{\mathsf{G}} % always
\newcommand{\X}{\mathsf{X}} % next
% The \mathbin tell TeX to adjust spacing for binary operators
% The \mathbin tells TeX to adjust spacing for binary operators
\newcommand{\M}{\mathbin{\mathsf{M}}} % strong release
\newcommand{\R}{\mathbin{\mathsf{R}}} % release
\newcommand{\U}{\mathbin{\mathsf{U}}} % until
@ -25,9 +25,11 @@
% Star-like PSL operators
\newcommand{\SereStar}[1]{^{\star#1}}
\newcommand{\SereFStar}[1]{^{\mathsf{:}\star#1}}
\newcommand{\SereEqual}[1]{^{=#1}}
\newcommand{\SereGoto}[1]{^{\to#1}}
\newcommand{\SerePlus}{^+}
\newcommand{\SereFPlus}{^{\mathsf{:}+}}
\newcommand{\SereFusion}{\mathbin{\mathsf{:}}}
\newcommand{\SereConcat}{\mathbin{\mathsf{;}}}
\newcommand{\SereOr}{\cup}
@ -45,5 +47,3 @@
%\newcommand{\seqXM}{\seqX}
\newcommand{\triggers}{\boxright}
\newcommand{\triggersX}{\boxRight}

99
doc/tl/tl.tex
View file

@ -92,6 +92,7 @@
\newcommand{\EQUAL}[1]{\texttt{[=#1]}}
\newcommand{\GOTO}[1]{\texttt{[->#1]}}
\newcommand{\PLUS}{\texttt{[+]}}
\newcommand{\FPLUS}{\texttt{[:+]}}
\newcommand{\eword}{\texttt{[*0]}}
\newcommand{\Esuffix}{\texttt{<>->}}
@ -599,14 +600,22 @@ denote arbitrary SERE.
NLM intersection\footnotemark & $f\AND g$ \\
concatenation & $f\CONCAT g$ \\
fusion & $f\FUSION g$ \\
bounded repetition & $f\STAR{\mvar{i}..\mvar{j}}$
bounded ;-iter. & $f\STAR{\mvar{i}..\mvar{j}}$
& $f\STAR{\mvar{i}:\mvar{j}}$
& $f\STAR{\mvar{i} to \mvar{j}}$
& $f\STAR{\mvar{i},\mvar{j}}$\\
\llap{un}bounded repetition & $f\STAR{\mvar{i}..}$
\llap{un}bounded ;-iter. & $f\STAR{\mvar{i}..}$
& $f\STAR{\mvar{i}:}$
& $f\STAR{\mvar{i} to}$
& $f\STAR{\mvar{i},}$\\
bounded :-iter. & $f\FSTAR{\mvar{i}..\mvar{j}}$
& $f\FSTAR{\mvar{i}:\mvar{j}}$
& $f\FSTAR{\mvar{i} to \mvar{j}}$
& $f\FSTAR{\mvar{i},\mvar{j}}$\\
\llap{un}bounded :-iter. & $f\FSTAR{\mvar{i}..}$
& $f\FSTAR{\mvar{i}:}$
& $f\FSTAR{\mvar{i} to}$
& $f\FSTAR{\mvar{i},}$\\
\end{tabular}
\end{center}
@ -657,6 +666,26 @@ $a$ is an atomic proposition.
\text{or} & \mvar{i}>0 \land (\exists k\in\N,\,
(\sigma^{0..k-1}\VDash f) \land (\sigma^{k..}
\VDash f\STAR{\mvar{i-1}..}))\\
\end{cases}\\
\sigma\VDash f\FSTAR{\mvar{i}..\mvar{j}}& \iff
\begin{cases}
\text{either} & \mvar{i}=0 \land \mvar{j}=0 \land \sigma\VDash\1 \\
\text{or} & \mvar{i}=0 \land \mvar{j}>0 \land (\exists k\in\N,\,
(\sigma^{0..k}\VDash f) \land (\sigma^{k..}
\VDash f\FSTAR{\mvar{0}..\mvar{j-1}}))\\
\text{or} & \mvar{i}>0 \land \mvar{j}>0 \land (\exists k\in\N,\,
(\sigma^{0..k}\VDash f) \land (\sigma^{k..}
\VDash f\FSTAR{\mvar{i-1}..\mvar{j-1}}))\\
\end{cases}\\
\sigma\VDash f\FSTAR{\mvar{i}..} & \iff
\begin{cases}
\text{either} & \mvar{i}=0 \land \sigma\VDash\1 \\
\text{or} & \mvar{i}=0 \land (\exists k\in\N,\,
(\sigma^{0..k}\VDash f) \land (\sigma^{k..}
\VDash f\FSTAR{\mvar{0}..}))\\
\text{or} & \mvar{i}>0 \land (\exists k\in\N,\,
(\sigma^{0..k}\VDash f) \land (\sigma^{k..}
\VDash f\FSTAR{\mvar{i-1}..}))\\
\end{cases}
\end{align*}}
@ -668,6 +697,29 @@ operands are Boolean formulas.
regardless of the value of $f$ and $g$. For instance
$a\STAR{}\FUSION b\STAR{}$ is actually equivalent to
$a\STAR{}\CONCAT\sere{a\ANDALT b}\CONCAT b\STAR{}$.
\item The $\FSTAR{\mvar{i}..}$ and $\FSTAR{\mvar{i}..\mvar{j}}$ operators are
iterations of the $\FUSION$ operator just like
The $\STAR{\mvar{i}..}$ and $\STAR{\mvar{i}..\mvar{j}}$ are
iterations of the $\CONCAT$ operator. More graphically:
\begin{align*}
f\STAR{\mvar{i}..\mvar{j}} &=
\underbrace{f\CONCAT f\CONCAT \ldots \CONCAT f}_{\text{between $\mvar{i}$ and $\mvar{j}$ copies of $f$}} &
f\FSTAR{\mvar{i}..\mvar{j}} &=
\underbrace{f\FUSION f\FUSION \ldots \FUSION f}_{\text{between $\mvar{i}$ and $\mvar{j}$ copies of $f$}}\\
\intertext{with the convention that}
f\STAR{0..0} &= \eword &
f\FSTAR{0..0} &= \1
\end{align*}
\item The $\FSTAR{\mvar{i}..}$ and $\FSTAR{\mvar{i}..\mvar{j}}$
operators are not defined in PSL. While the bounded iteration can
be seen as syntactic sugar on $\FUSION$, the unbounded version
really is a new operator.
$\FSTAR{1..}$, for which we define the $\FPLUS$ syntactic sugar
below, actually corresponds to the $^\oplus$ operator introduced
by~\citet{dax.09.atva}. With this simple addition, it is possible
to define a subset of PSL that expresses exactly the
stutter-invariant $\omega$-regular languages.
\end{itemize}
\subsection{Syntactic Sugar}
@ -687,24 +739,28 @@ it for output. $b$ must be a Boolean formula.
\begin{align*}
f\STARALT &\equiv f\STAR{0..}\\
f\STAR{} &\equiv f\STAR{0..} &
f\PLUS{} &\equiv f\STAR{1..} &
f\FSTAR{} &\equiv f\FSTAR{0..} &
f\EQUAL{} &\equiv f\EQUAL{0..} &
f\GOTO{} &\equiv f\GOTO{1..1} \\
f\STAR{..} &\equiv f\STAR{0..} &
&&
f\FSTAR{..} &\equiv f\FSTAR{0..} &
f\EQUAL{..} &\equiv f\EQUAL{0..} &
f\GOTO{..} &\equiv f\GOTO{1..} \\
f\STAR{..\mvar{j}} &\equiv f\STAR{0..\mvar{j}} &
&&
f\FSTAR{..\mvar{j}} &\equiv f\FSTAR{0..\mvar{j}} &
f\EQUAL{..\mvar{j}} &\equiv f\EQUAL{0..\mvar{j}} &
f\GOTO{..\mvar{j}} &\equiv f\GOTO{1..\mvar{j}} \\
f\STAR{\mvar{k}} &\equiv f\STAR{\mvar{k}..\mvar{k}} &
&&
f\FSTAR{\mvar{k}} &\equiv f\FSTAR{\mvar{k}..\mvar{k}} &
f\EQUAL{\mvar{k}} &\equiv f\EQUAL{\mvar{k}..\mvar{k}} &
f\GOTO{\mvar{k}} &\equiv f\GOTO{\mvar{k}..\mvar{k}} \\
\STAR{} &\equiv \1\STAR{0..} &
\PLUS{} &\equiv \1\STAR{1..} \\
\STAR{\mvar{k}} &\equiv \1\STAR{\mvar{k}..\mvar{k}} &
f\PLUS{} &\equiv f\STAR{1..} &
f\FPLUS{} &\equiv f\FSTAR{1..}
\end{align*}
\begin{align*}
\STAR{\mvar{k}} &\equiv \1\STAR{\mvar{k}..\mvar{k}} &
\STAR{} &\equiv \1\STAR{0..} &
\PLUS{} &\equiv \1\STAR{1..}
\end{align*}
\subsection{Trivial Identities (Occur Automatically)}
@ -720,6 +776,14 @@ $b_1$, $b_2$ are assumed to be Boolean formulas.
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{1}&\equiv f\\
b\FSTAR{0..\mvar{j}} &\equiv \1 &
b\FSTAR{\mvar{i}..\mvar{j}} &\equiv b \text{~if~}i>0 \\
\eword\FSTAR{0..\mvar{j}} &\equiv \1&
\eword\FSTAR{\mvar{i}..\mvar{j}} &\equiv \0\text{~if~}i>0 \\
&&
f\FSTAR{\mvar{i}..\mvar{j}}\FSTAR{\mvar{k}..\mvar{l}} &\equiv f\FSTAR{\mvar{ik}..\mvar{jl}}\text{~if~}i(k+1)\le jk+1 \\
f\FSTAR{0}&\equiv \1 &
f\FSTAR{1}&\equiv f\text{~if~}\varepsilon\nVDash f\\
\end{align*}
\noindent
@ -758,20 +822,19 @@ The following rules are all valid with the two arguments swapped.
f\AND f &\equiv f&
f\ANDALT f &\equiv f &
f\OR f &\equiv f&
&&
f\FUSION f&\equiv f\FSTAR{2}&
f\CONCAT f&\equiv f\STAR{2}\\
b_1 \AND b_2 &\equiv b_1\ANDALT b_2 &
&&
&&
b_1:b_2 &\equiv b_1\ANDALT b_2 &
f\STAR{\mvar{i}..\mvar{j}}\CONCAT f&\equiv f\STAR{\mvar{i+1}..\mvar{j+1}}\\
&&
&&
&&
&&
\mathllap{f\STAR{\mvar{i}..\mvar{j}}}\CONCAT f\STAR{\mvar{k}..\mvar{l}}&\equiv f\STAR{\mvar{i+k}..\mvar{j+l}}\\
b_1:b_2 &\equiv b_1\ANDALT b_2
\end{align*}
\begin{align*}
f\STAR{\mvar{i}..\mvar{j}}\CONCAT f&\equiv f\STAR{\mvar{i+1}..\mvar{j+1}} &
f\STAR{\mvar{i}..\mvar{j}}\CONCAT f\STAR{\mvar{k}..\mvar{l}}&\equiv f\STAR{\mvar{i+k}..\mvar{j+l}}\\
f\FSTAR{\mvar{i}..\mvar{j}}\FUSION f&\equiv f\FSTAR{\mvar{i+1}..\mvar{j+1}} &
f\FSTAR{\mvar{i}..\mvar{j}}\FUSION f\FSTAR{\mvar{k}..\mvar{l}}&\equiv f\FSTAR{\mvar{i+k}..\mvar{j+l}}
\end{align*}
\section{SERE-LTL Binding Operators}
The following operators combine a SERE $r$ with a PSL

201
src/ltlast/bunop.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -61,6 +61,11 @@ namespace spot
if (min_ == 0)
is.accepting_eword = true;
break;
case FStar:
is.accepting_eword = false;
if (max_ == unbounded)
is.finite = false;
break;
}
}
@ -106,6 +111,8 @@ namespace spot
{
case Star:
return "Star";
case FStar:
return "FStar";
}
SPOT_UNREACHABLE();
}
@ -120,20 +127,22 @@ namespace spot
case Star:
// Syntactic sugaring
if (min_ == 1 && max_ == unbounded)
{
out << "[+]";
return out.str();
}
return "[+]";
out << "[*";
break;
case FStar:
// Syntactic sugaring
if (min_ == 1 && max_ == unbounded)
return "[:+]";
out << "[:*";
break;
}
if (min_ != 0 || max_ != unbounded)
{
// Always print the min_, even when it is equal to
// default_min, this way we avoid ambiguities (like
// when reading a[*..3];b[->..2] which actually
// means a[*0..3];b[->1..2].
// Always print the min_, even when it is equal to 0, this
// way we avoid ambiguities (like when reading
// a[*..3];b[->..2] which actually means a[*0..3];b[->1..2].
out << min_;
if (min_ != max_)
{
@ -154,86 +163,110 @@ namespace spot
{
assert(min <= max);
// Some trivial simplifications.
const formula* neutral = nullptr;
switch (op)
{
case Star:
neutral = constant::empty_word_instance();
break;
case FStar:
neutral = constant::true_instance();
break;
}
// common trivial simplifications
// - [*0][*min..max] = [*0]
// - [*0][:*0..max] = 1
// - [*0][:*min..max] = 0 if min > 0
if (child == constant::empty_word_instance())
switch (op)
{
// - [*0][*min..max] = [*0]
if (child == constant::empty_word_instance())
return child;
// - 0[*0..max] = [*0]
// - 0[*min..max] = 0 if min > 0
if (child == constant::false_instance())
{
if (min == 0)
return constant::empty_word_instance();
else
return child;
}
// - Exp[*0] = [*0]
if (max == 0)
{
child->destroy();
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)]
// if i*(min+1)<=j(min)+1.
if (const bunop* s = is_bunop(child))
{
unsigned i = s->min();
unsigned j = s->max();
// Exp has to be true between i*min and j*min
// then between i*(min+1) and j*(min+1)
// ...
// finally between i*max and j*max
//
// We can merge these intervals into [i*min..j*max] iff the
// first are adjacent or overlap, i.e. iff
// i*(min+1) <= j*min+1.
// (Because i<=j, this entails that the other intervals also
// overlap).
const formula* exp = s->child();
if (j == unbounded)
{
min *= i;
max = unbounded;
// Exp[*min..max]
exp->clone();
child->destroy();
child = exp;
}
else
{
if (i * (min + 1) <= (j * min) + 1)
{
min *= i;
if (max != unbounded)
{
if (j == unbounded)
max = unbounded;
else
max *= j;
}
exp->clone();
child->destroy();
child = exp;
}
}
}
break;
case Star:
return neutral;
case FStar:
if (min == 0)
return neutral;
else
return constant::false_instance();
}
// - 0[*0..max] = [*0]
// - 0[*min..max] = 0 if min > 0
// - b[:*0..max] = 1
// - b[:*min..max] = 0 if min > 0
if (child == constant::false_instance()
|| (op == FStar && child->is_boolean()))
{
if (min == 0)
{
child->destroy();
return neutral;
}
return child;
}
// - Exp[*0] = [*0]
// - Exp[:*0] = 1
if (max == 0)
{
child->destroy();
return neutral;
}
// - Exp[*1] = Exp
// - Exp[:*1] = Exp if Exp does not accept [*0]
if (min == 1 && max == 1)
if (op == Star || !child->accepts_eword())
return child;
// - 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.
if (const bunop* s = is_bunop(child, op))
{
unsigned i = s->min();
unsigned j = s->max();
// Exp has to be true between i*min and j*min
// then between i*(min+1) and j*(min+1)
// ...
// finally between i*max and j*max
//
// We can merge these intervals into [i*min..j*max] iff the
// first are adjacent or overlap, i.e. iff
// i*(min+1) <= j*min+1.
// (Because i<=j, this entails that the other intervals also
// overlap).
const formula* exp = s->child();
if (j == unbounded)
{
min *= i;
max = unbounded;
// Exp[*min..max]
exp->clone();
child->destroy();
child = exp;
}
else
{
if (i * (min + 1) <= (j * min) + 1)
{
min *= i;
if (max != unbounded)
{
if (j == unbounded)
max = unbounded;
else
max *= j;
}
exp->clone();
child->destroy();
child = exp;
}
}
}
const formula* res;

13
src/ltlast/bunop.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche
// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -38,7 +38,7 @@ namespace spot
class SPOT_API bunop final : public formula
{
public:
enum type { Star };
enum type { Star, FStar };
static const unsigned unbounded = -1U;
@ -50,9 +50,16 @@ namespace spot
/// - 0[*0..max] = [*0]
/// - 0[*min..max] = 0 if min > 0
/// - [*0][*min..max] = [*0]
/// - Exp[*0] = [*0]
/// - Exp[*i..j][*k..l] = Exp[*ik..jl] if i*(k+1)<=jk+1.
/// - Exp[*0] = [*0]
/// - Exp[*1] = Exp
/// - b[:*0..max] = 1
/// - b[:*min..max] = b if min > 0
/// - [*0][:*0..max] = 1
/// - [*0][:*min..max] = 0 if min > 0
/// - Exp[:*i..j][:*k..l] = Exp[:*ik..jl] if i*(k+1)<=jk+1.
/// - Exp[:*0] = 1
/// - Exp[:*1] = Exp if Exp does not accept [*0]
///
/// These rewriting rules imply that it is not possible to build
/// an LTL formula object that is SYNTACTICALLY equal to one of

16
src/ltlast/multop.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@ -495,13 +495,19 @@ namespace spot
v->swap(tmp);
}
}
else if (op == Concat)
else if (op == Concat || op == Fusion)
{
// Perform an extra loop to merge starable items.
// f;f -> f[*2]
// f;f[*i..j] -> f[*i+1..j+1]
// f[*i..j];f -> f[*i+1..j+1]
// f[*i..j];f[*k..l] -> f[*i+k..j+l]
// same for FStar:
// f:f -> f[:*2]
// f:f[*i..j] -> f[:*i+1..j+1]
// f[:*i..j];f -> f[:*i+1..j+1]
// f[:*i..j];f[:*k..l] -> f[:*i+k..j+l]
bunop::type bop = op == Concat ? bunop::Star : bunop::FStar;
i = v->begin();
while (i != v->end())
{
@ -510,7 +516,7 @@ namespace spot
unsigned min;
unsigned max;
bool changed = false;
if (const bunop* is = is_Star(*i))
if (const bunop* is = is_bunop(*i, bop))
{
f = is->child();
min = is->min();
@ -528,7 +534,7 @@ namespace spot
const formula* f2;
unsigned min2;
unsigned max2;
if (const bunop* is = is_Star(*i))
if (const bunop* is = is_bunop(*i, bop))
{
f2 = is->child();
if (f2 != f)
@ -558,7 +564,7 @@ namespace spot
if (changed)
{
const formula* newfs =
bunop::instance(bunop::Star, f->clone(), min, max);
bunop::instance(bop, f->clone(), min, max);
(*fpos)->destroy();
*fpos = newfs;
}

55
src/ltlparse/ltlparse.yy
View file

@ -1,6 +1,6 @@
/* -*- coding: utf-8 -*-
** Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
** Recherche et Développement de l'Epita (LRDE).
** Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire
** de Recherche et Développement de l'Epita (LRDE).
** Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
** Université Pierre et Marie Curie.
@ -176,8 +176,11 @@ using namespace spot::ltl;
%token OP_F "sometimes operator" OP_G "always operator"
%token OP_X "next operator" OP_NOT "not operator"
%token OP_STAR "star operator" OP_BSTAR "bracket star operator"
%token OP_BFSTAR "bracket fusion-star operator"
%token OP_PLUS "plus operator"
%token OP_FPLUS "fusion-plus operator"
%token OP_STAR_OPEN "opening bracket for star operator"
%token OP_FSTAR_OPEN "opening bracket for fusion-star operator"
%token OP_EQUAL_OPEN "opening bracket for equal operator"
%token OP_GOTO_OPEN "opening bracket for goto operator"
%token OP_SQBKT_CLOSE "closing bracket"
@ -220,7 +223,9 @@ using namespace spot::ltl;
%nonassoc OP_X
/* High priority regex operator. */
%nonassoc OP_BSTAR OP_STAR_OPEN OP_PLUS OP_EQUAL_OPEN OP_GOTO_OPEN
%nonassoc OP_BSTAR OP_STAR_OPEN OP_PLUS
OP_BFSTAR OP_FSTAR_OPEN OP_FPLUS
OP_EQUAL_OPEN OP_GOTO_OPEN
/* Not has the most important priority (after Wring's `=0' and `=1',
but as those can only attach to atomic proposition, they do not
@ -229,7 +234,7 @@ using namespace spot::ltl;
%type <ltl> subformula booleanatom sere lbtformula boolformula
%type <ltl> bracedsere parenthesedsubformula
%type <minmax> starargs equalargs sqbracketargs gotoargs
%type <minmax> starargs fstarargs equalargs sqbracketargs gotoargs
%destructor { delete $$; } <str>
%destructor { $$->destroy(); } <ltl>
@ -370,6 +375,21 @@ starargs: kleen_star
{ error_list.emplace_back(@$, "missing closing bracket for star");
$$.min = $$.max = 0U; }
fstarargs: OP_BFSTAR
{ $$.min = 0U; $$.max = bunop::unbounded; }
| OP_FPLUS
{ $$.min = 1U; $$.max = bunop::unbounded; }
| OP_FSTAR_OPEN sqbracketargs
{ $$ = $2; }
| OP_FSTAR_OPEN error OP_SQBKT_CLOSE
{ error_list.emplace_back
(@$, "treating this fusion-star block as [:*]");
$$.min = 0U; $$.max = bunop::unbounded; }
| OP_FSTAR_OPEN error_opt END_OF_INPUT
{ error_list.emplace_back
(@$, "missing closing bracket for fusion-star");
$$.min = $$.max = 0U; }
equalargs: OP_EQUAL_OPEN sqbracketargs
{ $$ = $2; }
| OP_EQUAL_OPEN error OP_SQBKT_CLOSE
@ -507,15 +527,6 @@ sere: booleanatom
{ $$ = multop::instance(multop::Fusion, $1, $3); }
| sere OP_FUSION error
{ missing_right_binop($$, $1, @2, "fusion operator"); }
| sere starargs
{
if ($2.max < $2.min)
{
error_list.emplace_back(@2, "reversed range");
std::swap($2.max, $2.min);
}
$$ = bunop::instance(bunop::Star, $1, $2.min, $2.max);
}
| starargs
{
if ($1.max < $1.min)
@ -526,6 +537,24 @@ sere: booleanatom
$$ = bunop::instance(bunop::Star, constant::true_instance(),
$1.min, $1.max);
}
| sere starargs
{
if ($2.max < $2.min)
{
error_list.emplace_back(@2, "reversed range");
std::swap($2.max, $2.min);
}
$$ = bunop::instance(bunop::Star, $1, $2.min, $2.max);
}
| sere fstarargs
{
if ($2.max < $2.min)
{
error_list.emplace_back(@2, "reversed range");
std::swap($2.max, $2.min);
}
$$ = bunop::instance(bunop::FStar, $1, $2.min, $2.max);
}
| sere equalargs
{
if ($2.max < $2.min)

5
src/ltlparse/ltlscan.ll
View file

@ -1,5 +1,5 @@
/* -*- coding: utf-8 -*-
** Copyright (C) 2010, 2011, 2012, 2013, 2014, Laboratoire de
** Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 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), Université Pierre
@ -224,6 +224,9 @@ eol2 (\n\r)+|(\r\n)+
"[*]" BEGIN(0); return token::OP_BSTAR;
"[+]" BEGIN(0); return token::OP_PLUS;
"[*" BEGIN(sqbracket); return token::OP_STAR_OPEN;
"[:*]" BEGIN(0); return token::OP_BFSTAR;
"[:+]" BEGIN(0); return token::OP_FPLUS;
"[:*" BEGIN(sqbracket); return token::OP_FSTAR_OPEN;
"[=" BEGIN(sqbracket); return token::OP_EQUAL_OPEN;
"["{ARROWL} BEGIN(sqbracket); return token::OP_GOTO_OPEN;
<sqbracket>"]" BEGIN(0); return token::OP_SQBKT_CLOSE;

16
src/ltltest/equals.test
View file

@ -1,6 +1,6 @@
#! /bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2009, 2010, 2011, 2012, 2014 Laboratoire de Recherche et
# Copyright (C) 2009, 2010, 2011, 2012, 2014, 2015 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), Université Pierre
@ -181,6 +181,20 @@ G({1}<>->1), 1
{1[->10\,20];b}, {[*10..20];b}
{1[->..];b}, {[*1..];b}
{{a&!c}[->0];b}, b
{(a|c)[:*0..3];d}, {1;d}
{(a|c)[:*1..3];d}, {(a|c);d}
{0[:*0..3];d}, {1;d}
{0[:*1..3];d}, 0
{1[:*0..3];d}, {1;d}
{1[:*1..3];d}, {1;d}
{[*0][:*0..3];d}, {1;d}
{[*0][:*1..3];d}, 0
{(a*;b|c)[:*1to3][:*2:4]}, {(a*;b|c)[:*2..12]}
{(a*;b|c)[:*][:+]}, {(a*;b|c)[:*]}
{(a*;b|c)[:*0]}, 1
{(a*;b|c)[:*1]}, {(a*;b|c)}
{(a;b):(a;b):(a;b)[:*2]:(a;b):b*:b*:(c;d)[:*1]}, {(a;b)[:*5]:b*[:*2]:(c;d)}
EOF

3
src/ltltest/latex.test
View file

@ -1,6 +1,6 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2013 Laboratoire de Recherche et Développement
# Copyright (C) 2013, 2015 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@ -35,6 +35,7 @@ a U b W c R (d & e) M f
{a;b[=2];((c:d*) && f*);e[*2..]}<>-> {((a | [*0])*;b[+]) & (c1[->2])}[]-> h
{a;b;c} []=> {d*;e} <>=> !f
!{a;b*;c}! -> d
{a*;(b;c)[:*3..4];(c;d)[:+];d}!
G(uglyname->Fuglierlongname42)
EOF

13
src/ltltest/rand.test
View file

@ -1,6 +1,6 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2014 Laboratoire de Recherche et Développement
# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@ -34,6 +34,8 @@ eword 1
boolform 1
star 1
star_b 1
fstar 1
fstar_b 1
and 0
andNLM 0
or 1
@ -53,8 +55,11 @@ EOF
diff stdout expected
sere='eword=0,and=0,andNLM=0,fusion=0,star=0,star_b=0'
sere="$sere,or=0,concat=0,fstar=0,fstar_b=0"
run 0 $randltl -S -n 10000 a b c --tree-size=10..20 \
--sere-p=eword=0,and=0,andNLM=0,fusion=0,star=0,star_b=0,or=0,concat=0 \
--sere-p=$sere \
--boolean-p=equiv=0,implies=0,xor=0,and=0,not=0,false=0,true=0,or=0 \
--dump-pr > stdout
@ -64,6 +69,8 @@ eword 0
boolform 1
star 0
star_b 0
fstar 0
fstar_b 0
and 0
andNLM 0
or 0
@ -86,7 +93,7 @@ diff stdout expected
# Disabling all operators will prevent more formulas to be generated.
$randltl -S -n 10000 a b c --tree-size=10..20 \
--sere-p=eword=0,and=0,andNLM=0,fusion=0,star=0,star_b=0,or=0,concat=0 \
--sere-p=$sere \
--boolean-p=equiv=0,implies=0,xor=0,and=0,not=0,false=0,true=0,or=0 > out &&
exit 1
sort out > out2

14
src/ltlvisit/randomltl.cc
View file

@ -308,7 +308,7 @@ namespace spot
// SEREs
random_sere::random_sere(const atomic_prop_set* ap)
: random_formula(9, ap), rb(ap)
: random_formula(11, ap), rb(ap)
{
proba_[0].setup("eword", 1, eword_builder);
proba_2_ = proba_ + 1;
@ -316,11 +316,13 @@ namespace spot
proba_[1].setup("boolform", 1, boolform_builder);
proba_[2].setup("star", 2, bunop_unbounded_builder<bunop::Star>);
proba_[3].setup("star_b", 2, bunop_bounded_builder<bunop::Star>);
proba_[4].setup("and", 3, multop_builder<multop::AndRat>);
proba_[5].setup("andNLM", 3, multop_builder<multop::AndNLM>);
proba_[6].setup("or", 3, multop_builder<multop::OrRat>);
proba_[7].setup("concat", 3, multop_builder<multop::Concat>);
proba_[8].setup("fusion", 3, multop_builder<multop::Fusion>);
proba_[4].setup("fstar", 2, bunop_unbounded_builder<bunop::FStar>);
proba_[5].setup("fstar_b", 2, bunop_bounded_builder<bunop::FStar>);
proba_[6].setup("and", 3, multop_builder<multop::AndRat>);
proba_[7].setup("andNLM", 3, multop_builder<multop::AndNLM>);
proba_[8].setup("or", 3, multop_builder<multop::OrRat>);
proba_[9].setup("concat", 3, multop_builder<multop::Concat>);
proba_[10].setup("fusion", 3, multop_builder<multop::Fusion>);
update_sums();
}

9
src/ltlvisit/simplify.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche
// et Developpement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -1085,6 +1085,9 @@ namespace spot
}
result_ = bunop::instance(op, h, min, bo->max());
break;
case bunop::FStar:
result_ = bunop::instance(op, h, min, bo->max());
break;
}
}
@ -3274,6 +3277,8 @@ namespace spot
r->destroy();
f = 0;
break;
case bunop::FStar:
goto common;
}
break;
}

12
src/ltlvisit/snf.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2014 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
// Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -70,6 +70,11 @@ namespace spot
// Strip the star.
result_ = recurse(bo->child());
break;
case bunop::FStar:
// FIXME: Can we deal with FStar in a better way?
result_ = bo->clone();
break;
}
}
@ -171,6 +176,9 @@ namespace spot
std::max(bo->min(), 1U),
bo->max());
break;
case bunop::FStar:
result_ = bo->clone();
break;
}
}

39
src/ltlvisit/tostring.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2010, 2012, 2013, 2014 Laboratoire de Recherche
// et Développement de l'Epita (LRDE)
// Copyright (C) 2008, 2010, 2012, 2013, 2014, 2015 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), Université Pierre
// et Marie Curie.
@ -71,6 +71,8 @@ namespace spot
KCloseBunop,
KStarBunop,
KPlusBunop,
KFStarBunop,
KFPlusBunop,
KEqualBunop,
KGotoBunop,
};
@ -108,6 +110,8 @@ namespace spot
"]",
"[*",
"[+]",
"[:*",
"[:+]",
"[=",
"[->",
};
@ -121,7 +125,7 @@ namespace spot
" <-> ", // rewritten, although supported
" U ",
" V ",
" W ", // rewritten, although supported
" W ", // rewritten
" M ", // rewritten
"<>-> ", // not supported
"<>=> ", // not supported
@ -145,6 +149,8 @@ namespace spot
"]", // not supported
"[*", // not supported
"[+]", // not supported
"[:*", // not supported
"[:+]", // not supported
"[=", // not supported
"[->", // not supported
};
@ -182,6 +188,8 @@ namespace spot
"]", // not supported
"[*", // not supported
"[+]", // not supported
"[:*", // not supported
"[:+]", // not supported
"[=", // not supported
"[->", // not supported
};
@ -219,6 +227,8 @@ namespace spot
"]",
"[*",
"[+]",
"[:*",
"[:+]",
"[=",
"[->",
};
@ -256,6 +266,8 @@ namespace spot
"}",
"\\SereStar{",
"\\SerePlus{}",
"\\SereFStar{",
"\\SereFPlus{}",
"\\SereEqual{",
"\\SereGoto{",
};
@ -297,6 +309,8 @@ namespace spot
"}",
"^{\\star",
"^+",
"^{\\mathsf{:}\\star",
"^{\\mathsf{:}+}",
"^{=",
"^{\\to",
};
@ -577,17 +591,18 @@ namespace spot
visit(const bunop* bo)
{
const formula* c = bo->child();
enum { Star, Goto, Equal } sugar = Star;
enum { Star, FStar, Goto } sugar = Star;
unsigned default_min = 0;
unsigned default_max = bunop::unbounded;
bunop::type op = bo->op();
// Abbreviate "1[*]" as "[*]".
if (c != constant::true_instance())
if (c != constant::true_instance() || op != bunop::Star)
{
bunop::type op = bo->op();
switch (op)
{
case bunop::Star:
// Is this a Goto?
if (const multop* mo = is_Concat(c))
{
unsigned s = mo->size();
@ -599,6 +614,9 @@ namespace spot
}
}
break;
case bunop::FStar:
sugar = FStar;
break;
}
emit_bunop_child(c);
@ -616,8 +634,13 @@ namespace spot
}
emit(KStarBunop);
break;
case Equal:
emit(KEqualBunop);
case FStar:
if (min == 1 && max == bunop::unbounded)
{
emit(KFPlusBunop);
return;
}
emit(KFStarBunop);
break;
case Goto:
emit(KGotoBunop);

81
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire
// de Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015
// Laboratoire de Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire
// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
// Coopératifs (SRC), Université Pierre et Marie Curie.
@ -708,20 +708,30 @@ namespace spot
unsigned max = bo->max();
assert(max > 0);
bunop::type op = bo->op();
// we will interpret
// c[*i..j]
// or c[:*i..j]
// as
// c;c[*i-1..j-1]
// or c:c[*i-1..j-1]
// \........../
// this is f
unsigned min2 = (min == 0) ? 0 : (min - 1);
unsigned max2 =
(max == bunop::unbounded) ? bunop::unbounded : (max - 1);
f = bunop::instance(op, bo->child()->clone(), min2, max2);
// If we have something to append, we can actually append it
// to f. This is correct even in the case of FStar, as f
// cannot accept [*0].
if (to_concat_)
f = multop::instance(multop::Concat, f, to_concat_->clone());
bunop::type op = bo->op();
switch (op)
{
case bunop::Star:
f = bunop::instance(op, bo->child()->clone(), min2, max2);
if (to_concat_)
f = multop::instance(multop::Concat, f, to_concat_->clone());
if (!bo->child()->accepts_eword())
{
// f*;g -> f;f*;g | g
@ -777,6 +787,57 @@ namespace spot
res_ |= now_to_concat();
}
return;
case bunop::FStar:
{
res_ = recurse(bo->child());
bdd tail_bdd;
bool tail_computed = false;
minato_isop isop(res_);
bdd cube;
res_ = bddfalse;
if (min == 0)
{
// f[:*0..j];g can be satisfied by X(g).
res_ = next_to_concat();
}
while ((cube = isop.next()) != bddfalse)
{
bdd label = bdd_exist(cube, dict_.next_set);
bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
const formula* dest = dict_.conj_bdd_to_sere(dest_bdd);
// The destination is a final state. Make sure we
// can also exit if tail is satisfied. We do not
// even have to check the tail if min == 0.
if (dest->accepts_eword() && min != 0)
{
if (!tail_computed)
{
tail_bdd = recurse(f);
tail_computed = true;
}
res_ |= label & tail_bdd;
}
// If the destination is not 0 or [*0], it means it
// can have successors. Fusion the tail.
if (dest != constant::false_instance()
&& dest != constant::empty_word_instance())
{
const formula* dest2 =
multop::instance(multop::Fusion, dest, f->clone());
if (dest2 != constant::false_instance())
{
int x = dict_.register_next_variable(dest2);
dest2->destroy();
res_ |= label & bdd_ithvar(x);
}
}
}
f->destroy();
}
return;
}
SPOT_UNREACHABLE();
}
@ -961,8 +1022,8 @@ namespace spot
// If the destination is not 0 or [*0], it means it
// can have successors. Fusion the tail and append
// anything to concatenate.
if (dest->kind() != formula::Constant
|| dest == ltl::constant::true_instance())
if (dest != constant::false_instance()
&& dest != constant::empty_word_instance())
{
const formula* dest2 =
multop::instance(multop::Fusion, dest, tail->clone());

11
src/tgbatest/ltl2tgba.test
View file

@ -202,6 +202,17 @@ grep 'states: 4$' stdout
../../bin/ltlfilt -f '{a[*];b[*]}' --equivalent-to 'a | b'
../../bin/ltlfilt -r -f '{a[*];b[*]}' --equivalent-to 'a | b'
# A couple of tests for the [:*i..j] operator
../../bin/ltlfilt -q -f '{{a;b}[:*1..2];c}' \
--equivalent-to '(a&X(b&Xc)) | a&(X(b&a&X(b&Xc)))'
../../bin/ltlfilt -q -r -f '{{a;b}[:*1..2];c}' \
--equivalent-to '(a&X(b&Xc)) | a&(X(b&a&X(b&Xc)))'
../../bin/ltlfilt -q -f '{{a*}[:+];c}' --equivalent-to 'Xc R a'
../../bin/ltlfilt -q -r -f '{{a*}[:+];c}' --equivalent-to 'Xc R a'
../../bin/ltlfilt -q -f '{c && {b | [*0]}[:+]}' --equivalent-to 'c & b'
../../bin/ltlfilt -q -r -f '{c && {b | [*0]}[:+]}' --equivalent-to 'c & b'
# test unknown dot options
../../bin/ltl2tgba --dot=@ a 2>stderr && exit 1
grep 'ltl2tgba: unknown option.*@' stderr