Re: [tlaplus] TLAPS proof of increment and update

[Stephan Merz <stephan.merz@xxxxxxxxx>]

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

[1] https://lamport.azurewebsites.net/tla/inductive-invariant.pdf

--
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/4EB026AA-BF8D-40F8-BEB4-9B9670804FAC%40gmail.com.

Attachment: inc_spec.tla
Description: Binary data

On 20 Apr 2021, at 08:39, Smruti Padhy <smruti.padhy@xxxxxxxxx> wrote:

Thank you so much, Stephen for the detailed example.  It helped me a lot.

One quick question - Can this inductive invariant can be checked in the TLC model checker to check to get. an idea if it is a candidate inductive invariant? It involves Nat. I tried doing it by setting Nat to a small number but it shows the error : 

Attempted to enumerate a set of the form [l1 : v1, ..., ln : vn],

but can't enumerate the value of the `val' field:Nat

I think I am missing some assumptions in the spec or in the TLC settings. 

Best,

Smruti

On Thursday, April 15, 2021 at 2:00:25 AM UTC-5 Stephan Merz wrote:

Hello again,

my initial message was perhaps a little cryptic, so let me explain the rationale behind it. You were effectively trying to prove the implication

TypeInvariant /\ SafetyProperty /\ Inc => SafetyProperty'

but this implication doesn't hold. As a concrete counter-example, consider the state

valX = [ val |-> 42, ts |-> 23 ]

valY = [ val |-> 42, ts |-> 70 ]

clock = 27

(I'm omitting the variable n because it is unimportant for this discussion.)

Observe that this state satisfies both TypeInvariant and SafetyProperty. In particular, the latter holds trivially because the left-hand side of the implication is false. Now, Inc will lead you to the state

valX = [ val |-> 43, ts |-> 28 ]

valY = [ val |-> 42, ts |-> 70 ]

clock = 28

and SafetyProperty is false for that state. This shows that SafetyProperty is not inductive (relative to TypeInvariant).

However, the first state is actually not reachable in your specification, and one way to rule it out is to observe that time stamps cannot exceed the clock value. This observation leads to asserting the invariant ClockInv, which makes the proof go through. Now, in general there is no guarantee that the additional predicate is an inductive invariant: you may have to iterate the process and successively add more information about reachable states in order to obtain an inductive invariant that you can prove with a proof assistant such as TLAPS.

As for model checking, you are completely right that you need to bound the state space that TLC will explore. One standard way to do this is to add a state constraint where you bound the value of clock.

Stephan

On 14 Apr 2021, at 20:22, Smruti Padhy <smruti...@xxxxxxxxx> wrote:

Thank you, Stephan for the detailed proof and for pointing the need for the clock invariant for the safety property proof instead of those conditions as enabling conditions. I will go through examples and tutorials again as it seems I might be missing some basic concepts.

Regarding MaxNum, I added it to limit the number of Inc actions and in turn, limit the number of states during TLC model checking. I couldn't think of a better way to do that. I agree that SpecAssumption is spurious.

Thanks again for the help.

Best,

Smruti

On Tuesday, April 13, 2021 at 12:35:03 PM UTC-5 Stephan Merz wrote:

Hello,

the problem is that your safety property is not an inductive invariant (even with respect to the typing invariant). However, it is easy to see that the time stamps of your variables can never exceed the clock value, and so the extra guard that you added to the Inc action is actually an invariant of your specification. It even happens to be an inductive invariant. 

The attached TLA+ module contains a proof of the safety property. Please see the TLAPS tutorial or other examples in the distribution for the concept and the importance of inductive invariants.

Hope this helps,

Stephan

P.S.: The constant MaxNum is (obviously) unnecessary for the prover – better add a state constraint to the model that you use for TLC instead of adding a spurious precondition in your specification. -s

-- 
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d9af2d7a-f150-422f-956a-98b6b69f7843n%40googlegroups.com.

-- 
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/189be644-18f8-40ae-9584-b552fc0c5842n%40googlegroups.com.

--
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/4EB026AA-BF8D-40F8-BEB4-9B9670804FAC%40gmail.com.