Bx Examples Repository
Title: Person2Person
Version: 0.x
Type: Benchmark
Overview
This is a very simple example illustrative of a non information preserving transformation. It is the first benchmark example of the BenchmarX repository, as introduced in [1], and its main goal is to set the template to describe further benchmarks.
Models
A left model $m \in M$ is a set of persons, each with a name and age attributes. Using UML class diagrams the meta-model $M$ can be depicted as follows:
Additionally, there are two constraints: names should be unique and ages positive integers. Using OCL these can be specified as follows:
context Person
inv: Person.allInstances->forAll(x | x <> self implies x.name <> self.name))
inv: self.age >= 0
Additionally, there is one constraint: names should be unique. Using OCL this can be specified as follows:
context Person
inv: Person.allInstances->forAll(x | x <> self implies x.name <> self.name))
Consistency
Two models $m$ and $n$ are consistent if they contain the same names. That is: for every person in $m$, there is at least a person in $n$ with the same name, and vice-versa. This consistency relation is:
- Left-total;
- Right-total;
- Not left-unique;
- Right-unique.
This is an example of a consistency relation that can be expressed in terms of a consistency relation between elements of the models, known as traceability relation. In this case, the traceability relation $\varphi$ relates the identities of the persons with the same name in both models. The two models are consistent iff such traceability relation is one-to-one.
A more detailed formalization of this consistency relation can be found in [1].
Consistency Restoration
Forward
Forward propagation is completely defined by the fact that the consistency relation is left-unique. In particular, given a left model $m$ a consistent right model can be produced by generating it afresh (for efficiency reasons, implementations can still take the current value of $n$ into account): just create a new empty right model, and for each person $p \in m$, add a corresponding person to it with the same name.
Backward
The only updates to the right-model considered in this example are the ones that can be specified by a partial injective function $\mu$ between the identities of the persons in the original and updated right-model. This means that updates that split or merge identities are not considered. Valid updates are delete, create, or change the name of a person.
Given consistent left- and right-models, $m$ and $n$, a traceability relation $\varphi$ between them, an updated right-model $n'$, and a partial injective function $\mu$ between $n$ and $n'$ specifying the update, the updated consistent left-model $m'$ can be produced as follows:
- delete from $m$ any person $p$ that was deleted from $n$, namely delete every $\varphi^{-1}(p)$ such that $p \in n \setminus dom(\mu)$;
- for every person $p$ that was created in $n'$, namely $p \in n' \setminus cod(\mu)$ create a new person in $m'$ with the same name and default age 18;
- for every person $p$ whose name was changed in $n'$, change the name of the corresponding person in $\varphi^{-1}(p) \in m$ to match it.
The interesting cases, for which not all information is available in the right model, are when a person is created (in that case a default age has to be inserted) or when a name is changed (in that case the age must be preserved). Notice that state-based frameworks, that do not receive any description of the update $\mu$, but only the resulting model $n'$ will not be able to distinguish a name change from a deletion followed by an insertion of a new person.
A more detailed formalization of this backwards consistency restoration procedure can be found in [1].
Properties
The consistency restoration procedure described above is:
- Correct
- Complete
- Hippocratic
Variants
A variant is discussed in [2], using the meta-models depicted below:
The main difference is that the the consistency relation is now a bijection, but there is some interesting attribute manipulation required (splitting names into first and last names).
Discussion
This was the first example of a BenchmarX, as introduced in [1].
This example seems quite similar to the composers example already in the repository. However, there are two relevant differences:
- The additional constraints, in particular the key constraint, that makes the consistency relation right-unique and allows it to be expressed in terms of a one-to-one traceability relation;
- Absence of order in $N$, which simplifies the forward propagation.
Maybe in the future it should be redefined as a proper variant of composers.
Artefacts
| Artefact | EMF | XML |
|---|---|---|
| Meta-model $M$ | Left.ecore | tbd |
| Model $m_1 \in M$: empty model | Left1.xmi | tbd |
| Model $m_2 \in M$: two persons | Left2.xmi | tbd |
| Model $m_3 \in M$: eight persons, including one with age 0 | Left3.xmi | tbd |
| Model $m_4 \in M$: three persons with names differing only in case and spaces | Left4.xmi | tbd |
| Meta-model $N$ | Right.ecore | tbd |
| Model $n_1 \in N$: empty model | Right1.xmi | tbd |
| Model $n_2 \in N$: two persons | Right2.xmi | tbd |
| Model $n_3 \in N$: eight persons | Right3.xmi | tbd |
| Model $n_4 \in N$: three persons with names differing only in case and spaces | Right4.xmi | tbd |
Program Person2Person.jar provides a consistency checker that should be used to access correctness. It also also provides model generators to be used in performance test cases. Given models Left.xmi and Right.xmi to check if they are consistent (both with their meta-models and among themselves) use:
java -jar Person2Person.jar Left.xmi Right.xmi
To generate a left model called Left.xmi with size n use:
java -jar Person2Person.jar genleft Left.xmi n
Similarly for a right model.
Test cases
Here is a summary of the existing test cases for this benchmark:
| Test case | Status | Operational mode | Kind | Measured features |
|---|---|---|---|---|
| Person2Person.BCF | Draft | Batch forward propagation | Conformance | Correctness, Completeness |
| Person2Person.BCB | Draft | Batch backward propagation | Conformance | Correctness, Completeness |
| Person2Person.BSF | Draft | Batch forward propagation | Performance | Runtime (scalability), Memory (scalability) |
| Person2Person.BSB | Draft | Batch backward propagation | Performance | Runtime (scalability), Memory (scalability) |
| Person2Person.MCB | Draft | State-based backward propagation | Conformance | Correctness, Completeness, Hippocraticness |
Only test cases marked as final can be referenced in publications.
Conformance of batch forward propagation
The goal of this test case is to assess the conformance of a batch forward propagation of type $\mathit{to} : M \to N$. This test case shall be identified as Person2Person.BCF, and benchmarked tools shall report the percentage of successful runs.
Each of the following runs is successful if the propagation always succeeds (completeness) and the produced right model is consistent with the input left model (correctness).
| Run | Propagation | Input left model |
|---|---|---|
| Person2Person.BCF.1 | $\mathit{to}$ | Left1.xmi |
| Person2Person.BCF.2 | $\mathit{to}$ | Left2.xmi |
| Person2Person.BCF.3 | $\mathit{to}$ | Left3.xmi |
| Person2Person.BCF.4 | $\mathit{to}$ | Left4.xmi |
Conformance of batch backward propagation
The goal of this test suite is to assess the conformance of a batch backward transformation of type $\mathit{from} : N \to M$. This test case shall be identified as Person2Person.BCB, and benchmarked tools shall report the percentage of successful runs.
Each of the following runs is successful if the propagation always succeeds (completeness) and the produced left model is consistent with the input right model (correctness).
| Run | Propagation | Input right model |
|---|---|---|
| Person2Person.BCB.1 | $\mathit{from}$ | Right1.xmi |
| Person2Person.BCB.2 | $\mathit{from}$ | Right2.xmi |
| Person2Person.BCB.3 | $\mathit{from}$ | Right3.xmi |
| Person2Person.BCB.4 | $\mathit{from}$ | Right4.xmi |
Performance (scalability) of batch forward propagation
The goal of this test case is to assess the performance of the forward propagation run in batch mode. This test case shall be identified as Person2Person.BSF, and benchmarked tools shall report runtime and memory scalability (O-notation) taking into account runs with increasing left-model sizes, starting from 1 and at least up to 1000 (created with the provided model generator).
Performance (scalability) of batch backward propagation
The goal of this test case is to assess the performance of the backward propagation run in batch mode. This test case shall be identified as Person2Person.BSB, and benchmarked tools shall report runtime and memory scalability (O-notation) taking into account runs with increasing right-model sizes, starting from 1 and at least up to 1000 (created with the provided model generator).
Conformance of state based backward propagation
The goal of this test case is to assess the conformance of a state based backward consistency restoration procedure. This test suite shall be identified as Person2Person.MCB, and benchmarked tools shall report the percentage of successful runs.
This test case can be applied to tools providing a propagation $\mathit{bwd} : M \times N \to M$, allowing the propagation of updates from the right model to the left one in the the style of constraint maintainers (where only the result state of updating the right model is known). Since the right model contains strictly less information than the left one, the dual test case is equivalent to batch forward propagation and thus is omitted.
Each of the following runs is successful if the backward propagation succeeds in producing a model (completeness), the output (updated) left model is consistent with the input right model (correctness) and, when the input original left model is already consistent with the input right model, the output left model should be equal (or isomorphic) to the input one (hippocraticness). Creation of default ages cannot be checked in general for this scenario, since deletion and posterior creation of a person in the right model is indistinguishable from name change.
| Run | Propagation | Input left model | Input right model |
|---|---|---|---|
| Person2Person.MCB.1 | $\mathit{bwd}$ | Left1.xmi | Right1.xmi |
| Person2Person.MCB.2 | $\mathit{bwd}$ | Left1.xmi | Right2.xmi |
Author(s)
Anthony Anjorin, Alcino Cunha, Holger Giese, Frank Hermann, Arend Rensink, AndySchuerr
Reviewer(s)
None yet.
Comments
- Any more references where this example was introduced? [alcino]
- Concerning test cases, suggestions of interesting runs to add are very much welcome! And interesting instances, of course. [alcino]