Don't check Inv in state 0 with --init=Inv

[nano-o]

Apalache checks that Inv holds in state 0 even with option --init=Inv. This is unnecessary but takes time, so I suggest skipping this check.

[nano-o]

Ran into a variant of this again today, where it takes about 10 minutes to check that I /\ J => J... Maybe what would be needed is to first apply some basic simplification rules to discharge obviously tautological goals.

[konnov]

Yeah, totally, it annoys me all the time too. The quick workaround is to pass:

'--tuning-options=search.invariantFilter=1->.*'

[will62794]

+1. I also encountered this as a minor annoyance when checking a larger inductive invariant.

[konnov]

I have just lost half a day waiting for the invariant being checked against the initial states (totally forgot about that). Then the actual invariant violation was found in 1h. It's actually quite annoying for large specs. I am still struggling with finding a good UX for that though.

We had an idea of introducing profiles some time ago. For instance, this is how we could use a profile for an inductive step:

$ apalache-mc check --profile=inductive-step --init=IndInit --inv=IndInv spec.tla

In this profile, we could automatically:

• enable invariant testing for state 1 only,
• set --length to 1,
• potentially, tune z3 parameters to something that better fits inductive invariants, see Propagate z3 parameters in the tuning options #2990.