Hi Philipp,
On Sun, Nov 8, 2020 at 9:36 AM Philipp schwartz pschwartz090@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