From 7901a37747795acda07d6b545466386fefa2311b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 19 Jul 2024 17:04:21 +0200 Subject: [PATCH] =?UTF-8?q?formula:=20track=20=CE=94=E2=82=81,=20=CE=A3?= =?UTF-8?q?=E2=82=82,=20=CE=A0=E2=82=82,=20and=20=CE=94=E2=82=82=20members?= =?UTF-8?q?hip?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * spot/tl/formula.hh, spot/tl/formula.cc: Update the properties and track them. * tests/core/kind.test: Augment the test case. * doc/tl/tl.tex, doc/spot.bib, NEWS: Document these new classes. --- NEWS | 5 ++ doc/spot.bib | 15 ++++ doc/tl/tl.tex | 205 +++++++++++++++++++++++++++++++++++-------- spot/tl/formula.cc | 154 +++++++++++++++++++++++++------- spot/tl/formula.hh | 75 +++++++++++++--- tests/core/kind.test | 194 ++++++++++++++++++++-------------------- 6 files changed, 473 insertions(+), 175 deletions(-) diff --git a/NEWS b/NEWS index 45d0c958f..700942091 100644 --- a/NEWS +++ b/NEWS @@ -18,6 +18,11 @@ New in spot 2.12.0.dev (not yet released) in its highest setting. This can be fine-tuned with the "rde" extra option, see the spot-x (7) man page for detail. + - The formula class now keeps track of membership to the Δ₁, Σ₂, + Π₂, and Δ₂ syntactic class. This can be tested with + formula::is_delta1(), formula::is_sigma2(), formula::is_pi2(), + formula::is_delta2(). See doc/tl/tl.pdf from more discussion. + New in spot 2.12 (2024-05-16) Build: diff --git a/doc/spot.bib b/doc/spot.bib index 3f24e40be..a2d5c1e9d 100644 --- a/doc/spot.bib +++ b/doc/spot.bib @@ -1,3 +1,4 @@ + @InProceedings{ babiak.12.tacas, author = {Tom{\'a}{\v{s}} Babiak and Mojm{\'i}r K{\v{r}}et{\'i}nsk{\'y} and Vojt{\v{e}}ch {\v{R}}eh{\'a}k @@ -470,6 +471,20 @@ doi = {10.1145/3209108.3209161} } +@Article{ esparza.24.acm, + author = {Javier Esparza and Rub\'{e}n Rubio and Salomon Sickert}, + title = {Efficient Normalization of Linear Temporal Logic}, + year = 2024, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + volume = {71}, + number = {2}, + issn = {0004-5411}, + doi = {10.1145/3651152}, + journal = {Journal of the ACM}, + month = apr +} + @InProceedings{ etessami.00.concur, author = {Kousha Etessami and Gerard J. Holzmann}, title = {Optimizing {B\"u}chi Automata}, diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 8982f606f..65db63511 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1121,6 +1121,14 @@ instance using the following methods: recurrence property. \\\texttt{is\_syntactic\_persistence()}& Whether the formula is a syntactic persistence property. +\\\texttt{is\_syntactic\_delta1()}& Whether the formula belongs to + the $\Delta_1$ class. +\\\texttt{is\_syntactic\_pi2()}& Whether the formula belongs to + the $\Pi_2$ class. +\\\texttt{is\_syntactic\_sigma2()}& Whether the formula belongs to + the $\Sigma_2$ class. +\\\texttt{is\_syntactic\_delta2()}& Whether the formula belongs to + the $\Delta_2$ class. \\\texttt{is\_marked()}& Whether the formula contains a special ``marked'' version of the $\Esuffix$ or $\nsere{r}$ operators.\newfootnotemark{1} \\\texttt{accepts\_eword()}& Whether the formula accepts @@ -1198,6 +1206,9 @@ rules: \mid \varphi_U\M \varphi_U \end{align*} +Given a formula \texttt{f}, its membership to these two classes can be +tested with \texttt{f.is\_eventual()} and \texttt{f.is\_universal()}. + \section{Syntactic Hierarchy Classes} \begin{figure}[tbp] @@ -1221,12 +1232,13 @@ rules: \path[fill=green!40,fill opacity=.5] (6,0) -- (1.5,0) -- (6,3); \draw (0,0) rectangle (6,7); - \node[align=center] (rea) at (3,6) {Reactivity\\ $\bigwedge\G\F p_i\lor \F\G q_i$}; - \node[align=center] (rec) at (1,4.5) {Recurrence\\ $\G\F p$}; - \node[align=center] (per) at (5,4.5) {Persistence\\ $\F\G p$}; - \node[align=center] (obl) at (3,2.85) {Obligation\\ $\bigwedge\G p_i\lor \F q_i$}; - \node[align=center] (saf) at (1,1) {Safety\\ $\G p$}; - \node[align=center] (gua) at (5,1) {Guarantee\\ $\F p$}; + \node[align=center] (rea) at (3,5.9) {Reactivity\\ $\bigwedge\G\F p_i\lor \F\G q_i$ \\ $\Delta_2$}; + \node[align=center] (rec) at (1,4.4) {Recurrence\\ $\G\F p$ \\ $\Pi_2$}; + \node[align=center] (per) at (5,4.4) {Persistence\\ $\F\G p$ \\ $\Sigma_2$}; + \node[align=center] (obl) at (3,2.85) {Obligation\\ $\bigwedge\G p_i\lor \F q_i$ \\ $\Delta_1$}; + \node[align=center] (saf) at (1,1) {Safety\\ $\G p$ \\ $\Pi_1$}; + \node[align=center] (gua) at (5,1) {Guarantee\\ $\F p$ \\ $\Sigma_1$}; + \node[align=center] (bas) at (3,0.4) {$\Delta_0$}; \node[align=right,below left] (det) at (-.2,6.7) {Deterministic\\Büchi\\Automata}; \node[align=left,below right](weak) at (6.2,6.7) {Weak Büchi\\Automata}; @@ -1254,24 +1266,107 @@ presented by~\citet{chang.92.icalp}, but other presentations have been done including negation~\citep{cerna.03.mfcs} and weak until~\citep{schneider.01.lpar}. -The following grammar rules extend the aforementioned work slightly by -dealing with PSL operators. These are the rules used by Spot to -decide upon construction to which class a formula belongs (see the -methods \texttt{is\_syntactic\_safety()}, -\texttt{is\_syntactic\_guarantee()}, -\texttt{is\_syntactic\_obligation()}, -\texttt{is\_syntactic\_recurrence()}, and -\texttt{is\_syntactic\_persistence()} listed on -page~\pageref{property-methods}). +Spot implements two versions of a syntactic hierarchy, and extend them +to deal with PSL operators. -The symbols $\varphi_G$, $\varphi_S$, $\varphi_O$, $\varphi_P$, -$\varphi_R$ denote any formula belonging respectively to the -Guarantee, Safety, Obligation, Persistence, or Recurrence classes. -Additionally $\varphi_B$ denotes a finite LTL formula (the unnamed -class at the intersection of Safety and Guarantee formulas, at the -\textbf{b}ottom of Fig.~\ref{fig:hierarchy}). $v$ denotes any -variable, $r$ any SERE, $r_F$ any bounded SERE (no loops), and $r_I$ -any unbounded SERE. + +The first hierarchy, usually denoted with names such as $\Sigma_i$ and +$\Pi_i$, as shown in Fig.~\ref{fig:hierarchy}. Following Esparza et +al.~\cite{esparza.24.acm}, we also introduce the $\Delta_0$, +$\Delta_1$, and $\Delta_2$ classes. + +Intuitively, those classes are related to how the weak operators +($\G$, $\W$, $\R$) alternate with the strong operators ($\U$, $\F$, +$\M$) in formula: + +\begin{itemize} +\item the class $\Delta_0$ contains all formulas that may only + use $\X$ as temporal operator, +\item formulas in $\Pi_1$ contains no strong operators, +\item formulas in $\Sigma_1$ contains no weak operators, +\item the class $\Delta_1$ contains all boolean combinations of + $\Pi_1$ and $\Sigma_1$, +\item in each branch of a formula of $\Pi_2$ that contains both types + of operator, weak operators are all above strong operators, +\item in each branch of a formula of $\Sigma_2$ that contains both types + of operator, strong operators are all above weak operators, +\item the class $\Delta_2$ contains all boolean combinations of + $\Pi_2$ and $\Sigma_2$. +\end{itemize} + +Those classes can be captured by the following grammar rules, where +$v$ denotes any variable, $r$ any SERE, $r_F$ any bounded SERE (no +loops), and $r_I$ any unbounded SERE. + +\begin{align*} + \varphi_{\Delta_0} ::={}& \0\mid\1\mid v\mid\NOT\varphi_{\Delta_0}\mid\varphi_{\Delta_0}\AND\varphi_{\Delta_0} + \mid(\varphi_{\Delta_0}\OR\varphi_{\Delta_0})\mid\varphi_{\Delta_0}\EQUIV\varphi_{\Delta_0} + \mid\varphi_{\Delta_0}\XOR\varphi_{\Delta_0}\mid\varphi_{\Delta_0}\IMPLIES\varphi_{\Delta_0} + \mid\X\varphi_{\Delta_0}\\ + \mid{}& \sere{r_F}\mid \nsere{r_F}\\ + \varphi_{\Pi_1} ::={}& \varphi_{\Delta_0}\mid \NOT\varphi_S\mid + \varphi_{\Pi_1}\AND \varphi_{\Pi_1}\mid (\varphi_{\Pi_1}\OR \varphi_{\Pi_1}) + \mid\varphi_S\IMPLIES\varphi_{\Pi_1}\mid + \X\varphi_{\Pi_1} \mid \F\varphi_{\Pi_1}\mid + \varphi_{\Pi_1}\U\varphi_{\Pi_1}\mid \varphi_{\Pi_1}\M\varphi_{\Pi_1}\\ + \mid{}& \nsere{r}\mid + \sere{r}\Esuffix \varphi_{\Pi_1}\mid + \sere{r_F}\Asuffix \varphi_{\Pi_1} \\ + \varphi_{\Sigma_1} ::={}& \varphi_{\Delta_0}\mid \NOT\varphi_{\Pi_1}\mid + \varphi_{\Sigma_1}\AND \varphi_{\Sigma_1}\mid (\varphi_{\Sigma_1}\OR \varphi_{\Sigma_1}) + \mid\varphi_{\Pi_1}\IMPLIES\varphi_{\Sigma_1}\mid + \X\varphi_{\Sigma_1} \mid \G\varphi_{\Sigma_1}\mid + \varphi_{\Sigma_1}\R\varphi_{\Sigma_1}\mid \varphi_{\Sigma_1}\W\varphi_{\Sigma_1}\\ + \mid{}& \sere{r}\mid + \sere{r_F}\Esuffix \varphi_{\Sigma_1}\mid + \sere{r}\Asuffix \varphi_{\Sigma_1}\\ + \varphi_{\Delta_1} ::={}& \varphi_{\Pi_1} \mid \varphi_{\Sigma_1}\mid \NOT\varphi_{\Delta_1}\mid + \varphi_{\Delta_1}\AND \varphi_{\Delta_1}\mid (\varphi_{\Delta_1}\OR \varphi_{\Delta_1})\mid + \varphi_{\Delta_1}\EQUIV \varphi_{\Delta_1}\mid \varphi_{\Delta_1}\XOR \varphi_{\Delta_1}\mid + \varphi_{\Delta_1}\IMPLIES \varphi_{\Delta_1}\\ + \mid{}& \X\varphi_{\Delta_1} \mid{} + \sere{r_F}\Esuffix \varphi_{\Delta_1} \mid + \sere{r_F}\Asuffix \varphi_{\Delta_1}\\ + \varphi_{\Sigma_2} ::={}& \varphi_{\Delta_1} \mid \NOT\varphi_{\Pi_2}\mid + \varphi_{\Sigma_2}\AND \varphi_{\Sigma_2}\mid (\varphi_{\Sigma_2}\OR \varphi_{\Sigma_2})\mid + \varphi_{\Pi_2}\IMPLIES \varphi_{\Sigma_2}\\ + \mid{}& \X\varphi_{\Sigma_2} \mid \F\varphi_{\Sigma_2} \mid + \varphi_{\Sigma_2}\U\varphi_{\Sigma_2}\mid\varphi_{\Sigma_2}\M\varphi_{\Sigma_2} + \mid{} \sere{r}\Esuffix \varphi_{\Sigma_2}\mid \sere{r_F}\Asuffix \varphi_{\Sigma_2}\\ + \varphi_{\Pi_2} ::={}& \varphi_{\Delta_1} \mid \NOT\varphi_{\Sigma_2}\mid + \varphi_{\Pi_2}\AND \varphi_{\Pi_2}\mid (\varphi_{\Pi_2}\OR \varphi_{\Pi_2})\mid + \varphi_{\Sigma_2}\IMPLIES \varphi_{\Pi_2}\\ + \mid{}& \X\varphi_{\Pi_2} \mid \G\varphi_{\Pi_2} \mid + \varphi_{\Pi_2}\R\varphi_{\Pi_2}\mid + \varphi_{\Pi_2}\W\varphi_{\Pi_2} \mid{} \sere{r}\Asuffix \varphi_{\Pi_2}\mid \sere{r_F}\Esuffix \varphi_{\Pi_2}\\ + \varphi_{\Delta_2} ::={}& \varphi_{\Pi_2} \mid \varphi_{\Sigma_2}\mid \NOT\varphi_{\Delta_2}\mid + \varphi_{\Delta_2}\AND \varphi_{\Delta_2}\mid (\varphi_{\Delta_2}\OR \varphi_{\Delta_2})\mid + \varphi_{\Delta_2}\EQUIV \varphi_{\Delta_2}\mid \varphi_{\Delta_2}\XOR \varphi_{\Delta_2}\mid + \varphi_{\Delta_2}\IMPLIES \varphi_{\Delta_2}\\ + \mid{}& \X\varphi_{\Delta_2} \mid{} \sere{r_F}\Esuffix \varphi_{\Delta_2} \mid + \sere{r_F}\Asuffix \varphi_{\Delta_2}\\ +\end{align*} + + +A nice property of these classes, is that they are as expressive as +their corresponding automata classes. For instance any LTL/PSL +property that is representable by a deterministic Büchi automaton (the +recurrence class) can be represented by an LTL/PSL formula in the +$\Pi_2$ fragment, even if the original formula isn't in the $\Pi_2$ +fragment originally. + +If the objective is to classify properties syntactically, it is useful +to use some slightly more complete grammar rules. In the following +list, the rules the initial $G$, $S$, $O$, $P$, $R$ of their +corresponding property clases, as listed in Fig.~\ref{fig:hierarchy} +(i.e., Guarantee, Safety, Obligation, Persistence, Recurrence). +Additionally, $B$ denotes the ``bottom'' class (a.k.a. $\Delta_0$). +Note that $\varphi_B$, $\varphi_G$, and $\varphi_S$ are rigorously +equivalent to $\varphi_{\Delta_0}$, $\varphi_{\Pi_1}$, and +$\varphi_{\Sigma_1}$. The difference in the higher classes are +\colorbox{yellow}{highlighted}. There is no generalization of +$\varphi_{\Delta_2}$ since any LTL/PSL formula is a reactivity +property. \begin{align*} \varphi_B ::={}& \0\mid\1\mid v\mid\NOT\varphi_B\mid\varphi_B\AND\varphi_B @@ -1300,36 +1395,70 @@ any unbounded SERE. \varphi_O\EQUIV \varphi_O\mid \varphi_O\XOR \varphi_O\mid \varphi_O\IMPLIES \varphi_O\\ \mid{}& \X\varphi_O \mid - \varphi_O\U\varphi_G\mid\varphi_O\R\varphi_S \mid - \varphi_S\W\varphi_O\mid \varphi_G\M\varphi_O\\ - \mid{}& \sere{r} \mid \nsere{r}\mid - \sere{r_F}\Esuffix \varphi_O \mid \sere{r_I}\Esuffix \varphi_G\mid + \colorbox{yellow}{$\varphi_O\U\varphi_G$}\mid + \colorbox{yellow}{$\varphi_O\R\varphi_S$}\mid + \colorbox{yellow}{$\varphi_S\W\varphi_O$}\mid + \colorbox{yellow}{$\varphi_G\M\varphi_O$}\\ + \mid{}& \sere{r_F}\Esuffix \varphi_O \mid \colorbox{yellow}{$\sere{r_I}\Esuffix \varphi_G$}\mid \sere{r_F}\Asuffix \varphi_O\mid - \sere{r_I}\Asuffix \varphi_S\\ + \colorbox{yellow}{$\sere{r_I}\Asuffix \varphi_S$}\\ \varphi_P ::={}& \varphi_O \mid \NOT\varphi_R\mid \varphi_P\AND \varphi_P\mid (\varphi_P\OR \varphi_P)\mid \varphi_R\IMPLIES \varphi_P\\ \mid{}& \X\varphi_P \mid \F\varphi_P \mid - \varphi_P\U\varphi_P\mid\varphi_P\R\varphi_S\mid - \varphi_S\W\varphi_P\mid\varphi_P\M\varphi_P\\ + \varphi_P\U\varphi_P\mid\colorbox{yellow}{$\varphi_P\R\varphi_S$}\mid + \colorbox{yellow}{$\varphi_S\W\varphi_P$}\mid\varphi_P\M\varphi_P\\ \mid{}& \sere{r}\Esuffix \varphi_P\mid \sere{r_F}\Asuffix \varphi_P\mid - \sere{r_I}\Asuffix \varphi_S\\ + \colorbox{yellow}{$\sere{r_I}\Asuffix \varphi_S$}\\ \varphi_R ::={}& \varphi_O \mid \NOT\varphi_P\mid \varphi_R\AND \varphi_R\mid (\varphi_R\OR \varphi_R)\mid \varphi_P\IMPLIES \varphi_R\\ \mid{}& \X\varphi_R \mid \G\varphi_R \mid - \varphi_R\U\varphi_G\mid\varphi_R\R\varphi_R\mid - \varphi_R\W\varphi_R\mid\varphi_G\M\varphi_R\\ - \mid{}& \sere{r}\Asuffix \varphi_R\mid \sere{r_F}\Esuffix \varphi_R \mid \sere{r_I}\Esuffix \varphi_G\\ + \colorbox{yellow}{$\varphi_R\U\varphi_G$}\mid\varphi_R\R\varphi_R\mid + \varphi_R\W\varphi_R\mid\colorbox{yellow}{$\varphi_G\M\varphi_R$}\\ + \mid{}& \sere{r}\Asuffix \varphi_R\mid \sere{r_F}\Esuffix \varphi_R \mid \colorbox{yellow}{$\sere{r_I}\Esuffix \varphi_G$}\\ \end{align*} + It should be noted that a formula can belong to a class of the temporal hierarchy even if it does not syntactically appears so. For -instance the formula $(\G(q\OR \F\G p)\AND \G(r\OR \F\G\NOT p))\OR\G -q\OR \G r$ is not syntactically safe, yet it is a safety formula -equivalent to $\G q\OR \G r$. Such a formula is usually said -\emph{pathologically safe}. +instance the formula +$(\G(q\OR \F\G p)\AND \G(r\OR \F\G\NOT p))\OR\G q\OR \G r$ is not +syntactically safe (and isn't even in $\Delta_2$), yet it is a safety +formula equivalent to $\G q\OR \G r$ (which is in $\Pi_1$, the +syntactical class of safety formulas). Such a formula is usually said +to be a \emph{pathological safety} formula. + +To illustrate the difference in the grammar for the higher classes, +consider the formula $\G((\G a) \U b)$. This formula can be converted +to a deterministic Büchi automaton, so it specifies a recurrence +property. It is captured by the grammar rule for $\varphi_R$ above, +yet it does not belong to the $\Pi_2$ class because of the alternation +between weak ($\G$), strong ($\U$), and weak ($\G$) operators. +However the equivalent formula $\G((\G a) \W b))\land \G\F b$ belongs +to $\Pi_2$. + +Spot computes the membership to each of those class whenever a formula +$f$ is constructed. Here is how the membership to each of those class +can be tested: +\begin{center} +\begin{tabular}{cl} + \toprule + $f\in \Delta_0$ & \texttt{f.is\_syntactic\_safety() \&\& f.is\_syntactic\_guarantee()} \\ + $f\in \Pi_1$, $f\in S$ & \texttt{f.is\_syntactic\_safety()} \\ + $f\in \Sigma_1$, $f\in G$ & \texttt{f.is\_syntactic\_guarantee()} \\ + $f\in \Delta_1$ & \texttt{f.is\_delta1()} \\ + $f\in O$ & \texttt{f.is\_syntactic\_obligation()} \\ + $f\in \Pi_2$ & \texttt{f.is\_pi2()} \\ + $f\in R$ & \texttt{f.is\_syntactic\_recurrence()} \\ + $f\in \Sigma_2$ & \texttt{f.is\_sigma2()} \\ + $f\in P$ & \texttt{f.is\_syntactic\_persistence()} \\ + $f\in \Delta_2$ & \texttt{f.is\_delta2()} \\ + \bottomrule +\end{tabular} +\end{center} + \chapter{Rewritings} diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc index 1a1a4fb47..fe5770931 100644 --- a/spot/tl/formula.cc +++ b/spot/tl/formula.cc @@ -1290,6 +1290,10 @@ namespace spot is_.accepting_eword = false; is_.lbt_atomic_props = true; is_.spin_atomic_props = true; + is_.delta1 = true; + is_.sigma2 = true; + is_.pi2 = true; + is_.delta2 = true; break; case op::eword: is_.boolean = false; @@ -1312,6 +1316,10 @@ namespace spot is_.accepting_eword = true; is_.lbt_atomic_props = true; is_.spin_atomic_props = true; + is_.delta1 = true; + is_.sigma2 = true; + is_.pi2 = true; + is_.delta2 = true; break; case op::ap: is_.boolean = true; @@ -1348,6 +1356,10 @@ namespace spot is_.lbt_atomic_props = lbtap; is_.spin_atomic_props = lbtap || is_spin_ap(n.c_str()); } + is_.delta1 = true; + is_.sigma2 = true; + is_.pi2 = true; + is_.delta2 = true; break; case op::Not: props = children[0]->props; @@ -1364,6 +1376,10 @@ namespace spot is_.syntactic_persistence = children[0]->is_syntactic_recurrence(); is_.accepting_eword = false; + // is_.delta1 inherited + is_.sigma2 = children[0]->is_pi2(); + is_.pi2 = children[0]->is_sigma2(); + // is_.delta2 inherited break; case op::X: case op::strong_X: @@ -1382,6 +1398,10 @@ namespace spot // we could make sense of it if we start supporting LTL over // finite traces. is_.accepting_eword = false; + // is_.delta1 inherited + // is_.sigma2 inherited + // is_.pi2 inherited + // is_.delta2 inherited break; case op::F: props = children[0]->props; @@ -1397,6 +1417,10 @@ namespace spot is_.syntactic_recurrence = is_.syntactic_guarantee; // is_.syntactic_persistence inherited is_.accepting_eword = false; + is_.delta1 = is_.syntactic_guarantee; + is_.pi2 = is_.syntactic_guarantee; + // is_.sigma2 inherited + is_.delta2 = is_.pi2 | is_.sigma2; break; case op::G: props = children[0]->props; @@ -1412,6 +1436,10 @@ namespace spot // is_.syntactic_recurrence inherited is_.syntactic_persistence = is_.syntactic_safety; is_.accepting_eword = false; + is_.delta1 = is_.syntactic_safety; + is_.sigma2 = is_.syntactic_safety; + // is_.pi2 inherited + is_.delta2 = is_.pi2 | is_.sigma2; break; case op::NegClosure: case op::NegClosureMarked: @@ -1427,6 +1455,10 @@ namespace spot is_.syntactic_recurrence = true; is_.syntactic_persistence = true; is_.accepting_eword = false; + is_.delta1 = true; + is_.sigma2 = true; + is_.pi2 = true; + is_.delta2 = true; assert(children[0]->is_sere_formula()); assert(!children[0]->is_boolean()); break; @@ -1443,6 +1475,10 @@ namespace spot is_.syntactic_recurrence = true; is_.syntactic_persistence = true; is_.accepting_eword = false; + is_.delta1 = true; + is_.sigma2 = true; + is_.pi2 = true; + is_.delta2 = true; assert(children[0]->is_sere_formula()); assert(!children[0]->is_boolean()); break; @@ -1473,6 +1509,17 @@ namespace spot is_.syntactic_recurrence = false; is_.syntactic_persistence = false; } + if (is_.delta1) + { + assert(is_.pi2 == true); + assert(is_.sigma2 == true); + assert(is_.delta2 == true); + } + else + { + is_.pi2 = false; + is_.sigma2 = false; + } break; case op::Implies: props = children[0]->props & children[1]->props; @@ -1494,6 +1541,10 @@ namespace spot is_.syntactic_recurrence = children[0]->is_syntactic_persistence() && children[1]->is_syntactic_recurrence(); is_.accepting_eword = false; + // is_.delta1 inherited + is_.sigma2 = children[0]->is_pi2() && children[1]->is_sigma2(); + is_.pi2 = children[0]->is_sigma2() && children[1]->is_pi2(); + // is_.delta2 inherited break; case op::EConcatMarked: case op::EConcat: @@ -1507,18 +1558,25 @@ namespace spot is_.syntactic_guarantee = children[1]->is_syntactic_guarantee(); is_.syntactic_persistence = children[1]->is_syntactic_persistence(); - if (children[0]->is_finite()) + is_.sigma2 = children[1]->is_sigma2(); + if (children[0]->is_finite()) // behaves like X { is_.syntactic_safety = children[1]->is_syntactic_safety(); is_.syntactic_obligation = children[1]->is_syntactic_obligation(); is_.syntactic_recurrence = children[1]->is_syntactic_recurrence(); + is_.delta1 = children[1]->is_delta1(); + is_.pi2 = children[1]->is_pi2(); + is_.delta2 = children[1]->is_delta2(); } - else + else // behaves like F { is_.syntactic_safety = false; bool g = children[1]->is_syntactic_guarantee(); is_.syntactic_obligation = g; is_.syntactic_recurrence = g; + is_.delta1 = g; + is_.pi2 = g; + is_.delta2 = g | is_.sigma2; } assert(children[0]->is_sere_formula()); assert(children[1]->is_psl_formula()); @@ -1536,19 +1594,25 @@ namespace spot is_.syntactic_safety = children[1]->is_syntactic_safety(); is_.syntactic_recurrence = children[1]->is_syntactic_recurrence(); - if (children[0]->is_finite()) + is_.pi2 = children[1]->is_pi2(); + if (children[0]->is_finite()) // behaves like X { is_.syntactic_guarantee = children[1]->is_syntactic_guarantee(); is_.syntactic_obligation = children[1]->is_syntactic_obligation(); - is_.syntactic_persistence = - children[1]->is_syntactic_persistence(); + is_.syntactic_persistence = children[1]->is_syntactic_persistence(); + is_.delta1 = children[1]->is_delta1(); + is_.sigma2 = children[1]->is_sigma2(); + is_.delta2 = children[1]->is_delta2(); } - else + else // behaves like G { is_.syntactic_guarantee = false; bool s = children[1]->is_syntactic_safety(); is_.syntactic_obligation = s; is_.syntactic_persistence = s; + is_.delta1 = s; + is_.sigma2 = s; + is_.delta2 = is_.pi2 | s; } assert(children[0]->is_sere_formula()); assert(children[1]->is_psl_formula()); @@ -1596,6 +1660,10 @@ namespace spot children[0]->is_syntactic_recurrence() && children[1]->is_syntactic_guarantee(); // is_.syntactic_persistence = Persistence U Persistance + is_.delta1 = is_.syntactic_guarantee; + // is_.sigma2 = Σ₂ U Σ₂ + is_.pi2 = is_.syntactic_guarantee; + is_.delta2 = is_.sigma2 | is_.pi2; break; case op::W: // See comment for op::U. @@ -1617,7 +1685,10 @@ namespace spot is_.syntactic_persistence = // Safety W Persistance children[0]->is_syntactic_safety() && children[1]->is_syntactic_persistence(); - + is_.delta1 = is_.syntactic_safety; + is_.sigma2 = is_.syntactic_safety; + // is_.pi2 = Π₂ U Π₂ + is_.delta2 = is_.sigma2 | is_.pi2; break; case op::R: // See comment for op::U. @@ -1640,7 +1711,10 @@ namespace spot is_.syntactic_persistence = // Persistence R Safety children[0]->is_syntactic_persistence() && children[1]->is_syntactic_safety(); - + is_.delta1 = is_.syntactic_safety; + is_.sigma2 = is_.syntactic_safety; + // is_.pi2 = Π₂ U Π₂ + is_.delta2 = is_.sigma2 | is_.pi2; break; case op::M: // See comment for op::U. @@ -1662,7 +1736,10 @@ namespace spot children[0]->is_syntactic_guarantee() && children[1]->is_syntactic_recurrence(); // is_.syntactic_persistence = Persistence M Persistance - + is_.delta1 = is_.syntactic_guarantee; + // is_.sigma2 = Σ₂ M Σ₂ + is_.pi2 = is_.syntactic_guarantee; + is_.delta2 = is_.sigma2 | is_.pi2; break; case op::Or: { @@ -1787,6 +1864,10 @@ namespace spot is_.syntactic_obligation = false; is_.syntactic_recurrence = false; is_.syntactic_persistence = false; + is_.delta1 = false; + is_.pi2 = false; + is_.sigma2 = false; + is_.delta2 = false; switch (op_) { @@ -1832,6 +1913,10 @@ namespace spot is_.syntactic_obligation = false; is_.syntactic_recurrence = false; is_.syntactic_persistence = false; + is_.delta1 = false; + is_.pi2 = false; + is_.sigma2 = false; + is_.delta2 = false; break; } } @@ -2011,31 +2096,38 @@ namespace spot return strverscmp(f->ap_name().c_str(), g->ap_name().c_str()); } -#define printprops \ - proprint(is_boolean, "B", "Boolean formula"); \ +#define printprops \ + proprint(is_boolean, "B", "Boolean formula"); \ proprint(is_sugar_free_boolean, "&", "without Boolean sugar"); \ - proprint(is_in_nenoform, "!", "in negative normal form"); \ - proprint(is_syntactic_stutter_invariant, "x", \ - "syntactic stutter invariant"); \ + proprint(is_in_nenoform, "!", "in negative normal form"); \ + proprint(is_syntactic_stutter_invariant, "x", \ + "syntactic stutter invariant"); \ proprint(is_sugar_free_ltl, "f", "without LTL sugar"); \ - proprint(is_ltl_formula, "L", "LTL formula"); \ - proprint(is_psl_formula, "P", "PSL formula"); \ - proprint(is_sere_formula, "S", "SERE formula"); \ - proprint(is_finite, "F", "finite"); \ - proprint(is_eventual, "e", "pure eventuality"); \ - proprint(is_universal, "u", "purely universal"); \ - proprint(is_syntactic_safety, "s", "syntactic safety"); \ - proprint(is_syntactic_guarantee, "g", "syntactic guarantee"); \ - proprint(is_syntactic_obligation, "o", "syntactic obligation"); \ - proprint(is_syntactic_persistence, "p", "syntactic persistence"); \ - proprint(is_syntactic_recurrence, "r", "syntactic recurrence"); \ - proprint(is_marked, "+", "marked"); \ - proprint(accepts_eword, "0", "accepts the empty word"); \ - proprint(has_lbt_atomic_props, "l", \ - "has LBT-style atomic props"); \ - proprint(has_spin_atomic_props, "a", \ - "has Spin-style atomic props"); + proprint(is_ltl_formula, "L", "LTL formula"); \ + proprint(is_psl_formula, "P", "PSL formula"); \ + proprint(is_sere_formula, "S", "SERE formula"); \ + proprint(is_finite, "F", "finite"); \ + proprint(is_eventual, "e", "pure eventuality"); \ + proprint(is_universal, "u", "purely universal"); \ + proprint(is_syntactic_safety, "s", "syntactic safety"); \ + proprint(is_syntactic_guarantee, "g", "syntactic guarantee"); \ + proprint(is_syntactic_obligation, "o", "syntactic obligation"); \ + proprint(is_syntactic_persistence, "p", "syntactic persistence"); \ + proprint(is_syntactic_recurrence, "r", "syntactic recurrence"); \ + proprint(is_marked, "+", "marked"); \ + proprint(accepts_eword, "0", "accepts the empty word"); \ + proprint(has_lbt_atomic_props, "l", \ + "has LBT-style atomic props"); \ + proprint(has_spin_atomic_props, "a", \ + "has Spin-style atomic props"); \ + proprint(is_delta1, "O", "delta1"); \ + proprint(is_sigma2, "P", "sigma2"); \ + proprint(is_pi2, "R", "pi2"); \ + proprint(is_delta2, "D", "delta2"); + // O (for Δ₁), P (for Σ₂), R (for Π₂) are the uppercase versions of + // o (obligation), p (persistence), r (recurrence) because they are + // stricter subsets of those. std::list list_formula_props(const formula& f) diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh index 4f56c38bc..d2d3dd080 100644 --- a/spot/tl/formula.hh +++ b/spot/tl/formula.hh @@ -522,6 +522,30 @@ namespace spot return is_.spin_atomic_props; } + /// \see formula::is_sigma2 + bool is_sigma2() const + { + return is_.sigma2; + } + + /// \see formula::is_pi2 + bool is_pi2() const + { + return is_.pi2; + } + + /// \see formula::is_delta1 + bool is_delta1() const + { + return is_.delta1; + } + + /// \see formula::is_delta2 + bool is_delta2() const + { + return is_.delta2; + } + private: static size_t bump_next_id(); void setup_props(op o); @@ -627,15 +651,19 @@ namespace spot bool finite:1; // Finite SERE formulae, or Bool+X forms. bool eventual:1; // Purely eventual formula. bool universal:1; // Purely universal formula. - bool syntactic_safety:1; // Syntactic Safety Property. - bool syntactic_guarantee:1; // Syntactic Guarantee Property. - bool syntactic_obligation:1; // Syntactic Obligation Property. - bool syntactic_recurrence:1; // Syntactic Recurrence Property. - bool syntactic_persistence:1; // Syntactic Persistence Property. + bool syntactic_safety:1; // Syntactic Safety Property (S). + bool syntactic_guarantee:1; // Syntactic Guarantee Property (G). + bool syntactic_obligation:1; // Syntactic Obligation Property (O). + bool syntactic_recurrence:1; // Syntactic Recurrence Property (R). + bool syntactic_persistence:1; // Syntactic Persistence Property (P). bool not_marked:1; // No occurrence of EConcatMarked. bool accepting_eword:1; // Accepts the empty word. bool lbt_atomic_props:1; // Use only atomic propositions like p42. bool spin_atomic_props:1; // Use only spin-compatible atomic props. + bool delta1:1; // Boolean combination of (S) and (G). + bool sigma2:1; // Boolean comb. of (S) with X/F/U/M possibly applied. + bool pi2:1; // Boolean comb. of (G) with X/G/R/W possibly applied. + bool delta2:1; // Boolean combination of (Σ₂) and (Π₂). }; union { @@ -1698,16 +1726,43 @@ namespace spot /// universal formula also satisfies the formula. /// \cite etessami.00.concur SPOT_DEF_PROP(is_universal); - /// Whether a PSL/LTL formula is syntactic safety property. + /// \brief Whether a PSL/LTL formula is syntactic safety property. + /// + /// Is class is also called Π₁. SPOT_DEF_PROP(is_syntactic_safety); - /// Whether a PSL/LTL formula is syntactic guarantee property. + /// \brief Whether a PSL/LTL formula is syntactic guarantee property. + /// + /// Is class is also called Σ₁. SPOT_DEF_PROP(is_syntactic_guarantee); - /// Whether a PSL/LTL formula is syntactic obligation property. + /// \brief Whether a PSL/LTL formula is in the Δ₁ syntactic frament + /// + /// A formula is in Δ₁ if it is a boolean combination of syntactic + /// safety and syntactic guarantee properties. + SPOT_DEF_PROP(is_delta1); + /// \brief Whether a PSL/LTL formula is syntactic obligation property. + /// + /// This class is a proper syntactic superset of Δ₁, but has the + /// same expressive power. SPOT_DEF_PROP(is_syntactic_obligation); - /// Whether a PSL/LTL formula is syntactic recurrence property. + /// Whether a PSL/LTL formula is in Σ₂ + SPOT_DEF_PROP(is_sigma2); + /// Whether a PSL/LTL formula is in Π₂ + SPOT_DEF_PROP(is_pi2); + /// \brief Whether a PSL/LTL formula is syntactic recurrence property. + /// + /// This class is a proper syntactic superset of Σ₂ syntactically, + /// expressive power. SPOT_DEF_PROP(is_syntactic_recurrence); - /// Whether a PSL/LTL formula is syntactic persistence property. + /// \brief Whether a PSL/LTL formula is syntactic persistence property. + /// + /// This class is a proper syntactic superset of Π₂, but has the + /// same expressive power. SPOT_DEF_PROP(is_syntactic_persistence); + /// \brief Whether a PSL/LTL formula is in the Δ₂ syntactic frament + /// + /// A formula is in Δ₂ if it is a boolean combination of Σ₂ and Π₂ + /// properties. + SPOT_DEF_PROP(is_delta2); /// \brief Whether the formula has an occurrence of EConcatMarked /// or NegClosureMarked SPOT_DEF_PROP(is_marked); diff --git a/tests/core/kind.test b/tests/core/kind.test index 93c7dcef4..14e9870fa 100755 --- a/tests/core/kind.test +++ b/tests/core/kind.test @@ -25,118 +25,120 @@ set -e cat >input<b,BxfLPSFsgopra -!a,B&!xfLPSFsgopra -!(a|b),B&xfLPSFsgopra -F(a),&!xLPegopra -G(a),&!xLPusopra -a U b,&!xfLPgopra -a U Fb,&!xLPegopra -Ga U b,&!xLPopra -1 U a,&!xfLPegopra -a W b,&!xfLPsopra -a W 0,&!xfLPusopra -a M b,&!xfLPgopra -a M 1,&!xfLPegopra -a R b,&!xfLPsopra -0 R b,&!xfLPusopra -a R (b R (c R d)),&!xfLPsopra -a U (b U (c U d)),&!xfLPgopra -a W (b W (c W d)),&!xfLPsopra -a M (b M (c M d)),&!xfLPgopra -Fa -> Fb,xLPopra -Ga -> Fb,xLPegopra -Fa -> Gb,xLPusopra -(Ga|Fc) -> Fb,xLPopra -(Ga|Fa) -> Gb,xLPopra -{a;c*;b}|->!Xb,&fPsopra -{a;c*;b}|->X!b,&!fPsopra -{a;c*;b}|->!Fb,&Psopra -{a;c*;b}|->G!b,&!Psopra -{a;c*;b}|->!Gb,&Pra -{a;c*;b}|->F!b,&!Pra -{a;c*;b}|->GFa,&!Pra +a,B&!xfLPSFsgopraOPRD +a<->b,BxfLPSFsgopraOPRD +!a,B&!xfLPSFsgopraOPRD +!(a|b),B&xfLPSFsgopraOPRD +F(a),&!xLPegopraOPRD +G(a),&!xLPusopraOPRD +a U b,&!xfLPgopraOPRD +a U Fb,&!xLPegopraOPRD +Ga U b,&!xLPopraPD +1 U a,&!xfLPegopraOPRD +a W b,&!xfLPsopraOPRD +a W 0,&!xfLPusopraOPRD +a M b,&!xfLPgopraOPRD +a M 1,&!xfLPegopraOPRD +a R b,&!xfLPsopraOPRD +0 R b,&!xfLPusopraOPRD +a R (b R (c R d)),&!xfLPsopraOPRD +a U (b U (c U d)),&!xfLPgopraOPRD +a W (b W (c W d)),&!xfLPsopraOPRD +a M (b M (c M d)),&!xfLPgopraOPRD +Fa -> Fb,xLPopraOPRD +Ga -> Fb,xLPegopraOPRD +Fa -> Gb,xLPusopraOPRD +(Ga|Fc) -> Fb,xLPopraOPRD +(Ga|Fa) -> Gb,xLPopraOPRD +{a;c*;b}|->!Xb,&fPsopraOPRD +{a;c*;b}|->X!b,&!fPsopraOPRD +{a;c*;b}|->!Fb,&PsopraOPRD +{a;c*;b}|->G!b,&!PsopraOPRD +{a;c*;b}|->!Gb,&PraRD +{a;c*;b}|->F!b,&!PraRD +{a;c*;b}|->GFa,&!PraRD {a;c*;b}|->FGa,&!Pa -{a[+];c[+];b*}|->!Fb,&Psopra -{a*;c[+];b*}|->!Fb,&xPsopra -{a[+];c*;b[+]}|->G!b,&!Psopra -{a*;c[+];b[+]}|->!Gb,&Pra -{a[+];c*;b[+]}|->F!b,&!Pra -{a[+];c[+];b*}|->GFa,&!Pra +{a[+];c[+];b*}|->!Fb,&PsopraOPRD +{a*;c[+];b*}|->!Fb,&xPsopraOPRD +{a[+];c*;b[+]}|->G!b,&!PsopraOPRD +{a*;c[+];b[+]}|->!Gb,&PraRD +{a[+];c*;b[+]}|->F!b,&!PraRD +{a[+];c[+];b*}|->GFa,&!PraRD {a*;c[+];b[+]}|->FGa,&!Pa -{a;c;b|(d;e)}|->!Xb,&fPFsgopra -{a;c;b|(d;e)}|->X!b,&!fPFsgopra -{a;c;b|(d;e)}|->!Fb,&Psopra -{a;c;b|(d;e)}|->G!b,&!Psopra -{a;c;b|(d;e)}|->!Gb,&Pgopra -{a;c;b|(d;e)}|->F!b,&!Pgopra -{a;c;b|(d;e)}|->GFa,&!Pra -{a;c;b|(d;e)}|->FGa,&!Ppa -{a[+] && c[+]}|->!Xb,&fPsopra -{a[+] && c[+]}|->X!b,&!fPsopra -{a[+] && c[+]}|->!Fb,&xPsopra -{a[+] && c[+]}|->G!b,&!xPsopra -{a[+] && c[+]}|->!Gb,&xPra -{a[+] && c[+]}|->F!b,&!xPra -{a[+] && c[+]}|->GFa,&!xPra +{a;c;b|(d;e)}|->!Xb,&fPFsgopraOPRD +{a;c;b|(d;e)}|->X!b,&!fPFsgopraOPRD +{a;c;b|(d;e)}|->!Fb,&PsopraOPRD +{a;c;b|(d;e)}|->G!b,&!PsopraOPRD +{a;c;b|(d;e)}|->!Gb,&PgopraOPRD +{a;c;b|(d;e)}|->F!b,&!PgopraOPRD +{a;c;b|(d;e)}|->GFa,&!PraRD +{a;c;b|(d;e)}|->FGa,&!PpaPD +{a[+] && c[+]}|->!Xb,&fPsopraOPRD +{a[+] && c[+]}|->X!b,&!fPsopraOPRD +{a[+] && c[+]}|->!Fb,&xPsopraOPRD +{a[+] && c[+]}|->G!b,&!xPsopraOPRD +{a[+] && c[+]}|->!Gb,&xPraRD +{a[+] && c[+]}|->F!b,&!xPraRD +{a[+] && c[+]}|->GFa,&!xPraRD {a[+] && c[+]}|->FGa,&!xPa -{a;c*;b}<>->!Gb,&Pgopra -{a;c*;b}<>->F!b,&!Pgopra -{a;c*;b}<>->FGb,&!Ppa -{a;c*;b}<>->!GFb,&Ppa +{a;c*;b}<>->!Gb,&PgopraOPRD +{a;c*;b}<>->F!b,&!PgopraOPRD +{a;c*;b}<>->FGb,&!PpaPD +{a;c*;b}<>->!GFb,&PpaPD {a;c*;b}<>->GFb,&!Pa {a;c*;b}<>->!FGb,&Pa {a*;c[+];b[+]}<>->!FGb,&Pa -{a;c|d;b}<>->!Gb,&Pgopra -{a;c|d;b}<>->G!b,&!Psopra -{a;c|d;b}<>->FGb,&!Ppa -{a;c|d;b}<>->!GFb,&Ppa -{a;c|d;b}<>->GFb,&!Pra -{a;c|d;_b}<>->!FGb,&Pr +{a;c|d;b}<>->!Gb,&PgopraOPRD +{a;c|d;b}<>->G!b,&!PsopraOPRD +{a;c|d;b}<>->FGb,&!PpaPD +{a;c|d;b}<>->!GFb,&PpaPD +{a;c|d;b}<>->GFb,&!PraRD +{a;c|d;_b}<>->!FGb,&PrRD # Equivalent to a&b&c&d -{a:b:c:d}!,B&!xfLPSFsgopra -a&b&c&d,B&!xfLPSFsgopra -(Xa <-> XXXc) U (b & Fe),LPgopra -(!X(a|X(!b))&(FX(g xor h)))U(!G(a|b)),LPegopra -(!X(a|X(!b))&(GX(g xor h)))R(!F(a|b)),LPusopra -(!X(a|X(!b))&(GX(g xor h)))U(!G(a|b)),LPeopra -(!X(a|X(!b))&(FX(g xor h)))R(!F(a|b)),LPuopra -(!X(a|X(!b))&(GX(g xor h)))U(!F(a|b)),LPpa -(!X(a|X(!b))&(FX(g xor h)))R(!G(a|b)),LPra -(!X(a|GXF(!b))&(FGX(g xor h)))U(!F(a|b)),LPpa +{a:b:c:d}!,B&!xfLPSFsgopraOPRD +a&b&c&d,B&!xfLPSFsgopraOPRD +(Xa <-> XXXc) U (b & Fe),LPgopraOPRD +(!X(a|X(!b))&(FX(g xor h)))U(!G(a|b)),LPegopraOPRD +(!X(a|X(!b))&(GX(g xor h)))R(!F(a|b)),LPusopraOPRD +(!X(a|X(!b))&(GX(g xor h)))U(!G(a|b)),LPeopraPD +(!X(a|X(!b))&(FX(g xor h)))R(!F(a|b)),LPuopraRD +(!X(a|X(!b))&(GX(g xor h)))U(!F(a|b)),LPpaPD +(!X(a|X(!b))&(FX(g xor h)))R(!G(a|b)),LPraRD +(!X(a|GXF(!b))&(FGX(g xor h)))U(!F(a|b)),LPpaPD (!X(a|GXF(!b))&(FGX(g xor h)))R(!F(a|b)),LPupa -(!X(a|FXG(!b))&(GFX(g xor h)))R(!G(a|b)),LPra +(!X(a|FXG(!b))&(GFX(g xor h)))R(!G(a|b)),LPraRD (!X(a|FXG(!b))&(GFX(g xor h)))U(!G(a|b)),LPera -(!X(a|GXF(!b))&(FGX(g xor h)))U(!G(a|Fb)),LPepa +(!X(a|GXF(!b))&(FGX(g xor h)))U(!G(a|Fb)),LPepaPD (!X(a|GXF(!b))&(FGX(g xor h)))U(!F(a|Gb)),LPa -(!X(a|FXG(!b))&(GFX(g xor h)))R(!F(a|Gb)),LPura +(!X(a|FXG(!b))&(GFX(g xor h)))R(!F(a|Gb)),LPuraRD (!X(a|FXG(!b))&(GFX(g xor h)))R(!G(a|Fb)),LPa GFa M GFb,&!xLPeua -FGa M FGb,&!xLPeupa +FGa M FGb,&!xLPeupaPD Fa M GFb,&!xLPera -GFa W GFb,&!xLPeura +GFa W GFb,&!xLPeuraRD FGa W FGb,&!xLPeua Ga W FGb,&!xLPupa -Ga W b,&!xLPsopra -Fa M b,&!xLPgopra -{a;b*;c},&!fPsopra -{a;b*;c}!,&!fPgopra +Ga W b,&!xLPsopraOPRD +Fa M b,&!xLPgopraOPRD +{a;b*;c},&!fPsopraOPRD +{a;b*;c}!,&!fPgopraOPRD # The negative normal form is {a;b*;c}[]->1 -!{a;b*;c}!,&fPsopra -{a;b*;p112}[]->0,&!fPsopra -!{a;b*;c.2},&!fPgopr -!{a[+];b*;c[+]},&!fPgopra -!{a[+];b*;c*},&!xfPgopra -{a[+];b*;c[+]},&!fPsopra -{a[+] && b || c[+]},&!fPsopra -{a[+] && b[+] || c[+]},&!xfPsopra -{p[+]:p[+]},&!xfPsoprla -(!p W Gp) | ({(!p[*];(p[+]:(p[*];!p[+])))[:*4][:+]}<>-> (!p W Gp)),&!xPpla -{b[+][:*0..3]},&!fPsopra -{a->c[*]},xfPsopra -{(a[+];b*);c*}<>->d,&!xfPgopra -{first_match(a[+];b*);c*}<>->d,&!fPgopra +!{a;b*;c}!,&fPsopraOPRD +{a;b*;p112}[]->0,&!fPsopraOPRD +!{a;b*;c.2},&!fPgoprOPRD +!{a[+];b*;c[+]},&!fPgopraOPRD +!{a[+];b*;c*},&!xfPgopraOPRD +{a[+];b*;c[+]},&!fPsopraOPRD +{a[+] && b || c[+]},&!fPsopraOPRD +{a[+] && b[+] || c[+]},&!xfPsopraOPRD +{p[+]:p[+]},&!xfPsoprlaOPRD +(!p W Gp) | ({(!p[*];(p[+]:(p[*];!p[+])))[:*4][:+]}<>-> (!p W Gp)),&!xPplaPD +{b[+][:*0..3]},&!fPsopraOPRD +{a->c[*]},xfPsopraOPRD +{(a[+];b*);c*}<>->d,&!xfPgopraOPRD +{first_match(a[+];b*);c*}<>->d,&!fPgopraOPRD +G(Ga U b),&!xLPura +GFb & G(Ga R b),&!xLPuraRD EOF run 0 ../kind input