8 Nov
2020
8 Nov
'20
10:20 p.m.
Thank you very much,
In addition, when trying to translate a "concatenation" I get
error message: "unexpected atomic proposition"
E.g. spot.formula("p2;p1&!p2").translate()
Best regards,
Phillipp
On Sun, Nov 8, 2020, 11:59 Alexandre Duret-Lutz <adl(a)lrde.epita.fr> wrote:
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