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

Re: [tlaplus] TLAPS proof of increment and update

Hi Stephan,
Thank you so much for the detailed explanation and the updated spec example. Now I understand how to define and set state constraints options in TLC. I did not see or aware of the state constraint option in TLC additional spec before this conversation. Thanks again for taking the time to explain that to me.


On Friday, April 23, 2021 at 2:07:11 AM UTC-5 Stephan Merz wrote:
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.



You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/fea20d98-fe85-4082-954f-5a99ee24d35dn%40googlegroups.com.