Our lab is a very exciting place to learn and work!
Concept Modeling with OWL and Clafer
A presentation introducing Clafer, comparing concept modeling in OWL and Clafer, and presenting the details of a translation of the tutorial Pizza example from OWL to Clafer is available for viewing here.
To view, hoover mouse over the lower-right corner of the presentation More and select Fullscreen. Use right arrow to advance, left arrow to go back. Click on an element to zoom in. Click on empty space to zoom out. Use mouse wheel to zoom in and out. Use drag & drop to pan.
The translation of the Pizza example into Clafer is attached below (pizza.cfr). The translation is almost complete: it is missing IceCream and other inconsistent parts, and a few minor details.
The file pizza-only-Veneziana.als is a translation of the Clafer model to alloy which can be run using Alloy 4 analyzer (it gives semantics to the Clafer model in terms of alloy). The translation omits all unused abstract pizza types except for Veneziana which is instantiated.
To analyze and instantiate the model, open the file in Alloy 4 analyzer, press the buttons execute and, after analysis is completed, show. This will visualize an instance of the model found by Alloy that conforms to all constraints. The Alloy model represents a lower bound of the space of instances, that is, Alloy may create more instances than necessary to satisfy the constraints.
Instead of the standard graph visualization, the instance can also be viewed as a tree by clicking on the button Tree in the instance viewer. Subsequent instances can be generated by pressing Next.