Clafers

A Clafer model consists of basic elements called clafers and constraints. Clafers express concepts and variabilities among them. Let us look at a Clafer model that shows the structure of a car:

car
  engine
  radio
    cdPlayer

The model tells us that a car has an engine and a radio. In other words, engine and radio are parts of a car. We express the has relationship by indenting clafers to the right with respect to their parent. Similarly, radio has a built-in cdPlayer.

We understand the meaning of Clafer models in terms of possible configurations. Configuration is a model with no variability, such as the above car example. Generally, there are many configurations that conform to a Clafer model.

Terminology

Clafers form a hierarchy denoted by code indentation. Based on the car example, we use the following terminology related to the hierarchy of clafers:

• car is a root, a parent of engine and radio, and an ascendant of cdPlayer.
• engine is a child of car, and sibling of radio
• radio is a child of car, sibling of engine, and parent of cdPlayer.
• cdPlayer is a child of radio, and descendant of car.

Clafer Source Files

Clafer is a textual language. Clafer models are written in text files, similarly to programs written in C, C++, Java, or Haskell. A text file contains clafer definitions and constraints. Althogh the indentation of clafers matters (for forming hierarchy), their order in the text file may be arbitrary. The following two files have exactly the same meaning:

1. Engine before radio
   

   car
     engine
     radio
       cdPlayer

2. Radio before engine
   

   car
     radio
       cdPlayer
     engine

Clafer models try to resemble concept definitions written in a natural language. Sometimes, however, one needs to add additional comments that clarify the meaning of a model. We use comments for that purpose. Clafer uses the same syntax as C, C++, and Java, that is // for inline comments and /* */ for multiline comments. For example:

car  // car is a vehicle that has engine and radio
  engine
  /* In reality there are many types of radios.
     In our model there is only one type. It is
     a radio with CD player.
  */
  radio
    cdPlayer

What to do with Clafer models?

Alright, let’s say you have a Clafer model specified in a text file. What can you do with it? There are two fundamental ways of using Clafer models:

1. Communication. The models are meant to be shared and discussed. They serve as a means of documenting ideas and their structure. They are very like a system specification or documentation.
2. Analysis. Clafer models are analyzable by SAT / SMT -solvers and Alloy Analyzer. There are many interesting analyses that one can perform using those tools: checking consistency, finding conflicing constraints, fixing broken configurations, generating examples, finding dead clafers, etc.

Clafer Infrastructure

Our current Clafer infrastructure includes Clafer translator and Clafer Instance Generator. The former translates Clafer models to other notations (as for now: Alloy, XML, desugared Clafer). The latter takes a Clafer model and generates its configurations.

Working with Clafer translator
A typical Clafer translator workflow looks as follows:

1. Edit model in a text file, e.g. input.cfr
2. Translate the model to Alloy with command: clafer input.cfr
3. Run Alloy Analyzer, adjust the scope of analysis, generate model instance.
4. If model refinement is needed, go back to step 1.

Working with Clafer Instance Generator
A typical ClaferIG workflow looks as follows:

1. Edit model in a text file, e.g. input.cfr
2. Generate the first instance: claferIG input.cfr
3. Generate another instance by typing n within ClaferIG
4. If needed, adjust the scope of analysis, generate model instance.
5. If model refinement is needed, go back to step 1.

FAQ

In the above example, is it possible to have a car without radio ?

No, radio is present if and only if car is present. The same dependency exists between radio and cdPlayer.

---

How to pronounce Clafer?

The name Clafer comes from Class, Feature, Relationship. Thus, the first syllable “cla” sounds the same as in the word “class”.

---

What are correct names of clafers?

Names of clafers start with a small or capital letter. Each name has to be a continuous string of non-white-space characters (no spaces are allowed).

---

Do clafer names have to be unique?

They have to be unique if they have the same parent. The model:

car
  type
    type

is legal, because the more indented type has a different parent than the less indented type. On the other hand, the following is illegal:

car
  type
  type

because the two type s are at the same level of nesting and cause a name clash.

---

How to execute Clafer models?

Currently, Clafer models specify structure, not behavior. Therefore, they are not executable but analyzable. One can verify certain properties of those models.