How can I verify spec satisfies the properties for infinite states?

[myjul...@xxxxxxxxx]

Hello,

I wonder how can I verify spec satisfies the properties for infinite states.

In my spec, there are infinitely states so TLC is executed infinitely.

In this case, I wonder how can I verify spec satisfies the properties.

For example, 

I want to prove "Theorem Spec  => []TypeInv".

When i check by the bound length constraint because of infinite states, TypeInV is satisfied.

But, I think it can be not proved that spec satisfies the properties for infinitely states by this bounded checking. 

Thanks,

Juliet