qvtrPreferringCreationToReuse

Bx Examples Repository

Title: qvtrPreferringCreationToReuse

Version: 0.1

Type: QVT-R

Overview

This example illustrates some features of QVT-R semantics as standardised by OMG and implemented in ModelMorf. Discussion here is extracted almost verbatim from Cheney et al., see References.

Models

Let $M$ and $N$ be identical model sets, comprising models that contain two kinds of elements Parent and Child. Both kinds have a string attribute name; Parent elements can also be linked to children which are of type Child. We represent such models in the obvious way as forests, and notate them using the names of elements, e.g. $\{p \rightarrow \{c_1,c_2,c_2\}\}$ represents a model containing one element of type Parent with name $p$, having three children of type Child whose names are $c_1$,$c_2$,$c_2$. Notice that we do not forbid two model elements having the same name.

Consistency and consistency restoration

are both given by the following QVT-R transformation:

transformation T (m : M ; n : N) {
top relation R {
  s : String;
  firstchild : M::Child;
  secondchild : N::Child;
  enforce domain m me1:Parent {name = s, child = firstchild};
  enforce domain n me2:Parent {name = s, child = secondchild};
  where { S(firstchild,secondchild); }}

relation S {
  s : String;
  enforce domain m me1:Child {name = s};
  enforce domain n me2:Child {name = s};}}

Consistency

The consistency relation between $m\in M$ and $n\in N$ we consider is given by a pair of unidirectional checks. [$m$]] and $n$ are consistent "in the direction of $n$'' iff for any Parent element in $m$, say with name $t$, linked to a child having name $c$, there exists a(t least one) Parent element with name $t$ in $n$, also linked to a child with name $c$. The check in the direction of $m$ is dual.

Consistency Restoration

See discussion for examples.

Properties

Correct and hippocratic.

Discussion

Suppose that (for some strings $p$,$c_1$,$c_2$,$c_3$) we take $m=\{p \rightarrow \{c_1,c_2,c_3\}\}$, and for $n$ we take the empty model. When we restore consistency by modifying $n$, what are reasonable results, from the point of view of least change and considering only the consistency specification?

We might certainly argue that $n$ should be replaced by a copy of $m$; intuitively, $m$ is a good candidate for the least complex thing that is consistent with $m$ in this case. What the QVT-R specification, and its most faithful implementation, ModelMorf, actually produces is $\{p \rightarrow \{c_1\},p \rightarrow \{c_2\},p \rightarrow \{c_3\}\}$.

We refer the reader to BradfieldStevens for details of the semantics that gives these results, but in brief: QVT-R only changes model
elements when it is forced to do so by "key'' constraints. That is, when a certain kind of element is required, and one exists but with the wrong properties, and more than one is not allowed, then QVT-R changes the element's properties. Otherwise, QVT-R modifies a model in two phases.

First it adds model elements that are required for consistency to hold. Because it does not change properties of model elements, which include their links (Parent to Child in our case), it takes an "all or nothing'' view of whether an entire valid binding, that is, configuration of model elements that is needed according to a relation, exists. If not, it creates elements for the whole configuration.

So here, the transformation might first discover that it needs a Parent named $p$ linked to a Child named $c_1$; since
there isn't such a configuration, it creates both elements. Next, it discovers that it needs a Parent named $p$ linked to a Child named $c_2$; since such a configuration does not exist, it creates both a new Parent and a new Child. (We could have written the QVT-R transformation differently, e.g. used a "key'' constraint on Parent, but this would have other effects that might not be desired.) Similarly for $c_3$.

Next, with the same $m$ and a further string $x$, consider $n = \{p\rightarrow \{c_1,c_2,x\}\}$. Intuitively, the name of the third Child is wrong: it is $x$ and should be changed to $c_3$. In fact, QVT-R and ModelMorf, using the same transformation as before, actually produce $\{p \rightarrow \{c_1,c_2\},p \rightarrow \{c_3\}\}$. As in the previous example, rather than modify an existing Child, a whole new binding $\{p \rightarrow \{c_3\}\}$ has been created to be the match to the otherwise unmatchable binding involving $c_3$ in $m$. In the second phase, the Child with name $x$ has been deleted, as
otherwise the check in the direction of $m$ could not have succeeded.

A final example in BradfieldStevens, omitted here, demonstrates that the question of precisely when elements need to be deleted is problematic.

References

This is Example 4.5 from

@inproceedings{cheney15:bx,
author = {James Cheney and Jeremy Gibbons and James McKinna and Perdita Stevens},
title = {Towards a Principle of Least Surprise for Bidirectional Transformations},
booktitle = {Proceedings of {Bx} 2015},
year = 2015,
ee = {http://ceur-ws.org/Vol-1396/p66-cheney.pdf},
publisher = {CEUR-WS.org},
series = {CEUR Workshop Proceedings},
volume = 1396
}

See also

@inproceedings{BradfieldStevens,
author = {Julian C. Bradfield and
Perdita Stevens},
title = {Recursive Checkonly {QVT-R} Transformations with General when
and where Clauses via the Modal Mu Calculus},
booktitle = {Proceedings of {FASE}},
year = {2012},
pages = {194-208},
publisher = {Springer},
series = {LNCS},
volume = {7212},
isbn = {978-3-642-28871-5},
ee = {http://dx.doi.org/10.1007/978-3-642-28872-2_14}
}

Author(s)

Perdita Stevens

Reviewer(s)

Comments

Unless otherwise stated, the content of this page is licensed under GNU Free Documentation License.