From 31235eff70c29b2235dcc6c0fc57e55d22a032d6 Mon Sep 17 00:00:00 2001 From: Andreas Bayha <bayha@fortiss.org> Date: Thu, 3 Aug 2023 13:27:54 +0200 Subject: [PATCH] YELLOW Issue-ref: 4240 Issue-URL: https://git.fortiss.org/af3/af3/-/issues/4240 Signed-off-by: Andreas Bayha <bayha@fortiss.org> --- .../org/fortiss/variability/analysis/.ratings | 2 +- .../analysis/EMFProductLineTranslation.java | 106 +++++++++--------- 2 files changed, 53 insertions(+), 55 deletions(-) diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/.ratings b/org.fortiss.variability/src/org/fortiss/variability/analysis/.ratings index 8bc8602bd..cdb6b56d7 100644 --- a/org.fortiss.variability/src/org/fortiss/variability/analysis/.ratings +++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/.ratings @@ -1,6 +1,6 @@ BucketSetMap.java 665a28c80a9693b9b9e31b7ebe59f2de4195d56c YELLOW DualKeyMap.java 75fbe85a54e5a655aaf67108ae004f98ed2879d8 YELLOW -EMFProductLineTranslation.java a9f4daf255db599cef1a0fe894f702d88b008cc0 YELLOW +EMFProductLineTranslation.java 58487bc6e6f31115ff5388fcc204dd55a545f106 YELLOW GenericProductLineAnalysis.java 6f6d48544ec2b872fa0a4f747a85657889ad463e YELLOW IProductLineConstraint.java 1b0e1231cc578a6e7e544441ac33533b4feafeb1 YELLOW IProductLineTranslation.java 733dae03e2baae237b6f0b33f0dd618a4f47cf73 YELLOW diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java index a9f4daf25..58487bc6e 100644 --- a/org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java +++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java @@ -68,16 +68,29 @@ public class EMFProductLineTranslation implements IProductLineTranslation { /** Prefix to be displayed as prefix to all logging messages from the translation. */ private static final String LOG_PREFIX = "[EMF product-line translation]: "; + /* Configuration related fields */ + + /** Flag that specifies whether the optimization to only translate optional parts is enabled. */ + private boolean isIslandOptimizationEnabled = false; + + /** + * The number of non-variable elements that are connected to a variable element to be translated + * in case the "island optimization" is enabled. + */ + private int islandOptimizationStepNum = 0; + + /** The set to specify all {@link EClass} to be translated by this translation. */ + private Set<EClass> translatedClasses; + /** The set to specify all {@link EReference} to be translated by this translation. */ + private Set<EReference> translatedReferences; + /** The set to specify all {@link EAttribute} to be translated by this translation. */ + private Set<EAttribute> translatedAttributes; + + /* Solver related fields */ + /** {@link Context} to capture the translated model. */ private Context ctx; - /** Z3 sort for base type integer. */ - private IntSort intSort; - /** Z3 sort for base type string. */ - private SeqSort<?> stringSort; - /** Z3 sort for base type boolean. */ - private BoolSort boolSort; - /** List of all translated assertions for the model. */ private List<BoolExpr> modelAssertions; /** List of all assertions for the feature model. */ @@ -87,6 +100,15 @@ public class EMFProductLineTranslation implements IProductLineTranslation { /** List of all assertions which encode the constraints. */ private List<BoolExpr> constraintAssertions; + /* Meta-model related fields */ + + /** Z3 sort for base type integer. */ + private IntSort intSort; + /** Z3 sort for base type string. */ + private SeqSort<?> stringSort; + /** Z3 sort for base type boolean. */ + private BoolSort boolSort; + /** Mapping of EDataTypes (e.g. EInt) to their translated Z3 type. */ private Map<EDataType, Sort> eDataType2Sort; /** Mapping for classes to their respective Z3 type. */ @@ -99,6 +121,13 @@ public class EMFProductLineTranslation implements IProductLineTranslation { /** Mapping of enumerations to their respective z3 expression for 'null' */ private Map<EEnum, Expr<?>> eEnum2NullElement; + /** + * The mapping of translated {@link EReference}s to the type that will be used for translation. + * This type might be different from the references original type in case only a subtype is + * specified for translation. + */ + private Map<EReference, EClass> reference2TranslatedEClass; + /** Mapping of attributes to their translated Z3 function. */ private DualKeyMap<EAttribute, EClass, FuncDecl<?>> eAttribute2FunDecl = new DualKeyMap<EAttribute, EClass, FuncDecl<?>>(); @@ -106,6 +135,8 @@ public class EMFProductLineTranslation implements IProductLineTranslation { private DualKeyMap<EReference, EClass, FuncDecl<?>> eReference2FunDecl = new DualKeyMap<EReference, EClass, FuncDecl<?>>(); + /* Model related fields */ + /** * Mapping of objects with types to their translated Z3 expressions. The second key EClass is * necessary as an object is translated for all classes specified in 'translatedClasses'). @@ -113,19 +144,20 @@ public class EMFProductLineTranslation implements IProductLineTranslation { private DualKeyMap<EObject, EClass, Expr<?>> eObject2z3Expr = new DualKeyMap<EObject, EClass, Expr<?>>(); - /** Mapping of classes to the selection function for this type. */ - private Map<EClass, FuncDecl<?>> eClass2SelectionFunction; - - /** The set to specify all {@link EClass} to be translated by this translation. */ - private Set<EClass> translatedClasses; - /** The set to specify all {@link EReference} to be translated by this translation. */ - private Set<EReference> translatedReferences; - /** The set to specify all {@link EAttribute} to be translated by this translation. */ - private Set<EAttribute> translatedAttributes; + /** + * The mapping from Z3 {@link Expr} back to the respective {@link EObject} to be used for + * interpreting solver results. + */ + private Map<Expr<?>, EObject> expr2EObject = new HashMap<Expr<?>, EObject>(); /** The mapping of translated {@link EClass} to the objects that have been collected. */ private BucketSetMap<EClass, EObject> class2TranslatedEObjects; + /* Variability related fields */ + + /** Mapping of classes to the selection function for this type. */ + private Map<EClass, FuncDecl<?>> eClass2SelectionFunction; + /** The {@link AbstractFeatureModel} collected by this translation */ private AbstractFeatureModel featureModel; /** Mapping of features to corresponding Z3 {@link BoolExpr}. */ @@ -134,28 +166,6 @@ public class EMFProductLineTranslation implements IProductLineTranslation { /** The mapping of translated {@link EObject}s to global {@link PresenceCondition}s. */ private Map<EObject, PresenceConditionTerm> object2presenceCondition; - /** - * The mapping from Z3 {@link Expr} back to the respective {@link EObject} to be used for - * interpreting solver results. - */ - private Map<Expr<?>, EObject> expr2EObject = new HashMap<Expr<?>, EObject>(); - - /** - * The mapping of translated {@link EReference}s to the type that will be used for translation. - * This type might be different from the references original type in case only a subtype is - * specified for translation. - */ - private Map<EReference, EClass> reference2TranslatedEClass; - - /** Flag that specifies whether the optimization to only translate optional parts is enabled. */ - private boolean isIslandOptimizationEnabled = false; - - /** - * The number of non-variable elements that are connected to a variable element to be translated - * in case the "island optimization" is enabled. - */ - private int islandOptimizationStepNum = 0; - /** * Constructor. */ @@ -226,9 +236,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation { translatePresenceConditions(); } - /** - * - */ + /** Check and determine which types can be used to encode the translated relations. */ private void collectReferenceTypes() { for(EReference ref : translatedReferences) { EClass refType = ref.getEReferenceType(); @@ -264,10 +272,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation { } } - /** - * @param model - * @param parentCondition - */ + /** Recursively collect all objects which shall be translated. */ private void collectTranslatedObjects(EObject model, PresenceConditionTerm parentCondition) { if(model instanceof AbstractFeatureModel) { featureModel = (AbstractFeatureModel)model; @@ -299,11 +304,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation { } } - /** - * @param eo - * @param cls - * @param pc - */ + /** Collect one EObject to be translated. */ private void collectEObject(EObject eo, EClass cls, PresenceConditionTerm pc) { class2TranslatedEObjects.add(cls, eo); @@ -314,10 +315,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation { object2presenceCondition.put(eo, pc); } - /** - * @param model - * @param remainingSteps - */ + /** Collect all references which shall be translated for the "island optimization". */ private void collectTranslatedReferences(EObject model, int remainingSteps) { if(remainingSteps <= 0) { return; -- GitLab