Once issue #154 is addressed, a P module X will have the property that if
(1) interface I is bound to machine M in X,
(2) I is private in X,
(3) all receive events of M are private in X,
then a machine identifier (I,,) cannot leak outside P. Consequently, any renaming of interface I leaves the trace semantics unchanged. I suggest that for such an interface I, renaming be applied automatically to a freshly-generated name that is guaranteed to be different from interface names the programmer can write and any other freshly-generated names. An interface I may become a candidate for renaming when either hide operation is applied (events or interfaces).
It is possible that if automatic renaming is done, then the programmer may never need to do manual renaming for typical programs. The only other use of renaming we used to have was for renaming a machine to Main, but now we have a separate mechanism to indicate Main in test declarations.
Once issue #154 is addressed, a P module X will have the property that if
(1) interface I is bound to machine M in X,
(2) I is private in X,
(3) all receive events of M are private in X,
then a machine identifier (I,,) cannot leak outside P. Consequently, any renaming of interface I leaves the trace semantics unchanged. I suggest that for such an interface I, renaming be applied automatically to a freshly-generated name that is guaranteed to be different from interface names the programmer can write and any other freshly-generated names. An interface I may become a candidate for renaming when either hide operation is applied (events or interfaces).
It is possible that if automatic renaming is done, then the programmer may never need to do manual renaming for typical programs. The only other use of renaming we used to have was for renaming a machine to Main, but now we have a separate mechanism to indicate Main in test declarations.