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

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

[Ugur Yavuz]

I found myself needing to do something very similar: I'm working on something where I need to write a module that takes in actions (or in my case, sets of actions) and defines specifications in terms of these passed-in actions.

From Leslie’s earlier reply (and also from Section 17.5.5 of Specifying Systems) it seems that module instantiation isn't the right tool for this. And since I want to prove properties about these specs in TLAPS, Andrew's workaround of passing definitions through the model configuration file is not an option for me either.

Of course, the most straightforward approach is to have the user define the actions in a module, then extend that module and copy-paste my spec definitions. A slightly nicer approach would be to write a small script that takes a module containing the arguments, and generates a new module that extends it and defines the specs.

But I'm hoping to find a solution that stays entirely within the TLA+ ecosystem. Has anyone run into this challenge and found a solution?

Thanks!

Ugur