changes to refinement syntax

[tillmo]

During a presentation of refinements and networks in DOL, I got the following feedback:

• compositions R1 then R2 could be written R1 refined to R2. There is less confusion with then in extensions, and the syntax of refinements is more uniform. Maybe this even could mean that compositions are dropped from the abstract syntax
• in refinements of networks, a NodeMap could be a (named) refinement, which already contains source, target and signature morphism/comorphism - exactly what is needed for a NodeMap. The only question is how we can get the node names of source and target. Maybe they should be stored together with the refinement in the semantics?

@mcodescu, what do you think?

[mcodescu]

I find it a bit counterintuitive to refine refinements. Maybe we can think of another keyword than then, perhaps followed by, and stay with composition of refinements?

On the second issue: we need a NodeMap as a component of a network morphism. It could be the case that at some point in the future we will want to have some structuring mechanisms on networks, and then network morphisms would appear in other contexts than refinement. For this reason, I would not modify NodeMap.

[mcodescu]

Or perhaps allow to write a refinement or an interpretation instead of a symbol map, because it is shorter, but also specify source and target nodes:
OMSName |-> OMSName [using LanguageTranslation* [SymbolMap]] [using RefinementName | InterpretationName]

[tillmo]

Concerning the first issue: the target of a "refined to" can be a refinement already now. So why not the source?

Concerning the second issue: even if we needed network morphisms in a different context than refinement, it would be helpful to be able to write them succinctly. using RefinmentName is an idea in this direction, but why should we force the user to specify source and target if these are already available from the refinement?

[mcodescu]

I won't fight against the first idea, it is a matter of taste.

On the second issue, I think there is always a trade-off between less writing and specifications that can be easily understood. A reader would have to guess which nodes are connected by which refinements.
BTW, the semantics of refinements would not even have to be modified: for a simple refinement SP refined via sigma to SP' we already get in the semantics a tuple $(G,G'),\sigma, \cM$ where $G$ is the node of $SP$ and $G'$ the node of $SP'$. Given that the names of nodes are unique in networks, the semantics of NodeMap would just introduce the appropriate links.

[tillmo]

since a refinement can be a rather long chain of individual refinements, I think it is a good idea that it can be re-used in a context where it makes sense.

[mcodescu]

I don't object to this. But I suggest to keep the specification a little more verbose by also specifying the source and target nodes of the refinement, for the sake of readability.

[tillmo]

I suggest that optionally you can specify source and target, but you are not forced to do so.

[mcodescu]

Yes, this is the natural solution.

[tillmo]

good, could you please change abstract and concrete EBNF syntax accordingly?

[tillmo]

@MGlauer, could you please change the metamodel accordingly?