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

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