Support cyclic redefinitions

[lemmy]

A cyclic redefinition RF is a formula that is defined from another formula F while also re-defining F:

    ---- MODULE ModuleWithF ----
    F == /\ A
         /\ B
         /\ C
    ====

    ---- MODULE Derived -----
    EXTENDS ModuleWithF

    RF == /\ F
          /\ D
    ====

    Config file:
    CONSTANT F <- RF

Supported:

• Initial predicate
• Next-state relation
• 0-arity and higher-arity sub-actions provided the parameters are constant level
• Invariants
• Ordinary operators

[lemmy]

@Calvin-L Can you share any specific corner cases that you think might come up? While we all seem to agree that this feature could be beneficial, it's important to define its scope carefully. I'd rather tackle any possible problems beforehand, instead of wasting time only to find out that we should stay with what we already have (instantiation).

[Calvin-L]

One thing I had in mind is:

---- MODULE ... ----
A == "A"
B == "B"
====

CONSTANT A <- B
CONSTANT B <- A

Should this (1) make A = "B" and B = "A" or (2) make A and B mutually recursive?

[Calvin-L]

In the meeting today I think some people mentioned that you can use configuration files to create recursive operators. Will this change that behavior?

[lemmy]

One thing I had in mind is:

---- MODULE ... ----
A == "A"
B == "B"
====

CONSTANT A <- B
CONSTANT B <- A

Should this (1) make A = "B" and B = "A" or (2) make A and B mutually recursive?

This particular example produces Error: In the configuration file, the identifier B appears on the right-hand side of a <- after already appearing on the left-hand side of one. with and without this PR.

In the meeting today I think some people mentioned that you can use configuration files to create recursive operators. Will this change that behavior?

I would recommend maintaining TLC's backward compatibility whenever feasible. Additionally, it's worth noting that recursive operators can be defined without explicitly declaring them as recursive: a57a3a7

[lemmy]

While this now passes all the tests, I'm no longer convinced that it's worth the effort. The INSTANCE technique only adds a slight amount of syntactic overhead.

    ---- MODULE ModuleWithF ----
    F == /\ A
         /\ B
         /\ C
    ====

    ---- MODULE Derived -----
    EXTENDS ModuleWithF
    MWF == INSTANCE ModuleWithF

    RF == /\ MWF!F
          /\ D
    ====

    Config file:
    CONSTANT F <- RF

[Calvin-L]

The changes in this PR look reasonable---although this specific line looks a little fishy to me because it modifies the semantic graph while the graph is being traversed. There is a good reason the Java standard collections forbid this kind of behavior, and those data structures are much simpler than this one.

If we do end up merging this, I would want to at least document what kinds of changes preVisit and postVisit are allowed to make.

[lemmy]

@Calvin-L Agreed, substitueFor no longer mutates the graph during traversal.