Example: Directed Graph Reachability in Presence of Variability

by Michał Antkiewicz, updated on Oct 27, 2015

With the features recently introduced to Clafer 0.4.1 (nested abstract clafers and reference refinement, see Clafer 0.4.0 PowerPoint Slide Show, and Alloy and Choco escapes), we can now conveniently model directed graphs in Clafer and express constraints such as node reachability in a graph by escaping to Alloy.

On Oct 26, 2015, I gave a talk on the topic. Slides in PPSX. Slides in PDF.

The talk was based on the wiki page

Directed Graph Reachability in Presence of Variability

on Clafer Model Wiki shows an example.

Clafer Cheat Sheet and Syntax Documentation

by Michał Antkiewicz

Clafer has a formal grammar from which the lexer and parser are generated. I published two new language reference resources: 

• Syntax documentation (pdf), which is also automatically generated from the grammar
• Clafer cheat sheet, which is written manually based on the grammar to provide additional commentary and type information, while sacrificing the formality of the grammar.

All these resources, as of this posting, cover Clafer 0.4.1 and they will be updated with each release. They are also referenced from the page Documentation.