Description Class TempOperationModeSet

INTENTION

This class provides all the definitions to describe all operation modes concerning the temperature control of a room. Note that for each room there is a specific set of operation modes.

Four operation modes are distinguished: NonFreezeMode, ComfortMode, StandbyMode, and OffMode. The definitions of these modes are given in this class. Which mode is currently active depends on three predicates: expectedUsage, occUsed, and nonFreezeTime. Based on the currently active mode the desired room temperature is determined.

SIGNATURE

Object	OffMode  :  TempOperationMode

Intention

:

This object represents the operation mode offMode.

Object	StandbyMode  :  TempOperationMode

Intention

:

This object represents the operation mode StandbyMode.

Object	ComfortMode  :  TempOperationMode

Intention

:

This object represents the operation mode ComfortMode.

Object	NonFreezeMode  :  TempOperationMode

Intention

:

This object represents the operation mode NonFreezeMode.

Object	expUse  :  ExpectedUsage

Intention

:

This object represents the part of the definition of the operation modes defining whether a usage of a room is expected or not.

Object	occ  :  Occupancy

Intention

:

This object represents the part of the definition of the operation modes defining whether a room is occupied or not.

Timed Function	roomDesiredTemperature   TEMP

Intention	:	This function represents the currently desired temperature that should be established in a room.
Scope	:	mh

Timed Predicate	nonFreezeTime

Intention	:	This predicate is true iff it is currently non-freeze operation time.
Scope	:	mh

MACHINE SPECIFICATIONS

Property	M_TOMS1

Formal	:	(  OffMode. active          nonFreezeTime  expUse. expectedUsage  occ. occUsed )
NL	:	The operation mode OffMode is active in a room iff the following conditions are fulfilled together: currently it is not non-freeze operation time, no usage of the room is expected, and the room is not occupied.

Property	M_TOMS2

Formal	:	(  StandbyMode. active          nonFreezeTime  expUse. expectedUsage  occ. occUsed )
NL	:	The operation mode StandbyMode is active in a room iff the following conditions are fulfilled together: currently it is not non-freeze operation time, usage of the room is expected, and the room is not occupied.

Property	M_TOMS3

Formal	:	(  ComfortMode. active  nonFreezeTime  occ. occUsed )
NL	:	The operation mode ComfortMode is active in a room iff the following conditions are fulfilled together: currently it is not non-freeze operation time and the room is occupied.

Property	M_TOMS4

Formal	:	(  NonFreezeMode. active  nonFreezeTime )
NL	:	The operation mode NonFreezeMode is active in a room iff currently it is non-freeze operation time.

Property	M_TOMS5

Formal	:	(  OffMode. active            roomDesiredTemperature =  OffMode. desiredTemperature )
NL	:	Whenever the operation mode OffMode is active the desired temperature of the room is the temperature that should be established in the operation mode OffMode.

Property	M_TOMS6

Formal	:	(  StandbyMode. active                                 roomDesiredTemperature =                                           StandbyMode. desiredTemperature )
NL	:	Whenever the operation mode StandbyMode is active the desired temperature of the room is the temperature that should be established in the operation mode StandbyMode.

Property	M_TOMS7

Formal	:	(  ComfortMode. active                                 roomDesiredTemperature =                                           ComfortMode. desiredTemperature )
NL	:	Whenever the operation mode ComfortMode is active the desired temperature of the room is the temperature that should be established in the operation mode ComfortMode.

Property	M_TOMS8

Formal	:	(  NonFreezeMode. active                                 roomDesiredTemperature =                                           NonFreezeMode. desiredTemperature )
NL	:	Whenever the operation mode NonFreezeMode is active the desired temperature of the room is the temperature that should be established in the operation mode NonFreezeode.