Как я могу утверждать, что число идет или список растет в TLA+?

Question

У меня есть спецификация TLA+, в которой я хотел бы заявить, что список только увеличивается в длину (хорошо, если он остается неизменным при заикании).

Прямо сейчас у меня что-то вроде этого, но я уверен, что это не правильно

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

Я даже не уверен, что искать здесь, я уверен, что упускаю что-то супер очевидное!

Answer 1

Это зависит от того, что вы подразумеваете под "список только увеличивается в длину". Самый простой способ сделать это - написать

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

Но это говорит о том, что если длина изменяется, длина должна увеличиться. Это все еще позволяет вам изменять список без его изменения! Если вы вместо этого напишите

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

Тогда вы говорите, что если samples изменения, он также должен увеличиваться в длине. Но это позволяет вам вытолкнуть один элемент и нажать два в одном действии. Вы, вероятно, хотите выразить, что старая последовательность является префиксом новой. Вы можете сделать это с

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