Description Class SunBlind

INTENTION

This class provides all definitions to describe a sun blind. A sun blind combines a sun blind lifter and a blind rotator. Both, lifter and rotator, are controlled using the same three point actuator. Additionally, a sun blind contains two sensors recognizing whether the blind has reached the upper or lower end.

To model the lifting of the blind and the rotating of the blind blades several states are introduced: moveUp, moveDown, moveStop, rotateStatus, rotateIncrease, rotateDecrease, and rotateStop.

DOMAIN KNOWLEDGE

Property	D_SBL1

NL

:

The blind lifter is always in exactly one of the three possible states moveUp, moveDown, moveStop.

Property	D_SBL2

NL

:

The blind rotator is always in exactly one of the three possible states rotateIncrease, rotateDecrease, rotateStop.

Property	D_SBL3

NL

:

If the blinds are moved down the rotating state, i.e. the angle of the blades is 0 degree.

Property	D_SBL4

NL

:

If the blinds are moved up the rotating state, i.e. the angle of the blades is 180 degrees.

Property	D_SBL5

NL

:

Whenever the status of the sun blind is set to stop, the blind is neither lifted in any direction nor are the blades rotated in any direction.

Property	D_SBL6

NL

:

Whenever the status of the sun blind is set to FORWARD and the rotating state of the blades, i.e. the angle, is 180 degrees and the blind is not at the upper end, the blind is lifted up and the blades are not rotating.

Property	D_SBL7

NL

:

Whenever the status of the sun blind is set to BACKWARD and the rotating state of the blades, i.e. the angle, is 0 degrees and the blind is not at the lower end, the blind is lifted down and the blades are not rotating.

Property	D_SBL8

NL

:

Whenever the status of the sun blind is set to FORWARD and the rotating state of the blades, i.e. the angle, is not 180 degrees the blind is not lifted up or down in any direction but rotated in the direction of 180 degrees.

Property	D_SBL9

NL

:

Whenever the status of the sun blind is set to BACKWARD and the rotating state of the blades, i.e. the angle, is not 0 degree the blind is not lifted up or down in any direction but rotated in the direction of 0 degrees.

Property	D_SBL10

NonFormal

:

If the rotating angle of the blind blades is x degrees light can enter from an angle of x degrees from vertical.

MACHINE SPECIFICATIONS

Property	M_SBL1

NL

:

Whenever the machine has set the actuator to FORWARD, i.e. to move up, for at least $T_{\mathit{mal}}$ time units, and the lowerEndContact constantly signals for this time that the blind is still at the lower end, something is wrong.

Property	M_SBL2

NL

:

Whenever the machine has set the actuator to BACKWARD, i.e. to move down, for at least $T_{\mathit{mal}}$ time units, and the upperEndContact constantly signals for this time that the blind is still at the upper end, something is wrong.