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.  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. Should the word always contain a cycle and a prefix part. If yes, what should be the cycle part and what should be the prefix part. 

I will be waiting for your response.