How do I override only the "top-level" operator in TLC?

Question

I have two specs like this:

---- MODULE Spec ----
VARIABLE x

Init == x \in BOOLEAN

Next == x' = ~x
Spec == Init /\ [][Next]_x
====

---- MODULE MCSpec ----
EXTENDS Spec

MCInit == Init /\ x = FALSE \* Optimization

MCSpec == MCInit /\ [][Next]_x
====

It would be easier if I didn't have to define MCSpec, and could just add a module override to MCSpec.cfg:

CONSTANT
  Init <- MCInit

But this raises a recursion error, as MCInit calls Init, which is replaced by MCInit, which calls Init...

Is there a way to only replace the "Top-level" Init via an override?

Answer 1

If your only concern is not wanting to define MCSpec, instead of using SPECIFICATION MCSpec in your model file (.cfg) you can use:

INIT MCInit
NEXT Next