check: surprising temporal NoError result

[lucab]

System information

• Apalache version: 0.45.4 | build: 99508e4 (latest release)
• OS: Linux, Ubuntu 24.04 (latest release)
• JDK version [e.g. OpenJDK 0.8.0]: openjdk 21.0.4

Description

This is a bug report forwarded from Quint: informalsystems/quint#1501

The original Quint specification was:

module buggyTemporals {
    var myState: int
    action init = myState' = 0
    action step = { myState' = myState + 1 }
    temporal temporalProps = always(myState < 0)
}

quint verify (with Apalache) fails to find a counterexample for temporalProps.
I followed @bugarela's suggestions and translated the Quint file to TLA+ then directly checked with Apalache, below is the full ouput.

Details

TLA+ specification (autogenerated by quint compile):

---------------------------- MODULE buggyTemporals ----------------------------

EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache, Variants

VARIABLE
  (*
    @type: Int;
  *)
  myState

(*
  @type: (() => Bool);
*)
step == myState' := (myState + 1)

(*
  @type: (() => Bool);
*)
temporalProps == [](myState < 0)

(*
  @type: (() => Bool);
*)
init == myState' := 0

(*
  @type: (() => Bool);
*)
q_init == init

(*
  @type: (() => Bool);
*)
q_step == step

(*
  @type: (() => Bool);
*)
q_temporalProps == temporalProps

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

Config:

PROPERTIES
q_temporalProps

INIT
q_init

NEXT
q_step

Command:

apalache-mc check --config=buggyTemporals.cfg buggyTemporals.tla

Output:

16:11:50.998 [main] INFO at.forsyte.apalache.tla.tooling.opt.CheckCmd -- Loading configuration
# Usage statistics is OFF. We care about your privacy.
# If you want to help our project, consider enabling statistics with config --enable-stats=true.

Output directory: /tmp/_apalache-out/buggyTemporals.tla/2024-09-09T16-11-51_11624426143651718720
# APALACHE version: 0.45.4 | build: 99508e4                       I@16:11:51.285
  > buggyTemporals.cfg: Loading TLC configuration                 I@16:11:51.306
  > Using init predicate(s) q_init from the TLC config            I@16:11:51.351
  > Using next predicate(s) q_step from the TLC config            I@16:11:51.351
  > Using temporal predicate(s) q_temporalProps from the TLC config I@16:11:51.351
Tuning: search.outputTraces=false                                 I@16:11:51.352
PASS #0: SanyParser                                               I@16:11:51.528
Parsing file /tmp/buggyTemporals.tla
Parsing file /tmp/Integers.tla
Parsing file /tmp/__rewire_sequences_in_apalache.tla
Parsing file /tmp/FiniteSets.tla
Parsing file /tmp/__rewire_tlc_in_apalache.tla
Parsing file /tmp/Apalache.tla
Parsing file /tmp/Variants.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/__apalache_folds.tla
PASS #1: TypeCheckerSnowcat                                       I@16:11:51.783
 > Running Snowcat .::.                                           I@16:11:51.783
 > Your types are purrfect!                                       I@16:11:52.064
 > All expressions are typed                                      I@16:11:52.065
PASS #2: ConfigurationPass                                        I@16:11:52.065
  > buggyTemporals.cfg: found PROPERTIES: q_temporalProps         I@16:11:52.190
  > Set the initialization predicate to q_init                    I@16:11:52.191
  > Set the transition predicate to q_step                        I@16:11:52.191
  > Set a temporal property to q_temporalProps                    I@16:11:52.192
PASS #3: DesugarerPass                                            I@16:11:52.194
  > Desugaring...                                                 I@16:11:52.194
PASS #4: InlinePass                                               I@16:11:52.201
Leaving only relevant operators: CInitPrimed, q_init, q_initPrimed, q_step, q_temporalProps I@16:11:52.202
PASS #5: TemporalPass                                             I@16:11:52.223
  > Rewriting temporal operators...                               I@16:11:52.223
  > Found 1 temporal properties                                   I@16:11:52.227
  > Adding logic for loop finding                                 I@16:11:52.227
PASS #6: InlinePass                                               I@16:11:52.248
Leaving only relevant operators: CInitPrimed, q_init, q_initPrimed, q_step, q_temporalProps I@16:11:52.248
PASS #7: PrimingPass                                              I@16:11:52.250
  > Introducing q_initPrimed for q_init'                          I@16:11:52.251
PASS #8: VCGen                                                    I@16:11:52.252
  > Producing verification conditions from the invariant q_temporalProps I@16:11:52.252
  > VCGen produced 1 verification condition(s)                    I@16:11:52.253
PASS #9: PreprocessingPass                                        I@16:11:52.255
  > Before preprocessing: unique renaming                         I@16:11:52.255
 > Applying standard transformations:                             I@16:11:52.260
  > PrimePropagation                                              I@16:11:52.260
  > Desugarer                                                     I@16:11:52.261
  > UniqueRenamer                                                 I@16:11:52.263
  > Normalizer                                                    I@16:11:52.264
  > Keramelizer                                                   I@16:11:52.265
  > After preprocessing: UniqueRenamer                            I@16:11:52.268
PASS #10: TransitionFinderPass                                    I@16:11:52.270
  > Found 1 initializing transitions                              I@16:11:52.284
  > Found 2 transitions                                           I@16:11:52.288
  > No constant initializer                                       I@16:11:52.289
  > Applying unique renaming                                      I@16:11:52.289
PASS #11: OptimizationPass                                        I@16:11:52.291
 > Applying optimizations:                                        I@16:11:52.300
  > ConstSimplifier                                               I@16:11:52.300
  > ExprOptimizer                                                 I@16:11:52.302
  > SetMembershipSimplifier                                       I@16:11:52.303
  > ConstSimplifier                                               I@16:11:52.304
PASS #12: AnalysisPass                                            I@16:11:52.306
 > Marking skolemizable existentials and sets to be expanded...   I@16:11:52.307
  > Skolemization                                                 I@16:11:52.307
  > Expansion                                                     I@16:11:52.308
  > Remove unused let-in defs                                     I@16:11:52.308
 > Running analyzers...                                           I@16:11:52.309
  > Introduced expression grades                                  I@16:11:52.311
PASS #13: BoundedChecker                                          I@16:11:52.311
State 0: Checking 1 state invariants                              I@16:11:52.510
State 0: state invariant 0 holds.                                 I@16:11:52.511
Step 0: picking a transition out of 1 transition(s)               I@16:11:52.513
State 1: Checking 1 state invariants                              I@16:11:52.523
State 1: state invariant 0 holds.                                 I@16:11:52.524
Step 1: Transition #1 is disabled                                 I@16:11:52.532
Step 1: picking a transition out of 1 transition(s)               I@16:11:52.533
State 2: Checking 1 state invariants                              I@16:11:52.539
State 2: state invariant 0 holds.                                 I@16:11:52.540
State 2: Checking 1 state invariants                              I@16:11:52.548
State 2: state invariant 0 holds.                                 I@16:11:52.549
Step 2: picking a transition out of 2 transition(s)               I@16:11:52.551
State 3: Checking 1 state invariants                              I@16:11:52.563
State 3: state invariant 0 holds.                                 I@16:11:52.565
State 3: Checking 1 state invariants                              I@16:11:52.572
State 3: state invariant 0 holds.                                 I@16:11:52.573
Step 3: picking a transition out of 2 transition(s)               I@16:11:52.574
State 4: Checking 1 state invariants                              I@16:11:52.583
State 4: state invariant 0 holds.                                 I@16:11:52.584
State 4: Checking 1 state invariants                              I@16:11:52.590
State 4: state invariant 0 holds.                                 I@16:11:52.591
Step 4: picking a transition out of 2 transition(s)               I@16:11:52.592
State 5: Checking 1 state invariants                              I@16:11:52.600
State 5: state invariant 0 holds.                                 I@16:11:52.602
State 5: Checking 1 state invariants                              I@16:11:52.608
State 5: state invariant 0 holds.                                 I@16:11:52.609
Step 5: picking a transition out of 2 transition(s)               I@16:11:52.610
State 6: Checking 1 state invariants                              I@16:11:52.617
State 6: state invariant 0 holds.                                 I@16:11:52.618
State 6: Checking 1 state invariants                              I@16:11:52.623
State 6: state invariant 0 holds.                                 I@16:11:52.624
Step 6: picking a transition out of 2 transition(s)               I@16:11:52.624
State 7: Checking 1 state invariants                              I@16:11:52.630
State 7: state invariant 0 holds.                                 I@16:11:52.631
State 7: Checking 1 state invariants                              I@16:11:52.636
State 7: state invariant 0 holds.                                 I@16:11:52.637
Step 7: picking a transition out of 2 transition(s)               I@16:11:52.637
State 8: Checking 1 state invariants                              I@16:11:52.645
State 8: state invariant 0 holds.                                 I@16:11:52.648
State 8: Checking 1 state invariants                              I@16:11:52.655
State 8: state invariant 0 holds.                                 I@16:11:52.656
Step 8: picking a transition out of 2 transition(s)               I@16:11:52.657
State 9: Checking 1 state invariants                              I@16:11:52.665
State 9: state invariant 0 holds.                                 I@16:11:52.667
State 9: Checking 1 state invariants                              I@16:11:52.678
State 9: state invariant 0 holds.                                 I@16:11:52.679
Step 9: picking a transition out of 2 transition(s)               I@16:11:52.680
State 10: Checking 1 state invariants                             I@16:11:52.688
State 10: state invariant 0 holds.                                I@16:11:52.690
State 10: Checking 1 state invariants                             I@16:11:52.696
State 10: state invariant 0 holds.                                I@16:11:52.697
Step 10: picking a transition out of 2 transition(s)              I@16:11:52.698
The outcome is: NoError                                           I@16:11:52.704
Checker reports no error up to computation length 10              I@16:11:52.704
It took me 0 days  0 hours  0 min  1 sec                          I@16:11:52.704
Total time: 1.418 sec                                             I@16:11:52.705
EXITCODE: OK

I sanity-checked the TLA+ specification (after some minor fixes) with TLC and it correctly finds the counterexample:

Error: Invariant temporalProps is violated by the initial state:
myState = 0

Triage checklist (for maintainers)

• Reproduce the bug on the main development branch.
• Add the issue to the apalache GitHub project.
• If the bug is high impact, ensure someone available is assigned to fix it.

[konnov]

Thanks for submitting the report @lucab! I have been starring at the spec for some time, before I realized that the counter keeps incrementing. Technically, the liveness-to-safety reduction works only on finite-state systems. This explains why you were able to find a counterexample when you bounded myState in informalsystems/quint#1501.

However, there is another subtle issue at play here. It looks like the liveness reduction does not assume Next to be stuttering. If I change q_step as q_step == step \/ UNCHANGED myState instead of just step, Apalache finds a loop. It's a bit surprising though that it does not find a self-loop but finds a loop of length 2.

@p-offtermatt could you have a look? I am not really surprised about the behavior on an infinitely-increasing counter, though the example is quite simple. But I am surprised that the minimal counterexample is of length 2, when we add stuttering. Also, do you remember, why we decided not to add stuttering by default?

[p-offtermatt]

You are exactly right about the incrementing counter - it is a limitation of the current implementation that to decide liveness properties, we need an execution that has a loop (as in, coming back back to a state we have already visited and thus finding an execution that can loop infinitely).

For the counterexample, if I understand correctly, this is the answer:
Apalache first nondeterministically chooses for a state to be the start of the loop, and it then needs to find this same state again. Meaning, counterexamples for temporal properties need to have at least two states (state 0 starts the loop, and then state 1==state 0 ends the loop).

I am not sure why we did not add stuttering by default - probably just to not restrict the expressivity, although it does lead to weird situations like this.

[konnov]

I am not sure why we did not add stuttering by default - probably just to not restrict the expressivity, although it does lead to weird situations like this.

Right. Actually, TLC uses Spec as the input for checking temporal properties, which normally has stuttering Next. We did not need that for safety and now it bites us back. Perhaps, we should only allow non-stuttering steps in the expert mode (there is no expert mode though :)).

[lucab]

Thanks for the feedback. You touched quite a bit of topics, so I'll try to split them across different items:

• The temporal property above is a plain always check, i.e. it is a state invariant in disguise. I probably should have written it has a plain invariant without any temporal specifier, but I'm a bit surprised Apalache does not do that lifting for me. In the end, this is a condition that must hold true in each single state separately, regardless of loop-finding.

• I'm actually happy that Next has no stuttering, as my Quint spec does not actually have stuttering. Otherwise, it would break some other properties (e.g. that the counter is always strictly increasing by 1 per step) in a quite opaque way. I can manually encode stuttering in Quint in specific actions, where needed.

• I understand much of the trouble here come from the infinite state change, and in this (and most other cases) I can bound the execution. However that brings the additional problem of now having two caps: my arbitrary one, and the checker max-steps. If arbitrary_cap > max_steps, we are back to the problem of a (seemingly) infinite change.
  Ideally I'd need some way in Quint and Apalache to derive one value from the other, e.g. execLimit = (maxSteps / 2) + 1 with maxSteps coming from somewhere outside of the spec and linked to Quint/Apalache --max-steps.

[konnov]

• The temporal property above is a plain always check, i.e. it is a state invariant in disguise. I probably should have written it has a plain invariant without any temporal specifier, but I'm a bit surprised Apalache does not do that lifting for me. In the end, this is a condition that must hold true in each single state separately, regardless of loop-finding.

This is true. The preprocessor of temporal properties could probably do a better job. It just follows the general algorithm.

[konnov]

• I understand much of the trouble here come from the infinite state change, and in this (and most other cases) I can bound the execution. However that brings the additional problem of now having two caps: my arbitrary one, and the checker max-steps. If arbitrary_cap > max_steps, we are back to the problem of a (seemingly) infinite change.
  Ideally I'd need some way in Quint and Apalache to derive one value from the other, e.g. execLimit = (maxSteps / 2) + 1 with maxSteps coming from somewhere outside of the spec and linked to Quint/Apalache --max-steps.

Yeah. This is actually a very hard problem in bounded model checking. If you are curious about it, there is a paper on reoccurence diameters. In practice, this means though that you have to use something like a napkin computation to figure out the bounds.

[lucab]

@konnov thanks for the paper reference, it looks like an interesting topic, I've put that up in my reading queue!

For clarity, I'm totally fine deriving an approximate bound on my own through some napkin math.
The problem is that the input parameter for this (e.g. the maxSteps above) can dynamically change outside of the spec, depending on Quint/Apalache CLI argument. And that may turn a finite execution into an infinite one, and vice-versa.

I guess I'm effectively asking for a new(?) feature which somehow propagates Quint/Apalache --max-steps value to something usable in the spec formulas. That would allow deriving a bound in the spec to make the execution finite, regardless of being invoked with --max-steps 10 or max-steps 99999.