feat: SAT-based semantic check of class diagrams + OCL constraints

[pponzio]

What

An implementation of SAT-based semantic checking for BUML class diagrams with OCL constraints. The semantic check of class diagrams and OCL constraints is based on a characterization of these modeling elements into the Alloy formal notation, and the use of SAT solving (via Alloy Analyzer) for consistency checking.

We added documentation in the following files briefly explaining how to use the new features:

• docs/source/tutorials/first-project.rst
• docs/source/user-guide/diagrams/class-diagram.rst

Why

This is a new feature of BESSER. Semantic checking goes beyond just checking correct syntax of a model: it allows developers to check for logical consistency of model constraints, and thus to identify overlooked contradictions and inconsistencies in constraints.

How

The implementation is rather straightforward. The new functionality splits the original Quality Check functionality into Syntactic Check (existing check) and the newly implemented SAT-based check, under Semantic Check. The implementation also allows the user to generate the translation from model and constraints into Alloy, under Generate - Formal Notations - Alloy Specification.

Finally, in the Object Editor, there is an additional functionality, associated with the button “Semantic generation”. This allows the user to generate an object diagram compliant with the OCL constraints, witnessing the consistency of the class diagram and OCL constraints. This object diagram is generated by resorting to SAT solving, via Alloy Analyzer instance generation.

Testing

Manually tested with multiple examples, including sample models provided with the BESSER distribution, and newly added models, exercising various aspects of the OCL notation.

Screenshots / Recordings

Added Menu: Generate -> Formal Notations -> Alloy Specification

Generates an Alloy specification from a Class diagram.

After:

Before:

Added Menus:

Quality Check -> Syntactic Check (old Quality Check)
Quality Check -> Semantic Check

Semantic consistency checks of Class diagrams.

After:

Before:

Added Button: Semantic generation

Automatic generation of an object diagram

After:

Before: