8 Nov
2020
8 Nov
'20
10:59 a.m.
Hi Philipp,
On Sun, Nov 8, 2020 at 9:36 AM Philipp schwartz <pschwartz090(a)gmail.com> wrote:
My question is, is it possible to get boolean result
if LTL formula accepts or rejects a word?
e.g. In case the LTL formula is "aUb" is it possible to check that the formula
is accepting "cycle(b)"?
% ltlfilt -f 'a U b' --accept-word 'cycle{b}' -c
1
% ltlfilt -f 'a U b' --accept-word 'cycle{!b}' -c
0
Beware that since AP={a,b} are atomic propositions, cycle{b} is not a
word, but the set of words where b is always true. The --accept-word
option matches any formula that *intersect* the given set, so it just
has to accept one word. (The --reject-word match formulas that do not
intersect the given set, so they have to reject all words.)
As a consequence, the following should not be a surprise:
% ltlfilt -f 'a U b' --accept-word 'cycle{!a}' -c
1
This is because the word cycle{!a & b} which is one of the words
represented by cycle{!a} is accepted by 'a U b'.
Best regards
--
Alexandre Duret-Lutz