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.

SIGNATURE

Domain	DEGREE  = { 0 180 } NAT

Intention

:

This domain contains the possible values of the blind rotator, namely 0 to 180 degrees.

Object	blind  :  ThreePointActuator

Intention

:

This object represents the actuator by which the blind can be lifted and rotated.

Object	upperEndContact  :  BinarySensor

Intention

:

This object represents the end contact detecting whether the blind is lifted completely up or not.

Object	lowerEndContact  :  BinarySensor

Intention

:

This object represents the end contact detecting whether the blind is lifted completely down or not.

Time Constant	Tmal

Intention	:	This time constant is used to detect automatically a malfunction of a sun blind. See property $P\_SBL_{1}$ for details.
Scope	:	ev

Timed Function	rotateStatus   DEGREE

Intention	:	This function represents the current state of the blind rotator, i.e. the current position of the blind blades.
Scope	:	eh

Timed Predicate	moveUp

Intention	:	This predicate is true iff the blind is moving up.
Scope	:	eh

Timed Predicate	moveDown

Intention	:	This predicate is true iff the blind is moving down.
Scope	:	eh

Timed Predicate	moveStop

Intention	:	This predicate is true iff the blind stops, i.e. it is neither moving down nor up.
Scope	:	eh

Timed Predicate	rotateIncrease

Intention	:	This predicate is true iff the blind blades are rotated in the direction of 0 degree.
Scope	:	eh

Timed Predicate	rotateDecrease

Intention	:	This predicate is true iff the blind blades are rotated in the direction of 180 degree.
Scope	:	eh

Timed Predicate	rotateStop

Intention	:	This predicate is true iff the blind blades do not rotate in any direction. Note that this does not implies that the current rotating angle of the blades is 0 or 180 degrees.
Scope	:	eh

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.