Hello Smruti,
for checking if an invariant Inv is inductive you model check Inv for the specification
Inv /\ [][Next]_vars
i.e. you replace the initial condition of your original specification by the invariant.
In order for this to work, the invariant should begin with a typing invariant that contains conjuncts x \in S for each variable, and S must be a set that TLC can enumerate. In particular, Nat cannot be enumerated and you will need to override it by an interval 0 .. N for some value N.
Then, in order to make sure that values stay within that interval despite incrementation, you need to add a state constraint that ensures that states for which some Nat-valued variable or record component reaches N are discarded. For example, add a constraint "clock < N" so that TLC will never try to increment the clock in a state where clock = N.
By increasing the bound N, you increase your confidence in the result of (bounded) verification.
A corresponding variant of your spec is attached. In order to check that the invariant is inductive, do the following:
- Instantiate the constant largestNat by some value, say 10.
- In the model overview pane, indicate temporal formula CheckInductiveSpec as the behavior spec and InductiveInvariant as the invariant to be checked.
- In the additional spec options, add the predicate StateConstraint as (you guessed it) the state constraint and add a definition override Nat <- 0 .. largestNat.
Now run TLC. You'll see that all states are found when evaluating the initial state predicate (InductiveInvariant) whereas the actions do not generate any new states, confirming that the invariant is indeed inductive.
–––
This technique works for "small" state spaces. The note [1] mentioned by Karolis Petrauskas describes a technique for probabilistic invariant checking when state spaces are too big.
Regards,
Stephan