Conversion Between Language Levels

Universal-Variability-Language / uvl-lsp

Language server protocol for the Universal Variability Language (UVL)

MIT License

10 stars 3 forks source link

Conversion Between Language Levels #7

Open SundermannC opened 1 year ago

SundermannC commented 1 year ago

In addition to the core language, UVL supports several language levels that encapsulate more sophisticated language features. See the bachelor's thesis of Stefan Vill for more details. In particular, the following levels are currently supported.

SAT level
- Group Cardinality
SMT level
- Feature Cardinality
- Attribute Aggregates
TYPE level
- Constraints over numerical features
- Constraints over string features

While UVLS supports all listed language levels, other tools typically only support a subset. Transforming language constructs of a language level by transforming it to a "lower" level should simplify the usage of UVL models. Such transformations are also considered in uvl-parser2.0.

ThiBruUU commented 11 months ago

UVLParser: Extending UVL with Language Levels and Conversion Strategies

ThiBruUU commented 11 months ago

Link to the cloudstore file, which shows all possible functions and translations

MartinMUU commented 11 months ago

There are some unanswered questions about this issue:

how to translate constraints with dynamic attributes?
in the linked paper, the String and Numeric constraints are just dropped. Should handle it the same way?

SundermannC commented 11 months ago

The first question is a very good point and I think that the original translation considered in the bachelor's thesis of Vill will not work. However, bit blasting as done here may still be a valid option I think.

Regarding the second question, string constraints are just dropped and I do not think we currently have a sensible option to keep the semantics. Numeric constraints however should be kept and later transformed, also according to the paper.

SundermannC commented 11 months ago

In general, for a first version it may also be completely valid to just drop certain constructs and add semantic-preserving transformations later.

SundermannC commented 11 months ago

https://www.isf.cs.tu-bs.de/cms/team/thuem/papers/2019-SEFM-Bittner.pdf Also, relevant for both types of cardinality.

felixrieg commented 10 months ago

Feature cardinality

include
    Boolean
features
    A
        optional
            B // cardinality [2..5] 
                optional   
                    B_1
                    B_2
                    B_3
                    B_4
                    B_5

constraints
    B => B_1 & B_2 | B_1 & B_2 | B_1 & B_3 | B_1 & B_4 | B_1 & B_5 | B_2 & B_5 ...