Skip to content
Snippets Groups Projects
Commit 31235eff authored by Andreas Bayha's avatar Andreas Bayha
Browse files

YELLOW

Issue-ref: 4240
Issue-URL: af3#4240



Signed-off-by: default avatarAndreas Bayha <bayha@fortiss.org>
parent 988e02b7
No related branches found
No related tags found
1 merge request!1784240
Pipeline #38684 passed
Pipeline: maven-releng

#38685

    BucketSetMap.java 665a28c80a9693b9b9e31b7ebe59f2de4195d56c YELLOW BucketSetMap.java 665a28c80a9693b9b9e31b7ebe59f2de4195d56c YELLOW
    DualKeyMap.java 75fbe85a54e5a655aaf67108ae004f98ed2879d8 YELLOW DualKeyMap.java 75fbe85a54e5a655aaf67108ae004f98ed2879d8 YELLOW
    EMFProductLineTranslation.java a9f4daf255db599cef1a0fe894f702d88b008cc0 YELLOW EMFProductLineTranslation.java 58487bc6e6f31115ff5388fcc204dd55a545f106 YELLOW
    GenericProductLineAnalysis.java 6f6d48544ec2b872fa0a4f747a85657889ad463e YELLOW GenericProductLineAnalysis.java 6f6d48544ec2b872fa0a4f747a85657889ad463e YELLOW
    IProductLineConstraint.java 1b0e1231cc578a6e7e544441ac33533b4feafeb1 YELLOW IProductLineConstraint.java 1b0e1231cc578a6e7e544441ac33533b4feafeb1 YELLOW
    IProductLineTranslation.java 733dae03e2baae237b6f0b33f0dd618a4f47cf73 YELLOW IProductLineTranslation.java 733dae03e2baae237b6f0b33f0dd618a4f47cf73 YELLOW
    ......
    ...@@ -68,16 +68,29 @@ public class EMFProductLineTranslation implements IProductLineTranslation { ...@@ -68,16 +68,29 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
    /** Prefix to be displayed as prefix to all logging messages from the translation. */ /** Prefix to be displayed as prefix to all logging messages from the translation. */
    private static final String LOG_PREFIX = "[EMF product-line 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. */ /** {@link Context} to capture the translated model. */
    private Context ctx; 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. */ /** List of all translated assertions for the model. */
    private List<BoolExpr> modelAssertions; private List<BoolExpr> modelAssertions;
    /** List of all assertions for the feature model. */ /** List of all assertions for the feature model. */
    ...@@ -87,6 +100,15 @@ public class EMFProductLineTranslation implements IProductLineTranslation { ...@@ -87,6 +100,15 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
    /** List of all assertions which encode the constraints. */ /** List of all assertions which encode the constraints. */
    private List<BoolExpr> constraintAssertions; 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. */ /** Mapping of EDataTypes (e.g. EInt) to their translated Z3 type. */
    private Map<EDataType, Sort> eDataType2Sort; private Map<EDataType, Sort> eDataType2Sort;
    /** Mapping for classes to their respective Z3 type. */ /** Mapping for classes to their respective Z3 type. */
    ...@@ -99,6 +121,13 @@ public class EMFProductLineTranslation implements IProductLineTranslation { ...@@ -99,6 +121,13 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
    /** Mapping of enumerations to their respective z3 expression for 'null' */ /** Mapping of enumerations to their respective z3 expression for 'null' */
    private Map<EEnum, Expr<?>> eEnum2NullElement; 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. */ /** Mapping of attributes to their translated Z3 function. */
    private DualKeyMap<EAttribute, EClass, FuncDecl<?>> eAttribute2FunDecl = private DualKeyMap<EAttribute, EClass, FuncDecl<?>> eAttribute2FunDecl =
    new DualKeyMap<EAttribute, EClass, FuncDecl<?>>(); new DualKeyMap<EAttribute, EClass, FuncDecl<?>>();
    ...@@ -106,6 +135,8 @@ public class EMFProductLineTranslation implements IProductLineTranslation { ...@@ -106,6 +135,8 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
    private DualKeyMap<EReference, EClass, FuncDecl<?>> eReference2FunDecl = private DualKeyMap<EReference, EClass, FuncDecl<?>> eReference2FunDecl =
    new DualKeyMap<EReference, EClass, FuncDecl<?>>(); new DualKeyMap<EReference, EClass, FuncDecl<?>>();
    /* Model related fields */
    /** /**
    * Mapping of objects with types to their translated Z3 expressions. The second key EClass is * 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'). * necessary as an object is translated for all classes specified in 'translatedClasses').
    ...@@ -113,19 +144,20 @@ public class EMFProductLineTranslation implements IProductLineTranslation { ...@@ -113,19 +144,20 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
    private DualKeyMap<EObject, EClass, Expr<?>> eObject2z3Expr = private DualKeyMap<EObject, EClass, Expr<?>> eObject2z3Expr =
    new DualKeyMap<EObject, EClass, Expr<?>>(); new DualKeyMap<EObject, EClass, Expr<?>>();
    /** Mapping of classes to the selection function for this type. */ /**
    private Map<EClass, FuncDecl<?>> eClass2SelectionFunction; * The mapping from Z3 {@link Expr} back to the respective {@link EObject} to be used for
    * interpreting solver results.
    /** The set to specify all {@link EClass} to be translated by this translation. */ */
    private Set<EClass> translatedClasses; private Map<Expr<?>, EObject> expr2EObject = new HashMap<Expr<?>, EObject>();
    /** 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 of translated {@link EClass} to the objects that have been collected. */ /** The mapping of translated {@link EClass} to the objects that have been collected. */
    private BucketSetMap<EClass, EObject> class2TranslatedEObjects; 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 */ /** The {@link AbstractFeatureModel} collected by this translation */
    private AbstractFeatureModel featureModel; private AbstractFeatureModel featureModel;
    /** Mapping of features to corresponding Z3 {@link BoolExpr}. */ /** Mapping of features to corresponding Z3 {@link BoolExpr}. */
    ...@@ -134,28 +166,6 @@ public class EMFProductLineTranslation implements IProductLineTranslation { ...@@ -134,28 +166,6 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
    /** The mapping of translated {@link EObject}s to global {@link PresenceCondition}s. */ /** The mapping of translated {@link EObject}s to global {@link PresenceCondition}s. */
    private Map<EObject, PresenceConditionTerm> object2presenceCondition; 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. * Constructor.
    */ */
    ...@@ -226,9 +236,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation { ...@@ -226,9 +236,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
    translatePresenceConditions(); translatePresenceConditions();
    } }
    /** /** Check and determine which types can be used to encode the translated relations. */
    *
    */
    private void collectReferenceTypes() { private void collectReferenceTypes() {
    for(EReference ref : translatedReferences) { for(EReference ref : translatedReferences) {
    EClass refType = ref.getEReferenceType(); EClass refType = ref.getEReferenceType();
    ...@@ -264,10 +272,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation { ...@@ -264,10 +272,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
    } }
    } }
    /** /** Recursively collect all objects which shall be translated. */
    * @param model
    * @param parentCondition
    */
    private void collectTranslatedObjects(EObject model, PresenceConditionTerm parentCondition) { private void collectTranslatedObjects(EObject model, PresenceConditionTerm parentCondition) {
    if(model instanceof AbstractFeatureModel) { if(model instanceof AbstractFeatureModel) {
    featureModel = (AbstractFeatureModel)model; featureModel = (AbstractFeatureModel)model;
    ...@@ -299,11 +304,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation { ...@@ -299,11 +304,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
    } }
    } }
    /** /** Collect one EObject to be translated. */
    * @param eo
    * @param cls
    * @param pc
    */
    private void collectEObject(EObject eo, EClass cls, PresenceConditionTerm pc) { private void collectEObject(EObject eo, EClass cls, PresenceConditionTerm pc) {
    class2TranslatedEObjects.add(cls, eo); class2TranslatedEObjects.add(cls, eo);
    ...@@ -314,10 +315,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation { ...@@ -314,10 +315,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
    object2presenceCondition.put(eo, pc); object2presenceCondition.put(eo, pc);
    } }
    /** /** Collect all references which shall be translated for the "island optimization". */
    * @param model
    * @param remainingSteps
    */
    private void collectTranslatedReferences(EObject model, int remainingSteps) { private void collectTranslatedReferences(EObject model, int remainingSteps) {
    if(remainingSteps <= 0) { if(remainingSteps <= 0) {
    return; return;
    ......
    0% Loading or .
    You are about to add 0 people to the discussion. Proceed with caution.
    Finish editing this message first!
    Please register or to comment