---
title: Behavioral Modeling - Power Window
...

This example demonstrates modeling both structure and behavior with variability. 

# Feature modeling

We model features as final, that is, we do not allow dynamic reconfiguration.
Feature configuration from the first snapshot remains unchanged for the entire trace.

## Metamodel

```clafer
abstract final Feature
abstract final FeatureModel
```

## Model 

The optional feature `express` indicates the functionality of automatically closing the window.
The feature `pinchProtection` indicates the functionality of obstacle detection and stopping the window closure.

```clafer
WinFeatures : FeatureModel
    manualUpDown : Feature
    express : Feature ?
        pinchProtection : Feature ?
```

# Component and statemachine modeling

## Metamodel

Simple component modeling.

```clafer
abstract final Component
    abstract Port
abstract final Command
```

Inside the components, we will embed statemachines modeling their behavior.

```clafer
abstract State
abstract StateMachine
```

## Model 

Commands received by the window motor.

```clafer
motorUp : Command
motorStop : Command
motorDown : Command
```

Window motor

```clafer
WinMotor : Component
    cmd : Port -> Command
```

Requests from the user. 
Observe, that the request `expressUp` is optional.

```clafer
abstract final UserRequest
up : UserRequest
expressUp : UserRequest ?
stop : UserRequest
down : UserRequest
```

### Alphabet variability

The user request `expressUp` is only available when the feature `express` is present. 

```clafer
[ express <=> expressUp ]
```

Window controller with an optional component `pinchDetector`. 

```clafer
abstract WinController : Component
    final motor -> WinMotor
    pinchDetector : Component ?

    req : Port -> UserRequest ?
    endOfTravel : Port ?
    objectDetected : Port ?

    [ lone (req, endOfTravel, objectDetected )]

    final xor WinStates : StateMachine
        xor movingUp : State
            [ motor.cmd = motorUp ]
            [ req=down     --> movingDown ]
            [ endOfTravel  --> closed     ]
            [ req=up       --> movingUp ]
            initial basic : State
                [ req=stop      --> stopped   ]
                [ req=expressUp --> movingUpX ]
            movingUpX : State
                [ this -[objectDetected]-> stopped ]

        initial xor stopped : State
            [ motor.cmd = motorStop ]
            closed : State
                [ req=down --> movingDown ]
                [ (req=up || req=stop) --> closed ]
            partlyOpen : State
                [ req=up   --> movingUp   ]
                [ req=down --> movingDown ]
                [ req=stop --> partlyOpen ]
            open : State
                [ req=up   --> movingUp ]
                [ (req=down || req=stop) --> open ]

        movingDown : State
            [ motor.cmd = motorDown ]
            [ req=up       --> movingUp ]
            [ endOfTravel  --> open     ]
            [ req=stop     --> stopped  ]
            [ req=down     --> movingDown ]
```

### Linking the feature with the optional component (structural variability)

The component `pinchDetector` is only required if we support the feature `pinchProtection`.

```clafer
[ pinchProtection <=> pinchDetector ]
```

### Disabling `objectDetected` port

Without the feature `pinchProtection`, the port `objectDetected` should be inactive. 
Having the feature will allow receiving the signal `objectDetected`.

```clafer
[ no pinchProtection => no WinController.objectDetected ]
```

# Variability in behavior using inheritance

Two kinds of window controllers:
 
## With continuous chime 

```clafer
WinCtrWithContChime : WinController ?
    chime : Port ?
    [ movingUpX <=> chime ]
```

## With intermittent chime

```clafer
WinCtrWithChime : WinController ?
    chime : Port ?
    [ no movingUpX => no chime ]
    [ chime --> no chime ]
    [ no chime && movingUpX --> (movingUpX => chime) ]
```

# Variability in behavior using strategy pattern

We first define an abstract chiming strategy:
chiming can be `audible` but only if `active` (expressed by nesting).

```clafer
abstract ChimingStrategy
    active : State ?
        audible : State ?
```

Concrete strategies:

```clafer
NoChiming : ChimingStrategy
    [ not audible ]
```

```clafer
Continuous : ChimingStrategy
    [ active => audible ]
```

```clafer
Intermittent : ChimingStrategy
    [ audible --> not audible ]
    [ not audible --> (active => audible) ]
```

Now we can parameterize the controller with a chiming strategy.
Chiming should be active when moving up in express mode.
The chime should be emitted only when the chiming is audible.

```clafer
WinControllerStrategies : WinController ?
    chime : Port ?
    strategy -> ChimingStrategy
    [ strategy.active <=> movingUpX ]
    [ strategy.active.audible <=> chime ]
```

We can choose the chiming strategy using the following constraint:

```clafer
[ WinControllerStrategies.strategy = Intermittent ]
```

# Scenarios and properties

## An example positive scenario

```clafer
assert [ initially closed && req=down --> movingDown -->>
         req=expressUp --> movingUpX --> objectDetected --> stopped ]
```

## It must be possible to go from closed to open via partiallyOpen state

```clafer
assert [ sometime closed -->> partlyOpen -->> open ]
```

## It must be impossible for the user to request opening and the window remains closed

```clafer
assert [ never req = down --> closed ]
```

## It must be impossible for the window to be `closed` and continue sending `motorUp` command

It is a safety property to prevent burning the motor.

```clafer
assert [ never closed && cmd=motorUp ]
```

## The window must never continue `movingUp` after an object was detected

It is a safety property to prevent injury.

```clafer
assert [ never objectDetected --> movingUp ]
```