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.