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 -- Alexandre Duret-Lutz