Вопросы о постоянном операторе в TLA +

Question

Я недавно читаю книгу "Специфицирующие системы".В главе 5 Лесли определяет оператор константы Send (, , , ).

Я не понимаю, как присвоить значение (True / False) этому константному выражению?Нужно ли присваивать True / False каждому (p, v, m, m ') в программе проверки модели TLC?

Answer 1

Вы можете присвоить Send двумя способами:

1. Если вы создаете его в другом модуле, вы можете передать нужного оператора с помощью WITH: Instance Foo WITH Send <- Op \*...
2. Вы можете назначить оператора в TLC в разделе «Какая модель?»