# NuSMV - How to indicate the execution should visit some states infinitely often?

I have the following kripke structure:

I need my model to follow the LTL constraint that state d will be visited infinitely often:

LTLSPEC  G F (modelState=d)


This constraint fails due to existence of the loop .... b->c->b->c ......

Question: What would be a solution to this problem? This may be related to fair traces, but I am not very familiar with that, or how to indicate d as a fair state in NuSMV.

I am learning model checking on my own and I appreciate your help very much.