如何在TLC中仅覆写"顶层"Init算子？

你遇到的递归错误是因为覆写Init时，MCInit里引用的Init已经被替换成了MCInit本身，形成了循环调用。要只替换顶层Init且避免递归，直接在配置文件里明确引用原模块的Init即可，不需要单独定义MCInit。

具体做法是修改MCSpec.cfg为：

CONSTANT
  Init <- Spec!Init /\ x = FALSE

这里通过Spec!Init明确指定使用原Spec模块中的原始Init定义，而不是被覆写后的版本，这样就不会触发循环递归，同时实现了对顶层Init的覆写，效果和单独定义MCSpec模块完全一致。

内容的提问来源于stack exchange，提问作者Hovercouch