解析错误:替换“Def”的表达式或运算符的级别最多必须为0。

Question

我有两个规范: System和SystemMC。系统规范是我指定的系统的“好”规范，对文档很有用。它定义了一个常量MessyAction(_) (在我正在编写的实际规范中，它是一个散列函数)，以一种高效的模型检查方式进行指定是很麻烦的，因此会降低规范的可读性。我在MessyAction规范中实现了SystemMC (_)，所以我可以建模-检查系统规范。但是，解析器在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

按照Lamport的reply 这里，当您实例化一个非常数模块(一个包含变量的模块)(系统)时，常量实体只能被其他常量实例化。因此，在SystemMC中，您可以将MessyAction(_)重命名为MessyActionImpl(_)，将MessyAction(_)定义为常数，然后在模型中将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+的依赖注入！