Description Class MalfunctionOccupancy

INTENTION

This class provides all definitions to describe the behavior of the system concerning the detection of occupancy in an area in the case that some sensors used to determine occupancy have a malfunction.

In the case of a malfunction of such a sensor, a value is determined depending on a possibly manually entered value by a user and an automatically generated value. If a value has been entered manually this value has priority over the automatically determined value.

Most of the entities introduced in this description class have to be specified in the description classes where they are used.

SIGNATURE

Object	manualEnteredOcc  :  EnteredValue(CHECKED_DOM  =  BINARY)

Intention	:	This object represents the value concerning occupancy entered manually by a user in the case of a malfunction of some sensors used to determine occupancy. 1 means occupancy, 0 means no occupancy. Note that the value of this object is only meaningful if the predicate stateManualEnteredOcc is true.
Postreferences	:	msref MalfunctionOccupancy : M_MO1

Timed Predicate	malOccDetEnv

Intention	:	This predicate is true iff some sensors existing in the real world used to determine occupancy have a malfunction. Note that this predicate represents the value as it exists in the real world. This value is not visible for the machine.
Scope	:	eh

Timed Predicate	malOccDetMach

Intention	:	This predicate is true iff the machine assumes that some sensors used to determine occupancy have a malfunction. Note that this predicate represents the value as it seen by the machine.
Scope	:	mh
Postreferences	:	msref Occupancy : M_OCC1
		msref Occupancy : M_OCC2

Timed Predicate	stateManualEnteredOcc

Intention	:	This predicate is true iff it has been entered manually whether there is occupancy or not.
Scope	:	mh
Postreferences	:	msref MalfunctionOccupancy : I_MO1
		msref MalfunctionOccupancy : M_MO1

Timed Predicate	automaticDetermValue

Intention	:	This predicate represents the occupancy determined automatically by the machine in the case of a malfunction of the sensors used to determine occupancy. If this predicate is true this means occupancy. If it is false this means no occupancy.
Scope	:	mh
Postreferences	:	msref MalfunctionOccupancy : M_MO1
		msref AreaLight : M_AL6

Timed Predicate	occMal

Intention	:	This predicate represents the occupancy used by the machine in the case of a malfunction of the sensors used to determine occupancy. If this predicate is true this means occupancy. If it is false this means no occupancy.
Scope	:	mh
Postreferences	:	msref MalfunctionOccupancy : M_MO1
		msref Occupancy : M_OCC2

MACHINE SPECIFICATIONS

Property	I_MO1

Formal	:	stateManualEnteredOcc
NL	:	Initially no value for occupancy in the case of a malfunction is entered manually.

Property	M_MO1

Formal	:	(  stateManualEnteredOcc                      (  occMal  manualEnteredOcc. checked = 1 )                                (  stateManualEnteredOcc                      (  occMal  automaticDetermValue ) ) )
NL	:	If a value for the status of occupancy has been entered manually this is the value used for occupancy in the case of a malfunction of some sensors used to determine occupancy. Otherwise, the value used for occupancy in the case of a malfunction of the sensors used to determine occupancy corresponds with the value determined automatically.