[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: myjul...@xxxxxxxxx*Date*: Sun, 19 Aug 2018 01:54:48 -0700 (PDT)

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

**Follow-Ups**:

- Prev by Date:
**Re: [tlaplus] Unexpected result of [S -> T] evaluation** - Next by Date:
**Declared variables found undefined during evaluation** - Previous by thread:
**Re: [tlaplus] Unexpected result of [S -> T] evaluation** - Next by thread:
**Re: [tlaplus] How can I verify spec satisfies the properties for infinite states?** - Index(es):