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

*From*: Willy Schultz <will62794@xxxxxxxxx>*Date*: Wed, 15 Sep 2021 08:08:32 -0700 (PDT)*Ironport-hdrordr*: A9a23:nNadlqCzalwnXODlHekn55DYdb4zR+YMi2TDtnoBNSC9F/bz+vxG885rsSMc5AxhP03I3OrwQJVprxvnhOhICad4B8bUYOCkghraEGlahbGStwEIYheOv9K1tp0QDpSXvbbLfChHZLjBkXCF+o0bsai6GcmT7I+0vhVQpENRGtpdBmFCe3im+2JNKzWubqBJbqZ0iPA3wQZJuBwsH6eG77o+MdQrZeemqHpXCiR2ciLPJDPusdtZg4SKbCRwFy1/IlZy6IZny3HMl0jS56mosf23jj/ak0HJ6YhO8eGRuOd+OA==*References*: <546a3817-a702-4930-bb51-1af83da9238en@googlegroups.com> <A11B2B2E-E566-41C3-AEBA-FAA4BA1F7AEF@gmail.com>

Thank you to both Stephan and Igor for the helpful replies. A few thoughts in response.

Apalache assumes that all constants have been fixed (or that they belong to a finite set that is captured with ConstInit [1]). So for fixed parameters, we can prove inductive invariants. For instance, we have checked safety of the Tendermint consensus by proving an inductive invariant [2]. It is true that invariant violations are often easier to find with Apalache. It basically expands all quantifiers in disjunctions and conjunctions, which is probably what model-based quantifier instantiation has to do anyways. For the same reason, proving inductive invariants with Apalache takes longer, as the solver cannot use the structure of the quantified formulas to easily show unsatisfiability.

In general, if we work over only finite domains, can't all SMT problems, in theory, be reduced to plain (i.e. boolean) SAT? Not suggesting this is necessarily more efficient than using some finite encoding with an SMT solver, but I just want to clarify the theoretical hardness of the problem.

Yes, that is interesting. It would be also interesting to compare inductiveness checking when using predefined bounds on the data structures. We have recently introduced the operator `Apalache!Gen` that tells the model checker to produce data structures of bounded sizes [3], similar to generators in property-based testing. Intuitively, this is another instance of the small model hypothesis.

Yes, the "small model hypothesis" indeed seems to come into play here. It also seems to be exploited more concretely by recent tools like ic3po [1], which use Ivy as an input language but search for inductive invariants over finite domains, and then generalize them to the unbounded domain.

[1] https://link.springer.com/chapter/10.1007/978-3-030-76384-8_9

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/b70abf32-886d-4e45-b215-2b7cf74278a8n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Inductive Invariants and Counterexamples in TLAPS***From:*Igor Konnov

**References**:**[tlaplus] Inductive Invariants and Counterexamples in TLAPS***From:*Willy Schultz

**Re: [tlaplus] Inductive Invariants and Counterexamples in TLAPS***From:*Igor Konnov

- Prev by Date:
**[tlaplus] Re: Unexpected access to operator through CONSTANT** - Next by Date:
**Re: [tlaplus] Inductive Invariants and Counterexamples in TLAPS** - Previous by thread:
**Re: [tlaplus] Inductive Invariants and Counterexamples in TLAPS** - Next by thread:
**Re: [tlaplus] Inductive Invariants and Counterexamples in TLAPS** - Index(es):