Search code examples
tla+

how can I assert that a number goes or a list grows up in TLA+?

I have a TLA+ spec where I would like to assert that a list only ever grows in length (it's fine if it stays the same when stuttering.)

Right now I have something like this, but I'm certain that it's not right:

NoWorkIsLost == Len(samples) = Len(samples) ~> Len(samples) = Len(samples) + 1

I'm not even sure what to search for here, I'm sure I'm missing something super obvious!

Solution

  • It depends on what you mean by "the list only ever grows in length". The simplest way to do that would be to write

    Op == [][Len(samples') > Len(samples)]_Len(samples)

    But that's saying that if the length changes, the length must increase. That still allows for you to mutate the list without changing it! If you instead write

    Op == [][Len(samples') > Len(samples)]_samples

    Then you are saying that if samples changes, it must also increase in length. But this allows you to pop one element and push two in a single action. You probably want to express that the old sequence is a prefix of the new one. You can do that with

    Op == [][SubSeq(samples', 1, Len(samples)) = samples]_samples