introduce op::strong_X
This was prompted by reports by Andrew Wells and Yong Li. * NEWS, doc/tl/tl.tex: Document the changes. * THANKS: Add Andrew. * bin/ltlfilt.cc: Match --ltl before --from-ltlf if needed. * spot/parsetl/parsedecl.hh, spot/parsetl/parsetl.yy, spot/parsetl/scantl.ll: Parse X[!]. * spot/tl/formula.cc, spot/tl/formula.hh: Declare the new operator. * spot/tl/ltlf.cc: Adjust to handle op::X and op::strong_X correctly. * spot/tl/dot.cc, spot/tl/mark.cc, spot/tl/mutation.cc, spot/tl/print.cc, spot/tl/simplify.cc, spot/tl/snf.cc, spot/tl/unabbrev.cc, spot/twa/formula2bdd.cc, spot/twaalgos/ltl2taa.cc, spot/twaalgos/ltl2tgba_fm.cc, tests/core/ltlgrind.test, tests/core/rand.test, tests/core/sugar.test, tests/python/randltl.ipynb: Adjust. * tests/core/ltlfilt.test, tests/core/sugar.test, tests/core/utf8.test: More tests.
This commit is contained in:
Alexandre Duret-Lutz
parent
b91ba58bbe
commit
be389c5c25
26 changed files with 434 additions and 134 deletions
30
NEWS
30
NEWS
|
|
@ -1,5 +1,35 @@
|
|||
New in spot 2.8.1.dev (not yet released)
|
||||
|
||||
Library:
|
||||
|
||||
- Historically, Spot only supports LTL with infinite semantics
|
||||
so it had automatic simplifications reducing X(1) and X(0) to
|
||||
1 and 0 whenever such formulas are constructed. This
|
||||
caused issues for users of LTLf formulas, where it is important
|
||||
to distinguish a "weak next" (for which X(1)=1 but X(0)!=0) from
|
||||
a "strong next" (for which X(0)=0 but X(1)!=1).
|
||||
|
||||
To accomodate this, this version introduces a new operator
|
||||
op::strong_X in addition to the existing op::X (whose
|
||||
interpretation is now weak in LTLf). The syntax for the strong
|
||||
next is X[!] as a reference to the PSL syntax (where the strong
|
||||
next is written X!).
|
||||
|
||||
Trivial simplification rules for X are changed to just
|
||||
X(1) = 1 (and not X(0)=0 anymore)
|
||||
while we have
|
||||
X[!]0 = 0
|
||||
|
||||
The X(0)=0 and X[!]1=1 reductions are now preformed during LTL
|
||||
simplification, not automatically. Aside from the from_ltlf()
|
||||
function, the other functions of the library handle X and X[!] in
|
||||
the same way, since there is no different between X and X[!] over
|
||||
infinite words.
|
||||
|
||||
Operators F[n:m!] and G[n:m!] are also supported as strong
|
||||
variants of F[n:m] and G[n:m], but those four are only implemented
|
||||
as syntactic sugar.
|
||||
|
||||
Bugs fixed:
|
||||
|
||||
- Calling "autfilt --dualize" on an alternating automaton with
|
||||
|
|
|
|||
1
THANKS
1
THANKS
|
|
@ -2,6 +2,7 @@ We are grateful to these people for their comments, help, or suggestions.
|
|||
|
||||
Akim Demaille
|
||||
Andreas Tollkötter
|
||||
Andrew Wells
|
||||
Anton Pirogov
|
||||
Ayrat Khalimov
|
||||
Cambridge Yang
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement
|
||||
// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement
|
||||
// de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
|
|
@ -615,8 +615,14 @@ namespace
|
|||
if (negate)
|
||||
f = spot::formula::Not(f);
|
||||
|
||||
bool matched = true;
|
||||
|
||||
if (from_ltlf)
|
||||
{
|
||||
matched &= !ltl || f.is_ltl_formula();
|
||||
if (matched)
|
||||
f = spot::from_ltlf(f, from_ltlf);
|
||||
}
|
||||
|
||||
if (remove_x)
|
||||
{
|
||||
|
|
@ -656,8 +662,6 @@ namespace
|
|||
if (!opt->excl_ap.empty())
|
||||
f = opt->excl_ap.constrain(f);
|
||||
|
||||
bool matched = true;
|
||||
|
||||
matched &= !ltl || f.is_ltl_formula();
|
||||
matched &= !psl || f.is_psl_formula();
|
||||
matched &= !boolean || f.is_boolean();
|
||||
|
|
|
|||
|
|
@ -56,14 +56,18 @@
|
|||
\DeclareMathOperator{\F}{\texttt{F}}
|
||||
\DeclareMathOperator{\FALT}{\texttt{<>}}
|
||||
\newcommand{\FREP}[1]{\texttt{F[#1]}}
|
||||
\newcommand{\StrongFREP}[1]{\texttt{F[#1!]}}
|
||||
\DeclareMathOperator{\G}{\texttt{G}}
|
||||
\DeclareMathOperator{\GALT}{\texttt{[]}}
|
||||
\newcommand{\GREP}[1]{\texttt{G[#1]}}
|
||||
\newcommand{\StrongGREP}[1]{\texttt{G[#1!]}}
|
||||
\newcommand{\U}{\mathbin{\texttt{U}}}
|
||||
\newcommand{\R}{\mathbin{\texttt{R}}}
|
||||
\newcommand{\RALT}{\mathbin{\texttt{V}}}
|
||||
\DeclareMathOperator{\X}{\texttt{X}}
|
||||
\newcommand{\StrongX}{\texttt{X[!]}}
|
||||
\newcommand{\XREP}[1]{\texttt{X[#1]}}
|
||||
\newcommand{\StrongXREP}[1]{\texttt{X[#1!]}}
|
||||
\DeclareMathOperator{\XALT}{\texttt{()}}
|
||||
\newcommand{\M}{\mathbin{\texttt{M}}}
|
||||
\newcommand{\W}{\mathbin{\texttt{W}}}
|
||||
|
|
@ -485,7 +489,8 @@ temporal operators can be used to construct another temporal formula.
|
|||
& preferred & \multicolumn{1}{c}{other supported} & \multicolumn{2}{l}{UTF8 characters supported} \\
|
||||
operator & syntax & \multicolumn{1}{c}{syntaxes} & preferred & others \\
|
||||
\cmidrule(r){1-3} \cmidrule(l){4-5}
|
||||
Next & $\X f$ & $\XALT f$ & $\Circle$ \uni{25CB} & $\Circle$ \uni{25EF}\\
|
||||
(Weak) Next & $\X f$ & $\XALT f$ & $\Circle$ \uni{25CB} & $\Circle$ \uni{25EF}\\
|
||||
Strong Next & $\StrongX f$ & & \tikz[baseline=(X.base)]\node[inner sep=0pt, circle, draw](X){\textsc{x}}; \uni{24CD} & \\
|
||||
Eventually & $\F f$ & $\FALT f$ & $\Diamond$ \uni{25C7} & $\Diamond$ \uni{22C4} \uni{2662}\\
|
||||
Always & $\G f$ & $\GALT f$ & $\Square$ \uni{25A1} & $\Square$ \uni{2B1C} \uni{25FB}\\
|
||||
(Strong) Until & $f \U g$ \\
|
||||
|
|
@ -499,6 +504,7 @@ temporal operators can be used to construct another temporal formula.
|
|||
|
||||
\begin{align*}
|
||||
\sigma\vDash \X f &\iff \sigma^{1..}\vDash f\\
|
||||
\sigma\vDash \StrongX f &\iff \sigma^{1..}\vDash f\\
|
||||
\sigma\vDash \F f &\iff \exists i\in \N,\, \sigma^{i..}\vDash f\\
|
||||
\sigma\vDash \G f &\iff \forall i\in \N,\, \sigma^{i..}\vDash f\\
|
||||
\sigma\vDash f\U g &\iff \exists j\in\N,\,
|
||||
|
|
@ -515,6 +521,11 @@ temporal operators can be used to construct another temporal formula.
|
|||
\sigma \vDash f\R g &\iff (\sigma \vDash f\M g)\lor(\sigma\vDash \G g)
|
||||
\end{align*}
|
||||
|
||||
Note that the semantics of $\X$ (weak next) and $\StrongX$ (strong
|
||||
next) are identical in LTL formulas. The two operators make sense
|
||||
only to build LTLf formulas (i.e., LTL with finite semantics), for
|
||||
which support is being progressively introduced in Spot.
|
||||
|
||||
Appendix~\ref{sec:ltl-equiv} explains how to rewrite the above LTL
|
||||
operators using only $\X$ and one operator chosen among $\U$, $\W$,
|
||||
$\M$,and $\R$. This could be useful to understand the operators $\R$,
|
||||
|
|
@ -537,12 +548,20 @@ or all times between $n$ and $m$ steps.
|
|||
\GREP{\mvar{n}:\mvar{m}}f
|
||||
& \equiv \underbrace{\vphantom{(}\X\X\ldots\X}_{\mathclap{\text{\mvar{n} occ. of~}\X}} (f \AND \underbrace{\X(f \AND \X(\ldots \AND \X f))}_{\mathclap{\mvar{m}-\mvar{n}\text{~occ. of~}\X}})
|
||||
& \GREP{\mvar{n}:}f &\equiv \XREP{\mvar{n}}\G{}f\\
|
||||
\StrongXREP{\mvar{n}} f
|
||||
& \equiv \underbrace{\StrongX\StrongX\ldots\StrongX}_{\mathclap{\text{\mvar{n} occurrences of~}\StrongX}} f \\
|
||||
\StrongFREP{\mvar{n}:\mvar{m}}f
|
||||
& \equiv \underbrace{\vphantom{(}\StrongX\StrongX\ldots\StrongX}_{\mathclap{\text{\mvar{n} occ. of~}\StrongX}} (f \OR \underbrace{\StrongX(f \OR \StrongX(\ldots \OR \StrongX f))}_{\mathclap{\mvar{m}-\mvar{n}\text{~occ. of~}\StrongX}})
|
||||
& \StrongFREP{\mvar{n}:}f &\equiv \StrongXREP{\mvar{n}}\F{}f\\
|
||||
\StrongGREP{\mvar{n}:\mvar{m}}f
|
||||
& \equiv \underbrace{\vphantom{(}\StrongX\StrongX\ldots\StrongX}_{\mathclap{\text{\mvar{n} occ. of~}\StrongX}} (f \AND \underbrace{\StrongX(f \AND \StrongX(\ldots \AND \StrongX f))}_{\mathclap{\mvar{m}-\mvar{n}\text{~occ. of~}\StrongX}})
|
||||
& \StrongGREP{\mvar{n}:}f &\equiv \StrongXREP{\mvar{n}}\G{}f
|
||||
\end{align*}
|
||||
|
||||
\subsection{Trivial Identities (Occur Automatically)}
|
||||
|
||||
\begin{align*}
|
||||
\X\0 &\equiv \0 &
|
||||
\StrongX\0 &\equiv \0 &
|
||||
\F\0 &\equiv \0 &
|
||||
\G\0 &\equiv \0 \\
|
||||
\X\1 &\equiv \1 &
|
||||
|
|
@ -998,18 +1017,19 @@ operator, even if the operator has multiple synonyms (like \samp{|},
|
|||
\mid{} & \mathit{sere}\msamp{\CONCAT}\mathit{sere} & \mid{} & \mathit{sere}\msamp{\EQUAL{\mvar{i}..\mvar{j}}} \\
|
||||
\mid{} & \mathit{sere}\msamp{\FUSION}\mathit{sere} & \mid{} & \mathit{sere}\msamp{\GOTO{\mvar{i}..\mvar{j}}} \\[1ex]
|
||||
\mathit{tformula} ::={} & \mathit{bformula} & \mid{} & \msamp{\X}\,\mathit{tformula} & \mid{} & \tsamp{\{}\mathit{sere}\tsamp{\}}\,\msamp{\Asuffix}\,\mathit{tformula} \\
|
||||
\mid{} & \tsamp{(}\,\mathit{tformula}\,\tsamp{)} & \mid{} & \msamp{\XREP{\mvar{i}..\mvar{j}}}\,\mathit{tformula} & \mid{} & \tsamp{\{}\mathit{sere}\tsamp{\}}\,\msamp{\AsuffixEQ}\,\mathit{tformula} \\
|
||||
\mid{} & \msamp{\NOT}\,\mathit{tformula}\, & \mid{} & \msamp{\F}\,\mathit{tformula} & \mid{} & \tsamp{\{}\mathit{sere}\tsamp{\}}\,\msamp{\Esuffix}\,\mathit{tformula} \\
|
||||
\mid{} & \mathit{tformula}\,\msamp{\AND}\,\mathit{tformula} & \mid{} & \msamp{\FREP{\mvar{i}..\mvar{j}}}\,\mathit{tformula} & \mid{} & \tsamp{\{}\mathit{sere}\tsamp{\}}\,\msamp{\EsuffixEQ}\,\mathit{tformula} \\
|
||||
\mid{} & \mathit{tformula}\,\msamp{\OR}\,\mathit{tformula} & \mid{} & \msamp{\G}\,\mathit{tformula} & \mid{} & \tsamp{\{}\mathit{sere}\tsamp{\}} \\
|
||||
\mid{} & \mathit{tformula}\,\msamp{\IMPLIES}\,\mathit{tformula} & \mid{} & \msamp{\GREP{\mvar{i}..\mvar{j}}}\,\mathit{tformula} & \mid{} & \tsamp{\{}\mathit{sere}\tsamp{\}}\msamp{\NOT} \\
|
||||
\mid{} & \mathit{tformula}\,\msamp{\XOR}\,\mathit{tformula} & \mid{} & \mathit{tformula}\,\msamp{\U}\,\mathit{tformula} \\
|
||||
\mid{} & \mathit{tformula}\,\msamp{\EQUIV}\,\mathit{tformula} & \mid{} & \mathit{tformula}\,\msamp{\W}\,\mathit{tformula} \\
|
||||
& & \mid{} & \mathit{tformula}\,\msamp{\R}\,\mathit{tformula} \\
|
||||
& & \mid{} & \mathit{tformula}\,\msamp{\M}\,\mathit{tformula} \\
|
||||
\mid{} & \tsamp{(}\,\mathit{tformula}\,\tsamp{)} & \mid{} & \msamp{\StrongX}\,\mathit{tformula} & \mid{} & \tsamp{\{}\mathit{sere}\tsamp{\}}\,\msamp{\AsuffixEQ}\,\mathit{tformula} \\
|
||||
\mid{} & \msamp{\NOT}\,\mathit{tformula}\, & \mid{} & \msamp{\XREP{\mvar{i}..\mvar{j}}}\,\mathit{tformula} & \mid{} & \tsamp{\{}\mathit{sere}\tsamp{\}}\,\msamp{\Esuffix}\,\mathit{tformula} \\
|
||||
\mid{} & \mathit{tformula}\,\msamp{\AND}\,\mathit{tformula} & \mid{} & \msamp{\StrongXREP{\mvar{i}..\mvar{j}}}\,\mathit{tformula} & \mid{} & \tsamp{\{}\mathit{sere}\tsamp{\}}\,\msamp{\EsuffixEQ}\,\mathit{tformula} \\
|
||||
\mid{} & \mathit{tformula}\,\msamp{\OR}\,\mathit{tformula} & \mid{} & \msamp{\F}\,\mathit{tformula} & \mid{} & \tsamp{\{}\mathit{sere}\tsamp{\}} \\
|
||||
\mid{} & \mathit{tformula}\,\msamp{\IMPLIES}\,\mathit{tformula} & \mid{} & \msamp{\FREP{\mvar{i}..\mvar{j}}}\,\mathit{tformula} & \mid{} & \tsamp{\{}\mathit{sere}\tsamp{\}}\msamp{\NOT} \\
|
||||
\mid{} & \mathit{tformula}\,\msamp{\XOR}\,\mathit{tformula} & \mid{} & \msamp{\StrongFREP{\mvar{i}..\mvar{j}}}\,\mathit{tformula} \\
|
||||
\mid{} & \mathit{tformula}\,\msamp{\EQUIV}\,\mathit{tformula} & \mid{} & \msamp{\G}\,\mathit{tformula} \\
|
||||
\mid{} & \mathit{tformula}\,\msamp{\U}\,\mathit{tformula} & \mid{} & \msamp{\GREP{\mvar{i}..\mvar{j}}}\,\mathit{tformula} \\
|
||||
\mid{} & \mathit{tformula}\,\msamp{\W}\,\mathit{tformula} & \mid{} & \msamp{\StrongGREP{\mvar{i}..\mvar{j}}}\,\mathit{tformula} \\
|
||||
\mid{} & \mathit{tformula}\,\msamp{\R}\,\mathit{tformula} \\
|
||||
\mid{} & \mathit{tformula}\,\msamp{\M}\,\mathit{tformula}
|
||||
\end{align*}
|
||||
|
||||
|
||||
\section{Operator precedence}
|
||||
|
||||
The following operator precedence describes the current parser of
|
||||
|
|
@ -1142,6 +1162,7 @@ rules:
|
|||
\varphi_E ::={}& \0
|
||||
\mid \1
|
||||
\mid \X \varphi_E
|
||||
\mid \StrongX \varphi_E
|
||||
\mid \F \varphi
|
||||
\mid \G \varphi_E
|
||||
\mid \varphi_E\AND \varphi_E
|
||||
|
|
@ -1156,6 +1177,7 @@ rules:
|
|||
\varphi_U ::={}& \0
|
||||
\mid \1
|
||||
\mid \X \varphi_U
|
||||
\mid \StrongX \varphi_U
|
||||
\mid \F \varphi_U
|
||||
\mid \G \varphi
|
||||
\mid \varphi_U\AND \varphi_U
|
||||
|
|
@ -1450,6 +1472,10 @@ they try to lift subformulas that are both eventual and universal
|
|||
are applied only when \verb|favor_event_univ|' is \texttt{false}: they
|
||||
try to \textit{lower} subformulas that are both eventual and universal.
|
||||
|
||||
Currently all these simplifications assume LTL semantics, so they make
|
||||
no differences between $\X$ and $\StrongX$. For simplicity, they are
|
||||
only listed with $\X$.
|
||||
|
||||
\subsection{Basic Simplifications}\label{sec:basic-simp}
|
||||
|
||||
These simplifications are enabled with
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2010, 2012, 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
// Copyright (C) 2010, 2012, 2013, 2014, 2015, 2019 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE)
|
||||
// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
|
|
|
|||
|
|
@ -207,8 +207,10 @@ using namespace spot;
|
|||
%token OP_U "until operator" OP_R "release operator"
|
||||
%token OP_W "weak until operator" OP_M "strong release operator"
|
||||
%token OP_F "sometimes operator" OP_G "always operator"
|
||||
%token OP_X "next operator" OP_NOT "not operator"
|
||||
%token OP_XREP "X[.] operator" OP_FREP "F[.] operator" OP_GREP "G[.] operator"
|
||||
%token OP_X "next operator" OP_STRONG_X "strong next operator"
|
||||
%token OP_NOT "not operator"
|
||||
%token OP_XREP "X[.] operator"
|
||||
%token OP_FREP "F[.] operator" OP_GREP "G[.] operator"
|
||||
%token OP_STAR "star operator" OP_BSTAR "bracket star operator"
|
||||
%token OP_BFSTAR "bracket fusion-star operator"
|
||||
%token OP_PLUS "plus operator"
|
||||
|
|
@ -218,6 +220,7 @@ using namespace spot;
|
|||
%token OP_EQUAL_OPEN "opening bracket for equal operator"
|
||||
%token OP_GOTO_OPEN "opening bracket for goto operator"
|
||||
%token OP_SQBKT_CLOSE "closing bracket"
|
||||
%token OP_SQBKT_STRONG_CLOSE "closing !]"
|
||||
%token <num> OP_SQBKT_NUM "number for square bracket operator"
|
||||
%token OP_UNBOUNDED "unbounded mark"
|
||||
%token OP_SQBKT_SEP "separator for square bracket operator"
|
||||
|
|
@ -261,7 +264,7 @@ using namespace spot;
|
|||
/* LTL operators. */
|
||||
%right OP_U OP_R OP_M OP_W
|
||||
%precedence OP_F OP_G OP_FREP OP_GREP
|
||||
%precedence OP_X OP_XREP
|
||||
%precedence OP_X OP_XREP OP_STRONG_X
|
||||
|
||||
/* High priority regex operator. */
|
||||
%precedence OP_BSTAR OP_STAR_OPEN OP_PLUS
|
||||
|
|
@ -887,16 +890,33 @@ subformula: booleanatom
|
|||
error_list.emplace_back(@1 + @3,
|
||||
"F[n:m] expects two parameters");
|
||||
}
|
||||
| OP_FREP OP_SQBKT_NUM OP_SQBKT_STRONG_CLOSE subformula
|
||||
%prec OP_FREP
|
||||
{ $$ = fnode::nested_unop_range(op::strong_X, op::Or, $2, $2, $4);
|
||||
error_list.emplace_back(@1 + @3,
|
||||
"F[n:m!] expects two parameters");
|
||||
}
|
||||
| OP_FREP OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE
|
||||
subformula %prec OP_FREP
|
||||
{ $$ = fnode::nested_unop_range(op::X, op::Or, $2, $4, $6); }
|
||||
| OP_FREP OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM
|
||||
OP_SQBKT_STRONG_CLOSE subformula %prec OP_FREP
|
||||
{ $$ = fnode::nested_unop_range(op::strong_X,
|
||||
op::Or, $2, $4, $6); }
|
||||
| OP_FREP OP_SQBKT_NUM OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE
|
||||
subformula %prec OP_FREP
|
||||
{ $$ = fnode::nested_unop_range(op::X, op::Or, $2,
|
||||
fnode::unbounded(), $5); }
|
||||
| OP_FREP OP_SQBKT_NUM OP_SQBKT_SEP_unbounded OP_SQBKT_STRONG_CLOSE
|
||||
subformula %prec OP_FREP
|
||||
{ $$ = fnode::nested_unop_range(op::strong_X, op::Or, $2,
|
||||
fnode::unbounded(), $5); }
|
||||
| OP_FREP OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE
|
||||
error
|
||||
{ missing_right_op($$, @1 + @5, "F[.] operator"); }
|
||||
| OP_FREP OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM
|
||||
OP_SQBKT_STRONG_CLOSE error
|
||||
{ missing_right_op($$, @1 + @5, "F[.!] operator"); }
|
||||
| OP_FREP error_opt END_OF_INPUT
|
||||
{ error_list.emplace_back(@$, "missing closing bracket for F[.]");
|
||||
$$ = fnode::ff(); }
|
||||
|
|
@ -904,6 +924,10 @@ subformula: booleanatom
|
|||
{ error_list.emplace_back(@1 + @3,
|
||||
"treating this F[.] as a simple F");
|
||||
$$ = fnode::unop(op::F, $4); }
|
||||
| OP_FREP error OP_SQBKT_STRONG_CLOSE subformula %prec OP_FREP
|
||||
{ error_list.emplace_back(@1 + @3,
|
||||
"treating this F[.!] as a simple F");
|
||||
$$ = fnode::unop(op::F, $4); }
|
||||
| OP_G subformula
|
||||
{ $$ = fnode::unop(op::G, $2); }
|
||||
| OP_G error
|
||||
|
|
@ -911,18 +935,36 @@ subformula: booleanatom
|
|||
| OP_GREP OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE
|
||||
subformula %prec OP_GREP
|
||||
{ $$ = fnode::nested_unop_range(op::X, op::And, $2, $4, $6); }
|
||||
| OP_GREP OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM
|
||||
OP_SQBKT_STRONG_CLOSE subformula %prec OP_GREP
|
||||
{ $$ = fnode::nested_unop_range(op::strong_X, op::And,
|
||||
$2, $4, $6); }
|
||||
| OP_GREP OP_SQBKT_NUM OP_SQBKT_SEP_unbounded OP_SQBKT_CLOSE
|
||||
subformula %prec OP_GREP
|
||||
{ $$ = fnode::nested_unop_range(op::X, op::And, $2,
|
||||
fnode::unbounded(), $5); }
|
||||
| OP_GREP OP_SQBKT_NUM OP_SQBKT_SEP_unbounded OP_SQBKT_STRONG_CLOSE
|
||||
subformula %prec OP_GREP
|
||||
{ $$ = fnode::nested_unop_range(op::strong_X, op::And, $2,
|
||||
fnode::unbounded(), $5); }
|
||||
| OP_GREP OP_SQBKT_NUM OP_SQBKT_CLOSE subformula %prec OP_GREP
|
||||
{ $$ = fnode::nested_unop_range(op::X, op::And, $2, $2, $4);
|
||||
error_list.emplace_back(@1 + @3,
|
||||
"G[n:m] expects two parameters");
|
||||
}
|
||||
| OP_GREP OP_SQBKT_NUM OP_SQBKT_STRONG_CLOSE subformula
|
||||
%prec OP_GREP
|
||||
{ $$ = fnode::nested_unop_range(op::strong_X, op::And,
|
||||
$2, $2, $4);
|
||||
error_list.emplace_back(@1 + @3,
|
||||
"G[n:m!] expects two parameters");
|
||||
}
|
||||
| OP_GREP OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM OP_SQBKT_CLOSE
|
||||
error
|
||||
{ missing_right_op($$, @1 + @5, "G[.] operator"); }
|
||||
| OP_GREP OP_SQBKT_NUM OP_SQBKT_SEP OP_SQBKT_NUM
|
||||
OP_SQBKT_STRONG_CLOSE error
|
||||
{ missing_right_op($$, @1 + @5, "G[.!] operator"); }
|
||||
| OP_GREP error_opt END_OF_INPUT
|
||||
{ error_list.emplace_back(@$, "missing closing bracket for G[.]");
|
||||
$$ = fnode::ff(); }
|
||||
|
|
@ -930,10 +972,18 @@ subformula: booleanatom
|
|||
{ error_list.emplace_back(@1 + @3,
|
||||
"treating this G[.] as a simple G");
|
||||
$$ = fnode::unop(op::F, $4); }
|
||||
| OP_GREP error OP_SQBKT_STRONG_CLOSE subformula %prec OP_GREP
|
||||
{ error_list.emplace_back(@1 + @3,
|
||||
"treating this G[.!] as a simple G");
|
||||
$$ = fnode::unop(op::F, $4); }
|
||||
| OP_X subformula
|
||||
{ $$ = fnode::unop(op::X, $2); }
|
||||
| OP_X error
|
||||
{ missing_right_op($$, @1, "next operator"); }
|
||||
| OP_STRONG_X subformula
|
||||
{ $$ = fnode::unop(op::strong_X, $2); }
|
||||
| OP_STRONG_X error
|
||||
{ missing_right_op($$, @1, "strong next operator"); }
|
||||
| OP_XREP OP_SQBKT_NUM OP_SQBKT_CLOSE subformula %prec OP_XREP
|
||||
{ $$ = fnode::nested_unop_range(op::X, op::Or, $2, $2, $4); }
|
||||
| OP_XREP OP_SQBKT_NUM OP_SQBKT_CLOSE error
|
||||
|
|
@ -941,6 +991,15 @@ subformula: booleanatom
|
|||
| OP_XREP error OP_SQBKT_CLOSE subformula %prec OP_XREP
|
||||
{ error_list.emplace_back(@$, "treating this X[.] as a simple X");
|
||||
$$ = fnode::unop(op::X, $4); }
|
||||
| OP_XREP OP_SQBKT_STRONG_CLOSE subformula %prec OP_XREP
|
||||
{ $$ = fnode::unop(op::strong_X, $3); }
|
||||
| OP_XREP OP_SQBKT_NUM OP_SQBKT_STRONG_CLOSE subformula
|
||||
%prec OP_XREP
|
||||
{ $$ = fnode::nested_unop_range(op::strong_X,
|
||||
op::Or, $2, $2, $4); }
|
||||
| OP_XREP error OP_SQBKT_STRONG_CLOSE subformula %prec OP_XREP
|
||||
{ error_list.emplace_back(@$, "treating this X[.!] as a simple X[!]");
|
||||
$$ = fnode::unop(op::strong_X, $4); }
|
||||
| OP_XREP error_opt END_OF_INPUT
|
||||
{ error_list.emplace_back(@$, "missing closing bracket for X[.]");
|
||||
$$ = fnode::ff(); }
|
||||
|
|
|
|||
|
|
@ -64,6 +64,7 @@ DARROWL "=>"|"⇒"|"⟹"
|
|||
ARROWLR "<->"|"<-->"|"↔"
|
||||
DARROWLR "<=>"|"⇔"
|
||||
CIRCLE "()"|"○"|"◯"
|
||||
CIRCLEX "Ⓧ"
|
||||
NOT "!"|"~"|"¬"
|
||||
BOXARROW {BOX}{ARROWL}|"|"{ARROWL}|"↦"
|
||||
BOXDARROW {BOX}{DARROWL}|"|"{DARROWL}|"⤇"
|
||||
|
|
@ -254,6 +255,7 @@ eol2 (\n\r)+|(\r\n)+
|
|||
"[=" BEGIN(sqbracket); return token::OP_EQUAL_OPEN;
|
||||
"["{ARROWL} BEGIN(sqbracket); return token::OP_GOTO_OPEN;
|
||||
<sqbracket>"]" BEGIN(0); return token::OP_SQBKT_CLOSE;
|
||||
<sqbracket>"!]" BEGIN(0); return token::OP_SQBKT_STRONG_CLOSE;
|
||||
<sqbracket>[0-9]+ {
|
||||
errno = 0;
|
||||
unsigned long n = strtoul(yytext, 0, 10);
|
||||
|
|
@ -313,6 +315,7 @@ eol2 (\n\r)+|(\r\n)+
|
|||
"U" BEGIN(0); return token::OP_U;
|
||||
"R"|"V" BEGIN(0); return token::OP_R;
|
||||
"X"|{CIRCLE} BEGIN(0); return token::OP_X;
|
||||
{CIRCLEX} BEGIN(0); return token::OP_STRONG_X;
|
||||
"W" BEGIN(0); return token::OP_W;
|
||||
"M" BEGIN(0); return token::OP_M;
|
||||
|
||||
|
|
|
|||
|
|
@ -76,6 +76,7 @@ namespace spot
|
|||
case op::ap:
|
||||
case op::Not:
|
||||
case op::X:
|
||||
case op::strong_X:
|
||||
case op::F:
|
||||
case op::G:
|
||||
case op::Closure:
|
||||
|
|
|
|||
|
|
@ -242,6 +242,7 @@ namespace spot
|
|||
C(Star);
|
||||
C(FStar);
|
||||
C(first_match);
|
||||
C(strong_X);
|
||||
#undef C
|
||||
}
|
||||
SPOT_UNREACHABLE();
|
||||
|
|
@ -788,10 +789,20 @@ namespace spot
|
|||
}
|
||||
break;
|
||||
}
|
||||
|
||||
case op::X:
|
||||
// X(1) = 1, X(0) = 0
|
||||
if (f->is_tt() || f->is_ff())
|
||||
// X(1) = 1
|
||||
if (f->is_tt())
|
||||
return f;
|
||||
// We do not have X(0)=0 because that
|
||||
// is not true with finite semantics.
|
||||
assert(!f->is_eword());
|
||||
break;
|
||||
case op::strong_X:
|
||||
// X[!](0) = 0
|
||||
if (f->is_ff())
|
||||
return f;
|
||||
// Note: with finite semantics X[!](1)≠1.
|
||||
assert(!f->is_eword());
|
||||
break;
|
||||
|
||||
|
|
@ -1176,6 +1187,7 @@ namespace spot
|
|||
is_.accepting_eword = false;
|
||||
break;
|
||||
case op::X:
|
||||
case op::strong_X:
|
||||
props = children[0]->props;
|
||||
is_.not_marked = true;
|
||||
is_.boolean = false;
|
||||
|
|
@ -1186,6 +1198,10 @@ namespace spot
|
|||
// is_.syntactic_obligation inherited
|
||||
// is_.syntactic_recurrence inherited
|
||||
// is_.syntactic_persistence inherited
|
||||
|
||||
// is_.accepting_eword is currently unused outside SEREs, but
|
||||
// we could make sense of it if we start supporting LTL over
|
||||
// finite traces.
|
||||
is_.accepting_eword = false;
|
||||
break;
|
||||
case op::F:
|
||||
|
|
|
|||
|
|
@ -57,8 +57,22 @@
|
|||
#include <cstddef>
|
||||
#include <limits>
|
||||
|
||||
// The strong_X operator was introduced in Spot 2.8.2 to fix an issue
|
||||
// with from_ltlf(). As adding a new operator is a backward
|
||||
// incompatibility, causing new warnings from the compiler.
|
||||
#if defined(SPOT_BUILD) or defined(SPOT_USES_STRONG_X)
|
||||
// Use #if SPOT_HAS_STRONG_X in code that need to be backward
|
||||
// compatible with older Spot versions.
|
||||
# define SPOT_HAS_STRONG_X 1
|
||||
// You me #define SPOT_WANT_STRONG_X yourself before including
|
||||
// this file to force the use of STRONG_X
|
||||
# define SPOT_WANT_STRONG_X 1
|
||||
#endif
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
||||
|
||||
/// \ingroup tl_essentials
|
||||
/// \brief Operator types
|
||||
enum class op: uint8_t
|
||||
|
|
@ -98,6 +112,9 @@ namespace spot
|
|||
Star, ///< Star
|
||||
FStar, ///< Fustion Star
|
||||
first_match, ///< first_match(sere)
|
||||
#ifdef SPOT_WANT_STRONG_X
|
||||
strong_X, ///< strong Next
|
||||
#endif
|
||||
};
|
||||
|
||||
#ifndef SWIG
|
||||
|
|
@ -899,6 +916,22 @@ namespace spot
|
|||
return nested_unop_range(op::X, op::Or /* unused */, level, level, f);
|
||||
}
|
||||
|
||||
#if SPOT_WANT_STRONG_X
|
||||
/// \brief Construct a strong_X
|
||||
/// @{
|
||||
SPOT_DEF_UNOP(strong_X);
|
||||
/// @}
|
||||
|
||||
/// \brief Construct a strong_X[n]
|
||||
///
|
||||
/// strong_X[3]f = strong_X strong_X strong_X f
|
||||
static formula strong_X(unsigned level, const formula& f)
|
||||
{
|
||||
return nested_unop_range(op::strong_X, op::Or /* unused */,
|
||||
level, level, f);
|
||||
}
|
||||
#endif
|
||||
|
||||
/// \brief Construct an F
|
||||
/// @{
|
||||
SPOT_DEF_UNOP(F);
|
||||
|
|
@ -1662,6 +1695,9 @@ namespace spot
|
|||
return *this;
|
||||
case op::Not:
|
||||
case op::X:
|
||||
#if SPOT_HAS_STRONG_X
|
||||
case op::strong_X:
|
||||
#endif
|
||||
case op::F:
|
||||
case op::G:
|
||||
case op::Closure:
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2016, 2018 Laboratoire de Recherche et Développement
|
||||
// de l'Epita (LRDE).
|
||||
// Copyright (C) 2016, 2018, 2019 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
|
|
@ -29,11 +29,12 @@ namespace spot
|
|||
auto t = [&alive] (formula f) { return from_ltlf_aux(f, alive); };
|
||||
switch (auto o = f.kind())
|
||||
{
|
||||
case op::X:
|
||||
case op::strong_X:
|
||||
case op::F:
|
||||
return formula::unop(o, formula::And({alive, t(f[0])}));
|
||||
case op::X: // weak
|
||||
case op::G:
|
||||
return formula::G(formula::Or({formula::Not(alive), t(f[0])}));
|
||||
return formula::unop(o, formula::Or({formula::Not(alive), t(f[0])}));
|
||||
// Note that the t() function given in the proof of Theorem 1 of
|
||||
// the IJCAI'13 paper by De Giacomo & Vardi has a typo.
|
||||
// t(a U b) should be equal to t(a) U t(b & alive).
|
||||
|
|
|
|||
|
|
@ -42,6 +42,7 @@ namespace spot
|
|||
case op::ap:
|
||||
case op::Not:
|
||||
case op::X:
|
||||
case op::strong_X:
|
||||
case op::F:
|
||||
case op::G:
|
||||
case op::Closure:
|
||||
|
|
@ -109,6 +110,7 @@ namespace spot
|
|||
case op::ap:
|
||||
case op::Not:
|
||||
case op::X:
|
||||
case op::strong_X:
|
||||
case op::F:
|
||||
case op::G:
|
||||
case op::Closure:
|
||||
|
|
|
|||
|
|
@ -81,6 +81,7 @@ namespace spot
|
|||
return f;
|
||||
case op::Not:
|
||||
case op::X:
|
||||
case op::strong_X:
|
||||
case op::F:
|
||||
case op::G:
|
||||
case op::first_match:
|
||||
|
|
|
|||
|
|
@ -72,6 +72,7 @@ namespace spot
|
|||
KEqualBunop,
|
||||
KGotoBunop,
|
||||
KFirstMatch,
|
||||
KStrongX,
|
||||
};
|
||||
|
||||
const char* spot_kw[] = {
|
||||
|
|
@ -112,6 +113,7 @@ namespace spot
|
|||
"[=",
|
||||
"[->",
|
||||
"first_match",
|
||||
"X[!]",
|
||||
};
|
||||
|
||||
const char* spin_kw[] = {
|
||||
|
|
@ -152,6 +154,7 @@ namespace spot
|
|||
"[=", // not supported
|
||||
"[->", // not supported
|
||||
"first_match", // not supported
|
||||
"!X!",
|
||||
};
|
||||
|
||||
const char* wring_kw[] = {
|
||||
|
|
@ -192,6 +195,7 @@ namespace spot
|
|||
"[=", // not supported
|
||||
"[->", // not supported
|
||||
"first_match", // not supported
|
||||
"X[!]", // not supported, FIXME: we need a syntax
|
||||
};
|
||||
|
||||
const char* utf8_kw[] = {
|
||||
|
|
@ -232,6 +236,7 @@ namespace spot
|
|||
"[=",
|
||||
"[->",
|
||||
"first_match",
|
||||
"Ⓧ",
|
||||
};
|
||||
|
||||
const char* latex_kw[] = {
|
||||
|
|
@ -272,6 +277,7 @@ namespace spot
|
|||
"\\SereEqual{",
|
||||
"\\SereGoto{",
|
||||
"\\FirstMatch",
|
||||
"\\StrongX",
|
||||
};
|
||||
|
||||
const char* sclatex_kw[] = {
|
||||
|
|
@ -316,6 +322,7 @@ namespace spot
|
|||
"^{=",
|
||||
"^{\\to",
|
||||
"\\mathsf{first\\_match}",
|
||||
"\\textcircled{\\mathsf{X}}",
|
||||
};
|
||||
|
||||
static bool
|
||||
|
|
@ -519,7 +526,18 @@ namespace spot
|
|||
break;
|
||||
}
|
||||
case op::X:
|
||||
{
|
||||
emit(KX);
|
||||
bool cst = f[0].is_constant();
|
||||
if (cst)
|
||||
openp();
|
||||
visit(f[0]);
|
||||
if (cst)
|
||||
closep();
|
||||
break;
|
||||
}
|
||||
case op::strong_X:
|
||||
emit(KStrongX);
|
||||
visit(f[0]);
|
||||
break;
|
||||
case op::F:
|
||||
|
|
@ -1076,6 +1094,9 @@ namespace spot
|
|||
case op::X:
|
||||
os_ << 'X';
|
||||
break;
|
||||
case op::strong_X:
|
||||
os_ << 'X'; // unsupported
|
||||
break;
|
||||
case op::F:
|
||||
os_ << 'F';
|
||||
break;
|
||||
|
|
|
|||
|
|
@ -489,7 +489,13 @@ namespace spot
|
|||
result = negated ? formula::Not(f) : f;
|
||||
break;
|
||||
case op::X:
|
||||
case op::strong_X:
|
||||
// Currently we don't distinguish between weak and
|
||||
// strong semantics, so we treat the two operators
|
||||
// identically.
|
||||
//
|
||||
// !Xa == X!a
|
||||
// !X[!]a = X!a
|
||||
result = formula::X(rec(f[0], negated));
|
||||
break;
|
||||
case op::F:
|
||||
|
|
@ -714,7 +720,10 @@ namespace spot
|
|||
formula
|
||||
unop_multop(op uop, op mop, vec v)
|
||||
{
|
||||
return formula::unop(uop, formula::multop(mop, v));
|
||||
formula f = formula::unop(uop, formula::multop(mop, v));
|
||||
if (f.is(op::X) && f[0].is_ff())
|
||||
return formula::ff();
|
||||
return f;
|
||||
}
|
||||
|
||||
formula
|
||||
|
|
@ -797,6 +806,7 @@ namespace spot
|
|||
switch (f.kind())
|
||||
{
|
||||
case op::X:
|
||||
case op::strong_X:
|
||||
if (res_X && !eu)
|
||||
{
|
||||
res_X->emplace_back(f[0]);
|
||||
|
|
@ -950,8 +960,15 @@ namespace spot
|
|||
case op::FStar:
|
||||
return f;
|
||||
case op::X:
|
||||
case op::strong_X:
|
||||
{
|
||||
formula c = f[0];
|
||||
// The following rules are not trivial simplifications,
|
||||
// because they are not true in LTLf.
|
||||
// X(0)=0
|
||||
// X[!](1)=1
|
||||
if (c.is_constant())
|
||||
return c;
|
||||
// Xf = f if f is both eventual and universal.
|
||||
if (c.is_universal() && c.is_eventual())
|
||||
{
|
||||
|
|
@ -3731,9 +3748,10 @@ namespace spot
|
|||
switch (f.kind())
|
||||
{
|
||||
case op::X:
|
||||
case op::strong_X:
|
||||
if (g.is_eventual() && syntactic_implication(f[0], g))
|
||||
return true;
|
||||
if (g.is(op::X) && syntactic_implication(f[0], g[0]))
|
||||
if (g.is(op::X, op::strong_X) && syntactic_implication(f[0], g[0]))
|
||||
return true;
|
||||
break;
|
||||
|
||||
|
|
@ -3893,6 +3911,7 @@ namespace spot
|
|||
|
||||
case op::G:
|
||||
case op::X:
|
||||
case op::strong_X:
|
||||
if (f.is_universal() && syntactic_implication(f, g[0]))
|
||||
return true;
|
||||
break;
|
||||
|
|
|
|||
|
|
@ -103,6 +103,7 @@ namespace spot
|
|||
case op::ap:
|
||||
case op::Not:
|
||||
case op::X:
|
||||
case op::strong_X:
|
||||
case op::F:
|
||||
case op::G:
|
||||
case op::Closure:
|
||||
|
|
|
|||
|
|
@ -97,6 +97,7 @@ namespace spot
|
|||
case op::ap:
|
||||
case op::Not:
|
||||
case op::X:
|
||||
case op::strong_X:
|
||||
case op::Closure:
|
||||
case op::NegClosure:
|
||||
case op::NegClosureMarked:
|
||||
|
|
|
|||
|
|
@ -84,6 +84,7 @@ namespace spot
|
|||
case op::F:
|
||||
case op::G:
|
||||
case op::X:
|
||||
case op::strong_X:
|
||||
case op::Closure:
|
||||
case op::NegClosure:
|
||||
case op::NegClosureMarked:
|
||||
|
|
|
|||
|
|
@ -81,6 +81,7 @@ namespace spot
|
|||
return;
|
||||
}
|
||||
case op::X:
|
||||
case op::strong_X:
|
||||
{
|
||||
ltl2taa_visitor v = recurse(f[0]);
|
||||
std::vector<formula> dst;
|
||||
|
|
|
|||
|
|
@ -585,6 +585,7 @@ namespace spot
|
|||
case op::F:
|
||||
case op::G:
|
||||
case op::X:
|
||||
case op::strong_X:
|
||||
case op::Closure:
|
||||
case op::NegClosure:
|
||||
case op::NegClosureMarked:
|
||||
|
|
@ -1215,6 +1216,7 @@ namespace spot
|
|||
return bdd_not(recurse(node[0]));
|
||||
}
|
||||
case op::X:
|
||||
case op::strong_X:
|
||||
{
|
||||
// r(Xy) = Next[y]
|
||||
// r(X(a&b&c)) = Next[a]&Next[b]&Next[c]
|
||||
|
|
|
|||
|
|
@ -48,6 +48,8 @@ G(a & Xb)
|
|||
Xa
|
||||
F(a & !Xa & Xb)
|
||||
{a & {b|c} }
|
||||
((a && b) U (! (X 1)))
|
||||
((a && b) U (! (X[!] 1)))
|
||||
|
||||
{a[=2:3]}|->b
|
||||
{a[->2:3]}|->b
|
||||
|
|
@ -63,6 +65,7 @@ EOF
|
|||
|
||||
checkopt --boolean <<EOF
|
||||
a & (b | c)
|
||||
0
|
||||
EOF
|
||||
|
||||
checkopt --bsize-min=2 --bsize-max=4 <<EOF
|
||||
|
|
@ -81,6 +84,8 @@ F(GFa | Gb)
|
|||
F(b W GFa)
|
||||
a U Fb
|
||||
F(a & !Xa & Xb)
|
||||
0
|
||||
(a & b) U !X[!]1
|
||||
EOF
|
||||
|
||||
checkopt --universal <<EOF
|
||||
|
|
@ -88,16 +93,19 @@ GFa | FGb
|
|||
F(GFa | Gb)
|
||||
GFa | Gb
|
||||
G(a & Xb)
|
||||
0
|
||||
EOF
|
||||
|
||||
checkopt --eventual --universal <<EOF
|
||||
GFa | FGb
|
||||
F(GFa | Gb)
|
||||
0
|
||||
EOF
|
||||
|
||||
checkopt --suspendable <<EOF
|
||||
GFa | FGb
|
||||
F(GFa | Gb)
|
||||
0
|
||||
EOF
|
||||
|
||||
checkopt --stutter-invariant <<EOF
|
||||
|
|
@ -110,6 +118,8 @@ b W GFa
|
|||
a U Fb
|
||||
F(a & !Xa & Xb)
|
||||
a & (b | c)
|
||||
0
|
||||
(a & b) U !X[!]1
|
||||
{{!a}[*];a[+]}[]-> b
|
||||
{a[*];{!a}[*];a[*]}[]-> b
|
||||
{a[*];{!a}[+];a[*]}[]-> b
|
||||
|
|
@ -120,7 +130,7 @@ a & (b | c)
|
|||
EOF
|
||||
|
||||
checkopt -c --stutter-invariant <<EOF
|
||||
16
|
||||
18
|
||||
EOF
|
||||
|
||||
checkopt --syntactic-stutter-invariant <<EOF
|
||||
|
|
@ -131,6 +141,7 @@ GFa | Gb
|
|||
b W GFa
|
||||
a U Fb
|
||||
a & (b | c)
|
||||
0
|
||||
{{!a}[*];a[+]}[]-> b
|
||||
{a[*];{!a}[*];a[*]}[]-> b
|
||||
{a[*];{!a}[+];a[*]}[]-> b
|
||||
|
|
@ -152,6 +163,8 @@ G(a & Xb)
|
|||
Xa
|
||||
F(a & X(!a & b))
|
||||
a & (b | c)
|
||||
0
|
||||
0
|
||||
a R (!a | X({a[->1..2]}[]-> (b & X(b W a))))
|
||||
a R (!a | X({a[->1..2]}[]-> b))
|
||||
a R (b W !a)
|
||||
|
|
@ -169,6 +182,7 @@ F(GFa | Gb)
|
|||
F(b W GFa)
|
||||
Fb
|
||||
F(a & X(!a & b))
|
||||
0
|
||||
EOF
|
||||
|
||||
checkopt --liveness <<EOF
|
||||
|
|
@ -186,6 +200,8 @@ checkopt --safety <<EOF
|
|||
G(a & Xb)
|
||||
Xa
|
||||
a & (b | c)
|
||||
0
|
||||
(a & b) U !X[!]1
|
||||
{a[=2..3]}[]-> b
|
||||
{a[->2..3]}[]-> b
|
||||
{{!a}[*];a[+]}[]-> b
|
||||
|
|
@ -206,6 +222,8 @@ G(a & Xb)
|
|||
Xa
|
||||
F(a & !Xa & Xb)
|
||||
a & (b | c)
|
||||
0
|
||||
(a & b) U !X[!]1
|
||||
{a[=2..3]}[]-> b
|
||||
{a[->2..3]}[]-> b
|
||||
{{!a}[*];a[+]}[]-> b
|
||||
|
|
@ -224,6 +242,8 @@ a U Fb
|
|||
Xa
|
||||
F(a & !Xa & Xb)
|
||||
a & (b | c)
|
||||
0
|
||||
(a & b) U !X[!]1
|
||||
EOF
|
||||
|
||||
checkopt -v --ltl <<EOF
|
||||
|
|
@ -251,6 +271,8 @@ a U Fb
|
|||
G(a & Xb)
|
||||
Xa
|
||||
F(a & !Xa & Xb)
|
||||
0
|
||||
(a & b) U !X[!]1
|
||||
{a[=2..3]}[]-> b
|
||||
{a[->2..3]}[]-> b
|
||||
{{!a}[*];a[+]}[]-> b
|
||||
|
|
@ -273,6 +295,7 @@ a U Fb
|
|||
G(a & Xb)
|
||||
F(a & !Xa & Xb)
|
||||
a & (b | c)
|
||||
(a & b) U !X[!]1
|
||||
{a[=2..3]}[]-> b
|
||||
{a[->2..3]}[]-> b
|
||||
{{!a}[*];a[+]}[]-> b
|
||||
|
|
@ -300,10 +323,6 @@ F(GFa | Gb)
|
|||
F(b W GFa)
|
||||
EOF
|
||||
|
||||
# Restrict to LTL
|
||||
run 0 ltlfilt --ltl formulas > formulas2
|
||||
mv formulas2 formulas
|
||||
|
||||
checkopt --ltl --from-ltlf=al <<EOF
|
||||
al & (G(!al | F(a & al)) | F(al & G(!al | b))) & (al U G!al)
|
||||
al & F(al & (G(!al | F(a & al)) | G(!al | b))) & (al U G!al)
|
||||
|
|
@ -311,10 +330,12 @@ al & F(al & ((!al | b) W G(!al | F(a & al)))) & (al U G!al)
|
|||
al & (G(!al | F(a & al)) | G(!al | b)) & (al U G!al)
|
||||
al & ((!al | b) W G(!al | F(a & al))) & (al U G!al)
|
||||
al & (a U (al & F(al & b))) & (al U G!al)
|
||||
al & G(!al | (a & X(al & b))) & (al U G!al)
|
||||
al & X(a & al) & (al U G!al)
|
||||
al & F(a & al & !X(a & al) & X(al & b)) & (al U G!al)
|
||||
al & G(!al | (a & X(!al | b))) & (al U G!al)
|
||||
al & X(a | !al) & (al U G!al)
|
||||
al & F(a & al & !X(a | !al) & X(!al | b)) & (al U G!al)
|
||||
a & al & (b | c) & (al U G!al)
|
||||
0
|
||||
al & ((a & b) U (al & !X[!]al)) & (al U G!al)
|
||||
EOF
|
||||
|
||||
checkopt --ltl --from-ltlf='!dead' <<EOF
|
||||
|
|
@ -324,10 +345,12 @@ checkopt --ltl --from-ltlf='!dead' <<EOF
|
|||
!dead & (G(dead | F(a & !dead)) | G(b | dead)) & (!dead U Gdead)
|
||||
!dead & ((b | dead) W G(dead | F(a & !dead))) & (!dead U Gdead)
|
||||
!dead & (a U (!dead & F(b & !dead))) & (!dead U Gdead)
|
||||
!dead & G(dead | (a & X(b & !dead))) & (!dead U Gdead)
|
||||
!dead & X(a & !dead) & (!dead U Gdead)
|
||||
!dead & F(a & !dead & !X(a & !dead) & X(b & !dead)) & (!dead U Gdead)
|
||||
!dead & G(dead | (a & X(b | dead))) & (!dead U Gdead)
|
||||
!dead & X(a | dead) & (!dead U Gdead)
|
||||
!dead & F(a & !dead & !X(a | dead) & X(b | dead)) & (!dead U Gdead)
|
||||
a & !dead & (b | c) & (!dead U Gdead)
|
||||
0
|
||||
!dead & ((a & b) U (!dead & !X[!]!dead)) & (!dead U Gdead)
|
||||
EOF
|
||||
|
||||
cat >in <<EOF
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
|
||||
# Copyright (C) 2014, 2015, 2019 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
|
|
@ -52,6 +52,7 @@ p1 U (p4 | (p3 xor (p4 W p0)))
|
|||
1 U (p4 | (p3 xor (p4 W p0)))
|
||||
Xp1 U (p4 | !(p4 W p0))
|
||||
Xp1 W (p4 | (p3 xor (p4 W p0)))
|
||||
X(0) U (p4 | (p3 xor (p4 W p0)))
|
||||
Xp1 U (p4 | (p3 xor (p4 W 0)))
|
||||
Xp4 U (p4 | (p3 xor (p4 W p0)))
|
||||
Xp3 U (p4 | (p3 xor (p4 W p0)))
|
||||
|
|
@ -74,10 +75,10 @@ Xp4 R p3
|
|||
p3 W !p0
|
||||
Xp4 W !p0
|
||||
(p4 R p3) W !p0
|
||||
(0 R p3) W !p0
|
||||
(Xp4 R p3) W p0
|
||||
(Xp4 R p3) W 0
|
||||
(p3 W Xp4) W !p0
|
||||
(X(0) R p3) W !p0
|
||||
(Xp3 R p3) W !p0
|
||||
(Xp0 R p3) W !p0
|
||||
(Xp4 R p4) W !p0
|
||||
|
|
@ -180,11 +181,11 @@ F!{{p2;p0}[:*]}
|
|||
{{p2;p0}[:*]}[]-> Xp0
|
||||
F({p2;p0}[]-> Xp0)
|
||||
F({{p2;p0}[:*]}[]-> p0)
|
||||
F({{p2;p0}[:*]}[]-> 0)
|
||||
F({p0[*2][:*]}[]-> Xp0)
|
||||
F({p2[*2][:*]}[]-> Xp2)
|
||||
F({{1;p0}[:*]}[]-> Xp0)
|
||||
F({{p2;1}[:*]}[]-> Xp0)
|
||||
F({{p2;p0}[:*]}[]-> X(0))
|
||||
EOF
|
||||
|
||||
echo '1,a,3' > input
|
||||
|
|
|
|||
|
|
@ -114,17 +114,19 @@ grep -q p2 out
|
|||
grep p3 out && exit 1
|
||||
|
||||
|
||||
# We should be able to generate exactly two formulas with 0 atomic
|
||||
# propositions.
|
||||
run 0 randltl -n2 0 | sort > out
|
||||
# We should be able to generate exactly three formulas with 0 atomic
|
||||
# propositions and at most 2 nodes.
|
||||
run 0 randltl -n3 --tree-size=..2 0 > out
|
||||
sort <out >out2
|
||||
cat >expected <<EOF
|
||||
0
|
||||
1
|
||||
X(0)
|
||||
EOF
|
||||
diff out expected
|
||||
diff out2 expected
|
||||
|
||||
# requesting more formulas should fail
|
||||
run 2 randltl -n3 0
|
||||
run 2 randltl -n4 --tree-size=..2 0
|
||||
|
||||
# If more numbers are given, there are interpreted as atomic propositions
|
||||
run 0 randltl -n1000 0 1 > out
|
||||
|
|
|
|||
|
|
@ -24,19 +24,24 @@
|
|||
|
||||
set -e
|
||||
|
||||
cat >ok.in <<EOF
|
||||
cat >ok.in <<\EOF
|
||||
X[4]a
|
||||
X[3!]a
|
||||
G[2:4]a
|
||||
G[4:2]a
|
||||
F[2:4]a
|
||||
F[4:2]a
|
||||
F[2:$]a
|
||||
F[2..]a
|
||||
F[2:$!]a
|
||||
F[2:3!]a
|
||||
X [4]a | b
|
||||
G [2:4] a | b
|
||||
G [4:2] a | b
|
||||
G [2:] a | b
|
||||
G [2..] a | b
|
||||
G [2..!] a | b
|
||||
G [2..3!] a | b
|
||||
F [2:4] a | b
|
||||
F [4:2]a | F[2:2]b
|
||||
F[]a|G[]b|X[]c
|
||||
|
|
@ -59,19 +64,24 @@ EOF
|
|||
|
||||
ltlfilt -F ok.in > ok.out
|
||||
|
||||
cat >expect <<EOF
|
||||
cat >expect <<\EOF
|
||||
XXXXa
|
||||
X[!]X[!]X[!]a
|
||||
XX(a & X(a & Xa))
|
||||
XX(a & X(a & Xa))
|
||||
XX(a | X(a | Xa))
|
||||
XX(a | X(a | Xa))
|
||||
XXFa
|
||||
XXFa
|
||||
X[!]X[!]Fa
|
||||
X[!]X[!](a | X[!]a)
|
||||
b | XXXXa
|
||||
b | XX(a & X(a & Xa))
|
||||
b | XX(a & X(a & Xa))
|
||||
b | XXGa
|
||||
b | XXGa
|
||||
b | X[!]X[!]Ga
|
||||
b | X[!]X[!](a & X[!]a)
|
||||
b | XX(a | X(a | Xa))
|
||||
XX(a | X(a | Xa)) | XXb
|
||||
FGa | Gb | XGc
|
||||
|
|
@ -99,14 +109,19 @@ cat >err.in <<EOF
|
|||
F[
|
||||
F[3:1]
|
||||
F[3:1][2:1]
|
||||
F[2]a
|
||||
F[2!]a
|
||||
F[a
|
||||
G[2:4]
|
||||
G[2:.]a
|
||||
G[4]a
|
||||
G[4!]a
|
||||
G[a
|
||||
X[2
|
||||
X[2]
|
||||
X[2:3]
|
||||
X[2:4]a
|
||||
X[2:4!]a
|
||||
X[a
|
||||
{a ## b}
|
||||
{a ##7}
|
||||
|
|
@ -122,6 +137,7 @@ numoreof="$num or end of formula"
|
|||
sep="separator for square bracket operator"
|
||||
undefined='$undefined'
|
||||
closingbkt='square bracket operator, expecting closing bracket'
|
||||
eclosingbkt='expecting closing bracket or closing !]'
|
||||
|
||||
ltlfilt -F err.in 2>err && exit 1
|
||||
cat >expect2 <<EOF
|
||||
|
|
@ -153,6 +169,16 @@ missing right operand for "F[.] operator"
|
|||
ignoring trailing garbage
|
||||
|
||||
ltlfilt:err.in:4: parse error:
|
||||
>>> F[2]a
|
||||
^^^^
|
||||
F[n:m] expects two parameters
|
||||
|
||||
ltlfilt:err.in:5: parse error:
|
||||
>>> F[2!]a
|
||||
^^^^^
|
||||
F[n:m!] expects two parameters
|
||||
|
||||
ltlfilt:err.in:6: parse error:
|
||||
>>> F[a
|
||||
^
|
||||
syntax error, unexpected $undefined, expecting $numoreof
|
||||
|
|
@ -161,7 +187,7 @@ syntax error, unexpected $undefined, expecting $numoreof
|
|||
^^^
|
||||
missing closing bracket for F[.]
|
||||
|
||||
ltlfilt:err.in:5: parse error:
|
||||
ltlfilt:err.in:7: parse error:
|
||||
>>> G[2:4]
|
||||
^
|
||||
syntax error, unexpected end of formula
|
||||
|
|
@ -170,21 +196,26 @@ syntax error, unexpected end of formula
|
|||
^^^^^^
|
||||
missing right operand for "G[.] operator"
|
||||
|
||||
ltlfilt:err.in:6: parse error:
|
||||
ltlfilt:err.in:8: parse error:
|
||||
>>> G[2:.]a
|
||||
^
|
||||
syntax error, unexpected $undefined, expecting closing bracket
|
||||
syntax error, unexpected $undefined, $eclosingbkt
|
||||
|
||||
>>> G[2:.]a
|
||||
^^^^^^
|
||||
treating this G[.] as a simple G
|
||||
|
||||
ltlfilt:err.in:7: parse error:
|
||||
ltlfilt:err.in:9: parse error:
|
||||
>>> G[4]a
|
||||
^^^^
|
||||
G[n:m] expects two parameters
|
||||
|
||||
ltlfilt:err.in:8: parse error:
|
||||
ltlfilt:err.in:10: parse error:
|
||||
>>> G[4!]a
|
||||
^^^^^
|
||||
G[n:m!] expects two parameters
|
||||
|
||||
ltlfilt:err.in:11: parse error:
|
||||
>>> G[a
|
||||
^
|
||||
syntax error, unexpected $undefined, expecting $numoreof
|
||||
|
|
@ -193,16 +224,16 @@ syntax error, unexpected $undefined, expecting $numoreof
|
|||
^^^
|
||||
missing closing bracket for G[.]
|
||||
|
||||
ltlfilt:err.in:9: parse error:
|
||||
ltlfilt:err.in:12: parse error:
|
||||
>>> X[2
|
||||
^
|
||||
syntax error, unexpected end of formula, expecting closing bracket
|
||||
syntax error, unexpected end of formula, $eclosingbkt
|
||||
|
||||
>>> X[2
|
||||
^^^
|
||||
missing closing bracket for X[.]
|
||||
|
||||
ltlfilt:err.in:10: parse error:
|
||||
ltlfilt:err.in:13: parse error:
|
||||
>>> X[2]
|
||||
^
|
||||
syntax error, unexpected end of formula
|
||||
|
|
@ -211,25 +242,43 @@ syntax error, unexpected end of formula
|
|||
^^^^
|
||||
missing right operand for "X[.] operator"
|
||||
|
||||
ltlfilt:err.in:11: parse error:
|
||||
ltlfilt:err.in:14: parse error:
|
||||
>>> X[2:3]
|
||||
^
|
||||
syntax error, unexpected separator for square bracket operator, $eclosingbkt
|
||||
|
||||
>>> X[2:3]
|
||||
^^^^^^
|
||||
missing closing bracket for X[.]
|
||||
|
||||
ltlfilt:err.in:15: parse error:
|
||||
>>> X[2:4]a
|
||||
^
|
||||
syntax error, unexpected $sep, expecting closing bracket
|
||||
syntax error, unexpected $sep, $eclosingbkt
|
||||
|
||||
>>> X[2:4]a
|
||||
^^^^^^^
|
||||
treating this X[.] as a simple X
|
||||
|
||||
ltlfilt:err.in:12: parse error:
|
||||
ltlfilt:err.in:16: parse error:
|
||||
>>> X[2:4!]a
|
||||
^
|
||||
syntax error, unexpected separator for square bracket operator, $eclosingbkt
|
||||
|
||||
>>> X[2:4!]a
|
||||
^^^^^^^^
|
||||
treating this X[.!] as a simple X[!]
|
||||
|
||||
ltlfilt:err.in:17: parse error:
|
||||
>>> X[a
|
||||
^
|
||||
syntax error, unexpected $undefined, expecting $numoreof
|
||||
syntax error, unexpected $undefined, expecting closing !] or $numoreof
|
||||
|
||||
>>> X[a
|
||||
^^^
|
||||
missing closing bracket for X[.]
|
||||
|
||||
ltlfilt:err.in:13: parse error:
|
||||
ltlfilt:err.in:18: parse error:
|
||||
>>> {a ## b}
|
||||
^
|
||||
syntax error, unexpected $undefined
|
||||
|
|
@ -238,7 +287,7 @@ syntax error, unexpected $undefined
|
|||
^^^^
|
||||
ignoring this
|
||||
|
||||
ltlfilt:err.in:14: parse error:
|
||||
ltlfilt:err.in:19: parse error:
|
||||
>>> {a ##7}
|
||||
^
|
||||
syntax error, unexpected closing brace
|
||||
|
|
@ -247,7 +296,7 @@ syntax error, unexpected closing brace
|
|||
^^^
|
||||
missing right operand for "SVA delay operator"
|
||||
|
||||
ltlfilt:err.in:15: parse error:
|
||||
ltlfilt:err.in:20: parse error:
|
||||
>>> {a ##[::] b}
|
||||
^
|
||||
syntax error, unexpected separator for $closingbkt
|
||||
|
|
@ -256,12 +305,12 @@ syntax error, unexpected separator for $closingbkt
|
|||
^^^^^^
|
||||
treating this delay block as ##1
|
||||
|
||||
ltlfilt:err.in:16: parse error:
|
||||
ltlfilt:err.in:21: parse error:
|
||||
>>> {a ##[2:1] b}
|
||||
^
|
||||
reversed range
|
||||
|
||||
ltlfilt:err.in:17: parse error:
|
||||
ltlfilt:err.in:22: parse error:
|
||||
>>> {a ##[1:2]}
|
||||
^
|
||||
syntax error, unexpected closing brace
|
||||
|
|
@ -270,7 +319,7 @@ syntax error, unexpected closing brace
|
|||
^^^^^^^
|
||||
missing right operand for "SVA delay operator"
|
||||
|
||||
ltlfilt:err.in:18: parse error:
|
||||
ltlfilt:err.in:23: parse error:
|
||||
>>> {##[1:2]}
|
||||
^
|
||||
syntax error, unexpected closing brace
|
||||
|
|
@ -280,4 +329,4 @@ syntax error, unexpected closing brace
|
|||
missing right operand for "SVA delay operator"
|
||||
|
||||
EOF
|
||||
diff err expect2
|
||||
diff -u err expect2
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2012, 2013, 2015, 2016 Laboratoire de Recherche et
|
||||
# Copyright (C) 2012, 2013, 2015, 2016, 2019 Laboratoire de Recherche et
|
||||
# Développement de l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
|
|
@ -64,3 +64,9 @@ diff expected output
|
|||
|
||||
randltl --psl -8 --seed 0 --tree-size 16 a b c -n 100 > formulae
|
||||
../reduc -f -h 0 formulae
|
||||
|
||||
echo 'Ⓧa' >in
|
||||
ltlfilt -8 -f 'X[!]a' >out
|
||||
diff in out
|
||||
ltlfilt -8 -F in >out
|
||||
diff in out
|
||||
|
|
|
|||
|
|
@ -587,21 +587,14 @@
|
|||
"X(p2 & X(p2 U (!p0 | !(1 U !p2))))\n",
|
||||
"(1 U p2) | (X(!p2 | !(1 U !p2)) U (1 U (!p1 & (1 U p2))))\n",
|
||||
"XX!(1 U !((X!p1 U (!p2 U (!p0 & !p2))) | X!(1 U !p0)))\n",
|
||||
"XX(1 U (p1 U ((p0 & p1) | !(1 U !p1))))\n",
|
||||
"p2 & Xp0\n"
|
||||
"0\n",
|
||||
"XX(1 U (p1 U ((p0 & p1) | !(1 U !p1))))\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"for formula in spot.randltl(3, 10).simplify().unabbreviate(\"WMGFR\"): print(formula)"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": []
|
||||
}
|
||||
],
|
||||
"metadata": {
|
||||
|
|
@ -620,7 +613,7 @@
|
|||
"name": "python",
|
||||
"nbconvert_exporter": "python",
|
||||
"pygments_lexer": "ipython3",
|
||||
"version": "3.7.3"
|
||||
"version": "3.7.4+"
|
||||
}
|
||||
},
|
||||
"nbformat": 4,
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue