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.