Bx Examples Repository
Title: Water Tank
Version: 0.1
Type: Precise
Overview
Demonstrates a certain requirement against synchronizers (also the fact that it is difficult to achieve) that is unique to multiary transformations (as in, it does not occur in binary snychronization). This property was raised in the 2018 Dagstuhl seminar, and has no accepted name in literature nor a formal definition yet; for now, let us call it freedom from whack-a-mole behaviour.
From Wikipedia:
The term "Whac-a-mole" (or "Whack-a-mole") is used colloquially to denote a repetitious and futile task: each time an adversary is "whacked", it only pops up again somewhere else. In a military context, the term is used to refer to ostensibly inferior opposing troops who keep re-appearing. In a programming/debugging context it refers to the fact that fixing a bug has a certain chance of creating a new bug which itself needs to be fixed.
Models
Three engineers collaborate to create a factory design that includes, among other irrelevant details, a water tank. The tank is a rectangular block with dimensions X meters by Y meters by Z meters, and its volume is required to be exactly 1 cubic meters.
Each of the three engineers work with different cross-sections / perspectives / projections of the factory, so each of them is responsible for choosing the extent of the tank along a different axis. Thus (with a slight abuse of notation) engineer X is responsible for specifying the width X in their model, engineer Y is is responsible for specifying the depth Y in their model, while engineer Z is responsible for specifying the height Z. For the purposes of this example, we ignore any other information the engineers have in their model. Specifically, each engineer may even have read-only information on the other two dimensions, but crucially they are only allowed to / qualified to / responsible to determine the single dimension assigned to them.
To sum up, we have
- three models X,Y,Z,
- each with a model space isomorphic to the positive real numbers.
Consistency
The three models X,Y,Z are consistent for concrete values x,y,z IFF x*y*z = 1 m3.
(Note that both models and the notion of consistency are symmetric to permutation of the axes X,Y,Z.)
Consistency Restoration
Several consistency restoration strategies will be outlined. In their descriptions, we assume X is the most recently changed ("authoritive") model, and Y and Z have to be adjusted. Due to the symmetry of the axes, this is without any loss of generality.
Here we first outline one restorer to demonstrate (the lack of) the desired property, and later introduce more
- SPLIT
- if y*z = 1.0/x, do nothing (hippocraticness);
- otherwise, set y=z := 1/sqrt(x)
Properties
We need well-behaved consistency restorers that are additionally whack-a-mole free. As currently I am unaware of a formal definition of the latter property, an informal requirement is given below:
- Take any consistent multi-model (modulo reasonable equivalence/compatibility classes of multi-models) as desirable state, and any (consistent or non-consistent) multi-model as initial state. The property requires that the desirable state will be reached from the initial state by repeating steps of (i) arbitrarily taking a model (or several models) that is not yet in its desired state, (ii) adjusting it to its desired state (variant: or as close as possible given local consistency, read and write permissions), and (iii) using the consistency restorer to propagate the changes to the other models. (Additionally, the number of steps required must not be unreasonably large, i.e. the process should not take much longer than the number of models involved.)
The motivation behind such a requirement is that in order for the multx to serve its purpose in the engineering process, the consistency restoration mechanism must not prevent the engineers from being able to reach any desired solution.
Note that of course, even without this property, it is always possible to set all models at once to the desired state, after which a hippocrartic multx will not interfere. However, this is not a satisfactory alternative, as it would require coordination between the engineers beyond what is provided by the models themselves - so the multx as specified is not helpful.
SPLIT above is an example of a restorer that is well-behaved, but does unfortunately engage in whack-a-mole behaviour. When it intervenes, the restorer always leaves two of the axes with the same dimensions. A desired state of (0.5m, 1m, 2m), or any other desired state with three different edge dimensions, is thus not universally reachable (in fact, not reachable from any other consistent state).
Variants
Alternative consistency restorers to investigate:
- PROPORTIONAL
- let w = 1/sqrt(x*y*z) in
- set (y,z) := (y*w,z*w)
- LRU (note that this is not purely state-based)
- assume without loss of generality that Y was more (or equally) recently updated than Z, i.e. X,Y,Z are ordered "most authoritive" to "least authoritive"
- set z := 1/x*y
Like SPLIT, PROPORTIONAL is also well-behaved and it also "feels nicer" (why?), but it still engages in whack-a-mole. Although it at least converges to the desired solution (the sum of the squared errors of the logarithms of the dimensions is decreasing monotonically).
LRU is both well-behaved and refreshingly free of whack-a-mole. To reach a given state, we have to first update one of the models, then an another one, and then we are done.
Discussion
While LRU appears to be the preferred solution, its definition was based on the update history of the three models; it is not possible to implement using the conventional formalisms of the community (state-based synchronizers, delta lenses, etc.) without reifying at least some history information into the models. The description above informally introduced LRU using a nonstandard notion of gradual authoritiveness based on how recently each model was updated. The author of the example has no idea how to capture the definition nicely in a future-proof framework of discourse.
The whack-a-mole freedom property is unique to multxs, since it is not relevant for binary synchronizations (without reflective updates). This is because any well-behaved BX without reflective updates between models X and Y is automatically free from whack-a-mole behaviour: after setting X to its desired state and propagating to Y, the two models will now be consistent; the restorer may have chosen a model y that is different from the desired one, but this can be fixed by updating Y, which the restorer will leave be due to hippocraticness. On the other hand, for three models, we have seen examples (SPLIT, PROPORTIONAL) of multxs that are well-behaved but not free from whack-a-mole behaviour.
The whack-a-mole freedom property is distinct from other multx properties (well-behavedness, very-well behavedness, history ignorance, non-interference, confluence etc.) discussed in literature, up to the awareness of the author.
- In particular, it is distinct from resolvability (see P. Stevens, Bidirectional Transformations in the Large, MODELS 2018), which (a) only propagates a single initial set of authoritive models, not an even longer iterative process where engineers repeatedly adjust different models, also (b) only guarantees the existence of one path, and (c) only guarantees consistency, not the desired result.
- Furthermore, the author argues the property is distinct from "least change/surprise". LC/LS is considered for a single act of consistency restoration, not a longer engineering workflow. The author also intuitively believes that whack-a-mole freedom is not implied by all individual restorations adhering to LC/LS, but has no good arguments at the moment to support this.
Author(s)
Gábor Bergmann
Reviewer(s)
We intend that examples remain provisional (version 0.x) until reviewed (and approved, if necessary after modification) by other members of the wiki. In the interest of traceability and credit, such reviewers are identified here.
Comments
The CLOCKWISE solution
by Gábor Bergmann, original author.
Another interesting variant solution occurred to me recently. This one is only cyclically symmetrical among the three models.
- CLOCKWISE
- consistency restoration after modifying X from x to x': set y' := yx/x'
- consistency restoration after modifying Y from y to y': set z' := zy/y'
- consistency restoration after modifying Z from z to z': set x' := xz/z'
It is easy to see that this has the nice property that any desired consistent multimodel state $\langle x_D,y_D,z_D \rangle$ can be reached, starting from any consistent initial state $\langle x_I,y_I,z_I \rangle$, by updating first X, then Y and then Z to its desired value. Unfortunately, executing these updates out of order will lead to an incorrect result: if we update first Z, next Y, and finally X, then instead of the desired multimodel $\langle x_D,y_D,z_D \rangle$, we end up with $\langle x_D, y_D\frac{x_Iz_I}{x_Dz_D}, z_D\frac{y_I}{y_D} \rangle$ instead. So with the right engineering workflow, the desired state can be achieved; but this requires very tight coordination between the collaborating participants, not suitable for independent or especially distributed co-engineering.
Artefacts [optional section]
Formal descriptions, perhaps downloadable code, example inputs and outputs, virtual machine instances, diagrams…
