Commit 90a88d0b authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

tl: fix handling of f##[0:0]g, and of ##[0:n]g

The first issue was reported by Victor Khomenko.

* spot/tl/formula.cc: Introduce a single-argument
version of sugar_delay().
* spot/parsetl/parsetl.yy: Use it.
* doc/tl/tl.tex, spot/tl/formula.hh: Adjust doc.
* tests/core/ltlfilt.test, tests/core/sugar.test: More tests.
parent 66a3b6f7
Pipeline #9298 passed with stages
in 292 minutes and 42 seconds
......@@ -785,11 +785,12 @@ omitted.
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\} \\
\DELAYR{\mvar{i}..\mvar{j}}g & \equiv \1\STAR{\mvar{i}..\mvar{j}}\CONCAT g & \DELAYR{\mvar{i}..}g & \equiv \1\STAR{\mvar{i}..}\CONCAT g \\
f\DELAY{\mvar{i}} g & \equiv f\DELAYR{\mvar{i}..\mvar{i}} g & {}\DELAY{\mvar{i}} g & \equiv \1\STAR{\mvar{i}}\CONCAT 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)}
......
......@@ -541,8 +541,7 @@ sere: booleanatom
| sere OP_FUSION error
{ missing_right_binop($$, $1, @2, "fusion operator"); }
| OP_DELAY_N sere
{ $$ = formula::sugar_delay(formula::tt(), formula($2),
$1, $1).to_node_(); }
{ $$ = formula::sugar_delay(formula($2), $1, $1).to_node_(); }
| OP_DELAY_N error
{ missing_right_binop($$, fnode::tt(), @1, "SVA delay operator"); }
| sere OP_DELAY_N sere
......@@ -557,7 +556,7 @@ sere: booleanatom
error_list.emplace_back(@1, "reversed range");
std::swap($1.max, $1.min);
}
$$ = formula::sugar_delay(formula::tt(), formula($2),
$$ = formula::sugar_delay(formula($2),
$1.min, $1.max).to_node_();
}
| delayargs error
......
......@@ -1773,15 +1773,22 @@ namespace spot
return Concat({Star(Concat({s, b}), min, max), s});
}
formula formula::sugar_delay(const formula& b,
unsigned min, unsigned max)
{
// ##[min:max] b = 1[*min:max];b
return Concat({Star(tt(), min, max), b});
}
formula formula::sugar_delay(const formula& a, const formula& b,
unsigned min, unsigned max)
{
// If min>=1
// a ##[min:max] b = a;1[*min-1:max-1];b
// 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
// a ##[0:0] b = a:b
// a ##[0:max] b = a:(1[*0:max];b) if a rejects [*0]
// a ##[0:max] b = (a;1[*0:max]):b if b rejects [*0]
// a ##[0:max] b = (a:b)|(a;[*0:max-1];b) else
if (min > 0)
{
--min;
......@@ -1789,6 +1796,8 @@ namespace spot
--max;
return Concat({a, Star(tt(), min, max), b});
}
if (max == 0)
return Fusion({a, b});
if (!a.accepts_eword())
return Fusion({a, Concat({Star(tt(), 0, max), b})});
if (!b.accepts_eword())
......
......@@ -1245,9 +1245,25 @@ namespace spot
///
/// The operator does not exist in Spot it is handled as syntactic
/// sugar by the parser. This function is used by the parser to
/// create the equivalent SERE.
/// create the equivalent SERE using PSL operators.
///
/// The rewriting rules depends on the values of a, n, and b.
/// If n≥1 `a ##[n:m] b` is encoded as `a;1[*n-1,m-1];b`.
/// Otherwise:
/// * `a ##[0:0] b` is encoded as `a:b`,
/// * For m>0, `a ##[0:m] b` is encoded as
/// - `a:(1[*0:m];b)` is `a` rejects `[*0]`,
/// - `(a;1[*0:m]):b` is `b` rejects `[*0]`,
/// - `(a:b) | (a;1[*0:m-1];b)` is `a` and `b` accept `[*0]`.
///
/// The left operand can also be missing, in which case
/// `##[n:m] b` is rewritten as `1[*n:m];b`.
/// @{
static formula sugar_delay(const formula& a, const formula& b,
unsigned min, unsigned max);
static formula sugar_delay(const formula& b,
unsigned min, unsigned max);
/// @}
#ifndef SWIG
/// \brief Return the underlying pointer to the formula.
......
......@@ -58,6 +58,7 @@ F(a & !Xa & Xb)
{a*;(!a)*;a[+]}|->b
{a*;(!a)[+];a[+]}|->b
{a*;(!c)[+];a[+]}|->b
{a* ##0 b*}|->c
EOF
checkopt --boolean <<EOF
......@@ -115,10 +116,11 @@ a & (b | c)
{a[+];{!a}[*];a[*]}[]-> b
{a[*];{!a}[*];a[+]}[]-> b
{a[*];{!a}[+];a[+]}[]-> b
{a[*]:b[*]}[]-> c
EOF
checkopt -c --stutter-invariant <<EOF
15
16
EOF
checkopt --syntactic-stutter-invariant <<EOF
......@@ -134,6 +136,7 @@ a & (b | c)
{a[*];{!a}[+];a[*]}[]-> b
{a[+];{!a}[*];a[*]}[]-> b
{a[*];{!a}[*];a[+]}[]-> b
{a[*]:b[*]}[]-> c
EOF
checkopt --simplify <<EOF
......@@ -158,6 +161,7 @@ a R (b W !a)
!a R (a R (b W !a))
!a R (a | X(a R (b W !a)))
!a R (c | X(c R (b W !a)))
(c W !b) W !a
EOF
checkopt --simplify --eventual --unique <<EOF
......@@ -191,6 +195,7 @@ a & (b | c)
{a[*];{!a}[*];a[+]}[]-> b
{a[*];{!a}[+];a[+]}[]-> b
{a[*];{!c}[+];a[+]}[]-> b
{a[*]:b[*]}[]-> c
EOF
checkopt --obligation <<EOF
......@@ -210,6 +215,7 @@ a & (b | c)
{a[*];{!a}[*];a[+]}[]-> b
{a[*];{!a}[+];a[+]}[]-> b
{a[*];{!c}[+];a[+]}[]-> b
{a[*]:b[*]}[]-> c
EOF
checkopt --guarantee <<EOF
......@@ -232,6 +238,7 @@ checkopt -v --ltl <<EOF
{a[*];{!a}[*];a[+]}[]-> b
{a[*];{!a}[+];a[+]}[]-> b
{a[*];{!c}[+];a[+]}[]-> b
{a[*]:b[*]}[]-> c
EOF
checkopt -v --ap=3 <<EOF
......@@ -275,6 +282,7 @@ a & (b | c)
{a[*];{!a}[*];a[+]}[]-> b
{a[*];{!a}[+];a[+]}[]-> b
{a[*];{!c}[+];a[+]}[]-> b
{a[*]:b[*]}[]-> c
EOF
checkopt -v --stutter-invariant <<EOF
......
......@@ -37,12 +37,18 @@ F [2:4] a | b
F [4:2]a | F[2:2]b
F[]a|G[]b|X[]c
{a ##0 b ##1 c ##2 d}|->e
{a* ##0 b* ##1 c* ##2 d*}|->e
{(##2 a)[*] ##1 b}|->e
{a ##[0:3] b}|->e
{a* ##[0:3] b}|->e
{a ##[0:3] b*}|->e
{a* ##[0:3] b*}|->e
{a ##[1..] b}|->e
{a ##[:] b}|->e
{a ##[:1] b}|->e
{##[..3] b}|->e
{##[0..2] b*}|->e
{##[1..2] b*}|->e
{a ##[+] b}|->e
{##[*] b}|->e
EOF
......@@ -62,12 +68,18 @@ b | XX(a | X(a | Xa))
XX(a | X(a | Xa)) | XXb
FGa | Gb | XGc
{{a && b};c;1;d}[]-> e
{{a[*]:b[*]};c[*];1;d[*]}[]-> e
{{[*2];a}[*];b}[]-> e
{a:{[*0..3];b}}[]-> e
{{a[*];[*0..3]}:b}[]-> e
{a:{[*0..3];b[*]}}[]-> e
{{a[*]:b[*]} | {a[*];[*0..2];b[*]}}[]-> e
{a;[*];b}[]-> e
{a:{[*];b}}[]-> e
{a:{[*0..1];b}}[]-> e
{[*0..3];b}[]-> e
{[*0..2];b[*]}[]-> e
{[*1..2];b[*]}[]-> e
{a;[*];b}[]-> e
{[*];b}[]-> e
EOF
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment