diff --git a/NEWS b/NEWS index e6148b7ea..5690e4eae 100644 --- a/NEWS +++ b/NEWS @@ -46,6 +46,13 @@ New in spot 2.7.4.dev (not yet released) acceptance condition. The output can be alternating only if the input was alternating. + - SVA's first_match operator can now be used in SERE formulas and + that is supported by the ltl_to_tgba_fm() translation. See + doc/tl/tl.pdf for the semantics. *WARNING* Because this adds a + new operator, any code that switches over the spot::op type may + need a new case for op::first_match. Furthermore, the output of + "randltl --psl" will be different from previous releases. + - The parser for SERE learned to recognize the ##n and ##[i:j] operators from SVA. So {##2 a ##0 b[+] ##1 c ##2 e} is another way to write {[*2];a:b[+];c;1;e}, and {a ##[i:j] b} is parsed as diff --git a/doc/tl/tl.bib b/doc/tl/tl.bib index 2239cdfda..8a855f59b 100644 --- a/doc/tl/tl.bib +++ b/doc/tl/tl.bib @@ -216,6 +216,15 @@ publisher = {Springer-Verlag} } +@Book{ systemverilog.04.lrm, + title = {SystemVerilog 3.1a Language Reference Manual: + Accellera’s Extensions to Ver- ilog}, + publisher = {Accellera}, + year = {2004}, + month = may, + note = {\url{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.366.6206}} +} + @TechReport{ tauriainen.03.a83, author = {Heikki Tauriainen}, title = {On Translating Linear Temporal Logic into Alternating and diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 946ab538c..8c244814b 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -98,6 +98,7 @@ \newcommand{\GOTO}[1]{\texttt{[->#1]}} \newcommand{\PLUS}{\texttt{[+]}} \newcommand{\FPLUS}{\texttt{[:+]}} +\newcommand{\FIRSTMATCH}{\texttt{first\_match}} \newcommand{\eword}{\texttt{[*0]}} \newcommand{\Esuffix}{\texttt{<>->}} @@ -609,6 +610,7 @@ denote arbitrary SERE. & $f\FSTAR{\mvar{i}:}$ & $f\FSTAR{\mvar{i} to}$ & $f\FSTAR{\mvar{i},}$\\ + first match & $\mathclap{\FIRSTMATCH\code(f\code)}$ \\ \end{tabular} \end{center} @@ -679,7 +681,9 @@ $a$ is an atomic proposition. \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{cases}\\ + \sigma\VDash \FIRSTMATCH\code(f\code) & \iff + (\sigma\VDash f)\land (\nexists k<|\sigma|,\,\sigma^{0..k}\nVDash f) \end{align*}} Notes: @@ -713,6 +717,11 @@ operands are Boolean formulas. 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. +\item The $\FIRSTMATCH$ operator does not exist in PSL. It comes + from SystemVerilog Assertions (SVA)~\cite{systemverilog.04.lrm}. + One intuition behind $\FIRSTMATCH\code(f\code)$ is that the + DFA for $\FIRSTMATCH\code(f\code)$ can be obtained from the DFA + for $f$ by removing all transitions leaving accepting states. \end{itemize} \subsection{Syntactic Sugar} @@ -757,10 +766,11 @@ it for output. $b$ must be a Boolean formula. \end{align*} The following adds input support for the SVA concatenation (or delay) -operator. The simplest equivalence are that $f \DELAY{0} g$, -$f \DELAY{1} g$, $f \DELAY{2} g$ mean respectively $f \FUSION g$, -$f \CONCAT g$, and $f \CONCAT \1\CONCAT g$, but the delay can be a -range, and $f$ can be omitted. +operator~\cite{systemverilog.04.lrm}. The simplest equivalence are +that $f \DELAY{0} g$, $f \DELAY{1} g$, $f \DELAY{2} g$ mean +respectively $f \FUSION g$, $f \CONCAT g$, and +$f \CONCAT \1\CONCAT g$, but the delay can be a range, and $f$ can be +omitted. \begin{align*} f\DELAY{\mvar{i}} g &\equiv f\DELAYR{\mvar{i}..\mvar{i}} g & {}\DELAY{\mvar{i}} g &\equiv {}\DELAYR{\mvar{i}..\mvar{i}} g\\ @@ -790,8 +800,8 @@ $b_1$, $b_2$ are assumed to be Boolean formulas. \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\\ + f\FSTAR{0}&\equiv \1 & f\FSTAR{1}&\equiv f\text{~if~}\varepsilon\nVDash f\\ + \FIRSTMATCH\code(b\code) &\equiv b & \FIRSTMATCH\code(f\code) &\equiv \eword\text{~if~}\varepsilon\VDash f \end{align*} \noindent @@ -958,41 +968,49 @@ operator, even if the operator has multiple synonyms (like \samp{|}, \samp{||}, and {`\verb=\/='}). \begin{align*} -\mathit{constant} ::={}& \0 \mid \1 & \mathit{tformula} ::={}&\mathit{bformula}\\ -\mathit{atomic\_prop} ::={}& \text{see section~\ref{sec:ap}} & \mid{}&\tsamp{(}\,\mathit{tformula}\,\tsamp{)} \\ -\mathit{bformula} ::={}& \mathit{constant} & \mid{}&\msamp{\NOT}\,\mathit{tformula}\,\\ - \mid{}&\mathit{atomic\_prop} & \mid{}&\mathit{tformula}\,\msamp{\AND}\,\mathit{tformula} \\ - \mid{}&\mathit{atomic\_prop}\code{=0} & \mid{}&\mathit{tformula}\,\msamp{\OR}\,\mathit{tformula} \\ - \mid{}&\mathit{atomic\_prop}\code{=1} & \mid{}&\mathit{tformula}\,\msamp{\IMPLIES}\,\mathit{tformula} \\ - \mid{}&\tsamp{(}\,\mathit{bformula}\,\tsamp{)} & \mid{}&\mathit{tformula}\,\msamp{\XOR}\,\mathit{tformula} \\ - \mid{}&\msamp{\NOT}\,\mathit{bformula} & \mid{}&\mathit{tformula}\,\msamp{\EQUIV}\,\mathit{tformula} \\ - \mid{}&\mathit{bformula}\,\msamp{\AND}\,\mathit{bformula} & \mid{}&\msamp{\X}\,\mathit{tformula} \\ - \mid{}&\mathit{bformula}\,\msamp{\OR}\,\mathit{bformula} & \mid{}&\msamp{\XREP{\mvar{i}..\mvar{j}}}\,\mathit{tformula} \\ - \mid{}&\mathit{bformula}\,\msamp{\IMPLIES}\,\mathit{bformula} & \mid{}&\msamp{\F}\,\mathit{tformula}\\ - \mid{}&\mathit{bformula}\,\msamp{\XOR}\,\mathit{bformula} & \mid{}&\msamp{\FREP{\mvar{i}..\mvar{j}}}\,\mathit{tformula} \\ - \mid{}&\mathit{bformula}\,\msamp{\EQUIV}\,\mathit{bformula} & \mid{}&\msamp{\G}\,\mathit{tformula}\\ -\mathit{sere} ::={}&\mathit{bformula} & \mid{}&\msamp{\GREP{\mvar{i}..\mvar{j}}}\,\mathit{tformula} \\ - \mid{}&\tsamp{\{}\,\mathit{sere}\,\tsamp{\}} & \mid{}&\mathit{tformula}\,\msamp{\U}\,\mathit{tformula} \\ - \mid{}&\tsamp{(}\,\mathit{sere}\,\tsamp{)} & \mid{}&\mathit{tformula}\,\msamp{\W}\,\mathit{tformula} \\ - \mid{}&\mathit{sere}\msamp{\OR}\mathit{sere} & \mid{}&\mathit{tformula}\,\msamp{\R}\,\mathit{tformula} \\ - \mid{}&\mathit{sere}\msamp{\AND}\mathit{sere} & \mid{}&\mathit{tformula}\,\msamp{\M}\,\mathit{tformula} \\ - \mid{}&\mathit{sere}\msamp{\ANDALT}\mathit{sere} & \mid{}&\tsamp{\{}\mathit{sere}\tsamp{\}}\,\msamp{\Asuffix}\,\mathit{tformula}\\ - \mid{}&\mathit{sere}\msamp{\CONCAT}\mathit{sere} & \mid{}&\tsamp{\{}\mathit{sere}\tsamp{\}}\,\msamp{\AsuffixEQ}\,\mathit{tformula}\\ - \mid{}&\mathit{sere}\msamp{\FUSION}\mathit{sere} & \mid{}&\tsamp{\{}\mathit{sere}\tsamp{\}}\,\msamp{\Esuffix}\,\mathit{tformula}\\ - \mid{}&\msamp{\STAR{\mvar{i}..\mvar{j}}} & \mid{}&\tsamp{\{}\mathit{sere}\tsamp{\}}\,\msamp{\EsuffixEQ}\,\mathit{tformula} \\ - \mid{}&\msamp{\PLUS{}} & \mid{}&\tsamp{\{}\mathit{sere}\tsamp{\}} \\ - \mid{}&\mathit{sere}\msamp{\STAR{\mvar{i}..\mvar{j}}} & \mid{}&\tsamp{\{}\mathit{sere}\tsamp{\}}\msamp{\NOT} \\ - \mid{}&\mathit{sere}\msamp{\PLUS} \\ - \mid{}&\mathit{sere}\msamp{\FSTAR{\mvar{i}..\mvar{j}}} \\ - \mid{}&\mathit{sere}\msamp{\FPLUS} \\ - \mid{}&\mathit{sere}\msamp{\EQUAL{\mvar{i}..\mvar{j}}} \\ - \mid{}&\mathit{sere}\msamp{\GOTO{\mvar{i}..\mvar{j}}} \\ - \mid{}&\DELAY{\mvar{i}}\mathit{sere} \\ - \mid{}&\DELAYR{\mvar{i}..\mvar{j}}\mathit{sere} \\ - \mid{}&\mathit{sere}\DELAY{\mvar{i}}\mathit{sere} \\ - \mid{}&\mathit{sere}\DELAYR{\mvar{i}..\mvar{j}}\mathit{sere} \\ +\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} \\ \end{align*} + + + + + + + + + + + + + + + + + \section{Operator precedence} The following operator precedence describes the current parser of diff --git a/spot/parsetl/parsetl.yy b/spot/parsetl/parsetl.yy index 3a19b2e6a..7f353c31c 100644 --- a/spot/parsetl/parsetl.yy +++ b/spot/parsetl/parsetl.yy @@ -224,6 +224,7 @@ using namespace spot; %token OP_ECONCAT "existential concat operator" %token OP_UCONCAT_NONO "universal non-overlapping concat operator" %token OP_ECONCAT_NONO "existential non-overlapping concat operator" +%token OP_FIRST_MATCH "first_match" %token ATOMIC_PROP "atomic proposition" %token OP_CONCAT "concat operator" OP_FUSION "fusion operator" %token CONST_TRUE "constant true" CONST_FALSE "constant false" @@ -678,6 +679,8 @@ sere: booleanatom } | sere OP_EQUIV error { missing_right_binop($$, $1, @2, "equivalent operator"); } + | OP_FIRST_MATCH PAR_OPEN sere PAR_CLOSE + { $$ = fnode::unop(op::first_match, $3); } bracedsere: BRACE_OPEN sere BRACE_CLOSE { $$ = $2; } diff --git a/spot/parsetl/scantl.ll b/spot/parsetl/scantl.ll index 182e6e044..4c0a6cb11 100644 --- a/spot/parsetl/scantl.ll +++ b/spot/parsetl/scantl.ll @@ -217,6 +217,8 @@ eol2 (\n\r)+|(\r\n)+ /* ~ comes from Goal, ! from everybody else */ {NOT} BEGIN(0); return token::OP_NOT; +"first_match" BEGIN(0); return token::OP_FIRST_MATCH; + /* SVA operators */ "##"[0-9]+ { errno = 0; diff --git a/spot/tl/dot.cc b/spot/tl/dot.cc index 8d8f68c4e..853a9f958 100644 --- a/spot/tl/dot.cc +++ b/spot/tl/dot.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009-2015, 2018 Laboratoire de Recherche et +// Copyright (C) 2009-2015, 2018-2019 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é @@ -88,6 +88,7 @@ namespace spot case op::AndNLM: case op::Star: case op::FStar: + case op::first_match: childnum = 0; // No number for children break; case op::Xor: diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc index b27a9b2c0..ab01b15f5 100644 --- a/spot/tl/formula.cc +++ b/spot/tl/formula.cc @@ -241,6 +241,7 @@ namespace spot C(Fusion); C(Star); C(FStar); + C(first_match); #undef C } SPOT_UNREACHABLE(); @@ -826,6 +827,18 @@ namespace spot if (f->is_boolean()) return unop(op::Not, f); break; + case op::first_match: + // first_match(first_match(sere)) = first_match(sere); + // first_match(b) = b + if (f->is(o) || f->is_boolean()) + return f; + // first_match(r*) = [*0] + if (f->accepts_eword()) + { + f->destroy(); + return eword(); + } + break; default: SPOT_UNREACHABLE(); } @@ -1617,6 +1630,23 @@ namespace spot } } break; + case op::first_match: + props = children[0]->props; + // If first_match(r) == r && !(r;[*]), then it should follow + // that if r is stutter-inv, then first_match(r) is + // stutter-inv, so we do not reset the syntactic_si bit. + assert(is_.sere_formula); + is_.boolean = false; + is_.ltl_formula = false; + is_.psl_formula = false; + is_.eventual = false; + is_.universal = false; + is_.syntactic_safety = false; + is_.syntactic_guarantee = false; + is_.syntactic_obligation = false; + is_.syntactic_recurrence = false; + is_.syntactic_persistence = false; + break; } } diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh index 738350b9d..cf16accb3 100644 --- a/spot/tl/formula.hh +++ b/spot/tl/formula.hh @@ -97,6 +97,7 @@ namespace spot // star-like operators Star, ///< Star FStar, ///< Fustion Star + first_match, ///< first_match(sere) }; #ifndef SWIG @@ -942,6 +943,11 @@ namespace spot /// @{ SPOT_DEF_UNOP(NegClosureMarked); /// @} + + /// \brief Construct first_match(sere) + /// @{ + SPOT_DEF_UNOP(first_match); + /// @} #undef SPOT_DEF_UNOP /// @{ @@ -1680,6 +1686,7 @@ namespace spot case op::Closure: case op::NegClosure: case op::NegClosureMarked: + case op::first_match: return unop(o, trans((*this)[0], std::forward(args)...)); case op::Xor: case op::Implies: diff --git a/spot/tl/mark.cc b/spot/tl/mark.cc index ec17d78d3..1dc79ef13 100644 --- a/spot/tl/mark.cc +++ b/spot/tl/mark.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012, 2014, 2015, 2018 Laboratoire de Recherche -// et Développement de l'Epita (LRDE). +// Copyright (C) 2010, 2012, 2014-2015, 2018-2019 Laboratoire de +// Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -59,6 +59,7 @@ namespace spot case op::UConcat: case op::Concat: case op::Fusion: + case op::first_match: res = f; break; case op::NegClosure: @@ -120,6 +121,7 @@ namespace spot case op::EConcat: case op::EConcatMarked: case op::UConcat: + case op::first_match: res = f; break; case op::Or: diff --git a/spot/tl/mutation.cc b/spot/tl/mutation.cc index 7c704dba5..76403fa09 100644 --- a/spot/tl/mutation.cc +++ b/spot/tl/mutation.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2016, 2018 Laboratoire de Recherche et +// Copyright (C) 2014-2016, 2018-2019 Laboratoire de Recherche et // Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -83,6 +83,7 @@ namespace spot case op::X: case op::F: case op::G: + case op::first_match: if ((opts_ & Mut_Remove_Ops) && mutation_counter_-- == 0) return f[0]; diff --git a/spot/tl/print.cc b/spot/tl/print.cc index 5bbb0cf98..2cae78557 100644 --- a/spot/tl/print.cc +++ b/spot/tl/print.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2010, 2012-2016, 2018 Laboratoire de +// Copyright (C) 2008, 2010, 2012-2016, 2018, 2019 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 @@ -71,6 +71,7 @@ namespace spot KFPlusBunop, KEqualBunop, KGotoBunop, + KFirstMatch, }; const char* spot_kw[] = { @@ -110,6 +111,7 @@ namespace spot "[:+]", "[=", "[->", + "first_match", }; const char* spin_kw[] = { @@ -149,6 +151,7 @@ namespace spot "[:+]", // not supported "[=", // not supported "[->", // not supported + "first_match", // not supported }; const char* wring_kw[] = { @@ -188,6 +191,7 @@ namespace spot "[:+]", // not supported "[=", // not supported "[->", // not supported + "first_match", // not supported }; const char* utf8_kw[] = { @@ -227,6 +231,7 @@ namespace spot "[:+]", "[=", "[->", + "first_match", }; const char* latex_kw[] = { @@ -266,6 +271,7 @@ namespace spot "\\SereFPlus{}", "\\SereEqual{", "\\SereGoto{", + "\\FirstMatch", }; const char* sclatex_kw[] = { @@ -309,6 +315,7 @@ namespace spot "^{\\mathsf{:}+}", "^{=", "^{\\to", + "\\mathsf{first\\_match}", }; static bool @@ -840,6 +847,13 @@ namespace spot } } break; + case op::first_match: + emit(KFirstMatch); + os_ << '('; + top_level_ = true; + visit(f[0]); + os_ << ')'; + break; } if (want_par) closep(); @@ -1113,6 +1127,7 @@ namespace spot case op::Fusion: case op::Star: case op::FStar: + case op::first_match: SPOT_UNIMPLEMENTED(); } for (auto c: f) diff --git a/spot/tl/randomltl.cc b/spot/tl/randomltl.cc index 5f2754750..3157f6fe8 100644 --- a/spot/tl/randomltl.cc +++ b/spot/tl/randomltl.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008-2012, 2014-2016, 2018 Laboratoire de Recherche +// Copyright (C) 2008-2012, 2014-2016, 2018-2019 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -311,7 +311,7 @@ namespace spot // SEREs random_sere::random_sere(const atomic_prop_set* ap) - : random_formula(11, ap), rb(ap) + : random_formula(12, ap), rb(ap) { proba_[0].setup("eword", 1, eword_builder); proba_2_ = proba_ + 1; @@ -321,11 +321,12 @@ namespace spot proba_[3].setup("star_b", 2, bunop_bounded_builder); proba_[4].setup("fstar", 2, bunop_unbounded_builder); proba_[5].setup("fstar_b", 2, bunop_bounded_builder); - proba_[6].setup("and", 3, multop_builder); - proba_[7].setup("andNLM", 3, multop_builder); - proba_[8].setup("or", 3, multop_builder); - proba_[9].setup("concat", 3, multop_builder); - proba_[10].setup("fusion", 3, multop_builder); + proba_[6].setup("first_match", 2, unop_builder); + proba_[7].setup("and", 3, multop_builder); + proba_[8].setup("andNLM", 3, multop_builder); + proba_[9].setup("or", 3, multop_builder); + proba_[10].setup("concat", 3, multop_builder); + proba_[11].setup("fusion", 3, multop_builder); update_sums(); } diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc index 422529fc6..2d82ba983 100644 --- a/spot/tl/simplify.cc +++ b/spot/tl/simplify.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011-2018 Laboratoire de Recherche et Developpement +// Copyright (C) 2011-2019 Laboratoire de Recherche et Developpement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -498,6 +498,7 @@ namespace spot case op::Fusion: case op::Star: case op::FStar: + case op::first_match: // !(a*) etc. should never occur. { assert(!negated); @@ -855,6 +856,7 @@ namespace spot case op::ap: case op::Not: case op::FStar: + case op::first_match: return f; case op::X: { diff --git a/spot/tl/snf.cc b/spot/tl/snf.cc index e525fe6df..2ee40cdc3 100644 --- a/spot/tl/snf.cc +++ b/spot/tl/snf.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2014, 2015, 2016, 2018 Laboratoire de Recherche +// Copyright (C) 2012, 2014, 2015, 2016, 2018, 2019 Laboratoire de Recherche // et Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -35,7 +35,6 @@ namespace spot class snf_visitor final { protected: - formula result_; snf_cache* cache_; public: snf_visitor(snf_cache* c) @@ -125,6 +124,7 @@ namespace spot SPOT_UNREACHABLE(); case op::AndRat: // Can AndRat be handled better? case op::FStar: // Can FStar be handled better? + case op::first_match: // Can first_match be handled better? out = f; break; } diff --git a/spot/tl/unabbrev.cc b/spot/tl/unabbrev.cc index 3238c079e..e2e57d2a4 100644 --- a/spot/tl/unabbrev.cc +++ b/spot/tl/unabbrev.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2018 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2015, 2018-2019 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -113,6 +113,7 @@ namespace spot case op::Fusion: case op::Star: case op::FStar: + case op::first_match: break; case op::F: // F e = e if e eventual diff --git a/spot/twa/formula2bdd.cc b/spot/twa/formula2bdd.cc index d93e1ecf6..93368b8a4 100644 --- a/spot/twa/formula2bdd.cc +++ b/spot/twa/formula2bdd.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2009-2019 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), @@ -99,6 +99,7 @@ namespace spot case op::AndNLM: case op::OrRat: case op::AndRat: + case op::first_match: SPOT_UNIMPLEMENTED(); case op::ap: return bdd_ithvar(d->register_proposition(f, owner)); diff --git a/spot/twaalgos/ltl2taa.cc b/spot/twaalgos/ltl2taa.cc index 6430f43cb..565b4edba 100644 --- a/spot/twaalgos/ltl2taa.cc +++ b/spot/twaalgos/ltl2taa.cc @@ -121,6 +121,7 @@ namespace spot case op::AndNLM: case op::AndRat: case op::OrRat: + case op::first_match: SPOT_UNIMPLEMENTED(); case op::U: diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc index a506bce49..f1b40edd7 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/spot/twaalgos/ltl2tgba_fm.cc @@ -867,6 +867,35 @@ namespace spot } return res; } + case op::first_match: + { + assert(f.size() == 1); + assert(!f.accepts_eword()); + // Build deterministic successors, and + // rewrite each destination D as first_match(D). + // This will handle the semantic of the operator automatically, + // since first_match(D) = [*0] if D accepts [*0]. + bdd res_ndet = recurse(f[0]); + bdd res_det = bddfalse; + bdd var_set = bdd_existcomp(bdd_support(res_ndet), dict_.var_set); + bdd all_props = bdd_existcomp(res_ndet, dict_.var_set); + while (all_props != bddfalse) + { + bdd label = bdd_satoneset(all_props, var_set, bddtrue); + all_props -= label; + + formula dest = + dict_.bdd_to_sere(bdd_appex(res_ndet, label, bddop_and, + dict_.var_set)); + dest = formula::first_match(dest); + if (to_concat_) + dest = formula::Concat({dest, to_concat_}); + if (!dest.is_ff()) + res_det |= label + & bdd_ithvar(dict_.register_next_variable(dest)); + } + return res_det; + } } SPOT_UNREACHABLE(); } @@ -1311,6 +1340,7 @@ namespace spot } case op::Star: case op::FStar: + case op::first_match: SPOT_UNREACHABLE(); // Not an LTL operator // r(f1 logical-op f2) = r(f1) logical-op r(f2) case op::Xor: diff --git a/tests/core/acc_word.test b/tests/core/acc_word.test index 47c09d611..53ce4b98e 100644 --- a/tests/core/acc_word.test +++ b/tests/core/acc_word.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016, 2017, 2018 Laboratoire de Recherche et Développement +# Copyright (C) 2016, 2017, 2018, 2019 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -141,3 +141,22 @@ grep 'highlight-word.*Fin' stderr ltlfilt -f 'GFa' --accept-word 'cycle{!a}' && exit 1 ltlfilt -f 'GF!a' --accept-word 'cycle{!a}' + +cat >input < c +{first_match(a ##[2:3] b)} |-> c +EOF +test 2 = `ltlfilt -c input --accept-word 'a;!b&!c;!b&!c;b&c;cycle{1}'` +test 2 = `ltlfilt -c input --accept-word 'a;!b&!c;b&c;cycle{1}'` +test 0 = `ltlfilt -c input --accept-word 'a;!b;b&!c;b&c;cycle{1}'` +test 2 = `ltlfilt -c input --accept-word 'a;!b;b&c;b&c;cycle{1}'` +test 1 = `ltlfilt -c input --accept-word 'a;!b;b&c;b&!c;cycle{1}'` + +L='ltlfilt -c input --accept-word' +cat >input < e +{first_match(a ##[2:3] b):first_match(c ##[1:2] d)} |-> e +EOF +test 2 = `$L 'a;!b&!c;!b&!c;b&c;b&c&d&e;cycle{1}'` +test 1 = `$L 'a;!b&!c;!b&!c;b&c;b&c&d&e;b&c&d&!e;cycle{1}'` +test 1 = `$L 'a;!b&!c;b&c;b&c&d&e;b&c&d&!e;cycle{1}'` diff --git a/tests/core/rand.test b/tests/core/rand.test index 267c411a8..63cecf6a4 100755 --- a/tests/core/rand.test +++ b/tests/core/rand.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2015, 2017, 2018 Laboratoire de Recherche et +# Copyright (C) 2014, 2015, 2017, 2018, 2019 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -34,6 +34,7 @@ star 1 star_b 1 fstar 1 fstar_b 1 +first_match 1 and 0 andNLM 0 or 1 @@ -54,7 +55,7 @@ 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" +sere="$sere,or=0,concat=0,fstar=0,fstar_b=0,first_match=0" run 0 randltl -S -n 10000 a b c --tree-size=10..20 \ --sere-p=$sere \ @@ -69,6 +70,7 @@ star 0 star_b 0 fstar 0 fstar_b 0 +first_match 0 and 0 andNLM 0 or 0 diff --git a/tests/core/randpsl.test b/tests/core/randpsl.test index f06a75cc9..293226027 100755 --- a/tests/core/randpsl.test +++ b/tests/core/randpsl.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2011, 2012, 2014, 2015, 2016 Laboratoire de Recherche +# Copyright (C) 2011, 2012, 2014, 2015, 2016, 2019 Laboratoire de Recherche # et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -25,10 +25,15 @@ set -e # Generate 50 random unique PSL formula that do not simplify to LTL # formulae, and that have a size of at least 12. -randltl -n -1 --tree-size 30 --seed 12 --psl a b c | +# The seed is selected so the test is fast enough, feel free to +# adjust it whenever something changes in formula generation. +randltl -n -1 --tree-size 30 --seed 13 --psl a b c | ltlfilt -r --size 12.. --unique | ltlfilt -v --ltl -n 50 | tee formulas | ltlcross '../ikwiad -R3 -t %f >%T' '../ikwiad -x -R3 -t %f >%T' \ -F - -f '{{(p1)}[*]:{(p3) && {{!(p1)} xor {!(p3)}}}}' test `wc -l < formulas` = 50 + + +randltl --psl --sere-priorities=first_match=10 -n 100 2 | grep first_match diff --git a/tests/core/unambig.test b/tests/core/unambig.test index f90d6348f..dc9467979 100755 --- a/tests/core/unambig.test +++ b/tests/core/unambig.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2013, 2015-2018 Laboratoire de Recherche et +# Copyright (C) 2013, 2015-2019 Laboratoire de Recherche et # Developpement de l'Epita # # This file is part of Spot, a model checking library. @@ -152,7 +152,7 @@ run 0 autfilt --check input > output test `grep -c unambiguous output` = 0 # Check 1000 random PSL formulas -randltl --psl -n 1000 3 | ltl2tgba -U -H | +randltl --seed=12 --psl -n 1000 3 | ltl2tgba -U -H | autfilt -v --is-unamb --stats=%M && exit 1 cat >input <-> (c & GFb)\")" + "spot.formula(\"{a;first_match(b[*];c[+];d)}<>-> (c & GFb)\")" ] }, "execution_count": 3, @@ -69,7 +69,7 @@ } ], "source": [ - "g = spot.formula('{a;b*;c[+]}<>->(GFb & c)'); g" + "g = spot.formula('{a;first_match(b*;c[+];d)}<>->(GFb & c)'); g" ] }, { @@ -497,47 +497,47 @@ "name": "stdout", "output_type": "stream", "text": [ - "{a;b[*];c[+]}<>-> (c & GFb)\n" + "{a;first_match(b[*];c[+];d)}<>-> (c & GFb)\n" ] }, { "data": { "image/svg+xml": [ - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "EConcat\n", + "\n", + "EConcat\n", "\n", "\n", "\n", "1\n", - "\n", - "Concat\n", + "\n", + "Concat\n", "\n", "\n", - "\n", + "\n", "0->1\n", - "\n", - "\n", - "L\n", + "\n", + "\n", + "L\n", "\n", - "\n", - "\n", - "7\n", - "\n", - "And\n", + "\n", + "\n", + "10\n", + "\n", + "And\n", "\n", - "\n", - "\n", - "0->7\n", - "\n", - "\n", - "R\n", + "\n", + "\n", + "0->10\n", + "\n", + "\n", + "R\n", "\n", "\n", "\n", @@ -548,95 +548,133 @@ "\n", "\n", "1->2\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "3\n", - "\n", - "Star\n", + "\n", + "first_match\n", "\n", "\n", - "\n", + "\n", "1->3\n", - "\n", - "\n", - "2\n", - "\n", - "\n", - "\n", - "5\n", - "\n", - "Star\n", - "\n", - "\n", - "\n", - "1->5\n", - "\n", - "\n", - "3\n", + "\n", + "\n", + "2\n", "\n", "\n", "\n", "4\n", - "\n", - "b\n", + "\n", + "Concat\n", "\n", "\n", - "\n", - "3->4\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "6\n", - "\n", - "c\n", - "\n", - "\n", - "\n", - "5->6\n", - "\n", - "\n", - "\n", - "\n", "\n", - "7->6\n", - "\n", - "\n", + "3->4\n", + "\n", + "\n", "\n", - "\n", - "\n", - "8\n", - "\n", - "G\n", + "\n", + "\n", + "5\n", + "\n", + "Star\n", "\n", - "\n", - "\n", - "7->8\n", - "\n", - "\n", + "\n", + "\n", + "4->5\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "Star\n", + "\n", + "\n", + "\n", + "4->7\n", + "\n", + "\n", + "2\n", "\n", "\n", "\n", "9\n", - "\n", - "F\n", + "\n", + "d\n", "\n", - "\n", - "\n", - "8->9\n", - "\n", - "\n", + "\n", + "\n", + "4->9\n", + "\n", + "\n", + "3\n", "\n", - "\n", - "\n", - "9->4\n", - "\n", - "\n", + "\n", + "\n", + "6\n", + "\n", + "b\n", + "\n", + "\n", + "\n", + "5->6\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "8\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "7->8\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "10->8\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "11\n", + "\n", + "G\n", + "\n", + "\n", + "\n", + "10->11\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "12\n", + "\n", + "F\n", + "\n", + "\n", + "\n", + "11->12\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "12->6\n", + "\n", + "\n", "\n", "\n", "" @@ -927,7 +965,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.7.1" + "version": "3.7.3" } }, "nbformat": 4, diff --git a/tests/python/randltl.ipynb b/tests/python/randltl.ipynb index b607d4beb..5ba8dfc69 100644 --- a/tests/python/randltl.ipynb +++ b/tests/python/randltl.ipynb @@ -171,12 +171,12 @@ "name": "stdout", "output_type": "stream", "text": [ - "{{p0 && p2}[*]}<>-> (Fp2 & Fp0)\n" + "{{1 | [*0]}[:*] & [*2]}\n" ] } ], "source": [ - "f = spot.randltl(3, output='psl', seed=332)\n", + "f = spot.randltl(3, output='psl', seed=26)\n", "print(next(f))" ] }, @@ -370,6 +370,7 @@ "star_b\t1\n", "fstar\t1\n", "fstar_b\t1\n", + "first_match\t1\n", "and\t1\n", "andNLM\t1\n", "or\t1\n", @@ -403,6 +404,7 @@ "star_b\t1\n", "fstar\t1\n", "fstar_b\t1\n", + "first_match\t1\n", "and\t1\n", "andNLM\t1\n", "or\t1\n", @@ -618,7 +620,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.6+" + "version": "3.7.3" } }, "nbformat": 4,