From 66a3b6f7cbdc836216a8a5c187a0d48a68eaa826 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 19 May 2019 09:12:59 +0200 Subject: [PATCH] tl: fix the definition of ##[i:j] Reported by Victor Khomenko. * NEWS, doc/tl/tl.tex, spot/tl/formula.cc: Fix the definition. * tests/core/ltl2tgba.test: Add some test cases. --- NEWS | 9 +++++---- doc/tl/tl.tex | 25 ++++++++++++++++--------- spot/tl/formula.cc | 27 ++++++++++++++++++++------- tests/core/ltl2tgba.test | 13 ++++++++++++- 4 files changed, 53 insertions(+), 21 deletions(-) diff --git a/NEWS b/NEWS index 5ce805559..a3d332185 100644 --- a/NEWS +++ b/NEWS @@ -60,10 +60,11 @@ New in spot 2.7.4.dev (not yet released) - 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 - {a:{[*i..j];b}}. The formula::sugar_delay() function implement - this SVA operator in terms of the existing PSL operators. - ##[+] and ##[*] are sugar for ##[1:$] and ##[0:$]. + way to write {[*2];a:b[+];c;1;e}. The syntax {a ##[i:j] b} is + replaced in different ways depending on the values of i, a, and b. + The formula::sugar_delay() function implement this SVA operator in + terms of the existing PSL operators. ##[+] and ##[*] are sugar + for ##[1:$] and ##[0:$]. - spot::relabel_apply() make it easier to reverse the effect of spot::relabel() or spot::relabel_bse() on formula. diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index b0c42ef48..289c4fdc6 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -775,16 +775,23 @@ $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\\ - f\DELAYR{..} g &\equiv f\FUSION\{\STAR{}\CONCAT g\} & f\DELAYR{\mvar{i}..} g &\equiv f\FUSION\{\STAR{\mvar{i}..}\CONCAT g\} \\ - f\DELAYR{..\mvar{j}} g &\equiv f\FUSION\{\STAR{0..\mvar{j}}\CONCAT g\} & - f\DELAYR{\mvar{i}..\mvar{j}} g &\equiv f\FUSION\{\STAR{\mvar{i}..\mvar{j}}\CONCAT g\} \\ - {}\DELAYR{..} g &\equiv \STAR{}\CONCAT g & {}\DELAYR{\mvar{i}..} g &\equiv \STAR{\mvar{i}..}\CONCAT g \\ - {}\DELAYR{..\mvar{j}} g &\equiv \STAR{0..\mvar{j}}\CONCAT g & - {}\DELAYR{\mvar{i}..\mvar{j}} g &\equiv \STAR{\mvar{i}..\mvar{j}}\CONCAT g \\ - f \DELAYP{} g & \equiv f \DELAYR{1..} g & f \DELAYS{} g & \equiv f \DELAYR{0..} g \\ - \DELAYP{} g & \equiv \DELAYR{1..} g & \DELAYS{} g & \equiv \DELAYR{0..} g + f\DELAYR{\mvar{i}..\mvar{j}}g & \equiv f\CONCAT{}\1\STAR{\mvar{i-1}..\mvar{j-1}}\CONCAT{}g\quad\text{if~}i>0 \\ + f\DELAYR{0..\mvar{j}}g & \equiv f\FUSION(\1\STAR{0..\mvar{j}}\CONCAT{}g)\quad\text{if~}\varepsilon\nVDash f \\ + f\DELAYR{0..\mvar{j}}g & \equiv (f\CONCAT{}\1\STAR{0..\mvar{j}})\FUSION{}g)\quad\text{if~}\varepsilon\VDash f \land \varepsilon\nVDash g \\ + f\DELAYR{0..\mvar{j}}g & \equiv (f\FUSION{}g)\OR(f\CONCAT{}\1\STAR{0..\mvar{j-1}}\CONCAT{}g)\quad\text{if~}\varepsilon\VDash f \land \varepsilon\VDash g \\ + f\DELAYR{\mvar{i}..}g & \equiv f\CONCAT{}\1\STAR{\mvar{i-1}..}\CONCAT{}g\quad\text{if~}i>0 \\ + f\DELAYR{0..}g & \equiv f\FUSION(\1\STAR{}\CONCAT{}g)\quad\text{if~}\varepsilon\nVDash f \\ + f\DELAYR{0..}g & \equiv (f\CONCAT{}\1\STAR{})\FUSION{}g)\quad\text{if~}\varepsilon\VDash f \land \varepsilon\nVDash g \\ + f\DELAYR{0..}g & \equiv (f\FUSION{}g)\OR(f\CONCAT{}\1\STAR{}\CONCAT{}g)\quad\text{if~}\varepsilon\VDash f \land \varepsilon\VDash g \end{align*} +\begin{align*} + f\DELAY{\mvar{i}} g & \equiv f\DELAYR{\mvar{i}..\mvar{i}} g & {}\DELAY{\mvar{i}} g & \equiv \1\DELAYR{\mvar{i}..\mvar{i}} g \\ + f\DELAYP{}g & \equiv f\DELAYR{1..}g & \DELAYP{} g & \equiv\DELAYR{1..}g \\ + f\DELAYS{}g & \equiv f\DELAYR{0..}g & \DELAYS{} g & \equiv\DELAYR{0..}g + f\DELAYR{..\mvar{j}} g & \equiv f\DELAYR{0..\mvar{j}} g\} & \DELAYR{..\mvar{j}} g & \equiv \1\DELAYR{0..\mvar{j}} g\} \\ + f\DELAYR{..} g & \equiv f\DELAYR{0..} f g\} & \DELAYR{..} g & \equiv \1\DELAYR{0..} g\} \\ +\end{align*} + \subsection{Trivial Identities (Occur Automatically)} The following identities also hold if $j$ or $l$ are missing (assuming diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc index f6f4dbcfa..f31c974b5 100644 --- a/spot/tl/formula.cc +++ b/spot/tl/formula.cc @@ -1776,16 +1776,29 @@ namespace spot formula formula::sugar_delay(const formula& a, const formula& b, unsigned min, unsigned max) { - // In general - // a ##[min:max] b = a:(1[*min:max];b) - // however if min>=1 we prefer the following rule + // If min>=1 // a ##[min:max] b = a;1[*min-1:max-1];b - if (min == 0) - return Fusion({a, Concat({Star(tt(), min, max), b})}); - --min; + // If min==0 we can use + // a ##[min:max] b = a:(1[*0:max];b) if a rejects [*0] + // a ##[min:max] b = (a;1[*0:max]):b if b rejects [*0] + // a ##[min:max] b = (a:b)|(a;[*0:max-1];b) else + if (min > 0) + { + --min; + if (max != unbounded()) + --max; + return Concat({a, Star(tt(), min, max), b}); + } + if (!a.accepts_eword()) + return Fusion({a, Concat({Star(tt(), 0, max), b})}); + if (!b.accepts_eword()) + return Fusion({Concat({a, Star(tt(), 0, max)}), b}); + if (max != unbounded()) --max; - return Concat({a, Star(tt(), min, max), b}); + formula left = Fusion({a, b}); + formula right = Concat({a, Star(tt(), 0, max), b}); + return OrRat({left, right}); } int atomic_prop_cmp(const fnode* f, const fnode* g) diff --git a/tests/core/ltl2tgba.test b/tests/core/ltl2tgba.test index b1ede0f1b..ccb892f75 100755 --- a/tests/core/ltl2tgba.test +++ b/tests/core/ltl2tgba.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009-2018 Laboratoire de Recherche et Développement de +# 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), Université @@ -218,6 +218,17 @@ ltlfilt -q -r -f '{{a*}[:+];c}' --equivalent-to 'Xc R a' ltlfilt -q -f '{c && {b | [*0]}[:+]}' --equivalent-to 'c & b' ltlfilt -q -r -f '{c && {b | [*0]}[:+]}' --equivalent-to 'c & b' + +# The ##[i:j] operator introduced in 2.8 has four different rewritings +# depending on whether a or b accepts [*0]. + +for a in 'a1;a2' 'a1[*];a2[*]'; do + for b in 'b1;b2' 'b1[*];b2[*]'; do + ltlfilt -q -f "{($a) ##[0:8] ($b)}[]->c" \ + --equivalent-to "{(($a):($b))|(($a);[*0:7];($b))}[]->c" || exit 1 + done +done + # test unknown dot options ltl2tgba --dot=@ a 2>stderr && exit 1 grep 'ltl2tgba: unknown option.*@' stderr