Thank you for writing back. I am doing exactly like this. I append cycle{!alive} to my finite word before parsing it to an automaton. but I don't know what should be the length of my prefix i.e. how many steps it should have. I guess its more of a theoretical question, so can you direct me to some source where I can read on this.

Thanks and Regards,

Hashim Ali

Research Assistant

Laboratory for Cyber-Physical Networks and Systems (Cyphynets)

Lahore University of Management Sciences (LUMS)

Hi Hashim

On Mon, Mar 25, 2019 at 1:25 PM hashim ali <hashim_ali94@outlook.com> wrote:
>
> Hi,
> I am using
> spot.from_ltlf().translate()
> to translate LTL rules into a finite automata (with alive property).
> Now I want to verify certain words that whether they are accepted by the automata or not.

Because of from_ltlf(). I believe you are talking about finite words.

> These words will be generated from a powerset of the set of atomic propositions.
> Lets suppose I have AP = {a,b,c,d}. How do I generate words from the powerset of AP and verify it on the automata.

I do not understand what this means.

> Should the word always contain a cycle and a prefix part.

Spot only deals with infinite words that are lasso-shaped. [*]

The cycle part is mandatory, the prefix is not.

If you want to compare some finite words against Büchi automata
generated from the output of from_ltlf(), you should convert your
finite words to use the same convention as in the output of
from_ltlf(): put your finite words as a prefix where "alive" should
also always hold, and add a cycle with !"alive".

E.g. over AP={a,b}, the finite word a&b;a&!b would be encoded as the
infinite word a&b&alive;a&!b&alive;cycle{!alive}.

[*] In fact, because the twa_word object is labeled by Boolean
formulas (and not just conjunctions of litterals), it can actually
represent more than one word; it's more like a set of words with the
same shape. Or a restriction of an automaton to some lasso shape if
you prefer.