Verification

The verification in Lightning is performed using the automatic analysis provided by Alloy. It thus relies on the small scope hypothesis that claims that most of the design errors can be found in small instantiations. Lightning allows currently the verification of language definitions and will gradually provide support for language to language transformations verification.

How is the verification performed?

Step 1: Instance Generation

The verification is first performed via the generation of an Abstract Syntax instances. This instance is by default visualized using a visualization similar to the one provided by the Alloy Analyzer (it reflects the structure of the instance).
The instance generation is performed by simply "running" a language. (run as > generate instance or press the launch shortcut button). If several models are present in the Abstract Syntax Folder, then you will be requested to choose one. This choice will be remember for the given model, and can later be modified in the run configurations.
At this stage, the verification of the abstract syntax's correctness via visualization is thus already possible. For complex instances though, this verification can be tedious due to the overwhelming number of elements and connections. It is thus preferable to perform this verification once the concrete syntax is applied.

Step 2: Concrete Syntax Application

Remember that we have defined a concrete syntax definition as consisting of a transformation between the Abstract Syntax and a Visual Language model. Thus, in order to visualize the currently displayed instance using the concrete syntax we have defined, we first need to apply this transformation. This is done by simply selecting it in the first combo-box.
Once this selection is made, you will see a raw representation of the transformation output. In order to ask the tool to interpret visual elements and to render them accordingly, you will need to select the "CS with GEF" option in the second combobox.
Your language model should now appear in a far more readable way. You can now browse several instances (the selected instance and filter will be applied automatically), and spot design errors more easily. Note now that you are verifying your concrete syntax definition at the same time than your abstract syntax definition.