Clafer Evaluation

We have evaluated Clafer on over 60 realistic examples of feature models, meta-models, and feature-based templates. For each model, we performed instance finding analysis, since many other analyses can be reduced to this problem. For slices of meta-models and feature-based templates element liveness was verified, because it is another example of a non-trivial analysis. We consider our results promising, since we obtained acceptable timings (within seconds) without fully exploiting the potential of Alloy.

The attached files contain Clafer (*.cfr files) and corresponding Alloy (*.als files) models.

Language documentation is available here.