alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

tl: fix the definition of ##[i:j]

Browse source 
Reported by Victor Khomenko.

* NEWS, doc/tl/tl.tex, spot/tl/formula.cc: Fix the definition.
* tests/core/ltl2tgba.test: Add some test cases.
This commit is contained in:
Alexandre Duret-Lutz 2019-05-19 09:12:59 +02:00
parent 60bdf5de19
commit 66a3b6f7cb
4 changed files with 53 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

9
NEWS
View file

@ -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.

25
doc/tl/tl.tex
View file

@ -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

23
spot/tl/formula.cc
View file

@ -1776,17 +1776,30 @@ 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})});
// 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;
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)
{

13
tests/core/ltl2tgba.test
View file

@ -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