[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Sun, 1 Apr 2018 16:42:39 -0700 (PDT)*References*: <c88a1fc6-9174-4a18-958f-b01397cc002d@googlegroups.com>

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

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

On Saturday, March 31, 2018 at 7:44:08 PM UTC-7, Andrew Helwer wrote:

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

**Follow-Ups**:

**References**:**The level of the expression or operator substituted for 'Def' must be at most 0***From:*Andrew Helwer

- Prev by Date:
**The level of the expression or operator substituted for 'Def' must be at most 0** - Next by Date:
**TLC model checking RealTime module: problem with variable now** - Previous by thread:
**The level of the expression or operator substituted for 'Def' must be at most 0** - Next by thread:
**Re: The level of the expression or operator substituted for 'Def' must be at most 0** - Index(es):