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

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

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


distributed-system tla+ formalize
person Oliver Young    schedule 11.02.2019    source источник

Ответы (1)


arrow_upward
2
arrow_downward

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

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