Clafer Evaluation

We have evaluated Clafer on hundreds realistic examples of feature models, meta-models, feature-based templates, and domain models. 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 archive contains Clafer (*.cfr files) and corresponding Alloy (*.als files) models.