tla+ - 如何对依赖于未绑定变量的模块进行模型检查？

Question

我现在正在检查指定系统，我对如何对以下模块进行模型检查感到有些困惑：

---------------------------- 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

You can't:\E x : P(x)是 TLC 无法处理的无界表达式。指定系统中的许多规范无法建模。更新的指南，例如TLA+ Hyperbook或Learn TLA+，更加小心地保持所有规范的可建模性。