From be389c5c2554513ba519ea854aa79712b5d4dd32 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 22 Sep 2019 21:15:55 +0200 Subject: [PATCH] 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. --- NEWS | 30 +++++++++++ THANKS | 1 + bin/ltlfilt.cc | 12 +++-- doc/tl/tl.tex | 80 +++++++++++++++++++---------- spot/parsetl/parsedecl.hh | 2 +- spot/parsetl/parsetl.yy | 65 +++++++++++++++++++++-- spot/parsetl/scantl.ll | 3 ++ spot/tl/dot.cc | 1 + spot/tl/formula.cc | 20 +++++++- spot/tl/formula.hh | 36 +++++++++++++ spot/tl/ltlf.cc | 9 ++-- spot/tl/mark.cc | 2 + spot/tl/mutation.cc | 1 + spot/tl/print.cc | 99 ++++++++++++++++++++++-------------- spot/tl/simplify.cc | 25 +++++++-- spot/tl/snf.cc | 1 + spot/tl/unabbrev.cc | 1 + spot/twa/formula2bdd.cc | 1 + spot/twaalgos/ltl2taa.cc | 1 + spot/twaalgos/ltl2tgba_fm.cc | 2 + tests/core/ltlfilt.test | 45 ++++++++++++---- tests/core/ltlgrind.test | 7 +-- tests/core/rand.test | 12 +++-- tests/core/sugar.test | 91 +++++++++++++++++++++++++-------- tests/core/utf8.test | 8 ++- tests/python/randltl.ipynb | 13 ++--- 26 files changed, 434 insertions(+), 134 deletions(-) diff --git a/NEWS b/NEWS index 7707c4312..a6d4370c1 100644 --- a/NEWS +++ b/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 diff --git a/THANKS b/THANKS index 8fb1916d6..a18ea92d0 100644 --- a/THANKS +++ b/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 diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index a5a872012..72ca8bc3e 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -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) - f = spot::from_ltlf(f, 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(); diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index d8b7d9d24..9ec2ac0df 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -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 & @@ -983,33 +1002,34 @@ operator, even if the operator has multiple synonyms (like \samp{|}, \samp{||}, and {`\verb=\/='}). \begin{align*} -\mathit{constant} ::={} & \0 \mid \1 \\ -\mathit{atomic\_prop} ::={} & \text{see secn~\ref{sec:ap}} \\[1ex] - \mathit{bformula} ::={} & \mathit{constant} & \mid{} & \tsamp{(}\,\mathit{bformula}\,\tsamp{)} & \mid{} & \mathit{bformula}\,\msamp{\XOR}\,\mathit{bformula} \\ - \mid{} & \mathit{atomic\_prop} & \mid{} & \msamp{\NOT}\,\mathit{bformula} & \mid{} & \mathit{bformula}\,\msamp{\EQUIV}\,\mathit{bformula} \\ - \mid{} & \mathit{atomic\_prop}\code{=0} & \mid{} & \mathit{bformula}\,\msamp{\AND}\,\mathit{bformula} & \mid{} & \mathit{bformula}\,\msamp{\IMPLIES}\,\mathit{bformula} \\ - \mid{} & \mathit{atomic\_prop}\code{=1} & \mid{} & \mathit{bformula}\,\msamp{\OR}\,\mathit{bformula} \\[1ex] -\mathit{sere} ::={} & \mathit{bformula} & \mid{} & \msamp{\STAR{\mvar{i}..\mvar{j}}} & \mid{} & \DELAY{\mvar{i}}\mathit{sere} \\ - \mid{} & \tsamp{\{}\,\mathit{sere}\,\tsamp{\}} & \mid{} & \msamp{\PLUS{}} & \mid{} & \DELAYR{\mvar{i}..\mvar{j}}\mathit{sere} \\ - \mid{} & \tsamp{(}\,\mathit{sere}\,\tsamp{)} & \mid{} & \mathit{sere}\msamp{\STAR{\mvar{i}..\mvar{j}}} & \mid{} & \mathit{sere}\DELAY{\mvar{i}}\mathit{sere} \\ - \mid{} & \mathit{sere}\msamp{\OR}\mathit{sere} & \mid{} & \mathit{sere}\msamp{\PLUS} & \mid{} & \mathit{sere}\DELAYR{\mvar{i}..\mvar{j}}\mathit{sere} \\ - \mid{} & \mathit{sere}\msamp{\AND}\mathit{sere} & \mid{} & \mathit{sere}\msamp{\FSTAR{\mvar{i}..\mvar{j}}} & \mid{} & \FIRSTMATCH\code(\,sere\,\code) \\ - \mid{} & \mathit{sere}\msamp{\ANDALT}\mathit{sere} & \mid{} & \mathit{sere}\msamp{\FPLUS} \\ - \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} \\ +\mathit{constant} ::={} & \0 \mid \1 \\ +\mathit{atomic\_prop} ::={} & \text{see secn~\ref{sec:ap}} \\[1ex] + \mathit{bformula} ::={} & \mathit{constant} & \mid{} & \tsamp{(}\,\mathit{bformula}\,\tsamp{)} & \mid{} & \mathit{bformula}\,\msamp{\XOR}\,\mathit{bformula} \\ + \mid{} & \mathit{atomic\_prop} & \mid{} & \msamp{\NOT}\,\mathit{bformula} & \mid{} & \mathit{bformula}\,\msamp{\EQUIV}\,\mathit{bformula} \\ + \mid{} & \mathit{atomic\_prop}\code{=0} & \mid{} & \mathit{bformula}\,\msamp{\AND}\,\mathit{bformula} & \mid{} & \mathit{bformula}\,\msamp{\IMPLIES}\,\mathit{bformula} \\ + \mid{} & \mathit{atomic\_prop}\code{=1} & \mid{} & \mathit{bformula}\,\msamp{\OR}\,\mathit{bformula} \\[1ex] +\mathit{sere} ::={} & \mathit{bformula} & \mid{} & \msamp{\STAR{\mvar{i}..\mvar{j}}} & \mid{} & \DELAY{\mvar{i}}\mathit{sere} \\ + \mid{} & \tsamp{\{}\,\mathit{sere}\,\tsamp{\}} & \mid{} & \msamp{\PLUS{}} & \mid{} & \DELAYR{\mvar{i}..\mvar{j}}\mathit{sere} \\ + \mid{} & \tsamp{(}\,\mathit{sere}\,\tsamp{)} & \mid{} & \mathit{sere}\msamp{\STAR{\mvar{i}..\mvar{j}}} & \mid{} & \mathit{sere}\DELAY{\mvar{i}}\mathit{sere} \\ + \mid{} & \mathit{sere}\msamp{\OR}\mathit{sere} & \mid{} & \mathit{sere}\msamp{\PLUS} & \mid{} & \mathit{sere}\DELAYR{\mvar{i}..\mvar{j}}\mathit{sere} \\ + \mid{} & \mathit{sere}\msamp{\AND}\mathit{sere} & \mid{} & \mathit{sere}\msamp{\FSTAR{\mvar{i}..\mvar{j}}} & \mid{} & \FIRSTMATCH\code(\,sere\,\code) \\ + \mid{} & \mathit{sere}\msamp{\ANDALT}\mathit{sere} & \mid{} & \mathit{sere}\msamp{\FPLUS} \\ + \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{\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 diff --git a/spot/parsetl/parsedecl.hh b/spot/parsetl/parsedecl.hh index 55e5efdc6..a8e764ec4 100644 --- a/spot/parsetl/parsedecl.hh +++ b/spot/parsetl/parsedecl.hh @@ -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 diff --git a/spot/parsetl/parsetl.yy b/spot/parsetl/parsetl.yy index cd577fca0..f3ea1164a 100644 --- a/spot/parsetl/parsetl.yy +++ b/spot/parsetl/parsetl.yy @@ -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 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(); } diff --git a/spot/parsetl/scantl.ll b/spot/parsetl/scantl.ll index 53d971a81..a105de21c 100644 --- a/spot/parsetl/scantl.ll +++ b/spot/parsetl/scantl.ll @@ -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; "]" BEGIN(0); return token::OP_SQBKT_CLOSE; +"!]" BEGIN(0); return token::OP_SQBKT_STRONG_CLOSE; [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; diff --git a/spot/tl/dot.cc b/spot/tl/dot.cc index 853a9f958..a67de5fab 100644 --- a/spot/tl/dot.cc +++ b/spot/tl/dot.cc @@ -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: diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc index c844a0d1f..9f06443f1 100644 --- a/spot/tl/formula.cc +++ b/spot/tl/formula.cc @@ -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: diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh index 4c4fb0007..882fa8c69 100644 --- a/spot/tl/formula.hh +++ b/spot/tl/formula.hh @@ -57,8 +57,22 @@ #include #include +// 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: diff --git a/spot/tl/ltlf.cc b/spot/tl/ltlf.cc index a6a61fe96..7a07a3b2b 100644 --- a/spot/tl/ltlf.cc +++ b/spot/tl/ltlf.cc @@ -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). diff --git a/spot/tl/mark.cc b/spot/tl/mark.cc index 1dc79ef13..fd022fb7e 100644 --- a/spot/tl/mark.cc +++ b/spot/tl/mark.cc @@ -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: diff --git a/spot/tl/mutation.cc b/spot/tl/mutation.cc index 76403fa09..bf447fc92 100644 --- a/spot/tl/mutation.cc +++ b/spot/tl/mutation.cc @@ -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: diff --git a/spot/tl/print.cc b/spot/tl/print.cc index 2cae78557..57c7f6a5f 100644 --- a/spot/tl/print.cc +++ b/spot/tl/print.cc @@ -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[] = { @@ -138,60 +140,62 @@ namespace spot " || ", " || ", " && ", - " && ", // not supported - " & ", // not supported - ";", // not supported - ":", // not supported - "{", // not supported - "}", // not supported - "]", // not supported - "[*", // not supported - "[+]", // not supported - "[:*", // not supported - "[:+]", // not supported - "[=", // not supported - "[->", // not supported - "first_match", // not supported + " && ", // not supported + " & ", // not supported + ";", // not supported + ":", // not supported + "{", // not supported + "}", // not supported + "]", // not supported + "[*", // not supported + "[+]", // not supported + "[:*", // not supported + "[:+]", // not supported + "[=", // not supported + "[->", // not supported + "first_match", // not supported + "!X!", }; const char* wring_kw[] = { "FALSE", "TRUE", - "[*0]", // not supported + "[*0]", // not supported " ^ ", " -> ", " <-> ", " U ", " R ", - " W ", // rewritten - " M ", // rewritten - "<>-> ", // not supported - "<>=> ", // not supported - "<>+> ", // not supported - "<>=+> ", // not supported - "[]-> ", // not supported - "[]=> ", // not supported + " W ", // rewritten + " M ", // rewritten + "<>-> ", // not supported + "<>=> ", // not supported + "<>+> ", // not supported + "<>=+> ", // not supported + "[]-> ", // not supported + "[]=> ", // not supported "!", "X", "F", "G", " + ", - " | ", // not supported + " | ", // not supported " * ", - " && ", // not supported - " & ", // not supported - ";", // not supported - ":", // not supported - "{", // not supported - "}", // not supported - "]", // not supported - "[*", // not supported - "[+]", // not supported - "[:*", // not supported - "[:+]", // not supported - "[=", // not supported - "[->", // not supported - "first_match", // not supported + " && ", // not supported + " & ", // not supported + ";", // not supported + ":", // not supported + "{", // not supported + "}", // not supported + "]", // not supported + "[*", // not supported + "[+]", // not supported + "[:*", // not supported + "[:+]", // not supported + "[=", // 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); + { + 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; diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc index 8fd449283..8b22dd601 100644 --- a/spot/tl/simplify.cc +++ b/spot/tl/simplify.cc @@ -489,7 +489,13 @@ namespace spot result = negated ? formula::Not(f) : f; break; case op::X: - // !Xa == X!a + 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; diff --git a/spot/tl/snf.cc b/spot/tl/snf.cc index 2ee40cdc3..941ac1b10 100644 --- a/spot/tl/snf.cc +++ b/spot/tl/snf.cc @@ -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: diff --git a/spot/tl/unabbrev.cc b/spot/tl/unabbrev.cc index e2e57d2a4..fba2aec8f 100644 --- a/spot/tl/unabbrev.cc +++ b/spot/tl/unabbrev.cc @@ -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: diff --git a/spot/twa/formula2bdd.cc b/spot/twa/formula2bdd.cc index 93368b8a4..7596c0759 100644 --- a/spot/twa/formula2bdd.cc +++ b/spot/twa/formula2bdd.cc @@ -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: diff --git a/spot/twaalgos/ltl2taa.cc b/spot/twaalgos/ltl2taa.cc index 565b4edba..5cf779c2e 100644 --- a/spot/twaalgos/ltl2taa.cc +++ b/spot/twaalgos/ltl2taa.cc @@ -81,6 +81,7 @@ namespace spot return; } case op::X: + case op::strong_X: { ltl2taa_visitor v = recurse(f[0]); std::vector dst; diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc index f1b40edd7..bb0b0901d 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/spot/twaalgos/ltl2tgba_fm.cc @@ -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] diff --git a/tests/core/ltlfilt.test b/tests/core/ltlfilt.test index 0eee2f479..dd8f85a65 100755 --- a/tests/core/ltlfilt.test +++ b/tests/core/ltlfilt.test @@ -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 < b {a[*];{!a}[*];a[*]}[]-> b {a[*];{!a}[+];a[*]}[]-> b @@ -120,7 +130,7 @@ a & (b | c) EOF checkopt -c --stutter-invariant < 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 < 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 < 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 <in < 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 diff --git a/tests/core/rand.test b/tests/core/rand.test index 63cecf6a4..fd901a737 100755 --- a/tests/core/rand.test +++ b/tests/core/rand.test @@ -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 out2 cat >expected < out diff --git a/tests/core/sugar.test b/tests/core/sugar.test index cbdf7ec84..de6d89f38 100755 --- a/tests/core/sugar.test +++ b/tests/core/sugar.test @@ -24,19 +24,24 @@ set -e -cat >ok.in <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 <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 <err && exit 1 cat >expect2 <>> 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 diff --git a/tests/core/utf8.test b/tests/core/utf8.test index 729d0872c..45ba950f5 100755 --- a/tests/core/utf8.test +++ b/tests/core/utf8.test @@ -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 diff --git a/tests/python/randltl.ipynb b/tests/python/randltl.ipynb index 5ba8dfc69..7209275ab 100644 --- a/tests/python/randltl.ipynb +++ b/tests/python/randltl.ipynb @@ -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,