TLA+ Spec с предположениями о внешних системах

Question

Я пробую TLA+ для проекта на работе. Я хочу доказать, что выборка данных с одним и тем же ключом вернет те же данные, несмотря на некоторые изменения внутренних данных. Для этого я хотел бы смоделировать внешнюю систему как черный ящик, ответы которого имеют определенные свойства. Например:

CONSTANT ValidKeys
CONSTANT DataPoints
CONSTANT FETCH(_)

\* Incorrect use of ASSUME, but for illustrative purposes.
ASSUME ValidKeys \in SUBSET DOMAIN FETCH(ValidKeys)
ASSUME \forall key in ValidKeys:
  LET fetched == Fetch(ValidKeys)[key]
  IN fetched \in Seq(DataPoints)

Затем я хотел бы написать свою собственную систему, в которой TLA+ выводит поведение на основе указанных предположений. Это возможно?

Answer 1

Да, но лучше - особенно если вы хотите использовать TLC, средство проверки модели TLA+, являющееся частью панели инструментов - использовать недетерминированность напрямую, а не полагаться на аксиоматическую спецификацию с использованием констант и предположений, которые требуют от вас предоставления определенного экземпляр при проверке модели, что, вероятно, не то, что вы хотите.

Вы можете сделать это:

CONSTANT ValidKey
CONSTANT DataPoint

VARIABLE x

Fetch(key) == key \in ValidKey /\ x' \in Seq(DataPoint)

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

Если ты хочешь Fetch чтобы всегда "возвращать" один и тот же результат для одного и того же ключа, вы можете сделать что-то другое:

CONSTANTS ValidKey, DataPoint
VARIABLE fetch

Init == fetch \in [ValidKey -> Seq(DataPoint)] /\ ...

Next == UNCHANGED fetch /\ ...

что говорит о том, что fetch некоторая неизвестная функция желаемого типа. TLC также проверит спецификации на все возможные fetch функции.