Description Class Room

INTENTION

This class extends the description class BasicRoom with the definitions concerning those objects of which in each room at least one instantiation is installed but where the concrete number of instantion can vary from room to room.

In addition to the objects introduced in description class BasicRoom each room is equipped with

• numRad many radiators
• numDoorHallway many doors to the hallway

FORMAL PARAMETERS

Function	numRad  NAT

Intention

:

This parameter represents the number of radiators that belong to a room.

Function	numDoorHallway  NAT

Intention

:

This parameter represents the number of doors of a room to the hallway.

BASE CLASSES

Class	BasicRoom

Intention

:

All definitions of description class BasicRoom are also provided here.

SIGNATURE

Object	rad  :  Radiator[ numRad]

Intention

:

Each object represents one radiator of a room.

Object	hallwayDoor  :  Door[ numDoorHallway]

Intention

:

Each object represents one door of a room to the hallway.

Timed Function	tempRadSet   THREE_PT_ACT_RANGE

Intention	:	This function represents the current setting of the radiators in a room intended by the temperature control.
Scope	:	mh

Timed Function	tempRadNoMalSet  :  TEMP  THREE_PT_ACT_RANGE

Intention	:	This function represents the current setting of the radiators in a room intended by the temperature control if the machine assumes that there is no malfunction of the sensors needed to determine this setting. This setting depends (at least) on the current desired room temperature (first argument).
Scope	:	mh

Timed Function	tempRadMalSet  :  TEMP  THREE_PT_ACT_RANGE

Intention	:	This function represents the current setting of the radiators in a room intended by the temperature control if the machine assumes that there is a malfunction of the sensors needed to determine this setting. This setting depends (at least) on the current desired room temperature (first argument). Further arguments can be the current outdoor temperature and the settings of the neighbour rooms.
Scope	:	mh

Timed Predicate	malTemp

Intention	:	This predicate is true iff the machine assumes that the sensors, used to determine the settings of the actuators controlling the temperature, have such a serious malfunction that the settings of the actuators have to be determined using makeshift operations.
Scope	:	mh

REQUIREMENT SPECIFICATIONS

Property	R_R1

NonFormal

:

The desired temperature shall be reached as fast as possible during the heating up state. This requirement is a basis for the definition of the functions tempRadNoMalSet and tempRadMalSet.

Property	R_R2

NonFormal

:

The currently desired temperature is maintained during the current temperature state as good as possible. This requirement is a basis for the definition of the functions tempRadNoMalSet and tempRadMalSet.

MACHINE SPECIFICATIONS

Property	I_R1

Formal	:	malTemp
NL	:	Initially the machine does not assume that the sensors, used to determine the settings of the actuators controlling the temperature, have such a serious malfunction that the settings of the actuators have to be determined using makeshift operations.

Property	M_R1

Formal	:	(  malTemp  malfunctionAllTempSens )
NL	:	The machine assumes that the sensors, used to determine the settings of the actuators controlling the temperature, have such a serious malfunction that the settings of the actuators have to be determined using makeshift operations iff all temperature sensors of a room have a malfunction.

Property	M_R2

Formal	:	( (  malTemp             tempRadSet =                  tempRadNoMalSet( RT. modes. roomDesiredTemperature) )       (  malTemp             tempRadSet =                  tempRadMalSet( RT. modes. roomDesiredTemperature) ) )
NL	:	If the machine does not assume a serious malfunction of the sensors, used to determine the settings of the actuators controlling the temperature, the current setting of the radiators in a room intended by the temperature control are as determined by the function tempRadNoMalSet. If the machine assumes a serious malfunction of the sensors, used to determine the settings of the actuators controlling the temperature, the current setting of the radiators in a room intended by the temperature control are as determined by the function tempRadMalSet.

Property	M_R3

Formal	:	( n NAT (  numRad ) :             rad[n]. valveAct. noMalAct. adjustedEntity =  tempRadSet )
NL	:	The value adjusted by the machine for the radiator valves corresponds with the value intended by the temperature control for these actuators depending on the currently desired temperature. Note that all radiator valves in a room are always set to the same value. A specific value for a single radiator is not determined.