Разница между => и <=>

Я изучаю TLA+ с этой замечательной страницы "Learn TLA+".

Я не могу получить практическую разницу между => а также <=>, Я понимаю это с точки зрения "таблицы правды", но я не могу этого понять.

Можно ли привести практический пример TLA+, подчеркивающий разницу между этими двумя?

Связанные с:

Источник

3 ответа

Решение

Представьте, что у нас ограниченная очередь q с максимальным размером MAX, reader процесс, который выскакивает сообщения из очереди, writer процесс, который добавляет сообщения в очередь, и queue_maxed_flag это либо правда, либо ложь. Вот четыре возможных инварианта:

  • (len(q) = MAX) => queue_maxed_flag означает (в дополнение к другим возможным вещам, в зависимости от спецификации), что если автор добавляет сообщение, когда q имеет MAX-1 сообщения также должны установить queue_maxed_flagв противном случае инвариант нарушается. Однако, если читатель выскочит из очереди с максимальными значениями, его не нужно сбрасывать queue_maxed_flag,
  • queue_maxed_flag => (len(q) = MAX) означает (в дополнение к и т. д.), что если читатель выскакивает сообщение, когда q имеет MAX сообщения также должны сбрасывать queue_maxed_flag, Однако, если автор добавляет сообщение, когда q имеет MAX-1 сообщения, его не нужно устанавливать queue_maxed_flag,
  • (len(q) = MAX) <=> queue_maxed_flag а также queue_maxed_flag <=> (len(q) = MAX) означают одно и то же: оба предыдущих инварианта верны. Если писатель записывает последнее сообщение в очередь, он должен установить флаг, а если читатель читает из полной очереди, он должен сбросить флаг.

Так почему A <=> B и не A = B? A <=> B строже, так как ожидает, что и A, и B будут логическими значениями. TLC оценивает 5 = 6 как FALSE, но это вызывает ошибку на 5 <=> 6,

Источник

=> ("если") является следствием. Вот пример:если дверь открывается, подайте сигнал тревоги.
Обратите внимание, что сигнал тревоги все еще может сработать из-за чего-то, кроме открытия двери (например, открытия окна).

Вот его таблица правды. Думаю, вы программируете систему сигнализации для клиента. x представляет собой открытие двери, y звучит тревога.

x | y | x => y | Explanation
0 | 0 |   1    | The door doesn't open, the alarm doesn't sound (You don't want the alarm to go off for nothing)
0 | 1 |   1    | The door doesn't open, but the alarm still sounds (e.g. because a window was opened)
1 | 0 |   0    | The door opens, but the alarm doesn't sound (That is not how you want to protect your house)
1 | 1 |   1    | The door opens and the alarm sounds (What else would you have an alarm for)

Давайте перейдем к уравнению (<=> или "только если"). Это верно только тогда, когда оба параметра имеют одинаковое значение. В этом примере сигнал тревоги сохраняется, но меняется на " Только если дверь открывается", подайте сигнал тревоги.
Примечание: на этот раз открывающееся окно не должно вызывать тревогу, а только дверь.

x | y | x => y | Explanation
0 | 0 |   1    | The door doesn't open, the alarm doesn't sound
0 | 1 |   0    | The door doesn't open, the alarm sounds (That's a false positive, that window opening is not what your alarm should cover)
1 | 0 |   0    | The door opens, but the alarm doesn't sound (That is not how you want to protect your house)
1 | 1 |   1    | The door opens and the alarm sounds (What else would you have an alarm for)

Это часто смешивается и неправильно описывается в спецификациях (это также удобно для юридической защиты, если вы это знаете).

Источник 
THEOREM TRUE = \A x:  (x \in {1, 2})  =>  (x \in {1, 2, 3})

в отличие от

THEOREM FALSE = \A x:  (x \in {1, 2})  <=> (x \in {1, 2, 3})

который не держит, потому что \E x: (x \in {1, 2, 3}) /\ ~ (x \in {1, 2}) (а именно x = 3).

Идентификатор x может представлять, в какой комнате находится система.

Кроме того, единственный случай, когда A <=> B не FALSE для A \in BOOLEAN /\ B \in BOOLEAN, Даже если A = B, если либо A или же B снаружи BOOLEAN, затем (A <=> B) = FALSE, По сравнению, A => B а также B => A оба могут быть TRUE для некоторых A, B вне BOOLEAN (Аксиомы TLA+ оставляют эту ситуацию неопределенной).

Раздел 16.1.3 "Интерпретации булевых операторов" на стр. 296-297 и раздел 1.1 "Пропозициональная логика" на стр. 9-11 (в частности, стр.9) из [1] наиболее актуальны для того, что операторы <=> а также => имею в виду.

[1] Лесли Лампорт, "Уточняющие системы", Addison-Wesley, 2002

Источник
Другие вопросы по тегам