Как доказать или смоделировать проверку теоремы в TLA +?

Question

Приведенный ниже модуль объявляет набор чисел в диапазоне от 10 до 99, которые делятся на 2 только один раз, и вызывает его NumbersThatDivideBy2Once.В конце он объявляет теорему о том, что константа input является подмножеством NumbersThatDivideBy2Once.

--------------------------- MODULE TestModule ---------------------------
EXTENDS Naturals

CONSTANT input

Numbers == { n \in Nat : n > 9 /\ n < 100 }

DividesBy2(n) == (n % 2) = 0

DividesBy2Once(n) == DividesBy2(n) /\  ~DividesBy2(n \div 2)

NumbersThatDivideBy2Once == { n \in Numbers: DividesBy2Once(n) }

THEOREM input \subseteq NumbersThatDivideBy2Once

=======================

Как я могу проверить, справедлива ли эта теорема для данного входа?Если я запускаю проверку модели с предоставленным набором чисел как input, даже если некоторые из этих чисел не являются частью NumbersThatDivideBy2Once, я все равно не получаю ошибок.

Answer 1

Дайте своей теореме имя,

THEOREM T == input \subseteq NumbersThatDivideBy2Once

Перейдите на вкладку «Результаты проверки модели» и в «Оцените выражение константы» введите T, чтобыбыть оцененным.

---

Необходимо проверить вашу модель, что делать с файлом спецификации, который по сути является просто набором математических определений.

В «обычном использовании» вы хотите предоставить TLC временную формулу, представляющую вашу спецификацию (обычно дается имя Spec в файле спецификации).Вы вводите его на вкладке «Обзор модели» в разделе «Какова спецификация поведения?».И это то, что TLC использует для проверки моделей.

В этом случае у вас этого нет.Поэтому просто оставьте параметр «без спецификации поведения» и, как указано выше, укажите на вкладке «Результаты проверки модели» постоянное выражение, которое вы хотите оценить.