Currently, opening another module will import sigs, predicates, etc. into the target module. Multiple modules can be imported into a single target. It is reasonable to imagine that both modules bind the same identifier. For example, suppose we are modeling Prim's algorithm: we'd probably have a Node sig. But then if we're modeling Kruskal's algorithm, we'd also have a Node sig. If we then want to reason about these algorithms in (some sort of) composition, we'd import both into a third module.
It is inconvenient to need to manually rename identifiers (e.g., KNode vs. PNode for the two above). Alloy handles this by automatically prepending the imported module name to the identifier imported. We should consider doing the same, or at least doing so when a conflict occurs.
If we do this, we should add an as annotation to open, similar to Alloy's, so a module can control the naming.
Currently,
opening another module will import sigs, predicates, etc. into the target module. Multiple modules can be imported into a single target. It is reasonable to imagine that both modules bind the same identifier. For example, suppose we are modeling Prim's algorithm: we'd probably have aNodesig. But then if we're modeling Kruskal's algorithm, we'd also have aNodesig. If we then want to reason about these algorithms in (some sort of) composition, we'd import both into a third module.It is inconvenient to need to manually rename identifiers (e.g.,
KNodevs.PNodefor the two above). Alloy handles this by automatically prepending the imported module name to the identifier imported. We should consider doing the same, or at least doing so when a conflict occurs.If we do this, we should add an
asannotation toopen, similar to Alloy's, so a module can control the naming.