lamp abstraction
In Clafer, abstract clafers are defined using a keyword
abstract, which means that there will never be any direct
instances of that clafer in a model. We can extract the common parts of
every lamp into an abstraction as follows:
then, we can inherit the properties and
the xor constraint from the abstraction as follows:
The clafer TrafficLight is a concrete
clafer, which is why we see instances generated for it in the
configurator. The clafers for each lamp are also concrete and they only
inherit properties from the abstract clafer Lamp.
This model change is a refactoring–change of structure without changing the semantics; the set of instances of the model remains the same.
From now on, always use the Alloy-based instance
generator.
Now, let’s analyze the 
valid states of a
traffic light.
Previous
