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, as well as automated generation of logically consistent object diagrams. 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. Alloy Analyzer is used to produce semantically compliant instances, which are translated back into BESSER as object diagrams.

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

• docs/source/api/api_generators.rst
• docs/source/api/generators/api_alloy.rst
• docs/source/generators.rst
• docs/source/generators/alloy.rst
• docs/source/web_editor_backend.rst

Depends on: Merging the frontend’s pull request uvamarcelo1977/BESSER-Web-Modeling-Editor/erator-integration#183.

We updated the frontend submodule pointer accordingly.

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. Moreover, this implementation is able to produce object diagrams that are not only syntactically consistent with a class diagram, but also semantically consistent with cardinality constraints and OCL constraints present in the model.

How

The implementation involves some minor fixes and additions to BESSER, as well as two major new functionalities:

• A new translation from BUML class diagrams + OCL constraints into the Alloy notation.
• A translation of an Alloy instance file (representing a logical model of an Alloy specification) into a BUML object diagram.

The minor fixes and additions are, basically, syntactic support for OCL operators that were not supported in BESSER (e.g., IsKindOf, Includes, etc).

Testing

Further Unit tests were added/updated, specifically targeting the new functionality:

• tests/generators/alloy/test_alloy_generator.py
• tests/generators/alloy/test_alloy_generator_football.py

Manual checks were also performed on newly devised BESSER case studies, that incorporate complex OCL constraints:

• tests/BUML/metamodel/structural/HospitalManagementSystem.py
• tests/BUML/metamodel/structural/genealogy.py
• tests/BUML/metamodel/structural/nodeCachingLinkedList.py

Screenshots / Recordings

Follow-ups / Known limitations

[ArmenSl]

Hi @uvamarcelo1977, @pponzio thanks for the contribution. Semantic checking is something we've wanted in BESSER for a while, and the design is genuinely nice: the Alloy translation, the streaming progress over increasing scopes, and generating a consistent object diagram back into the editor. I also appreciated that the object-diagram conversion is AST-based and that the translation tests run without Java.

I did a first pass focused on the structural side before we go into the detailed backend/frontend reviews. A few things we need to sort out first, and some of them involve other repos, so bear with me:

Please rebase on current development. The diff currently deletes the test_case and bpmn generator registrations in config/generators.py I assume a conflict-resolution accident, but as-is it would regress two shipped features.

On the OCL grammar. Removing Type::allInstances() breaks models people have already saved, so we should keep it. The good news is that Fitash's #585 (just approved) adds most of what you needed asSet, intersection, and the standard dot-form allInstances() while keeping the old syntax. So the simplest path is: since #585 is in, rebase this branch on developpement and drop your own edits to BOCL.g4 and the regenerated ANTLR files. If you still miss operators after that (I think closure, including/excluding and the enum literals are yours only), you can add them on top of that grammar and we'll review them.

One thing that's easy to miss: the editor evaluates OCL constraints through the B-OCL interpreter, which is a separate package (bocl on PyPI, own repo). Anything that parses here but can't be evaluated there gives users confusing validation results. So the new operators also need interpreter support in that repo before we ship this @FitashUlHaq can guide you there.

On the alloy.jar. Could you remove the 19 MB jar out of the repo? It stays in the git history forever, and it never reaches users anyway our packaging only ships *.j2 files, so a pip install has no jar and the code silently falls back to the BESSER_ALLOY_JAR env var. Downloading it on demand (or documenting the install) would be much better. AMost importantly let’s keep one canonical location. Right now, the JAR is under BUML/notations/ocl/consistency/, while the code lives in generators/alloy_generator/. We also need to verify the license/attribution requirements for redistributing Alloy Analyzer.

On Java in production. I saw JRE support was added to the Docker setup and then reverted. As the PR stands, the deployed editor image has no java, so both new endpoints would fail in production. We need the deployment side back in (or as a linked change). Related question, maybe for @rdegiovanni too: do you see this as an editor-only feature, or should it also work from a pip-installed BESSER? The answer drives how we handle both the jar and the JRE.

A few smaller things you can fold into the same pass:

• pipeline.py, step_1_buml_alloy.py and step_2_alloy_to_xml.py look like your local experiment scripts rather than library code (Spanish output, print-based CLIs, duplicated java -jar calls) the backend doesn't use them, so please drop them from the package or move them out of the installed tree.
• The package should follow our generator naming: besser/generators/alloy/ rather than alloy_generator/ (see react/, django/, terraform/…).
• The three sample models added at the top of tests/BUML/metamodel/structural/ should each get their own subfolder, like the existing examples (library/library.py, etc.)

Once the rebase and the grammar alignment with #585 are done, we'll do the full review on both sides.

Thank you very much !!

[pponzio]

Hello @ArmenSl,

First, we would like to thank you for your in-depth and insightful review. We are currently working on a new pull request based on your suggestions.

Regarding OCL, we will roll back our changes and start again from the current development branch and follow your suggestions.

Regarding Java and the alloy.jar, we are waiting for Renzo to come back from vacation to discuss with him what's the best way to add these tools.

And of course we are rolling back the changes we involuntarily made to existing generators (sorry for that).

Finally, we are doing a refactor to remove some duplicated code (and some old code that is not used anymore), and to improve the APIs of our classes (mostly to facilitate the generation of B-UML object diagrams using Alloy). This is the part that is taking longer, but we believe we will be sending a new pull request with all these improvements early next week.

Best regards,
Marcelo, Naza and Pablo.

[ArmenSl]

Closing this one in favour of #614, which is the new version you opened with the changes from the review above. We'll continue the review there. Thanks again @pponzio @uvamarcelo1977!