Как проверить модель модуля, который зависит от несвязанной переменной?

Question

Я сейчас прохожу через Specifying Systems и немного озадачен тем, как я проверю модель следующего модуля:

---------------------------- MODULE BoundedFIFO ----------------------------
EXTENDS Naturals, Sequences
VARIABLES in, out
CONSTANT Message, N
ASSUME (N \in Nat) /\ (N > 0)

Inner(q) == INSTANCE InnerFIFO

BNext(q) == /\ Inner(q)!Next
            /\ Inner(q)!BufRcv => (Len(q) < N)

Spec == \EE q : Inner(q)!Init /\ [][BNext(q)]_<<in, out, q>>
=============================================================================

Я вижу, что оба Init а также BNext формулы являются операторами, параметризованными q, Как бы я поставил это на модель проверки?

Answer 1

Вы не можете: \E x : P(x) является неограниченным выражением, которое TLC не может обработать. Многие из спецификаций в Specifying Systems не могут быть смоделированы. Более поздние руководства, такие как TLA+ Hyperbook или Learn TLA +, более осторожны, чтобы поддерживать все их спецификации в модельном состоянии.