You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I'm exploring inductive invariants in Quint with Apalache, and it seems to be achieavable with some tweaks to the interface and mode verification for Init. See this example (from the Apalache manual):
/// A spec based on the y2k TLA+ specification from Igor Konnov [1]////// [1]: https://github.com/informalsystems/apalache/blob/main/test/tla/y2k.tlamodule y2k {
const birth_year: int
const license_age: int
var year: int
var has_license: bool
val age = year - birth_year
pure def increment_year(old_year: int): int ={(old_year +1)%100// Only two digits were used to store the year!}action new_year = all {
year' = increment_year(year),
has_license' = has_license
}action issue_license = all {
age >= license_age,
has_license' = true,
year' = year,}action init = all {
year' = birth_year,
has_license' = false,}action step = any {
new_year,
issue_license,}
val safety = has_license implies (age >= license_age)
val inv = year.in(0.to(99))and has_license.in(Bool)action inv_as_action = all {
nondet y =0.to(99).oneOf()
year' = y,
nondet b =Bool.oneOf()
has_license' = b,}}module y2k_instance {importy2k(birth_year=80, license_age=18).*}
IndInit:
$ quint verify --init=init --invariant=inv --max-steps=0 --main=y2k_instance inductive_invariant.qnt
[ok] No violation found (83ms).
You may increase --max-steps.
Use --verbosity to produce more (or less) output.
IndNext:
$ quint verify --init=inv_as_action --invariant=inv --max-steps=1 --main=y2k_instance inductive_invariant.qnt
[ok] No violation found (121ms).
You may increase --max-steps.
Use --verbosity to produce more (or less) output.
IndProp:
$ quint verify --init=inv_as_action --invariant=safety --max-steps=1 --main=y2k_instance inductive_invariant.qnt
An example execution:
[State 0] { y2k_instance::y2k::has_license: true, y2k_instance::y2k::year: 0 }
[violation] Found an issue (145ms).
error: found a counterexample
The worst part of it is that we need to write an action version of inv to be used as init in IndNext and IndProp, which might not be trivial. The thing is, we can simply remove some restrictions from Quint, and use the predicate directly, since apalache does accept that.
So my idea is:
Create a command that verifies inductive invariants
take init, inv and prop (optional) as arguments.
call Apalache 2-3 times verifying each part
if there is an error, properly report it with information about at which stage the error occurred.
The text was updated successfully, but these errors were encountered:
I mean that, in this new command, quint shouldn't complain if your init is actually a predicate. Currently, Quint expects init to be an action and will complain if you give an invariant as init. We can remove this check from quint, and apalache should accept it normally. Makes sense?
I'm exploring inductive invariants in Quint with Apalache, and it seems to be achieavable with some tweaks to the interface and mode verification for Init. See this example (from the Apalache manual):
IndInit:
IndNext:
IndProp:
The worst part of it is that we need to write an action version of
inv
to be used asinit
in IndNext and IndProp, which might not be trivial. The thing is, we can simply remove some restrictions from Quint, and use the predicate directly, since apalache does accept that.So my idea is:
The text was updated successfully, but these errors were encountered: