CODEWITHSUNDEEP
tla+
Brian Hicks
Brian Hicks

Reputation: 6403

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!

Upvotes: 2

Views: 94

Answers (1)

Hovercouch
Hovercouch

Reputation: 2314

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

Upvotes: 2

Related Questions