Как я могу утверждать, что число идет или список растет в 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