Station Building Blocks
In order to implement a product line of train station we need a way to represent the solution space.
In many system the solution space is represented as code in some existing programming language. In the train station domain, and in the context of the DSM-TP summer school, it seems more appropriate to consider a small DSL that will describe train station designs.
We will use the same language (Clafer) to design a simple, under-constrained, meta-model for railway station track design.
Now it is more useful to think about clafers as classes, than as features; although obviously nothing changes from the language perspective, they remain just clafers.
The track layout will be built of elements of type
Track
:
Each
Track
will have a set of pointers toincident
tracks. The arrow represents a reference to a set (a uni-directional association). The cardinality constraint as previously constraints the amount of incident clafers, so it carries also to the referenced set.For the first time, we see cardinalities higher than one. In our models we will consider tracks that can connect to up to three other tracks.
We have two constraints. The first one assumes that the incidence relation is symmetric: so if track A is incident to a track B, then also track B is incident to A. It is written here using the
parent
keyword which refers to the parent of the context (so an instance of the track), as opposed tothis
which refers to the context clafer.The use of
this
here implicitly follows the reference for convenience. The fully desugared constraint could also be written asthis.parent in this.dref.incident.dref
.The second constraint is written in the context of the root clafer, and it states that a track cannot be incident with itself. Here
&
is the set intersection operator. Again the reference from incident is followed automatically, so the parenthesized expression means(this & incident.dref)
.In Clafer, like in Alloy, expressions are set valued, so an instance expression represents a set of instances (possibly empty, possibly singleton, but perhaps larger).
The keyword
this
actually represents a singleton set containing the context instance, whileincident.dref
represents a set of incident tracks. This is why it makes sense to compute an intersection of the two.The quantifier
no
turns a set into a Boolean value, true if the following set is empty, and false otherwise.Like in Alloy, the default quantifier is
some
(meaning a singleton or a larger set, roughly corresponding to existential quantification).Some
is inserted everywhere in front of sets, where a Boolean value is expected; this is why our constraints in the first part looked like propositional, despite operating on sets.Having introduced the basic type of tracks, we now refine it to four subtypes, which we will later instantiate to build stations. Simple tracks are straight line tracks, with two connection endpoints.
The
#
symbol is a set cardinality operator:
- A junction is a track with three endpoints:
- An incoming or outgoing line will only have one endpoint (the other of its ends is irrelevant for modeling the station):
Note that
one
is another quantifier. It results in true iff the subsequent set is a singleton.A track barrier is a kind of track that is blind (or allows to close an open track safely):
- Instantiate this meta-model creating a domain specific model of a station (or more precisely an abstract syntax of it) :
In our model we have one incoming line (
I1
), one outgoing line (I2
) and one simple track (T1
) which is connected to the two lines. This is a very common case of a single track rural station.the
++
operator denotes set union.Since we could always make a mistake, it is useful to ask the Clafer instance generator, to check whether this model is consistent. It should return exactly one instance, as the model is fully specified (no variability).
Task 6
- Now once you have the model opened in Clafer IDE change it to a model of an even simpler station that has one incoming track and is blind on the other side. Like the following beatiful station in Rabka, which I visited during a recent summer hike:
![The train station in Rabka (there is only a barrier in the other direction)](/rabka.jpg)
- Remember to use the instance generator to see whether your design is consistent with the meta-model.
With this super simple DSL we can move to Part III Base Model.
Previous