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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Fri, 23 Apr 2021 09:07:07 +0200*Ironport-hdrordr*: A9a23:UA8HGa0EOjxUFfrELr2PAwqjBFYkLtp033Aq2lEZdDV+dMuEm8ey2MkKzBOcslcscVwphNzoAtjmfVry7phwiLN+AZ6HUBP9sGWlaKFuhLGSoQHIPy37+qpj2bx7c654YeeRMXFAgcz34Ba1Hr8bqbHtmszGuc7kw3hgVg1sYa17hj0JbzqzKFF8RwVNGPMCZfmhz/dAzgDQHUg/X4CSAWQEYOjZu8ejruOeXTc2Qzou6AyDllqTmdjHOind4RcETykK+70r9m/InmXCi5mejw==*References*: <90b306a3-c413-4b09-810e-98aedb44d91fn@googlegroups.com> <BA49039D-022B-486C-B57A-D7DFC676F265@gmail.com> <d9af2d7a-f150-422f-956a-98b6b69f7843n@googlegroups.com> <A085D874-3F90-4D91-B89C-28C06ED3AB4D@gmail.com> <189be644-18f8-40ae-9584-b552fc0c5842n@googlegroups.com>

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 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**

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. |

**Follow-Ups**:**Re: [tlaplus] TLAPS proof of increment and update***From:*Smruti Padhy

**References**:**[tlaplus] TLAPS proof of increment and update***From:*Smruti Padhy

**Re: [tlaplus] TLAPS proof of increment and update***From:*Stephan Merz

**Re: [tlaplus] TLAPS proof of increment and update***From:*Smruti Padhy

**Re: [tlaplus] TLAPS proof of increment and update***From:*Stephan Merz

**Re: [tlaplus] TLAPS proof of increment and update***From:*Smruti Padhy

- Prev by Date:
**[tlaplus] CSP vs. TLA+** - Next by Date:
**[tlaplus] Re: CSP vs. TLA+** - Previous by thread:
**Re: [tlaplus] TLAPS proof of increment and update** - Next by thread:
**Re: [tlaplus] TLAPS proof of increment and update** - Index(es):