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 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 |
Property | D_SBL1 |
---|
Formal | : | ( ( moveUp ( moveDown moveStop ) )
( moveDown ( moveUp moveStop ) ) ( moveStop ( moveUp moveDown ) ) ) |
NL | : | The blind lifter is always in exactly one of the three possible states moveUp, moveDown, moveStop. |
Property | D_SBL2 |
---|
Formal | : | ( ( rotateIncrease ( rotateDecrease rotateStop ) )
( rotateDecrease ( rotateIncrease rotateStop ) ) ( rotateStop ( rotateIncrease rotateDecrease ) ) ) |
NL | : | The blind rotator is always in exactly one of the three possible states rotateIncrease, rotateDecrease, rotateStop. |
Property | D_SBL3 |
---|
Formal | : | ( moveDown rotateStatus = 0 ) |
NL | : | If the blinds are moved down the rotating state, i.e. the angle of the blades is 0 degree. |
Property | D_SBL4 |
---|
Formal | : | ( moveUp rotateStatus = 180 ) |
NL | : | If the blinds are moved up the rotating state, i.e. the angle of the blades is 180 degrees. |
Property | D_SBL5 |
---|
Formal | : | ( blind. noMalAct. envEntity = STOP moveStop rotateStop ) |
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 |
---|
Formal | : | ( ( ( blind. noMalAct. envEntity = FORWARD )
( rotateStatus = 180 ) upperEndContact. noMalSens. envEntity = 0 ) ( moveUp rotateStop ) ) |
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 |
---|
Formal | : | ( ( ( blind. noMalAct. envEntity = BACKWARD )
( rotateStatus = 0 ) lowerEndContact. noMalSens. envEntity = 0 ) ( moveDown rotateStop ) ) |
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 |
---|
Formal | : | ( ( ( blind. noMalAct. envEntity = FORWARD )
( rotateStatus = 180 ) ) ( moveStop rotateIncrease ) ) |
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 |
---|
Formal | : | ( ( ( blind. noMalAct. envEntity = BACKWARD )
( rotateStatus = 0 ) ) ( moveStop rotateDecrease ) ) |
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 |
---|
Formal | : | ( ( Tmal ( blind. noMalAct. adjustedEntity = FORWARD
lowerEndContact. noMalSens. convertedEntity = 1 ) ) blind. automaticDetMal lowerEndContact. automaticDetMal ) |
NL | : | Whenever the machine has set the actuator to FORWARD, i.e. to move up, for at least 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 |
---|
Formal | : | ( ( Tmal ( blind. noMalAct. adjustedEntity = BACKWARD
upperEndContact. noMalSens. convertedEntity = 1 ) ) blind. automaticDetMal upperEndContact. automaticDetMal ) |
NL | : | Whenever the machine has set the actuator to BACKWARD, i.e. to move down, for at least time units, and the upperEndContact constantly signals for this time that the blind is still at the upper end, something is wrong. |