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

This example demonstrates modeling both structure and behaviour 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 detecting obstacles and stopping the window.

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

# Component and statemachine modeling

## Metamodel

Simple component modeling.
Nesting the `Port` under `Component` ensures that all ports are always children of components.
The components are final because we do not allow dynamic reconfiguration; 
however, the ports are not final: 
a port instance can appear to point to a value, disappear, and a new instance can appear to point to a different value.

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

Inside the components, we will embed statemachines modeling their behavior.
The states are not final because we want to allow state changes.

```clafer
abstract State
abstract final StateMachine
```

## Model 

Commands received by the window motor.

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

Window motor. 
The port `cmd` is mandatory, meaning that the motor must always be given a command.

```clafer
abstract 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
```

The user request `expressUp` is only available when the feature `express` is present (alphabet variability). 

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

The component `pinchDetector` of the `WinController` is only required if the feature `pinchProtection` is present.

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

Instances of the ports `endOfTravel` and `objectDetected` appear when the corresponding binary signal is received.
On the other hand, instances of the port `req` point to a specific user request. 
No instance of the port `req` indicates no user request.
Finally, we allow at most one of `req`, `endOfTravel`, and `objectDetected` in order to remove non-determinism.

```clafer
abstract WinController : Component
    motor : WinMotor
    pinchDetector : Component ?

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

    [ lone (req, endOfTravel, objectDetected )]
    [ always req=stop between req=down and req=up]
    [ always req=stop between req=up and req=down]
    [ always req=up between req=stop and req=expressUp ]
    [ always req=expressUp => next no req]

    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 ]
```

We model state actions by fixing the motor command. 
E.g., in state `movingDown`, motor command is fixed to `motorDown`.

State transitions are modeled using "next transitions": `-->`.
In the state `movingUpX` we demonstrate "guarded next transition": `-[objectDetected]->`.

### 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 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 behaviour 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 parametrize 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

For each case, we define a concrete WinController and state the assertion. 

## An example positive scenario

```clafer
wc1 : WinController
assert [ initially wc1.WinStates.stopped.closed && wc1.req=down --> wc1.WinStates.movingDown -->>
         wc1.req=expressUp --> wc1.WinStates.movingUp.movingUpX --> wc1.objectDetected --> wc1.WinStates.stopped ]
```

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

```clafer
wc2 : WinController
assert [ sometime wc2.WinStates.stopped.closed -->> wc2.WinStates.stopped.partlyOpen -->> wc2.WinStates.stopped.open ]
```

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

```clafer
wc3 : WinController
assert [ never wc3.req = down --> wc3.WinStates.stopped.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
wc4 : WinController
assert [ never wc4.WinStates.stopped.closed && wc4.motor.cmd=motorUp ]
```

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

It is a safety property to prevent injury.

```clafer
wc5 : WinController
assert [ never wc5.objectDetected --> wc5.WinStates.movingUp ]
```