NuSMV at least 5 time steps to win

Question

I have an NuSMV program and I need to specify in either CTL or LTL that the program (which is a game) can't be won in less than 5 time steps. Or more formal: There are at least 5 time steps needed to win the game.

I don't have an explicit time variable, and I wouldn't want to make one for the verification. Is there some way to count the amount of transitions already made? The amount of visited states, something like that?

At the moment I have this:

SPEC ( (gameState != WIN) U (how to count time steps?))

Answer 1

BEST of my knowledge, you have to use an extra variable for specifying time, and increment the time at each step. In prisim you can specify time interval but not in NuSMV.

Answer 2

IT's an old question, but yes you can using:

COMPUTE MIN [initial state, end state]