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

[Andrew Helwer]

I have two specs: System and SystemMC. The System spec is the "nice" spec of the system I am specifying, useful for documentation. It defines a CONSTANT MessyAction(_) (in the actual specs I am writing, a hash function) that is messy to specify in an efficiently model-checkable way and so would reduce spec readability. I implement MessyAction(_) in the SystemMC spec, so I can model-check the System spec. However, the parser gives the following error:

Level error in instantiating module 'System': The level of the expression or operator substituted for 'MessyAction' must be at most 0.

What does this error mean, and how can I accomplish my goal of model-checking the System spec without adding a bunch of stuff to it that is optimized for TLC? Here are the specs in full:

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

EXTENDS
    Naturals

CONSTANTS
    MessyAction(_)

VARIABLES
    Counter

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

TypeInvariant ==
    /\ Counter \in Nat

Init ==
    /\ Counter = 0

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

Next ==
    \/ Increment

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

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

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

Thanks!

Andrew

[Leslie Lamport]

Hi Andrew,

The error message is perfectly accurate.  When you instantiate a
non-constant module (one that has variables) like System, declared
CONSTANTs can be instantiated only by constant expressions.  (And
declared VARIABLEs can be instantiated only by state expressions.)

An important property of instantiation is that if the instantiation of
all the module's ASSUME statements are true, then the instantiation of
all its valid THEOREMs are true.  It's not hard to see that this property
would not hold if declared constants in non-constant modules could be
instantiated with non-constant expressions.

Leslie

[Andrew Helwer]

Ah, I see! Given that, I was able to solve my problem by defining MessyAction(_) as a CONSTANT in the SystemMC spec, then in the model I define the value of the MessyAction(_) constant as MessyActionImpl(_). See below, differences highlighted:

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

EXTENDS
    Naturals

CONSTANTS
    MessyAction(_)

VARIABLES
    Counter

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

TypeInvariant ==
    /\ Counter \in Nat

Init ==
    /\ Counter = 0

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

Next ==
    \/ Increment

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

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

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