The SPL consists of three parts:

The feature model F of W allows for three optional features to be added to a basic washing machine: Heat adds the ability to have hot water washes, Dry adds an automatic dry following the wash, and Delay adds the ability to delay the start time of the wash. Note that the heated wash and delayed wash features are mutually exclusive while drying can be added independently. The Excludes constraint between Heat and Delay in the feature model indicates that at most one of these can be selected. A set of features that form a valid combination is called a configuration.

The domain model D of W is a state-machine which specifies that after initiating and locking the washer, a basic wash begins or a pre-washing waiting period is initiated, either for heating the water or for a delayed wash. Then the washing takes place, followed, optionally, by drying. Finally,if drying or heating was used, the clothes are cooled and the washer is unlocked, terminating the process.

Depending on which of the features have been selected for a particular washing machine product, only some parts of this state machine controller will be available. The propositional formulas in boxes throughout the controller state machine indicate the presence conditions C for different model elements, i.e., the configurations of features under which the element is present in a product. For example, the transition startPrewash from state Locking to state Waiting is only present if the feature Heat or the feature Delay is selected. Creating a particular washing machine product from W is called configuring the SPL.

Tasks:

1. Encode the feature model F of W in propositional logic using Z3. o Hint: you can omit the default feature Wash

2. Prove that your encoding forbids configurations that violate the mutual exclusion constraint between Delay and Heat.

3. Encode the domain model D of W in propositional logic using Z3. Treat Entry/TempCheck() as a single model element.

o Hint 1: each model element should be represented by a propositional variable meaning the element is present.

o Hint 2: an edge can only be present in the model if both its endpoints are also present in the model.

o Hint 3: a contained element can only be present in the model if its container is also present. o Hint 4: dont bother with encoding the meta-model and the typing of model elements.

4. Encode the set of presence conditions C of W. o Hint: a presence condition is merely a constraint between feature and model element variables o Hint: you can omit the default feature Wash

5. Combine F, D, C, and verify that your encoding of W is satisfiable.

6. Using Z3, check whether the following model can be generated by configuring W or not.

Software Product Lines (SPLs) are a methodology for modelling and managing families of related software products that are similar but have slight variations. Consider this example of an SPL W of washing machine controllers: startPrewash dDelay Locking Waiting Heatv Delay cludes staktWash endPrewash Wash Heat Washing Entry/TempCheck() Dry Feature Model endW startDrying UnlockingK Dry Drying Dry Domain Model The SPL consists of three parts startPrewash Locking Waiting endPrewash stactWash Washing endWasti startDrying Drying Unlocking Is this a valid product? Software Product Lines (SPLs) are a methodology for modelling and managing families of related software products that are similar but have slight variations. Consider this example of an SPL W of washing machine controllers: startPrewash dDelay Locking Waiting Heatv Delay cludes staktWash endPrewash Wash Heat Washing Entry/TempCheck() Dry Feature Model endW startDrying UnlockingK Dry Drying Dry Domain Model The SPL consists of three parts startPrewash Locking Waiting endPrewash stactWash Washing endWasti startDrying Drying Unlocking Is this a valid product