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.

• Depends on: Merging the frontend’s pull request Reordering of the attributes in the web modeling editor #183 - “feat: SAT-based semantic check of class diagrams + OCL constraints”.

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, implemented by the AlloyGenerator class (documented in docs/source/generators/alloy.rst, see below).
Automated generation of BUML object diagrams, implemented by the AlloySolver class (documented in docs/source/generators/object_diagram.rst).

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

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

As the AlloySolver employs the Alloy Analyzer as a backend, it depends on the following software:

• Java JDK 17 or greater.
• The Alloy Analyzer 6.2 .jar.

Also, the following environment variables must be set for consistency checks/object diagram generation:

• JAVA_HOME: The path to the Java JDK installation.
• BESSER_ALLOY_JAR: The path to the Alloy Analyzer file (must be named alloy.jar).

We updated Dockerfile to automatically download and install these dependencies, and set the environment variables. We also added a THIRD_PARTY_LICENSES.md disclosing the use of the Alloy Analyzer (which has an Open Source MIT License).

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

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
• tests/generators/alloy/test_alloy_solver.py

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

• tests/BUML/metamodel/structural/genealogy/genealogy.py
• tests/BUML/metamodel/structural/hospital/hospitalManagementSystem.py
• tests/BUML/metamodel/structural/nodecachinglist/nodecachinglist.py
• tests/BUML/metamodel/structural/school/school.py

[ArmenSl]

Thanks for opening the new PR, and for addressing the points from #586. The feature is valuable: finding out whether a class diagram and its OCL have any valid instance, and getting a sample object diagram, is something BESSER can't do today. We'd like to merge it.

A good part of it already works. The branch merges cleanly into the current development, and with the Alloy Analyzer installed the whole flow runs: generating the .als, solving, and returning an object diagram with objects and attribute values. I ran the branch against a range of models, and here is what needs to change before we merge.

Must fix before merge

1. Constraints are mistranslated with no warning. Some OCL is turned into Alloy that means something else, so the check answers a question about a different model:

   • x implies false becomes always true.
   • a xor b keeps only a.
   • self.pages * 2 > 10 loses the multiplication.
   • a implies b or c is grouped as (a implies b) or c.
   • let and .abs() produce broken Alloy.
   • Trailing tokens are silently dropped.

   Most of these come from the translator's own parser: it flattens the ANTLR tree back into text tokens and parses them a second time. The translator should work directly on the typed OCL tree from parse_ocl (besser/BUML/metamodel/ocl). This PR already extends that tree with including/excluding, and it already handles precedence, xor, * and syntax errors. A visitor that generates Alloy per node type, and reports any construct it doesn't support ("unsupported construct X") instead of approximating it, avoids adding a second OCL implementation to the codebase. This should be done in this PR rather than later.

2. "Unsatisfiable" is overstated. The integer bit width equals the scope, so at scope 5 integers only go up to 15:

   • self.pages > 20 is UNSAT at scope 5 and only SAT at scope 10.
   • self.pages > 600 and self.bs->size() >= 12 are reported as "Model is likely unsatisfiable", although both are trivially satisfiable.
   • A timeout is also reported as "model may be unsatisfiable".

   Please derive the bit width from the integer literals in the OCL, and report results as "no instance found within N objects / integers in [a, b]". A timeout should be shown as a timeout. The run line also repeats 5 Str.

3. B-UML features are dropped silently.

   • Multiple inheritance is emitted as sig X in A + B. Alloy then refuses the scope ("Cannot specify a scope for a subset signature"), so the check crashes.
   • An abstract class that has a parent loses abstract.
   • float is mapped to Int.
   • A 0..1 attribute becomes required.
   • An association class is emitted as a separate sig with no link to its association.

   Each of these should either be supported or raise a clear error.

4. Strings are not preserved.

   • String literals in OCL are lower-cased during translation.
   • On the way back, self.title = 'good Morning' gives title="strings/Str0" (the internal name) instead of the value.
   • Character atoms such as c32 (a space) are decoded as the literal text "c32".

5. Shared state and reproducibility. DATES_DICT in date_ops.py is a module-level dict rebuilt on every request, and requests run in parallel threads, so concurrent checks can decode each other's dates. Filler dates also come from an unseeded random.randint. Three runs of the same model gave three different release dates. Please pass this state explicitly and make date generation deterministic.

6. Frontend timeout (WME Reordering of the attributes in the web modeling editor #183). postSSE falls back to the 30 s default timeout, and that timer keeps running while the stream is being read. Neither checkConsistencyModel.ts nor DiagramTabs.tsx passes a longer one, while the backend can search for up to 4 scopes × 50 s. So any check that takes more than 30 s is cut off in the editor. Please pass an explicit timeout that covers the backend budget.

Smaller fixes

• OCL grammar:

  • After the grammar change, an attribute named closure no longer parses (self.closure > 0 was fine before).
  • ->closure(...) and ->including(...) now parse, but the OCL evaluator (bocl) can't evaluate them, so they fail later with a less clear error.

  Please keep the new operators from breaking existing identifiers, and either support them in evaluation or reject them clearly.

• CI: test_generates_als_file_and_sanitizes_names fails when the Alloy jar isn't installed; it should be skipped like the other solver tests. Ruff reports 5 errors in besser/generators/alloy.

• Docs: docs/source/generators/alloy.rst:15 imports from besser.generators.alloy_generator; it should be besser.generators.alloy. Please also document which OCL constructs are supported, and what a satisfiable or unsatisfiable result means given the bounds.

Structure (to align with the rest of the codebase)

• The .als export fits well as a generator (AlloyGenerator plus its entry in config/generators.py). The satisfiability check and instance extraction are validation features, though, and belong in the validation services rather than besser/generators/alloy/instance_generator/.
• alloy_instance_to_BUML.py writes model code in a special dialect that isn't meant to be run, only so it can be parsed back into JSON. Please build an ObjectModel directly and pass it to the existing object converter.

Happy to do another round once these are in. Points 1 to 3 matter most, since they decide whether users can trust the answer.

[ArmenSl]

Two additions to my review above:

Unsupported features don't have to be implemented now. For points 1 and 3, full support isn't required for this PR. When the model uses something the translation doesn't cover yet (multiple inheritance, association classes, float, let, xor, …), it's fine to skip it as long as the user is told. For example, the check could return a warning like "constraint inv3 uses xor, which is not supported yet, and was not checked", or "class Hybrid has multiple parents; the check was skipped". What we want to avoid is a result that looks valid but was computed on a different model. Point 2 is the same idea: report what was actually checked (the bounds, and any constraints or features that were skipped).

Please add a complete example to the docs. The Alloy page currently shows only the generation step and a single invariant. It would really help to have one full walkthrough:

• a small model with a few OCL invariants;
• the generated .als (the fact snippet in the docs currently says self.book_pages, but the generator now emits self.Book_pages);
• running the check from Python, and showing the result;
• the generated object diagram;
• the same flow in the web editor (where the button is, and what the result looks like, with a screenshot);
• one case where no instance is found, and one with an unsupported construct, so users can see what those messages look like.

[jcabot]

You say :" the translator should work on the typed OCL tree from parse_ocl (besser/BUML/metamodel/ocl) instead of re-tokenising and parsing strings a second time. That avoids a third OCL implementation in the codebase."

Not sure this is longer term instead of something to be addressed now.

Is there a technical reason for not using the parsed tree we already have?

And what is the other OCL implemeentation???? (you say this would be three meaning we have 2)

[ArmenSl]

You're right on both points. I was imprecise.

The “other” OCL implementation:
I was counting BESSER's own OCL support, the ANTLR grammar and visitor that build the typed tree in besser/BUML/metamodel/ocl, returned by parse_ocl and the bocl package, which evaluates OCL, as two separate pieces.
However, bocl reuses exactly the same parser and visitor and only adds evaluation on top of the resulting tree. So, strictly speaking, this PR introduces a second OCL implementation, not a third.

Why don't use the parsed tree:
I don't see any technical reason for it. The translator calls our ANTLR parser, but then flattens the resulting tree back into text tokens and parses those tokens again using its own hand-written parser. It also generates Alloy using string and regex manipulation.
This PR even extends the typed tree they added including/excluding support to the visitor but then does not use that tree for the translation. The generator already has everything parse_ocl needs: the model and the context class. This should be addressed in this PR

Most of the mistranslations I found come from that second parser, including:

• incorrect precedence between implies and or;
• xor and * being silently dropped; and
• trailing tokens being ignored.
  With the typed tree, these cases are already handled by the grammar.

A visitor that generates Alloy based on each OCL node type and explicitly reports anything it does not support would also provide the “inform the user” behaviour we want.

The date and string handling, as well as the solver-related parts, can mostly remain as they are. Only the OCL front end needs to be rewritten.

I will update my comments