Semantics Definition

The semantics currently supported by Lightning is an Operational semantics. It is currently in an experimental state and thus we do not yet provide a full documentation.

work in progress

We are currently investigating the use of functional module in order to define semantics as a transformation from semantics instance to semantics instance. A semantics instance being an encapsulation of the Abstract syntax with notions of States and Traces. This feature will be supported soon.

If you still want to play with it

If you want to play a bit with semantics, you should have a Semantics.als model in your semantics folder that imports the abstract syntax model. It should define a signature named State that provides the notion of semantics state to the language model. in order to access the index of the State in a functional alloy module (for visualization of the semantics), just use the $currentState variable.