Better parameterized instantiation support

[quaeler]

• Supporting parameterized instantiation used in specification definition in which temporal actions are involved.

[Bug][Tools]

[quaeler]

This commit does not break any of the existing unit tests, which lessens slightly my trepidation in this change.

A review of the investigation

Using this module and inner-module as reference, i'll discuss what was originally working and what was not.

What was working

• Model checking with the SPECIFICATION as SpecB
• Model checking with the INIT / NEXT as ParamInstance's Init and Next

What was failing

• Model checking with the SPECIFICATION as SpecA

Why was this failing

In SpecProcessor#processConfigSpec(ExprNode, Context, List) we encountered the logic problem that the predicate embodying the SpecA assignment (Z7(7)!Spec) does have a non-zero-length argument this, and it is also considered a custom operation (opcode == 0,) so it remains unprocessed in lines 1100-1289 (whereas SpecB, as it is a conjunction, gets processed in lines 1104-1110.)
This results in the instance variable initPredVec have a zero-size and so this check will fail the launch of TLC.

The remediation

The changes embodied in this PR augment the logic in processConfigSpec(...) to handle the non-zero-length argument case for an action whose operator's body is an instance of SubstInNode, whose body is another instance of OpApplNode.

At this point, we need to hand curate the current Context instance to capture the mapping between the argument(s)'s value(s) and the variable name(s), so that when the tool and the workers are evaluating expressions later on, they have the value available to them. This is commented on in the changes introduced in this method.

Also discussed in those comments, we are ensuring in this Context curation, and the context curations in Tool#getInitStates(...) and in Tool#getNextStatesImplSubstInKind(...), that we do not double-map the variable name within the Context. If we do not observe this, a later mapping of the variable name will occur during recursive calls of processConfigSpec(...) / getInitStates(...) / getNextStatesImplSubstInKind(...) done to process the invoked inner module actions, and this mapping will be valueless (because at that point we've lost the argument value.)

[lemmy]

Did you also look into operator instantiation (see section 5 of TLA+2 guide) or do you expect no special handling is required in TLC?

[quaeler]

I did not, will verify and address if kaput.

[lemmy]

Section 2.1 of current-tools.pdf suggests a simple workaround. To what extent does is this related?

Please add test cases if operator instantiation is different.

[quaeler]

Not sure what you mean by related, but since the suggested workaround has a zero-length argument list, its functioning will not be affected by these code changes.

[quaeler]

This has not affected the handling of infix operator definitions; e.g

ModSanityCheck == Z7(7)!$$(5,9) < 7

where the inner module has this definition

  x $$ y == (x + y) % cardinality

evaluates correctly. I'm unable to create a correctly parsed prefix or postfix operator definition even in older builds of the Toolbox/TLATools, though TLA documentation implies this is supposed to work.

[lemmy]

Non-exhaustive set of background information/context:

http://discuss.tlapl.us/msg01141.html