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