Parse error: The level of the expression or operator substituted for 'Def' must be at most 0

Question

我有两个规范：System 和 SystemMC。系统规范是我指定的系统的 "nice" 规范，对文档很有用。它定义了一个 CONSTANT MessyAction(_)（在我正在编写的实际规范中，一个散列函数），以有效的模型可检查方式指定它很混乱，因此会降低规范的可读性。我在 SystemMC 规范中实现了 MessyAction(_)，因此我可以对系统规范进行模型检查。但是，解析器在 SystemMC 规范中给出以下错误：

实例化模块时出现级别错误'System'：替换'MessyAction'的表达式或运算符的级别最多必须为0。

此错误是什么意思，我如何才能实现对系统规范进行模型检查而不向其添加一堆针对 TLC 优化的内容的目标？这是系统规格：

------------------------------- MODULE System -------------------------------

EXTENDS
    Naturals

CONSTANTS
    MessyAction(_)

VARIABLES
    Counter

-----------------------------------------------------------------------------

TypeInvariant ==
    /\ Counter \in Nat

Init ==
    /\ Counter = 0

Increment ==
    /\ Counter' = Counter + 1
    /\ MessyAction(Counter)

Next ==
    \/ Increment

=============================================================================

这是 SystemMC 规范：

------------------------------ MODULE SystemMC ------------------------------

EXTENDS
    Naturals

CONSTANTS
    MaxCounterValue

VARIABLES
    Counter,
    PastValues

ASSUME MaxCounterValue \in Nat

-----------------------------------------------------------------------------

MessyAction(c) ==
    /\ PastValues' = PastValues \cup {c}

S == INSTANCE System

TypeInvariant ==
    /\ PastValues \subseteq Nat
    /\ S!TypeInvariant

Init ==
    /\ PastValues = {}
    /\ S!Init

Increment ==
    /\ Counter < MaxCounterValue
    /\ S!Increment

Next ==
    \/ Increment

=============================================================================

Answer 1

根据 Leslie Lamport 的回复 here，当您实例化一个 non-constant 模块（包含变量的模块）时，例如 System，CONSTANT 实体只能由其他常量实例化。因此，在 SystemMC 中，您可以将 MessyAction(_) 重命名为 MessyActionImpl(_)，将 MessyAction(_) 定义为 CONSTANT，然后在模型中将 MessyAction(c) 定义为 MessyActionImpl(c)。系统规范未更改，但这是新的 SystemMC 规范：

------------------------------ MODULE SystemMC ------------------------------

EXTENDS
    Naturals

CONSTANTS
    MessyAction(_),
    MaxCounterValue

VARIABLES
    Counter,
    PastValues

ASSUME MaxCounterValue \in Nat

-----------------------------------------------------------------------------

MessyActionImpl(c) ==
    /\ PastValues' = PastValues \cup {c}

S == INSTANCE System

TypeInvariant ==
    /\ PastValues \subseteq Nat
    /\ S!TypeInvariant

Init ==
    /\ PastValues = {}
    /\ S!Init

Increment ==
    /\ Counter < MaxCounterValue
    /\ S!Increment

Next ==
    \/ Increment

=============================================================================

在工具箱中创建模型时，将 MessyAction(_) 常量的值定义为 MessyActionImpl(_):

最终结果：

瞧，TLA+ 的依赖注入！

Parse error: The level of the expression or operator substituted for 'Def' must be at most 0

Parse error: The level of the expression or operator substituted for 'Def' must be at most 0

tla+