[FEATURE] Check trace invariants w.r.t. views

[andrey-kuprianov]

Is your feature request related to a problem? Please describe.

I have started to use trace invariants, which I think is a great feature, as they allow to describe precisely the shape of the computation I want to obtain.

The problem I am facing is that I have a fairly large spec with 13 variables, and the implementation of the trace invariants seem to require the history to be the sequence of STATEs which are records over _all state variables. I have tried to define a history over a subset of variables, but this is rejected:

PASS #8: VCGen                                                    I@19:49:15.261
  > Producing verification conditions from the invariant ThreeActions I@19:49:15.262
(Please report an issue at: [https://github.com/informalsystems/apalache/issues],at.forsyte.apalache.tla.lir.MalformedTlaError: Expected the trace invariant ThreeActions to be a predicate of a sequence of records over the names of state variables)
kernel_test.tla:117:3-117:19: unexpected TLA+ expression: Expected the trace invariant ThreeActions to be a predicate of a sequence of records over the names of state variables E@19:49:15.286
at.forsyte.apalache.tla.lir.MalformedTlaError: Expected the trace invariant ThreeActions to be a predicate of a sequence of records over the names of state variables
	at at.forsyte.apalache.tla.bmcmt.VCGenerator.assertTraceInvType(VCGenerator.scala:111)

The problem is that having all state variables slows down the model checker up to the point of being almost unusable.

Describe the solution you'd like

I would like to be able to describe trace invariants over a subset of state variables. As I typically will need only a few of variables for each trace invariant, this should dramatically speed up the model checker.

Additional context

E.g. I have tried to use this trace invariant which requires access only to 1 out of 13 state variables:

\* @type: Seq(STATE) => Bool;
ThreeActions(history) == 
  LET test == 
    /\ Len(history) >= 3 
    /\ \A i, j \in DOMAIN history : history[i].action /= history[j].action 
  IN
  ~test

[konnov]

Interesting. Do you like to combine trace invariants with the view abstraction?

[andrey-kuprianov]

That is an interesting idea, might be; depends on the implementation I guess. Currently as it seems to me that allowing history to be defined over a subset of state variables is the most straightforward and easy to understand approach.

[danwt]

I think it would be very useful to have views over the history. Here's an illustrative use case:

I have an algorithm with multiple processes and each action is performed by one process. The algorithm is symmetric wrt. process id.

I would like to generate counter examples by projecting on the set containing the number of times each process took an action.

For example the if p1, p2, p3 took 3,4,5 actions then the set would look like {3,4,5}. Then I want to enumerate different sets (maybe restricted to something I like) so I would get runs with {3,3,3}, {3,3,4}, {3,4,4} ... ect.

I think this would be concretely useful and enable useful symmetries (AFAIK is not possible for a spec author to explicitly demand symmetries, please correct me if I'm wrong).

I'd be happy to investigate an implementation for this at some point but I don't think I can make it a priority right now, and I suspect I'd need to spend quite some time learning the guts as I go.

[danwt]

@konnov we were discussing this in today's Apalache planning meeting. I can make a self-standing issue too.

[konnov]

yes, please make an issue

[konnov]

This issue got lost under the pile of other issues. It is actually quite relevant for temporal properties #488.

[konnov]

also got relevant to @angbrav

[Kukovec]

This could also potentially be combined with #1845.

[konnov]

This could also potentially be combined with https://github.com/informalsystems/apalache/issues/1845.

Hmmm. I do not see any connection. @Kukovec could you elaborate?

[Kukovec]

Trace invariants should combine nicely with trace exploration.

[Kukovec]

View-restricted trace invariants are just a special kind of input for the feature described in #1845