VCGenerator should annotate decomposed invariants

[konnov]

Is your feature request related to a problem? Please describe

VCGenerator decomposes state invariants like Inv == A /\ B into smaller pieces such as Inv$0 == A and Inv$1 == B. These pieces are propagated into InvariantViolation in the counterexamples. While it works, usability is not great. It's actually quite hard to see, which part (A or B) has been violated.

Describe the solution you'd like

Annotate the violated subformula with the definitions that it includes, e.g., Inv/A or Inv/B.

Describe the impact on your work

It will definitely make it easier for me to debug invariant violations.

[konnov]

This has always been a hard nut. I think I have found a solution that would work with TLA+, but then what about Quint.

After several hours of trial and error, I have an amazing solution for TLA+ that has always been there. It's TLA+ labels! Look at this one:

----------- MODULE t ---------------
EXTENDS Integers

VARIABLE
    \* @type: Int;
    x

Init == x = 0

Next == x' = x + 1

Inv ==
    /\ Lemma1 :: x >= 0
    /\ Lemma2 :: x < 10                                                                                                          
====================================

Let's check this spec:

$ apalache-mc check --inv=Inv t.tla
...
Check the trace in: [redacted]/_apalache-out/t.tla/2024-09-30T20-39-07_11757565786153457186/violation1.tla

$ tail [redacted]/_apalache-out/t.tla/2024-09-30T20-39-07_11757565786153457186/violation1.tla

(* Transition 0 to State10 *)
State10 == x = 10

(* The following formula holds true in the last state and violates the invariant *)
InvariantViolation == Lemma2 :: (x >= 10)

================================================================================

This is so simple and beautiful at the same time.

@bugarela any ideas how we could produce labels in Quint? It's a huge usability unlock, for real. We could do the same for actions, as people have been constantly asking about something like labels.

[bugarela]

Hi, this looks amazing! What do you mean by produce here?

1. Have something equivalent to TLA+ labels in the Quint syntax; or
2. Have Quint introduce something when combining multiple invariants into q::inv that can get the translation to Apalache IR to contain the labels for each original invariant

[konnov]

Hi, this looks amazing! What do you mean by produce here?

1. Have something equivalent to TLA+ labels in the Quint syntax; or

Yes, it would be great to have something like TLA+ labels in the Quint syntax. This would help us to annotate some parts of the code. They probably do not need to have exactly the same syntax, just a way to annotate an expression, similar to TLA+ labels.

2. Have Quint introduce something when combining multiple invariants into q::inv that can get the translation to Apalache IR to contain the labels for each original invariant

Well, if we have labels in Quint, I would assume that we would have to translate them to TLA+ labels, to benefit from that feature.